[Eva] set a limit to the number of possible partitioning splits

src/plugins/value/engine/partition.ml

@@ -20,6 +20,19 @@
 (*                                                                        *)
 (**************************************************************************)
 
+(* --- Split monitors --- *)
+
+type split_monitor = {
+  split_limit : int;
+  mutable split_values : Datatype.Integer.Set.t;
+}
+
+let new_monitor ~split_limit = {
+  split_limit;
+  split_values = Datatype.Integer.Set.empty;
+}
+
+
 (* --- Keys --- *)
 
 module ExpMap = Cil_datatype.ExpStructEq.Map
@@ -33,8 +46,8 @@ type key = {
   ration_stamp : (int * int) option;
   branches : branch list;
   loops : (int * int) list;
-  static_split : Integer.t ExpMap.t;
-  dynamic_split : Integer.t ExpMap.t;
+  static_split : (Integer.t*split_monitor) ExpMap.t;
+  dynamic_split : (Integer.t*split_monitor) ExpMap.t;
 }
 
 module Key =
@@ -54,10 +67,13 @@ struct
     let (<?>) c (cmp,x,y) =
       if c = 0 then cmp x y else c
     in
+    let compare_split (i1,_m1) (i2,_m2) =
+      Integer.compare i1 i2
+    in
     Extlib.opt_compare IntPair.compare k1.ration_stamp k2.ration_stamp
     <?> (LoopList.compare, k1.loops, k2.loops)
-    <?> (ExpMap.compare Integer.compare, k1.static_split, k2.static_split)
-    <?> (ExpMap.compare Integer.compare, k1.dynamic_split, k2.dynamic_split)
+    <?> (ExpMap.compare compare_split, k1.static_split, k2.static_split)
+    <?> (ExpMap.compare compare_split, k1.dynamic_split, k2.dynamic_split)
     <?> (BranchList.compare, k1.branches, k2.branches)
 
   let pretty fmt key =
@@ -74,7 +90,7 @@ struct
       fmt
       key.loops;
     Pretty_utils.pp_list ~pre:"{@[" ~sep:" ;@ " ~suf:"@]}"
