pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[backend] Make Sil.subst type variant to allow more types of substitution

Browse Source 
Reviewed By: jberdine

Differential Revision: D5182491

fbshipit-source-id: 3ea6b66
master
Andrzej Kotulski 7 years ago committed by Facebook Github Bot
parent 431b5c6ede
commit 621ace48af
17 changed files with 234 additions and 228 deletions
Show Stats Download Patch File Download Diff File

57
infer/src/IR/Sil.re
Unescape View File

@ -1651,11 +1651,13 @@ type ident_exp = (Ident.t, Exp.t) [@@deriving compare];
let equal_ident_exp = [%compare.equal : ident_exp];
type subst = list ident_exp [@@deriving compare];
type exp_subst = list ident_exp [@@deriving compare];
type subst = [ | `Exp exp_subst] [@@deriving compare];
/** Equality for substitutions. */
let equal_subst = [%compare.equal : subst];
let equal_exp_subst = [%compare.equal : exp_subst];
let sub_check_duplicated_ids sub => {
let f (id1, _) (id2, _) => Ident.equal id1 id2;
@ -1666,7 +1668,7 @@ let 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. */
let sub_of_list sub => {
let exp_subst_of_list sub => {
let sub' = List.sort cmp::compare_ident_exp sub;
let sub'' = remove_duplicates_from_sorted equal_ident_exp sub';
if (sub_check_duplicated_ids sub'') {
@ -1675,9 +1677,11 @@ let sub_of_list sub => {
sub'
};
let subst_of_list sub => `Exp (exp_subst_of_list sub);
/** like sub_of_list, but allow duplicate ids and only keep the first occurrence */
let sub_of_list_duplicates sub => {
/** like exp_subst_of_list, but allow duplicate ids and only keep the first occurrence */
let exp_subst_of_list_duplicates sub => {
let sub' = List.sort cmp::compare_ident_exp sub;
let rec remove_duplicate_ids =
fun
@ -1697,7 +1701,14 @@ let sub_to_list sub => sub;
/** The empty substitution. */
let sub_empty = sub_of_list [];
let exp_sub_empty = exp_subst_of_list [];
let sub_empty = `Exp exp_sub_empty;
let is_sub_empty =
fun
| `Exp [] => true
| `Exp _ => false;
/** Join two substitutions into one.
@ -1743,12 +1754,12 @@ let sub_symmetric_difference sub1_in sub2_in => {
/** [sub_find filter sub] returns the expression associated to the first identifier
that satisfies [filter]. Raise [Not_found] if there isn't one. */
let sub_find filter (sub: subst) => snd (List.find_exn f::(fun (i, _) => filter i) sub);
let sub_find filter (sub: exp_subst) => snd (List.find_exn f::(fun (i, _) => filter i) sub);
/** [sub_filter filter sub] restricts the domain of [sub] to the
identifiers satisfying [filter]. */
let sub_filter filter (sub: subst) => List.filter f::(fun (i, _) => filter i) sub;
let sub_filter filter (sub: exp_subst) => List.filter f::(fun (i, _) => filter i) sub;
/** [sub_filter_pair filter sub] restricts the domain of [sub] to the
@ -1758,12 +1769,14 @@ let sub_filter_pair = List.filter;
/** [sub_range_partition filter sub] partitions [sub] according to
whether range expressions satisfy [filter]. */
let sub_range_partition filter (sub: subst) => List.partition_tf f::(fun (_, e) => filter e) sub;
let sub_range_partition filter (sub: exp_subst) =>
List.partition_tf f::(fun (_, e) => filter e) sub;
/** [sub_domain_partition filter sub] partitions [sub] according to
whether domain identifiers satisfy [filter]. */
let sub_domain_partition filter (sub: subst) => List.partition_tf f::(fun (i, _) => filter i) sub;
let sub_domain_partition filter (sub: exp_subst) =>
List.partition_tf f::(fun (i, _) => filter i) sub;
/** Return the list of identifiers in the domain of the substitution. */
@ -1775,18 +1788,18 @@ let sub_range sub => List.map f::snd sub;
/** [sub_range_map f sub] applies [f] to the expressions in the range of [sub]. */
let sub_range_map f sub => sub_of_list (List.map f::(fun (i, e) => (i, f e)) sub);
let sub_range_map f sub => exp_subst_of_list (List.map f::(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]. */
let sub_map f g sub => sub_of_list (List.map f::(fun (i, e) => (f i, g e)) sub);
let sub_map f g sub => exp_subst_of_list (List.map f::(fun (i, e) => (f i, g e)) sub);
let mem_sub id sub => List.exists f::(fun (id1, _) => Ident.equal id id1) sub;
/** Extend substitution and return [None] if not possible. */
let extend_sub sub id exp :option subst => {
let extend_sub sub id exp :option exp_subst => {
let compare (id1, _) (id2, _) => Ident.compare id1 id2;
if (mem_sub id sub) {
None
@ -1798,7 +1811,7 @@ let extend_sub sub id exp :option subst => {
/** Free auxilary variables in the domain and range of the
substitution. */
let sub_fav_add fav (sub: subst) =>
let sub_fav_add fav (sub: exp_subst) =>
List.iter
f::(
fun (id, e) => {
@ -1808,8 +1821,6 @@ let sub_fav_add fav (sub: subst) =>
)
sub;
let sub_fpv (sub: subst) => List.concat_map f::(fun (_, e) => exp_fpv e) sub;
/** Substitutions do not contain binders */
let sub_av_add = sub_fav_add;
@ -1898,12 +1909,12 @@ let rec exp_sub_ids (f: Ident.t => Exp.t) exp =>
let rec apply_sub subst id =>
switch subst {
| [] => Exp.Var id
| [(i, e), ...l] =>
| `Exp [] => Exp.Var id
| `Exp [(i, e), ...l] =>
if (Ident.equal i id) {
e
} else {
apply_sub l id
apply_sub (`Exp l) id
}
};
@ -2473,7 +2484,9 @@ let hpara_instantiate para e1 e2 elist => {
}
};
let subst =
sub_of_list ([(para.root, e1), (para.next, e2), ...subst_for_svars] @ subst_for_evars);
`Exp (
exp_subst_of_list ([(para.root, e1), (para.next, e2), ...subst_for_svars] @ subst_for_evars)
);
(ids_evars, List.map f::(hpred_sub subst) para.body)
};
@ -2501,8 +2514,10 @@ let hpara_dll_instantiate (para: hpara_dll) cell blink flink elist => {
}
};
let subst =
sub_of_list (
`Exp (
exp_subst_of_list (
[(para.cell, cell), (para.blink, blink), (para.flink, flink), ...subst_for_svars] @ subst_for_evars
)
);
(ids_evars, List.map f::(hpred_sub subst) para.body_dll)
};

55
infer/src/IR/Sil.rei
Unescape View File

@ -668,108 +668,113 @@ let hpara_av_add: fav => hpara => unit;
/** {2 Substitution} */
type subst [@@deriving compare];
type exp_subst [@@deriving compare];
type subst = [ | `Exp exp_subst] [@@deriving compare];
/** Equality for substitutions. */
let equal_subst: subst => subst => bool;
let equal_exp_subst: exp_subst => exp_subst => bool;
/** Create a substitution from a list of pairs.
For all (id1, e1), (id2, e2) in the input list,
if id1 = id2, then e1 = e2. */
let sub_of_list: list (Ident.t, Exp.t) => subst;
let exp_subst_of_list: list (Ident.t, Exp.t) => exp_subst;
let subst_of_list: list (Ident.t, Exp.t) => subst;
/** like sub_of_list, but allow duplicate ids and only keep the first occurrence */
let sub_of_list_duplicates: list (Ident.t, Exp.t) => subst;
/** like exp_subst_of_list, but allow duplicate ids and only keep the first occurrence */
let exp_subst_of_list_duplicates: list (Ident.t, Exp.t) => exp_subst;
/** Convert a subst to a list of pairs. */
let sub_to_list: subst => list (Ident.t, Exp.t);
let sub_to_list: exp_subst => list (Ident.t, Exp.t);
/** The empty substitution. */
let sub_empty: subst;
let exp_sub_empty: exp_subst;
let is_sub_empty: subst => bool;
/* let to_exp_subst : [< `Exp exp_subst] => exp_subst; */
/** 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. */
let sub_join: subst => subst => subst;
let sub_join: exp_subst => exp_subst => exp_subst;
/** 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. */
let sub_symmetric_difference: subst => subst => (subst, subst, subst);
let sub_symmetric_difference: exp_subst => exp_subst => (exp_subst, exp_subst, exp_subst);
/** [sub_find filter sub] returns the expression associated to the first identifier
that satisfies [filter].
Raise [Not_found] if there isn't one. */
let sub_find: (Ident.t => bool) => subst => Exp.t;
let sub_find: (Ident.t => bool) => exp_subst => Exp.t;
/** [sub_filter filter sub] restricts the domain of [sub] to the
identifiers satisfying [filter]. */
let sub_filter: (Ident.t => bool) => subst => subst;
let sub_filter: (Ident.t => bool) => exp_subst => exp_subst;
/** [sub_filter_exp filter sub] restricts the domain of [sub] to the
identifiers satisfying [filter(id, sub(id))]. */
let sub_filter_pair: subst => f::((Ident.t, Exp.t) => bool) => subst;
let sub_filter_pair: exp_subst => f::((Ident.t, Exp.t) => bool) => exp_subst;
/** [sub_range_partition filter sub] partitions [sub] according to
whether range expressions satisfy [filter]. */
let sub_range_partition: (Exp.t => bool) => subst => (subst, subst);
let sub_range_partition: (Exp.t => bool) => exp_subst => (exp_subst, exp_subst);
/** [sub_domain_partition filter sub] partitions [sub] according to
whether domain identifiers satisfy [filter]. */
let sub_domain_partition: (Ident.t => bool) => subst => (subst, subst);
let sub_domain_partition: (Ident.t => bool) => exp_subst => (exp_subst, exp_subst);
/** Return the list of identifiers in the domain of the substitution. */
let sub_domain: subst => list Ident.t;
let sub_domain: exp_subst => list Ident.t;
/** Return the list of expressions in the range of the substitution. */
let sub_range: subst => list Exp.t;
let sub_range: exp_subst => list Exp.t;
/** [sub_range_map f sub] applies [f] to the expressions in the range of [sub]. */
let sub_range_map: (Exp.t => Exp.t) => subst => subst;
let sub_range_map: (Exp.t => Exp.t) => exp_subst => exp_subst;
/** [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]. */
let sub_map: (Ident.t => Ident.t) => (Exp.t => Exp.t) => subst => subst;
let sub_map: (Ident.t => Ident.t) => (Exp.t => Exp.t) => exp_subst => exp_subst;
/** Checks whether [id] belongs to the domain of [subst]. */
let mem_sub: Ident.t => subst => bool;
let mem_sub: Ident.t => exp_subst => bool;
/** Extend substitution and return [None] if not possible. */
let extend_sub: subst => Ident.t => Exp.t => option subst;
let extend_sub: exp_subst => Ident.t => Exp.t => option exp_subst;
/** Free auxilary variables in the domain and range of the
substitution. */
let sub_fav_add: fav => subst => unit;
let sub_fav_add: fav => exp_subst => unit;
/** Free or bound auxilary variables in the domain and range of the
substitution. */
let sub_av_add: fav => subst => unit;
/** Compute free pvars in a sub */
let sub_fpv: subst => list Pvar.t;
let sub_av_add: fav => exp_subst => unit;
/** substitution functions */

