Skip to content
Snippets Groups Projects
Commit e229038d authored by Valentin Perrelle's avatar Valentin Perrelle Committed by David Bühler
Browse files

[Eva] Add / fix comments and small simplifications

parent 3d252889
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/value/engine/partition.ml
+ 61
− 73
View file @ e229038d
......@@ -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 ->
......
src/plugins/value/engine/partition.mli
+ 38
− 35
View file @ e229038d
......@@ -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
......
src/plugins/value/engine/partitioning_parameters.ml
+ 22
− 22
View file @ e229038d
......@@ -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 ()
......
src/plugins/value/engine/state_partitioning.mli
+ 7
− 14
View file @ e229038d
......@@ -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
......
src/plugins/value/engine/trace_partitioning.ml
+ 9
− 8
View file @ e229038d
......@@ -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 {
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment