[Eva] Multidim domain: optimized but imprecise join.

Disabled by default,
enabled by a new invisible parameter -eva-multidim-fast-imprecise.

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

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

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                                                --- *)

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