diff --git a/src/plugins/value/Eva.mli b/src/plugins/value/Eva.mli
index 97761d74c2583992f4fcd2a463e8380e860766c4..f44c2e4c112623521a6b4404f2c007e29b3e91b0 100644
--- a/src/plugins/value/Eva.mli
+++ b/src/plugins/value/Eva.mli
@@ -88,12 +88,15 @@ module Eva_annotations: sig
| UnrollFull (** Unroll amount defined by -eva-default-loop-unroll. *)
type split_kind = Static | Dynamic
+ type split_term =
+ | Expression of Cil_types.exp
+ | Predicate of Cil_types.predicate
(** Split/merge annotations for value partitioning. *)
type flow_annotation =
- | FlowSplit of Cil_types.term * split_kind
+ | FlowSplit of split_term * split_kind
(** Split states according to a term. *)
- | FlowMerge of Cil_types.term
+ | FlowMerge of split_term
(** Merge states separated by a previous split. *)
val add_slevel_annot : emitter:Emitter.t -> loc:Cil_types.location ->
diff --git a/src/plugins/value/partitioning/partition.ml b/src/plugins/value/partitioning/partition.ml
index 2325162fd0ccd2e1557bc5b3fbf8e5c43fd4d68a..47019da338d0c85d1e28c6cde7ae52915863e020 100644
--- a/src/plugins/value/partitioning/partition.ml
+++ b/src/plugins/value/partitioning/partition.ml
@@ -53,7 +53,25 @@ let new_rationing ~limit ~merge = { current = ref 0; limit; merge }
(* --- Keys --- *)
-module ExpMap = Cil_datatype.ExpStructEq.Map
+type split_term = Eva_annotations.split_term =
+ | Expression of Cil_types.exp
+ | Predicate of Cil_types.predicate
+
+module SplitTerm = struct
+ type t = split_term
+ let compare x y =
+ match x, y with
+ | Expression e1, Expression e2 -> Cil_datatype.ExpStructEq.compare e1 e2
+ | Predicate p1, Predicate p2 -> Logic_utils.compare_predicate p1 p2
+ | Expression _, Predicate _ -> 1
+ | Predicate _, Expression _ -> -1
+
+ let pretty fmt = function
+ | Expression e -> Printer.pp_exp fmt e
+ | Predicate p -> Printer.pp_predicate fmt p
+end
+
+module SplitMap = Map.Make (SplitTerm)
module IntPair = Datatype.Pair (Datatype.Int) (Datatype.Int)
module LoopList = Datatype.List (IntPair)
module BranchList = Datatype.List (Datatype.Int)
@@ -85,8 +103,8 @@ type key = {
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 *)
- dynamic_split : (Integer.t*split_monitor) ExpMap.t; (* exp->value*monitor *)
+ static_split : (Integer.t*split_monitor) SplitMap.t; (* exp->value*monitor *)
+ dynamic_split : (Integer.t*split_monitor) SplitMap.t; (* exp->value*monitor *)
}
module Key =
@@ -98,8 +116,8 @@ struct
ration_stamp = None;
branches = [];
loops = [];
- static_split = ExpMap.empty;
- dynamic_split = ExpMap.empty;
+ static_split = SplitMap.empty;
+ dynamic_split = SplitMap.empty;
}
let compare k1 k2 =
@@ -111,8 +129,8 @@ struct
in
Option.compare IntPair.compare k1.ration_stamp k2.ration_stamp
<?> (LoopList.compare, k1.loops, k2.loops)
- <?> (ExpMap.compare compare_split, k1.static_split, k2.static_split)
- <?> (ExpMap.compare compare_split, k1.dynamic_split, k2.dynamic_split)
+ <?> (SplitMap.compare compare_split, k1.static_split, k2.static_split)
+ <?> (SplitMap.compare compare_split, k1.dynamic_split, k2.dynamic_split)
<?> (BranchList.compare, k1.branches, k2.branches)
let pretty fmt key =
@@ -129,11 +147,11 @@ struct
fmt
key.loops;
Pretty_utils.pp_list ~pre:"{@[" ~sep:" ;@ " ~suf:"@]}"
- (fun fmt (e,(i,_m)) -> Format.fprintf fmt "%a:%a"
- Cil_printer.pp_exp e
+ (fun fmt (t,(i,_m)) -> Format.fprintf fmt "%a:%a"
+ SplitTerm.pretty t
(Integer.pretty ~hexa:false) i)
fmt
- (ExpMap.bindings key.static_split @ ExpMap.bindings key.dynamic_split)
+ (SplitMap.bindings key.static_split @ SplitMap.bindings key.dynamic_split)
let exceed_rationing key = key.ration_stamp = None
end
@@ -175,8 +193,8 @@ type action =
| Branch of branch * int
| Ration of rationing
| Restrict of Cil_types.exp * Integer.t list
- | Split of Cil_types.exp * split_kind * split_monitor
- | Merge of Cil_types.exp
+ | Split of split_term * split_kind * split_monitor
+ | Merge of split_term
| Update_dynamic_splits
exception InvalidAction
@@ -328,6 +346,26 @@ struct
| Failure _ ->
fail ~exp "this partitioning parameter is too big"
+ let split_by_predicate state predicate =
+ let env =
+ let states = function _ -> Abstract.Dom.top in
+ Abstract_domain.{ states; result = None }
+ in
+ let source = fst (predicate.Cil_types.pred_loc) in
+ let aux positive =
+ Abstract.Dom.reduce_by_predicate env state predicate positive
+ >>-: fun state' ->
+ let x = Abstract.Dom.evaluate_predicate env state' predicate in
+ if x == Unknown
+ then
+ Value_parameters.warning ~source ~once:true
+ "failing to learn perfectly from split predicate";
+ if Abstract.Dom.equal state' state then raise Operation_failed;
+ let value = if positive then Integer.one else Integer.zero in
+ value, state'
+ in
+ Bottom.all [ aux true; aux false ]
+
(* --- Applying partitioning actions onto flows --------------------------- *)
let stamp_by_value = match Abstract.Val.get Main_values.CVal.key with
@@ -352,10 +390,10 @@ struct
None
end
- let split_state ~monitor (kind : split_kind) (exp : Cil_types.exp)
+ let split_state ~monitor (kind : split_kind) (term : split_term)
(key : key) (state : state) : (key * state) list =
try
- let add value map = ExpMap.add exp (value, monitor) map in
+ let add value map = SplitMap.add term (value, monitor) map in
let update_key (v,x) =
let k =
match kind with
@@ -364,13 +402,18 @@ struct
in
(k,x)
in
- List.map update_key (split_by_value ~monitor state exp)
+ let states =
+ match term with
+ | Expression exp -> split_by_value ~monitor state exp
+ | Predicate pred -> split_by_predicate state pred
+ in
+ List.map update_key states
with Operation_failed ->
[(key,state)]
- let split ~monitor (kind : split_kind) (exp : Cil_types.exp) (p : t) =
+ let split ~monitor (kind : split_kind) (term : split_term) (p : t) =
let add_split acc (key,state) =
- split_state ~monitor kind exp key state @ acc
+ split_state ~monitor kind term key state @ acc
in
List.fold_left add_split [] p
@@ -385,7 +428,7 @@ struct
List.fold_left resplit [] l
in
(* Foreach exp in original state: split *)
- ExpMap.fold update_exp key.dynamic_split [(key,state)] @ acc
+ SplitMap.fold update_exp key.dynamic_split [(key,state)] @ acc
in
List.fold_left update_state [] p
@@ -472,8 +515,8 @@ struct
{ k with ration_stamp = stamp_by_value expr expected_values s}
| Merge exp -> fun k _x ->
- { k with static_split = ExpMap.remove exp k.static_split;
- dynamic_split = ExpMap.remove exp k.dynamic_split }
+ { k with static_split = SplitMap.remove exp k.static_split;
+ dynamic_split = SplitMap.remove exp k.dynamic_split }
in
map_keys transfer p
diff --git a/src/plugins/value/partitioning/partition.mli b/src/plugins/value/partitioning/partition.mli
index 1b773efe9871741fa80dccd87cd5d8043a3f3472..fe3dc9f303f8332f8009fdf419dc10f6676509c1 100644
--- a/src/plugins/value/partitioning/partition.mli
+++ b/src/plugins/value/partitioning/partition.mli
@@ -94,6 +94,11 @@ type unroll_limit =
states are then split or merged accordingly. *)
type split_kind = Eva_annotations.split_kind = Static | Dynamic
+(** Splits can be performed according to a C expression or an ACSL predicate. *)
+type split_term = Eva_annotations.split_term =
+ | Expression of Cil_types.exp
+ | Predicate of Cil_types.predicate
+
(** Split monitor: prevents splits from generating too many states. *)
type split_monitor
@@ -137,7 +142,7 @@ type action =
– all other states are joined together.
Previous rationing is erased and replaced by this new stamping.
Implementation of the option -eva-split-return. *)
- | Split of Cil_types.exp * split_kind * split_monitor
+ | Split of split_term * split_kind * split_monitor
(** [Split (exp, kind, monitor)] tries to separate states such as the [exp]
evaluates to a singleton value in each state in the flow. If necessary and
possible, splits states into multiple states. States in which the [exp]
@@ -145,7 +150,7 @@ type action =
if [exp] evaluates to more than [limit] values, [limit] being the split
limit of the [monitor]. A same monitor can be used for successive splits
on different flows. *)
- | Merge of Cil_types.exp
+ | Merge of split_term
(** Forgets the split of an expression: states that were kept separate only
by the split of this expression will be joined together. *)
| Update_dynamic_splits
diff --git a/src/plugins/value/partitioning/partitioning_parameters.ml b/src/plugins/value/partitioning/partitioning_parameters.ml
index b3609a90cc6a44a40b5f9c9ba369a3426c9b0cef..519e2fc02290aabc32213050079494afe4a23073 100644
--- a/src/plugins/value/partitioning/partitioning_parameters.ml
+++ b/src/plugins/value/partitioning/partitioning_parameters.ml
@@ -116,7 +116,8 @@ struct
try
let vi = Globals.Vars.find_from_astinfo name VGlobal in
let monitor = Partition.new_monitor ~split_limit in
- Partition.Split (Cil.evar vi, Partition.Dynamic, monitor) :: l
+ let expr = Partition.Expression (Cil.evar vi) in
+ Partition.Split (expr, Partition.Dynamic, monitor) :: l
with Not_found ->
warn ~current:false "cannot find the global variable %s for value \
partitioning; ignoring" name;
@@ -130,8 +131,8 @@ struct
let monitor = Partition.new_monitor ~split_limit in
let action =
match t with
- | FlowSplit (t, kind) -> Partition.Split (term_to_exp t, kind, monitor)
- | FlowMerge t -> Partition.Merge (term_to_exp t)
+ | FlowSplit (t, kind) -> Partition.Split (t, kind, monitor)
+ | FlowMerge t -> Partition.Merge t
in
action :: acc
with
diff --git a/src/plugins/value/utils/eva_annotations.ml b/src/plugins/value/utils/eva_annotations.ml
index adaf06945a43d70cf60b9961a85b01753885ebf3..075cc5773385e4b7f315d9e719f79a1fbb4f081e 100644
--- a/src/plugins/value/utils/eva_annotations.ml
+++ b/src/plugins/value/utils/eva_annotations.ml
@@ -34,10 +34,13 @@ type unroll_annotation =
| UnrollFull
type split_kind = Static | Dynamic
+type split_term =
+ | Expression of Cil_types.exp
+ | Predicate of Cil_types.predicate
type flow_annotation =
- | FlowSplit of term * split_kind
- | FlowMerge of term
+ | FlowSplit of split_term * split_kind
+ | FlowMerge of split_term
type taint_annotation = Cil_types.term list
@@ -155,26 +158,6 @@ module Slevel = Register (struct
| SlevelFull -> Format.pp_print_string fmt "full"
end)
-module SimpleTermAnnotation =
-struct
- type t = term
-
- let parse ~typing_context = function
- | [t] ->
- let open Logic_typing in
- typing_context.type_term typing_context typing_context.pre_state t
- | _ -> raise Parse_error
-
- let export t =
- Ext_terms [t]
-
- let import = function
- | Ext_terms [t] -> t
- | _ -> assert false
-
- let print = Printer.pp_term
-end
-
module ListTermAnnotation =
struct
type t = term list
@@ -222,20 +205,64 @@ module Unroll = Register (struct
| UnrollAmount t -> Printer.pp_term fmt t
end)
+module SplitTermAnnotation =
+struct
+ type t = split_term
+
+ let term_to_exp = !Db.Properties.Interp.term_to_exp ~result:None
+
+ let parse ~typing_context = function
+ | [t] ->
+ begin
+ let open Logic_typing in
+ let exception No_term in
+ try
+ let error _loc _fmt = raise No_term in
+ let typing_context = { typing_context with error } in
+ let term =
+ typing_context.type_term typing_context typing_context.pre_state t
+ in
+ Expression (term_to_exp term)
+ with
+ | No_term ->
+ Predicate
+ (typing_context.type_predicate
+ typing_context typing_context.pre_state t)
+ | Db.Properties.Interp.No_conversion ->
+ Kernel.warning ~wkey:Kernel.wkey_annot_error ~once:true ~current:true
+ "split/merge expressions must be valid expressions; ignoring";
+ raise Parse_error
+ end
+ | _ -> raise Parse_error
+
+ let export = function
+ | Expression expr -> Ext_terms [ Logic_utils.expr_to_term expr ]
+ | Predicate pred -> Ext_preds [pred]
+
+ let import = function
+ | Ext_terms [term] -> Expression (term_to_exp term)
+ | Ext_preds [pred] -> Predicate pred
+ | _ -> assert false
+
+ let print fmt = function
+ | Expression expr -> Printer.pp_exp fmt expr
+ | Predicate pred -> Printer.pp_predicate fmt pred
+end
+
module Split = Register (struct
- include SimpleTermAnnotation
+ include SplitTermAnnotation
let name = "split"
let is_loop_annot = false
end)
module Merge = Register (struct
- include SimpleTermAnnotation
+ include SplitTermAnnotation
let name = "merge"
let is_loop_annot = false
end)
module DynamicSplit = Register (struct
- include SimpleTermAnnotation
+ include SplitTermAnnotation
let name = "dynamic_split"
let is_loop_annot = false
end)
diff --git a/src/plugins/value/utils/eva_annotations.mli b/src/plugins/value/utils/eva_annotations.mli
index 629f8ffe5adb5b1116e5f1214be649bbfb04ca6d..dd7d580bdb463911ea778c79cce32184008d0859 100644
--- a/src/plugins/value/utils/eva_annotations.mli
+++ b/src/plugins/value/utils/eva_annotations.mli
@@ -40,9 +40,13 @@ type unroll_annotation =
type split_kind = Static | Dynamic
+type split_term =
+ | Expression of Cil_types.exp
+ | Predicate of Cil_types.predicate
+
type flow_annotation =
- | FlowSplit of Cil_types.term * split_kind
- | FlowMerge of Cil_types.term
+ | FlowSplit of split_term * split_kind
+ | FlowMerge of split_term
type taint_annotation = Cil_types.term list