From 1078b9d418331718a504dad7683b865d2f636f76 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 28 Jan 2020 13:45:23 +0100
Subject: [PATCH] [Eva] Uses Map.union instead of Map.merge.
---
.../value/engine/subdivided_evaluation.ml | 14 +++---
src/plugins/value/legacy/eval_terms.ml | 8 +---
src/plugins/value/utils/structure.ml | 9 +---
src/plugins/value/utils/value_results.ml | 8 +---
src/plugins/value_types/widen_type.ml | 45 +++++++------------
5 files changed, 27 insertions(+), 57 deletions(-)
diff --git a/src/plugins/value/engine/subdivided_evaluation.ml b/src/plugins/value/engine/subdivided_evaluation.ml
index b832e789d36..9a2864ae1c1 100644
--- a/src/plugins/value/engine/subdivided_evaluation.ml
+++ b/src/plugins/value/engine/subdivided_evaluation.ml
@@ -67,16 +67,12 @@ let union expr depth map1 map2 =
let top = ref LvalSet.empty in
(* Lvalues such that a lvalue from [!top] appears in their subexpression. *)
let deps = ref LvalSet.empty in
- let merge lval a b = match a, b with
- | None, None -> None
- | Some x, None
- | None, Some x -> Some x
- | Some (_, _, deps1), Some (_, _, deps2) ->
- top := LvalSet.add lval !top;
- deps := LvalSet.union (LvalSet.union deps1 deps2) !deps;
- Some (expr, depth, LvalSet.union deps1 deps2)
+ let merge lval (_, _, deps1) (_, _, deps2) =
+ top := LvalSet.add lval !top;
+ deps := LvalSet.union (LvalSet.union deps1 deps2) !deps;
+ Some (expr, depth, LvalSet.union deps1 deps2)
in
- let map = LvalMap.merge merge map1 map2 in
+ let map = LvalMap.union merge map1 map2 in
LvalMap.mapi
(fun lval (e, d, lvs) ->
(* Alls lvalues in [expr] now appear in the subexpression of [!top]. *)
diff --git a/src/plugins/value/legacy/eval_terms.ml b/src/plugins/value/legacy/eval_terms.ml
index 291139e5ccd..44ac39bcd7a 100644
--- a/src/plugins/value/legacy/eval_terms.ml
+++ b/src/plugins/value/legacy/eval_terms.ml
@@ -164,13 +164,9 @@ let find_or_alarm ~alarm_mode state loc =
type labels_states = Cvalue.Model.t Logic_label.Map.t
let join_label_states m1 m2 =
- let aux _ s1 s2 = match s1, s2 with
- | None, None -> None
- | Some s, None | None, Some s -> Some s
- | Some s1, Some s2 -> Some (Cvalue.Model.join s1 s2)
- in
+ let aux _ s1 s2 = Some (Cvalue.Model.join s1 s2) in
if m1 == m2 then m1
- else Logic_label.Map.merge aux m1 m2
+ else Logic_label.Map.union aux m1 m2
(* The logic can refer to the state at other points of the program
using labels. [e_cur] indicates the current label (in changes when
diff --git a/src/plugins/value/utils/structure.ml b/src/plugins/value/utils/structure.ml
index c30e307d2f8..02faf9f20ee 100644
--- a/src/plugins/value/utils/structure.ml
+++ b/src/plugins/value/utils/structure.ml
@@ -140,11 +140,6 @@ module Open
type 'a getter = Get : ('a, 'b) get -> 'a getter
- let merge _k a b = match a, b with
- | Some _, _ -> a
- | _, Some _ -> b
- | None, None -> assert false
-
let lift_get f (Get (key, get)) = Get (key, fun t -> get (f t))
let rec compute_getters : type a. a structure -> (a getter) KMap.t = function
@@ -153,7 +148,7 @@ module Open
| Node (left, right) ->
let l = compute_getters left and r = compute_getters right in
let l = KMap.map (lift_get fst) l and r = KMap.map (lift_get snd) r in
- KMap.merge merge l r
+ KMap.union (fun _k a _b -> Some a) l r
let getters = compute_getters M.structure
let get (type a) (key: a Shape.key) : (M.t -> a) option =
@@ -177,7 +172,7 @@ module Open
let l = compute_setters left and r = compute_setters right in
let l = KMap.map (lift_set (fun set (l, r) -> set l, r)) l
and r = KMap.map (lift_set (fun set (l, r) -> l, set r)) r in
- KMap.merge merge l r
+ KMap.union (fun _k a _b -> Some a) l r
let setters = compute_setters M.structure
let set (type a) (key: a Shape.key) : (a -> M.t -> M.t) =
diff --git a/src/plugins/value/utils/value_results.ml b/src/plugins/value/utils/value_results.ml
index d82bc2853b2..57748e2f270 100644
--- a/src/plugins/value/utils/value_results.ml
+++ b/src/plugins/value/utils/value_results.ml
@@ -319,12 +319,8 @@ let merge r1 r2 =
| True, True -> True
in
let merge_callers _ m1 m2 =
- let aux _kf s1 s2 = match s1, s2 with
- | None, None -> None
- | None, s | s, None -> s
- | Some s1, Some s2 -> Some (Stmt.Set.union s1 s2)
- in
- Kernel_function.Map.merge aux m1 m2
+ let aux _kf s1 s2 = Some (Stmt.Set.union s1 s2) in
+ Kernel_function.Map.union aux m1 m2
in
let merge_s_cs = StmtH.merge merge_cs in
let main = match r1.main, r2.main with
diff --git a/src/plugins/value_types/widen_type.ml b/src/plugins/value_types/widen_type.ml
index ad9bdd90604..55917e30b50 100644
--- a/src/plugins/value_types/widen_type.ml
+++ b/src/plugins/value_types/widen_type.ml
@@ -88,40 +88,33 @@ include Datatype.Make(struct
end)
let join wh1 wh2 =
- let map_merge s_join os1 os2 =
- match os1, os2 with
- | Some bs1, Some bs2 -> Some (s_join bs1 bs2)
- | Some bs, None | None, Some bs -> Some bs
- | None, None -> None
- in
+ let map_union s_join _key bs1 bs2 = Some (s_join bs1 bs2) in
{ priority_bases =
- Stmt.Map.merge (fun _key -> map_merge Base.Set.union)
+ Stmt.Map.union (map_union Base.Set.union)
wh1.priority_bases wh2.priority_bases;
default_hints =
Ival.Widen_Hints.union wh1.default_hints wh2.default_hints;
default_float_hints =
Fc_float.Widen_Hints.union wh1.default_float_hints wh2.default_float_hints;
default_hints_by_stmt =
- Stmt.Map.merge (fun _key -> map_merge Ival.Widen_Hints.union)
+ Stmt.Map.union (map_union Ival.Widen_Hints.union)
wh1.default_hints_by_stmt wh2.default_hints_by_stmt;
default_float_hints_by_stmt =
- Stmt.Map.merge (fun _key -> map_merge Fc_float.Widen_Hints.union)
+ Stmt.Map.union (map_union Fc_float.Widen_Hints.union)
wh1.default_float_hints_by_stmt wh2.default_float_hints_by_stmt;
hints_by_addr =
- Base.Map.merge (fun _key -> map_merge Ival.Widen_Hints.union)
+ Base.Map.union (map_union Ival.Widen_Hints.union)
wh1.hints_by_addr wh2.hints_by_addr;
float_hints_by_addr =
- Base.Map.merge (fun _key -> map_merge Fc_float.Widen_Hints.union)
+ Base.Map.union (map_union Fc_float.Widen_Hints.union)
wh1.float_hints_by_addr wh2.float_hints_by_addr;
hints_by_addr_by_stmt =
- Stmt.Map.merge (fun _key ->
- map_merge (Base.Map.merge
- (fun _key -> map_merge Ival.Widen_Hints.union)))
+ Stmt.Map.union
+ (map_union (Base.Map.union (map_union Ival.Widen_Hints.union)))
wh1.hints_by_addr_by_stmt wh2.hints_by_addr_by_stmt;
float_hints_by_addr_by_stmt =
- Stmt.Map.merge (fun _key ->
- map_merge (Base.Map.merge
- (fun _key -> map_merge Fc_float.Widen_Hints.union)))
+ Stmt.Map.union
+ (map_union (Base.Map.union (map_union Fc_float.Widen_Hints.union)))
wh1.float_hints_by_addr_by_stmt wh2.float_hints_by_addr_by_stmt;
}
@@ -196,23 +189,17 @@ let hints_from_keys stmt h =
let int_hints_by_base =
try
let at_stmt = Stmt.Map.find stmt h.hints_by_addr_by_stmt in
- Base.Map.merge (fun _b os1 os2 ->
- match os1, os2 with
- | Some s1, Some s2 -> Some (Ival.Widen_Hints.union s1 s2)
- | Some s, None | None, Some s -> Some s
- | None, None -> None
- ) at_stmt h.hints_by_addr
+ Base.Map.union
+ (fun _b s1 s2 -> Some (Ival.Widen_Hints.union s1 s2))
+ at_stmt h.hints_by_addr
with Not_found -> h.hints_by_addr
in
let float_hints_by_base =
try
let at_stmt = Stmt.Map.find stmt h.float_hints_by_addr_by_stmt in
- Base.Map.merge (fun _b os1 os2 ->
- match os1, os2 with
- | Some s1, Some s2 -> Some (Fc_float.Widen_Hints.union s1 s2)
- | Some s, None | None, Some s -> Some s
- | None, None -> None
- ) at_stmt h.float_hints_by_addr
+ Base.Map.union
+ (fun _b s1 s2 -> Some (Fc_float.Widen_Hints.union s1 s2))
+ at_stmt h.float_hints_by_addr
with Not_found -> h.float_hints_by_addr
in
let prio =
--
GitLab