From 84af386f3d08ff9002a6a14239c8c3ac21af68f5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 15 Jul 2019 17:18:26 +0200
Subject: [PATCH] [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 | 5 ++--
.../value/utils/partitioning_annots.ml | 27 +++++++++++++++++++
.../value/utils/partitioning_annots.mli | 3 +++
src/plugins/value/utils/value_util.ml | 12 ++++++++-
4 files changed, 44 insertions(+), 3 deletions(-)
diff --git a/Makefile b/Makefile
index dd8b0234365..77433b677c0 100644
--- a/Makefile
+++ b/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 \
diff --git a/src/plugins/value/utils/partitioning_annots.ml b/src/plugins/value/utils/partitioning_annots.ml
index 804c3c8e15f..767cf487636 100644
--- a/src/plugins/value/utils/partitioning_annots.ml
+++ b/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
diff --git a/src/plugins/value/utils/partitioning_annots.mli b/src/plugins/value/utils/partitioning_annots.mli
index a95de0105a7..3d86f2f4007 100644
--- a/src/plugins/value/utils/partitioning_annots.mli
+++ b/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
diff --git a/src/plugins/value/utils/value_util.ml b/src/plugins/value/utils/value_util.ml
index 24df6f735e5..6db4c29ae67 100644
--- a/src/plugins/value/utils/value_util.ml
+++ b/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
--
GitLab