From 4f89adfd1b01b56b8a8e1d9579c126930f148e69 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 21 Jul 2023 18:42:28 +0200
Subject: [PATCH] [Eva] Multidim domain: optimized but imprecise join.
Disabled by default,
enabled by a new invisible parameter -eva-multidim-fast-imprecise.
---
.../eva/domains/multidim/multidim_domain.ml | 26 ++++++++++++++++---
.../eva/domains/multidim/segmentation.ml | 22 +++++++++-------
src/plugins/eva/parameters.ml | 9 +++++++
src/plugins/eva/parameters.mli | 1 +
4 files changed, 45 insertions(+), 13 deletions(-)
diff --git a/src/plugins/eva/domains/multidim/multidim_domain.ml b/src/plugins/eva/domains/multidim/multidim_domain.ml
index 26d4bab6710..2924a236128 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 5a429105dd7..3a9f3ce61ec 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 6bd34e41303..9900dd5cc70 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 d477b8af08a..7fa79238485 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
--
GitLab