diff --git a/src/plugins/eva/domains/multidim/multidim_domain.ml b/src/plugins/eva/domains/multidim/multidim_domain.ml
index 2b2bb6301f28d2a3547714dce4c2c3e10f5314e9..2924a23612871f2dbbaa59c831ce7710cbb83180 100644
--- a/src/plugins/eva/domains/multidim/multidim_domain.ml
+++ b/src/plugins/eva/domains/multidim/multidim_domain.ml
@@ -611,7 +611,8 @@ struct
let narrow = join ~cache ~symmetric:false ~idempotent:true ~decide in
fun (m1,t1) (m2,t2) -> `Value (narrow m1 m2, join_tracked t1 t2)
- let join' ~oracle (m1,t1) (m2,t2) =
+ (* Precise join with oracle, but cannot be cached. *)
+ let precise_join ~oracle m1 m2 =
let open BaseMap in
let cache = Hptmap_sig.NoCache
and decide _ x1 x2 =
@@ -619,8 +620,27 @@ struct
and m2,r2 = Option.value ~default:V.top x2 in
Memory.join ~oracle m1 m2, Referers.union r1 r2 (* TODO: Remove tops *)
in
- generic_join ~cache ~symmetric:false ~idempotent:true ~decide m1 m2,
- join_tracked t1 t2
+ generic_join ~cache ~symmetric:false ~idempotent:true ~decide m1 m2
+
+ (* Optimized join without oracle. *)
+ let fast_join =
+ let open BaseMap in
+ let oracle _ _ = Int_val.top in
+ let cache = cache_name "fast_join"
+ and decide _ x1 x2 =
+ let m1, r1 = Option.value ~default:V.top x1
+ and m2, r2 = Option.value ~default:V.top x2 in
+ Memory.join ~oracle m1 m2, Referers.union r1 r2 (* TODO: Remove tops *)
+ in
+ generic_join ~cache ~symmetric:true ~idempotent:true ~decide
+
+ let join' ~oracle (m1, t1) (m2, t2) =
+ let m =
+ if Parameters.MultidimFastImprecise.get ()
+ then fast_join m1 m2
+ else precise_join ~oracle m1 m2
+ in
+ m, join_tracked t1 t2
let join s1 s2 =
let oracle = mk_bioracle s1 s2 in
@@ -890,21 +910,16 @@ struct
let relate _kf _bases _state = Base.SetLattice.empty
- let filter _kind bases (base_map,tracked : t) =
- BaseMap.filter (fun elt -> Base.Hptset.mem elt bases) base_map,
+ let filter _kind bases (base_map, tracked : t) =
+ BaseMap.inter_with_shape bases base_map,
Option.map (Tracking.inter bases) tracked
- let reuse _kf bases =
- let open BaseMap in
- let cache = Hptmap_sig.NoCache in
- let decide_both _key _v1 v2 = Some v2 in
- let decide_left key v1 =
- if Base.Hptset.mem key bases then None else Some v1
- in
- let reuse = merge ~cache ~symmetric:false ~idempotent:true
- ~decide_both ~decide_left:(Traversing decide_left) ~decide_right:Neutral
- in
- fun ~current_input:(m1,t1) ~previous_output:(m2,t2) ->
+ let reuse =
+ let cache = cache_name "reuse" in
+ let decide _key _v1 v2 = v2 in
+ let reuse = BaseMap.join ~cache ~symmetric:false ~idempotent:true ~decide in
+ fun _kf bases ~current_input:(m1,t1) ~previous_output:(m2,t2) ->
+ let m1 = BaseMap.diff_with_shape bases m1 in
reuse m1 m2, join_tracked t1 t2
end
@@ -923,15 +938,22 @@ let multidim_hook (module Abstract: Abstractions.S) : (module Abstractions.S) =
let join a b =
let r = join (set key Domain.top a) (set key Domain.top b) in
- let oracle state exp = (* TODO: cache results *)
- let v, _alarms = Eval.evaluate state exp in
- match v with
- | `Bottom -> Cvalue.V.top
- | `Value (_valuation,v) -> get_cval v
+ let oracle state =
+ let valuation_ref = ref Eval.Valuation.empty in
+ fun exp ->
+ let valuation = !valuation_ref in
+ let v, _alarms = Eval.evaluate ~valuation state exp in
+ match v with
+ | `Bottom -> Cvalue.V.top
+ | `Value (valuation, v) ->
+ valuation_ref := valuation;
+ get_cval v
in
+ let left_oracle = oracle a
+ and right_oracle = oracle b in
let oracle = function
- | Abstract_memory.Left -> convert_oracle (oracle a)
- | Abstract_memory.Right -> convert_oracle (oracle b)
+ | Abstract_memory.Left -> convert_oracle left_oracle
+ | Abstract_memory.Right -> convert_oracle right_oracle
in
let multidim = Domain.join' ~oracle (get_multidim a) (get_multidim b) in
set key multidim r
diff --git a/src/plugins/eva/domains/multidim/segmentation.ml b/src/plugins/eva/domains/multidim/segmentation.ml
index 475933251eaa60f4d2ca7ea589200eeeb63ce19b..3a9f3ce61ec69cf8c416f50c9e5e732ba2d5e920 100644
--- a/src/plugins/eva/domains/multidim/segmentation.ml
+++ b/src/plugins/eva/domains/multidim/segmentation.ml
@@ -288,21 +288,25 @@ struct
let eq ?(oracle=no_oracle) b1 b2 =
cmp ~oracle b1 b2 = Equal
+ let missing_bound kind b =
+ (* Do not warn when -eva-multidim-fast-imprecise is set, as it is expected
+ that bounds cannot be retrieved in this case. *)
+ if not (Parameters.MultidimFastImprecise.get ())
+ then
+ Self.warning ~current:true ~once:true
+ "Multidim domain: cannot retrieve %s for %a"
+ kind pretty b;
+ `Top
+
let lower_integer ~oracle b =
match Int_val.min_int (to_int_val ~oracle b) with
| Some l -> `Value l
- | None ->
- Self.warning ~current:true "cannot retrieve a lower bound for %a"
- pretty b;
- `Top
+ | None -> missing_bound "a lower bound" b
let upper_integer ~oracle b =
match Int_val.max_int (to_int_val ~oracle b) with
| Some u -> `Value u
- | None ->
- Self.warning ~current:true "cannot retrieve an upper bound for %a"
- pretty b;
- `Top
+ | None -> missing_bound "an upper bound" b
let lower_bound ~oracle b1 b2 =
if b1 == b2 || eq b1 b2 then `Value b1 else
@@ -870,8 +874,8 @@ struct
| `Value m -> m
| `Bottom -> assert false
| `Top ->
- Self.warning ~current:true
- "failed to introduce %a inside the array segmentation"
+ Self.warning ~current:true ~once:true
+ "Multidim domain: failed to introduce %a inside the array segmentation"
Bound.pretty b;
m
in
diff --git a/src/plugins/eva/parameters.ml b/src/plugins/eva/parameters.ml
index 6bd34e41303c915de0220d07de608ce1c0222721..9900dd5cc70f953e69095e7a1a3e02c8453f7105 100644
--- a/src/plugins/eva/parameters.ml
+++ b/src/plugins/eva/parameters.ml
@@ -355,6 +355,15 @@ module MultidimDisjunctiveInvariants = False
end)
let () = add_precision_dep MultidimDisjunctiveInvariants.parameter
+let () = Parameter_customize.set_group domains
+let () = Parameter_customize.is_invisible ()
+module MultidimFastImprecise = False
+ (struct
+ let option_name = "-eva-multidim-fast-imprecise"
+ let help = "Makes the multidim domain faster but less precise: \
+ the domain can lose more information when joining states."
+ end)
+let () = add_precision_dep MultidimFastImprecise.parameter
(* -------------------------------------------------------------------------- *)
(* --- Performance options --- *)
diff --git a/src/plugins/eva/parameters.mli b/src/plugins/eva/parameters.mli
index d477b8af08ab8777ec7c2e534df5b8a522707a1e..7fa79238485ed73982558724e55d2687172c97ae 100644
--- a/src/plugins/eva/parameters.mli
+++ b/src/plugins/eva/parameters.mli
@@ -45,6 +45,7 @@ module TracesProject: Parameter_sig.Bool
module MultidimSegmentLimit: Parameter_sig.Int
module MultidimDisjunctiveInvariants: Parameter_sig.Bool
+module MultidimFastImprecise: Parameter_sig.Bool
module AutomaticContextMaxDepth: Parameter_sig.Int
module AutomaticContextMaxWidth: Parameter_sig.Int