From 3896b10265f13e8c667faa5892a117eeefc65847 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Tue, 9 Aug 2016 03:37:37 -0700
Subject: [PATCH] Move Prop.Attribute to toplevel

Summary:
This diff lifts the Prop.Attribute module out of Prop.  This required
moving several Prop functions that depend on Attribute
(find_arithmetic_problem, deallocate_stack_vars, find_equal_formal_path)
and adding numerous calls to Prop.normalize to fix normal/exposed
mismatches.  Also note that the type of Prop.normalize is generalized to
allow calling it on normalized props.

Reviewed By: cristianoc

Differential Revision: D3684523

fbshipit-source-id: f37af8b
---
 infer/src/IR/Cfg.re                |   8 +-
 infer/src/IR/Const.re              |  18 ++
 infer/src/IR/Const.rei             |   6 +
 infer/src/backend/Attribute.ml     | 327 +++++++++++++++++++++++++++
 infer/src/backend/Attribute.mli    | 113 ++++++++++
 infer/src/backend/abs.ml           |   8 +-
 infer/src/backend/dom.ml           |   2 +-
 infer/src/backend/errdesc.ml       |   6 +-
 infer/src/backend/interproc.ml     |   6 +-
 infer/src/backend/modelBuiltins.ml |  22 +-
 infer/src/backend/prop.ml          | 347 ++---------------------------
 infer/src/backend/prop.mli         |  97 --------
 infer/src/backend/rearrange.ml     |  10 +-
 infer/src/backend/symExec.ml       |  44 ++--
 infer/src/backend/tabulation.ml    |  26 +--
 infer/src/backend/taint.ml         |   2 +-
 16 files changed, 544 insertions(+), 498 deletions(-)
 create mode 100644 infer/src/backend/Attribute.ml
 create mode 100644 infer/src/backend/Attribute.mli

diff --git a/infer/src/IR/Cfg.re b/infer/src/IR/Cfg.re
index e79ac2393..8de31709b 100644
--- a/infer/src/IR/Cfg.re
+++ b/infer/src/IR/Cfg.re
@@ -987,7 +987,7 @@ let remove_abducted_retvars p =>
         )
         ([], [])
         (Prop.get_sigma p);