2
infer/src/backend/Attribute.ml
Unescape View File

@ -277,7 +277,7 @@ let deallocate_stack_vars tenv (p: 'a Prop.t) pvars =
let p' =
Prop.normalize tenv
(Prop.set p
~sub:Sil.sub_empty
~sub:Sil.exp_sub_empty
~sigma: (Prop.sigma_replace_exp tenv exp_replace sigma_other)) in
let p'' =
let res = ref p' in

34
infer/src/backend/abs.ml
Unescape View File

@ -22,8 +22,8 @@ type rule =
r_root: Match.hpred_pat;
r_sigma: Match.hpred_pat list; (* sigma should be in a specific order *)
r_new_sigma: Sil.hpred list;
r_new_pi: Prop.normal Prop.t -> Prop.normal Prop.t -> Sil.subst -> Sil.atom list;
r_condition: Prop.normal Prop.t -> Sil.subst -> bool }
r_new_pi: Prop.normal Prop.t -> Prop.normal Prop.t -> Sil.exp_subst -> Sil.atom list;
r_condition: Prop.normal Prop.t -> Sil.exp_subst -> bool }
let sigma_rewrite tenv p r : Prop.normal Prop.t option =
match (Match.prop_match_with_impl tenv p r.r_condition r.r_vars r.r_root r.r_sigma) with
@ -32,7 +32,7 @@ let sigma_rewrite tenv p r : Prop.normal Prop.t option =
if not (r.r_condition p_leftover sub) then None
else
let res_pi = r.r_new_pi p p_leftover sub in
let res_sigma = Prop.sigma_sub sub r.r_new_sigma in
let res_sigma = Prop.sigma_sub (`Exp sub) r.r_new_sigma in
let p_with_res_pi = List.fold ~f:(Prop.prop_atom_and tenv) ~init:p_leftover res_pi in
let p_new = Prop.prop_sigma_star p_with_res_pi res_sigma in
Some (Prop.normalize tenv p_new)
@ -63,7 +63,7 @@ let create_fresh_primeds_ls para =
let exps_tuple = (exp_base, exp_next, exp_end, exps_shared) in
(ids_tuple, exps_tuple)
let create_condition_ls ids_private id_base p_leftover (inst: Sil.subst) =
let create_condition_ls ids_private id_base p_leftover (inst: Sil.exp_subst) =
let (insts_of_private_ids, insts_of_public_ids, inst_of_base) =
let f id' = List.exists ~f:(fun id'' -> Ident.equal id' id'') ids_private in
let (inst_private, inst_public) = Sil.sub_domain_partition f inst in
@ -112,7 +112,7 @@ let mk_rule_ptspts_ls tenv impl_ok1 impl_ok2 (para: Sil.hpara) =
let para_body_hpats = List.map ~f:mark_impl_flag para_body in
(ids, para_body_hpats) in
let lseg_res = Prop.mk_lseg tenv Sil.Lseg_NE para exp_base exp_end exps_shared in
let gen_pi_res _ _ (_: Sil.subst) = [] in
let gen_pi_res _ _ (_: Sil.exp_subst) = [] in
let condition =
let ids_private = id_next :: (ids_exist_fst @ ids_exist_snd) in
create_condition_ls ids_private id_base in
@ -138,7 +138,7 @@ let mk_rule_ptsls_ls tenv k2 impl_ok1 impl_ok2 para =
(allow_impl hpred, List.map ~f:allow_impl hpreds) in
let lseg_pat = { Match.hpred = Prop.mk_lseg tenv k2 para exp_next exp_end exps_shared; Match.flag = impl_ok2 } in
let lseg_res = Prop.mk_lseg tenv Sil.Lseg_NE para exp_base exp_end exps_shared in
let gen_pi_res _ _ (_: Sil.subst) = [] in
let gen_pi_res _ _ (_: Sil.exp_subst) = [] in
let condition =
let ids_private = id_next :: ids_exist in
create_condition_ls ids_private id_base in
@ -160,7 +160,7 @@ let mk_rule_lspts_ls tenv k1 impl_ok1 impl_ok2 para =
let para_body_pat = List.map ~f:allow_impl para_body in
(ids, para_body_pat) in
let lseg_res = Prop.mk_lseg tenv Sil.Lseg_NE para exp_base exp_end exps_shared in
let gen_pi_res _ _ (_: Sil.subst) = [] in
let gen_pi_res _ _ (_: Sil.exp_subst) = [] in
let condition =
let ids_private = id_next :: ids_exist in
create_condition_ls ids_private id_base in
@ -185,7 +185,7 @@ let mk_rule_lsls_ls tenv k1 k2 impl_ok1 impl_ok2 para =
{ Match.hpred = Prop.mk_lseg tenv k2 para exp_next exp_end exps_shared; Match.flag = impl_ok2 } in
let k_res = lseg_kind_add k1 k2 in
let lseg_res = Prop.mk_lseg tenv k_res para exp_base exp_end exps_shared in
let gen_pi_res _ _ (_: Sil.subst) = []
let gen_pi_res _ _ (_: Sil.exp_subst) = []
(*
let inst_base, inst_next, inst_end =
let find x = sub_find (equal x) inst in
@ -269,7 +269,7 @@ let mk_rule_ptspts_dll tenv impl_ok1 impl_ok2 para =
let para_body_hpats = List.map ~f:mark_impl_flag para_body in
(ids, para_body_hpats) in
let dllseg_res = Prop.mk_dllseg tenv Sil.Lseg_NE para exp_iF exp_oB exp_oF exp_iF' exps_shared in
let gen_pi_res _ _ (_: Sil.subst) = [] in
let gen_pi_res _ _ (_: Sil.exp_subst) = [] in
let condition =
(* for the case of ptspts since iF'=iB therefore iF' cannot be private*)
let ids_private = ids_exist_fst @ ids_exist_snd in
@ -312,7 +312,7 @@ let mk_rule_ptsdll_dll tenv k2 impl_ok1 impl_ok2 para =
(allow_impl hpred, List.map ~f:allow_impl hpreds) in
let dllseg_pat = { Match.hpred = Prop.mk_dllseg tenv k2 para exp_iF' exp_iF exp_oF exp_iB exps_shared; Match.flag = impl_ok2 } in
let dllseg_res = Prop.mk_dllseg tenv Sil.Lseg_NE para exp_iF exp_oB exp_oF exp_iB exps_shared in
let gen_pi_res _ _ (_: Sil.subst) = [] in
let gen_pi_res _ _ (_: Sil.exp_subst) = [] in
let condition =
let ids_private = id_iF':: ids_exist in
create_condition_dll ids_private id_iF in
@ -345,7 +345,7 @@ let mk_rule_dllpts_dll tenv k1 impl_ok1 impl_ok2 para =
List.map ~f:allow_impl para_inst in
let dllseg_pat = { Match.hpred = Prop.mk_dllseg tenv k1 para exp_iF exp_oB exp_iF' exp_oB' exps_shared; Match.flag = impl_ok1 } in
let dllseg_res = Prop.mk_dllseg tenv Sil.Lseg_NE para exp_iF exp_oB exp_oF exp_iF' exps_shared in
let gen_pi_res _ _ (_: Sil.subst) = [] in
let gen_pi_res _ _ (_: Sil.exp_subst) = [] in
let condition =
let ids_private = id_oB':: ids_exist in
create_condition_dll ids_private id_iF in
@ -378,7 +378,7 @@ let mk_rule_dlldll_dll tenv k1 k2 impl_ok1 impl_ok2 para =
let lseg_snd_pat = { Match.hpred = Prop.mk_dllseg tenv k2 para exp_iF' exp_oB' exp_oF exp_iB exps_shared; Match.flag = impl_ok2 } in
let k_res = lseg_kind_add k1 k2 in
let lseg_res = Prop.mk_dllseg tenv k_res para exp_iF exp_oB exp_oF exp_iB exps_shared in
let gen_pi_res _ _ (_: Sil.subst) = [] in
let gen_pi_res _ _ (_: Sil.exp_subst) = [] in
let condition =
let ids_private = [id_iF'; id_oB'] in
create_condition_dll ids_private id_iF in
@ -603,10 +603,10 @@ let reset_current_rules () =
Global.current_rules := []
let eqs_sub subst eqs =
List.map ~f:(fun (e1, e2) -> (Sil.exp_sub subst e1, Sil.exp_sub subst e2)) eqs
List.map ~f:(fun (e1, e2) -> (Sil.exp_sub (`Exp subst) e1, Sil.exp_sub (`Exp subst) e2)) eqs
let eqs_solve ids_in eqs_in =
let rec solve (sub: Sil.subst) (eqs: (Exp.t * Exp.t) list) : Sil.subst option =
let rec solve (sub: Sil.exp_subst) (eqs: (Exp.t * Exp.t) list) : Sil.exp_subst option =
let do_default id e eqs_rest =
if not (List.exists ~f:(fun id' -> Ident.equal id id') ids_in) then None
else
@ -639,7 +639,7 @@ let eqs_solve ids_in eqs_in =
let filter id =
not (List.exists ~f:(fun id' -> Ident.equal id id') sub_dom) in
List.filter ~f:filter ids_in in
match solve Sil.sub_empty eqs_in with
match solve Sil.exp_sub_empty eqs_in with
| None -> None
| Some sub -> Some (compute_ids sub, sub)
@ -677,7 +677,7 @@ let sigma_special_cases ids sigma : (Ident.t list * Sil.hpred list) list =
match (eqs_solve ids_all eqs_cur) with
| None -> acc
| Some (ids_res, sub) ->
(ids_res, List.map ~f:(Sil.hpred_sub sub) sigma_cur) :: acc in
(ids_res, List.map ~f:(Sil.hpred_sub (`Exp sub)) sigma_cur) :: acc in
List.fold ~f ~init:[] special_cases_eqs in
List.rev special_cases_rev
@ -794,7 +794,7 @@ let abstract_pure_part tenv p ~(from_abstract_footprint: bool) =
List.rev new_pure in
let new_pure = do_pure (Prop.get_pure p) in
let eprop' = Prop.set p ~pi:new_pure ~sub:Sil.sub_empty in
let eprop' = Prop.set p ~pi:new_pure ~sub:Sil.exp_sub_empty in
let eprop'' =
if !Config.footprint && not from_abstract_footprint then
let new_pi_footprint = do_pure p.Prop.pi_fp in

