From 7f231b8aa0a0c92571d1cfad7dbeca181d92246d Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Tue, 16 Feb 2016 17:13:15 -0800 Subject: [PATCH] Move pi and sigma types from Dom to Prop Summary: public Reviewed By: jeremydubreil Differential Revision: D2941587 fb-gh-sync-id: 7188027 shipit-source-id: 7188027 --- infer/src/backend/dom.ml | 31 +++++++++++++++---------------- infer/src/backend/prop.ml | 35 +++++++++++++++++++---------------- infer/src/backend/prop.mli | 32 ++++++++++++++++++-------------- 3 files changed, 52 insertions(+), 46 deletions(-) diff --git a/infer/src/backend/dom.ml b/infer/src/backend/dom.ml index 795c19515..fdef79472 100644 --- a/infer/src/backend/dom.ml +++ b/infer/src/backend/dom.ml @@ -17,9 +17,6 @@ open Utils let (++) = Sil.Int.add let (--) = Sil.Int.sub -type pi = Sil.atom list -type sigma = Sil.hpred list - (** {2 Object representing the status of the join operation} *) module JoinState : sig @@ -221,7 +218,7 @@ end module type InfoLossCheckerSig = sig - val init : sigma -> sigma -> unit + val init : Prop.sigma -> Prop.sigma -> unit val final : unit -> unit val lost_little : side -> Sil.exp -> Sil.exp list -> bool val add : side -> Sil.exp -> Sil.exp -> unit @@ -229,7 +226,7 @@ end module Dangling : sig - val init : sigma -> sigma -> unit + val init : Prop.sigma -> Prop.sigma -> unit val final : unit -> unit val check : side -> Sil.exp -> bool @@ -343,7 +340,7 @@ end module CheckJoin : sig - val init : JoinState.mode -> sigma -> sigma -> unit + val init : JoinState.mode -> Prop.sigma -> Prop.sigma -> unit val final : unit -> unit val lost_little : side -> Sil.exp -> Sil.exp list -> bool val add : side -> Sil.exp -> Sil.exp -> unit @@ -459,7 +456,7 @@ module FreshVarExp : sig val init : unit -> unit val get_fresh_exp : Sil.exp -> Sil.exp -> Sil.exp - val get_induced_pi : unit -> pi + val get_induced_pi : unit -> Prop.pi val lookup : side -> Sil.exp -> (Sil.exp * Sil.exp) option val final : unit -> unit @@ -1293,7 +1290,7 @@ let hpred_partial_meet (todo: Sil.exp * Sil.exp * Sil.exp) (hpred1: Sil.hpred) ( (** {2 Join and Meet for Sigma} *) -let find_hpred_by_address (e: Sil.exp) (sigma: sigma) : Sil.hpred option * sigma = +let find_hpred_by_address (e: Sil.exp) (sigma: Prop.sigma) : Sil.hpred option * Prop.sigma = let is_root_for_e e' = match (Prover.is_root Prop.prop_emp e' e) with | None -> false @@ -1321,7 +1318,7 @@ let same_pred (hpred1: Sil.hpred) (hpred2: Sil.hpred) : bool = (* check that applying renaming to the lhs / rhs of [sigma_new] * gives [sigma] and that the renaming is injective *) -let sigma_renaming_check (lhs: side) (sigma: sigma) (sigma_new: sigma) = +let sigma_renaming_check (lhs: side) (sigma: Prop.sigma) (sigma_new: Prop.sigma) = (* apply the lhs / rhs of the renaming to sigma, * and check that the renaming of primed vars is injective *) let fav_sigma = Prop.sigma_fav sigma_new in @@ -1332,8 +1329,8 @@ let sigma_renaming_check (lhs: side) (sigma: sigma) (sigma_new: sigma) = let sigma_renaming_check_lhs = sigma_renaming_check Lhs let sigma_renaming_check_rhs = sigma_renaming_check Rhs -let rec sigma_partial_join' mode (sigma_acc: sigma) - (sigma1_in: sigma) (sigma2_in: sigma) : (sigma * sigma * sigma) = +let rec sigma_partial_join' mode (sigma_acc: Prop.sigma) + (sigma1_in: Prop.sigma) (sigma2_in: Prop.sigma) : (Prop.sigma * Prop.sigma * Prop.sigma) = let lookup_and_expand side e e' = match (Rename.get_others side e, side) with @@ -1398,7 +1395,7 @@ let rec sigma_partial_join' mode (sigma_acc: sigma) 'side' describes that target is Lhs or Rhs. 'todo' describes the start point. *) - let cut_sigma side todo (target: sigma) (other: sigma) = + let cut_sigma side todo (target: Prop.sigma) (other: Prop.sigma) = let list_is_empty l = if l != [] then (L.d_strln "failure reason 61"; raise IList.Fail) in let x = Todo.take () in Todo.push todo; @@ -1518,7 +1515,8 @@ let rec sigma_partial_join' mode (sigma_acc: sigma) | _:: _, _:: _ -> L.d_strln "todo is empty, but the sigmas are not"; raise IList.Fail | _ -> sigma_acc, sigma1_in, sigma2_in -let sigma_partial_join mode (sigma1: sigma) (sigma2: sigma) : (sigma * sigma * sigma) = +let sigma_partial_join mode (sigma1: Prop.sigma) (sigma2: Prop.sigma) + : (Prop.sigma * Prop.sigma * Prop.sigma) = CheckJoin.init mode sigma1 sigma2; let lost_little = CheckJoin.lost_little in let s1, s2, s3 = sigma_partial_join' mode [] sigma1 sigma2 in @@ -1533,7 +1531,8 @@ let sigma_partial_join mode (sigma1: sigma) (sigma2: sigma) : (sigma * sigma * s with | exn -> (CheckJoin.final (); raise exn) -let rec sigma_partial_meet' (sigma_acc: sigma) (sigma1_in: sigma) (sigma2_in: sigma) : sigma = +let rec sigma_partial_meet' (sigma_acc: Prop.sigma) (sigma1_in: Prop.sigma) (sigma2_in: Prop.sigma) + : Prop.sigma = try let todo_curr = Todo.pop () in let e1, e2, e = todo_curr in @@ -1570,7 +1569,7 @@ let rec sigma_partial_meet' (sigma_acc: sigma) (sigma1_in: sigma) (sigma2_in: si | [], [] -> sigma_acc | _, _ -> L.d_strln "todo is empty, but the sigmas are not"; raise IList.Fail -let sigma_partial_meet (sigma1: sigma) (sigma2: sigma) : sigma = +let sigma_partial_meet (sigma1: Prop.sigma) (sigma2: Prop.sigma) : Prop.sigma = sigma_partial_meet' [] sigma1 sigma2 let widening_top = Sil.Int.of_int64 Int64.max_int -- Sil.Int.of_int 1000 (* nearly max_int but not so close to overflow *) @@ -1579,7 +1578,7 @@ let widening_bottom = Sil.Int.of_int64 Int64.min_int ++ Sil.Int.of_int 1000 (* n (** {2 Join and Meet for Pi} *) let pi_partial_join mode (ep1: Prop.exposed Prop.t) (ep2: Prop.exposed Prop.t) - (pi1: pi) (pi2: pi) : pi + (pi1: Prop.pi) (pi2: Prop.pi) : Prop.pi = let exp_is_const = function (* | Sil.Var id -> is_normal id *) diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml index 97248828b..89066fab9 100644 --- a/infer/src/backend/prop.ml +++ b/infer/src/backend/prop.ml @@ -30,6 +30,9 @@ let unSome = function type normal (** kind for normal props, i.e. normalized *) type exposed (** kind for exposed props *) +type pi = Sil.atom list +type sigma = Sil.hpred list + (** A proposition. The following invariants are mantained. [sub] is of the form id1 = e1 ... idn = en where: the id's are distinct and do not occur in the e's nor in [pi] or [sigma]; the id's are in sorted @@ -39,11 +42,11 @@ type exposed (** kind for exposed props *) normalized. *) type 'a t = { - sigma: Sil.hpred list; (** spatial part *) + sigma: sigma; (** spatial part *) sub: Sil.subst; (** substitution *) - pi: Sil.atom list; (** pure part *) - foot_sigma : Sil.hpred list; (** abduced spatial part *) - foot_pi: Sil.atom list; (** abduced pure part *) + pi: pi; (** pure part *) + foot_sigma : sigma; (** abduced spatial part *) + foot_pi: pi; (** abduced pure part *) } exception Cannot_star of ml_loc @@ -162,7 +165,7 @@ let pp_pi pe = else pp_semicolon_seq_oneline pe (Sil.pp_atom pe) (** Dump a pi. *) -let d_pi (pi: Sil.atom list) = L.add_print_action (L.PTpi, Obj.repr pi) +let d_pi (pi: pi) = L.add_print_action (L.PTpi, Obj.repr pi) (** Pretty print a sigma. *) let pp_sigma pe = @@ -191,7 +194,7 @@ let pp_sigma_simple pe env fmt sigma = Format.fprintf fmt "%a%a%a" pp_stack sigma_stack pp_nl (sigma_stack != [] && sigma_nonstack != []) pp_nonstack sigma_nonstack (** Dump a sigma. *) -let d_sigma (sigma: Sil.hpred list) = L.add_print_action (L.PTsigma, Obj.repr sigma) +let d_sigma (sigma: sigma) = L.add_print_action (L.PTsigma, Obj.repr sigma) (** Dump a pi and a sigma *) let d_pi_sigma pi sigma = @@ -202,13 +205,13 @@ let d_pi_sigma pi sigma = let get_sub (p: 'a t) : Sil.subst = p.sub (** Return the pi part of [prop]. *) -let get_pi (p: 'a t) : Sil.atom list = p.pi +let get_pi (p: 'a t) : pi = p.pi let pi_of_subst sub = IList.map (fun (id1, e2) -> Sil.Aeq (Sil.Var id1, e2)) (Sil.sub_to_list sub) (** Return the pure part of [prop]. *) -let get_pure (p: 'a t) : Sil.atom list = +let get_pure (p: 'a t) : pi = pi_of_subst p.sub @ p.pi (** Print existential quantification *) @@ -239,7 +242,7 @@ let pp_hpara_dll_simple _pe env n f pred = F.fprintf f "P_{%d} = %a%a" n (pp_evars pe) pred.Sil.evars_dll (pp_semicolon_seq pe (Sil.pp_hpred_env pe (Some env))) pred.Sil.body_dll (** Create an environment mapping (ident) expressions to the program variables containing them *) -let create_pvar_env (sigma: Sil.hpred list) : (Sil.exp -> Sil.exp) = +let create_pvar_env (sigma: sigma) : (Sil.exp -> Sil.exp) = let env = ref [] in let filter = function | Sil.Hpointsto (Sil.Lvar pvar, Sil.Eexp (Sil.Var v, inst), _) -> @@ -1535,7 +1538,7 @@ let prop_hpred_star (p : 'a t) (h : Sil.hpred) : exposed t = let sigma' = h:: p.sigma in { p with sigma = sigma'} -let prop_sigma_star (p : 'a t) (sigma : Sil.hpred list) : exposed t = +let prop_sigma_star (p : 'a t) (sigma : sigma) : exposed t = let sigma' = sigma @ p.sigma in { p with sigma = sigma' } @@ -1758,7 +1761,7 @@ let conjoin_neq ?(footprint = false) exp1 exp2 prop = prop_atom_and ~footprint prop (Sil.Aneq (exp1, exp2)) (** Return the spatial part *) -let get_sigma (p: 'a t) : Sil.hpred list = p.sigma +let get_sigma (p: 'a t) : sigma = p.sigma (** Return the pure part of the footprint *) let get_pi_footprint p = @@ -2511,15 +2514,15 @@ let prop_rename_fav_with_existentials (p : normal t) : normal t = (** Iterator state over sigma. *) type 'a prop_iter = { pit_sub : Sil.subst; (** substitution for equalities *) - pit_pi : Sil.atom list; (** pure part *) + pit_pi : pi; (** pure part *) pit_newpi : (bool * Sil.atom) list; (** newly added atoms. *) (** The first records !Config.footprint. *) - pit_old : Sil.hpred list; (** sigma already visited *) + pit_old : sigma; (** sigma already visited *) pit_curr : Sil.hpred; (** current element *) pit_state : 'a; (** state of current element *) - pit_new : Sil.hpred list; (** sigma not yet visited *) - pit_foot_pi : Sil.atom list; (** pure part of the footprint *) - pit_foot_sigma : Sil.hpred list; (** sigma part of the footprint *) + pit_new : sigma; (** sigma not yet visited *) + pit_foot_pi : pi; (** pure part of the footprint *) + pit_foot_sigma : sigma; (** sigma part of the footprint *) } let prop_iter_create prop = diff --git a/infer/src/backend/prop.mli b/infer/src/backend/prop.mli index e934ce15c..e7f9e8339 100644 --- a/infer/src/backend/prop.mli +++ b/infer/src/backend/prop.mli @@ -17,6 +17,10 @@ type normal (** kind for normal props, i.e. normalized *) type exposed (** kind for exposed props *) (** Proposition. *) + +type pi = Sil.atom list +type sigma = Sil.hpred list + type 'a t (** the kind 'a should range over [normal] and [exposed] *) (** type to describe different strategies for initializing fields of a structure. [No_init] does not @@ -34,7 +38,7 @@ exception Cannot_star of ml_loc val prop_compare : 'a t -> 'a t -> int (** Check the equality of two sigma's *) -val sigma_equal : Sil.hpred list -> Sil.hpred list -> bool +val sigma_equal : sigma -> sigma -> bool (** Check the equality of two propositions *) val prop_equal : 'a t -> 'a t -> bool @@ -46,23 +50,23 @@ val pp_sub : printenv -> Format.formatter -> subst -> unit val d_sub : subst -> unit (** Pretty print a pi. *) -val pp_pi : printenv -> Format.formatter -> Sil.atom list -> unit +val pp_pi : printenv -> Format.formatter -> pi -> unit (** Dump a pi. *) -val d_pi : Sil.atom list -> unit +val d_pi : pi -> unit (** Pretty print a sigma. *) -val pp_sigma : printenv -> Format.formatter -> Sil.hpred list -> unit +val pp_sigma : printenv -> Format.formatter -> sigma -> unit (** Dump a sigma. *) -val d_sigma : Sil.hpred list -> unit +val d_sigma : sigma -> unit (** Dump a pi and a sigma *) -val d_pi_sigma: Sil.atom list -> Sil.hpred list -> unit +val d_pi_sigma: pi -> sigma -> unit (** Split sigma into stack and nonstack parts. The boolean indicates whether the stack should only include local variales. *) -val sigma_get_stack_nonstack : bool -> Sil.hpred list -> Sil.hpred list * Sil.hpred list +val sigma_get_stack_nonstack : bool -> sigma -> sigma * sigma (** Update the object substitution given the stack variables in the prop *) val prop_update_obj_sub : printenv -> 'a t -> printenv @@ -385,25 +389,25 @@ val prop_primed_vars_to_normal_vars : normal t -> normal t val prop_rename_primed_fresh : normal t -> normal t (** Build an exposed prop from pi *) -val from_pi : Sil.atom list -> exposed t +val from_pi : pi -> exposed t (** Build an exposed prop from sigma *) -val from_sigma : Sil.hpred list -> exposed t +val from_sigma : sigma -> exposed t (** Replace the substitution part of a prop *) val replace_sub : Sil.subst -> 'a t -> exposed t (** Replace the pi part of a prop *) -val replace_pi : Sil.atom list -> 'a t -> exposed t +val replace_pi : pi -> 'a t -> exposed t (** Replace the sigma part of a prop *) -val replace_sigma : Sil.hpred list -> 'a t -> exposed t +val replace_sigma : sigma -> 'a t -> exposed t (** Replace the sigma part of the footprint of a prop *) -val replace_sigma_footprint : Sil.hpred list -> 'a t -> exposed t +val replace_sigma_footprint : sigma -> 'a t -> exposed t (** Replace the pi part of the footprint of a prop *) -val replace_pi_footprint : Sil.atom list -> 'a t -> exposed t +val replace_pi_footprint : pi -> 'a t -> exposed t (** Rename free variables in a prop replacing them with existentially quantified vars *) val prop_rename_fav_with_existentials : normal t -> normal t @@ -489,7 +493,7 @@ val get_fld_typ_path_opt : Sil.ExpSet.t -> Sil.exp -> Sil.HpredSet.t -> (Ident.fieldname option * Sil.typ) list option (** filter [pi] by removing the pure atoms that do not contain an expression in [exps] *) -val compute_reachable_atoms : Sil.atom list -> Sil.ExpSet.t -> Sil.atom list +val compute_reachable_atoms : pi -> Sil.ExpSet.t -> pi (** {2 Internal modules} *)