[Eva] Trace partitioning: makes the flow type non mutable.

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 *)

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

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