From 0850d5349ba30e255220b15525434727a70eead2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 5 Apr 2019 22:42:33 +0200
Subject: [PATCH] [Eva] Partition: do not export split_monitor, simplifies the
split/merge actions.
split_monitors are created and internally used by partition.
New type split_kind to distinguish between static and dynamic splits, instead
of using different constructors in the action type.
---
src/plugins/value/engine/partition.ml | 39 +++++++++----------
src/plugins/value/engine/partition.mli | 18 ++-------
.../value/engine/partitioning_parameters.ml | 14 ++++---
.../value/engine/state_partitioning.mli | 1 -
4 files changed, 30 insertions(+), 42 deletions(-)
diff --git a/src/plugins/value/engine/partition.ml b/src/plugins/value/engine/partition.ml
index 8c555ff0a8d..83a988cfd11 100644
--- a/src/plugins/value/engine/partition.ml
+++ b/src/plugins/value/engine/partition.ml
@@ -134,6 +134,8 @@ type unroll_limit =
| ExpLimit of Cil_types.exp
| IntLimit of int
+type split_kind = Static | Dynamic
+
type action =
| Enter_loop of unroll_limit
| Leave_loop
@@ -141,10 +143,8 @@ type action =
| Branch of branch * int
| Ration of int
| Ration_merge of (int*int) option
- | 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
+ | Split of Cil_types.exp * split_kind * int
+ | Merge of Cil_types.exp * split_kind
| Update_dynamic_splits
exception InvalidAction
@@ -295,16 +295,15 @@ struct
(* --- Applying partitioning actions onto flows --------------------------- *)
- let split_state ~monitor ~(static : bool) (exp : Cil_types.exp)
+ let split_state ~monitor (kind : split_kind) (exp : Cil_types.exp)
(key : key) (state : state) : (key * state) list =
try
+ let add value map = ExpMap.add exp (value, monitor) map in
let update_key (v,x) =
let k =
- let m = monitor in
- if static then
- { key with static_split = ExpMap.add exp (v,m) key.static_split }
- else
- { key with dynamic_split = ExpMap.add exp (v,m) key.dynamic_split }
+ match kind with
+ | Static -> { key with static_split = add v key.static_split }
+ | Dynamic -> { key with dynamic_split = add v key.dynamic_split }
in
(k,x)
in
@@ -312,9 +311,10 @@ struct
with Operation_failed ->
[(key,state)]
- let split ~monitor ~(static : bool) (p : t) (exp : Cil_types.exp) =
+ let split ~limit (kind : split_kind) (exp : Cil_types.exp) (p : t) =
+ let monitor = new_monitor limit in
let add_split acc (key,state) =
- split_state ~monitor ~static exp key state @ acc
+ split_state ~monitor kind exp key state @ acc
in
List.fold_left add_split [] p
@@ -324,7 +324,7 @@ struct
(* Split the states in the list l for the given exp *)
let update_exp exp (_i,monitor) l =
let resplit acc (k,x) =
- split_state ~monitor ~static:false exp k x @ acc
+ split_state ~monitor Dynamic exp k x @ acc
in
List.fold_left resplit [] l
in
@@ -337,18 +337,15 @@ struct
List.map (fun (k,x) -> f k x, x) p
let transfer_keys p = function
- | Static_split (exp,monitor) ->
- split ~monitor ~static:true p exp
-
- | Dynamic_split (exp,monitor) ->
- split ~monitor ~static:false p exp
+ | Split (expr, kind, limit) ->
+ split ~limit kind expr p
| Update_dynamic_splits ->
update_dynamic_splits p
| action -> (* Simple map transfer functions *)
let transfer = match action with
- | Static_split _ | Dynamic_split _ | Update_dynamic_splits ->
+ | Split _ | Update_dynamic_splits ->
assert false (* Handled above *)
| Enter_loop limit_kind -> fun k x ->
@@ -402,10 +399,10 @@ struct
| Ration_merge ration_stamp -> fun k _x ->
{ k with ration_stamp }
- | Static_merge exp -> fun k _x ->
+ | Merge (exp, Static) -> fun k _x ->
{ k with static_split = ExpMap.remove exp k.static_split }
- | Dynamic_merge exp -> fun k _x ->
+ | Merge (exp, Dynamic) -> fun k _x ->
{ k with dynamic_split = ExpMap.remove exp k.dynamic_split }
in
map_keys transfer p
diff --git a/src/plugins/value/engine/partition.mli b/src/plugins/value/engine/partition.mli
index f5e03e8642f..27f287d438d 100644
--- a/src/plugins/value/engine/partition.mli
+++ b/src/plugins/value/engine/partition.mli
@@ -20,16 +20,6 @@
(* *)
(**************************************************************************)
-(* 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
@@ -101,6 +91,8 @@ type unroll_limit =
| ExpLimit of Cil_types.exp
| IntLimit of int
+type split_kind = Static | Dynamic
+
type action =
| Enter_loop of unroll_limit
| Leave_loop
@@ -108,10 +100,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 * split_monitor)
- | Dynamic_split of (Cil_types.exp * split_monitor)
- | Static_merge of Cil_types.exp
- | Dynamic_merge of Cil_types.exp
+ | Split of Cil_types.exp * split_kind * int
+ | Merge of Cil_types.exp * split_kind
| Update_dynamic_splits
exception InvalidAction
diff --git a/src/plugins/value/engine/partitioning_parameters.ml b/src/plugins/value/engine/partitioning_parameters.ml
index 60ed14ebdc6..3cd62544005 100644
--- a/src/plugins/value/engine/partitioning_parameters.ml
+++ b/src/plugins/value/engine/partitioning_parameters.ml
@@ -110,8 +110,7 @@ struct
let add name l =
try
let vi = Globals.Vars.find_from_astinfo name VGlobal in
- let m = Partition.new_monitor split_limit in
- Partition.Dynamic_split (Cil.evar vi, m) :: l
+ Partition.Split (Cil.evar vi, Partition.Dynamic, split_limit) :: l
with Not_found ->
warn ~current:false "cannot find the global variable %s for value \
partitioning" name;
@@ -120,12 +119,15 @@ struct
ValuePartitioning.fold add []
let flow_actions stmt =
+ let kind = Partition.Static in
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,m) :: acc
- | FlowMerge t -> Partition.Static_merge (term_to_exp t) :: acc
+ let action =
+ match t with
+ | FlowSplit t -> Partition.Split (term_to_exp t, kind, split_limit)
+ | FlowMerge t -> Partition.Merge (term_to_exp t, kind)
+ in
+ action :: acc
with
Db.Properties.Interp.No_conversion ->
warn "split/merge expressions must be valid expressions";
diff --git a/src/plugins/value/engine/state_partitioning.mli b/src/plugins/value/engine/state_partitioning.mli
index fdaaec4ff31..d5b8df9227e 100644
--- a/src/plugins/value/engine/state_partitioning.mli
+++ b/src/plugins/value/engine/state_partitioning.mli
@@ -38,7 +38,6 @@ sig
val merge : Cil_types.stmt -> bool
val unroll : loop -> Partition.unroll_limit
val history_size : int
- val split_limit : int
val universal_splits : Partition.action list
val flow_actions : Cil_types.stmt -> Partition.action list
end
--
GitLab