From efc29e71cdc5040b4b48458291270f5f7f2b5e6b Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Fri, 3 Dec 2021 18:35:02 +0100
Subject: [PATCH] [Eva] multidim: the limit on the number of segments is now a
parameter
---
.../abstract_interp/abstract_memory.ml | 10 +++++++---
.../abstract_interp/abstract_memory.mli | 6 ++++++
src/plugins/value/domains/multidim_domain.ml | 5 ++++-
src/plugins/value/parameters.ml | 12 ++++++++++++
src/plugins/value/parameters.mli | 2 ++
tests/value/oracle/multidim.res.oracle | 4 +---
6 files changed, 32 insertions(+), 7 deletions(-)
diff --git a/src/kernel_services/abstract_interp/abstract_memory.ml b/src/kernel_services/abstract_interp/abstract_memory.ml
index e848f1dc018..3abafeefb83 100644
--- a/src/kernel_services/abstract_interp/abstract_memory.ml
+++ b/src/kernel_services/abstract_interp/abstract_memory.ml
@@ -170,6 +170,7 @@ end
module type Config =
sig
val deps : State.t list
+ val slice_limit : unit -> int
end
@@ -949,10 +950,13 @@ struct
{ m with segments = aux [] m.start m.segments }
let limit_size ~oracle m =
- let rec aux m n =
- if n <= 0 then m else aux (remove_oldest_bounds ~oracle m) (n - 1)
+ let limit = Config.slice_limit () in
+ let rec aux m =
+ if List.length m.segments <= limit
+ then m
+ else aux (remove_oldest_bounds ~oracle m)
in
- aux m (List.length m.segments - segments_limit)
+ aux m
(* TODO: partitioning strategies
1. reinforcement without loss
diff --git a/src/kernel_services/abstract_interp/abstract_memory.mli b/src/kernel_services/abstract_interp/abstract_memory.mli
index 32ac5f50cb6..296116384fe 100644
--- a/src/kernel_services/abstract_interp/abstract_memory.mli
+++ b/src/kernel_services/abstract_interp/abstract_memory.mli
@@ -59,7 +59,13 @@ end
module type Config =
sig
+ (* Dependencies of the hash-consing table. The table will be cleared
+ whenever one of those dependencies is cleared. *)
val deps : State.t list
+
+ (* Limit on the number of slice after a write for array segmentations.
+ Makes sense above or equal to 1, though below 3 is counter-productive. *)
+ val slice_limit : unit -> int
end
diff --git a/src/plugins/value/domains/multidim_domain.ml b/src/plugins/value/domains/multidim_domain.ml
index 82ae326f38f..7e99502ba9d 100644
--- a/src/plugins/value/domains/multidim_domain.ml
+++ b/src/plugins/value/domains/multidim_domain.ml
@@ -184,7 +184,10 @@ end
module Memory =
struct
- module Config = struct let deps = [Ast.self] end
+ module Config = struct
+ let deps = [Ast.self]
+ let slice_limit = Value_parameters.MultidimSegmentLimit.get
+ end
module Memory = Abstract_memory.TypedMemory (Config) (Value)
module Prototype =
diff --git a/src/plugins/value/parameters.ml b/src/plugins/value/parameters.ml
index d09607a544d..9dbe62ba5ad 100644
--- a/src/plugins/value/parameters.ml
+++ b/src/plugins/value/parameters.ml
@@ -336,6 +336,18 @@ module TracesProject = Bool
let default = false
end)
+let () = Parameter_customize.set_group domains
+module MultidimSegmentLimit = Int
+ (struct
+ let option_name = "-eva-multidim-segment-limit"
+ let arg_name = "N"
+ let help = "Limit the number of segments in the abstraction of arrays."
+ let default = 8
+ end)
+let () = MultidimSegmentLimit.set_range ~min:3 ~max:max_int
+let () = add_precision_dep MultidimSegmentLimit.parameter
+
+
(* -------------------------------------------------------------------------- *)
(* --- Performance options --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/value/parameters.mli b/src/plugins/value/parameters.mli
index 6f45638c5ca..335d9afe224 100644
--- a/src/plugins/value/parameters.mli
+++ b/src/plugins/value/parameters.mli
@@ -43,6 +43,8 @@ module TracesUnifyLoop: Parameter_sig.Bool
module TracesDot: Parameter_sig.Filepath
module TracesProject: Parameter_sig.Bool
+module MultidimSegmentLimit: Parameter_sig.Int
+
module AutomaticContextMaxDepth: Parameter_sig.Int
module AutomaticContextMaxWidth: Parameter_sig.Int
diff --git a/tests/value/oracle/multidim.res.oracle b/tests/value/oracle/multidim.res.oracle
index 343affc156a..b540f066a70 100644
--- a/tests/value/oracle/multidim.res.oracle
+++ b/tests/value/oracle/multidim.res.oracle
@@ -169,9 +169,7 @@
Frama_C_domain_show_each:
t : # cvalue: {0}
# multidim: {
- [0 .. 90] = {0},
- [91] = {0},
- [92] = {0},
+ [0 .. 92] = {0},
[93] = {0},
[94] = {0},
[95] = {0},
--
GitLab