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

@@ -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 *)

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 =

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} *)