[Eva] multidim: the limit on the number of segments is now a parameter

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

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
 
 

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 =

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

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
 

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},