-      (fun fmt (e,i) -> Format.fprintf fmt "%a:%a"
+      (fun fmt (e,(i,_m)) -> Format.fprintf fmt "%a:%a"
           Cil_printer.pp_exp e
           (Integer.pretty ~hexa:false) i)
       fmt
@@ -123,8 +139,8 @@ type action =
   | Branch of branch * int
   | Ration of int
   | Ration_merge of (int*int) option
-  | Static_split of Cil_types.exp
-  | Dynamic_split of Cil_types.exp
+  | Static_split of (Cil_types.exp * split_monitor)
+  | Dynamic_split of (Cil_types.exp * split_monitor)
   | Static_merge of Cil_types.exp
   | Dynamic_merge of Cil_types.exp
   | Update_dynamic_splits
@@ -141,7 +157,8 @@ sig
   exception Operation_failed
 
   val join : t -> t -> t
-  val split : t -> Cil_types.exp -> (Integer.t * t) list
+  val split : monitor:split_monitor ->
+    t -> Cil_types.exp -> (Integer.t * t) list
   val eval_exp_to_int : t -> Cil_types.exp -> int
 end
 
@@ -182,25 +199,26 @@ struct
   let union (p1 : t) (p2 : t) : t =
     p1 @ p2
 
-  let split_state ~(static : bool) (exp : Cil_types.exp)
+  let split_state ~monitor ~(static : bool) (exp : Cil_types.exp)
       (key : key) (state : state) : (key * state) list =
     try
       let update_key (v,x) =
         let k =
+          let m = monitor in
           if static then
-            { key with static_split = ExpMap.add exp v key.static_split }
+            { key with static_split = ExpMap.add exp (v,m) key.static_split }
           else
-            { key with dynamic_split = ExpMap.add exp v key.dynamic_split }
+            { key with dynamic_split = ExpMap.add exp (v,m) key.dynamic_split }
         in
         (k,x)
       in
-      List.map update_key (Domain.split state exp)
+      List.map update_key (Domain.split ~monitor state exp)
     with Domain.Operation_failed ->
       [(key,state)]
 
-  let split ~(static : bool) (p : t) (exp : Cil_types.exp) =
+  let split ~monitor ~(static : bool) (p : t) (exp : Cil_types.exp) =
     let add_split acc (key,state) =
-      split_state ~static exp key state @ acc
+      split_state ~monitor ~static exp key state @ acc
     in
     List.fold_left add_split [] p
 
@@ -208,9 +226,11 @@ struct
     (* Update one state *)
     let update_state acc (key,state) =
       (* Split the states in the list l for the given exp *)
-      let update_exp exp _ l =
-        let static = false in
-        List.fold_left (fun l (k,x) -> split_state ~static exp k x @ l) [] l
+      let update_exp exp (_i,monitor) l =
+        let resplit acc (k,x) =
+          split_state ~monitor ~static:false exp k x @ acc
+        in
+        List.fold_left resplit [] l
       in
       (* Foreach exp in original state: split *)
       ExpMap.fold update_exp key.dynamic_split [(key,state)] @ acc
@@ -224,11 +244,11 @@ struct
     f p
 
   let transfer_keys p = function
-    | Static_split exp ->
-      split ~static:true p exp
+    | Static_split (exp,monitor) ->
+      split ~monitor ~static:true p exp
 
-    | Dynamic_split exp ->
-      split ~static:false p exp
+    | Dynamic_split (exp,monitor) ->
+      split ~monitor ~static:false p exp
 
     | Update_dynamic_splits ->
       update_dynamic_splits p

src/plugins/value/engine/partition.mli

@@ -20,6 +20,16 @@
 (*                                                                        *)
 (**************************************************************************)
 
+(* Split monitor : prevents splits from generating too many states *)
+
+type split_monitor = {
+  split_limit : int;
+  mutable split_values : Datatype.Integer.Set.t;
+}
+
+val new_monitor : split_limit:int -> split_monitor
+
+
 (*  A state partition is a collection of states, each of which is identified
     by a unique key. The key identifies the reason for which we want to keep
     the state separate from the others. The partitioning method will involve
@@ -63,10 +73,17 @@ type key = private {
   ration_stamp : (int * int) option; (* store stamp / transfer stamp *)
   branches : branch list;
   loops : (int * int) list; (* current iteration / max unrolling *)
-  static_split : Integer.t ExpMap.t;
-  dynamic_split : Integer.t ExpMap.t;
+  static_split : (Integer.t * split_monitor) ExpMap.t; (* exp->value*monitor *)
+  dynamic_split : (Integer.t * split_monitor) ExpMap.t; (* exp->value*monitor *)
 }
 
+module Key : sig
+  type t = key
+  val zero : t
+  val compare : t -> t -> int
+  val pretty : Format.formatter -> t -> unit
+end
+
 type 'a partition
 
 val empty : 'a partition
@@ -83,7 +100,6 @@ val map : ('a  -> 'a) -> 'a partition -> 'a partition
 val map_filter : (key -> 'a -> 'b option) -> 'a partition -> 'b partition
 
 
-
 (* Partitioning actions *)
 
 type 'a transfer_function = (key * 'a) list -> (key * 'a) list
@@ -99,8 +115,8 @@ type action =
   | 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 *)
-  | Static_split of Cil_types.exp
-  | Dynamic_split of Cil_types.exp
+  | Static_split of (Cil_types.exp * split_monitor)
+  | Dynamic_split of (Cil_types.exp * split_monitor)
   | Static_merge of Cil_types.exp
   | Dynamic_merge of Cil_types.exp
   | Update_dynamic_splits
@@ -117,7 +133,8 @@ sig
   exception Operation_failed
 
   val join : t -> t -> t
-  val split : t -> Cil_types.exp -> (Integer.t * t) list
+  val split : monitor:split_monitor ->
+    t -> Cil_types.exp -> (Integer.t * t) list
   val eval_exp_to_int : t -> Cil_types.exp -> int
 end
 

src/plugins/value/engine/partitioning_parameters.ml

@@ -104,11 +104,14 @@ struct
 
   let history_size = HistoryPartitioning.get ()
 
+  let split_limit = SplitLimit.get ()
+
   let universal_splits =
     let add name l =
       try
         let vi = Globals.Vars.find_from_astinfo name VGlobal in
-        Cil.evar vi :: l
+        let m = Partition.new_monitor split_limit in
+        Partition.Dynamic_split (Cil.evar vi, m) :: l
       with Not_found ->
         warn ~current:false "cannot find the global variable %s for value \
                              partitioning" name;
@@ -119,8 +122,9 @@ struct
   let flow_actions stmt =
     let map_annot acc t =
       try
+        let m = Partition.new_monitor split_limit in
         match t with
-        | FlowSplit t -> Partition.Static_split (term_to_exp t) :: acc
+        | FlowSplit t -> Partition.Static_split (term_to_exp t,m) :: acc
         | FlowMerge t -> Partition.Static_merge (term_to_exp t) :: acc
       with
         Db.Properties.Interp.No_conversion ->

src/plugins/value/engine/state_partitioning.mli

@@ -38,7 +38,8 @@ sig
   val merge : Cil_types.stmt -> bool
   val unroll : loop -> Partition.unroll_limit
   val history_size : int
-  val universal_splits : Cil_types.exp list
+  val split_limit : int
+  val universal_splits : Partition.action list
   val flow_actions : Cil_types.stmt -> Partition.action list
 end
 

src/plugins/value/engine/trace_partitioning.ml

@@ -112,12 +112,9 @@ struct
     }
 
   let initial_tank (states : state list) : tank =
