diff --git a/src/plugins/value/Eva.mli b/src/plugins/value/Eva.mli index 686e7ab24143eb3e8109230b809c2b36ef7955b8..97761d74c2583992f4fcd2a463e8380e860766c4 100644 --- a/src/plugins/value/Eva.mli +++ b/src/plugins/value/Eva.mli @@ -87,10 +87,14 @@ module Eva_annotations: sig | UnrollAmount of Cil_types.term (** Unroll the n first iterations. *) | UnrollFull (** Unroll amount defined by -eva-default-loop-unroll. *) + type split_kind = Static | Dynamic + (** Split/merge annotations for value partitioning. *) type flow_annotation = - | FlowSplit of Cil_types.term (** Split states according to a term. *) - | FlowMerge of Cil_types.term (** Merge states separated by a previous split. *) + | FlowSplit of Cil_types.term * split_kind + (** Split states according to a term. *) + | FlowMerge of Cil_types.term + (** Merge states separated by a previous split. *) val add_slevel_annot : emitter:Emitter.t -> loc:Cil_types.location -> Cil_types.stmt -> slevel_annotation -> unit diff --git a/src/plugins/value/partitioning/partition.ml b/src/plugins/value/partitioning/partition.ml index a7138c912d6edcd7e3316299c63486fc1e5ee5aa..2325162fd0ccd2e1557bc5b3fbf8e5c43fd4d68a 100644 --- a/src/plugins/value/partitioning/partition.ml +++ b/src/plugins/value/partitioning/partition.ml @@ -166,7 +166,7 @@ type unroll_limit = | IntLimit of int | AutoUnroll of Cil_types.stmt * int * int -type split_kind = Static | Dynamic +type split_kind = Eva_annotations.split_kind = Static | Dynamic type action = | Enter_loop of unroll_limit @@ -176,7 +176,7 @@ type action = | Ration of rationing | Restrict of Cil_types.exp * Integer.t list | Split of Cil_types.exp * split_kind * split_monitor - | Merge of Cil_types.exp * split_kind + | Merge of Cil_types.exp | Update_dynamic_splits exception InvalidAction @@ -471,11 +471,9 @@ struct | Restrict (expr, expected_values) -> fun k s -> { k with ration_stamp = stamp_by_value expr expected_values s} - | Merge (exp, Static) -> fun k _x -> - { k with static_split = ExpMap.remove exp k.static_split } - - | Merge (exp, Dynamic) -> fun k _x -> - { k with dynamic_split = ExpMap.remove exp k.dynamic_split } + | Merge exp -> fun k _x -> + { k with static_split = ExpMap.remove exp k.static_split; + dynamic_split = ExpMap.remove exp k.dynamic_split } in map_keys transfer p diff --git a/src/plugins/value/partitioning/partition.mli b/src/plugins/value/partitioning/partition.mli index a5a3a569b37aa90168a42418279e6918552c9450..1b773efe9871741fa80dccd87cd5d8043a3f3472 100644 --- a/src/plugins/value/partitioning/partition.mli +++ b/src/plugins/value/partitioning/partition.mli @@ -92,7 +92,7 @@ type unroll_limit = split point, and the key is then kept unchanged until a merge. - dynamic splits are regularly redone: the expression is re-evaluated, and states are then split or merged accordingly. *) -type split_kind = Static | Dynamic +type split_kind = Eva_annotations.split_kind = Static | Dynamic (** Split monitor: prevents splits from generating too many states. *) type split_monitor @@ -145,7 +145,7 @@ type action = 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 + | Merge of Cil_types.exp (** Forgets the split of an expression: states that were kept separate only by the split of this expression will be joined together. *) | Update_dynamic_splits diff --git a/src/plugins/value/partitioning/partitioning_parameters.ml b/src/plugins/value/partitioning/partitioning_parameters.ml index d77a88990c76c64b530c0617eff3e2b26d58fef8..b3609a90cc6a44a40b5f9c9ba369a3426c9b0cef 100644 --- a/src/plugins/value/partitioning/partitioning_parameters.ml +++ b/src/plugins/value/partitioning/partitioning_parameters.ml @@ -125,14 +125,13 @@ struct ValuePartitioning.fold add [] let flow_actions stmt = - 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, monitor) - | FlowMerge t -> Partition.Merge (term_to_exp t, kind) + | FlowSplit (t, kind) -> Partition.Split (term_to_exp t, kind, monitor) + | FlowMerge t -> Partition.Merge (term_to_exp t) in action :: acc with diff --git a/src/plugins/value/utils/eva_annotations.ml b/src/plugins/value/utils/eva_annotations.ml index 9cbcd7d3f9d2813ca42019e4c764488b0dfd55fb..adaf06945a43d70cf60b9961a85b01753885ebf3 100644 --- a/src/plugins/value/utils/eva_annotations.ml +++ b/src/plugins/value/utils/eva_annotations.ml @@ -33,8 +33,10 @@ type unroll_annotation = | UnrollAmount of Cil_types.term | UnrollFull +type split_kind = Static | Dynamic + type flow_annotation = - | FlowSplit of term + | FlowSplit of term * split_kind | FlowMerge of term type taint_annotation = Cil_types.term list @@ -232,6 +234,12 @@ module Merge = Register (struct let is_loop_annot = false end) +module DynamicSplit = Register (struct + include SimpleTermAnnotation + let name = "dynamic_split" + let is_loop_annot = false + end) + module Taint = Register (struct include ListTermAnnotation let name = "taint" @@ -248,7 +256,8 @@ let get_slevel_annot stmt = let get_unroll_annot stmt = Unroll.get stmt let get_flow_annot stmt = - List.map (fun a -> FlowSplit a) (Split.get stmt) @ + List.map (fun a -> FlowSplit (a, Static)) (Split.get stmt) @ + List.map (fun a -> FlowSplit (a, Dynamic)) (DynamicSplit.get stmt) @ List.map (fun a -> FlowMerge a) (Merge.get stmt) @@ -257,7 +266,8 @@ let add_slevel_annot = Slevel.add let add_unroll_annot = Unroll.add let add_flow_annot ~emitter ~loc stmt = function - | FlowSplit annot -> Split.add ~emitter ~loc stmt annot + | FlowSplit (annot, Static) -> Split.add ~emitter ~loc stmt annot + | FlowSplit (annot, Dynamic) -> DynamicSplit.add ~emitter ~loc stmt annot | FlowMerge annot -> Merge.add ~emitter ~loc stmt annot diff --git a/src/plugins/value/utils/eva_annotations.mli b/src/plugins/value/utils/eva_annotations.mli index 2299ead597d043d37a436f870f2958c88decd946..629f8ffe5adb5b1116e5f1214be649bbfb04ca6d 100644 --- a/src/plugins/value/utils/eva_annotations.mli +++ b/src/plugins/value/utils/eva_annotations.mli @@ -38,8 +38,10 @@ type unroll_annotation = | UnrollAmount of Cil_types.term | UnrollFull +type split_kind = Static | Dynamic + type flow_annotation = - | FlowSplit of Cil_types.term + | FlowSplit of Cil_types.term * split_kind | FlowMerge of Cil_types.term type taint_annotation = Cil_types.term list