From b6cf5ea4ee5d2a3205eb725a5a2f564baf77c097 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Fri, 19 Oct 2018 15:46:12 +0200
Subject: [PATCH] [Eva] Uniformize transfer functions and use association list
instead of maps for flow
---
src/kernel_services/abstract_interp/bottom.ml | 5 +
.../abstract_interp/bottom.mli | 1 +
src/plugins/value/engine/partition.ml | 278 +++++++--------
src/plugins/value/engine/partition.mli | 65 ++--
.../value/engine/partitioned_dataflow.ml | 325 +++++++++---------
.../value/engine/state_partitioning.mli | 66 ++--
.../value/engine/trace_partitioning.ml | 188 ++++++----
7 files changed, 498 insertions(+), 430 deletions(-)
diff --git a/src/kernel_services/abstract_interp/bottom.ml b/src/kernel_services/abstract_interp/bottom.ml
index c6ae61d80ae..def68537529 100644
--- a/src/kernel_services/abstract_interp/bottom.ml
+++ b/src/kernel_services/abstract_interp/bottom.ml
@@ -134,6 +134,11 @@ let to_list = function
| `Bottom -> []
| `Value v -> [v]
+let of_list = function
+ | [] -> `Bottom
+ | [v] -> `Value v
+ | _ -> assert false
+
let bot_of_list = function
| [] -> `Bottom
| l -> `Value l
diff --git a/src/kernel_services/abstract_interp/bottom.mli b/src/kernel_services/abstract_interp/bottom.mli
index 7fca1504bf3..8c5a6ab97ce 100644
--- a/src/kernel_services/abstract_interp/bottom.mli
+++ b/src/kernel_services/abstract_interp/bottom.mli
@@ -69,6 +69,7 @@ module Bound_Lattice
(** Conversion functions. *)
val to_list: 'a or_bottom -> 'a list
+val of_list: 'a list -> 'a or_bottom
val bot_of_list: 'a list -> 'a list or_bottom
val list_of_bot: 'a list or_bottom -> 'a list
val all: 'a or_bottom list -> 'a list
diff --git a/src/plugins/value/engine/partition.ml b/src/plugins/value/engine/partition.ml
index 54a03072c68..cc63597feab 100644
--- a/src/plugins/value/engine/partition.ml
+++ b/src/plugins/value/engine/partition.ml
@@ -20,25 +20,50 @@
(* *)
(**************************************************************************)
-(* Utility function on options *)
-let opt_flatten (type a) (o : a option option) : a option =
- Extlib.opt_conv None o
-
module ExpMap = Cil_datatype.ExpStructEq.Map
-module LoopList = Datatype.List (Datatype.Pair (Datatype.Int) (Datatype.Int))
+module IntPair = Datatype.Pair (Datatype.Int) (Datatype.Int)
+module LoopList = Datatype.List (IntPair)
module BranchList = Datatype.List (Datatype.Int)
type branch = int
type key = {
- ration_stamp : int option;
- transfer_stamp : int option;
+ ration_stamp : (int * int) option;
branches : branch list;
loops : (int * int) list;
static_split : Integer.t ExpMap.t;
dynamic_split : Integer.t ExpMap.t;
}
+let zero_key : key = {
+ ration_stamp = None;
+ branches = [];
+ loops = [];
+ static_split = ExpMap.empty;
+ dynamic_split = ExpMap.empty;
+}
+
+let pretty_key fmt key =
+ begin match key.ration_stamp with
+ | Some (n,_) -> Format.fprintf fmt "#%d" n
+ | None -> ()
+ end;
+ Pretty_utils.pp_list ~pre:"[@[" ~sep:" ;@ " ~suf:"@]]"
+ Format.pp_print_int
+ fmt
+ key.branches;
+ Pretty_utils.pp_list ~pre:"(@[" ~sep:" ;@ " ~suf:"@])"
+ (fun fmt (i,_j) -> Format.pp_print_int fmt i)
+ fmt
+ key.loops;
+ Pretty_utils.pp_list ~pre:"{@[" ~sep:" ;@ " ~suf:"@]}"
+ (fun fmt (e,i) -> Format.fprintf fmt "%a:%a"
+ Cil_printer.pp_exp e
+ (Integer.pretty ~hexa:false) i)
+ fmt
+ (ExpMap.bindings key.static_split @ ExpMap.bindings key.dynamic_split)
+
+
module Key =
struct
type t = key
@@ -47,8 +72,7 @@ struct
let (<?>) c (cmp,x,y) =
if c = 0 then cmp x y else c
in
- Extlib.opt_compare (-) k1.ration_stamp k2.ration_stamp
- <?> (Extlib.opt_compare (-), k1.transfer_stamp, k2.transfer_stamp)
+ Extlib.opt_compare IntPair.compare k1.ration_stamp k2.ration_stamp
<?> (LoopList.compare, k1.loops, k2.loops)
<?> (ExpMap.compare Integer.compare, k1.static_split, k2.static_split)
<?> (ExpMap.compare Integer.compare, k1.dynamic_split, k2.dynamic_split)
@@ -61,20 +85,6 @@ module KMap = Map.Make (Key)
type 'a partition = 'a KMap.t
type 'a transfer_function = (key * 'a) list -> (key * 'a) list
-let stamp_after_transfer k = function
- | [x] -> [(k,x)]
- | l ->
- let t = ref 0 in
- let add acc x =
- let k' = { k with transfer_stamp = Some !t } in
- incr t;
- (k',x) :: acc
- in
- List.fold_left add [] l
-
-let update_after_call k l =
- List.map (fun x -> k,x) l
-
type unroll_limit =
| ExpLimit of Cil_types.exp
| IntLimit of int
@@ -85,8 +95,7 @@ type action =
| Incr_loop
| Branch of branch * int
| Ration of int
- | Ration_merge of int option
- | Transfer_merge
+ | Ration_merge of (int*int) option
| Static_split of Cil_types.exp
| Dynamic_split of Cil_types.exp
| Static_merge of Cil_types.exp
@@ -108,46 +117,82 @@ sig
end
-module Make (Domain : InputDomain) =
+let empty : 'a partition =
+ KMap.empty
+
+let is_empty (p : 'a partition) : bool =
+ KMap.is_empty p
+
+let size (p : 'a partition) : int =
+ KMap.fold (fun _k _x n -> n + 1) p 0
+
+let to_list (p : 'a partition) : 'a list =
+ KMap.fold (fun _k x l -> x :: l) p []
+
+let find = KMap.find
+let replace = KMap.add
+
+let merge (f : 'a option -> 'b option -> 'c option) (p1 : 'a partition)
+ (p2 : 'b partition) : 'c partition =
+ KMap.merge (fun _k o1 o2 -> f o1 o2) p1 p2
+
+let iter (f : 'a -> unit) (p : 'a partition) : unit =
+ KMap.iter (fun _k x -> f x) p
+
+let iteri (f : key -> 'a -> unit) (p : 'a partition) : unit =
+ KMap.iter f p
+
+
+(* Utility function on options *)
+let opt_flatten (type a) (o : a option option) : a option =
+ Extlib.opt_conv None o
+
+let map_states (f : 'a -> 'a) (p : 'a partition) : 'a partition =
+ KMap.map f p
+
+let filter_keys (f : key -> bool) (p : 'a partition) : 'a partition =
+ KMap.filter (fun k _x -> f k) p
+
+let map_filter (f : key -> 'a -> 'b option) (p : 'a partition) : 'b partition =
+ KMap.merge (fun k o _ -> opt_flatten (Extlib.opt_map (f k) o)) p KMap.empty
+
+
+module MakeFlow (Domain : InputDomain) =
struct
- type t = Domain.t partition
type state = Domain.t
+ type t = (key * state) list
- let empty : 'a partition =
- KMap.empty
-
- let empty_key : key = {
- ration_stamp = None;
- transfer_stamp = None;
- branches = [];
- loops = [];
- static_split = ExpMap.empty;
- dynamic_split = ExpMap.empty;
- }
-
- let is_empty (p : 'a partition) : bool =
- KMap.is_empty p
-
- let initial (l : 'a list) : 'a partition =
- let stamp = ref 0 in
- let add p state =
- let k = { empty_key with ration_stamp = Some !stamp } in
- incr stamp;
- KMap.add k state p
- in
- List.fold_left add KMap.empty l
-
- let add (p : t) (k : key) (x : state) : t =
- (* Join states with the same key *)
- let x =
- try
- Domain.join (KMap.find k p) x
- with Not_found -> x
+ let empty = []
+
+ let initial (p : 'a list) : t =
+ List.map (fun state -> zero_key, state) p
+
+ let to_list (f : t) : state list =
+ List.map snd f
+
+ let of_partition (p : state partition) : t =
+ KMap.fold (fun k x l -> (k,x) :: l) p []
+
+ let to_partition (p : t) : state partition =
+ let add p (k,x) =
+ (* Join states with the same key *)
+ let x' =
+ try
+ Domain.join (KMap.find k p) x
+ with Not_found -> x
+ in
+ KMap.add k x' p
in
- KMap.add k x p
+ List.fold_left add KMap.empty p
- let add_list (p : t) (l : (key * state) list) : t =
- List.fold_left (fun p (k,x) -> add p k x) p l
+ let is_empty (p : t) =
+ p = []
+
+ let size (p : t) =
+ List.length p
+
+ let union (p1 : t) (p2 : t) : t =
+ p1 @ p2
let split_state ~(static : bool) (exp : Cil_types.exp)
(key : key) (state : state) : (key * state) list =
@@ -166,32 +211,29 @@ struct
[(key,state)]
let split ~(static : bool) (p : t) (exp : Cil_types.exp) =
- let add_split key state p =
- add_list p (split_state ~static exp key state)
+ let add_split acc (key,state) =
+ split_state ~static exp key state @ acc
in
- KMap.fold add_split p KMap.empty
+ List.fold_left add_split [] p
let update_dynamic_splits p =
(* Update one state *)
- let update_state key state p =
+ let update_state acc (key,state) =
(* 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 exp k s @ l) [] l
+ List.fold_left (fun l (k,x) -> split_state ~static exp k x @ l) [] l
in
(* Foreach exp in original state: split *)
- let l = ExpMap.fold update_exp key.dynamic_split [(key,state)] in
- add_list p l
+ ExpMap.fold update_exp key.dynamic_split [(key,state)] @ acc
in
- KMap.fold update_state p KMap.empty
+ List.fold_left update_state [] p
- let map_keys (f : key -> state -> key) (p : t) =
- KMap.fold (fun k x acc -> add acc (f k x) x) p empty
+ let map_keys (f : key -> state -> key) (p : t) : t =
+ List.map (fun (k,x) -> f k x, x) p
let transfer (f : state transfer_function) (p : t) : t =
- let l = KMap.fold (fun k x l -> (k,x) :: l) p [] in
- let l' = f l in
- add_list empty (l')
+ f p
let transfer_keys p = function
| Static_split exp ->
@@ -252,16 +294,13 @@ struct
| Ration (min) ->
let r = ref min in
fun k _x ->
- let ration_stamp = Some !r in
+ let ration_stamp = Some (!r, 0) in
incr r;
{ k with ration_stamp }
- | Ration_merge ration_stamp -> fun k _x ->
+ | Ration_merge ration_stamp -> fun k _x ->
{ k with ration_stamp }
- | Transfer_merge -> fun k _x ->
- { k with transfer_stamp = None }
-
| Static_merge exp -> fun k _x ->
{ k with static_split = ExpMap.remove exp k.static_split }
@@ -270,22 +309,27 @@ struct
in
map_keys transfer p
- let map_states (f : 'a -> 'a) (p : 'a partition) : 'a partition =
- KMap.map f p
-
- let transfer_states (f : 'a -> 'a list) (p : 'a partition) : 'a partition =
- let transfer_one k x p =
- let l = stamp_after_transfer k (f x) in
- List.fold_left (fun p (k,x) -> KMap.add k x p) p l
+ let transfer_states (f : state -> state list) (p : t) : t =
+ let n = ref 0 in
+ let transfer acc (k,x) =
+ let add =
+ match k.ration_stamp with
+ (* No ration stam, just add the state to the list *)
+ | None -> fun l y -> (k,y) :: l
+ (* There is a ration stamp, set the second part of the stamp to a unique transfer number *)
+ | Some (s,_) -> fun l y ->
+ let k' = { k with ration_stamp = Some (s, !n) } in
+ incr n;
+ (k',y) :: l
+ in
+ List.fold_left add acc (f x)
in
- KMap.fold transfer_one p KMap.empty
+ List.fold_left transfer [] p
- (*
- let legacy_transfer_states (f : 'a list -> 'a list) (p : 'a partition)
- : 'a partition =
+ let legacy_transfer_states (f : state list -> state list) (p : t) : t =
(* Group the states in buckets, where each bucket is a list of states
with the same key except for the ration stamp *)
- let fill_buckets k x buckets =
+ let fill_buckets buckets (k,x) =
(* Ignore the ration stamp *)
let k = { k with ration_stamp = None } in
(* Find the bucket *)
@@ -296,55 +340,15 @@ struct
(* Add the state to the bucket *)
KMap.add k (x :: contents) buckets
in
- let buckets = KMap.fold fill_buckets p KMap.empty in
+ let buckets = List.fold_left fill_buckets KMap.empty p in
(* Apply the transfer function to each bucket *)
let result = KMap.map f buckets in
- (* Rebuild a partition by rationing out all the states *)
- let r = ref 0 in
- let ration_bucket k bucket acc =
- let ration_one acc x =
- let k' = { k with ration_stamp = Some !r } in
- incr r;
- KMap.add k' x acc
- in
- List.fold_left ration_one acc bucket
- in
- KMap.fold ration_bucket result KMap.empty *)
-
- let find = KMap.find
- let replace = KMap.add
-
- let to_list (p : 'a partition) : 'a list =
- KMap.fold (fun _k x l -> x :: l) p []
-
- let size (p : 'a partition) : int =
- KMap.fold (fun _k _x n -> n + 1) p 0
-
-
- let merge (f : 'a option -> 'b option -> 'c option) (p1 : 'a partition)
- (p2 : 'b partition) : 'c partition =
- KMap.merge (fun _k o1 o2 -> f o1 o2) p1 p2
-
- (* Almost like Map.union of Ocaml 4.03.0 *)
- let union (f : 'a -> 'a -> 'a) (p1 : 'a partition)
- (p2 : 'a partition) : 'a partition =
- let g _k o1 o2 =
- match o1 with
- | None -> o2
- | Some x1 ->
- match o2 with
- | None -> o1
- | Some x2 -> Some (f x1 x2)
+ (* Rebuild the flow *)
+ let add_bucket k bucket acc =
+ List.map (fun x -> k,x) bucket @ acc
in
- KMap.merge g p1 p2
-
- let iter (f : 'a -> unit) (p : 'a partition) : unit =
- KMap.iter (fun _k x -> f x) p
-
- let filter_keys (f : key -> bool) (p : 'a partition) : 'a partition =
- KMap.filter (fun k _x -> f k) p
+ KMap.fold add_bucket result []
- let map_filter (f : key -> 'a -> 'b option) (p : 'a partition)
- : 'b partition =
- KMap.merge (fun k o _ -> opt_flatten (Extlib.opt_map (f k) o)) p KMap.empty
+ let iter (f : state -> unit) (p : t) : unit =
+ List.iter (fun (_k,x) -> f x) p
end
diff --git a/src/plugins/value/engine/partition.mli b/src/plugins/value/engine/partition.mli
index ee417755012..c817ca18685 100644
--- a/src/plugins/value/engine/partition.mli
+++ b/src/plugins/value/engine/partition.mli
@@ -55,20 +55,19 @@ type branch = int
module ExpMap = Cil_datatype.ExpStructEq.Map
type key = private {
- ration_stamp : int option;
- transfer_stamp : int option;
+ ration_stamp : (int * int) option;
branches : branch list;
loops : (int * int) list;
static_split : Integer.t ExpMap.t;
dynamic_split : Integer.t ExpMap.t;
}
+val pretty_key : Format.formatter -> key -> unit
+
+
type 'a partition
type 'a transfer_function = (key * 'a) list -> (key * 'a) list
-val stamp_after_transfer : key -> 'a list -> (key * 'a) list
-val update_after_call : key -> 'a list -> (key * 'a) list
-
type unroll_limit =
| ExpLimit of Cil_types.exp
| IntLimit of int
@@ -79,8 +78,7 @@ type action =
| Incr_loop
| Branch of branch * int (* branch taken, max branches in history *)
| Ration of int (* starting ration stamp *)
- | Ration_merge of int option (* new ration stamp for the merge state *)
- | Transfer_merge
+ | Ration_merge of (int * int) option (* new ration stamp for the merge state *)
| Static_split of Cil_types.exp
| Dynamic_split of Cil_types.exp
| Static_merge of Cil_types.exp
@@ -90,6 +88,25 @@ type action =
exception InvalidAction
+val empty : 'a partition
+val is_empty : 'a partition -> bool
+val size : 'a partition -> int
+
+val to_list : 'a partition -> 'a list
+
+val find : key -> 'a partition -> 'a
+val replace : key -> 'a -> 'a partition -> 'a partition
+
+val merge : ('a option -> 'b option -> 'c option) -> 'a partition ->
+ 'b partition -> 'c partition
+
+val iter : ('a -> unit) -> 'a partition -> unit
+val iteri : (key -> 'a -> unit) -> 'a partition -> unit
+val filter_keys : (key -> bool) -> 'a partition -> 'a partition
+val map_states : ('a -> 'a) -> 'a partition -> 'a partition
+val map_filter : (key -> 'a -> 'b option) -> 'a partition -> 'b partition
+
+
module type InputDomain =
sig
type t
@@ -101,29 +118,27 @@ sig
val eval_exp_to_int : t -> Cil_types.exp -> int
end
-
-module Make (Domain : InputDomain) :
+module MakeFlow (Domain : InputDomain) :
sig
- type t = Domain.t partition
type state = Domain.t
+ type t
- val empty : 'a partition
- val is_empty : 'a partition -> bool
- val initial : 'a list -> 'a partition
- val size : 'a partition -> int
- val to_list : 'a partition -> 'a list
+ val empty : t
- val find : key -> 'a partition -> 'a
- val replace : key -> 'a -> 'a partition -> 'a partition
- val merge : ('a option -> 'b option -> 'c option) -> 'a partition
- -> 'b partition -> 'c partition
- val union : ('a -> 'a -> 'a) -> 'a partition -> 'a partition -> 'a partition
+ val initial : state list -> t
+ val to_list : t -> state list
+ val of_partition : state partition -> t
+ val to_partition : t -> state partition
+
+ val is_empty : t -> bool
+ val size : t -> int
+
+ val union : t -> t -> t
- val iter : ('a -> unit) -> 'a partition -> unit
val transfer : state transfer_function -> t -> t
val transfer_keys : t -> action -> t
- val filter_keys : (key -> bool) -> 'a partition -> 'a partition
- val map_states : ('a -> 'a) -> 'a partition -> 'a partition
- val transfer_states : ('a -> 'a list) -> 'a partition -> 'a partition
- val map_filter : (key -> 'a -> 'b option) -> 'a partition -> 'b partition
+ val transfer_states : (state -> state list) -> t -> t
+ val legacy_transfer_states : (state list -> state list) -> t -> t
+
+ val iter : (state -> unit) -> t -> unit
end
diff --git a/src/plugins/value/engine/partitioned_dataflow.ml b/src/plugins/value/engine/partitioned_dataflow.ml
index 14ede992285..e1b461e4c09 100644
--- a/src/plugins/value/engine/partitioned_dataflow.ml
+++ b/src/plugins/value/engine/partitioned_dataflow.ml
@@ -100,8 +100,9 @@ module Make_Dataflow
module Partition = Trace_partitioning.Make (Domain) (Transfer) (AnalysisParam)
type store = Partition.store
+ type flow = Partition.flow
+ type tank = Partition.tank
type widening = Partition.widening
- type propagation = Partition.propagation
type edge_info = {
mutable fireable : bool (* Does any states survive the transition ? *)
@@ -141,9 +142,10 @@ module Make_Dataflow
| `Bottom -> Domain.top (* No analysis in this case. *)
| `Value state -> state
- let initial_propagation =
- -1, (* dummy edge identifier *)
- Partition.initial_propagation (States.to_list initial_states)
+ let initial_tank =
+ Partition.initial_tank (States.to_list initial_states)
+ let get_initial_flow () =
+ -1 (* Dummy edge id *), Partition.drain initial_tank
let post_conditions = ref false
@@ -175,7 +177,7 @@ module Make_Dataflow
VertexTable.create control_point_count
let w_table : widening VertexTable.t =
VertexTable.create 7
- let e_table : (propagation * edge_info) EdgeTable.t =
+ let e_table : (tank * edge_info) EdgeTable.t =
EdgeTable.create transition_count
(* Default (Initial) stores on vertex and edges *)
@@ -183,23 +185,18 @@ module Make_Dataflow
Partition.empty_store ~stmt:v.vertex_start_of
let default_vertex_widening (v : vertex) () : widening =
Partition.empty_widening ~stmt:v.vertex_start_of
- let default_edge_propagation () : propagation * edge_info =
- Partition.empty_propagation (), { fireable = false }
+ let default_edge_tank () : tank * edge_info =
+ Partition.empty_tank (), { fireable = false }
(* Get the stores associated to a control point or edge *)
let get_vertex_store (v : vertex) : store =
VertexTable.find_or_add v_table v ~default:(default_vertex_store v)
let get_vertex_widening (v : vertex) : widening =
VertexTable.find_or_add w_table v ~default:(default_vertex_widening v)
- let get_edge_propagation (e : vertex edge) : propagation * edge_info =
- EdgeTable.find_or_add e_table e ~default:default_edge_propagation
- let get_pred_propagations (v : vertex) : ('branch * propagation) list =
- let get (_,e,_) =
- e.edge_key, fst (get_edge_propagation e)
- in
- List.map get (G.pred_e graph v)
- let get_succ_propagations (v : vertex) : propagation list =
- List.map (fun (_,e,_) -> fst (get_edge_propagation e)) (G.succ_e graph v)
+ let get_edge_data (e : vertex edge) : tank * edge_info =
+ EdgeTable.find_or_add e_table e ~default:default_edge_tank
+ let get_succ_tanks (v : vertex) : tank list =
+ List.map (fun (_,e,_) -> fst (get_edge_data e)) (G.succ_e graph v)
module StmtTable = struct
include Cil_datatype.Stmt.Hashtbl
@@ -224,47 +221,54 @@ module Make_Dataflow
type state = Domain.t
- (** Join every state in the list *)
- let smash (l : state list) : state or_bottom =
- match l with
- | [] -> `Bottom
- | v1 :: l -> `Value (List.fold_left Domain.join v1 l)
+ type transfer_function = state -> state list
+
+ let id : transfer_function = fun x -> [x]
(* Thse lifting function helps to uniformize the transfer functions to a
common signature *)
- let lift (f : state -> state list) : state list -> state list =
- fun l -> List.fold_left (fun acc x -> (f x) @ acc) [] l
+ let lift (f : state -> state) : transfer_function =
+ fun x -> [f x]
+
+ let lift' (f : state -> state or_bottom) : transfer_function =
+ fun x -> Bottom.to_list (f x)
+
+ let sequence (f1 : transfer_function) (f2 : transfer_function)
+ : transfer_function =
+ fun x -> List.fold_left (fun acc y -> f2 y @ acc) [] (f1 x)
- let lift' (f : state -> state or_bottom) : state list -> state list =
- fun l -> List.fold_left (fun acc x -> Bottom.add_to_list (f x) acc) [] l
(* Tries to evaluate \assigns … \from … clauses for assembly code. *)
- let transfer_asm (stmt : stmt) (states : state list) : state list =
+ let transfer_asm (stmt : stmt) : transfer_function =
let asm_contracts = Annotations.code_annot stmt in
match Logic_utils.extract_contract asm_contracts with
| [] ->
Value_util.warning_once_current
"assuming assembly code has no effects in function %t"
Value_util.pretty_current_cfunction_name;
- states
+ id
(* There should be only one statement contract, if any. *)
| (_, spec) :: _ ->
let assigns = Ast_info.merge_assigns_from_spec ~warn:false spec in
- List.map (Spec.treat_statement_assigns assigns) states
+ lift (Spec.treat_statement_assigns assigns)
let transfer_assume (stmt : stmt) (exp : exp) (kind : guard_kind)
- (states : state list) : state list =
+ : transfer_function =
let positive = (kind = Then) in
- lift' (fun s -> Transfer.assume s stmt exp positive) states
+ lift' (fun s -> Transfer.assume s stmt exp positive)
+
+ let transfer_assign (stmt : stmt) (dest : Cil_types.lval) (exp : exp)
+ : transfer_function =
+ lift' (fun s -> Transfer.assign s (Kstmt stmt) dest exp)
- let transfer_enter (block : block) (states : state list) : state list =
+ let transfer_enter (block : block) : transfer_function =
let vars = block_toplevel_locals block in
- if vars = [] then states else List.map (Transfer.enter_scope kf vars) states
+ if vars = [] then id else lift (Transfer.enter_scope kf vars)
- let transfer_leave (block : block) (states : state list) : state list =
+ let transfer_leave (block : block) : transfer_function =
let vars = block.blocals in
- if vars = [] then states else List.map (Domain.leave_scope kf vars) states
+ if vars = [] then id else lift (Domain.leave_scope kf vars)
let transfer_call (stmt : stmt) (dest : lval option) (callee : exp)
(args : exp list) (state : state) : state list =
@@ -276,8 +280,7 @@ module Make_Dataflow
cacheable := Value_types.NoCacheCallers;
Bottom.list_of_bot result
- let transfer_instr (stmt : stmt) (instr : instr) : state list -> state list =
- let id states = states in
+ let transfer_instr (stmt : stmt) (instr : instr) : transfer_function =
match instr with
| Local_init (vi, AssignInit exp, _loc) ->
let transfer state =
@@ -294,11 +297,11 @@ module Make_Dataflow
let state = Domain.enter_scope kf [vi] state in
transfer_call stmt dest callee args state
in
- lift (Cil.treat_constructor_as_func as_func vi f args k loc)
+ Cil.treat_constructor_as_func as_func vi f args k loc
| Set (dest, exp, _loc) ->
- lift' (fun s -> Transfer.assign s (Kstmt stmt) dest exp)
+ transfer_assign stmt dest exp
| Call (dest, callee, args, _loc) ->
- lift (transfer_call stmt dest callee args)
+ transfer_call stmt dest callee args
| Asm _ ->
transfer_asm stmt
| Skip _loc -> id
@@ -306,7 +309,7 @@ module Make_Dataflow
from the annotation table *)
let transfer_return (stmt : stmt) (return_exp : exp option)
- (states : state list) : state list =
+ : transfer_function =
(* Deconstruct return statement *)
let return_var = match return_exp with
| Some {enode = Lval (Var v, NoOffset)} -> Some v
@@ -314,62 +317,46 @@ module Make_Dataflow
| _ -> assert false (* Cil invariant *)
in
(* Check postconditions *)
- post_conditions := true;
- let states =
+ let check_postconditions = fun state ->
+ post_conditions := true;
if Value_util.skip_specifications kf then
- states
+ [state]
else match
Logic.check_fct_postconditions kf active_behaviors Normal
- ~pre_state:initial_state ~post_states:(States.of_list states)
+ ~pre_state:initial_state ~post_states:(States.singleton state)
~result:return_var
with
| `Bottom -> []
| `Value v -> States.to_list v
- in
- (* Split strategies *)
- let states = match Split_return.kf_strategy kf with
- | Split_strategy.SplitEqList i ->
- begin match return_exp with
- | Some return_exp ->
- let split_states = Transfer.split_final_states kf return_exp i states in
- let states' = List.map smash split_states in
- Bottom.all states'
- | None ->
- Bottom.to_list (smash states)
- end
- | Split_strategy.NoSplit -> Bottom.to_list (smash states)
- | Split_strategy.FullSplit -> states
- (* Last case not possible : already transformed into SplitEqList *)
- | Split_strategy.SplitAuto -> assert false
- in
(* Assign the return value *)
- match return_exp with
- | None ->
- states
- | Some return_exp ->
- let vi_ret = Extlib.the (Library_functions.get_retres_vi kf) in
- let return_lval = Var vi_ret, NoOffset in
- let transfer state =
- let state = Domain.enter_scope kf [vi_ret] state in
- Transfer.assign state (Kstmt stmt) return_lval return_exp
- in
- lift' transfer states
+ and assign_retval =
+ match return_exp with
+ | None -> id
+ | Some return_exp ->
+ let vi_ret = Extlib.the (Library_functions.get_retres_vi kf) in
+ let return_lval = Var vi_ret, NoOffset in
+ let kstmt = Kstmt stmt in
+ fun state ->
+ let state = Domain.enter_scope kf [vi_ret] state in
+ let state' = Transfer.assign state kstmt return_lval return_exp in
+ Bottom.to_list state'
+ in
+ sequence check_postconditions assign_retval
- let transfer_transition (t : vertex transition) (states : state list) : state list =
+ let transfer_transition (t : vertex transition) : transfer_function =
match t with
- | Skip -> states
- | Return (return_exp,stmt) -> transfer_return stmt return_exp states
- | Guard (exp,kind,stmt) -> transfer_assume stmt exp kind states
- | Instr (instr,stmt) -> transfer_instr stmt instr states
- | Enter (block) -> transfer_enter block states
+ | Skip -> id
+ | Return (return_exp,stmt) -> transfer_return stmt return_exp
+ | Guard (exp,kind,stmt) -> transfer_assume stmt exp kind
+ | Instr (instr,stmt) -> transfer_instr stmt instr
+ | Enter (block) -> transfer_enter block
| Leave (block) when blocks_share_locals fundec.sbody block ->
(* The variables from the toplevel block will be removed by the caller *)
- states
- | Leave (block) -> transfer_leave block states
- | Prop _ -> states (* Annotations are interpreted in [transfer_statement]. *)
+ id
+ | Leave (block) -> transfer_leave block
+ | Prop _ -> id (* Annotations are interpreted in [transfer_statement]. *)
- let transfer_statement_annot (stmt : stmt) ~(record : bool)
- (states : state list) : state list =
+ let transfer_annotations (stmt : stmt) ~(record : bool) : transfer_function =
let annots =
(* We do not interpret annotations that come from statement contracts
and everything previously emitted by Value (currently, alarms) *)
@@ -378,29 +365,19 @@ module Make_Dataflow
in
List.map fst (Annotations.code_annot_emitter ~filter stmt)
in
- let interp_annot states ca =
- Logic.interp_annot
- ~limit:(slevel stmt) ~record
- kf active_behaviors stmt ca
- ~initial_state states
- in
- States.to_list (List.fold_left interp_annot (States.of_list states) annots)
-
- let get_cvalue = Domain.get Cvalue_domain.key
- let gather_cvalues states =
- match get_cvalue with
- | Some get -> List.map get states
- | None -> []
+ fun state ->
+ let interp_annot states ca =
+ Logic.interp_annot
+ ~limit:(slevel stmt) ~record
+ kf active_behaviors stmt ca
+ ~initial_state states
+ in
+ States.to_list
+ (List.fold_left interp_annot (States.singleton state) annots)
- let transfer_statement (stmt : stmt) (states : state list) : state list =
- current_ki := Kstmt stmt;
- (* Apply callback *)
- (* TODO: apply on all domains. *)
- let cvalue_states = gather_cvalues states in
- Db.Value.Compute_Statement_Callbacks.apply
- (stmt, Value_util.call_stack (), cvalue_states);
+ let transfer_statement (stmt : stmt) (state : state) : state list =
(* Interpret annotations *)
- let states = transfer_statement_annot stmt ~record:true states in
+ let states = transfer_annotations stmt ~record:true state in
(* Check unspecified sequences *)
match stmt.skind with
| UnspecifiedSequence seq when Kernel.UnspecifiedAccess.get () ->
@@ -419,24 +396,31 @@ module Make_Dataflow
if x >= !max_displayed + slevel_display_step
then begin
let rounded = x / slevel_display_step * slevel_display_step in
- Value_parameters.feedback ~once:true
+ Value_parameters.feedback ~once:true ~current:true
"Semantic level unrolling superposing up to %d states"
rounded;
max_displayed := rounded;
end
- let process_loop_transitions (v1 : vertex) (v2 : vertex) (p : propagation)
- : unit =
+ let process_partitioning_transitions (v1 : vertex) (v2 : vertex)
+ (transition : vertex transition) (f : flow) : unit =
+ (* Split return *)
+ begin match transition with
+ | Return (return_exp, _) ->
+ Partition.split_return f return_exp
+ | _ -> ()
+ end;
+ (* Loop transitions *)
let the_stmt v = Extlib.the v.vertex_start_of in
let enter_loop v =
- Partition.transfer (List.map (Domain.enter_loop (the_stmt v))) p;
- Partition.enter_loop p (the_stmt v)
+ Partition.transfer (lift (Domain.enter_loop (the_stmt v))) f;
+ Partition.enter_loop f (the_stmt v)
and leave_loop v =
- Partition.transfer (List.map (Domain.leave_loop (the_stmt v))) p;
- Partition.leave_loop p (the_stmt v)
+ Partition.transfer (lift (Domain.leave_loop (the_stmt v))) f;
+ Partition.leave_loop f (the_stmt v)
and incr_loop_counter v =
- Partition.transfer (List.map (Domain.incr_loop_counter (the_stmt v))) p;
- Partition.next_loop_iteration p (the_stmt v)
+ Partition.transfer (lift (Domain.incr_loop_counter (the_stmt v))) f;
+ Partition.next_loop_iteration f (the_stmt v)
in
let loops_left, loops_entered =
Interpreted_automata.get_wto_index_diff kf v1 v2
@@ -448,97 +432,116 @@ module Make_Dataflow
if loop_incr then
incr_loop_counter v2
- let process_edge (v1,e,v2 : G.edge) : unit =
+ let process_edge (v1,e,v2 : G.edge) : flow =
let {edge_transition=transition; edge_kinstr=kinstr} = e in
- let propagation,edge_info = get_edge_propagation e in
+ let tank,edge_info = get_edge_data e in
+ let flow = Partition.drain tank in
!Db.progress ();
check_signals ();
current_ki := kinstr;
Cil.CurrentLoc.set e.edge_loc;
- Partition.transfer (transfer_transition transition) propagation;
- process_loop_transitions v1 v2 propagation;
- if not (Partition.is_empty_propagation propagation) then
- edge_info.fireable <- true
-
- let update_vertex ?(widening : bool = false) (v : vertex) : bool =
- (* Set location if possible *)
- Extlib.may
- (fun stmt -> Cil.CurrentLoc.set (Cil_datatype.Stmt.loc stmt))
- v.vertex_start_of;
+ Partition.transfer (transfer_transition transition) flow;
+ process_partitioning_transitions v1 v2 transition flow;
+ if not (Partition.is_empty_flow flow) then
+ edge_info.fireable <- true;
+ flow
+
+ let get_cvalue = Domain.get Cvalue_domain.key
+ let gather_cvalues states =
+ match get_cvalue with
+ | Some get -> List.map get states
+ | None -> []
+
+ let call_statement_callbacks (stmt : stmt) (f : flow) : unit =
+ (* TODO: apply on all domains. *)
+ let states = Partition.contents f in
+ let cvalue_states = gather_cvalues states in
+ Db.Value.Compute_Statement_Callbacks.apply
+ (stmt, Value_util.call_stack (), cvalue_states)
+
+ let update_vertex ?(widening : bool = false) (v : vertex)
+ (sources : ('branch * flow) list) : bool =
+ begin match v.vertex_start_of with
+ | Some stmt ->
+ (* Set location *)
+ current_ki := Kstmt stmt;
+ Cil.CurrentLoc.set (Cil_datatype.Stmt.loc stmt);
+ | None -> ()
+ end;
(* Get vertex store *)
let store = get_vertex_store v in
(* Join incoming s tates *)
- let sources = get_pred_propagations v in
- let sources =
- if v == automaton.entry_point
- then initial_propagation :: sources
- else sources
- in
- let p = Partition.join sources store in
+ let f = Partition.join sources store in
(* Output slevel related things *)
let store_size = Partition.store_size store in
+ output_slevel store_size;
begin match v.vertex_start_of with
| Some stmt ->
+ (* Callbacks *)
+ call_statement_callbacks stmt f;
+ (* Transfer function associated to the statement *)
+ Partition.transfer (transfer_statement stmt) f;
+ (* Debug informations *)
Value_parameters.debug ~dkey ~current:true
"reached statement %d with %d / %d eternal states, %d to propagate"
- stmt.sid store_size (slevel stmt) (Partition.propagation_size p)
+ stmt.sid store_size (slevel stmt) (Partition.flow_size f);
| _ -> ()
end;
- output_slevel store_size;
- (* Transfer function associated to the statement *)
- Extlib.may
- (fun stmt -> Partition.transfer (transfer_statement stmt) p)
- v.vertex_start_of;
(* Widen if necessary *)
let stable =
- if Partition.is_empty_propagation p then
+ if Partition.is_empty_flow f then
true
else if widening then begin
- let stable = Partition.widen store (get_vertex_widening v) p in
+ let stable = Partition.widen (get_vertex_widening v) f in
(* Try to correct over-widenings *)
let correct_over_widening stmt =
(* Do *not* record the status after interpreting the annotation
here. Possible unproven assertions have already been recorded
when the assertion has been interpreted the first time higher
in this function. *)
- Partition.transfer (transfer_statement_annot stmt ~record:false) p
+ Partition.transfer (transfer_annotations stmt ~record:false) f
in
Extlib.may correct_over_widening v.vertex_start_of;
stable
end else
false
in
- (* Reset sources *)
- List.iter (fun (_,p) -> Partition.clear_propagation p) sources;
(* Dispatch to successors *)
- List.iter (fun p2 -> Partition.merge p ~into:p2) (get_succ_propagations v);
+ List.iter (fun into -> Partition.fill f ~into) (get_succ_tanks v);
(* Return wether the iterator should stop or not *)
stable
let process_vertex ?(widening : bool = false) (v : vertex) : bool =
(* Process predecessors *)
- G.iter_pred_e process_edge graph v;
+ let process_source (_,e,_ as edge) =
+ e.edge_key, process_edge edge
+ in
+ let sources = List.map process_source (G.pred_e graph v) in
+ (* Add initial source *)
+ let sources =
+ if v <> automaton.entry_point
+ then sources
+ else get_initial_flow () :: sources
+ in
(* Update the vertex *)
- update_vertex ~widening v
+ update_vertex ~widening v sources
- let rec simulate (v : vertex) : unit =
+ let rec simulate (v : vertex) (source : 'branch * flow) : unit =
(* Update the current vertex *)
- ignore (update_vertex v);
+ ignore (update_vertex v [source]);
(* Try every possible successor *)
- G.iter_succ_e process_edge graph v;
- (* Find which edges were fireable *)
- let add_if_fireable (_,e,succ) acc =
- let p = fst (get_edge_propagation e) in
- if Partition.is_empty_propagation p
- then (Partition.clear_propagation p; acc)
- else succ :: acc
+ let add_if_fireable (_,e,succ as edge) acc =
+ let f = process_edge edge in
+ if Partition.is_empty_flow f
+ then acc
+ else (e.edge_key,f,succ) :: acc
in
let successors = G.fold_succ_e add_if_fireable graph v [] in
(* How many possible successors ? *)
match successors with
| [] -> () (* No successor - end of simulation *)
- | [succ] -> (* One successor - continue simulation *)
- simulate succ
+ | [b,f,succ] -> (* One successor - continue simulation *)
+ simulate succ (b,f)
| _ -> (* Several successors - failure *)
Value_parameters.abort "Do not know which branch to take. Stopping."
@@ -583,8 +586,8 @@ module Make_Dataflow
relevant.*)
let mark_degeneration () =
let f stmt (v,_) =
- let l = get_succ_propagations v in
- if not (List.for_all Partition.is_empty_propagation l) then
+ let l = get_succ_tanks v in
+ if not (List.for_all Partition.is_empty_tank l) then
Value_util.DegenerationPoints.replace stmt false
in
StmtTable.iter f automaton.stmt_table;
@@ -602,7 +605,7 @@ module Make_Dataflow
let compute () : state list or_bottom =
if interpreter_mode then
- simulate automaton.entry_point
+ simulate automaton.entry_point (get_initial_flow ())
else begin
let wto = Interpreted_automata.get_wto kf in
iterate_list wto
@@ -623,7 +626,7 @@ module Make_Dataflow
| Then -> Db.Value.mask_then
| Else -> Db.Value.mask_else
in
- let edge_info = snd (get_edge_propagation e) in
+ let edge_info = snd (get_edge_data e) in
let old_status =
try StmtTable.find table stmt
with Not_found -> 0
diff --git a/src/plugins/value/engine/state_partitioning.mli b/src/plugins/value/engine/state_partitioning.mli
index 223d3db8d60..5f2508badf7 100644
--- a/src/plugins/value/engine/state_partitioning.mli
+++ b/src/plugins/value/engine/state_partitioning.mli
@@ -45,36 +45,40 @@ end
module type Partition =
sig
type state (** The states being partitioned *)
- type store (** The storage of a partition *)
- type propagation (** Only contains states which needs to be propagated, i.e.
- states which have not been propagated yet *)
+ type store (** The storage of all states ever met at a control point *)
+ type flow (** A set of states which are currently propagated *)
+ type tank (** An organized temporary accumulation of flows *)
type widening (** Widening informations *)
(* --- Constructors --- *)
val empty_store : stmt:Cil_types.stmt option -> store
- val empty_propagation : unit -> propagation
+ val empty_flow : unit -> flow
+ val empty_tank : unit -> tank
val empty_widening : stmt:Cil_types.stmt option -> widening
- (** Build the initial propagation for the entry point of a function. *)
- val initial_propagation : state list -> propagation
+ (** Build the initial tank for the entry point of a function. *)
+ val initial_tank : state list -> tank
(* --- Pretty printing --- *)
val pretty_store : Format.formatter -> store -> unit
- val pretty_propagation : Format.formatter -> propagation -> unit
+ val pretty_flow : Format.formatter -> flow -> unit
(* --- Accessors --- *)
val expanded : store -> state list
val smashed : store -> state or_bottom
+ val contents : flow -> state list
val is_empty_store : store -> bool
- val is_empty_propagation : propagation -> bool
+ val is_empty_flow : flow -> bool
+ val is_empty_tank : tank -> bool
val store_size : store -> int
- val propagation_size : propagation -> int
+ val flow_size : flow -> int
+ val tank_size : tank -> int
(* --- Reset state (for hierchical convergence) --- *)
@@ -83,7 +87,8 @@ sig
been obtained after a widening. *)
val reset_store : store -> unit
- val reset_propagation : propagation -> unit
+ val reset_flow : flow -> unit
+ val reset_tank : tank -> unit
val reset_widening : widening -> unit
(** Resets (or just delays) the widening counter. Used on nested loops, to
@@ -95,25 +100,24 @@ sig
(* --- Partition transfer functions --- *)
- val enter_loop : propagation -> loop -> unit
- val leave_loop : propagation -> loop -> unit
- val next_loop_iteration : propagation -> loop -> unit
+ val enter_loop : flow -> loop -> unit
+ val leave_loop : flow -> loop -> unit
+ val next_loop_iteration : flow -> loop -> unit
+ val split_return : flow -> Cil_types.exp option -> unit
(* --- Operators --- *)
- (** Remove all states from the propagation, leaving it empty as if it was just
- created by [empty_propagation] *)
- val clear_propagation : propagation -> unit
+ (** Remove all states from the tank, leaving it empty as if it was just
+ created by [empty_tank] *)
+ val drain : tank -> flow
- (** Apply a transfer function to all the states of a propagation. *)
- val transfer : (state list -> state list) -> propagation -> unit
+ (** Fill the states of the flow into the tank, modifying [into] inplace but
+ letting the flow unchanged *)
+ val fill: into:tank -> flow -> unit
- (** Merge two propagations together, modifying [into] inplace. At the return
- of the function, [into] should contain all the states of both original
- propagations, or an overapproximation of this union: joining two states
- together inside the propagation is allowed. *)
- val merge : into:propagation -> propagation -> unit
+ (** Apply a transfer function to all the states of a propagation. *)
+ val transfer : (state -> state list) -> flow -> unit
(** Join all incoming propagations into the given store. This function returns
a set of states which still need to be propagated past the store.
@@ -127,17 +131,13 @@ sig
This function also interprets partitioning annotations at the store
vertex (slevel, splits, merges, ...) which will generally change the
current partitioning. *)
- val join : (branch * propagation) list -> store -> propagation
-
- (** Widen a propagation at the position of the given store. The widening
- object keeps track of the previous widenings to ensure termination. The
- result is true when it is correct to end the propagation here, i.e. when
- the current propagation is only carrying states which are included into
- already propagated states.
+ val join : (branch * flow) list -> store -> flow
- Note that the propagation given to [widen] *must* have been produced by
- the [join] on the same store. *)
- val widen : store -> widening -> propagation -> bool
+ (** Widen a tank. The widening object keeps track of the previous widenings to
+ ensure termination. The result is true when it is correct to end the
+ propagation here, i.e. when the current tank is only containng
+ states which are included into already propagated states. *)
+ val widen : widening -> flow -> bool
end
diff --git a/src/plugins/value/engine/trace_partitioning.ml b/src/plugins/value/engine/trace_partitioning.ml
index 1e4e6e679ee..810f61e1a7a 100644
--- a/src/plugins/value/engine/trace_partitioning.ml
+++ b/src/plugins/value/engine/trace_partitioning.ml
@@ -44,10 +44,14 @@ struct
let eval_exp_to_int = Transfer.eval_exp_to_int
include Domain
+
+ let smash = function
+ | [] -> []
+ | v1 :: l -> [ List.fold_left join v1 l ]
end
module Index = Partitioning.Make (Domain)
- module Partition = Partition.Make (Domain)
+ module Flow = Partition.MakeFlow (Domain)
type state = Domain.t
@@ -61,8 +65,12 @@ struct
mutable store_size : int;
}
- type propagation = {
- mutable partition : state partition;
+ type flow = {
+ mutable flow_states : Flow.t;
+ }
+
+ type tank = {
+ mutable tank_states : state partition;
}
type widening_state = {
@@ -91,8 +99,11 @@ struct
store_size = 0;
}
- let empty_propagation () : propagation =
- { partition = Partition.empty }
+ let empty_flow () : flow =
+ { flow_states = Flow.empty }
+
+ let empty_tank () : tank =
+ { tank_states = Partition.empty }
let empty_widening ~(stmt : stmt option) : widening =
{
@@ -100,14 +111,14 @@ struct
widening_partition = Partition.empty;
}
- let initial_propagation (states : state list) : propagation =
- let partition = Partition.initial states in
+ let initial_tank (states : state list) : tank =
+ let propagation = Flow.initial states in
(* Split the initial partition according to the global split seetings *)
- let split partition lval =
- Partition.transfer_keys partition (Dynamic_split lval)
+ let split propagation lval =
+ Flow.transfer_keys propagation (Dynamic_split lval)
in
- let partition = List.fold_left split partition universal_splits in
- { partition }
+ let states = List.fold_left split propagation universal_splits in
+ { tank_states = Flow.to_partition states }
(* Pretty printing *)
@@ -115,8 +126,8 @@ struct
let pretty_store (fmt : Format.formatter) (s : store) : unit =
Partition.iter (Domain.pretty fmt) s.store_partition
- let pretty_propagation (fmt : Format.formatter) (p : propagation) =
- Partition.iter (Domain.pretty fmt) p.partition
+ let pretty_flow (fmt : Format.formatter) (p : flow) =
+ Flow.iter (Domain.pretty fmt) p.flow_states
(* Accessors *)
@@ -125,33 +136,62 @@ struct
Partition.to_list s.store_partition
let smashed (s : store) : state or_bottom =
- match expanded s with
- | [] -> `Bottom
- | v1 :: l -> `Value (List.fold_left Domain.join v1 l)
+ Bottom.of_list (Domain.smash (expanded s))
+
+ let contents (f : flow) : state list =
+ Flow.to_list f.flow_states
let is_empty_store (s : store) : bool =
Partition.is_empty s.store_partition
- let is_empty_propagation (p : propagation) : bool =
- Partition.is_empty p.partition
+ let is_empty_flow (f : flow) : bool =
+ Flow.is_empty f.flow_states
+
+ let is_empty_tank (t : tank) : bool =
+ Partition.is_empty t.tank_states
let store_size (s : store) : int =
s.store_size
- let propagation_size (p : propagation) : int =
- Partition.size p.partition
+ let flow_size (f : flow) : int =
+ Flow.size f.flow_states
+ let tank_size (t : tank) : int =
+ Partition.size t.tank_states
(* Partition transfer functions *)
- let enter_loop (p : propagation) (i : loop) =
- p.partition <- Partition.transfer_keys p.partition (Enter_loop (unroll i))
-
- let leave_loop (p : propagation) (_i : loop) =
- p.partition <- Partition.transfer_keys p.partition Leave_loop
-
- let next_loop_iteration (p : propagation) (_i : loop) =
- p.partition <- Partition.transfer_keys p.partition Incr_loop
+ let loop_transfer p action =
+ p.flow_states <- Flow.transfer_keys p.flow_states action
+
+ let enter_loop (p : flow) (i : loop) : unit =
+ loop_transfer p (Enter_loop (unroll i))
+
+ let leave_loop (p : flow) (_i : loop) : unit =
+ loop_transfer p Leave_loop
+
+ let next_loop_iteration (p : flow) (_i : loop) : unit =
+ loop_transfer p Incr_loop
+
+ let split_return (flow : flow) (return_exp : exp option) : unit =
+ (** Join every state in the list *)
+ let transfer_split states =
+ match Split_return.kf_strategy kf with
+ | Split_strategy.SplitEqList i ->
+ begin match return_exp with
+ | Some return_exp ->
+ let states = Transfer.split_final_states kf return_exp i states in
+ List.flatten (List.map Domain.smash states)
+ | None ->
+ Domain.smash states
+ end
+ | Split_strategy.NoSplit -> Domain.smash states
+ | Split_strategy.FullSplit -> states
+ (* Last case not possible : already transformed into SplitEqList *)
+ | Split_strategy.SplitAuto -> assert false
+ in
+ flow.flow_states <-
+ Flow.legacy_transfer_states transfer_split flow.flow_states
(* Reset state (for hierchical convergence) *)
@@ -162,8 +202,11 @@ struct
in
s.store_partition <- Partition.filter_keys is_eternal s.store_partition
- let reset_propagation (p : propagation) : unit =
- p.partition <- Partition.empty
+ let reset_flow (f : flow) : unit =
+ f.flow_states <- Flow.empty
+
+ let reset_tank (t : tank) : unit =
+ t.tank_states <- Partition.empty
let reset_widening (w : widening) : unit =
w.widening_partition <- Partition.empty
@@ -177,73 +220,68 @@ struct
(* Operators *)
- let clear_propagation (p : propagation) : unit =
- p.partition <- Partition.empty
-
- let transfer (f : state list -> state list) (p : propagation) : unit =
- p.partition <- Partition.transfer_states (fun s -> f [s]) p.partition
+ let drain (t : tank) : flow =
+ let flow_states = Flow.of_partition t.tank_states in
+ t.tank_states <- Partition.empty;
+ { flow_states }
- let merge ~(into : propagation) (source : propagation) : unit =
- (* TODO: state the precondition for this to be correct *)
- let merge_two dest src = (* Erase the destination *)
+ let fill ~(into : tank) (f : flow) : unit =
+ let erase dest src =
if Extlib.has_some src
then src
else dest
in
- into.partition <- Partition.merge merge_two into.partition source.partition
+ let new_states = Flow.to_partition f.flow_states in
+ into.tank_states <- Partition.merge erase into.tank_states new_states
- let join (sources : (branch*propagation) list) (dest : store)
- : propagation =
+ let transfer (f : state -> state list) (p : flow) : unit =
+ p.flow_states <- Flow.transfer_states f p.flow_states
+
+ let join (sources : (branch*flow) list) (dest : store) : flow =
let is_loop_head =
match dest.store_stmt with
| Some {skind=Cil_types.Loop _} -> true
| _ -> false
in
- let current_ration = ref dest.store_size in
- (* Update states counters *)
- let count acc (_b,p) =
- acc + Partition.size p.partition
- in
- dest.store_size <- List.fold_left count dest.store_size sources;
- (* Get every source propagation *)
- let source_partitions =
+ (* Get every source flow *)
+ let sources_states =
match sources with
- | [(_,p)] -> [p.partition]
+ | [(_,p)] -> [p.flow_states]
| sources ->
(* Several branches ; partition according to the incoming branch *)
let get (b,p) =
- Partition.transfer_keys p.partition (Branch (b,history_size))
+ Flow.transfer_keys p.flow_states (Branch (b,history_size))
in
List.map get sources
in
+ (* Merge incomming flows *)
+ let flow_states =
+ List.fold_left Flow.union Flow.empty sources_states
+ in
(* Handle ration stamps *)
+ let previous_store_size = dest.store_size in
+ dest.store_size <- dest.store_size + Flow.size flow_states;
let slevel_exceeded = dest.store_size > dest.size_limit in
- let rationing =
+ let rationing_action =
if slevel_exceeded then
(* No more slevel, no more ration tickets *)
- fun p -> Partition.transfer_keys p (Ration_merge None)
+ Ration_merge None
else if dest.merge then
(* Merge / Merge after loop : a unique ration stamp for all *)
- fun p -> Partition.transfer_keys p (Ration_merge (Some !current_ration))
- else begin fun p ->
+ Ration_merge (Some (previous_store_size, 0))
+ else
(* Attribute a ration stamp to each individual state *)
- let p = Partition.transfer_keys p (Ration !current_ration) in
- current_ration := !current_ration + Partition.size p;
- p
- end
+ Ration previous_store_size
in
- let source_partitions = List.map rationing source_partitions in
(* Handle Split / Merge operations *)
- let do_flow_actions partition =
- let actions =
- dest.flow_actions @ [Update_dynamic_splits ; Transfer_merge]
- in
- List.fold_left Partition.transfer_keys partition actions
+ let flow_actions = Update_dynamic_splits :: dest.flow_actions in
+ (* Execute actions *)
+ let actions = rationing_action :: flow_actions in
+ let flow_states =
+ List.fold_left Flow.transfer_keys flow_states actions
in
- let source_partitions = List.map do_flow_actions source_partitions in
- (* Merge incomming propagations *)
- let union = Partition.union Domain.join in
- let partition = List.fold_left union Partition.empty source_partitions in
+ (* Join states with unique keys *)
+ let partition = Flow.to_partition flow_states in
(* Add states to the store but filter out already propagated states *)
let update key current_state =
(* Inclusion test *)
@@ -272,11 +310,11 @@ struct
(* Filter out already propagated states *)
Extlib.opt_filter (fun s -> Index.add s dest.store_index) state
in
- let partition = Partition.map_filter update partition in
- { partition }
+ let partition' = Partition.map_filter update partition in
+ { flow_states = Flow.of_partition partition' }
- let widen (_s : store) (w : widening) (p : propagation) : bool =
+ let widen (w : widening) (f : flow) : bool =
let stmt = w.widening_stmt in
(* Auxiliary function to update the result *)
let update key widening_state =
@@ -331,6 +369,8 @@ struct
};
Some curr
in
- p.partition <- Partition.map_filter widen_one p.partition;
- Partition.is_empty p.partition
+ let p = Flow.to_partition f.flow_states in
+ let p' = Partition.map_filter widen_one p in
+ f.flow_states <- Flow.of_partition p';
+ Flow.is_empty f.flow_states
end
--
GitLab