[Eva] New rationing implementation embedded in partition.ml.

src/plugins/value/engine/partition.ml

@@ -34,6 +34,22 @@ let new_monitor ~split_limit = {
   split_values = Datatype.Integer.Set.empty;
 }
 
+(* --- Stamp rationing --- *)
+
+(* Stamps used to label states according to slevel.
+   The second integer is used to keep separate the different states resulting
+   from a transfer function producing a state list before a new stamping.  *)
+type stamp = (int * int) option (* store stamp / transfer stamp *)
+
+(* Stamp rationing according to the slevel. *)
+type rationing =
+  { current: int ref; (* last used stamp. *)
+    limit: int;       (* limit of available stamps; after, stamps are [None]. *)
+    merge: bool       (* on merge slevel annotations or -eva-merge-after-loop,
+                         merge the incoming states with one unique stamp. *)
+  }
+
+let new_rationing ~limit ~merge = { current = ref 0; limit; merge }
 
 (* --- Keys --- *)
 
@@ -45,7 +61,7 @@ module BranchList = Datatype.List (Datatype.Int)
 type branch = int
 
 type key = {
-  ration_stamp : (int * int) option; (* store stamp / transfer stamp *)
+  ration_stamp : stamp;
   branches : branch list;
   loops : (int * int) list; (* current iteration / max unrolling *)
   static_split : (Integer.t*split_monitor) ExpMap.t; (* exp->value*monitor *)
@@ -141,8 +157,7 @@ type action =
   | Leave_loop
   | Incr_loop
   | Branch of branch * int
-  | Ration of int
-  | Ration_merge of (int*int) option
+  | Ration of rationing
   | Split of Cil_types.exp * split_kind * int
   | Merge of Cil_types.exp * split_kind
   | Update_dynamic_splits
@@ -389,15 +404,22 @@ struct
           else
             k
 
-        | Ration (min) ->
-          let r = ref min in
-          fun k _x ->
-            let ration_stamp = Some (!r, 0) in
-            incr r;
-            { k with ration_stamp }
-
-        | Ration_merge ration_stamp  -> fun k _x ->
-          { k with ration_stamp }
+        | Ration { current; limit; merge } ->
+          let length = List.length p in
+          (* The incoming states exceed the rationing limit: no more stamps. *)
+          if !current + length > limit then begin
+            current := limit;
+            fun k _ -> { k with ration_stamp = None }
+          end
+          (* If merge, a unique ration stamp for all incoming states. *)
+          else if merge then begin
+            current := !current + length;
+            fun k _ -> { k with ration_stamp = Some (!current, 0) }
+          end
+          (* Default case: a different stamp for each incoming state. *)
+          else
+            let stamp () = incr current; Some (!current, 0) in
+            fun k _ -> { k with ration_stamp = stamp () }
 
         | Merge (exp, Static) -> fun k _x ->
           { k with static_split = ExpMap.remove exp k.static_split }

src/plugins/value/engine/partition.mli

@@ -87,6 +87,9 @@ val map_filter : (key -> 'a -> 'b option) -> 'a partition -> 'b partition
 
 (* Partitioning actions *)
 
+type rationing
+val new_rationing: limit:int -> merge:bool -> rationing
+
 type unroll_limit =
   | ExpLimit of Cil_types.exp
   | IntLimit of int
@@ -98,8 +101,7 @@ type action =
   | Leave_loop
   | Incr_loop
   | Branch of branch * int (* branch taken, max branches in history *)
-  | Ration of int (* starting ration stamp *)
-  | Ration_merge of (int * int) option (* new ration stamp for the merge state *)
+  | Ration of rationing
   | Split of Cil_types.exp * split_kind * int
   | Merge of Cil_types.exp * split_kind
   | Update_dynamic_splits

src/plugins/value/engine/trace_partitioning.ml

@@ -48,8 +48,7 @@ struct
   type state = Domain.t
 
   type store = {
-    size_limit : int;
-    merge : bool;
+    rationing: Partition.rationing;
     flow_actions : action list;
     store_stmt : stmt option;
     store_index : Index.t;
@@ -79,12 +78,13 @@ struct
   (* Constructors *)
 
   let empty_store ~(stmt : stmt option) : store =
-    let size_limit, merge, flow_actions = match stmt with
+    let limit, merge, flow_actions = match stmt with
       | None -> max_int, false, []
       | Some stmt -> slevel stmt, merge stmt, flow_actions stmt
     in
+    let rationing = Partition.new_rationing ~limit ~merge in
     {
-      size_limit; merge; flow_actions;
+      rationing; flow_actions;
       store_stmt = stmt;
       store_index = Index.empty ();
       store_partition = Partition.empty;
@@ -247,20 +247,8 @@ struct
       List.fold_left Flow.union Flow.empty sources_states
     in
     (* Handle ration stamps *)
-    let previous_store_size = dest.store_size in
     dest.store_size <- dest.store_size + Flow.size flow_states;
-    let slevel_exceeded = dest.store_size > dest.size_limit in
-    let rationing_action =
-      if slevel_exceeded then
-        (* No more slevel, no more ration tickets *)
-        Ration_merge None
-      else if dest.merge then
-        (* Merge / Merge after loop : a unique ration stamp for all *)
-        Ration_merge (Some (previous_store_size, 0))
-      else
-        (* Attribute a ration stamp to each individual state *)
-        Ration previous_store_size
-    in
+    let rationing_action = Ration dest.rationing in
     (* Handle Split / Merge operations *)
     let flow_actions = Update_dynamic_splits :: dest.flow_actions in
     (* Execute actions *)