diff --git a/src/kernel_services/abstract_interp/abstract_memory.ml b/src/kernel_services/abstract_interp/abstract_memory.ml index e848f1dc01800239574f9de00650db40c260d61b..3abafeefb83011d7da6db8c567b2353ebd7441eb 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 32ac5f50cb63672f3ea1031a3780082e84c187cb..296116384feb36ec443201a9df8fd09f895470bb 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 82ae326f38f053823b7443d76259536b63b855fc..7e99502ba9d6e257e7de2e91e42ba1de7e03284c 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 d09607a544dc82f0a5f7f3585eb2709ff97a6e25..9dbe62ba5ad8f1ca4eaa4a6f233d3062c2033376 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 6f45638c5ca84bb224e0112612ebd5a7f5f8347f..335d9afe2245d82a502f6dbde5e405aad9d97997 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 343affc156a2cd89da7662aa4776904eb8328b0a..b540f066a700df4baadda33f45a2333c359a2367 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},