diff --git a/src/plugins/value/engine/partition.ml b/src/plugins/value/engine/partition.ml index 89545afeba4d9bcb8d78840c34df5dd9f82a2889..cedd0f86ffe906d00cbf8bddd9c274c63f78c046 100644 --- a/src/plugins/value/engine/partition.ml +++ b/src/plugins/value/engine/partition.ml @@ -137,12 +137,6 @@ let merge = KMap.merge let to_list (p : 'a partition) : 'a list = KMap.fold (fun _k x l -> x :: l) p [] -let map_filter (f : key -> 'a -> 'b option) (p : 'a partition) : 'b partition = - let opt_flatten (type a) (o : a option option) : a option = - Extlib.opt_conv None o - in - KMap.merge (fun k o _ -> opt_flatten (Extlib.opt_map (f k) o)) p KMap.empty - (* --- Partitioning actions --- *) @@ -473,4 +467,27 @@ struct let iter (f : state -> unit) (p : t) : unit = List.iter (fun (_k,x) -> f x) p + + let join_duplicate_keys (p : t) : t = + let cmp (k, _) (k', _) = Key.compare k k' in + let p = List.fast_sort cmp p in + let rec aux acc (key, state) = function + | [] -> (key, state) :: acc + | (key', state') :: tl -> + if Key.compare key key' = 0 + then aux acc (key, Abstract.Dom.join state state') tl + else aux ((key, state) :: acc) (key', state') tl + in + match p with + | [] | [_] -> p + | e :: tl -> aux [] e tl + + let filter_map (f: key -> state -> state option) (p : t) : t = + let rec aux = function + | [] -> [] + | (key, x) :: tl -> match f key x with + | Some y -> (key, y) :: (aux tl) + | None -> aux tl + in + aux p end diff --git a/src/plugins/value/engine/partition.mli b/src/plugins/value/engine/partition.mli index ed7a1211289140c3610e494d20d632008f8af0c2..6e5c2be9533defbb217881fd1a37a17f819a0cf1 100644 --- a/src/plugins/value/engine/partition.mli +++ b/src/plugins/value/engine/partition.mli @@ -82,7 +82,6 @@ val merge : (key -> 'a option -> 'b option -> 'c option) -> 'a partition -> val iter : (key -> 'a -> unit) -> 'a partition -> unit val filter : (key -> 'a -> bool) -> 'a partition -> 'a partition val map : ('a -> 'a) -> 'a partition -> 'a partition -val map_filter : (key -> 'a -> 'b option) -> 'a partition -> 'b partition (* Partitioning actions *) @@ -133,4 +132,7 @@ sig val transfer_states : (state -> state list) -> t -> t val iter : (state -> unit) -> t -> unit + val filter_map: (key -> state -> state option) -> t -> t + + val join_duplicate_keys: t -> t end diff --git a/src/plugins/value/engine/trace_partitioning.ml b/src/plugins/value/engine/trace_partitioning.ml index 2f0ed37ad9e69f9533f1f57043f93d9fdbb2e4ae..9c02b2708fe7e25415b7774dc777b7525c69a85e 100644 --- a/src/plugins/value/engine/trace_partitioning.ml +++ b/src/plugins/value/engine/trace_partitioning.ml @@ -170,9 +170,8 @@ struct if strategy <> Split_strategy.FullSplit then let apply action = - transfer_action flow action; - let p = Flow.to_partition flow.flow_states in - flow.flow_states <- Flow.of_partition p + let f = Flow.transfer_keys flow.flow_states action in + flow.flow_states <- Flow.join_duplicate_keys f in match Split_return.kf_strategy kf with (* SplitAuto already transformed into SplitEqList. *) @@ -258,8 +257,6 @@ struct let flow_states = List.fold_left Flow.transfer_keys flow_states actions in - (* Join states with unique keys *) - let partition = Flow.to_partition flow_states in (* Add states to the store but filter out already propagated states *) let update key current_state = (* Inclusion test *) @@ -288,8 +285,9 @@ struct (* Filter out already propagated states *) Extlib.opt_filter (fun s -> Index.add s dest.store_index) state in - let partition' = Partition.map_filter update partition in - { flow_states = Flow.of_partition partition' } + let flow = Flow.join_duplicate_keys flow_states in + let flow = Flow.filter_map update flow in + { flow_states = flow } let widen (w : widening) (f : flow) : bool = @@ -347,8 +345,8 @@ struct }; Some curr in - let p = Flow.to_partition f.flow_states in - let p' = Partition.map_filter widen_one p in - f.flow_states <- Flow.of_partition p'; + let flow = Flow.join_duplicate_keys f.flow_states in + let flow = Flow.filter_map widen_one flow in + f.flow_states <- flow; Flow.is_empty f.flow_states end