From 621ace48af0f7dcec3cc5862b623ea45180b0de5 Mon Sep 17 00:00:00 2001 From: Andrzej Kotulski Date: Wed, 5 Jul 2017 08:42:49 -0700 Subject: [PATCH] [backend] Make Sil.subst type variant to allow more types of substitution Reviewed By: jberdine Differential Revision: D5182491 fbshipit-source-id: 3ea6b66 --- infer/src/IR/Sil.re | 59 ++++++++++++------- infer/src/IR/Sil.rei | 55 ++++++++++-------- infer/src/backend/Attribute.ml | 2 +- infer/src/backend/abs.ml | 34 +++++------ infer/src/backend/dom.ml | 14 ++--- infer/src/backend/interproc.ml | 10 ++-- infer/src/backend/match.ml | 38 ++++++------ infer/src/backend/match.mli | 4 +- infer/src/backend/prop.ml | 100 ++++++++++++++------------------ infer/src/backend/prop.mli | 7 +-- infer/src/backend/prover.ml | 100 ++++++++++++++++---------------- infer/src/backend/prover.mli | 5 +- infer/src/backend/rearrange.ml | 2 +- infer/src/backend/specs.ml | 2 +- infer/src/backend/state.ml | 4 +- infer/src/backend/symExec.ml | 4 +- infer/src/backend/tabulation.ml | 22 +++---- 17 files changed, 234 insertions(+), 228 deletions(-) diff --git a/infer/src/IR/Sil.re b/infer/src/IR/Sil.re index 76e6fa463..028681be9 100644 --- a/infer/src/IR/Sil.re +++ b/infer/src/IR/Sil.re @@ -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 ( - [(para.cell, cell), (para.blink, blink), (para.flink, flink), ...subst_for_svars] @ subst_for_evars + `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) }; diff --git a/infer/src/IR/Sil.rei b/infer/src/IR/Sil.rei index 46dbb8285..c68726312 100644 --- a/infer/src/IR/Sil.rei +++ b/infer/src/IR/Sil.rei @@ -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 */ diff --git a/infer/src/backend/Attribute.ml b/infer/src/backend/Attribute.ml index b604a26c1..8aa3d986b 100644 --- a/infer/src/backend/Attribute.ml +++ b/infer/src/backend/Attribute.ml @@ -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 diff --git a/infer/src/backend/abs.ml b/infer/src/backend/abs.ml index 0f8bdcd09..38acede89 100644 --- a/infer/src/backend/abs.ml +++ b/infer/src/backend/abs.ml @@ -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 diff --git a/infer/src/backend/dom.ml b/infer/src/backend/dom.ml index b2c53b865..c2fac47be 100644 --- a/infer/src/backend/dom.ml +++ b/infer/src/backend/dom.ml @@ -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) diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index e346887b3..80321bb94 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -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 diff --git a/infer/src/backend/match.ml b/infer/src/backend/match.ml index 8bc3e6787..305e3cb00 100644 --- a/infer/src/backend/match.ml +++ b/infer/src/backend/match.ml @@ -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 diff --git a/infer/src/backend/match.mli b/infer/src/backend/match.mli index e1222447e..138bd0250 100644 --- a/infer/src/backend/match.mli +++ b/infer/src/backend/match.mli @@ -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. diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml index fc2bd20a1..9e4101ab2 100644 --- a/infer/src/backend/prop.ml +++ b/infer/src/backend/prop.ml @@ -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,9 +152,10 @@ 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 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 +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 (** Dump a substitution. *) let d_sub (sub: Sil.subst) = L.add_print_action (PTsub, Obj.repr 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,9 +2159,9 @@ 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 - ~f:(fun i -> (i, Exp.Var (Ident.create_fresh Ident.knormal))) - ids) in + 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 (** convert the normal vars to primed vars. *) @@ -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 diff --git a/infer/src/backend/prop.mli b/infer/src/backend/prop.mli index 043b7c2a6..a48fe902c 100644 --- a/infer/src/backend/prop.mli +++ b/infer/src/backend/prop.mli @@ -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 *) diff --git a/infer/src/backend/prover.ml b/infer/src/backend/prover.ml index c39692197..aa9f1b59b 100644 --- a/infer/src/backend/prover.ml +++ b/infer/src/backend/prover.ml @@ -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 diff --git a/infer/src/backend/prover.mli b/infer/src/backend/prover.mli index 584a49139..a7011a9cd 100644 --- a/infer/src/backend/prover.mli +++ b/infer/src/backend/prover.mli @@ -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 - - - diff --git a/infer/src/backend/rearrange.ml b/infer/src/backend/rearrange.ml index ad364d821..ece74cea5 100644 --- a/infer/src/backend/rearrange.ml +++ b/infer/src/backend/rearrange.ml @@ -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') diff --git a/infer/src/backend/specs.ml b/infer/src/backend/specs.ml index 9a738791a..57361aa1e 100644 --- a/infer/src/backend/specs.ml +++ b/infer/src/backend/specs.ml @@ -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 diff --git a/infer/src/backend/state.ml b/infer/src/backend/state.ml index 884ea3ed5..0b08aaf02 100644 --- a/infer/src/backend/state.ml +++ b/infer/src/backend/state.ml @@ -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 diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index c4a4cd15b..3760d7dcd 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -1631,8 +1631,8 @@ 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 - ~f:(fun (id1, id2) -> (id1, Exp.Var id2)) ids_primed_normal) in + 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 p', fav_normal in diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml index 92e2dc2bb..1371174ec 100644 --- a/infer/src/backend/tabulation.ml +++ b/infer/src/backend/tabulation.ml @@ -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