-    let propagation = Flow.initial states in
+    let flow = Flow.initial states in
     (* Split the initial partition according to the global split seetings *)
-    let split propagation lval =
-      Flow.transfer_keys propagation (Dynamic_split lval)
-    in
-    let states = List.fold_left split propagation universal_splits in
+    let states = List.fold_left Flow.transfer_keys flow universal_splits in
     { tank_states = Flow.to_partition states }
 
 

src/plugins/value/engine/transfer_stmt.ml

@@ -41,7 +41,8 @@ module type S = sig
     unit or_bottom
   val enter_scope: kernel_function -> varinfo list -> state -> state
   exception Operation_failed
-  val split_by_value: state -> exp -> (Integer.t * state) list
+  val split_by_value: monitor:Partition.split_monitor ->
+    state -> exp -> (Integer.t * state) list
   val eval_exp_to_int: state -> exp -> int
   type call_result = {
     states: state list or_bottom;
@@ -883,49 +884,88 @@ module Make (Abstract: Abstractions.Eva) = struct
   exception Operation_failed
 
   let fail ~exp message =
-    Value_parameters.warning ~source:(fst exp.eloc) ~once:true message;
-    raise Operation_failed
+    let warn_and_raise message =
+      Value_parameters.warning ~source:(fst exp.eloc) ~once:true "%s" message;
+      raise Operation_failed
+    in
+    Pretty_utils.ksfprintf warn_and_raise message
 
-  let evaluate_exp_to_ival state exp =
+  let evaluate_exp_to_ival ?valuation state exp =
     (* Evaluate the expression *)
-    let valuation, value = match Eval.evaluate ~reduction:false state exp with
+    let valuation, value =
+      match Eval.evaluate ?valuation ~reduction:false state exp with
       | `Value (valuation, value), alarms when Alarmset.is_empty alarms ->
         valuation, value
       | _ ->
-        fail ~exp "this partitioning parameter cannot be evaluated safely on all states"
+        fail ~exp "this partitioning parameter cannot be evaluated safely on \
+                   all states"
     in
     (* Get the cvalue *)
     let cvalue = match Value.get Main_values.cvalue_key with
       | Some get_cvalue -> get_cvalue value
-      | None -> fail ~exp "partitioning is disabled when the CValue domain is not active"
+      | None -> fail ~exp "partitioning is disabled when the CValue domain is \
+                           not active"
     in
     (* Extract the ival *)
     let ival =
       try
         Cvalue.V.project_ival cvalue
       with Cvalue.V.Not_based_on_null ->
-        fail ~exp "this partitioning parameter must evaluate to an integer"
+        fail ~exp "this partitioning parameter must evaluatassumee to an integer"
     in
     valuation, ival
 
-  let split_by_value state exp =
+  exception Split_limit of Integer.t option
+
+  let split_by_value ~monitor state exp =
+    let module SplitValues = Datatype.Integer.Set in
     let valuation, ival = evaluate_exp_to_ival state exp in
     (* Build a state with the lvalue set to a singleton *)
     let build i acc =
       let value = Value.inject_int (Cil.typeOf exp) i in
       match Eval.assume ~valuation state exp value with
       | `Value valuation ->
-        (i, TF.update valuation state) :: acc
+        (* Check the reduction *)
+        let state = TF.update valuation state in
+        let _,new_ival = evaluate_exp_to_ival ~valuation state exp in
+        if not (Ival.is_singleton_int new_ival) then
+          fail ~exp "failing to learn perfectly from split" ;
+        monitor.Partition.split_values <-
+          SplitValues.add i monitor.Partition.split_values;
+        (i, state) :: acc
       | _ -> (* This value cannot be set in the state ; the evaluation of
                 expr was unprecise *)
         acc
     in
-    (* For each integer of the ival, build a new state *)
-    begin try
-        Ival.fold_int build ival []
-      with Abstract_interp.Error_Top ->
-        fail ~exp "too many values to partition by value on"
-    end
+    try
+      (* Check the size of the ival *)
+      begin match Ival.cardinal ival with
+        | None -> raise (Split_limit None)
+        | Some c as count ->
+          if Integer.(gt c (of_int monitor.Partition.split_limit)) then
+            raise (Split_limit count)
+      end;
+      (* For each integer of the ival, build a new state *)
+      try
+        let result = Ival.fold_int build ival [] in
+        let c = SplitValues.cardinal monitor.Partition.split_values in
+        if c > monitor.Partition.split_limit then
+          raise (Split_limit (Some (Integer.of_int c)));
+        result
+      with Abstract_interp.Error_Top -> (* The ival is float *)
+        raise (Split_limit None)
+    with
+    | Split_limit count ->
+      let pp_count fmt =
+        match count with
+        | None -> ()
+        | Some c -> Format.fprintf fmt " (%a)" (Integer.pretty ~hexa:false) c
+      in
+      fail ~exp "split on more than %d values%t prevented ; try to improve \
+                 the analysis precision or look at the option -eva-split-limit \
+                 to increase this limit."
+        monitor.Partition.split_limit pp_count
+
 
   let eval_exp_to_int state exp =
     let _valuation, ival = evaluate_exp_to_ival state exp in

src/plugins/value/engine/transfer_stmt.mli

@@ -53,7 +53,8 @@ module type S = sig
 
   exception Operation_failed
 
-  val split_by_value: state -> exp -> (Integer.t * state) list
+  val split_by_value: monitor:Partition.split_monitor ->
+    state -> exp -> (Integer.t * state) list
   val eval_exp_to_int: state -> exp -> int
 
   type call_result = {

src/plugins/value/value_parameters.ml

@@ -753,6 +753,19 @@ module ValuePartitioning =
     end)
 let () = add_precision_dep ValuePartitioning.parameter
 
+let () = Parameter_customize.set_group precision_tuning
+module SplitLimit =
+  Int
+    (struct
+      let option_name = "-eva-split-limit"
+      let arg_name = "N"
+      let default = 100
+      let help = "prevents the split annotations or -eva-partition-value to \
+                  enumerate more than N cases"
+    end)
+let () = add_precision_dep SplitLimit.parameter
+let () = SplitLimit.set_range 0 max_int
+
 let () = Parameter_customize.set_group precision_tuning
 let () = Parameter_customize.argument_may_be_fundecl ()
 module SplitReturnFunction =

src/plugins/value/value_parameters.mli

@@ -88,6 +88,7 @@ module MinLoopUnroll : Parameter_sig.Int
 module DefaultLoopUnroll : Parameter_sig.Int
 module HistoryPartitioning : Parameter_sig.Int
 module ValuePartitioning : Parameter_sig.String_set
+module SplitLimit : Parameter_sig.Int
 
 module ArrayPrecisionLevel: Parameter_sig.Int