diff --git a/src/plugins/value/engine/partition.ml b/src/plugins/value/engine/partition.ml
index 77a8ef9fdcd2b501b4d96d357aae05b5680cfc13..8b71d9866ca5002aec4077a1e6a8a9d13d97fa8a 100644
--- a/src/plugins/value/engine/partition.ml
+++ b/src/plugins/value/engine/partition.ml
@@ -20,6 +20,8 @@
(* *)
(**************************************************************************)
+(* --- Keys --- *)
+
module ExpMap = Cil_datatype.ExpStructEq.Map
module IntPair = Datatype.Pair (Datatype.Int) (Datatype.Int)
module LoopList = Datatype.List (IntPair)
@@ -35,39 +37,19 @@ type key = {
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
+ (* Initial key, before any partitioning *)
+ let zero = {
+ ration_stamp = None;
+ branches = [];
+ loops = [];
+ static_split = ExpMap.empty;
+ dynamic_split = ExpMap.empty;
+ }
+
let compare k1 k2 =
let (<?>) c (cmp,x,y) =
if c = 0 then cmp x y else c
@@ -77,12 +59,57 @@ struct
<?> (ExpMap.compare Integer.compare, k1.static_split, k2.static_split)
<?> (ExpMap.compare Integer.compare, k1.dynamic_split, k2.dynamic_split)
<?> (BranchList.compare, k1.branches, k2.branches)
+
+ let pretty 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)
end
-module KMap = Map.Make (Key)
+(* --- Partitions --- *)
+
+module KMap = Map.Make (Key)
type 'a partition = 'a KMap.t
+
+let empty = KMap.empty
+let find = KMap.find
+let replace = KMap.add
+let is_empty = KMap.is_empty
+let size = KMap.cardinal
+let iter = KMap.iter
+let map = KMap.map
+let filter = KMap.filter
+let merge = KMap.merge
+
+let to_list (p : 'a partition) : 'a list =
+ KMap.fold (fun _k x l -> x :: l) p []
+
+let map_filter (f : key -> 'a -> 'b option) (p : 'a partition) : 'b partition =
+ let opt_flatten (type a) (o : a option option) : a option =
+ Extlib.opt_conv None o
+ in
+ KMap.merge (fun k o _ -> opt_flatten (Extlib.opt_map (f k) o)) p KMap.empty
+
+
+(* --- Partitioning actions --- *)
+
type 'a transfer_function = (key * 'a) list -> (key * 'a) list
type unroll_limit =
@@ -105,6 +132,8 @@ type action =
exception InvalidAction
+(* --- Flows --- *)
+
module type InputDomain =
sig
type t
@@ -116,47 +145,6 @@ sig
val eval_exp_to_int : t -> Cil_types.exp -> int
end
-
-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 state = Domain.t
@@ -165,7 +153,7 @@ struct
let empty = []
let initial (p : 'a list) : t =
- List.map (fun state -> zero_key, state) p
+ List.map (fun state -> Key.zero, state) p
let to_list (f : t) : state list =
List.map snd f
@@ -314,7 +302,7 @@ struct
let transfer acc (k,x) =
let add =
match k.ration_stamp with
- (* No ration stam, just add the state to the list *)
+ (* No ration stamp, 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 ->
diff --git a/src/plugins/value/engine/partition.mli b/src/plugins/value/engine/partition.mli
index c817ca1868570625a848429fbdcec843cf0b42b2..69e115d0335c7da30a25a2f1f577fdcf3fa9b794 100644
--- a/src/plugins/value/engine/partition.mli
+++ b/src/plugins/value/engine/partition.mli
@@ -30,24 +30,29 @@
The key have several fields, one for each kind of partitioning.
- Ration stamps: These modelize the legacy slevel. Each state is given
- a ration stamp (represented by an integer) until there is no slevel left.
+ a ration stamp (represented by two integers) until there is no slevel
+ left. The first number is attributed by the store it comes from, the
+ second one is attributed by the last transfer.
It is an option type, when there is no more ration stamp, this field is
set to None; each new state will not be distinguished by this field.
- - Branches: This field enumerate the last branches taken to reach this
- state. The partitioning may chose how the branches are identified, but it
+ - Branches: This field enumerate the last junctions points passed through.
+ The partitioning may chose how the branches are identified, but it
is a First-In-First-Out set.
- Loops: This field stores the loop iterations needed to reach this state
for each loop we are currently in. It is stored in reverse order
- (innermost loop first)
- - Static/Dynamic splits:
-
- Note on implementation. These partitions are implemented as map from keys
- to states. We chose to have the same partition for stores, propagation and
- widenings so the combination of propagation + store or propagation +
- widening can be done as a map2 operation. However, this involve some tricks
- to make keys be always distinguished in propagation, like giving them new
- ration stamps. It may have been more natural to consider that propagations
- are lists, allowing states to have the same key.
+ (innermost loop first) It also stores the maximum number of unrolling ;
+ this number varies from a state to another, as it is computed from
+ an expression evaluated when we enter the loop.
+ - Static/Dynamic splits: track the splits applied to the state as a map
+ from the expression of the split to the value of this expression. Since
+ the split creates states in which the expression evalutates to a
+ singleton, the values of the map are integers.
+ Static splits are only evaluated when the annotation is encountered
+ whereas dynamic splits are reevaluated regularly.
+
+ A flow is a list of states accompanied by their key. It is used to
+ transfer states from one partition to another. It doesn't enforce unicity
+ of keys.
*)
type branch = int
@@ -55,17 +60,32 @@ type branch = int
module ExpMap = Cil_datatype.ExpStructEq.Map
type key = private {
- ration_stamp : (int * int) option;
+ ration_stamp : (int * int) option; (* store stamp / transfer stamp *)
branches : branch list;
- loops : (int * int) list;
+ loops : (int * int) list; (* current iteration / max unrolling *)
static_split : Integer.t ExpMap.t;
dynamic_split : Integer.t ExpMap.t;
}
-val pretty_key : Format.formatter -> key -> unit
+type 'a partition
+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 : (key -> 'a option -> 'b option -> 'c option) -> 'a partition ->
+ 'b partition -> 'c partition
+val iter : (key -> 'a -> unit) -> 'a partition -> unit
+val filter : (key -> 'a -> bool) -> 'a partition -> 'a partition
+val map : ('a -> 'a) -> 'a partition -> 'a partition
+val map_filter : (key -> 'a -> 'b option) -> 'a partition -> 'b partition
+
+
+
+(* Partitioning actions *)
-type 'a partition
type 'a transfer_function = (key * 'a) list -> (key * 'a) list
type unroll_limit =
@@ -88,24 +108,7 @@ 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
-
+(* Flows *)
module type InputDomain =
sig
diff --git a/src/plugins/value/engine/partitioning_parameters.ml b/src/plugins/value/engine/partitioning_parameters.ml
index 99c16a11e92966ec125457f1f0579eed66e5ba22..9111ade0ea39468a6aa486619878d0699e3ad6fb 100644
--- a/src/plugins/value/engine/partitioning_parameters.ml
+++ b/src/plugins/value/engine/partitioning_parameters.ml
@@ -78,28 +78,28 @@ struct
let unroll stmt =
let default = Partition.IntLimit min_loop_unroll in
- try match get_unroll_annot stmt with
- | [] -> warn_no_loop_unroll stmt; default
- | [None] -> Partition.IntLimit default_loop_unroll
- | [(Some t)] -> begin
- (* Inlines the value of const variables in [t]. *)
- let global_init vi =
- try (Globals.Vars.find vi).init with Not_found -> None
- in
- let t =
- Cil.visitCilTerm (new Logic_utils.simplify_const_lval global_init) t
- in
- match Logic_utils.constFoldTermToInt t with
- | Some n -> Partition.IntLimit (Integer.to_int n)
- | None -> Partition.ExpLimit (term_to_exp t)
- end
- | _ ->
- warn "ignoring invalid unroll annotation";
- raise Exit
- with
- | Exit -> default
- | Db.Properties.Interp.No_conversion ->
- warn "loop unrolling parameters must be valid expressions";
+ match get_unroll_annot stmt with
+ | [] -> warn_no_loop_unroll stmt; default
+ | [None] -> Partition.IntLimit default_loop_unroll
+ | [(Some t)] -> begin
+ (* Inlines the value of const variables in [t]. *)
+ let global_init vi =
+ try (Globals.Vars.find vi).init with Not_found -> None
+ in
+ let t =
+ Cil.visitCilTerm (new Logic_utils.simplify_const_lval global_init) t
+ in
+ match Logic_utils.constFoldTermToInt t with
+ | Some n -> Partition.IntLimit (Integer.to_int n)
+ | None ->
+ try
+ Partition.ExpLimit (term_to_exp t)
+ with Db.Properties.Interp.No_conversion ->
+ warn "loop unrolling parameters must be valid expressions";
+ default
+ end
+ | _ ->
+ warn "ignoring invalid unroll annotation";
default
let history_size = HistoryPartitioning.get ()
diff --git a/src/plugins/value/engine/state_partitioning.mli b/src/plugins/value/engine/state_partitioning.mli
index 5f2508badf79566ea94f552e423ef7026701373d..8e330f01be9dcfc81ab515b3d77b52ce40be18b0 100644
--- a/src/plugins/value/engine/state_partitioning.mli
+++ b/src/plugins/value/engine/state_partitioning.mli
@@ -22,8 +22,8 @@
open Bottom.Type
-type branch = Partition.branch
-type loop = Cil_types.stmt
+type branch = Partition.branch (* Junction branch id in the control flow *)
+type loop = Cil_types.stmt (* Loop head id *)
module type Kf =
sig
@@ -50,7 +50,6 @@ sig
type tank (** An organized temporary accumulation of flows *)
type widening (** Widening informations *)
-
(* --- Constructors --- *)
val empty_store : stmt:Cil_types.stmt option -> store
@@ -61,13 +60,11 @@ sig
(** 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_flow : Format.formatter -> flow -> unit
-
(* --- Accessors --- *)
val expanded : store -> state list
@@ -80,12 +77,10 @@ sig
val flow_size : flow -> int
val tank_size : tank -> int
-
(* --- Reset state (for hierchical convergence) --- *)
(* These functions reset the part of the state of the analysis which has
been obtained after a widening. *)
-
val reset_store : store -> unit
val reset_flow : flow -> unit
val reset_tank : tank -> unit
@@ -97,7 +92,6 @@ sig
depend on the outer loop. *)
val reset_widening_counter : widening -> unit
-
(* --- Partition transfer functions --- *)
val enter_loop : flow -> loop -> unit
@@ -105,7 +99,6 @@ sig
val next_loop_iteration : flow -> loop -> unit
val split_return : flow -> Cil_types.exp option -> unit
-
(* --- Operators --- *)
(** Remove all states from the tank, leaving it empty as if it was just
@@ -133,12 +126,12 @@ sig
current partitioning. *)
val join : (branch * flow) list -> store -> flow
- (** 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. *)
+ (** Widen a flow. The widening object keeps track of the previous widenings
+ and previous propagated states to ensure termination. The result is true
+ when it is correct to end the propagation here, i.e. when the flow
+ object is only containng states which are included into already propagated
+ states. *)
val widen : widening -> flow -> bool
-
end
module type Domain = Partitioning.Domain
diff --git a/src/plugins/value/engine/trace_partitioning.ml b/src/plugins/value/engine/trace_partitioning.ml
index 810f61e1a7af6a44b021ca108a66e4ef440a6447..a32d411f363e59d22a26c27536ac344b84a041d4 100644
--- a/src/plugins/value/engine/trace_partitioning.ml
+++ b/src/plugins/value/engine/trace_partitioning.ml
@@ -124,7 +124,7 @@ struct
(* Pretty printing *)
let pretty_store (fmt : Format.formatter) (s : store) : unit =
- Partition.iter (Domain.pretty fmt) s.store_partition
+ Partition.iter (fun _key state -> Domain.pretty fmt state) s.store_partition
let pretty_flow (fmt : Format.formatter) (p : flow) =
Flow.iter (Domain.pretty fmt) p.flow_states
@@ -159,6 +159,7 @@ struct
let tank_size (t : tank) : int =
Partition.size t.tank_states
+
(* Partition transfer functions *)
let loop_transfer p action =
@@ -197,10 +198,10 @@ struct
(* Reset state (for hierchical convergence) *)
let reset_store (s : store) : unit =
- let is_eternal key =
+ let is_eternal key _state =
key.ration_stamp <> None
in
- s.store_partition <- Partition.filter_keys is_eternal s.store_partition
+ s.store_partition <- Partition.filter is_eternal s.store_partition
let reset_flow (f : flow) : unit =
f.flow_states <- Flow.empty
@@ -215,7 +216,7 @@ struct
let reset w =
{ w with widening_counter = max w.widening_counter (widening_period - 1) }
in
- w.widening_partition <- Partition.map_states reset w.widening_partition
+ w.widening_partition <- Partition.map reset w.widening_partition
(* Operators *)
@@ -226,7 +227,7 @@ struct
{ flow_states }
let fill ~(into : tank) (f : flow) : unit =
- let erase dest src =
+ let erase _key dest src =
if Extlib.has_some src
then src
else dest
@@ -248,7 +249,7 @@ struct
match sources with
| [(_,p)] -> [p.flow_states]
| sources ->
- (* Several branches ; partition according to the incoming branch *)
+ (* Several branches -> partition according to the incoming branch *)
let get (b,p) =
Flow.transfer_keys p.flow_states (Branch (b,history_size))
in
@@ -332,7 +333,7 @@ struct
previous_state = curr;
widening_counter = wstate.widening_counter - 1
};
- (* Propagated state decreases, stop to propagate *)
+ (* Propagated state decreases, stop propagating *)
if Domain.is_included curr wstate.previous_state then
None
(* Widening is delayed *)
@@ -359,7 +360,7 @@ struct
Some next
end
with Not_found ->
- (* The key is not in the widening state; add it if slevel is not
+ (* The key is not in the widening state; add the state if slevel is
exceeded *)
if key.ration_stamp = None then
update key {