diff --git a/src/plugins/value/engine/partition.ml b/src/plugins/value/engine/partition.ml index bf2a5e2b66c3893bb605cd08c9e530ecf662ead8..8c690af3db9115b776b70cc37aab00181ce6d2e2 100644 --- a/src/plugins/value/engine/partition.ml +++ b/src/plugins/value/engine/partition.ml @@ -174,7 +174,7 @@ type action = | Branch of branch * int | Ration of rationing | Restrict of Cil_types.exp * Integer.t list - | Split of Cil_types.exp * split_kind * int + | Split of Cil_types.exp * split_kind * split_monitor | Merge of Cil_types.exp * split_kind | Update_dynamic_splits @@ -363,8 +363,7 @@ struct with Operation_failed -> [(key,state)] - let split ~limit (kind : split_kind) (exp : Cil_types.exp) (p : t) = - let monitor = new_monitor limit in + let split ~monitor (kind : split_kind) (exp : Cil_types.exp) (p : t) = let add_split acc (key,state) = split_state ~monitor kind exp key state @ acc in @@ -389,8 +388,8 @@ struct List.map (fun (k,x) -> f k x, x) p let transfer_keys p = function - | Split (expr, kind, limit) -> - split ~limit kind expr p + | Split (expr, kind, monitor) -> + split ~monitor kind expr p | Update_dynamic_splits -> update_dynamic_splits p diff --git a/src/plugins/value/engine/partition.mli b/src/plugins/value/engine/partition.mli index 52449a00e20fca102d2005f51bb846907881301b..1a48bf6e154c36c54bd8cee64fba21cea2a7f1f7 100644 --- a/src/plugins/value/engine/partition.mli +++ b/src/plugins/value/engine/partition.mli @@ -90,6 +90,12 @@ type unroll_limit = states are then split or merged accordingly. *) type split_kind = Static | Dynamic +(** Split monitor: prevents splits from generating too many states. *) +type split_monitor + +(** Creates a new monitor that allows to split up to [split_limit] states. *) +val new_monitor: split_limit:int -> split_monitor + (** These actions redefine the partitioning by updating keys or spliting states. They are applied to all the pair (key, state) in a flow. *) type action = @@ -127,12 +133,14 @@ type action = - all other states are joined together. Previous rationing is erased and replaced by this new stamping. Implementation of the option -eva-split-return. *) - | Split of Cil_types.exp * split_kind * int - (** [Split (exp, kind, max)] tries to separate states such as the [exp] + | Split of Cil_types.exp * split_kind * split_monitor + (** [Split (exp, kind, monitor)] tries to separate states such as the [exp] evaluates to a singleton value in each state in the flow. If necessary and possible, splits states into multiple states. States in which the [exp] evaluates to different values will be kept separate. Gives up the split - if [exp] evaluates to more than [max] values. *) + if [exp] evaluates to more than [limit] values, [limit] being the split + limit of the [monitor]. A same monitor can be used for successive splits + on different flows. *) | Merge of Cil_types.exp * split_kind (** Forgets the split of an expression: states that were kept separate only by the split of this expression will be joined together. *) diff --git a/src/plugins/value/engine/partitioning_parameters.ml b/src/plugins/value/engine/partitioning_parameters.ml index 100803fa8c3d2147dbfb7ade5206b73d76043674..b480f4e425da2b3ce6f1dd62384c0ffd326a1151 100644 --- a/src/plugins/value/engine/partitioning_parameters.ml +++ b/src/plugins/value/engine/partitioning_parameters.ml @@ -109,7 +109,8 @@ struct let add name l = try let vi = Globals.Vars.find_from_astinfo name VGlobal in - Partition.Split (Cil.evar vi, Partition.Dynamic, split_limit) :: l + let monitor = Partition.new_monitor ~split_limit in + Partition.Split (Cil.evar vi, Partition.Dynamic, monitor) :: l with Not_found -> warn ~current:false "cannot find the global variable %s for value \ partitioning" name; @@ -121,9 +122,10 @@ struct let kind = Partition.Static in let map_annot acc t = try + let monitor = Partition.new_monitor ~split_limit in let action = match t with - | FlowSplit t -> Partition.Split (term_to_exp t, kind, split_limit) + | FlowSplit t -> Partition.Split (term_to_exp t, kind, monitor) | FlowMerge t -> Partition.Merge (term_to_exp t, kind) in action :: acc