14
infer/src/backend/dom.ml
Unescape View File

@ -535,8 +535,8 @@ module Rename : sig
val lookup_list : side -> Exp.t list -> Exp.t list
val lookup_list_todo : side -> Exp.t list -> Exp.t list
val to_subst_proj : side -> Sil.fav -> Sil.subst
val to_subst_emb : side -> Sil.subst
val to_subst_proj : side -> Sil.fav -> Sil.exp_subst
val to_subst_emb : side -> Sil.exp_subst
(*
val get : Exp.t -> Exp.t -> Exp.t option
val pp : printenv -> Format.formatter -> (Exp.t * Exp.t * Exp.t) list -> unit
@ -635,7 +635,7 @@ end = struct
| (_, e):: ((_, e'):: _ as t) -> Exp.equal e e' || find_duplicates t
| _ -> false in
if find_duplicates sub_list_side_sorted then (L.d_strln "failure reason 11"; raise Sil.JoinFail)
else Sil.sub_of_list sub_list_side
else Sil.exp_subst_of_list sub_list_side
let to_subst_emb (side : side) =
let renaming_restricted =
@ -657,7 +657,7 @@ end = struct
| (i, _):: ((i', _):: _ as t) -> Ident.equal i i' || find_duplicates t
| _ -> false in
if find_duplicates sub_list_sorted then (L.d_strln "failure reason 12"; raise Sil.JoinFail)
else Sil.sub_of_list sub_list_sorted
else Sil.exp_subst_of_list sub_list_sorted
let get_others' f_lookup side e =
let side_op = opposite side in
@ -1327,7 +1327,7 @@ let sigma_renaming_check (lhs: side) (sigma: Prop.sigma) (sigma_new: Prop.sigma)
* and check that the renaming of primed vars is injective *)
let fav_sigma = Prop.sigma_fav sigma_new in
let sub = Rename.to_subst_proj lhs fav_sigma in
let sigma' = Prop.sigma_sub sub sigma_new in
let sigma' = Prop.sigma_sub (`Exp sub) sigma_new in
equal_sigma sigma sigma'
let sigma_renaming_check_lhs = sigma_renaming_check Lhs
@ -1713,7 +1713,7 @@ let pi_partial_meet tenv (p: Prop.normal Prop.t) (ep1: 'a Prop.t) (ep2: 'b Prop.
let handle_atom sub dom atom =
let fav_list = Sil.fav_to_list (Sil.atom_fav atom) in
if List.for_all ~f:(fun id -> Ident.IdentSet.mem id dom) fav_list then
Sil.atom_sub sub atom
Sil.atom_sub (`Exp sub) atom
else (L.d_str "handle_atom failed on "; Sil.d_atom atom; L.d_ln (); raise Sil.JoinFail) in
let f1 p' atom =
Prop.prop_atom_and tenv p' (handle_atom sub1 dom1 atom) in
@ -1745,7 +1745,7 @@ let eprop_partial_meet tenv (ep1: 'a Prop.t) (ep2: 'b Prop.t) : 'c Prop.t =
let sub2 = ep2.Prop.sub in
let range1 = Sil.sub_range sub1 in
let f e = Sil.fav_for_all (Sil.exp_fav e) Ident.is_normal in
Sil.equal_subst sub1 sub2 && List.for_all ~f range1 in
Sil.equal_exp_subst sub1 sub2 && List.for_all ~f range1 in
if not (sub_check ()) then
(L.d_strln "sub_check() failed"; raise Sil.JoinFail)

10
infer/src/backend/interproc.ml
Unescape View File

@ -285,7 +285,7 @@ let propagate_nodes_divergence
let prop_incons =
let mk_incons prop =
let p_abs = Abs.abstract pname tenv prop in
let p_zero = Prop.set p_abs ~sub:Sil.sub_empty ~sigma:[] in
let p_zero = Prop.set p_abs ~sub:Sil.exp_sub_empty ~sigma:[] in
Prop.normalize tenv (Prop.set p_zero ~pi:[Sil.Aneq (Exp.zero, Exp.zero)]) in
Paths.PathSet.map mk_incons diverging_states in
(L.d_strln_color Orange) "Propagating Divergence -- diverging states:";
@ -751,20 +751,20 @@ let extract_specs tenv pdesc pathset : Prop.normal Specs.spec list =
List.map
~f:(fun id -> (id, Exp.Var (Ident.create_fresh (Ident.knormal))))
(Sil.fav_to_list fav) in
Sil.sub_of_list sub_list in
Sil.exp_subst_of_list sub_list in
let pre_post_visited_list =
let pplist = Paths.PathSet.elements pathset in
let f (prop, path) =
let _, prop' = PropUtil.remove_locals_formals tenv pdesc prop in
let prop'' = Abs.abstract pname tenv prop' in
let pre, post = Prop.extract_spec prop'' in
let pre' = Prop.normalize tenv (Prop.prop_sub sub pre) in
let pre' = Prop.normalize tenv (Prop.prop_sub (`Exp sub) pre) in
if Config.curr_language_is Config.Java &&
Procdesc.get_access pdesc <> PredSymb.Private then
report_context_leaks pname post.Prop.sigma tenv;
let post' =
if Prover.check_inconsistency_base tenv prop then None
else Some (Prop.normalize tenv (Prop.prop_sub sub post), path) in
else Some (Prop.normalize tenv (Prop.prop_sub (`Exp sub) post), path) in
let visited =
let vset_ref = ref Procdesc.NodeSet.empty in
vset_ref_add_path vset_ref path;
@ -901,7 +901,7 @@ let initial_prop_from_pre tenv curr_f pre =
List.map
~f:(fun id -> (id, Exp.Var (Ident.create_fresh (Ident.kfootprint))))
vars in
let sub = Sil.sub_of_list sub_list in
let sub = Sil.subst_of_list sub_list in
let pre2 = Prop.prop_sub sub pre in
let pre3 =
Prop.set pre2 ~pi_fp:(Prop.get_pure pre2) ~sigma_fp:pre2.Prop.sigma in

38
infer/src/backend/match.ml
Unescape View File

@ -35,9 +35,9 @@ let rec pp_hpat_list pe f = function
(** Checks e1 = e2[sub ++ sub'] for some sub' with dom(sub') subseteq vars.
Returns (sub ++ sub', vars - dom(sub')). *)
let rec exp_match e1 sub vars e2 : (Sil.subst * Ident.t list) option =
let rec exp_match e1 sub vars e2 : (Sil.exp_subst * Ident.t list) option =
let check_equal sub vars e1 e2 =
let e2_inst = Sil.exp_sub sub e2
let e2_inst = Sil.exp_sub (`Exp sub) e2
in if (Exp.equal e1 e2_inst) then Some(sub, vars) else None in
match e1, e2 with
| _, Exp.Var id2 when (Ident.is_primed id2 && mem_idlist id2 vars) ->
@ -95,7 +95,7 @@ let exp_list_match es1 sub vars es2 =
dom(sub') subseteq vars. Returns (sub ++ sub', vars - dom(sub')).
WARNING: This function does not consider the fact that the analyzer
sometimes forgets fields of hpred. It can possibly cause a problem. *)
let rec strexp_match sexp1 sub vars sexp2 : (Sil.subst * Ident.t list) option =
let rec strexp_match sexp1 sub vars sexp2 : (Sil.exp_subst * Ident.t list) option =
match sexp1, sexp2 with
| Sil.Eexp (exp1, _), Sil.Eexp (exp2, _) ->
exp_match exp1 sub vars exp2
@ -139,7 +139,7 @@ and isel_match isel1 sub vars isel2 =
| [], [] -> Some (sub, vars)
| [], _ | _, [] -> None
| (idx1, se1') :: isel1', (idx2, se2') :: isel2' ->
let idx2 = Sil.exp_sub sub idx2 in
let idx2 = Sil.exp_sub (`Exp sub) idx2 in
let sanity_check = not (List.exists ~f:(fun id -> Sil.ident_in_exp id idx2) vars) in
if (not sanity_check) then begin
let pe = Pp.text in
@ -159,12 +159,12 @@ and isel_match isel1 sub vars isel2 =
(* extends substitution sub by creating a new substitution for vars *)
let sub_extend_with_ren (sub: Sil.subst) vars =
let sub_extend_with_ren (sub: Sil.exp_subst) vars =
let f id = (id, Exp.Var (Ident.create_fresh Ident.kprimed)) in
let renaming_for_vars = Sil.sub_of_list (List.map ~f vars) in
let renaming_for_vars = Sil.exp_subst_of_list (List.map ~f vars) in
Sil.sub_join sub renaming_for_vars
type sidecondition = Prop.normal Prop.t -> Sil.subst -> bool
type sidecondition = Prop.normal Prop.t -> Sil.exp_subst -> bool
let rec execute_with_backtracking = function
| [] -> None
@ -175,7 +175,7 @@ let rec execute_with_backtracking = function
| None -> execute_with_backtracking fs
| Some _ -> res_f
let rec instantiate_to_emp p condition sub vars = function
let rec instantiate_to_emp p condition (sub : Sil.exp_subst) vars = function
| [] -> if condition p sub then Some(sub, p) else None
| hpat:: hpats ->
if not hpat.flag then None
@ -184,7 +184,7 @@ let rec instantiate_to_emp p condition sub vars = function
| Sil.Hlseg (_, _, e1, e2, _) ->
let fully_instantiated = not (List.exists ~f:(fun id -> Sil.ident_in_exp id e1) vars)
in if (not fully_instantiated) then None else
let e1' = Sil.exp_sub sub e1
let e1' = Sil.exp_sub (`Exp sub) e1
in begin
match exp_match e1' sub vars e2 with
| None -> None
@ -195,8 +195,8 @@ let rec instantiate_to_emp p condition sub vars = function
let fully_instantiated =
not (List.exists ~f:(fun id -> Sil.ident_in_exp id iF || Sil.ident_in_exp id oB) vars)
in if (not fully_instantiated) then None else
let iF' = Sil.exp_sub sub iF in
let oB' = Sil.exp_sub sub oB
let iF' = Sil.exp_sub (`Exp sub) iF in
let oB' = Sil.exp_sub (`Exp sub) oB
in match exp_list_match [iF'; oB'] sub vars [oF; iB] with
| None -> None
| Some (sub_new, vars_leftover) ->
@ -293,7 +293,7 @@ let rec iter_match_with_impl tenv iter condition sub vars hpat hpats =
not (List.exists ~f:(fun id -> Sil.ident_in_exp id e_start2) vars) in
if (not fully_instantiated_start2) then None
else
let e_start2' = Sil.exp_sub sub e_start2 in
let e_start2' = Sil.exp_sub (`Exp sub) e_start2 in
match (exp_match e_start2' sub vars e_end2, hpats) with
| None, _ ->
(*
@ -350,8 +350,8 @@ let rec iter_match_with_impl tenv iter condition sub vars hpat hpats =
let fully_instantiated_iFoB2 =
not (List.exists ~f:(fun id -> Sil.ident_in_exp id iF2 || Sil.ident_in_exp id oB2) vars)
in if (not fully_instantiated_iFoB2) then None else
let iF2' = Sil.exp_sub sub iF2 in
let oB2' = Sil.exp_sub sub oB2
let iF2' = Sil.exp_sub (`Exp sub) iF2 in
let oB2' = Sil.exp_sub (`Exp sub) oB2
in match (exp_list_match [iF2'; oB2'] sub vars [oF2; iB2], hpats) with
| None, _ -> None
| Some (sub_new, vars_leftover), [] ->
@ -364,7 +364,7 @@ let rec iter_match_with_impl tenv iter condition sub vars hpat hpats =
let do_para_dllseg _ =
let fully_instantiated_iF2 = not (List.exists ~f:(fun id -> Sil.ident_in_exp id iF2) vars)
in if (not fully_instantiated_iF2) then None else
let iF2' = Sil.exp_sub sub iF2
let iF2' = Sil.exp_sub (`Exp sub) iF2
in match exp_match iF2' sub vars iB2 with
| None -> None
| Some (sub_new, vars_leftover) ->
@ -418,18 +418,18 @@ and hpara_common_match_with_impl tenv impl_ok ids1 sigma1 eids2 ids2 sigma2 =
let eids_fresh = List.map ~f:snd ren_eids in
let sub_eids = List.map ~f:(fun (id2, id1) -> (id2, Exp.Var id1)) ren_eids in
(sub_eids, eids_fresh) in
let sub = Sil.sub_of_list (sub_ids @ sub_eids) in
let sub = Sil.exp_subst_of_list (sub_ids @ sub_eids) in
match sigma2 with
| [] -> if List.is_empty sigma1 then true else false
| hpred2 :: sigma2 ->
let (hpat2, hpats2) =
let (hpred2_ren, sigma2_ren) = (Sil.hpred_sub sub hpred2, Prop.sigma_sub sub sigma2) in
let (hpred2_ren, sigma2_ren) = (Sil.hpred_sub (`Exp sub) hpred2, Prop.sigma_sub (`Exp sub) sigma2) in
let allow_impl hpred = { hpred = hpred; flag = impl_ok } in
(allow_impl hpred2_ren, List.map ~f:allow_impl sigma2_ren) in
let condition _ _ = true in
let p1 = Prop.normalize tenv (Prop.from_sigma sigma1) in
begin
match (prop_match_with_impl_sub tenv p1 condition Sil.sub_empty eids_fresh hpat2 hpats2) with
match (prop_match_with_impl_sub tenv p1 condition Sil.exp_sub_empty eids_fresh hpat2 hpats2) with
| None -> false
| Some (_, p1') when Prop.prop_is_emp p1' -> true
| _ -> false
@ -466,7 +466,7 @@ and hpara_dll_match_with_impl tenv impl_ok para1 para2 : bool =
2) [p |- (hpat.hpred * hpats.hpred)[subst] * p_leftover].
Using the flag [field], we can control the strength of |-. *)
let prop_match_with_impl tenv p condition vars hpat hpats =
prop_match_with_impl_sub tenv p condition Sil.sub_empty vars hpat hpats
prop_match_with_impl_sub tenv p condition Sil.exp_sub_empty vars hpat hpats
let sigma_remove_hpred eq sigma e =
let filter = function

4
infer/src/backend/match.mli
Unescape View File

@ -29,14 +29,14 @@ val pp_hpat : Pp.env -> Format.formatter -> hpred_pat -> unit
val pp_hpat_list : Pp.env -> Format.formatter -> hpred_pat list -> unit
type sidecondition = Prop.normal Prop.t -> Sil.subst -> bool
type sidecondition = Prop.normal Prop.t -> Sil.exp_subst -> bool
(** [prop_match_with_impl p condition vars hpat hpats]
returns [(subst, p_leftover)] such that
1) [dom(subst) = vars]
2) [p |- (hpat.hpred * hpats.hpred)[subst] * p_leftover].
Using the flag [field], we can control the strength of |-. *)
val prop_match_with_impl : Tenv.t -> Prop.normal Prop.t -> sidecondition -> Ident.t list -> hpred_pat -> hpred_pat list -> (Sil.subst * Prop.normal Prop.t) option
val prop_match_with_impl : Tenv.t -> Prop.normal Prop.t -> sidecondition -> Ident.t list -> hpred_pat -> hpred_pat list -> (Sil.exp_subst * Prop.normal Prop.t) option
(** [find_partial_iso] finds disjoint isomorphic sub-sigmas inside a given sigma.
The first argument is an equality checker.

92
infer/src/backend/prop.ml
Unescape View File

@ -44,7 +44,7 @@ module Core : sig
type 'a t = private
{
sigma: sigma; (** spatial part *)
sub: Sil.subst; (** substitution *)
sub: Sil.exp_subst; (** substitution *)
pi: pi; (** pure part *)
sigma_fp : sigma; (** abduced spatial part *)
pi_fp: pi; (** abduced pure part *)
@ -54,7 +54,7 @@ module Core : sig
val prop_emp : normal t
(** Set individual fields of the prop. *)
val set : ?sub:Sil.subst -> ?pi:pi -> ?sigma:sigma -> ?pi_fp:pi -> ?sigma_fp:sigma ->
val set : ?sub:Sil.exp_subst -> ?pi:pi -> ?sigma:sigma -> ?pi_fp:pi -> ?sigma_fp:sigma ->
'a t -> exposed t
(** Cast an exposed prop to a normalized one by just changing the type *)
@ -72,7 +72,7 @@ end = struct
type 'a t =
{
sigma: sigma; (** spatial part *)
sub: Sil.subst; (** substitution *)
sub: Sil.exp_subst; (** substitution *)
pi: pi; (** pure part *)
sigma_fp : sigma; (** abduced spatial part *)
pi_fp: pi; (** abduced pure part *)
@ -81,7 +81,7 @@ end = struct
(** Proposition [true /\ emp]. *)
let prop_emp : normal t =
{
sub = Sil.sub_empty;
sub = Sil.exp_sub_empty;
pi = [];
sigma = [];
pi_fp = [];
@ -152,7 +152,8 @@ let pp_hpred_stackvar pe0 f (hpred : Sil.hpred) =
Sil.color_post_wrapper changed pe0 f
(** Pretty print a substitution. *)
let pp_sub pe f sub =
let pp_sub pe f = function
| `Exp sub ->
let pi_sub = List.map ~f:(fun (id, e) -> Sil.Aeq (Var id, e)) (Sil.sub_to_list sub) in
(Pp.semicolon_seq_oneline pe (Sil.pp_atom pe)) f pi_sub
@ -411,19 +412,6 @@ let hpred_fav_in_pvars_add fav (hpred : Sil.hpred) = match hpred with
let sigma_fav_in_pvars_add fav sigma =
List.iter ~f:(hpred_fav_in_pvars_add fav) sigma
let sigma_fpv sigma =
List.concat_map ~f:Sil.hpred_fpv sigma
let pi_fpv pi =
List.concat_map ~f:Sil.atom_fpv pi
let prop_fpv prop =
(Sil.sub_fpv prop.sub) @
(pi_fpv prop.pi) @
(pi_fpv prop.pi_fp) @
(sigma_fpv prop.sigma_fp) @
(sigma_fpv prop.sigma)
(** {2 Functions for Subsitition} *)
let pi_sub (subst: Sil.subst) pi =
@ -1291,7 +1279,7 @@ module Normalize = struct
if atom_is_inequality a' then inequality_normalize tenv a' else a'
let normalize_and_strengthen_atom tenv (p : normal t) (a : Sil.atom) : Sil.atom =
let a' = atom_normalize tenv p.sub a in
let a' = atom_normalize tenv (`Exp p.sub) a in
match a' with
| Aeq (BinOp (Le, Var id, Const (Cint n)), Const (Cint i))
when IntLit.isone i ->
@ -1564,7 +1552,7 @@ module Normalize = struct
let ids_footprint =
List.map ~f:(fun id -> (id, Ident.create_fresh Ident.kfootprint)) ids_primed in
let ren_sub =
Sil.sub_of_list (List.map ~f:(fun (id1, id2) -> (id1, Exp.Var id2)) ids_footprint) in
Sil.subst_of_list (List.map ~f:(fun (id1, id2) -> (id1, Exp.Var id2)) ids_footprint) in
let nsigma' = sigma_normalize tenv Sil.sub_empty (sigma_sub ren_sub nsigma) in
let npi' = pi_normalize tenv Sil.sub_empty nsigma' (pi_sub ren_sub npi) in
(npi', nsigma') in
@ -1574,7 +1562,7 @@ module Normalize = struct
let sub_normalize sub =
let f (id, e) = (not (Ident.is_primed id)) && (not (Sil.ident_in_exp id e)) in
let sub' = Sil.sub_filter_pair ~f sub in
if Sil.equal_subst sub sub' then sub else sub'
if Sil.equal_exp_subst sub sub' then sub else sub'
(** Conjoin a pure atomic predicate by normal conjunction. *)
let rec prop_atom_and tenv ?(footprint=false) (p : normal t) a : normal t =
@ -1586,12 +1574,13 @@ module Normalize = struct
| Aeq (Var i, e) when Sil.ident_in_exp i e -> p
| Aeq (Var i, e) ->
let sub_list = [(i, e)] in
let mysub = Sil.sub_of_list sub_list in
let mysub = Sil.exp_subst_of_list sub_list in
let p_sub = Sil.sub_filter (fun i' -> not (Ident.equal i i')) p.sub in
let sub' = Sil.sub_join mysub (Sil.sub_range_map (Sil.exp_sub mysub) p_sub) in
let exp_sub' = Sil.sub_join mysub (Sil.sub_range_map (Sil.exp_sub (`Exp mysub)) p_sub) in
let sub' = `Exp exp_sub' in
let (nsub', npi', nsigma') =
let nsigma' = sigma_normalize tenv sub' p.sigma in
(sub_normalize sub', pi_normalize tenv sub' nsigma' p.pi, nsigma') in
(sub_normalize exp_sub', pi_normalize tenv sub' nsigma' p.pi, nsigma') in
let (eqs_zero, nsigma'') = sigma_remove_emptylseg nsigma' in
let p' =
unsafe_cast_to_normal
@ -1601,11 +1590,11 @@ module Normalize = struct
p
| Aneq (e1, e2) ->
let sigma' = sigma_intro_nonemptylseg e1 e2 p.sigma in
let pi' = pi_normalize tenv p.sub sigma' (a':: p.pi) in
let pi' = pi_normalize tenv (`Exp p.sub) sigma' (a':: p.pi) in
unsafe_cast_to_normal
(set p ~pi:pi' ~sigma:sigma')
| _ ->
let pi' = pi_normalize tenv p.sub p.sigma (a':: p.pi) in
let pi' = pi_normalize tenv (`Exp p.sub) p.sigma (a':: p.pi) in
unsafe_cast_to_normal
(set p ~pi:pi') in
if not footprint then p'
@ -1620,7 +1609,7 @@ module Normalize = struct
else
match a' with
| Aeq (Exp.Var i, e) when not (Sil.ident_in_exp i e) ->
let mysub = Sil.sub_of_list [(i, e)] in
let mysub = Sil.subst_of_list [(i, e)] in
let sigma_fp' = sigma_normalize tenv mysub p'.sigma_fp in
let pi_fp' = a' :: pi_normalize tenv mysub sigma_fp' p'.pi_fp in
footprint_normalize tenv
@ -1646,7 +1635,7 @@ end
(* End of module Normalize *)
let exp_normalize_prop tenv prop exp =
Config.run_with_abs_val_equal_zero (Normalize.exp_normalize tenv prop.sub) exp
Config.run_with_abs_val_equal_zero (Normalize.exp_normalize tenv (`Exp prop.sub)) exp
let lexp_normalize_prop tenv p lexp =
let root = Exp.root_of_lexp lexp in
@ -1662,19 +1651,19 @@ let lexp_normalize_prop tenv p lexp =
Sil.exp_add_offsets nroot noffsets
let atom_normalize_prop tenv prop atom =
Config.run_with_abs_val_equal_zero (Normalize.atom_normalize tenv prop.sub) atom
Config.run_with_abs_val_equal_zero (Normalize.atom_normalize tenv (`Exp prop.sub)) atom
let strexp_normalize_prop tenv prop strexp =
Config.run_with_abs_val_equal_zero (Normalize.strexp_normalize tenv prop.sub) strexp
Config.run_with_abs_val_equal_zero (Normalize.strexp_normalize tenv (`Exp prop.sub)) strexp
let hpred_normalize_prop tenv prop hpred =
Config.run_with_abs_val_equal_zero (Normalize.hpred_normalize tenv prop.sub) hpred
Config.run_with_abs_val_equal_zero (Normalize.hpred_normalize tenv (`Exp prop.sub)) hpred
let sigma_normalize_prop tenv prop sigma =
Config.run_with_abs_val_equal_zero (Normalize.sigma_normalize tenv prop.sub) sigma
Config.run_with_abs_val_equal_zero (Normalize.sigma_normalize tenv (`Exp prop.sub)) sigma
let pi_normalize_prop tenv prop pi =
Config.run_with_abs_val_equal_zero (Normalize.pi_normalize tenv prop.sub prop.sigma) pi
Config.run_with_abs_val_equal_zero (Normalize.pi_normalize tenv (`Exp prop.sub) prop.sigma) pi
let sigma_replace_exp tenv epairs sigma =
let sigma' = List.map ~f:(Sil.hpred_replace_exp epairs) sigma in
@ -1904,7 +1893,7 @@ let compute_reindexing fav_add get_id_offset list =
let exp_new : Exp.t = BinOp (PlusA, base_new, offset_new) in
(id, exp_new) in
let reindexing = List.map ~f:transform list_passed in
Sil.sub_of_list reindexing
Sil.exp_subst_of_list reindexing
let compute_reindexing_from_indices indices =
let get_id_offset (e : Exp.t) = match e with
@ -1914,11 +1903,12 @@ let compute_reindexing_from_indices indices =
let fav_add = Sil.exp_fav_add in
compute_reindexing fav_add get_id_offset indices
let apply_reindexing tenv subst prop =
let apply_reindexing tenv (exp_subst : Sil.exp_subst) prop =
let subst = (`Exp exp_subst) in
let nsigma = Normalize.sigma_normalize tenv subst prop.sigma in
let npi = Normalize.pi_normalize tenv subst nsigma prop.pi in
let nsub, atoms =
let dom_subst = List.map ~f:fst (Sil.sub_to_list subst) in
let dom_subst = List.map ~f:fst (Sil.sub_to_list exp_subst) in
let in_dom_subst id = List.exists ~f:(Ident.equal id) dom_subst in
let sub' = Sil.sub_filter (fun id -> not (in_dom_subst id)) prop.sub in
let contains_substituted_id e = Sil.fav_exists (Sil.exp_fav e) in_dom_subst in
@ -2131,8 +2121,8 @@ let prop_sub subst (prop: 'a t) : exposed t =
set prop_emp ~pi ~sigma ~pi_fp ~sigma_fp
(** Apply renaming substitution to a proposition. *)
let prop_ren_sub tenv (ren_sub: Sil.subst) (prop: normal t) : normal t =
Normalize.normalize tenv (prop_sub ren_sub prop)
let prop_ren_sub tenv (ren_sub: Sil.exp_subst) (prop: normal t) : normal t =
Normalize.normalize tenv (prop_sub (`Exp ren_sub) prop)
(** Existentially quantify the [fav] in [prop].
[fav] should not contain any primed variables. *)
@ -2141,12 +2131,12 @@ let exist_quantify tenv fav (prop : normal t) : normal t =
if List.exists ~f:Ident.is_primed ids then assert false; (* sanity check *)
if List.is_empty ids then prop else
let gen_fresh_id_sub id = (id, Exp.Var (Ident.create_fresh Ident.kprimed)) in
let ren_sub = Sil.sub_of_list (List.map ~f:gen_fresh_id_sub ids) in
let ren_sub = Sil.exp_subst_of_list (List.map ~f:gen_fresh_id_sub ids) in
let prop' =
(* throw away x=E if x becomes _x *)
let mem_idlist i = List.exists ~f:(fun id -> Ident.equal i id) in
let sub = Sil.sub_filter (fun i -> not (mem_idlist i ids)) prop.sub in
if Sil.equal_subst sub prop.sub then prop
if Sil.equal_exp_subst sub prop.sub then prop
else unsafe_cast_to_normal (set prop ~sub) in
(*
L.out "@[<2>.... Existential Quantification ....@\n";
@ -2169,7 +2159,7 @@ let prop_expmap (fe: Exp.t -> Exp.t) prop =
let vars_make_unprimed tenv fav prop =
let ids = Sil.fav_to_list fav in
let ren_sub =
Sil.sub_of_list (List.map
Sil.exp_subst_of_list (List.map
~f:(fun i -> (i, Exp.Var (Ident.create_fresh Ident.knormal)))
ids) in
prop_ren_sub tenv ren_sub prop
@ -2198,7 +2188,7 @@ let prop_rename_fav_with_existentials tenv (p : normal t) : normal t =
prop_fav_add fav p;
let ids = Sil.fav_to_list fav in
let ids' = List.map ~f:(fun i -> (i, Ident.create_fresh Ident.kprimed)) ids in
let ren_sub = Sil.sub_of_list (List.map ~f:(fun (i, i') -> (i, Exp.Var i')) ids') in
let ren_sub = Sil.subst_of_list (List.map ~f:(fun (i, i') -> (i, Exp.Var i')) ids') in
let p' = prop_sub ren_sub p in
(*L.d_strln "Prop after renaming:"; d_prop p'; L.d_strln "";*)
Normalize.normalize tenv p'
@ -2220,7 +2210,7 @@ let remove_seed_captured_vars_block tenv captured_vars prop =
(** Iterator state over sigma. *)
type 'a prop_iter =
{ pit_sub : Sil.subst; (** substitution for equalities *)
{ pit_sub : Sil.exp_subst; (** substitution for equalities *)
pit_pi : pi; (** pure part *)
pit_newpi : (bool * Sil.atom) list; (** newly added atoms. *)
(* The first records !Config.footprint. *)
@ -2272,7 +2262,7 @@ let prop_iter_add_atom footprint iter atom =
associated to the resulting iterator *)
let prop_iter_remove_curr_then_to_prop tenv iter : normal t =
let sigma = List.rev_append iter.pit_old iter.pit_new in
let normalized_sigma = Normalize.sigma_normalize tenv iter.pit_sub sigma in
let normalized_sigma = Normalize.sigma_normalize tenv (`Exp iter.pit_sub) sigma in
let prop =
set prop_emp
~sub:iter.pit_sub
@ -2284,7 +2274,7 @@ let prop_iter_remove_curr_then_to_prop tenv iter : normal t =
(** Return the current hpred and state. *)
let prop_iter_current tenv iter =
let curr = Normalize.hpred_normalize tenv iter.pit_sub iter.pit_curr in
let curr = Normalize.hpred_normalize tenv (`Exp iter.pit_sub) iter.pit_curr in
let prop =
unsafe_cast_to_normal
(set prop_emp ~sigma:[curr]) in
@ -2349,7 +2339,7 @@ let prop_iter_set_state iter state =
let prop_iter_make_id_primed tenv id iter =
let pid = Ident.create_fresh Ident.kprimed in
let sub_id = Sil.sub_of_list [(id, Exp.Var pid)] in
let sub_id = Sil.subst_of_list [(id, Exp.Var pid)] in
let normalize (id, e) =
let eq' : Sil.atom = Aeq (Sil.exp_sub sub_id (Var id), Sil.exp_sub sub_id e) in
@ -2385,16 +2375,16 @@ let prop_iter_make_id_primed tenv id iter =
let pairs_unpid, pairs_pid = split [] [] eqs in
match pairs_pid with
| [] ->
let sub_unpid = Sil.sub_of_list pairs_unpid in
let sub_unpid = Sil.exp_subst_of_list pairs_unpid in
let pairs = (id, Exp.Var pid) :: pairs_unpid in
sub_unpid, Sil.sub_of_list pairs, []
sub_unpid, Sil.subst_of_list pairs, []
| (id1, e1):: _ ->
let sub_id1 = Sil.sub_of_list [(id1, e1)] in
let sub_id1 = Sil.subst_of_list [(id1, e1)] in
let pairs_unpid' =
List.map ~f:(fun (id', e') -> (id', Sil.exp_sub sub_id1 e')) pairs_unpid in
let sub_unpid = Sil.sub_of_list pairs_unpid' in
let sub_unpid = Sil.exp_subst_of_list pairs_unpid' in
let pairs = (id, e1) :: pairs_unpid' in
sub_unpid, Sil.sub_of_list pairs, get_eqs [] pairs_pid in
sub_unpid, Sil.subst_of_list pairs, get_eqs [] pairs_pid in
let nsub_new = Normalize.sub_normalize sub_new in
{ iter with

7
infer/src/backend/prop.mli
Unescape View File

@ -27,7 +27,7 @@ type sigma = Sil.hpred list
type 'a t = private
{
sigma: sigma; (** spatial part *)
sub: Sil.subst; (** substitution *)
sub: Sil.exp_subst; (** substitution *)
pi: pi; (** pure part *)
sigma_fp : sigma; (** abduced spatial part *)
pi_fp: pi; (** abduced pure part *)
@ -128,9 +128,6 @@ val prop_fav_nonpure : normal t -> fav
(** Find fav of the footprint part of the prop *)
val prop_footprint_fav : 'a t -> fav
(** Compute all the free program variables in the prop *)
val prop_fpv: 'a t -> Pvar.t list
(** Apply substitution for pi *)
val pi_sub : subst -> atom list -> atom list
@ -304,7 +301,7 @@ val from_pi : pi -> exposed t
val from_sigma : sigma -> exposed t
(** Set individual fields of the prop. *)
val set : ?sub:Sil.subst -> ?pi:pi -> ?sigma:sigma -> ?pi_fp:pi -> ?sigma_fp:sigma ->
val set : ?sub:Sil.exp_subst -> ?pi:pi -> ?sigma:sigma -> ?pi_fp:pi -> ?sigma_fp:sigma ->
'a t -> exposed t
(** Rename free variables in a prop replacing them with existentially quantified vars *)

100
infer/src/backend/prover.ml
Unescape View File

@ -939,7 +939,7 @@ let check_inconsistency_pi tenv pi =
(** {2 Abduction prover} *)
type subst2 = Sil.subst * Sil.subst
type subst2 = Sil.exp_subst * Sil.exp_subst
type exc_body =
| EXC_FALSE
@ -1089,7 +1089,7 @@ end = struct
end
let d_missing sub = (* optional print of missing: if print something, prepend with newline *)
if !missing_pi <> [] || !missing_sigma <> [] || !missing_fld <> [] || !missing_typ <> [] || Sil.sub_to_list sub <> [] then
if !missing_pi <> [] || !missing_sigma <> [] || !missing_fld <> [] || !missing_typ <> [] || not (Sil.is_sub_empty sub) then
begin
L.d_ln ();
L.d_str "[";
@ -1153,21 +1153,23 @@ end = struct
L.d_ln ()
end
let d_impl = ProverState.d_implication
let d_impl_err = ProverState.d_implication_error
let d_impl (s1, s2) = ProverState.d_implication (`Exp s1, `Exp s2)
let d_impl_err (arg1, (s1, s2), arg3) =
ProverState.d_implication_error (arg1, (`Exp s1, `Exp s2), arg3)
(** extend a substitution *)
let extend_sub sub v e =
let new_sub = Sil.sub_of_list [v, e] in
Sil.sub_join new_sub (Sil.sub_range_map (Sil.exp_sub new_sub) sub)
let new_exp_sub = Sil.exp_subst_of_list [v, e] in
let new_sub = `Exp new_exp_sub in
Sil.sub_join new_exp_sub (Sil.sub_range_map (Sil.exp_sub new_sub) sub)
(** Extend [sub1] and [sub2] to witnesses that each instance of
[e1[sub1]] is an instance of [e2[sub2]]. Raise IMPL_FALSE if not
possible. *)
let exp_imply tenv calc_missing subs e1_in e2_in : subst2 =
let e1 = Prop.exp_normalize_noabs tenv (fst subs) e1_in in
let e2 = Prop.exp_normalize_noabs tenv (snd subs) e2_in in
let var_imply subs v1 v2 : subst2 =
let exp_imply tenv calc_missing (subs : subst2) e1_in e2_in : subst2 =
let e1 = Prop.exp_normalize_noabs tenv (`Exp (fst subs)) e1_in in
let e2 = Prop.exp_normalize_noabs tenv (`Exp (snd subs)) e2_in in
let var_imply (subs : subst2) v1 v2 : subst2 =
match Ident.is_primed v1, Ident.is_primed v2 with
| false, false ->
if Ident.equal v1 v2 then subs
@ -1178,7 +1180,7 @@ let exp_imply tenv calc_missing subs e1_in e2_in : subst2 =
else raise (IMPL_EXC ("exps", subs, (EXC_FALSE_EXPS (e1, e2))))
| true, false -> raise (IMPL_EXC ("exps", subs, (EXC_FALSE_EXPS (e1, e2))))
| false, true ->
let sub2' = extend_sub (snd subs) v2 (Sil.exp_sub (fst subs) (Exp.Var v1)) in
let sub2' = extend_sub (snd subs) v2 (Sil.exp_sub (`Exp (fst subs)) (Exp.Var v1)) in
(fst subs, sub2')
| true, true ->
let v1' = Ident.create_fresh Ident.knormal in
@ -1328,7 +1330,7 @@ let rec sexp_imply tenv source calc_index_frame calc_missing subs se1 se2 typ2 :
subs', fld_frame_opt, fld_missing_opt
| Sil.Estruct _, Sil.Eexp (e2, _) ->
begin
let e2' = Sil.exp_sub (snd subs) e2 in
let e2' = Sil.exp_sub (`Exp (snd subs)) e2 in
match e2' with
| Exp.Var id2 when Ident.is_primed id2 ->
let id2' = Ident.create_fresh Ident.knormal in
@ -1418,8 +1420,8 @@ and array_imply tenv source calc_index_frame calc_missing subs esel1 esel2 typ2
match esel1, esel2 with
| _,[] -> subs, esel1, []
| (e1, se1) :: esel1', (e2, se2) :: esel2' ->
let e1n = Prop.exp_normalize_noabs tenv (fst subs) e1 in
let e2n = Prop.exp_normalize_noabs tenv (snd subs) e2 in
let e1n = Prop.exp_normalize_noabs tenv (`Exp (fst subs)) e1 in
let e2n = Prop.exp_normalize_noabs tenv (`Exp (snd subs)) e2 in
let n = Exp.compare e1n e2n in
if n < 0 then array_imply tenv source calc_index_frame calc_missing subs esel1' esel2 typ2
else if n > 0 then array_imply tenv source calc_index_frame calc_missing subs esel1 esel2' typ2
@ -1433,10 +1435,10 @@ and array_imply tenv source calc_index_frame calc_missing subs esel1 esel2 typ2
let index_missing' = (e2, se2) :: index_missing in
subs'', index_frame, index_missing'
and sexp_imply_nolhs tenv source calc_missing subs se2 typ2 =
and sexp_imply_nolhs tenv source calc_missing (subs : subst2) se2 typ2 =
match se2 with
| Sil.Eexp (_e2, _) ->
let e2 = Sil.exp_sub (snd subs) _e2 in
let e2 = Sil.exp_sub (`Exp (snd subs)) _e2 in
begin
match e2 with
| Exp.Var v2 when Ident.is_primed v2 ->
@ -1476,7 +1478,7 @@ let filter_ne_lhs sub e0 = function
else None
| _ -> None
let filter_hpred sub hpred2 hpred1 = match (Sil.hpred_sub sub hpred1), hpred2 with
let filter_hpred sub hpred2 hpred1 = match (Sil.hpred_sub (`Exp sub) hpred1), hpred2 with
| Sil.Hlseg(Sil.Lseg_NE, hpara1, e1, f1, el1), Sil.Hlseg(Sil.Lseg_PE, _, _, _, _) ->
if Sil.equal_hpred (Sil.Hlseg(Sil.Lseg_PE, hpara1, e1, f1, el1)) hpred2 then Some false else None
| Sil.Hlseg(Sil.Lseg_PE, hpara1, e1, f1, el1), Sil.Hlseg(Sil.Lseg_NE, _, _, _, _) ->
@ -1507,9 +1509,9 @@ let hpred_has_primed_lhs sub hpred =
let move_primed_lhs_from_front subs sigma = match sigma with
| [] -> sigma
| hpred:: _ ->
if hpred_has_primed_lhs (snd subs) hpred then
if hpred_has_primed_lhs (`Exp (snd subs)) hpred then
let (sigma_primed, sigma_unprimed) =
List.partition_tf ~f:(hpred_has_primed_lhs (snd subs)) sigma
List.partition_tf ~f:(hpred_has_primed_lhs (`Exp (snd subs))) sigma
in match sigma_unprimed with
| [] -> raise (IMPL_EXC ("every hpred has primed lhs, cannot proceed", subs, (EXC_FALSE_SIGMA sigma)))
| _:: _ -> sigma_unprimed @ sigma_primed
@ -1799,7 +1801,7 @@ let handle_parameter_subtype tenv prop1 sigma2 subs (e1, se1, texp1) (se2, texp2
let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2 : subst2 * Prop.normal Prop.t = match hpred2 with
| Sil.Hpointsto (_e2, se2, texp2) ->
let e2 = Sil.exp_sub (snd subs) _e2 in
let e2 = Sil.exp_sub (`Exp (snd subs)) _e2 in
let _ = match e2 with
| Exp.Lvar _ -> ()
| Exp.Var v -> if Ident.is_primed v then
@ -1809,7 +1811,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
(match Prop.prop_iter_create prop1 with
| None -> raise (IMPL_EXC ("lhs is empty", subs, EXC_FALSE))
| Some iter1 ->
(match Prop.prop_iter_find iter1 (filter_ne_lhs (fst subs) e2) with
(match Prop.prop_iter_find iter1 (filter_ne_lhs (`Exp (fst subs)) e2) with
| None -> raise (IMPL_EXC ("lhs does not have e|->", subs, (EXC_FALSE_HPRED hpred2)))
| Some iter1' ->
(match Prop.prop_iter_current tenv iter1' with
@ -1856,7 +1858,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
L.d_decrease_indent 1;
res
| Sil.Hdllseg (Sil.Lseg_NE, para1, iF1, oB1, oF1, iB1, elist1), _
when Exp.equal (Sil.exp_sub (fst subs) iF1) e2 -> (* Unroll dllseg forward *)
when Exp.equal (Sil.exp_sub (`Exp (fst subs)) iF1) e2 -> (* Unroll dllseg forward *)
let n' = Exp.Var (Ident.create_fresh Ident.kprimed) in
let (_, para_inst1) = Sil.hpara_dll_instantiate para1 iF1 oB1 n' elist1 in
let hpred_list1 = para_inst1@[Prop.mk_dllseg tenv Sil.Lseg_PE para1 n' iF1 oF1 iB1 elist1] in
@ -1868,7 +1870,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
L.d_decrease_indent 1;
res
| Sil.Hdllseg (Sil.Lseg_NE, para1, iF1, oB1, oF1, iB1, elist1), _
when Exp.equal (Sil.exp_sub (fst subs) iB1) e2 -> (* Unroll dllseg backward *)
when Exp.equal (Sil.exp_sub (`Exp (fst subs)) iB1) e2 -> (* Unroll dllseg backward *)
let n' = Exp.Var (Ident.create_fresh Ident.kprimed) in
let (_, para_inst1) = Sil.hpara_dll_instantiate para1 iB1 n' oF1 elist1 in
let hpred_list1 = para_inst1@[Prop.mk_dllseg tenv Sil.Lseg_PE para1 iF1 oB1 iB1 n' elist1] in
@ -1884,7 +1886,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
)
)
| Sil.Hlseg (k, para2, _e2, _f2, _elist2) -> (* for now ignore implications between PE and NE *)
let e2, f2 = Sil.exp_sub (snd subs) _e2, Sil.exp_sub (snd subs) _f2 in
let e2, f2 = Sil.exp_sub (`Exp (snd subs)) _e2, Sil.exp_sub (`Exp (snd subs)) _f2 in
let _ = match e2 with
| Exp.Lvar _ -> ()
| Exp.Var v -> if Ident.is_primed v then
@ -1897,9 +1899,9 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
(match Prop.prop_iter_create prop1 with
| None -> raise (IMPL_EXC ("lhs is empty", subs, EXC_FALSE))
| Some iter1 ->
(match Prop.prop_iter_find iter1 (filter_hpred (fst subs) (Sil.hpred_sub (snd subs) hpred2)) with
(match Prop.prop_iter_find iter1 (filter_hpred (fst subs) (Sil.hpred_sub (`Exp (snd subs)) hpred2)) with
| None ->
let elist2 = List.map ~f:(fun e -> Sil.exp_sub (snd subs) e) _elist2 in
let elist2 = List.map ~f:(fun e -> Sil.exp_sub (`Exp (snd subs)) e) _elist2 in
let _, para_inst2 = Sil.hpara_instantiate para2 e2 f2 elist2 in
L.d_increase_indent 1;
let res =
@ -1909,7 +1911,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
L.d_decrease_indent 1;
res
| Some iter1' ->
let elist2 = List.map ~f:(fun e -> Sil.exp_sub (snd subs) e) _elist2 in
let elist2 = List.map ~f:(fun e -> Sil.exp_sub (`Exp (snd subs)) e) _elist2 in
(* force instantiation of existentials *)
let subs' = exp_list_imply tenv calc_missing subs (f2:: elist2) (f2:: elist2) in
let prop1' = Prop.prop_iter_remove_curr_then_to_prop tenv iter1' in
@ -1944,8 +1946,8 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
raise (Exceptions.Abduction_case_not_implemented __POS__))
| Sil.Hdllseg (_, para2, iF2, oB2, oF2, iB2, elist2) ->
(* for now ignore implications between PE and NE *)
let iF2, oF2 = Sil.exp_sub (snd subs) iF2, Sil.exp_sub (snd subs) oF2 in
let iB2, oB2 = Sil.exp_sub (snd subs) iB2, Sil.exp_sub (snd subs) oB2 in
let iF2, oF2 = Sil.exp_sub (`Exp (snd subs)) iF2, Sil.exp_sub (`Exp (snd subs)) oF2 in
let iB2, oB2 = Sil.exp_sub (`Exp (snd subs)) iB2, Sil.exp_sub (`Exp (snd subs)) oB2 in
let _ = match oF2 with
| Exp.Lvar _ -> ()
| Exp.Var v -> if Ident.is_primed v then
@ -1963,9 +1965,9 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
(match Prop.prop_iter_create prop1 with
| None -> raise (IMPL_EXC ("lhs is empty", subs, EXC_FALSE))
| Some iter1 ->
(match Prop.prop_iter_find iter1 (filter_hpred (fst subs) (Sil.hpred_sub (snd subs) hpred2)) with
(match Prop.prop_iter_find iter1 (filter_hpred (fst subs) (Sil.hpred_sub (`Exp (snd subs)) hpred2)) with
| None ->
let elist2 = List.map ~f:(fun e -> Sil.exp_sub (snd subs) e) elist2 in
let elist2 = List.map ~f:(fun e -> Sil.exp_sub (`Exp (snd subs)) e) elist2 in
let _, para_inst2 =
if Exp.equal iF2 iB2 then
Sil.hpara_dll_instantiate para2 iF2 oB2 oF2 elist2
@ -1978,7 +1980,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
L.d_decrease_indent 1;
res
| Some iter1' -> (* Only consider implications between identical listsegs for now *)
let elist2 = List.map ~f:(fun e -> Sil.exp_sub (snd subs) e) elist2 in
let elist2 = List.map ~f:(fun e -> Sil.exp_sub (`Exp (snd subs)) e) elist2 in
(* force instantiation of existentials *)
let subs' =
exp_list_imply tenv calc_missing subs
@ -1995,7 +1997,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : (subst2 * Prop.normal Prop.t) =
let is_constant_string_class subs = function (* if the hpred represents a constant string, return the string *)
| Sil.Hpointsto (_e2, _, _) ->
let e2 = Sil.exp_sub (snd subs) _e2 in
let e2 = Sil.exp_sub (`Exp (snd subs)) _e2 in
(match e2 with
| Exp.Const (Const.Cstr s) -> Some (s, true)
| Exp.Const (Const.Cclass c) -> Some (Ident.name_to_string c, false)
@ -2087,7 +2089,7 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : (subst2 *
res in
(match hpred2 with
| Sil.Hpointsto(_e2, se2, t) ->
let changed, calc_index_frame', hpred2' = expand_hpred_pointer tenv calc_index_frame (Sil.Hpointsto (Prop.exp_normalize_noabs tenv (snd subs) _e2, se2, t)) in
let changed, calc_index_frame', hpred2' = expand_hpred_pointer tenv calc_index_frame (Sil.Hpointsto (Prop.exp_normalize_noabs tenv (`Exp (snd subs)) _e2, se2, t)) in
if changed
then sigma_imply tenv calc_index_frame' calc_missing subs prop1 (hpred2' :: sigma2') (* calc_index_frame=true *)
else normal_case hpred2'
@ -2099,14 +2101,14 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : (subst2 *
subs, prop1
let prepare_prop_for_implication tenv (_, sub2) pi1 sigma1 =
let pi1' = (Prop.pi_sub sub2 (ProverState.get_missing_pi ())) @ pi1 in
let sigma1' = (Prop.sigma_sub sub2 (ProverState.get_missing_sigma ())) @ sigma1 in
let pi1' = (Prop.pi_sub (`Exp sub2) (ProverState.get_missing_pi ())) @ pi1 in
let sigma1' = (Prop.sigma_sub (`Exp sub2) (ProverState.get_missing_sigma ())) @ sigma1 in
let ep = Prop.set Prop.prop_emp ~sub:sub2 ~sigma:sigma1' ~pi:pi1' in
Prop.normalize tenv ep
let imply_pi tenv calc_missing (sub1, sub2) prop pi2 =
let do_atom a =
let a' = Sil.atom_sub sub2 a in
let a' = Sil.atom_sub (`Exp sub2) a in
try
if not (check_atom tenv prop a')
then raise (IMPL_EXC ("rhs atom missing in lhs", (sub1, sub2), (EXC_FALSE_ATOM a')))
@ -2122,11 +2124,11 @@ let imply_atom tenv calc_missing (sub1, sub2) prop a =
(** Check pure implications before looking at the spatial part. Add
necessary instantiations for equalities and check that instantiations
are possible for disequalities. *)
let rec pre_check_pure_implication tenv calc_missing subs pi1 pi2 =
let rec pre_check_pure_implication tenv calc_missing (subs : subst2) pi1 pi2 =
match pi2 with
| [] -> subs
| (Sil.Aeq (e2_in, f2_in) as a) :: pi2' when not (Prop.atom_is_inequality a) ->
let e2, f2 = Sil.exp_sub (snd subs) e2_in, Sil.exp_sub (snd subs) f2_in in
let e2, f2 = Sil.exp_sub (`Exp (snd subs)) e2_in, Sil.exp_sub (`Exp (snd subs)) f2_in in
if Exp.equal e2 f2 then pre_check_pure_implication tenv calc_missing subs pi1 pi2'
else
(match e2, f2 with
@ -2141,7 +2143,7 @@ let rec pre_check_pure_implication tenv calc_missing subs pi1 pi2 =
let sub2' = extend_sub (snd subs) v2 e2 in
pre_check_pure_implication tenv calc_missing (fst subs, sub2') pi1 pi2'
| _ ->
let pi1' = Prop.pi_sub (fst subs) pi1 in
let pi1' = Prop.pi_sub (`Exp (fst subs)) pi1 in
let prop_for_impl = prepare_prop_for_implication tenv subs pi1' [] in
imply_atom tenv calc_missing subs prop_for_impl (Sil.Aeq (e2_in, f2_in));
pre_check_pure_implication tenv calc_missing subs pi1 pi2'
@ -2149,7 +2151,7 @@ let rec pre_check_pure_implication tenv calc_missing subs pi1 pi2 =
| (Sil.Aneq (e, _) | Apred (_, e :: _) | Anpred (_, e :: _)) :: _
when not calc_missing && (match e with Var v -> not (Ident.is_primed v) | _ -> true) ->
raise (IMPL_EXC ("ineq e2=f2 in rhs with e2 not primed var",
(Sil.sub_empty, Sil.sub_empty), EXC_FALSE))
(Sil.exp_sub_empty, Sil.exp_sub_empty), EXC_FALSE))
| (Sil.Aeq _ | Aneq _ | Apred _ | Anpred _) :: pi2' ->
pre_check_pure_implication tenv calc_missing subs pi1 pi2'
@ -2167,15 +2169,15 @@ let check_array_bounds tenv (sub1, sub2) prop =
if check_atom tenv prop lt_ineq then check_failed lt_ineq in
let check_bound = function
| ProverState.BClen_imply (len1_, len2_, _indices2) ->
let len1 = Sil.exp_sub sub1 len1_ in
let len2 = Sil.exp_sub sub2 len2_ in
let len1 = Sil.exp_sub (`Exp sub1) len1_ in
let len2 = Sil.exp_sub (`Exp sub2) len2_ in
(* L.d_strln_color Orange "check_bound ";
Sil.d_exp len1; L.d_str " "; Sil.d_exp len2; L.d_ln(); *)
let indices_to_check = match len2 with
| _ -> [Exp.BinOp(Binop.PlusA, len2, Exp.minus_one)] (* only check len *) in
List.iter ~f:(fail_if_le len1) indices_to_check
| ProverState.BCfrom_pre _atom ->
let atom_neg = atom_negate tenv (Sil.atom_sub sub2 _atom) in
let atom_neg = atom_negate tenv (Sil.atom_sub (`Exp sub2) _atom) in
(* L.d_strln_color Orange "BCFrom_pre"; Sil.d_atom atom_neg; L.d_ln (); *)
if check_atom tenv prop atom_neg then check_failed atom_neg in
List.iter ~f:check_bound (ProverState.get_bounds_checks ())
@ -2204,12 +2206,12 @@ let check_implication_base pname tenv check_frame_empty calc_missing prop1 prop2
then (L.d_str "pi2 bounds checks: "; Prop.d_pi pi2_bcheck; L.d_ln ());
L.d_strln "returns";
L.d_strln "sub1: ";
L.d_increase_indent 1; Prop.d_sub (fst subs); L.d_decrease_indent 1; L.d_ln ();
L.d_increase_indent 1; Prop.d_sub (`Exp (fst subs)); L.d_decrease_indent 1; L.d_ln ();
L.d_strln "sub2: ";
L.d_increase_indent 1; Prop.d_sub (snd subs); L.d_decrease_indent 1; L.d_ln ();
L.d_increase_indent 1; Prop.d_sub (`Exp (snd subs)); L.d_decrease_indent 1; L.d_ln ();
let (sub1, sub2), frame_prop = sigma_imply tenv false calc_missing subs prop1 sigma2 in
let pi1' = Prop.pi_sub sub1 pi1 in
let sigma1' = Prop.sigma_sub sub1 sigma1 in
let pi1' = Prop.pi_sub (`Exp sub1) pi1 in
let sigma1' = Prop.sigma_sub (`Exp sub1) sigma1 in
L.d_ln ();
let prop_for_impl = prepare_prop_for_implication tenv (sub1, sub2) pi1' sigma1' in
(* only deal with pi2 without bound checks *)
@ -2235,7 +2237,7 @@ let check_implication_base pname tenv check_frame_empty calc_missing prop1 prop2
type implication_result =
| ImplOK of
(check list * Sil.subst * Sil.subst * Sil.hpred list * (Sil.atom list) * (Sil.hpred list) *
(check list * Sil.exp_subst * Sil.exp_subst * Sil.hpred list * (Sil.atom list) * (Sil.hpred list) *
(Sil.hpred list) * (Sil.hpred list) * ((Exp.t * Exp.t) list) * ((Exp.t * Exp.t) list))
| ImplFail of check list

5
infer/src/backend/prover.mli
Unescape View File

@ -77,7 +77,7 @@ val d_typings : (Exp.t * Exp.t) list -> unit
type implication_result =
| ImplOK of
(check list * Sil.subst * Sil.subst * Sil.hpred list * (Sil.atom list) * (Sil.hpred list) *
(check list * Sil.exp_subst * Sil.exp_subst * Sil.hpred list * (Sil.atom list) * (Sil.hpred list) *
(Sil.hpred list) * (Sil.hpred list) * ((Exp.t * Exp.t) list) * ((Exp.t * Exp.t) list))
| ImplFail of check list
@ -113,6 +113,3 @@ sig
end
val get_overrides_of : Tenv.t -> Typ.t -> Typ.Procname.t -> (Typ.t * Typ.Procname.t) list

2
infer/src/backend/rearrange.ml
Unescape View File

@ -464,7 +464,7 @@ let mk_ptsto_exp_footprint
(atoms, Prop.mk_ptsto tenv root se
(Exp.Sizeof {typ; nbytes=None; dynamic_length=None; subtype})) in
let atoms, ptsto_foot = create_ptsto true off_foot in
let sub = Sil.sub_of_list eqs in
let sub = Sil.subst_of_list eqs in
let ptsto = Sil.hpred_sub sub ptsto_foot in
let atoms' = List.map ~f:(fun (id, e) -> Prop.mk_eq tenv (Exp.Var id) e) eqs in
(ptsto, ptsto_foot, atoms @ atoms')

2
infer/src/backend/specs.ml
Unescape View File

@ -199,7 +199,7 @@ end = struct
let idlist = Sil.fav_to_list fav in
let count = ref 0 in
let sub =
Sil.sub_of_list (List.map ~f:(fun id ->
Sil.subst_of_list (List.map ~f:(fun id ->
incr count; (id, Exp.Var (Ident.create_normal Ident.name_spec !count))) idlist) in
spec_sub tenv sub spec

4
infer/src/backend/state.ml
Unescape View File

@ -157,7 +157,7 @@ let instrs_normalize instrs =
let gensym id =
incr count;
Ident.set_stamp id !count in
Sil.sub_of_list (List.map ~f:(fun id -> (id, Exp.Var (gensym id))) bound_ids) in
Sil.subst_of_list (List.map ~f:(fun id -> (id, Exp.Var (gensym id))) bound_ids) in
List.map ~f:(Sil.instr_sub subst) instrs
(** Create a function to find duplicate nodes.
@ -253,7 +253,7 @@ let extract_pre p tenv pdesc abstract_fun =
let fav = Prop.prop_fav p in
let idlist = Sil.fav_to_list fav in
let count = ref 0 in
Sil.sub_of_list (List.map ~f:(fun id ->
Sil.subst_of_list (List.map ~f:(fun id ->
incr count; (id, Exp.Var (Ident.create_normal Ident.name_spec !count))) idlist) in
let _, p' = PropUtil.remove_locals_formals tenv pdesc p in
let pre, _ = Prop.extract_spec p' in

2
infer/src/backend/symExec.ml
Unescape View File

@ -1631,7 +1631,7 @@ and sym_exec_wrapper handle_exn tenv pdesc instr ((prop: Prop.normal Prop.t), pa
let ids_primed_normal =
List.map ~f:(fun id -> (id, Ident.create_fresh Ident.knormal)) ids_primed in
let ren_sub =
Sil.sub_of_list (List.map
Sil.subst_of_list (List.map
~f:(fun (id1, id2) -> (id1, Exp.Var id2)) ids_primed_normal) in
let p' = Prop.normalize tenv (Prop.prop_sub ren_sub p) in
let fav_normal = Sil.fav_from_list (List.map ~f:snd ids_primed_normal) in

22
infer/src/backend/tabulation.ml
Unescape View File

@ -107,7 +107,7 @@ let spec_rename_vars pname spec =
List.iter ~f:(fun (p, _) -> Prop.prop_fav_add fav p) spec.Specs.posts;
let ids = Sil.fav_to_list fav in
let ids' = List.map ~f:(fun i -> (i, Ident.create_fresh Ident.kprimed)) ids in
let ren_sub = Sil.sub_of_list (List.map ~f:(fun (i, i') -> (i, Exp.Var i')) ids') in
let ren_sub = Sil.subst_of_list (List.map ~f:(fun (i, i') -> (i, Exp.Var i')) ids') in
let pre' = Specs.Jprop.jprop_sub ren_sub spec.Specs.pre in
let posts' = List.map ~f:(fun (p, path) -> (Prop.prop_sub ren_sub p, path)) spec.Specs.posts in
let pre'' = jprop_add_callee_suffix pre' in
@ -163,7 +163,7 @@ let process_splitting
List.map
~f:(function (id, Exp.Var id') -> (id', Exp.Var id) | _ -> assert false)
sub1_list'
in Sil.sub_of_list_duplicates sub1_inverse_list in
in Sil.exp_subst_of_list_duplicates sub1_inverse_list in
let fav_actual_pre =
let fav_sub2 = (* vars which represent expansions of fields *)
let fav = Sil.fav_new () in
@ -175,15 +175,15 @@ let process_splitting
Sil.ident_list_fav_add (Sil.fav_to_list fav_sub2) fav_pre;
fav_pre in
let fav_missing = Prop.sigma_fav (Prop.sigma_sub sub missing_sigma) in
Prop.pi_fav_add fav_missing (Prop.pi_sub sub missing_pi);
let fav_missing = Prop.sigma_fav (Prop.sigma_sub (`Exp sub) missing_sigma) in
Prop.pi_fav_add fav_missing (Prop.pi_sub (`Exp sub) missing_pi);
let fav_missing_primed =
let filter id = Ident.is_primed id && not (Sil.fav_mem fav_actual_pre id)
in Sil.fav_copy_filter_ident fav_missing filter in
let fav_missing_fld = Prop.sigma_fav (Prop.sigma_sub sub missing_fld) in
let fav_missing_fld = Prop.sigma_fav (Prop.sigma_sub (`Exp sub) missing_fld) in
let map_var_to_pre_var_or_fresh id =
match Sil.exp_sub sub1_inverse (Exp.Var id) with
match Sil.exp_sub (`Exp sub1_inverse) (Exp.Var id) with
| Exp.Var id' ->
if Sil.fav_mem fav_actual_pre id' || Ident.is_path id'
(* a path id represents a position in the pre *)
@ -216,13 +216,13 @@ let process_splitting
L.d_str "Don't know about id: "; Sil.d_exp (Exp.Var id); L.d_ln ();
assert false;
end
in Sil.sub_of_list (List.map ~f fav_sub_list) in
in Sil.subst_of_list (List.map ~f fav_sub_list) in
let sub2_list =
let f id = (id, Exp.Var (Ident.create_fresh Ident.kfootprint))
in List.map ~f (Sil.fav_to_list fav_missing_primed) in
let sub_list' =
List.map ~f:(fun (id, e) -> (id, Sil.exp_sub sub1 e)) sub_list in
let sub' = Sil.sub_of_list (sub2_list @ sub_list') in
let sub' = Sil.subst_of_list (sub2_list @ sub_list') in
(* normalize everything w.r.t sub' *)
let norm_missing_pi = Prop.pi_sub sub' missing_pi in
let norm_missing_sigma = Prop.sigma_sub sub' missing_sigma in
@ -947,7 +947,7 @@ let inconsistent_actualpre_missing tenv actual_pre split_opt =
let do_taint_check tenv caller_pname callee_pname calling_prop missing_pi sub actual_params =
let calling_pi = calling_prop.Prop.pi in
(* get a version of [missing_pi] whose var names match the names in calling pi *)
let missing_pi_sub = Prop.pi_sub sub missing_pi in
let missing_pi_sub = Prop.pi_sub (`Exp sub) missing_pi in
let combined_pi = calling_pi @ missing_pi_sub in
(* build a map from exp -> [taint attrs, untaint attrs], keeping only exprs with both kinds of
attrs (we will flag errors on those exprs) *)
@ -1068,8 +1068,8 @@ let exe_spec
vr_incons_res = inconsistent_results } in
begin
List.iter ~f:log_check_exn checks;
let subbed_pre = (Prop.prop_sub sub1 actual_pre) in
match check_dereferences tenv callee_pname subbed_pre sub2 spec_pre formal_params with
let subbed_pre = (Prop.prop_sub (`Exp sub1) actual_pre) in
match check_dereferences tenv callee_pname subbed_pre (`Exp sub2) spec_pre formal_params with
| Some (Deref_undef _, _) when Config.angelic_execution ->
let split = do_split () in
report_valid_res split

Write Preview
Loading…
Cancel
Save