-    let (_, p') = Prop.deallocate_stack_vars p abducteds;
+    let (_, p') = Attribute.deallocate_stack_vars p abducteds;
     let normal_pvar_set =
       IList.fold_left
         (fun normal_pvar_set pvar => Exp.Set.add (Exp.Lvar pvar) normal_pvar_set)
@@ -1009,7 +1009,7 @@ let remove_locals (curr_f: Procdesc.t) p => {
       names_of_block_locals @ names_of_locals @ names_of_static_locals
     | _ => names_of_locals
     };
-  let (removed, p') = Prop.deallocate_stack_vars p names_of_locals';
+  let (removed, p') = Attribute.deallocate_stack_vars p names_of_locals';
   (
     removed,
     if Config.angelic_execution {
@@ -1023,7 +1023,7 @@ let remove_locals (curr_f: Procdesc.t) p => {
 let remove_formals (curr_f: Procdesc.t) p => {
   let pname = Procdesc.get_proc_name curr_f;
   let formal_vars = IList.map (fun (n, _) => Pvar.mk n pname) (Procdesc.get_formals curr_f);
-  Prop.deallocate_stack_vars p formal_vars
+  Attribute.deallocate_stack_vars p formal_vars
 };
 
 
@@ -1031,7 +1031,7 @@ let remove_formals (curr_f: Procdesc.t) p => {
 let remove_ret (curr_f: Procdesc.t) (p: Prop.t Prop.normal) => {
   let pname = Procdesc.get_proc_name curr_f;
   let name_of_ret = Procdesc.get_ret_var curr_f;
-  let (_, p') = Prop.deallocate_stack_vars p [Pvar.to_callee pname name_of_ret];
+  let (_, p') = Attribute.deallocate_stack_vars p [Pvar.to_callee pname name_of_ret];
   p'
 };
 
diff --git a/infer/src/IR/Const.re b/infer/src/IR/Const.re
index 3c525dea5..898c2946e 100644
--- a/infer/src/IR/Const.re
+++ b/infer/src/IR/Const.re
@@ -82,3 +82,21 @@ let pp pe f =>
   | Cptr_to_fld fn _ => F.fprintf f "__fld_%a" Ident.pp_fieldname fn;
 
 let to_string c => pp_to_string (pp pe_text) c;
+
+let iszero_int_float =
+  fun
+  | Cint i => IntLit.iszero i
+  | Cfloat 0.0 => true
+  | _ => false;
+
+let isone_int_float =
+  fun
+  | Cint i => IntLit.isone i
+  | Cfloat 1.0 => true
+  | _ => false;
+
+let isminusone_int_float =
+  fun
+  | Cint i => IntLit.isminusone i
+  | Cfloat (-1.0) => true
+  | _ => false;
diff --git a/infer/src/IR/Const.rei b/infer/src/IR/Const.rei
index 90d352b07..da4905967 100644
--- a/infer/src/IR/Const.rei
+++ b/infer/src/IR/Const.rei
@@ -43,3 +43,9 @@ let kind_equal: t => t => bool;
 let pp: printenv => F.formatter => t => unit;
 
 let to_string: t => string;
+
+let iszero_int_float: t => bool;
+
+let isone_int_float: t => bool;
+
+let isminusone_int_float: t => bool;
diff --git a/infer/src/backend/Attribute.ml b/infer/src/backend/Attribute.ml
new file mode 100644
index 000000000..93a575311
--- /dev/null
+++ b/infer/src/backend/Attribute.ml
@@ -0,0 +1,327 @@
+(*
+ * Copyright (c) 2009 - 2013 Monoidics ltd.
+ * Copyright (c) 2013 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ *)
+
+open! Utils
+
+(** Attribute manipulation in Propositions (i.e., Symbolic Heaps) *)
+
+module L = Logging
+module F = Format
+
+
+(** Check whether an atom is used to mark an attribute *)
+let is_pred atom =
+  match atom with
+  | Sil.Apred _ | Anpred _ -> true
+  | _ -> false
+
+(** Add an attribute associated to the argument expressions *)
+let add ?(footprint = false) ?(polarity = true) prop attr args =
+  Prop.prop_atom_and ~footprint prop
+    (if polarity then Sil.Apred (attr, args) else Sil.Anpred (attr, args))
+
+let attributes_in_same_category attr1 attr2 =
+  let cat1 = PredSymb.to_category attr1 in
+  let cat2 = PredSymb.to_category attr2 in
+  PredSymb.category_equal cat1 cat2
+
+(** Replace an attribute associated to the expression *)
+let add_or_replace_check_changed check_attribute_change prop atom0 =
+  match atom0 with
+  | Sil.Apred (att0, ((_ :: _) as exps0)) | Anpred (att0, ((_ :: _) as exps0)) ->
+      let nexps = IList.map (fun e -> Prop.exp_normalize_prop prop e) exps0 in
+      let nexp = IList.hd nexps in (* len nexps = len exps0 > 0 by match *)
+      let natom = Sil.atom_replace_exp (IList.combine exps0 nexps) atom0 in
+      let atom_map = function
+        | Sil.Apred (att, exp :: _) | Anpred (att, exp :: _)
+          when Exp.equal nexp exp && attributes_in_same_category att att0 ->
+            check_attribute_change att att0;
+            natom
+        | atom ->
+            atom in
+      let pi = Prop.get_pi prop in
+      let pi' = IList.map_changed atom_map pi in
+      if pi == pi'
+      then Prop.prop_atom_and prop natom
+      else Prop.normalize (Prop.replace_pi pi' prop)
+  | _ ->
+      prop
+
+let add_or_replace prop atom =
+  (* wrapper for the most common case: do nothing *)
+  let check_attr_changed = (fun _ _ -> ()) in
+  add_or_replace_check_changed check_attr_changed prop atom
+
+(** Get all the attributes of the prop *)
+let get_all (prop: 'a Prop.t) =
+  let res = ref [] in
+  let do_atom a = if is_pred a then res := a :: !res in
+  IList.iter do_atom (Prop.get_pi prop);
+  IList.rev !res
+
+(** Get all the attributes of the prop *)
+let get_for_symb prop att =
+  IList.filter (function
+      | Sil.Apred (att', _) | Anpred (att', _) -> PredSymb.equal att' att
+      | _ -> false
+    ) (Prop.get_pi prop)
+
+(** Get the attribute associated to the expression, if any *)
+let get_for_exp (prop: 'a Prop.t) exp =
+  let nexp = Prop.exp_normalize_prop prop exp in
+  let atom_get_attr attributes atom =
+    match atom with
+    | Sil.Apred (_, es) | Anpred (_, es) when IList.mem Exp.equal nexp es -> atom :: attributes
+    | _ -> attributes in
+  IList.fold_left atom_get_attr [] (Prop.get_pi prop)
+
+let get prop exp category =
+  let atts = get_for_exp prop exp in
+  try
+    Some
+      (IList.find (function
+           | Sil.Apred (att, _) | Anpred (att, _) ->
+               PredSymb.category_equal (PredSymb.to_category att) category
+           | _ -> false
+         ) atts)
+  with Not_found -> None
+
+let get_undef prop exp =
+  get prop exp ACundef
+
+let get_resource prop exp =
+  get prop exp ACresource
+
+let get_taint prop exp =
+  get prop exp ACtaint
+
+let get_autorelease prop exp =
+  get prop exp ACautorelease
+
+let get_objc_null prop exp =
+  get prop exp ACobjc_null
+
+let get_div0 prop exp =
+  get prop exp ACdiv0
+
+let get_observer prop exp =
+  get prop exp ACobserver
+
+let get_retval prop exp =
+  get prop exp ACretval
+
+let has_dangling_uninit prop exp =
+  let la = get_for_exp prop exp in
+  IList.exists (function
+      | Sil.Apred (a, _) -> PredSymb.equal a (Adangling DAuninit)
+      | _ -> false
+    ) la
+
+let filter_atoms ~f prop =
+  let pi0 = Prop.get_pi prop in
+  let pi1 = IList.filter_changed f pi0 in
+  if pi1 == pi0 then
+    prop
+  else
+    Prop.normalize (Prop.replace_pi pi1 prop)
+
+let remove prop atom =
+  match atom with
+  | Sil.Apred (_, exps) | Anpred (_, exps) ->
+      let nexps = IList.map (fun e -> Prop.exp_normalize_prop prop e) exps in
+      let natom = Sil.atom_replace_exp (IList.combine exps nexps) atom in
+      let f a = not (Sil.atom_equal natom a) in
+      filter_atoms ~f prop
+  | _ ->
+      prop
+
+(** Remove an attribute from all the atoms in the heap *)
+let remove_for_attr prop att0 =
+  let f = function
+    | Sil.Apred (att, _) | Anpred (att, _) -> not (PredSymb.equal att0 att)
+    | _ -> true in
+  filter_atoms ~f prop
+
+let remove_resource ra_kind ra_res =
+  let f = function
+    | Sil.Apred (Aresource res_action, _) ->
+        PredSymb.res_act_kind_compare res_action.ra_kind ra_kind <> 0
+        || PredSymb.resource_compare res_action.ra_res ra_res <> 0
+    | _ -> true in
+  filter_atoms ~f
+
+(** Apply f to every resource attribute in the prop *)
+let map_resource prop f =
+  let attribute_map e = function
+    | PredSymb.Aresource ra -> PredSymb.Aresource (f e ra)
+    | att -> att in
+  let atom_map = function
+    | Sil.Apred (att, ([e] as es)) -> Sil.Apred (attribute_map e att, es)
+    | Sil.Anpred (att, ([e] as es)) -> Sil.Anpred (attribute_map e att, es)
+    | atom -> atom in
+  let pi0 = Prop.get_pi prop in
+  let pi1 = IList.map_changed atom_map pi0 in
+  if pi1 == pi0 then
+    prop
+  else
+    Prop.normalize (Prop.replace_pi pi1 prop)
+
+(* Replace an attribute OBJC_NULL($n1) with OBJC_NULL(var) when var = $n1, and also sets $n1 =
+   0 *)
+let replace_objc_null prop lhs_exp rhs_exp =
+  match get_objc_null prop rhs_exp, rhs_exp with
+  | Some atom, Exp.Var _ ->
+      let prop = remove prop atom in
+      let prop = Prop.conjoin_eq rhs_exp Exp.zero prop in
+      let natom = Sil.atom_replace_exp [(rhs_exp, lhs_exp)] atom in
+      add_or_replace prop natom
+  | _ -> prop
+
+let rec nullify_exp_with_objc_null prop exp =
+  match exp with
+  | Exp.BinOp (_, exp1, exp2) ->
+      let prop' = nullify_exp_with_objc_null prop exp1 in
+      nullify_exp_with_objc_null prop' exp2
+  | Exp.UnOp (_, exp, _) ->
+      nullify_exp_with_objc_null prop exp
+  | Exp.Var _ ->
+      (match get_objc_null prop exp with
+       | Some atom ->
+           let prop' = remove prop atom in
+           Prop.conjoin_eq exp Exp.zero prop'
+       | _ -> prop)
+  | _ -> prop
+
+(** mark Exp.Var's or Exp.Lvar's as undefined *)
+let mark_vars_as_undefined prop vars_to_mark callee_pname ret_annots loc path_pos =
+  let att_undef = PredSymb.Aundef (callee_pname, ret_annots, loc, path_pos) in
+  let mark_var_as_undefined exp prop =
+    match exp with
+    | Exp.Var _ | Lvar _ -> add_or_replace prop (Apred (att_undef, [exp]))
+    | _ -> prop in
+  IList.fold_left (fun prop id -> mark_var_as_undefined id prop) prop vars_to_mark
+
+(** type for arithmetic problems *)
+type arith_problem =
+  (* division by zero *)
+  | Div0 of Exp.t
+
+  (* unary minus of unsigned type applied to the given expression *)
+  | UminusUnsigned of Exp.t * Typ.t
+
+(** Look for an arithmetic problem in [exp] *)
+let find_arithmetic_problem proc_node_session prop exp =
+  let exps_divided = ref [] in
+  let uminus_unsigned = ref [] in
+  let res = ref prop in
+  let check_zero e =
+    match Prop.exp_normalize_prop prop e with
+    | Exp.Const c when Const.iszero_int_float c -> true
+    | _ ->
+        res := add_or_replace !res (Apred (Adiv0 proc_node_session, [e]));
+        false in
+  let rec walk = function
+    | Exp.Var _ -> ()
+    | Exp.UnOp (Unop.Neg, e, Some (
+        (Typ.Tint
+           (Typ.IUChar | Typ.IUInt | Typ.IUShort | Typ.IULong | Typ.IULongLong) as typ))) ->
+        uminus_unsigned := (e, typ) :: !uminus_unsigned
+    | Exp.UnOp(_, e, _) -> walk e
+    | Exp.BinOp(op, e1, e2) ->
+        if op = Binop.Div || op = Binop.Mod then exps_divided := e2 :: !exps_divided;
+        walk e1; walk e2
+    | Exp.Exn _ -> ()
+    | Exp.Closure _ -> ()
+    | Exp.Const _ -> ()
+    | Exp.Cast (_, e) -> walk e
+    | Exp.Lvar _ -> ()
+    | Exp.Lfield (e, _, _) -> walk e
+    | Exp.Lindex (e1, e2) -> walk e1; walk e2
+    | Exp.Sizeof (_, None, _) -> ()
+    | Exp.Sizeof (_, Some len, _) -> walk len in
+  walk exp;
+  try Some (Div0 (IList.find check_zero !exps_divided)), !res
+  with Not_found ->
+    (match !uminus_unsigned with
+     | (e, t):: _ -> Some (UminusUnsigned (e, t)), !res
+     | _ -> None, !res)
+
+(** Deallocate the stack variables in [pvars], and replace them by normal variables.
+    Return the list of stack variables whose address was still present after deallocation. *)
+let deallocate_stack_vars (p: 'a Prop.t) pvars =
+  let filter = function
+    | Sil.Hpointsto (Exp.Lvar v, _, _) ->
+        IList.exists (Pvar.equal v) pvars
+    | _ -> false in
+  let sigma_stack, sigma_other = IList.partition filter (Prop.get_sigma p) in
+  let fresh_address_vars = ref [] in (* fresh vars substituted for the address of stack vars *)
+  let stack_vars_address_in_post = ref [] in (* stack vars whose address is still present *)
+  let exp_replace = IList.map (function
+      | Sil.Hpointsto (Exp.Lvar v, _, _) ->
+          let freshv = Ident.create_fresh Ident.kprimed in
+          fresh_address_vars := (v, freshv) :: !fresh_address_vars;
+          (Exp.Lvar v, Exp.Var freshv)
+      | _ -> assert false) sigma_stack in
+  let pi1 = IList.map (fun (id, e) -> Sil.Aeq (Exp.Var id, e)) (Sil.sub_to_list (Prop.get_sub p)) in
+  let pi = IList.map (Sil.atom_replace_exp exp_replace) ((Prop.get_pi p) @ pi1) in
+  let p' =
+    Prop.normalize
+      (Prop.replace_sub Sil.sub_empty
+         (Prop.replace_sigma (Prop.sigma_replace_exp exp_replace sigma_other) p)) in
+  let p'' =
+    let res = ref p' in
+    let p'_fav = Prop.prop_fav p' in
+    let do_var (v, freshv) =
+      if Sil.fav_mem p'_fav freshv then (* the address of a de-allocated stack var in in the post *)
+        begin
+          stack_vars_address_in_post := v :: !stack_vars_address_in_post;
+          let pred = Sil.Apred (Adangling DAaddr_stack_var, [Exp.Var freshv]) in
+          res := add_or_replace !res pred
+        end in
+    IList.iter do_var !fresh_address_vars;
+    !res in
+  !stack_vars_address_in_post, IList.fold_left Prop.prop_atom_and p'' pi
+
+(** Input of this method is an exp in a prop. Output is a formal variable or path from a
+    formal variable that is equal to the expression,
+    or the OBJC_NULL attribute of the expression. *)
+let find_equal_formal_path e prop =
+  let rec find_in_sigma e seen_hpreds =
+    IList.fold_right (
+      fun hpred res ->
+        if IList.mem Sil.hpred_equal hpred seen_hpreds then None
+        else
+          let seen_hpreds = hpred :: seen_hpreds in
+          match res with
+          | Some _ -> res
+          | None ->
+              match hpred with
+              | Sil.Hpointsto (Exp.Lvar pvar1, Sil.Eexp (exp2, Sil.Iformal(_, _) ), _)
+                when Exp.equal exp2 e &&
+                     (Pvar.is_local pvar1 || Pvar.is_seed pvar1) ->
+                  Some (Exp.Lvar pvar1)
+              | Sil.Hpointsto (exp1, Sil.Estruct (fields, _), _) ->
+                  IList.fold_right (fun (field, strexp) res ->
+                      match res with
+                      | Some _ -> res
+                      | None ->
+                          match strexp with
+                          | Sil.Eexp (exp2, _) when Exp.equal exp2 e ->
+                              (match find_in_sigma exp1 seen_hpreds with
+                               | Some vfs -> Some (Exp.Lfield (vfs, field, Typ.Tvoid))
+                               | None -> None)
+                          | _ -> None) fields None
+              | _ -> None) (Prop.get_sigma prop) None in
+  match find_in_sigma e [] with
+  | Some vfs -> Some vfs
+  | None ->
+      match get_objc_null prop e with
+      | Some (Apred (Aobjc_null, [_; vfs])) -> Some vfs
+      | _ -> None
diff --git a/infer/src/backend/Attribute.mli b/infer/src/backend/Attribute.mli
new file mode 100644
index 000000000..c5ab512a9
--- /dev/null
+++ b/infer/src/backend/Attribute.mli
@@ -0,0 +1,113 @@
+(*
+ * Copyright (c) 2009 - 2013 Monoidics ltd.
+ * Copyright (c) 2013 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ *)
+
+open! Utils
+
+(** Attribute manipulation in Propositions (i.e., Symbolic Heaps) *)
+
+module L = Logging
+module F = Format
+
+
+(** Check whether an atom is used to mark an attribute *)
+val is_pred : Sil.atom -> bool
+
+(** Add an attribute associated to the argument expressions *)
+val add : ?footprint: bool -> ?polarity: bool ->
+  Prop.normal Prop.t -> PredSymb.t -> Exp.t list -> Prop.normal Prop.t
+
+(** Replace an attribute associated to the expression *)
+val add_or_replace : Prop.normal Prop.t -> Sil.atom -> Prop.normal Prop.t
+
+(** Replace an attribute associated to the expression, and call the given function with new and
+    old attributes if they changed. *)
+val add_or_replace_check_changed :
+  (PredSymb.t -> PredSymb.t -> unit) -> Prop.normal Prop.t -> Sil.atom -> Prop.normal Prop.t
+
+(** Get all the attributes of the prop *)
+val get_all : 'a Prop.t -> Sil.atom list
+
+(** Get the attributes associated to the expression, if any *)
+val get_for_exp : 'a Prop.t -> Exp.t -> Sil.atom list
+
+(** Retrieve all the atoms that contain a specific attribute *)
+val get_for_symb : 'a Prop.t -> PredSymb.t -> Sil.atom list
+
+(** Get the autorelease attribute associated to the expression, if any *)
+val get_autorelease : 'a Prop.t -> Exp.t -> Sil.atom option
+
+(** Get the div0 attribute associated to the expression, if any *)
+val get_div0 : 'a Prop.t -> Exp.t -> Sil.atom option
+
+(** Get the objc null attribute associated to the expression, if any *)
+val get_objc_null : 'a Prop.t -> Exp.t -> Sil.atom option
+
+(** Get the observer attribute associated to the expression, if any *)
+val get_observer : 'a Prop.t -> Exp.t -> Sil.atom option
+
+(** Get the resource attribute associated to the expression, if any *)
+val get_resource : 'a Prop.t -> Exp.t -> Sil.atom option
+
+(** Get the retval null attribute associated to the expression, if any *)
+val get_retval : 'a Prop.t -> Exp.t -> Sil.atom option
+
+(** Get the taint attribute associated to the expression, if any *)
+val get_taint : 'a Prop.t -> Exp.t -> Sil.atom option
+
+(** Get the undef attribute associated to the expression, if any *)
+val get_undef : 'a Prop.t -> Exp.t -> Sil.atom option
+
+(** Test for existence of an Adangling DAuninit attribute associated to the exp *)
+val has_dangling_uninit : 'a Prop.t -> Exp.t -> bool
+
+(** Remove an attribute *)
+val remove : Prop.normal Prop.t -> Sil.atom -> Prop.normal Prop.t
+
+(** Remove all attributes for the given attr *)
+val remove_for_attr : Prop.normal Prop.t -> PredSymb.t -> Prop.normal Prop.t
+
+(** Remove all attributes for the given resource and kind *)
+val remove_resource :
+  PredSymb.res_act_kind -> PredSymb.resource -> Prop.normal Prop.t -> Prop.normal Prop.t
+
+(** Apply f to every resource attribute in the prop *)
+val map_resource :
+  Prop.normal Prop.t -> (Exp.t -> PredSymb.res_action -> PredSymb.res_action) -> Prop.normal Prop.t
+
+(** [replace_objc_null lhs rhs].
+    If rhs has the objc_null attribute, replace the attribute and set the lhs = 0 *)
+val replace_objc_null : Prop.normal Prop.t -> Exp.t -> Exp.t -> Prop.normal Prop.t
+
+(** For each Var subexp of the argument with an Aobjc_null attribute,
+    remove the attribute and conjoin an equality to zero. *)
+val nullify_exp_with_objc_null : Prop.normal Prop.t -> Exp.t -> Prop.normal Prop.t
+
+(** mark Exp.Var's or Exp.Lvar's as undefined *)
+val mark_vars_as_undefined :
+  Prop.normal Prop.t -> Exp.t list -> Procname.t -> Typ.item_annotation -> Location.t ->
+  PredSymb.path_pos -> Prop.normal Prop.t
+
+(** type for arithmetic problems *)
+type arith_problem =
+  (* division by zero *)
+  | Div0 of Exp.t
+
+  (* unary minus of unsigned type applied to the given expression *)
+  | UminusUnsigned of Exp.t * Typ.t
+
+(** Look for an arithmetic problem in [exp] *)
+val find_arithmetic_problem :
+  PredSymb.path_pos -> Prop.normal Prop.t -> Exp.t -> arith_problem option * Prop.normal Prop.t
+
+(** Deallocate the stack variables in [pvars], and replace them by normal variables.
+    Return the list of stack variables whose address was still present after deallocation. *)
+val deallocate_stack_vars : Prop.normal Prop.t -> Pvar.t list -> Pvar.t list * Prop.normal Prop.t
+
+val find_equal_formal_path : Exp.t -> 'a Prop.t -> Exp.t option
diff --git a/infer/src/backend/abs.ml b/infer/src/backend/abs.ml
index d0c0f3217..4fb80f5e1 100644
--- a/infer/src/backend/abs.ml
+++ b/infer/src/backend/abs.ml
@@ -1029,11 +1029,11 @@ let cycle_has_weak_or_unretained_or_assign_field cycle =
   do_cycle cycle
 
 let check_observer_is_unsubscribed_deallocation prop e =
-  let pvar_opt = match Prop.Attribute.get_resource prop e with
+  let pvar_opt = match Attribute.get_resource prop e with
     | Some (Apred (Aresource ({ ra_vpath =  Some (Dpvar pvar) }), _)) -> Some pvar
     | _ -> None in
   let loc = State.get_loc () in
-  match Prop.Attribute.get_observer prop e with
+  match Attribute.get_observer prop e with
   | Some (Apred (Aobserver, _)) ->
       (match pvar_opt with
        |  Some pvar when Config.nsnotification_center_checker_backend ->
@@ -1099,12 +1099,12 @@ let check_junk ?original_prop pname tenv prop =
                 let res = ref None in
                 let do_entry e =
                   check_observer_is_unsubscribed_deallocation prop e;
-                  match Prop.Attribute.get_resource prop e with
+                  match Attribute.get_resource prop e with
                   | Some (Apred (Aresource ({ ra_kind = Racquire }) as a, _)) ->
                       L.d_str "ATTRIBUTE: "; PredSymb.d_attribute a; L.d_ln ();
                       res := Some a
                   | _ ->
-                      (match Prop.Attribute.get_undef prop e with
+                      (match Attribute.get_undef prop e with
                        | Some (Apred (Aundef _ as a, _)) ->
                            res := Some a
                        | _ -> ()) in
diff --git a/infer/src/backend/dom.ml b/infer/src/backend/dom.ml
index b66a5295d..859828dcd 100644
--- a/infer/src/backend/dom.ml
+++ b/infer/src/backend/dom.ml
@@ -1642,7 +1642,7 @@ let pi_partial_join mode
     | None -> None
     | Some (a_res, a_op) ->
         if mode = JoinState.Pre then join_atom_check_pre p_op a_op;
-        if Prop.Attribute.is_pred a then join_atom_check_attribute p_op a_op;
+        if Attribute.is_pred a then join_atom_check_attribute p_op a_op;
         if not (Prover.check_atom p_op a_op) then None
         else begin
           match Prop.atom_exp_le_const a_op with
diff --git a/infer/src/backend/errdesc.ml b/infer/src/backend/errdesc.ml
index 0c191d034..f8c22c62a 100644
--- a/infer/src/backend/errdesc.ml
+++ b/infer/src/backend/errdesc.ml
@@ -55,7 +55,7 @@ let is_special_field class_names field_name_opt field =
 (** Check whether the hpred is a |-> representing a resource in the Racquire state *)
 let hpred_is_open_resource prop = function
   | Sil.Hpointsto(e, _, _) ->
-      (match Prop.Attribute.get_resource prop e with
+      (match Attribute.get_resource prop e with
        | Some (Apred (Aresource { ra_kind = Racquire; ra_res = res }, _)) -> Some res
        | _ -> None)
   | _ ->
@@ -847,7 +847,7 @@ let create_dereference_desc
       match de_opt with
       | Some (DExp.Dpvar pvar)
       | Some (DExp.Dpvaraddr pvar) ->
-          (match Prop.Attribute.get_objc_null prop (Exp.Lvar pvar) with
+          (match Attribute.get_objc_null prop (Exp.Lvar pvar) with
            | Some (Apred (Aobjc_null, [_; vfs])) ->
                Localise.parameter_field_not_null_checked_desc desc vfs
            | _ ->
@@ -1047,7 +1047,7 @@ let explain_dereference_as_caller_expression
         if verbose then L.d_strln ("parameter number: " ^ string_of_int position);
         explain_nth_function_parameter use_buckets deref_str actual_pre position pvar_off
       else
-      if Prop.Attribute.has_dangling_uninit spec_pre exp then
+      if Attribute.has_dangling_uninit spec_pre exp then
         Localise.desc_uninitialized_dangling_pointer_deref deref_str (Pvar.to_string pv) loc
       else Localise.no_desc
   | None ->
diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml
index 2b245e1f4..5a3d7ad2a 100644
--- a/infer/src/backend/interproc.ml
+++ b/infer/src/backend/interproc.ml
@@ -773,9 +773,9 @@ let collect_postconditions wl tenv pdesc : Paths.PathSet.t * Specs.Visitedset.t
     | Procname.ObjC_Cpp _ ->
         if (Procname.is_constructor pname) then
           Paths.PathSet.map (fun prop ->
-              let prop = Prop.Attribute.remove_resource Racquire Rfile prop in
-              let prop = Prop.Attribute.remove_resource Racquire (Rmemory Mmalloc) prop in
-              Prop.Attribute.remove_resource Racquire (Rmemory Mobjc) prop
+              Attribute.remove_resource Racquire (Rmemory Mobjc)
+                (Attribute.remove_resource Racquire (Rmemory Mmalloc)
+                   (Attribute.remove_resource Racquire Rfile prop))
             ) pathset
         else pathset
     | _ -> pathset in
diff --git a/infer/src/backend/modelBuiltins.ml b/infer/src/backend/modelBuiltins.ml
index 2cc51cd75..4f76217b4 100644
--- a/infer/src/backend/modelBuiltins.ml
+++ b/infer/src/backend/modelBuiltins.ml
@@ -137,7 +137,7 @@ let execute___print_value { Builtin.pdesc; prop_; path; args; }
 
 let is_undefined_opt prop n_lexp =
   let is_undef =
-    Option.is_some (Prop.Attribute.get_undef prop n_lexp) in
+    Option.is_some (Attribute.get_undef prop n_lexp) in
   is_undef && (Config.angelic_execution || Config.optimistic_cast)
 
 (** Creates an object in the heap with a given type, when the object is not known to be null or when
@@ -311,9 +311,9 @@ let execute___cast builtin_args
   execute___instanceof_cast ~instof:false builtin_args
 
 let set_resource_attribute prop path n_lexp loc ra_res =
-  let prop' = match Prop.Attribute.get_resource prop n_lexp with
+  let prop' = match Attribute.get_resource prop n_lexp with
     | Some (Apred (Aresource ra, _)) ->
-        Prop.Attribute.add_or_replace prop (Apred (Aresource { ra with ra_res }, [n_lexp]))
+        Attribute.add_or_replace prop (Apred (Aresource { ra with ra_res }, [n_lexp]))
     | _ ->
         let pname = PredSymb.mem_alloc_pname PredSymb.Mnew in
         let ra =
@@ -323,7 +323,7 @@ let set_resource_attribute prop path n_lexp loc ra_res =
             ra_pname = pname;
             ra_loc = loc;
             ra_vpath = None } in
-        Prop.Attribute.add_or_replace prop (Apred (Aresource ra, [n_lexp])) in
+        Attribute.add_or_replace prop (Apred (Aresource ra, [n_lexp])) in
   [(prop', path)]
 
 (** Set the attibute of the value as file *)
@@ -545,7 +545,7 @@ let execute___set_autorelease_attribute
       let prop = return_result lexp prop_ ret_ids in
       if Config.objc_memory_model_on then
         let n_lexp, prop = check_arith_norm_exp pname lexp prop in
-        let prop' = Prop.Attribute.add_or_replace prop (Apred (Aautorelease, [n_lexp])) in
+        let prop' = Attribute.add_or_replace prop (Apred (Aautorelease, [n_lexp])) in
         [(prop', path)]
       else execute___no_op prop path
   | _ -> raise (Exceptions.Wrong_argument_number __POS__)
@@ -555,8 +555,8 @@ let execute___release_autorelease_pool
     ({ Builtin.prop_; path; } as builtin_args)
   : Builtin.ret_typ =
   if Config.objc_memory_model_on then
-    let autoreleased_objects = Prop.Attribute.get_for_symb prop_ Aautorelease in
-    let prop_without_attribute = Prop.Attribute.remove_for_attr prop_ Aautorelease in
+    let autoreleased_objects = Attribute.get_for_symb prop_ Aautorelease in
+    let prop_without_attribute = Attribute.remove_for_attr prop_ Aautorelease in
     let call_release res atom =
       match res, atom with
       | ((prop', path') :: _, Sil.Apred (_, exp :: _)) ->
@@ -582,12 +582,12 @@ let execute___release_autorelease_pool
 let set_attr pdesc prop path exp attr =
   let pname = Cfg.Procdesc.get_proc_name pdesc in
   let n_lexp, prop = check_arith_norm_exp pname exp prop in
-  [(Prop.Attribute.add_or_replace prop (Apred (attr, [n_lexp])), path)]
+  [(Attribute.add_or_replace prop (Apred (attr, [n_lexp])), path)]
 
 let delete_attr pdesc prop path exp attr =
   let pname = Cfg.Procdesc.get_proc_name pdesc in
   let n_lexp, prop = check_arith_norm_exp pname exp prop in
-  [(Prop.Attribute.remove prop (Apred (attr, [n_lexp])), path)]
+  [(Attribute.remove prop (Apred (attr, [n_lexp])), path)]
 
 
 (** Set attibute att *)
@@ -694,7 +694,7 @@ let _execute_free mk loc acc iter =
           PredSymb.ra_vpath = None } in
       (* mark value as freed *)
       let p_res =
-        Prop.Attribute.add_or_replace_check_changed
+        Attribute.add_or_replace_check_changed
           Tabulation.check_attr_dealloc_mismatch prop (Apred (Aresource ra, [lexp])) in
       p_res :: acc
   | (Sil.Hpointsto _, _ :: _) -> assert false (* alignment error *)
@@ -796,7 +796,7 @@ let execute_alloc mk can_return_null
         PredSymb.ra_loc = loc;
         PredSymb.ra_vpath = None } in
     (* mark value as allocated *)
-    Prop.Attribute.add_or_replace prop' (Apred (Aresource ra, [exp_new])) in
+    Attribute.add_or_replace prop' (Apred (Aresource ra, [exp_new])) in
   let prop_alloc = Prop.conjoin_eq (Exp.Var ret_id) exp_new prop_plus_ptsto in
   if can_return_null then
     let prop_null = Prop.conjoin_eq (Exp.Var ret_id) Exp.zero prop in
diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml
index c7e926eeb..ae089f7ba 100644
--- a/infer/src/backend/prop.ml
+++ b/infer/src/backend/prop.ml
@@ -430,21 +430,6 @@ let sub_normalize sub =
 let (--) = IntLit.sub
 let (++) = IntLit.add
 
-let iszero_int_float = function
-  | Const.Cint i -> IntLit.iszero i
-  | Const.Cfloat 0.0 -> true
-  | _ -> false
-
-let isone_int_float = function
-  | Const.Cint i -> IntLit.isone i
-  | Const.Cfloat 1.0 -> true
-  | _ -> false
-
-let isminusone_int_float = function
-  | Const.Cint i -> IntLit.isminusone i
-  | Const.Cfloat (-1.0) -> true
-  | _ -> false
-
 let sym_eval abs e =
   let rec eval e =
     (* L.d_str " ["; Sil.d_exp e; L.d_str"] "; *)
@@ -622,9 +607,9 @@ let sym_eval abs e =
             when isPlusA && (extensible_array_element_typ_equal elt typ) ->
               let len = match len1_opt with Some len1 -> len1 +++ len2 | None -> len2 in
               Exp.Sizeof (typ, Some len, st)
-          | Exp.Const c, _ when iszero_int_float c ->
+          | Exp.Const c, _ when Const.iszero_int_float c ->
               e2'
-          | _, Exp.Const c when iszero_int_float c ->
+          | _, Exp.Const c when Const.iszero_int_float c ->
               e1'
           | Exp.Const (Const.Cint n), Exp.Const (Const.Cint m) ->
               Exp.int (n ++ m)
@@ -666,9 +651,9 @@ let sym_eval abs e =
         if Exp.equal e1' e2' then Exp.zero
         else begin
           match e1', e2' with
-          | Exp.Const c, _ when iszero_int_float c ->
+          | Exp.Const c, _ when Const.iszero_int_float c ->
               eval (Exp.UnOp(Unop.Neg, e2', None))
-          | _, Exp.Const c when iszero_int_float c ->
+          | _, Exp.Const c when Const.iszero_int_float c ->
               e1'
           | Exp.Const (Const.Cint n), Exp.Const (Const.Cint m) ->
               Exp.int (n -- m)
@@ -693,17 +678,17 @@ let sym_eval abs e =
         let e2' = eval e2 in
         begin
           match e1', e2' with
-          | Exp.Const c, _ when iszero_int_float c ->
+          | Exp.Const c, _ when Const.iszero_int_float c ->
               Exp.zero
-          | Exp.Const c, _ when isone_int_float c ->
+          | Exp.Const c, _ when Const.isone_int_float c ->
               e2'
-          | Exp.Const c, _ when isminusone_int_float c ->
+          | Exp.Const c, _ when Const.isminusone_int_float c ->
               eval (Exp.UnOp (Unop.Neg, e2', None))
-          | _, Exp.Const c when iszero_int_float c ->
+          | _, Exp.Const c when Const.iszero_int_float c ->
               Exp.zero
-          | _, Exp.Const c when isone_int_float c ->
+          | _, Exp.Const c when Const.isone_int_float c ->
               e1'
-          | _, Exp.Const c when isminusone_int_float c ->
+          | _, Exp.Const c when Const.isminusone_int_float c ->
               eval (Exp.UnOp (Unop.Neg, e1', None))
           | Exp.Const (Const.Cint n), Exp.Const (Const.Cint m) ->
               Exp.int (IntLit.mul n m)
@@ -722,11 +707,11 @@ let sym_eval abs e =
         let e2' = eval e2 in
         begin
           match e1', e2' with
-          | _, Exp.Const c when iszero_int_float c ->
+          | _, Exp.Const c when Const.iszero_int_float c ->
               Exp.get_undefined false
-          | Exp.Const c, _ when iszero_int_float c ->
+          | Exp.Const c, _ when Const.iszero_int_float c ->
               e1'
-          | _, Exp.Const c when isone_int_float c ->
+          | _, Exp.Const c when Const.isone_int_float c ->
               e1'
           | Exp.Const (Const.Cint n), Exp.Const (Const.Cint m) ->
               Exp.int (IntLit.div n m)
@@ -1773,275 +1758,6 @@ let prop_reset_inst inst_map prop =
   let sigma_fp' = IList.map (Sil.hpred_instmap inst_map) (get_sigma_footprint prop) in
   replace_sigma_footprint sigma_fp' (replace_sigma sigma' prop)
 
-(** {2 Attributes} *)
-module Attribute = struct
-
-  (** Check whether an atom is used to mark an attribute *)
-  let is_pred atom =
-    match atom with
-    | Sil.Apred _ | Anpred _ -> true
-    | _ -> false
-
-  (** Add an attribute associated to the argument expressions *)
-  let add ?(footprint = false) ?(polarity = true) prop attr args =
-    prop_atom_and ~footprint prop
-      (if polarity then Sil.Apred (attr, args) else Sil.Anpred (attr, args))
-
-  let attributes_in_same_category attr1 attr2 =
-    let cat1 = PredSymb.to_category attr1 in
-    let cat2 = PredSymb.to_category attr2 in
-    PredSymb.category_equal cat1 cat2
-
-  (** Replace an attribute associated to the expression *)
-  let add_or_replace_check_changed check_attribute_change prop atom0 =
-    match atom0 with
-    | Sil.Apred (att0, ((_ :: _) as exps0)) | Anpred (att0, ((_ :: _) as exps0)) ->
-        let nexps = IList.map (fun e -> exp_normalize_prop prop e) exps0 in
-        let nexp = IList.hd nexps in (* len nexps = len exps0 > 0 by match *)
-        let natom = Sil.atom_replace_exp (IList.combine exps0 nexps) atom0 in
-        let atom_map = function
-          | Sil.Apred (att, exp :: _) | Anpred (att, exp :: _)
-            when Exp.equal nexp exp && attributes_in_same_category att att0 ->
-              check_attribute_change att att0;
-              natom
-          | atom ->
-              atom in
-        let pi = get_pi prop in
-        let pi' = IList.map_changed atom_map pi in
-        if pi == pi'
-        then prop_atom_and prop natom
-        else replace_pi pi' prop
-    | _ ->
-        prop
-
-  let add_or_replace prop atom =
-    (* wrapper for the most common case: do nothing *)
-    let check_attr_changed = (fun _ _ -> ()) in
-    add_or_replace_check_changed check_attr_changed prop atom
-
-  (** Get all the attributes of the prop *)
-  let get_all prop =
-    let res = ref [] in
-    let do_atom a = if is_pred a then res := a :: !res in
-    IList.iter do_atom prop.pi;
-    IList.rev !res
-
-  (** Get all the attributes of the prop *)
-  let get_for_symb prop att =
-    IList.filter (function
-        | Sil.Apred (att', _) | Anpred (att', _) -> PredSymb.equal att' att
-        | _ -> false
-      ) (get_pi prop)
-
-  (** Get the attribute associated to the expression, if any *)
-  let get_for_exp prop exp =
-    let nexp = exp_normalize_prop prop exp in
-    let atom_get_attr attributes atom =
-      match atom with
-      | Sil.Apred (_, es) | Anpred (_, es) when IList.mem Exp.equal nexp es -> atom :: attributes
-      | _ -> attributes in
-    IList.fold_left atom_get_attr [] prop.pi
-
-  let get prop exp category =
-    let atts = get_for_exp prop exp in
-    try
-      Some
-        (IList.find (function
-             | Sil.Apred (att, _) | Anpred (att, _) ->
-                 PredSymb.category_equal (PredSymb.to_category att) category
-             | _ -> false
-           ) atts)
-    with Not_found -> None
-
-  let get_undef prop exp =
-    get prop exp ACundef
-
-  let get_resource prop exp =
-    get prop exp ACresource
-
-  let get_taint prop exp =
-    get prop exp ACtaint
-
-  let get_autorelease prop exp =
-    get prop exp ACautorelease
-
-  let get_objc_null prop exp =
-    get prop exp ACobjc_null
-
-  let get_div0 prop exp =
-    get prop exp ACdiv0
-
-  let get_observer prop exp =
-    get prop exp ACobserver
-
-  let get_retval prop exp =
-    get prop exp ACretval
-
-  let has_dangling_uninit prop exp =
-    let la = get_for_exp prop exp in
-    IList.exists (function
-        | Sil.Apred (a, _) -> PredSymb.equal a (Adangling DAuninit)
-        | _ -> false
-      ) la
-
-  let filter_atoms ~f prop =
-    replace_pi (IList.filter f (get_pi prop)) prop
-
-  let remove prop atom =
-    match atom with
-    | Sil.Apred (_, exps) | Anpred (_, exps) ->
-        let nexps = IList.map (fun e -> exp_normalize_prop prop e) exps in
-        let natom = Sil.atom_replace_exp (IList.combine exps nexps) atom in
-        let f a = not (Sil.atom_equal natom a) in
-        filter_atoms ~f prop
-    | _ ->
-        replace_pi (get_pi prop) prop
-
-  (** Remove an attribute from all the atoms in the heap *)
-  let remove_for_attr prop att0 =
-    let f = function
-      | Sil.Apred (att, _) | Anpred (att, _) -> not (PredSymb.equal att0 att)
-      | _ -> true in
-    filter_atoms ~f prop
-
-  let remove_resource ra_kind ra_res =
-    let f = function
-      | Sil.Apred (Aresource res_action, _) ->
-          PredSymb.res_act_kind_compare res_action.ra_kind ra_kind <> 0
-          || PredSymb.resource_compare res_action.ra_res ra_res <> 0
-      | _ -> true in
-    filter_atoms ~f
-
-  (** Apply f to every resource attribute in the prop *)
-  let map_resource prop f =
-    let attribute_map e = function
-      | PredSymb.Aresource ra -> PredSymb.Aresource (f e ra)
-      | att -> att in
-    let atom_map = function
-      | Sil.Apred (att, ([e] as es)) -> Sil.Apred (attribute_map e att, es)
-      | Sil.Anpred (att, ([e] as es)) -> Sil.Anpred (attribute_map e att, es)
-      | atom -> atom in
-    replace_pi (IList.map atom_map (get_pi prop)) prop
-
-  (* Replace an attribute OBJC_NULL($n1) with OBJC_NULL(var) when var = $n1, and also sets $n1 =
-     0 *)
-  let replace_objc_null prop lhs_exp rhs_exp =
-    match get_objc_null prop rhs_exp, rhs_exp with
-    | Some atom, Exp.Var _ ->
-        let prop = remove prop atom in
-        let prop = conjoin_eq rhs_exp Exp.zero prop in
-        let natom = Sil.atom_replace_exp [(rhs_exp, lhs_exp)] atom in
-        add_or_replace prop natom
-    | _ -> prop
-
-  let rec nullify_exp_with_objc_null prop exp =
-    match exp with
-    | Exp.BinOp (_, exp1, exp2) ->
-        let prop' = nullify_exp_with_objc_null prop exp1 in
-        nullify_exp_with_objc_null prop' exp2
-    | Exp.UnOp (_, exp, _) ->
-        nullify_exp_with_objc_null prop exp
-    | Exp.Var _ ->
-        (match get_objc_null prop exp with
-         | Some atom ->
-             let prop' = remove prop atom in
-             conjoin_eq exp Exp.zero prop'
-         | _ -> prop)
-    | _ -> prop
-
-  (** mark Exp.Var's or Exp.Lvar's as undefined *)
-  let mark_vars_as_undefined prop vars_to_mark callee_pname ret_annots loc path_pos =
-    let att_undef = PredSymb.Aundef (callee_pname, ret_annots, loc, path_pos) in
-    let mark_var_as_undefined exp prop =
-      match exp with
-      | Exp.Var _ | Lvar _ -> add_or_replace prop (Apred (att_undef, [exp]))
-      | _ -> prop in
-    IList.fold_left (fun prop id -> mark_var_as_undefined id prop) prop vars_to_mark
-
-end
-
-(** type for arithmetic problems *)
-type arith_problem =
-  (* division by zero *)
-  | Div0 of Exp.t
-
-  (* unary minus of unsigned type applied to the given expression *)
-  | UminusUnsigned of Exp.t * Typ.t
-
-(** Look for an arithmetic problem in [exp] *)
-let find_arithmetic_problem proc_node_session prop exp =
-  let exps_divided = ref [] in
-  let uminus_unsigned = ref [] in
-  let res = ref prop in
-  let check_zero e =
-    match exp_normalize_prop prop e with
-    | Exp.Const c when iszero_int_float c -> true
-    | _ ->
-        res := Attribute.add_or_replace !res (Apred (Adiv0 proc_node_session, [e]));
-        false in
-  let rec walk = function
-    | Exp.Var _ -> ()
-    | Exp.UnOp (Unop.Neg, e, Some (
-        (Typ.Tint
-           (Typ.IUChar | Typ.IUInt | Typ.IUShort | Typ.IULong | Typ.IULongLong) as typ))) ->
-        uminus_unsigned := (e, typ) :: !uminus_unsigned
-    | Exp.UnOp(_, e, _) -> walk e
-    | Exp.BinOp(op, e1, e2) ->
-        if op = Binop.Div || op = Binop.Mod then exps_divided := e2 :: !exps_divided;
-        walk e1; walk e2
-    | Exp.Exn _ -> ()
-    | Exp.Closure _ -> ()
-    | Exp.Const _ -> ()
-    | Exp.Cast (_, e) -> walk e
-    | Exp.Lvar _ -> ()
-    | Exp.Lfield (e, _, _) -> walk e
-    | Exp.Lindex (e1, e2) -> walk e1; walk e2
-    | Exp.Sizeof (_, None, _) -> ()
-    | Exp.Sizeof (_, Some len, _) -> walk len in
-  walk exp;
-  try Some (Div0 (IList.find check_zero !exps_divided)), !res
-  with Not_found ->
-    (match !uminus_unsigned with
-     | (e, t):: _ -> Some (UminusUnsigned (e, t)), !res
-     | _ -> None, !res)
-
-(** Deallocate the stack variables in [pvars], and replace them by normal variables.
-    Return the list of stack variables whose address was still present after deallocation. *)
-let deallocate_stack_vars p pvars =
-  let filter = function
-    | Sil.Hpointsto (Exp.Lvar v, _, _) ->
-        IList.exists (Pvar.equal v) pvars
-    | _ -> false in
-  let sigma_stack, sigma_other = IList.partition filter p.sigma in
-  let fresh_address_vars = ref [] in (* fresh vars substituted for the address of stack vars *)
-  let stack_vars_address_in_post = ref [] in (* stack vars whose address is still present *)
-  let exp_replace = IList.map (function
-      | Sil.Hpointsto (Exp.Lvar v, _, _) ->
-          let freshv = Ident.create_fresh Ident.kprimed in
-          fresh_address_vars := (v, freshv) :: !fresh_address_vars;
-          (Exp.Lvar v, Exp.Var freshv)
-      | _ -> assert false) sigma_stack in
-  let pi1 = IList.map (fun (id, e) -> Sil.Aeq (Exp.Var id, e)) (Sil.sub_to_list p.sub) in
-  let pi = IList.map (Sil.atom_replace_exp exp_replace) (p.pi @ pi1) in
-  let p' =
-    { p with
-      sub = Sil.sub_empty;
-      pi = [];
-      sigma = sigma_replace_exp exp_replace sigma_other } in
-  let p'' =
-    let res = ref p' in
-    let p'_fav = prop_fav p' in
-    let do_var (v, freshv) =
-      if Sil.fav_mem p'_fav freshv then (* the address of a de-allocated stack var in in the post *)
-        begin
-          stack_vars_address_in_post := v :: !stack_vars_address_in_post;
-          let pred = Sil.Apred (Adangling DAaddr_stack_var, [Exp.Var freshv]) in
-          res := Attribute.add_or_replace !res pred
-        end in
-    IList.iter do_var !fresh_address_vars;
-    !res in
-  !stack_vars_address_in_post, IList.fold_left prop_atom_and p'' pi
-
 
 (** {1 Functions for transforming footprints into propositions.} *)
 
@@ -2802,43 +2518,6 @@ let trans_land_lor op ((idl1, stml1), e1) ((idl2, stml2), e2) loc =
       ((id:: idl1@idl2, stml1@instrs2), Exp.Var id)
     end
 
-(** Input of this method is an exp in a prop. Output is a formal variable or path from a
-    formal variable that is equal to the expression,
-    or the OBJC_NULL attribute of the expression. *)
-let find_equal_formal_path e prop =
-  let rec find_in_sigma e seen_hpreds =
-    IList.fold_right (
-      fun hpred res ->
-        if IList.mem Sil.hpred_equal hpred seen_hpreds then None
-        else
-          let seen_hpreds = hpred :: seen_hpreds in
-          match res with
-          | Some _ -> res
-          | None ->
-              match hpred with
-              | Sil.Hpointsto (Exp.Lvar pvar1, Sil.Eexp (exp2, Sil.Iformal(_, _) ), _)
-                when Exp.equal exp2 e &&
-                     (Pvar.is_local pvar1 || Pvar.is_seed pvar1) ->
-                  Some (Exp.Lvar pvar1)
-              | Sil.Hpointsto (exp1, Sil.Estruct (fields, _), _) ->
-                  IList.fold_right (fun (field, strexp) res ->
-                      match res with
-                      | Some _ -> res
-                      | None ->
-                          match strexp with
-                          | Sil.Eexp (exp2, _) when Exp.equal exp2 e ->
-                              (match find_in_sigma exp1 seen_hpreds with
-                               | Some vfs -> Some (Exp.Lfield (vfs, field, Typ.Tvoid))
-                               | None -> None)
-                          | _ -> None) fields None
-              | _ -> None) (get_sigma prop) None in
-  match find_in_sigma e [] with
-  | Some vfs -> Some vfs
-  | None ->
-      match Attribute.get_objc_null prop e with
-      | Some (Apred (Aobjc_null, [_; vfs])) -> Some vfs
-      | _ -> None
-
 (** translate an if-then-else expression *)
 let trans_if_then_else ((idl1, stml1), e1) ((idl2, stml2), e2) ((idl3, stml3), e3) loc =
   match sym_eval false e1 with
diff --git a/infer/src/backend/prop.mli b/infer/src/backend/prop.mli
index 632b8e61a..642a7d9b5 100644
--- a/infer/src/backend/prop.mli
+++ b/infer/src/backend/prop.mli
@@ -160,18 +160,6 @@ val atom_const_lt_exp : Sil.atom -> (IntLit.t * Exp.t) option
 (** Negate an atom *)
 val atom_negate : Sil.atom -> Sil.atom
 
-(** type for arithmetic problems *)
-type arith_problem =
-  (* division by zero *)
-  | Div0 of Exp.t
-
-  (* unary minus of unsigned type applied to the given expression *)
-  | UminusUnsigned of Exp.t * Typ.t
-
-(** Look for an arithmetic problem in [exp] *)
-val find_arithmetic_problem :
-  PredSymb.path_pos -> normal t -> Exp.t -> arith_problem option * normal t
-
 (** Normalize [exp] using the pure part of [prop].  Later, we should
     change this such that the normalization exposes offsets of [exp]
     as much as possible. *)
@@ -280,85 +268,6 @@ val conjoin_eq : ?footprint: bool -> Exp.t -> Exp.t -> normal t -> normal t
 (** Conjoin [exp1]!=[exp2] with a symbolic heap [prop]. *)
 val conjoin_neq : ?footprint: bool -> Exp.t -> Exp.t -> normal t -> normal t
 
-module Attribute : sig
-
-  (** Check whether an atom is used to mark an attribute *)
-  val is_pred : atom -> bool
-
-  (** Add an attribute associated to the argument expressions *)
-  val add : ?footprint: bool -> ?polarity: bool -> normal t -> PredSymb.t -> Exp.t list -> normal t
-
-  (** Replace an attribute associated to the expression *)
-  val add_or_replace : normal t -> atom -> normal t
-
-  (** Replace an attribute associated to the expression, and call the given function with new and
-      old attributes if they changed. *)
-  val add_or_replace_check_changed :
-    (PredSymb.t -> PredSymb.t -> unit) -> normal t -> atom -> normal t
-
-  (** Get all the attributes of the prop *)
-  val get_all : 'a t -> atom list
-
-  (** Get the attributes associated to the expression, if any *)
-  val get_for_exp : 'a t -> Exp.t -> atom list
-
-  (** Retrieve all the atoms that contain a specific attribute *)
-  val get_for_symb : 'a t -> PredSymb.t -> Sil.atom list
-
-  (** Get the autorelease attribute associated to the expression, if any *)
-  val get_autorelease : 'a t -> Exp.t -> atom option
-
-  (** Get the div0 attribute associated to the expression, if any *)
-  val get_div0 : 'a t -> Exp.t -> atom option
-
-  (** Get the objc null attribute associated to the expression, if any *)
-  val get_objc_null : 'a t -> Exp.t -> atom option
-
-  (** Get the observer attribute associated to the expression, if any *)
-  val get_observer : 'a t -> Exp.t -> atom option
-
-  (** Get the resource attribute associated to the expression, if any *)
-  val get_resource : 'a t -> Exp.t -> atom option
-
-  (** Get the retval null attribute associated to the expression, if any *)
-  val get_retval : 'a t -> Exp.t -> atom option
-
-  (** Get the taint attribute associated to the expression, if any *)
-  val get_taint : 'a t -> Exp.t -> atom option
-
-  (** Get the undef attribute associated to the expression, if any *)
-  val get_undef : 'a t -> Exp.t -> atom option
-
-  (** Test for existence of an Adangling DAuninit attribute associated to the exp *)
-  val has_dangling_uninit : 'a t -> Exp.t -> bool
-
-  (** Remove an attribute *)
-  val remove : 'a t -> atom -> normal t
-
-  (** Remove all attributes for the given attr *)
-  val remove_for_attr : 'a t -> PredSymb.t -> normal t
-
-  (** Remove all attributes for the given resource and kind *)
-  val remove_resource : PredSymb.res_act_kind -> PredSymb.resource -> 'a t -> normal t
-
-  (** Apply f to every resource attribute in the prop *)
-  val map_resource : normal t -> (Exp.t -> PredSymb.res_action -> PredSymb.res_action) -> normal t
-
-  (** [replace_objc_null lhs rhs].
-      If rhs has the objc_null attribute, replace the attribute and set the lhs = 0 *)
-  val replace_objc_null : normal t -> Exp.t -> Exp.t -> normal t
-
-  (** For each Var subexp of the argument with an Aobjc_null attribute,
-      remove the attribute and conjoin an equality to zero. *)
-  val nullify_exp_with_objc_null : normal t -> Exp.t -> normal t
-
-  (** mark Exp.Var's or Exp.Lvar's as undefined *)
-  val mark_vars_as_undefined :
-    normal t -> Exp.t list -> Procname.t -> Typ.item_annotation -> Location.t ->
-    PredSymb.path_pos -> normal t
-
-end
-
 (** Return the sub part of [prop]. *)
 val get_sub : 'a t -> subst
 
@@ -377,10 +286,6 @@ val get_pi_footprint : 'a t -> atom list
 (** Return the sigma part of the footprint of [prop] *)
 val get_sigma_footprint : 'a t -> hpred list
 
-(** Deallocate the stack variables in [pvars], and replace them by normal variables.
-    Return the list of stack variables whose address was still present after deallocation. *)
-val deallocate_stack_vars : normal t -> Pvar.t list -> Pvar.t list * normal t
-
 (** Canonicalize the names of primed variables. *)
 val prop_rename_primed_footprint_vars : normal t -> normal t
 
@@ -506,8 +411,6 @@ val prop_iter_make_id_primed : Ident.t -> 'a prop_iter -> 'a prop_iter
 (** Collect garbage fields. *)
 val prop_iter_gc_fields : unit prop_iter -> unit prop_iter
 
-val find_equal_formal_path : Exp.t -> 'a t -> Exp.t option
-
 (** return the set of subexpressions of [strexp] *)
 val strexp_get_exps : Sil.strexp -> Exp.Set.t
 
diff --git a/infer/src/backend/rearrange.ml b/infer/src/backend/rearrange.ml
index 0f6ba23e7..3a3b3c665 100644
--- a/infer/src/backend/rearrange.ml
+++ b/infer/src/backend/rearrange.ml
@@ -746,7 +746,7 @@ let add_guarded_by_constraints prop lexp pdesc =
         (function
           | Sil.Apred (Alocked, _) -> true
           | _ -> false)
-        (Prop.Attribute.get_for_exp prop guarded_by_exp) in
+        (Attribute.get_for_exp prop guarded_by_exp) in
     let should_warn pdesc =
       (* adding this check implements "by reference" semantics for guarded-by rather than "by value"
          semantics. if this access is through a local L or field V.f
@@ -793,7 +793,7 @@ let add_guarded_by_constraints prop lexp pdesc =
           end
         else
           (* private method. add locked proof obligation to [pdesc] *)
-          Prop.Attribute.add ~footprint:true prop Alocked [guarded_by_exp]
+          Attribute.add ~footprint:true prop Alocked [guarded_by_exp]
     | _ ->
         if not (proc_has_matching_annot pdesc guarded_by_str
                 || is_synchronized_on_class guarded_by_str) && should_warn pdesc
@@ -1205,7 +1205,7 @@ let check_dereference_error pdesc (prop : Prop.normal Prop.t) lexp loc =
                        nullable_obj_str := Some (Procname.to_string pname);
                        true
                    | _ -> false in
-                 IList.exists is_nullable_attr (Prop.Attribute.get_for_exp prop exp) in
+                 IList.exists is_nullable_attr (Attribute.get_for_exp prop exp) in
              (* it's ok for a non-nullable local to point to deref_exp *)
              is_nullable || Pvar.is_local pvar
          | Sil.Hpointsto (_, Sil.Estruct (flds, _), Exp.Sizeof (typ, _, _)) ->
@@ -1232,8 +1232,8 @@ let check_dereference_error pdesc (prop : Prop.normal Prop.t) lexp loc =
     Config.report_nullable_inconsistency && not (is_definitely_non_null root prop)
     && is_only_pt_by_nullable_fld_or_param root in
   let relevant_attributes_getters = [
-    Prop.Attribute.get_resource;
-    Prop.Attribute.get_undef;
+    Attribute.get_resource;
+    Attribute.get_undef;
   ] in
   let get_relevant_attributes exp =
     let rec fold_getters = function
diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml
index 9917821db..6448d6650 100644
--- a/infer/src/backend/symExec.ml
+++ b/infer/src/backend/symExec.ml
@@ -109,7 +109,7 @@ let rec apply_offlist
             lookup_inst := Some inst_curr;
             let alloc_attribute_opt =
               if inst_curr = Sil.Iinitial then None
-              else Prop.Attribute.get_undef p root_lexp in
+              else Attribute.get_undef p root_lexp in
             let deref_str = Localise.deref_str_uninitialized alloc_attribute_opt in
             let err_desc = Errdesc.explain_memory_access deref_str p (State.get_loc ()) in
             let exn = (Exceptions.Uninitialized_value (err_desc, __POS__)) in
@@ -418,14 +418,14 @@ let check_constant_string_dereference lexp =
 
 (** Normalize an expression and check for arithmetic problems *)
 let check_arith_norm_exp pname exp prop =
-  match Prop.find_arithmetic_problem (State.get_path_pos ()) prop exp with
-  | Some (Prop.Div0 div), prop' ->
+  match Attribute.find_arithmetic_problem (State.get_path_pos ()) prop exp with
+  | Some (Attribute.Div0 div), prop' ->
       let desc = Errdesc.explain_divide_by_zero div (State.get_node ()) (State.get_loc ()) in
       let exn = Exceptions.Divide_by_zero (desc, __POS__) in
       let pre_opt = State.get_normalized_pre (Abs.abstract_no_symop pname) in
       Reporting.log_warning pname ~pre: pre_opt exn;
       Prop.exp_normalize_prop prop exp, prop'
-  | Some (Prop.UminusUnsigned (e, typ)), prop' ->
+  | Some (Attribute.UminusUnsigned (e, typ)), prop' ->
       let desc =
         Errdesc.explain_unary_minus_applied_to_unsigned_expression
           e typ (State.get_node ()) (State.get_loc ()) in
@@ -484,7 +484,7 @@ let check_deallocate_static_memory prop_after =
         let freed_desc = Errdesc.explain_deallocate_constant_string s ra in
         raise (Exceptions.Deallocate_static_memory freed_desc)
     | _ -> () in
-  let exp_att_list = Prop.Attribute.get_all prop_after in
+  let exp_att_list = Attribute.get_all prop_after in
   IList.iter check_deallocated_attribute exp_att_list;
   prop_after
 
@@ -731,14 +731,14 @@ let handle_objc_instance_method_call_or_skip actual_pars path callee_pname pre r
     match actual_pars with
     | (e, _) :: _
       when Exp.equal e Exp.zero ||
-           Option.is_some (Prop.Attribute.get_objc_null pre e) -> true
+           Option.is_some (Attribute.get_objc_null pre e) -> true
     | _ -> false in
   let add_objc_null_attribute_or_nullify_result prop =
     match ret_ids with
     | [ret_id] -> (
-        match Prop.find_equal_formal_path receiver prop with
+        match Attribute.find_equal_formal_path receiver prop with
         | Some vfs ->
-            Prop.Attribute.add_or_replace prop (Apred (Aobjc_null, [Exp.Var ret_id; vfs]))
+            Attribute.add_or_replace prop (Apred (Aobjc_null, [Exp.Var ret_id; vfs]))
         | None ->
             Prop.conjoin_eq (Exp.Var ret_id) Exp.zero prop
       )
@@ -756,7 +756,7 @@ let handle_objc_instance_method_call_or_skip actual_pars path callee_pname pre r
        so that in a NPE we can separate it into a different error type *)
     [(add_objc_null_attribute_or_nullify_result pre, path)]
   else
-    let is_undef = Option.is_some (Prop.Attribute.get_undef pre receiver) in
+    let is_undef = Option.is_some (Attribute.get_undef pre receiver) in
     if !Config.footprint && not is_undef then
       let res_null = (* returns: (objc_null(res) /\ receiver=0) or an empty list of results *)
         let pre_with_attr_or_null = add_objc_null_attribute_or_nullify_result pre in
@@ -843,7 +843,7 @@ let add_constraints_on_retval pdesc prop ret_exp ~has_nullable_annot typ callee_
         | Typ.Tptr _ -> Prop.conjoin_neq exp Exp.zero prop
         | _ -> prop in
     let add_tainted_post ret_exp callee_pname prop =
-      Prop.Attribute.add_or_replace prop (Apred (Ataint callee_pname, [ret_exp])) in
+      Attribute.add_or_replace prop (Apred (Ataint callee_pname, [ret_exp])) in
 
     if Config.angelic_execution && not (is_rec_call callee_pname) then
       (* introduce a fresh program variable to allow abduction on the return value *)
@@ -872,7 +872,7 @@ let add_taint prop lhs_id rhs_exp pname tenv  =
     if Taint.has_taint_annotation fieldname struct_typ
     then
       let taint_info = { PredSymb.taint_source = pname; taint_kind = Tk_unknown; } in
-      Prop.Attribute.add_or_replace prop (Apred (Ataint taint_info, [Exp.Var lhs_id]))
+      Attribute.add_or_replace prop (Apred (Ataint taint_info, [Exp.Var lhs_id]))
     else
       prop in
   match rhs_exp with
@@ -903,7 +903,7 @@ let execute_letderef ?(report_deref_errors=true) pname pdesc tenv id rhs_exp typ
           let prop' = Prop.prop_iter_to_prop iter' in
           let prop'' =
             if lookup_uninitialized then
-              Prop.Attribute.add_or_replace prop' (Apred (Adangling DAuninit, [Exp.Var id]))
+              Attribute.add_or_replace prop' (Apred (Adangling DAuninit, [Exp.Var id]))
             else prop' in
           let prop''' =
             if Config.taint_analysis
@@ -936,7 +936,7 @@ let execute_letderef ?(report_deref_errors=true) pname pdesc tenv id rhs_exp typ
             match callee_opt, atom with
             | None, Sil.Apred (Aundef _, _) -> Some atom
             | _ -> callee_opt in
-          IList.fold_left fold_undef_pname None (Prop.Attribute.get_for_exp prop exp) in
+          IList.fold_left fold_undef_pname None (Attribute.get_for_exp prop exp) in
         let prop' =
           if Config.angelic_execution then
             (* when we try to deref an undefined value, add it to the footprint *)
@@ -985,7 +985,7 @@ let execute_set ?(report_deref_errors=true) pname pdesc tenv lhs_exp typ rhs_exp
   try
     let n_lhs_exp, prop_' = check_arith_norm_exp pname lhs_exp prop_ in
     let n_rhs_exp, prop = check_arith_norm_exp pname rhs_exp prop_' in
-    let prop = Prop.Attribute.replace_objc_null prop n_lhs_exp n_rhs_exp in
+    let prop = Attribute.replace_objc_null prop n_lhs_exp n_rhs_exp in
     let n_lhs_exp' = Prop.exp_collapse_consecutive_indices_prop typ n_lhs_exp in
     let iter_list = Rearrange.rearrange ~report_deref_errors pdesc tenv n_lhs_exp' typ prop loc in
     IList.rev (IList.fold_left (execute_set_ pdesc tenv n_rhs_exp) [] iter_list)
@@ -1045,7 +1045,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
       execute_set current_pname current_pdesc tenv lhs_exp typ rhs_exp loc prop_
       |> ret_old_path
   | Sil.Prune (cond, loc, true_branch, ik) ->
-      let prop__ = Prop.Attribute.nullify_exp_with_objc_null prop_ cond in
+      let prop__ = Attribute.nullify_exp_with_objc_null prop_ cond in
       let check_condition_always_true_false () =
         let report_condition_always_true_false i =
           let skip_loop = match ik with
@@ -1362,7 +1362,7 @@ and add_constraints_on_actuals_by_ref tenv prop actuals_by_ref callee_pname call
     IList.fold_left (fun p var -> havoc_actual_by_ref var p) prop actuals_by_ref
 
 and check_untainted exp taint_kind caller_pname callee_pname prop =
-  match Prop.Attribute.get_taint prop exp with
+  match Attribute.get_taint prop exp with
   | Some (Apred (Ataint taint_info, _)) ->
       let err_desc =
         Errdesc.explain_tainted_value_reaching_sensitive_function
@@ -1375,12 +1375,12 @@ and check_untainted exp taint_kind caller_pname callee_pname prop =
         Exceptions.Tainted_value_reaching_sensitive_function
           (err_desc, __POS__) in
       Reporting.log_warning caller_pname exn;
-      Prop.Attribute.add_or_replace prop (Apred (Auntaint taint_info, [exp]))
+      Attribute.add_or_replace prop (Apred (Auntaint taint_info, [exp]))
   | _ ->
       if !Config.footprint then
         let taint_info = { PredSymb.taint_source = callee_pname; taint_kind; } in
         (* add untained(n_lexp) to the footprint *)
-        Prop.Attribute.add ~footprint:true prop (Auntaint taint_info) [exp]
+        Attribute.add ~footprint:true prop (Auntaint taint_info) [exp]
       else prop
 
 (** execute a call for an unknown or scan function *)
@@ -1391,9 +1391,9 @@ and unknown_or_scan_call ~is_scan ret_type_option ret_annots
     let do_exp p (e, _) =
       let do_attribute q atom =
         match atom with
-        | Sil.Apred ((Aresource {ra_res = Rfile} as res), _) -> Prop.Attribute.remove_for_attr q res
+        | Sil.Apred ((Aresource {ra_res = Rfile} as res), _) -> Attribute.remove_for_attr q res
         | _ -> q in
-      IList.fold_left do_attribute p (Prop.Attribute.get_for_exp p e) in
+      IList.fold_left do_attribute p (Attribute.get_for_exp p e) in
     let filtered_args =
       match args, instr with
       | _:: other_args, Sil.Call (_, _, _, _, { CallFlags.cf_virtual }) when cf_virtual ->
@@ -1451,7 +1451,7 @@ and unknown_or_scan_call ~is_scan ret_type_option ret_annots
         (fun exps_to_mark (exp, _) -> exp :: exps_to_mark) ret_exps actuals_by_ref in
     let prop_with_undef_attr =
       let path_pos = State.get_path_pos () in
-      Prop.Attribute.mark_vars_as_undefined
+      Attribute.mark_vars_as_undefined
         pre_final exps_to_mark callee_pname ret_annots loc path_pos in
     [(prop_with_undef_attr, path)]
 
@@ -1641,7 +1641,7 @@ and sym_exec_wrapper handle_exn tenv pdesc instr ((prop: Prop.normal Prop.t), pa
         let map_res_action e ra = (* update the vpath in resource attributes *)
           let vpath, _ = Errdesc.vpath_find p' e in
           { ra with PredSymb.ra_vpath = vpath } in
-        Prop.Attribute.map_resource p' map_res_action in
+        Attribute.map_resource p' map_res_action in
       p'', fav in
     let post_process_result fav_normal p path =
       let p' = prop_normal_to_primed fav_normal p in
diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml
index cf8fcfb53..540218ac6 100644
--- a/infer/src/backend/tabulation.ml
+++ b/infer/src/backend/tabulation.ml
@@ -313,15 +313,15 @@ let check_dereferences callee_pname actual_pre sub spec_pre formal_params =
     else
       (* Check if the dereferenced expr has the dangling uninitialized attribute. *)
       (* In that case it raise a dangling pointer dereferece *)
-    if Prop.Attribute.has_dangling_uninit spec_pre e then
+    if Attribute.has_dangling_uninit spec_pre e then
       Some (Deref_undef_exp, desc false (Localise.deref_str_dangling (Some PredSymb.DAuninit)) )
     else if Exp.equal e_sub Exp.minus_one
     then Some (Deref_minusone, desc true (Localise.deref_str_dangling None))
-    else match Prop.Attribute.get_resource actual_pre e_sub with
+    else match Attribute.get_resource actual_pre e_sub with
       | Some (Apred (Aresource ({ ra_kind = Rrelease } as ra), _)) ->
           Some (Deref_freed ra, desc true (Localise.deref_str_freed ra))
       | _ ->
-          (match Prop.Attribute.get_undef actual_pre e_sub with
+          (match Attribute.get_undef actual_pre e_sub with
            | Some (Apred (Aundef (s, _, loc, pos), _)) ->
                Some (Deref_undef (s, loc, pos), desc false (Localise.deref_str_undef (s, loc)))
            | _ -> None) in
@@ -375,14 +375,14 @@ let check_path_errors_in_post caller_pname post post_path =
           let pre_opt = State.get_normalized_pre (fun _ p -> p) (* Abs.abstract_no_symop *) in
           Reporting.log_warning caller_pname ~pre: pre_opt exn
     | _ -> () in
-  IList.iter check_attr (Prop.Attribute.get_all post)
+  IList.iter check_attr (Attribute.get_all post)
 
 (** Post process the instantiated post after the function call so that
     x.f |-> se becomes x |-> \{ f: se \}.
     Also, update any Aresource attributes to refer to the caller *)
 let post_process_post
     caller_pname callee_pname loc actual_pre ((post: Prop.exposed Prop.t), post_path) =
-  let actual_pre_has_freed_attribute e = match Prop.Attribute.get_resource actual_pre e with
+  let actual_pre_has_freed_attribute e = match Attribute.get_resource actual_pre e with
     | Some (Apred (Aresource ({ ra_kind = Rrelease }), _)) -> true
     | _ -> false in
   let atom_update_alloc_attribute = function
@@ -599,12 +599,12 @@ let prop_copy_footprint_pure p1 p2 =
     Prop.replace_sigma_footprint
       (Prop.get_sigma_footprint p1) (Prop.replace_pi_footprint (Prop.get_pi_footprint p1) p2) in
   let pi2 = Prop.get_pi p2' in
-  let pi2_attr, pi2_noattr = IList.partition Prop.Attribute.is_pred pi2 in
+  let pi2_attr, pi2_noattr = IList.partition Attribute.is_pred pi2 in
   let res_noattr = Prop.replace_pi (Prop.get_pure p1 @ pi2_noattr) p2' in
   let replace_attr prop atom = (* call replace_atom_attribute which deals with existing attibutes *)
     (* if [atom] represents an attribute [att], add the attribure to [prop] *)
-    if Prop.Attribute.is_pred atom then
-      Prop.Attribute.add_or_replace_check_changed check_attr_dealloc_mismatch prop atom
+    if Attribute.is_pred atom then
+      Attribute.add_or_replace_check_changed check_attr_dealloc_mismatch prop atom
     else
       prop in
   IList.fold_left replace_attr (Prop.normalize res_noattr) pi2_attr
@@ -836,7 +836,7 @@ let check_taint_on_variadic_function callee_pname caller_pname actual_params cal
       L.d_str "Paramters to be checked:  [ ";
       IList.iter(fun (e,_) ->
           L.d_str (" " ^ (Sil.exp_to_string e) ^ " ");
-          match Prop.Attribute.get_taint calling_prop e with
+          match Attribute.get_taint calling_prop e with
           | Some (Apred (Ataint taint_info, _)) ->
               report_taint_error e taint_info callee_pname caller_pname calling_prop
           | _ -> ()) actual_params';
@@ -887,7 +887,7 @@ let mk_posts ret_ids prop callee_pname callee_attrs posts =
               | Sil.Apred (Aretval (pname, _), [exp]) when Procname.equal callee_pname pname ->
                   Prover.check_disequal prop exp Exp.zero
               | _ -> false)
-            (Prop.Attribute.get_all prop) in
+            (Attribute.get_all prop) in
         if last_call_ret_non_null then
           let returns_null prop =
             IList.exists
@@ -904,7 +904,7 @@ let mk_posts ret_ids prop callee_pname callee_attrs posts =
             let taint_retval (prop, path) =
               let prop_normal = Prop.normalize prop in
               let prop' =
-                Prop.Attribute.add_or_replace prop_normal
+                Attribute.add_or_replace prop_normal
                   (Apred (Ataint { taint_source = callee_pname; taint_kind; }, [Exp.Var ret_id]))
                 |> Prop.expose in
               (prop', path) in
@@ -1109,7 +1109,7 @@ let quantify_path_idents_remove_constant_strings (prop: Prop.normal Prop.t) : Pr
 (** Strengthen the footprint by adding pure facts from the current part *)
 let prop_pure_to_footprint (p: 'a Prop.t) : Prop.normal Prop.t =
   let is_footprint_atom_not_attribute a =
-    not (Prop.Attribute.is_pred a)
+    not (Attribute.is_pred a)
     &&
     let a_fav = Sil.atom_fav a in
     Sil.fav_for_all a_fav Ident.is_footprint in
@@ -1262,7 +1262,7 @@ let exe_call_postprocess ret_ids trace_call callee_pname callee_attrs loc result
       let ret_var = Exp.Var ret_id in
       let mark_id_as_retval (p, path) =
         let att_retval = PredSymb.Aretval (callee_pname, ret_annot) in
-        Prop.Attribute.add p att_retval [ret_var], path in
+        Attribute.add p att_retval [ret_var], path in
       IList.map mark_id_as_retval res
   | _ -> res
 
diff --git a/infer/src/backend/taint.ml b/infer/src/backend/taint.ml
index a7949587b..cbfda8e88 100644
--- a/infer/src/backend/taint.ml
+++ b/infer/src/backend/taint.ml
@@ -379,6 +379,6 @@ let add_tainting_attribute att pvar_param prop =
          when Pvar.equal pvar pvar_param ->
            L.d_strln ("TAINT ANALYSIS: setting taint/untaint attribute of parameter " ^
                       (Pvar.to_string pvar));
-           Prop.Attribute.add_or_replace prop_acc (Apred (att, [rhs]))
+           Attribute.add_or_replace prop_acc (Apred (att, [rhs]))
        | _ -> prop_acc)
     prop (Prop.get_sigma prop)