[Eva] New "subdivide" annotation to override -eva-subdivide-non-linear option.

This annotation sets the maximum number of subdivisions in the evaluation
of expressions at a given statement.

Makefile

@@ -860,9 +860,10 @@ endif
 # General rules for ordering files within PLUGIN_CMO:
 # - try to keep the legacy Value before Eva
 PLUGIN_CMO:= partitioning/split_strategy value_parameters \
-	utils/value_perf utils/value_util utils/red_statuses \
+	utils/value_perf utils/partitioning_annots \
+        utils/value_util utils/red_statuses \
 	utils/mark_noresults \
-	utils/widen_hints_ext utils/widen utils/partitioning_annots \
+	utils/widen_hints_ext utils/widen \
 	partitioning/split_return \
 	partitioning/per_stmt_slevel \
 	utils/library_functions \

src/plugins/value/utils/partitioning_annots.ml

@@ -224,3 +224,30 @@ let add_unroll_annot = Unroll.add
 let add_flow_annot ~emitter ~loc stmt = function
   | FlowSplit annot -> Split.add ~emitter ~loc stmt annot
   | FlowMerge annot -> Merge.add ~emitter ~loc stmt annot
+
+
+module Subdivision = Register (struct
+    type t = int
+    let name = "subdivide"
+    let is_loop_annot = false
+
+    let parse ~typing_context:_ = function
+      | [{lexpr_node = PLconstant (IntConstant i)}] ->
+        let i =
+          try int_of_string i
+          with Failure _ -> raise Parse_error
+        in
+        if i < 0 then raise Parse_error;
+        i
+      | _ -> raise Parse_error
+
+    let export i = Ext_terms [Logic_const.tinteger i]
+    let import = function
+      | Ext_terms [{term_node = TConst (Integer (i, _))}] -> Integer.to_int i
+      | _ -> assert false
+
+    let print fmt i = Format.pp_print_int fmt i
+  end)
+
+let get_subdivision_annot = Subdivision.get
+let add_subdivision_annot = Subdivision.add

src/plugins/value/utils/partitioning_annots.mli

@@ -34,6 +34,7 @@ type flow_annotation =
 val get_slevel_annot : Cil_types.stmt -> slevel_annotation option
 val get_unroll_annot : Cil_types.stmt -> unroll_annotation list
 val get_flow_annot : Cil_types.stmt -> flow_annotation list
+val get_subdivision_annot : Cil_types.stmt -> int list
 
 val add_slevel_annot : emitter:Emitter.t -> loc:Cil_types.location ->
   Cil_types.stmt -> slevel_annotation -> unit
@@ -41,3 +42,5 @@ val add_unroll_annot : emitter:Emitter.t -> loc:Cil_types.location ->
   Cil_types.stmt -> unroll_annotation -> unit
 val add_flow_annot : emitter:Emitter.t -> loc:Cil_types.location ->
   Cil_types.stmt -> flow_annotation -> unit
+val add_subdivision_annot : emitter:Emitter.t -> loc:Cil_types.location ->
+  Cil_types.stmt -> int -> unit

src/plugins/value/utils/value_util.ml

@@ -71,12 +71,22 @@ let get_slevel kf =
   try Value_parameters.SlevelFunction.find kf
   with Not_found -> Value_parameters.SemanticUnrollingLevel.get ()
 
-let get_subdivision stmt =
+let get_subdivision_option stmt =
   try
     let kf = Kernel_function.find_englobing_kf stmt in
     Value_parameters.LinearLevelFunction.find kf
   with Not_found -> Value_parameters.LinearLevel.get ()
 
+let get_subdivision stmt =
+  match Partitioning_annots.get_subdivision_annot stmt with
+  | [] -> get_subdivision_option stmt
+  | [x] -> x
+  | x :: _ ->
+    Value_parameters.warning ~current:true ~once:true
+      "Several subdivision annotations at the same statement; selecting %i\
+       and ignoring the others." x;
+    x
+
 let pretty_actuals fmt actuals =
   let pp fmt (e,x,_) = Cvalue.V.pretty_typ (Some (Cil.typeOf e)) fmt x in
   Pretty_utils.pp_flowlist pp fmt actuals