From aed92e803dc74657e046aea8de50506514658096 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Wed, 6 Jun 2018 16:32:17 +0200
Subject: [PATCH] [Eva] Extends value partitioning to any expression, not just
lvalues
---
src/plugins/value/engine/partition.ml | 63 +++++++++---------
src/plugins/value/engine/partition.mli | 16 ++---
.../value/engine/partitioned_dataflow.ml | 2 +-
.../value/engine/partitioning_parameters.ml | 19 +++---
.../value/engine/state_partitioning.mli | 8 ++-
.../value/engine/trace_partitioning.ml | 64 ++-----------------
src/plugins/value/engine/transfer_stmt.ml | 51 +++++++++++++++
src/plugins/value/engine/transfer_stmt.mli | 5 ++
8 files changed, 118 insertions(+), 110 deletions(-)
diff --git a/src/plugins/value/engine/partition.ml b/src/plugins/value/engine/partition.ml
index 44642d2a166..64e2e6c5d80 100644
--- a/src/plugins/value/engine/partition.ml
+++ b/src/plugins/value/engine/partition.ml
@@ -24,7 +24,7 @@
let opt_flatten (type a) (o : a option option) : a option =
Extlib.opt_conv None o
-module LvalMap = Cil_datatype.LvalStructEq.Map
+module ExpMap = Cil_datatype.ExpStructEq.Map
module IList = Datatype.List (Datatype.Int)
type branch = int
@@ -34,8 +34,8 @@ type key = {
transfer_stamp : int option;
branches : branch list;
loops : int list;
- static_split : Integer.t LvalMap.t;
- dynamic_split : Integer.t LvalMap.t;
+ static_split : Integer.t ExpMap.t;
+ dynamic_split : Integer.t ExpMap.t;
}
module Key =
@@ -49,8 +49,8 @@ struct
Extlib.opt_compare (-) k1.ration_stamp k2.ration_stamp
<?> (Extlib.opt_compare (-), k1.transfer_stamp, k2.transfer_stamp)
<?> (IList.compare, k1.loops, k2.loops)
- <?> (LvalMap.compare Integer.compare, k1.static_split, k2.static_split)
- <?> (LvalMap.compare Integer.compare, k1.dynamic_split, k2.dynamic_split)
+ <?> (ExpMap.compare Integer.compare, k1.static_split, k2.static_split)
+ <?> (ExpMap.compare Integer.compare, k1.dynamic_split, k2.dynamic_split)
<?> (IList.compare, k1.branches, k2.branches)
end
@@ -67,10 +67,10 @@ type action =
| Ration of int
| Ration_merge of int option
| Transfer_merge
- | Static_split of Cil_types.lval
- | Dynamic_split of Cil_types.lval
- | Static_merge of Cil_types.lval
- | Dynamic_merge of Cil_types.lval
+ | Static_split of Cil_types.exp
+ | Dynamic_split of Cil_types.exp
+ | Static_merge of Cil_types.exp
+ | Dynamic_merge of Cil_types.exp
| Update_dynamic_splits
exception InvalidAction
@@ -83,7 +83,7 @@ sig
exception Cant_split
val join : t -> t -> t
- val split : t -> Cil_types.lval -> (Integer.t * t) list
+ val split : t -> Cil_types.exp -> (Integer.t * t) list
end
@@ -100,8 +100,8 @@ struct
transfer_stamp = None;
branches = [];
loops = [];
- static_split = LvalMap.empty;
- dynamic_split = LvalMap.empty;
+ static_split = ExpMap.empty;
+ dynamic_split = ExpMap.empty;
}
let is_empty (p : 'a partition) : bool =
@@ -128,38 +128,38 @@ struct
let add_list (p : t) (l : (key * state) list) : t =
List.fold_left (fun p (k,x) -> add p k x) p l
- let split_state ~(static : bool) (lval : Cil_types.lval)
+ let split_state ~(static : bool) (exp : Cil_types.exp)
(key : key) (state : state) : (key * state) list =
try
let update_key (v,x) =
let k =
if static then
- { key with static_split = LvalMap.add lval v key.static_split }
+ { key with static_split = ExpMap.add exp v key.static_split }
else
- { key with dynamic_split = LvalMap.add lval v key.dynamic_split }
+ { key with dynamic_split = ExpMap.add exp v key.dynamic_split }
in
(k,x)
in
- List.map update_key (Domain.split state lval)
+ List.map update_key (Domain.split state exp)
with Domain.Cant_split ->
[(key,state)]
- let split ~(static : bool) (p : t) (lval : Cil_types.lval) =
+ let split ~(static : bool) (p : t) (exp : Cil_types.exp) =
let add_split key state p =
- add_list p (split_state ~static lval key state)
+ add_list p (split_state ~static exp key state)
in
KMap.fold add_split p KMap.empty
let update_dynamic_splits p =
(* Update one state *)
let update_state key state p =
- (* Split the states in the list l for the given lval *)
- let update_lval lval _ l =
+ (* 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,s) -> split_state ~static lval k s @ l) [] l
+ List.fold_left (fun l (k,s) -> split_state ~static exp k s @ l) [] l
in
- (* Foreach lval in original state: split *)
- let l = LvalMap.fold update_lval key.dynamic_split [(key,state)] in
+ (* Foreach exp in original state: split *)
+ let l = ExpMap.fold update_exp key.dynamic_split [(key,state)] in
add_list p l
in
KMap.fold update_state p KMap.empty
@@ -168,11 +168,11 @@ struct
KMap.fold (fun k x acc -> add acc (f k) x) p empty
let transfer_keys p = function
- | Static_split lval ->
- split ~static:true p lval
+ | Static_split exp ->
+ split ~static:true p exp
- | Dynamic_split lval ->
- split ~static:false p lval
+ | Dynamic_split exp ->
+ split ~static:false p exp
| Update_dynamic_splits ->
update_dynamic_splits p
@@ -230,11 +230,11 @@ struct
| Transfer_merge -> fun k ->
{ k with transfer_stamp = None }
- | Static_merge lval -> fun k ->
- { k with static_split = LvalMap.remove lval k.static_split }
+ | Static_merge exp -> fun k ->
+ { k with static_split = ExpMap.remove exp k.static_split }
- | Dynamic_merge lval -> fun k ->
- { k with dynamic_split = LvalMap.remove lval k.dynamic_split }
+ | Dynamic_merge exp -> fun k ->
+ { k with dynamic_split = ExpMap.remove exp k.dynamic_split }
in
map_keys transfer p
@@ -247,6 +247,7 @@ struct
let add p y =
let k' = { k with transfer_stamp = Some !t } in
incr t;
+ assert (not (KMap.mem k' p));
KMap.add k' y p
in
match f x with
diff --git a/src/plugins/value/engine/partition.mli b/src/plugins/value/engine/partition.mli
index 161b95ca6ba..6d2c5a27f3a 100644
--- a/src/plugins/value/engine/partition.mli
+++ b/src/plugins/value/engine/partition.mli
@@ -52,15 +52,15 @@
type branch = int
-module LvalMap = Cil_datatype.LvalStructEq.Map
+module ExpMap = Cil_datatype.ExpStructEq.Map
type key = private {
ration_stamp : int option;
transfer_stamp : int option;
branches : branch list;
loops : int list;
- static_split : Integer.t LvalMap.t;
- dynamic_split : Integer.t LvalMap.t;
+ static_split : Integer.t ExpMap.t;
+ dynamic_split : Integer.t ExpMap.t;
}
type 'a partition
@@ -73,10 +73,10 @@ type action =
| Ration of int (* starting ration stamp *)
| Ration_merge of int option (* new ration stamp for the merge state *)
| Transfer_merge
- | Static_split of Cil_types.lval
- | Dynamic_split of Cil_types.lval
- | Static_merge of Cil_types.lval
- | Dynamic_merge of Cil_types.lval
+ | Static_split of Cil_types.exp
+ | Dynamic_split of Cil_types.exp
+ | Static_merge of Cil_types.exp
+ | Dynamic_merge of Cil_types.exp
| Update_dynamic_splits
exception InvalidAction
@@ -89,7 +89,7 @@ sig
exception Cant_split
val join : t -> t -> t
- val split : t -> Cil_types.lval -> (Integer.t * t) list
+ val split : t -> Cil_types.exp -> (Integer.t * t) list
end
diff --git a/src/plugins/value/engine/partitioned_dataflow.ml b/src/plugins/value/engine/partitioned_dataflow.ml
index e3d842a247f..14ede992285 100644
--- a/src/plugins/value/engine/partitioned_dataflow.ml
+++ b/src/plugins/value/engine/partitioned_dataflow.ml
@@ -97,7 +97,7 @@ module Make_Dataflow
(* --- Abstract values storage --- *)
- module Partition = Trace_partitioning.Make (Domain) (AnalysisParam)
+ module Partition = Trace_partitioning.Make (Domain) (Transfer) (AnalysisParam)
type store = Partition.store
type widening = Partition.widening
diff --git a/src/plugins/value/engine/partitioning_parameters.ml b/src/plugins/value/engine/partitioning_parameters.ml
index d625a9ef865..87d8cd6fd75 100644
--- a/src/plugins/value/engine/partitioning_parameters.ml
+++ b/src/plugins/value/engine/partitioning_parameters.ml
@@ -102,7 +102,7 @@ struct
let add name l =
try
let vi = Globals.Vars.find_from_astinfo name VGlobal in
- Cil.var vi :: l
+ Cil.evar vi :: l
with Not_found ->
warn ~current:false "cannot find the global variable %s for value \
partitioning" name;
@@ -111,19 +111,18 @@ struct
ValuePartitioning.fold add []
let flow_actions stmt =
- let term_to_lval = function
- | {term_node = TLval tlv} ->
- !Db.Properties.Interp.term_lval_to_lval ~result:None tlv
- | _ ->
- warn "split/merge expressions must be lvalues";
- raise Exit
+ let term_to_exp term =
+ !Db.Properties.Interp.term_to_exp ~result:None term
in
let map_annot acc t =
try
match t with
- | FlowSplit t -> Partition.Static_split (term_to_lval t) :: acc
- | FlowMerge t -> Partition.Static_merge (term_to_lval t) :: acc
- with Exit -> acc (* Impossible to convert term to lval *)
+ | FlowSplit t -> Partition.Static_split (term_to_exp t) :: acc
+ | FlowMerge t -> Partition.Static_merge (term_to_exp t) :: acc
+ with
+ Db.Properties.Interp.No_conversion ->
+ warn "split/merge expressions must be valid expressions";
+ acc (* Impossible to convert term to lval *)
in
List.fold_left map_annot [] (get_flow_annot stmt)
end
diff --git a/src/plugins/value/engine/state_partitioning.mli b/src/plugins/value/engine/state_partitioning.mli
index 7395634a2c1..86956872280 100644
--- a/src/plugins/value/engine/state_partitioning.mli
+++ b/src/plugins/value/engine/state_partitioning.mli
@@ -38,7 +38,7 @@ sig
val merge : Cil_types.stmt -> bool
val unroll : loop -> int
val history_size : int
- val universal_splits : Cil_types.lval list
+ val universal_splits : Cil_types.exp list
val flow_actions : Cil_types.stmt -> Partition.action list
end
@@ -143,6 +143,8 @@ end
module type Domain = Partitioning.Domain
-module type Partitioning =
- functor (Domain : Domain) (Kf : Kf) ->
+module type Partitioning = functor
+ (Domain : Abstract_domain.External)
+ (Transfer : Transfer_stmt.S with type state = Domain.t)
+ (Kf : Kf) ->
Partition with type state = Domain.t
diff --git a/src/plugins/value/engine/trace_partitioning.ml b/src/plugins/value/engine/trace_partitioning.ml
index 081851332d4..c93ab0ad40d 100644
--- a/src/plugins/value/engine/trace_partitioning.ml
+++ b/src/plugins/value/engine/trace_partitioning.ml
@@ -26,7 +26,10 @@ open State_partitioning
open Partition
-module Make (Domain : Domain) (Kf : Kf) =
+module Make
+ (Domain : Abstract_domain.External)
+ (Transfer : Transfer_stmt.S with type state = Domain.t)
+ (Kf : Kf) =
struct
module Parameters = Partitioning_parameters.Make (Kf)
@@ -36,63 +39,10 @@ struct
(* Add the split function to the domain *)
module Domain =
struct
- include Domain
+ exception Cant_split = Transfer.Cant_split
+ let split = Transfer.split_by_value
- module Val = struct
- include Main_values.CVal
- include Structure.Open (Structure.Key_Value) (Main_values.CVal)
- let reduce t = t
- end
-
- module Eva =
- Evaluation.Make
- (Val)
- (Main_locations.PLoc)
- (Cvalue_domain.State)
-
- exception Cant_split
-
- (* TODO: size of split limit *)
- let split state lval =
- (* Whenever the split fail, warn the user and exit with an exception *)
- let fail message =
- Value_parameters.warning ~once:true message;
- raise Cant_split
- in
- (* Get the cvalue *)
- let cvalue = match get Cvalue_domain.key with
- | Some get_cvalue -> get_cvalue state
- | None -> fail "cannot partition by value when the CValue domain is not\
- active"
- in
- (* Retrieve the location of the lval *)
- let cstate = Cvalue_domain.inject cvalue in
- let location = match Eva.lvaluate ~for_writing:true cstate lval with
- | `Value (_valuation, loc, _typ), _alarmset ->
- Precise_locs.imprecise_location loc
- | `Bottom, _alarmset ->
- fail "cannot partition by value on an imprecise lvalue"
- in
- (* Extract the ival *)
- let ival =
- try
- let v = Cvalue.Model.find cvalue location in
- Cvalue.V.project_ival v
- with Cvalue.V.Not_based_on_null ->
- fail "cannot partition by value on pointers"
- in
- (* Build a state with the lvalue set to a singleton *)
- let build i acc =
- let v = Cvalue.V.inject_int i in
- let cvalue = Cvalue.Model.add_binding ~exact:true cvalue location v in
- let new_state = set Cvalue_domain.key cvalue state in
- (i,new_state) :: acc
- in
- (* For each integer of the ival, build a new state *)
- try
- Ival.fold_int build ival []
- with Abstract_interp.Error_Top ->
- fail "too many values to partition by value on"
+ include Domain
end
module Index = Partitioning.Make (Domain)
diff --git a/src/plugins/value/engine/transfer_stmt.ml b/src/plugins/value/engine/transfer_stmt.ml
index 22ec00d8c54..b3cea597c20 100644
--- a/src/plugins/value/engine/transfer_stmt.ml
+++ b/src/plugins/value/engine/transfer_stmt.ml
@@ -40,6 +40,8 @@ module type S = sig
state -> (stmt * lval list * lval list * lval list * stmt ref list) list ->
unit or_bottom
val enter_scope: kernel_function -> varinfo list -> state -> state
+ exception Cant_split
+ val split_by_value: state -> exp -> (Integer.t * state) list
type call_result = {
states: state list or_bottom;
cacheable: Value_types.cacheable;
@@ -872,6 +874,55 @@ module Make (Abstract: Abstractions.Eva) = struct
in
List.fold_left initialize_volatile state vars
+
+ (* ------------------------------------------------------------------------ *)
+ (* Split by value *)
+ (* ------------------------------------------------------------------------ *)
+
+ exception Cant_split
+
+ let split_by_value state exp =
+ (* Whenever the split fails, warn the user and raise an exception *)
+ let fail message =
+ Value_parameters.warning ~once:true message;
+ raise Cant_split
+ in
+ (* Evaluate the expression *)
+ let valuation, value = match Eval.evaluate ~reduction:false state exp with
+ | `Value (valuation, value), alarms when Alarmset.is_empty alarms ->
+ valuation, value
+ | _ ->
+ fail "the split expression 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 "cannot partition by value 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 "cannot partition by value on pointers"
+ 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
+ | _ -> (* 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 "too many values to partition by value on"
+ end
end
diff --git a/src/plugins/value/engine/transfer_stmt.mli b/src/plugins/value/engine/transfer_stmt.mli
index a2e64699a2e..7d8cee112e8 100644
--- a/src/plugins/value/engine/transfer_stmt.mli
+++ b/src/plugins/value/engine/transfer_stmt.mli
@@ -51,6 +51,11 @@ module type S = sig
val enter_scope: kernel_function -> varinfo list -> state -> state
+ exception Cant_split
+
+ val split_by_value: state -> exp -> (Integer.t * state) list
+
+
type call_result = {
states: state list or_bottom;
cacheable: Value_types.cacheable;
--
GitLab