diff --git a/src/plugins/eva/domains/multidim/multidim_domain.ml b/src/plugins/eva/domains/multidim/multidim_domain.ml index 26d4bab671088b8b01b05c297bf3981dd97820c1..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 diff --git a/src/plugins/eva/domains/multidim/segmentation.ml b/src/plugins/eva/domains/multidim/segmentation.ml index 5a429105dd758678dce03e0ed8ce61fd8ea3fd82..3a9f3ce61ec69cf8c416f50c9e5e732ba2d5e920 100644 --- a/src/plugins/eva/domains/multidim/segmentation.ml +++ b/src/plugins/eva/domains/multidim/segmentation.ml @@ -288,23 +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 ~once:true - "Multidim domain: 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 ~once:true - "Multidim domain: 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 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