diff --git a/src/plugins/value/engine/iterator.ml b/src/plugins/value/engine/iterator.ml
index b22c6f12e9f4e828c71980ed072f00ee33f5af0d..a7f9573a00e766c65e71cf51f6b8b1fb6c1ce82d 100644
--- a/src/plugins/value/engine/iterator.ml
+++ b/src/plugins/value/engine/iterator.ml
@@ -407,34 +407,32 @@ module Make_Dataflow
end
let process_partitioning_transitions (v1 : vertex) (v2 : vertex)
- (transition : vertex transition) (f : flow) : unit =
+ (transition : vertex transition) (flow : flow) : flow =
(* Split return *)
- begin match transition with
- | Return (return_exp, _) ->
- Partition.split_return f return_exp
- | _ -> ()
- end;
+ let flow = match transition with
+ | Return (return_exp, _) -> Partition.split_return flow return_exp
+ | _ -> flow
+ in
(* Loop transitions *)
let the_stmt v = Extlib.the v.vertex_start_of in
- let enter_loop v =
- Partition.transfer (lift (Domain.enter_loop (the_stmt v))) f;
- Partition.enter_loop f (the_stmt v)
- and leave_loop v =
- Partition.transfer (lift (Domain.leave_loop (the_stmt v))) f;
- Partition.leave_loop f (the_stmt v)
- and incr_loop_counter v =
- Partition.transfer (lift (Domain.incr_loop_counter (the_stmt v))) f;
- Partition.next_loop_iteration f (the_stmt v)
+ let enter_loop f v =
+ let f = Partition.enter_loop f (the_stmt v) in
+ Partition.transfer (lift (Domain.enter_loop (the_stmt v))) f
+ and leave_loop f v =
+ let f = Partition.leave_loop f (the_stmt v) in
+ Partition.transfer (lift (Domain.leave_loop (the_stmt v))) f
+ and incr_loop_counter f v =
+ let f = Partition.next_loop_iteration f (the_stmt v) in
+ Partition.transfer (lift (Domain.incr_loop_counter (the_stmt v))) f
in
let loops_left, loops_entered =
Interpreted_automata.get_wto_index_diff kf v1 v2
and loop_incr =
Interpreted_automata.is_back_edge kf (v1,v2)
in
- List.iter leave_loop loops_left;
- List.iter enter_loop loops_entered;
- if loop_incr then
- incr_loop_counter v2
+ let flow = List.fold_left leave_loop flow loops_left in
+ let flow = List.fold_left enter_loop flow loops_entered in
+ if loop_incr then incr_loop_counter flow v2 else flow
let process_edge (v1,e,v2 : G.edge) : flow =
let {edge_transition=transition; edge_kinstr=kinstr} = e in
@@ -444,8 +442,8 @@ module Make_Dataflow
check_signals ();
current_ki := kinstr;
Cil.CurrentLoc.set e.edge_loc;
- Partition.transfer (transfer_transition transition) flow;
- process_partitioning_transitions v1 v2 transition flow;
+ let flow = Partition.transfer (transfer_transition transition) flow in
+ let flow = process_partitioning_transitions v1 v2 transition flow in
if not (Partition.is_empty_flow flow) then
edge_info.fireable <- true;
flow
@@ -476,45 +474,44 @@ module Make_Dataflow
(* Get vertex store *)
let store = get_vertex_store v in
(* Join incoming s tates *)
- let f = Partition.join sources store in
- begin match v.vertex_start_of with
+ let flow = Partition.join sources store in
+ let flow =
+ match v.vertex_start_of with
| Some stmt ->
(* Callbacks *)
- call_statement_callbacks stmt f;
+ call_statement_callbacks stmt flow;
(* Transfer function associated to the statement *)
- Partition.transfer (transfer_statement stmt) f;
+ let flow = Partition.transfer (transfer_statement stmt) flow in
(* Output slevel related things *)
let store_size = Partition.store_size store in
output_slevel store_size;
(* Debug informations *)
Value_parameters.debug ~dkey ~current:true
"reached statement %d with %d / %d eternal states, %d to propagate"
- stmt.sid store_size (slevel stmt) (Partition.flow_size f);
- | _ -> ()
- end;
+ stmt.sid store_size (slevel stmt) (Partition.flow_size flow);
+ flow
+ | _ -> flow
+ in
(* Widen if necessary *)
- let stable =
- if Partition.is_empty_flow f then
- true
- else if widening then begin
- let stable = Partition.widen (get_vertex_widening v) f in
+ let flow =
+ if widening && not (Partition.is_empty_flow flow) then begin
+ let flow = Partition.widen (get_vertex_widening v) flow in
(* Try to correct over-widenings *)
let correct_over_widening stmt =
(* Do *not* record the status after interpreting the annotation
here. Possible unproven assertions have already been recorded
when the assertion has been interpreted the first time higher
in this function. *)
- Partition.transfer (transfer_annotations stmt ~record:false) f
+ Partition.transfer (transfer_annotations stmt ~record:false) flow
in
- Extlib.may correct_over_widening v.vertex_start_of;
- stable
+ Extlib.may_map correct_over_widening ~dft:flow v.vertex_start_of
end else
- false
+ flow
in
(* Dispatch to successors *)
- List.iter (fun into -> Partition.fill f ~into) (get_succ_tanks v);
- (* Return wether the iterator should stop or not *)
- stable
+ List.iter (fun into -> Partition.fill flow ~into) (get_succ_tanks v);
+ (* Return whether the iterator should stop or not *)
+ Partition.is_empty_flow flow
let process_vertex ?(widening : bool = false) (v : vertex) : bool =
(* Process predecessors *)
diff --git a/src/plugins/value/engine/trace_partitioning.ml b/src/plugins/value/engine/trace_partitioning.ml
index 96c8bc8f5afb1c72207353101382a350536a074a..eaa7a3ca361da88cfb2f72b946342221f87eb983 100644
--- a/src/plugins/value/engine/trace_partitioning.ml
+++ b/src/plugins/value/engine/trace_partitioning.ml
@@ -50,9 +50,7 @@ struct
mutable store_size : int;
}
- type flow = {
- mutable flow_states : Flow.t;
- }
+ type flow = Flow.t
type tank = {
mutable tank_states : state partition;
@@ -85,8 +83,7 @@ struct
store_size = 0;
}
- let empty_flow () : flow =
- { flow_states = Flow.empty }
+ let empty_flow : flow = Flow.empty
let empty_tank () : tank =
{ tank_states = Partition.empty }
@@ -109,8 +106,8 @@ struct
let pretty_store (fmt : Format.formatter) (s : store) : unit =
Partition.iter (fun _key state -> Domain.pretty fmt state) s.store_partition
- let pretty_flow (fmt : Format.formatter) (p : flow) =
- Flow.iter (Domain.pretty fmt) p.flow_states
+ let pretty_flow (fmt : Format.formatter) (flow : flow) =
+ Flow.iter (Domain.pretty fmt) flow
(* Accessors *)
@@ -123,14 +120,14 @@ struct
| [] -> `Bottom
| v1 :: l -> `Value (List.fold_left Domain.join v1 l)
- let contents (f : flow) : state list =
- Flow.to_list f.flow_states
+ let contents (flow : flow) : state list =
+ Flow.to_list flow
let is_empty_store (s : store) : bool =
Partition.is_empty s.store_partition
- let is_empty_flow (f : flow) : bool =
- Flow.is_empty f.flow_states
+ let is_empty_flow (flow : flow) : bool =
+ Flow.is_empty flow
let is_empty_tank (t : tank) : bool =
Partition.is_empty t.tank_states
@@ -138,8 +135,8 @@ struct
let store_size (s : store) : int =
s.store_size
- let flow_size (f : flow) : int =
- Flow.size f.flow_states
+ let flow_size (flow : flow) : int =
+ Flow.size flow
let tank_size (t : tank) : int =
Partition.size t.tank_states
@@ -147,27 +144,24 @@ struct
(* Partition transfer functions *)
- let transfer_action p action =
- p.flow_states <- Flow.transfer_keys p.flow_states action
-
- let enter_loop (p : flow) (i : stmt) : unit =
- transfer_action p (Enter_loop (unroll i))
+ let enter_loop (flow : flow) (i : stmt) : flow =
+ Flow.transfer_keys flow (Enter_loop (unroll i))
- let leave_loop (p : flow) (_i : stmt) : unit =
- transfer_action p Leave_loop
+ let leave_loop (flow : flow) (_i : stmt) : flow =
+ Flow.transfer_keys flow Leave_loop
- let next_loop_iteration (p : flow) (_i : stmt) : unit =
- transfer_action p Incr_loop
+ let next_loop_iteration (flow : flow) (_i : stmt) : flow =
+ Flow.transfer_keys flow Incr_loop
let empty_rationing = new_rationing ~limit:0 ~merge:false
- let split_return (flow : flow) (return_exp : exp option) : unit =
+ let split_return (flow : flow) (return_exp : exp option) : flow =
let strategy = Split_return.kf_strategy kf in
- if strategy <> Split_strategy.FullSplit
- then
+ if strategy = Split_strategy.FullSplit
+ then flow
+ else
let apply action =
- let f = Flow.transfer_keys flow.flow_states action in
- flow.flow_states <- Flow.join_duplicate_keys f
+ Flow.join_duplicate_keys (Flow.transfer_keys flow action)
in
match Split_return.kf_strategy kf with
(* SplitAuto already transformed into SplitEqList. *)
@@ -187,9 +181,6 @@ struct
let is_eternal key _state = not (Key.exceed_rationing key) in
s.store_partition <- Partition.filter is_eternal s.store_partition
- let reset_flow (f : flow) : unit =
- f.flow_states <- Flow.empty
-
let reset_tank (t : tank) : unit =
t.tank_states <- Partition.empty
@@ -206,21 +197,20 @@ struct
(* Operators *)
let drain (t : tank) : flow =
- let flow_states = Flow.of_partition t.tank_states in
+ let flow = Flow.of_partition t.tank_states in
t.tank_states <- Partition.empty;
- { flow_states }
+ flow
- let fill ~(into : tank) (f : flow) : unit =
+ let fill ~(into : tank) (flow : flow) : unit =
let erase _key dest src =
if Extlib.has_some src
then src
else dest
in
- let new_states = Flow.to_partition f.flow_states in
+ let new_states = Flow.to_partition flow in
into.tank_states <- Partition.merge erase into.tank_states new_states
- let transfer (f : state -> state list) (p : flow) : unit =
- p.flow_states <- Flow.transfer_states f p.flow_states
+ let transfer = Flow.transfer_states
let join (sources : (branch*flow) list) (dest : store) : flow =
let is_loop_head =
@@ -231,11 +221,11 @@ struct
(* Get every source flow *)
let sources_states =
match sources with
- | [(_,p)] -> [p.flow_states]
+ | [(_,flow)] -> [flow]
| sources ->
(* Several branches -> partition according to the incoming branch *)
- let get (b,p) =
- Flow.transfer_keys p.flow_states (Branch (b,history_size))
+ let get (b,flow) =
+ Flow.transfer_keys flow (Branch (b,history_size))
in
List.map get sources
in
@@ -282,11 +272,10 @@ struct
Extlib.opt_filter (fun s -> Index.add s dest.store_index) state
in
let flow = Flow.join_duplicate_keys flow_states in
- let flow = Flow.filter_map update flow in
- { flow_states = flow }
+ Flow.filter_map update flow
- let widen (w : widening) (f : flow) : bool =
+ let widen (w : widening) (flow : flow) : flow =
let stmt = w.widening_stmt in
(* Auxiliary function to update the result *)
let update key widening_state =
@@ -341,8 +330,6 @@ struct
};
Some curr
in
- 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
+ let flow = Flow.join_duplicate_keys flow in
+ Flow.filter_map widen_one flow
end
diff --git a/src/plugins/value/engine/trace_partitioning.mli b/src/plugins/value/engine/trace_partitioning.mli
index dd9dfaadeec26b40da00c3d0e4e6728f5a78de84..584134d4d145952e501942657a1b92985b788e11 100644
--- a/src/plugins/value/engine/trace_partitioning.mli
+++ b/src/plugins/value/engine/trace_partitioning.mli
@@ -29,14 +29,15 @@ module Make
sig
type state = Abstract.Dom.t (** The states being partitioned *)
type store (** The storage of all states ever met at a control point *)
+ type tank (** The set of states that remains to propagate from a
+ control point. *)
type flow (** A set of states which are currently propagated *)
- type tank (** An organized temporary accumulation of flows *)
- type widening (** Widening informations *)
+ type widening (** Widening information *)
(* --- Constructors --- *)
val empty_store : stmt:Cil_types.stmt option -> store
- val empty_flow : unit -> flow
+ val empty_flow : flow
val empty_tank : unit -> tank
val empty_widening : stmt:Cil_types.stmt option -> widening
@@ -65,7 +66,6 @@ sig
(* These functions reset the part of the state of the analysis which has
been obtained after a widening. *)
val reset_store : store -> unit
- val reset_flow : flow -> unit
val reset_tank : tank -> unit
val reset_widening : widening -> unit
@@ -77,10 +77,10 @@ sig
(* --- Partition transfer functions --- *)
- val enter_loop : flow -> Cil_types.stmt -> unit
- val leave_loop : flow -> Cil_types.stmt -> unit
- val next_loop_iteration : flow -> Cil_types.stmt -> unit
- val split_return : flow -> Cil_types.exp option -> unit
+ val enter_loop : flow -> Cil_types.stmt -> flow
+ val leave_loop : flow -> Cil_types.stmt -> flow
+ val next_loop_iteration : flow -> Cil_types.stmt -> flow
+ val split_return : flow -> Cil_types.exp option -> flow
(* --- Operators --- *)
@@ -88,12 +88,11 @@ sig
created by [empty_tank] *)
val drain : tank -> flow
- (** Fill the states of the flow into the tank, modifying [into] inplace but
- letting the flow unchanged *)
+ (** Fill the states of the flow into the tank, modifying [into] inplace. *)
val fill : into:tank -> flow -> unit
(** Apply a transfer function to all the states of a propagation. *)
- val transfer : (state -> state list) -> flow -> unit
+ val transfer : (state -> state list) -> flow -> flow
(** Join all incoming propagations into the given store. This function returns
a set of states which still need to be propagated past the store.
@@ -110,10 +109,7 @@ sig
val join : (Partition.branch * flow) list -> store -> flow
(** Widen a flow. The widening object keeps track of the previous widenings
- and previous propagated states to ensure termination. The result is true
- when it is correct to end the propagation here, i.e. when the flow
- object is only containng states which are included into already propagated
- states. *)
- val widen : widening -> flow -> bool
+ and previous propagated states to ensure termination. *)
+ val widen : widening -> flow -> flow
end