|
|
|
|
@ -651,7 +651,7 @@ type dexp =
|
|
|
|
|
| Dretcall of dexp * dexp list * location * call_flags
|
|
|
|
|
|
|
|
|
|
(** Value paths: identify an occurrence of a value in a symbolic heap
|
|
|
|
|
each expression represents a path, with Dpvar being the simplest one *)
|
|
|
|
|
each expression represents a path, with Dpvar being the simplest one *)
|
|
|
|
|
and vpath =
|
|
|
|
|
dexp option
|
|
|
|
|
|
|
|
|
|
@ -810,11 +810,11 @@ type strexp =
|
|
|
|
|
| Estruct of (Ident.fieldname * strexp) list * inst (** C structure *)
|
|
|
|
|
| Earray of exp * (exp * strexp) list * inst (** Array of given size. *)
|
|
|
|
|
(** There are two conditions imposed / used in the array case.
|
|
|
|
|
First, if some index and value pair appears inside an array
|
|
|
|
|
in a strexp, then the index is less than the size of the array.
|
|
|
|
|
For instance, x |->[10 | e1: v1] implies that e1 <= 9.
|
|
|
|
|
Second, if two indices appear in an array, they should be different.
|
|
|
|
|
For instance, x |->[10 | e1: v1, e2: v2] implies that e1 != e2. *)
|
|
|
|
|
First, if some index and value pair appears inside an array
|
|
|
|
|
in a strexp, then the index is less than the size of the array.
|
|
|
|
|
For instance, x |->[10 | e1: v1] implies that e1 <= 9.
|
|
|
|
|
Second, if two indices appear in an array, they should be different.
|
|
|
|
|
For instance, x |->[10 | e1: v1, e2: v2] implies that e1 != e2. *)
|
|
|
|
|
|
|
|
|
|
(** an atomic heap predicate *)
|
|
|
|
|
and hpred =
|
|
|
|
|
@ -827,14 +827,14 @@ and hpred =
|
|
|
|
|
This assumption is used in the rearrangement. The last [exp list] parameter
|
|
|
|
|
is used to denote the shared links by all the nodes in the list. *)
|
|
|
|
|
| Hdllseg of lseg_kind * hpara_dll * exp * exp * exp * exp * exp list
|
|
|
|
|
(** higher-order predicate for doubly-linked lists. *)
|
|
|
|
|
(** higher-order predicate for doubly-linked lists. *)
|
|
|
|
|
|
|
|
|
|
(** parameter for the higher-order singly-linked list predicate.
|
|
|
|
|
Means "lambda (root,next,svars). Exists evars. body".
|
|
|
|
|
Assume that root, next, svars, evars are disjoint sets of
|
|
|
|
|
primed identifiers, and include all the free primed identifiers in body.
|
|
|
|
|
body should not contain any non - primed identifiers or program
|
|
|
|
|
variables (i.e. pvars). *)
|
|
|
|
|
Means "lambda (root,next,svars). Exists evars. body".
|
|
|
|
|
Assume that root, next, svars, evars are disjoint sets of
|
|
|
|
|
primed identifiers, and include all the free primed identifiers in body.
|
|
|
|
|
body should not contain any non - primed identifiers or program
|
|
|
|
|
variables (i.e. pvars). *)
|
|
|
|
|
and hpara =
|
|
|
|
|
{ root: Ident.t;
|
|
|
|
|
next: Ident.t;
|
|
|
|
|
@ -843,8 +843,8 @@ and hpara =
|
|
|
|
|
body: hpred list }
|
|
|
|
|
|
|
|
|
|
(** parameter for the higher-order doubly-linked list predicates.
|
|
|
|
|
Assume that all the free identifiers in body_dll should belong to
|
|
|
|
|
cell, blink, flink, svars_dll, evars_dll. *)
|
|
|
|
|
Assume that all the free identifiers in body_dll should belong to
|
|
|
|
|
cell, blink, flink, svars_dll, evars_dll. *)
|
|
|
|
|
and hpara_dll =
|
|
|
|
|
{ cell: Ident.t; (** address cell *)
|
|
|
|
|
blink: Ident.t; (** backward link *)
|
|
|
|
|
@ -1087,8 +1087,8 @@ let binop_compare o1 o2 = match o1, o2 with
|
|
|
|
|
let binop_equal o1 o2 = binop_compare o1 o2 = 0
|
|
|
|
|
|
|
|
|
|
(** This function returns true if the operation is injective
|
|
|
|
|
wrt. each argument: op(e,-) and op(-, e) is injective for all e.
|
|
|
|
|
The return value false means "don't know". *)
|
|
|
|
|
wrt. each argument: op(e,-) and op(-, e) is injective for all e.
|
|
|
|
|
The return value false means "don't know". *)
|
|
|
|
|
let binop_injective = function
|
|
|
|
|
| PlusA | PlusPI | MinusA | MinusPI | MinusPP -> true
|
|
|
|
|
| _ -> false
|
|
|
|
|
@ -1099,9 +1099,9 @@ let binop_invertible = function
|
|
|
|
|
| _ -> false
|
|
|
|
|
|
|
|
|
|
(** This function inverts an injective binary operator
|
|
|
|
|
with respect to the first argument. It returns an expression [e'] such that
|
|
|
|
|
BinOp([binop], [e'], [exp1]) = [exp2]. If the [binop] operation is not invertible,
|
|
|
|
|
the function raises an exception by calling "assert false". *)
|
|
|
|
|
with respect to the first argument. It returns an expression [e'] such that
|
|
|
|
|
BinOp([binop], [e'], [exp1]) = [exp2]. If the [binop] operation is not invertible,
|
|
|
|
|
the function raises an exception by calling "assert false". *)
|
|
|
|
|
let binop_invert bop e1 e2 =
|
|
|
|
|
let inverted_bop = match bop with
|
|
|
|
|
| PlusA -> MinusA
|
|
|
|
|
@ -1112,7 +1112,7 @@ let binop_invert bop e1 e2 =
|
|
|
|
|
BinOp(inverted_bop, e2, e1)
|
|
|
|
|
|
|
|
|
|
(** This function returns true if 0 is the right unit of [binop].
|
|
|
|
|
The return value false means "don't know". *)
|
|
|
|
|
The return value false means "don't know". *)
|
|
|
|
|
let binop_is_zero_runit = function
|
|
|
|
|
| PlusA | PlusPI | MinusA | MinusPI | MinusPP -> true
|
|
|
|
|
| _ -> false
|
|
|
|
|
@ -2030,8 +2030,8 @@ and pp_typ pe f te =
|
|
|
|
|
if !Config.print_types then pp_typ_full pe f te else ()
|
|
|
|
|
|
|
|
|
|
(** Pretty print a type declaration.
|
|
|
|
|
pp_base prints the variable for a declaration, or can be skip to print only the type
|
|
|
|
|
pp_size prints the expression for the array size *)
|
|
|
|
|
pp_base prints the variable for a declaration, or can be skip to print only the type
|
|
|
|
|
pp_size prints the expression for the array size *)
|
|
|
|
|
and pp_type_decl pe pp_base pp_size f = function
|
|
|
|
|
| Tvar tname -> F.fprintf f "%s %a" (typename_to_string tname) pp_base ()
|
|
|
|
|
| Tint ik -> F.fprintf f "%s %a" (ikind_to_string ik) pp_base ()
|
|
|
|
|
@ -2384,9 +2384,9 @@ let rec pp_star_seq pp f = function
|
|
|
|
|
|
|
|
|
|
(********* START OF MODULE Predicates **********)
|
|
|
|
|
(** Module Predicates records the occurrences of predicates as parameters
|
|
|
|
|
of (doubly -)linked lists and Epara. Provides unique numbering for predicates and an iterator. *)
|
|
|
|
|
of (doubly -)linked lists and Epara. Provides unique numbering for predicates and an iterator. *)
|
|
|
|
|
module Predicates : sig
|
|
|
|
|
(** predicate environment *)
|
|
|
|
|
(** predicate environment *)
|
|
|
|
|
type env
|
|
|
|
|
(** create an empty predicate environment *)
|
|
|
|
|
val empty_env : unit -> env
|
|
|
|
|
@ -2868,14 +2868,14 @@ let unsome_typ s = function
|
|
|
|
|
assert false
|
|
|
|
|
|
|
|
|
|
(** Turn an expression representing a type into the type it represents
|
|
|
|
|
If not a sizeof, return the default type if given, otherwise raise an exception *)
|
|
|
|
|
If not a sizeof, return the default type if given, otherwise raise an exception *)
|
|
|
|
|
let texp_to_typ default_opt = function
|
|
|
|
|
| Sizeof (t, _) -> t
|
|
|
|
|
| t ->
|
|
|
|
|
unsome_typ "texp_to_typ" default_opt
|
|
|
|
|
|
|
|
|
|
(** If a struct type with field f, return the type of f.
|
|
|
|
|
If not, return the default type if given, otherwise raise an exception *)
|
|
|
|
|
If not, return the default type if given, otherwise raise an exception *)
|
|
|
|
|
let struct_typ_fld default_opt f =
|
|
|
|
|
let def () = unsome_typ "struct_typ_fld" default_opt in
|
|
|
|
|
function
|
|
|
|
|
@ -2885,7 +2885,7 @@ let struct_typ_fld default_opt f =
|
|
|
|
|
| _ -> def ()
|
|
|
|
|
|
|
|
|
|
(** If an array type, return the type of the element.
|
|
|
|
|
If not, return the default type if given, otherwise raise an exception *)
|
|
|
|
|
If not, return the default type if given, otherwise raise an exception *)
|
|
|
|
|
let array_typ_elem default_opt = function
|
|
|
|
|
| Tarray (t_el, _) -> t_el
|
|
|
|
|
| t ->
|
|
|
|
|
@ -2903,7 +2903,7 @@ let rec root_of_lexp lexp = match lexp with
|
|
|
|
|
| Sizeof _ -> lexp
|
|
|
|
|
|
|
|
|
|
(** Checks whether an expression denotes a location by pointer arithmetic.
|
|
|
|
|
Currently, catches array - indexing expressions such as a[i] only. *)
|
|
|
|
|
Currently, catches array - indexing expressions such as a[i] only. *)
|
|
|
|
|
let rec exp_pointer_arith = function
|
|
|
|
|
| Lfield (e, _, _) -> exp_pointer_arith e
|
|
|
|
|
| Lindex _ -> true
|
|
|
|
|
@ -2999,9 +2999,9 @@ and hpred_fpv = function
|
|
|
|
|
@ fpvars_in_elist
|
|
|
|
|
|
|
|
|
|
(** hpara should not contain any program variables.
|
|
|
|
|
This is because it might cause problems when we do interprocedural
|
|
|
|
|
analysis. In interprocedural analysis, we should consider the issue
|
|
|
|
|
of scopes of program variables. *)
|
|
|
|
|
This is because it might cause problems when we do interprocedural
|
|
|
|
|
analysis. In interprocedural analysis, we should consider the issue
|
|
|
|
|
of scopes of program variables. *)
|
|
|
|
|
and hpara_fpv para =
|
|
|
|
|
let fpvars_in_body = list_flatten (list_map hpred_fpv para.body) in
|
|
|
|
|
match fpvars_in_body with
|
|
|
|
|
@ -3009,9 +3009,9 @@ and hpara_fpv para =
|
|
|
|
|
| _ -> assert false
|
|
|
|
|
|
|
|
|
|
(** hpara_dll should not contain any program variables.
|
|
|
|
|
This is because it might cause problems when we do interprocedural
|
|
|
|
|
analysis. In interprocedural analysis, we should consider the issue
|
|
|
|
|
of scopes of program variables. *)
|
|
|
|
|
This is because it might cause problems when we do interprocedural
|
|
|
|
|
analysis. In interprocedural analysis, we should consider the issue
|
|
|
|
|
of scopes of program variables. *)
|
|
|
|
|
and hpara_dll_fpv para =
|
|
|
|
|
let fpvars_in_body = list_flatten (list_map hpred_fpv para.body_dll) in
|
|
|
|
|
match fpvars_in_body with
|
|
|
|
|
@ -3069,7 +3069,7 @@ let rec remove_duplicates_from_sorted special_equal = function
|
|
|
|
|
else x:: (remove_duplicates_from_sorted special_equal (y:: l))
|
|
|
|
|
|
|
|
|
|
(** Convert a [fav] to a list of identifiers while preserving the order
|
|
|
|
|
that the identifiers were added to [fav]. *)
|
|
|
|
|
that the identifiers were added to [fav]. *)
|
|
|
|
|
let fav_to_list fav =
|
|
|
|
|
list_rev !fav
|
|
|
|
|
|
|
|
|
|
@ -3107,7 +3107,7 @@ let rec ident_sorted_list_subset l1 l2 =
|
|
|
|
|
else false
|
|
|
|
|
|
|
|
|
|
(** [fav_subset_ident fav1 fav2] returns true if every ident in [fav1]
|
|
|
|
|
is in [fav2].*)
|
|
|
|
|
is in [fav2].*)
|
|
|
|
|
let fav_subset_ident fav1 fav2 =
|
|
|
|
|
ident_sorted_list_subset (fav_to_list fav1) (fav_to_list fav2)
|
|
|
|
|
|
|
|
|
|
@ -3173,9 +3173,9 @@ let hpred_fav =
|
|
|
|
|
fav_imperative_to_functional hpred_fav_add
|
|
|
|
|
|
|
|
|
|
(** This function should be used before adding a new
|
|
|
|
|
index to Earray. The [exp] is the newly created
|
|
|
|
|
index. This function "cleans" [exp] according to whether it is the footprint or current part of the prop.
|
|
|
|
|
The function faults in the re - execution mode, as an internal check of the tool. *)
|
|
|
|
|
index to Earray. The [exp] is the newly created
|
|
|
|
|
index. This function "cleans" [exp] according to whether it is the footprint or current part of the prop.
|
|
|
|
|
The function faults in the re - execution mode, as an internal check of the tool. *)
|
|
|
|
|
let array_clean_new_index footprint_part new_idx =
|
|
|
|
|
if footprint_part && not !Config.footprint then assert false;
|
|
|
|
|
let fav = exp_fav new_idx in
|
|
|
|
|
@ -3288,8 +3288,8 @@ let sub_check_inv sub =
|
|
|
|
|
(sub_check_sortedness sub) && not (sub_check_duplicated_ids sub)
|
|
|
|
|
|
|
|
|
|
(** Create a substitution from a list of pairs.
|
|
|
|
|
For all (id1, e1), (id2, e2) in the input list,
|
|
|
|
|
if id1 = id2, then e1 = e2. *)
|
|
|
|
|
For all (id1, e1), (id2, e2) in the input list,
|
|
|
|
|
if id1 = id2, then e1 = e2. *)
|
|
|
|
|
let sub_of_list sub =
|
|
|
|
|
let sub' = list_sort ident_exp_compare sub in
|
|
|
|
|
let sub'' = remove_duplicates_from_sorted ident_exp_equal sub' in
|
|
|
|
|
@ -3315,7 +3315,7 @@ let sub_to_list sub =
|
|
|
|
|
let sub_empty = sub_of_list []
|
|
|
|
|
|
|
|
|
|
(** Join two substitutions into one.
|
|
|
|
|
For all id in dom(sub1) cap dom(sub2), sub1(id) = sub2(id). *)
|
|
|
|
|
For all id in dom(sub1) cap dom(sub2), sub1(id) = sub2(id). *)
|
|
|
|
|
let sub_join sub1 sub2 =
|
|
|
|
|
let sub = sorted_list_merge ident_exp_compare sub1 sub2 in
|
|
|
|
|
let sub' = remove_duplicates_from_sorted ident_exp_equal sub in
|
|
|
|
|
@ -3323,9 +3323,9 @@ let sub_join sub1 sub2 =
|
|
|
|
|
sub
|
|
|
|
|
|
|
|
|
|
(** Compute the common id-exp part of two inputs [subst1] and [subst2].
|
|
|
|
|
The first component of the output is this common part.
|
|
|
|
|
The second and third components are the remainder of [subst1]
|
|
|
|
|
and [subst2], respectively. *)
|
|
|
|
|
The first component of the output is this common part.
|
|
|
|
|
The second and third components are the remainder of [subst1]
|
|
|
|
|
and [subst2], respectively. *)
|
|
|
|
|
let sub_symmetric_difference sub1_in sub2_in =
|
|
|
|
|
let rec diff sub_common sub1_only sub2_only sub1 sub2 =
|
|
|
|
|
match sub1, sub2 with
|
|
|
|
|
@ -3353,21 +3353,21 @@ let sub_find filter (sub: subst) =
|
|
|
|
|
snd (list_find (fun (i, _) -> filter i) sub)
|
|
|
|
|
|
|
|
|
|
(** [sub_filter filter sub] restricts the domain of [sub] to the
|
|
|
|
|
identifiers satisfying [filter]. *)
|
|
|
|
|
identifiers satisfying [filter]. *)
|
|
|
|
|
let sub_filter filter (sub: subst) =
|
|
|
|
|
list_filter (fun (i, _) -> filter i) sub
|
|
|
|
|
|
|
|
|
|
(** [sub_filter_pair filter sub] restricts the domain of [sub] to the
|
|
|
|
|
identifiers satisfying [filter(id, sub(id))]. *)
|
|
|
|
|
identifiers satisfying [filter(id, sub(id))]. *)
|
|
|
|
|
let sub_filter_pair = list_filter
|
|
|
|
|
|
|
|
|
|
(** [sub_range_partition filter sub] partitions [sub] according to
|
|
|
|
|
whether range expressions satisfy [filter]. *)
|
|
|
|
|
whether range expressions satisfy [filter]. *)
|
|
|
|
|
let sub_range_partition filter (sub: subst) =
|
|
|
|
|
list_partition (fun (_, e) -> filter e) sub
|
|
|
|
|
|
|
|
|
|
(** [sub_domain_partition filter sub] partitions [sub] according to
|
|
|
|
|
whether domain identifiers satisfy [filter]. *)
|
|
|
|
|
whether domain identifiers satisfy [filter]. *)
|
|
|
|
|
let sub_domain_partition filter (sub: subst) =
|
|
|
|
|
list_partition (fun (i, _) -> filter i) sub
|
|
|
|
|
|
|
|
|
|
@ -3384,7 +3384,7 @@ let sub_range_map f sub =
|
|
|
|
|
sub_of_list (list_map (fun (i, e) -> (i, f e)) sub)
|
|
|
|
|
|
|
|
|
|
(** [sub_map f g sub] applies the renaming [f] to identifiers in the domain
|
|
|
|
|
of [sub] and the substitution [g] to the expressions in the range of [sub]. *)
|
|
|
|
|
of [sub] and the substitution [g] to the expressions in the range of [sub]. *)
|
|
|
|
|
let sub_map f g sub =
|
|
|
|
|
sub_of_list (list_map (fun (i, e) -> (f i, g e)) sub)
|
|
|
|
|
|
|
|
|
|
@ -3398,7 +3398,7 @@ let extend_sub sub id exp : subst option =
|
|
|
|
|
else Some (sorted_list_merge compare sub [(id, exp)])
|
|
|
|
|
|
|
|
|
|
(** Free auxilary variables in the domain and range of the
|
|
|
|
|
substitution. *)
|
|
|
|
|
substitution. *)
|
|
|
|
|
let sub_fav_add fav (sub: subst) =
|
|
|
|
|
list_iter (fun (id, e) -> fav ++ id; exp_fav_add fav e) sub
|
|
|
|
|
|
|
|
|
|
@ -3840,9 +3840,9 @@ let sigma_to_sigma_ne sigma : (atom list * hpred list) list =
|
|
|
|
|
[([], sigma)]
|
|
|
|
|
|
|
|
|
|
(** [hpara_instantiate para e1 e2 elist] instantiates [para] with [e1],
|
|
|
|
|
[e2] and [elist]. If [para = lambda (x, y, xs). exists zs. b],
|
|
|
|
|
then the result of the instantiation is [b\[e1 / x, e2 / y, elist / xs, _zs'/ zs\]]
|
|
|
|
|
for some fresh [_zs'].*)
|
|
|
|
|
[e2] and [elist]. If [para = lambda (x, y, xs). exists zs. b],
|
|
|
|
|
then the result of the instantiation is [b\[e1 / x, e2 / y, elist / xs, _zs'/ zs\]]
|
|
|
|
|
for some fresh [_zs'].*)
|
|
|
|
|
let hpara_instantiate para e1 e2 elist =
|
|
|
|
|
let subst_for_svars =
|
|
|
|
|
let g id e = (id, e) in
|
|
|
|
|
@ -3859,9 +3859,9 @@ let hpara_instantiate para e1 e2 elist =
|
|
|
|
|
(ids_evars, list_map (hpred_sub subst) para.body)
|
|
|
|
|
|
|
|
|
|
(** [hpara_dll_instantiate para cell blink flink elist] instantiates [para] with [cell],
|
|
|
|
|
[blink], [flink], and [elist]. If [para = lambda (x, y, z, xs). exists zs. b],
|
|
|
|
|
then the result of the instantiation is [b\[cell / x, blink / y, flink / z, elist / xs, _zs'/ zs\]]
|
|
|
|
|
for some fresh [_zs'].*)
|
|
|
|
|
[blink], [flink], and [elist]. If [para = lambda (x, y, z, xs). exists zs. b],
|
|
|
|
|
then the result of the instantiation is [b\[cell / x, blink / y, flink / z, elist / xs, _zs'/ zs\]]
|
|
|
|
|
for some fresh [_zs'].*)
|
|
|
|
|
let hpara_dll_instantiate (para: hpara_dll) cell blink flink elist =
|
|
|
|
|
let subst_for_svars =
|
|
|
|
|
let g id e = (id, e) in
|
|
|
|
|
|
Jules Villard
10 years ago