Add negated attributes, with 2-valued semantics

Summary:
Treat attributes as unary predicates in classical first-order logic.
This diff extends predicates with a polarity and uses classical 2-valued
semantics.  This potentially changes the behavior of negating
attributes, which was not previously relied on.

Reviewed By: sblackshear

Differential Revision: D3669365

fbshipit-source-id: 2f26776

infer/src/backend/abs.ml

@@ -1030,11 +1030,11 @@ let cycle_has_weak_or_unretained_or_assign_field cycle =
 
 let check_observer_is_unsubscribed_deallocation prop e =
   let pvar_opt = match Prop.get_resource_attribute prop e with
-    | Some (Sil.Aresource ({Sil.ra_vpath =  Some (DecompiledExp.Dpvar pvar) })) -> Some pvar
+    | Some (true, Aresource ({ ra_vpath =  Some (DecompiledExp.Dpvar pvar) })) -> Some pvar
     | _ -> None in
   let loc = State.get_loc () in
   match Prop.get_observer_attribute prop e with
-  | Some Sil.Aobserver ->
+  | Some (true, Aobserver) ->
       (match pvar_opt with
        |  Some pvar when Config.nsnotification_center_checker_backend ->
            L.d_strln (" ERROR: Object " ^ (Pvar.to_string pvar) ^
@@ -1100,12 +1100,12 @@ let check_junk ?original_prop pname tenv prop =
                 let do_entry e =
                   check_observer_is_unsubscribed_deallocation prop e;
                   match Prop.get_resource_attribute prop e with
-                  | Some (Sil.Aresource ({ Sil.ra_kind = Sil.Racquire }) as a) ->
+                  | Some (true, (Aresource ({ ra_kind = Racquire }) as a)) ->
                       L.d_str "ATTRIBUTE: "; Sil.d_attribute a; L.d_ln ();
                       res := Some a
                   | _ ->
                       (match Prop.get_undef_attribute prop e with
-                       | Some (Sil.Aundef _ as a) ->
+                       | Some (true, (Aundef _ as a)) ->
                            res := Some a
                        | _ -> ()) in
                 IList.iter do_entry entries;

infer/src/backend/errdesc.ml

@@ -56,7 +56,7 @@ let is_special_field class_names field_name_opt field =
 let hpred_is_open_resource prop = function
   | Sil.Hpointsto(e, _, _) ->
       (match Prop.get_resource_attribute prop e with
-       | Some (Sil.Aresource { Sil.ra_kind = Sil.Racquire; Sil.ra_res = res }) -> Some res
+       | Some (true, Aresource { ra_kind = Racquire; ra_res = res }) -> Some res
        | _ -> None)
   | _ ->
       None
@@ -848,7 +848,7 @@ let create_dereference_desc
       | Some (DExp.Dpvar pvar)
       | Some (DExp.Dpvaraddr pvar) ->
           (match Prop.get_objc_null_attribute prop (Sil.Lvar pvar) with
-           | Some (Sil.Aobjc_null (v,fs)) ->
+           | Some (true, Aobjc_null (v,fs)) ->
                let e = IList.fold_left (fun e f -> Sil.Lfield (e, f, Typ.Tvoid)) (Sil.Lvar v) fs in
                Localise.parameter_field_not_null_checked_desc desc e
            | _ ->

infer/src/backend/localise.ml

@@ -399,7 +399,7 @@ let deref_str_array_bound size_opt index_opt =
 let deref_str_uninitialized alloc_att_opt =
   let tags = Tags.create () in
   let creation_str = match alloc_att_opt with
-    | Some (Sil.Aresource ({ Sil.ra_kind = Sil.Racquire } as ra)) ->
+    | Some (true, Sil.Aresource ({ ra_kind = Racquire } as ra)) ->
         "after allocation " ^ by_call_to_ra tags ra
     | _ -> "after declaration" in
   { tags = tags;

infer/src/backend/localise.mli

@@ -162,7 +162,7 @@ val deref_str_dangling : Sil.dangling_kind option -> deref_str
 val deref_str_array_bound : IntLit.t option -> IntLit.t option -> deref_str
 
 (** dereference strings for an uninitialized access whose lhs has the given attribute *)
-val deref_str_uninitialized : Sil.attribute option -> deref_str
+val deref_str_uninitialized : (bool * Sil.attribute) option -> deref_str
 
 (** dereference strings for nonterminal nil arguments in c/objc variadic methods *)
 val deref_str_nil_argument_in_variadic_method : Procname.t -> int -> int -> deref_str

infer/src/backend/modelBuiltins.ml

@@ -312,11 +312,12 @@ let execute___cast builtin_args
 
 let set_resource_attribute prop path n_lexp loc ra_res =
   let prop' = match Prop.get_resource_attribute prop n_lexp with
-    | Some (Sil.Aresource (_ as ra)) ->
+    | Some (true, Aresource ra) ->
         Prop.add_or_replace_exp_attribute
           prop
-          n_lexp
+          true
           (Sil.Aresource { ra with Sil.ra_res = ra_res })
+          n_lexp
     | _ ->
         ( let pname = Sil.mem_alloc_pname Sil.Mnew in
           let ra =
@@ -325,7 +326,7 @@ let set_resource_attribute prop path n_lexp loc ra_res =
               Sil.ra_pname = pname;
               Sil.ra_loc = loc;
               Sil.ra_vpath = None } in
-          Prop.add_or_replace_exp_attribute prop n_lexp (Sil.Aresource ra)) in
+          Prop.add_or_replace_exp_attribute prop true (Aresource ra) n_lexp) in
   [(prop', path)]
 
 (** Set the attibute of the value as file *)
@@ -547,7 +548,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.add_or_replace_exp_attribute prop n_lexp Sil.Aautorelease in
+        let prop' = Prop.add_or_replace_exp_attribute prop true Aautorelease n_lexp in
         [(prop', path)]
       else execute___no_op prop path
   | _ -> raise (Exceptions.Wrong_argument_number __POS__)
@@ -558,7 +559,7 @@ let execute___release_autorelease_pool
   : Builtin.ret_typ =
   if Config.objc_memory_model_on then
     let autoreleased_objects = Prop.get_atoms_with_attribute Sil.Aautorelease prop_ in
-    let prop_without_attribute = Prop.remove_attribute Sil.Aautorelease prop_ in
+    let prop_without_attribute = Prop.remove_attribute prop_ true Aautorelease in
     let call_release res exp =
       match res with
       | (prop', path'):: _ ->
@@ -584,12 +585,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.add_or_replace_exp_attribute prop n_lexp attr, path)]
+  [(Prop.add_or_replace_exp_attribute prop true 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.remove_attribute_from_exp attr prop n_lexp, path)]
+  [(Prop.remove_attribute_from_exp prop true attr n_lexp, path)]
 
 
 (** Set attibute att *)
@@ -699,8 +700,9 @@ let _execute_free mk loc acc iter =
         Prop.add_or_replace_exp_attribute_check_changed
           Tabulation.check_attr_dealloc_mismatch
           prop
-          lexp
-          (Sil.Aresource ra) in
+          true
+          (Aresource ra)
+          lexp in
       p_res :: acc
   | (Sil.Hpointsto _, _ :: _) -> assert false (* alignment error *)
   | _ -> assert false (* should not happen *)
@@ -801,7 +803,7 @@ let execute_alloc mk can_return_null
         Sil.ra_loc = loc;
         Sil.ra_vpath = None } in
     (* mark value as allocated *)
-    Prop.add_or_replace_exp_attribute prop' exp_new (Sil.Aresource ra) in
+    Prop.add_or_replace_exp_attribute prop' true (Aresource ra) exp_new in
   let prop_alloc = Prop.conjoin_eq (Sil.Var ret_id) exp_new prop_plus_ptsto in
   if can_return_null then
     let prop_null = Prop.conjoin_eq (Sil.Var ret_id) Sil.exp_zero prop in

infer/src/backend/prop.ml

@@ -1781,7 +1781,7 @@ let prop_reset_inst inst_map prop =
 
 (** Return the exp and attribute marked in the atom if any, and return None otherwise *)
 let atom_get_exp_attribute = function
-  | Sil.Apred (true, att, e) -> Some (e, att)
+  | Sil.Apred (p, a, e) -> Some (p, a, e)
   | _ -> None
 
 (** Check whether an atom is used to mark an attribute *)
@@ -1793,7 +1793,7 @@ let get_exp_attributes prop exp =
   let nexp = exp_normalize_prop prop exp in
   let atom_get_attr attributes atom =
     match atom with
-    | Sil.Apred (true, att, e) when Sil.exp_equal e nexp -> att :: attributes
+    | Sil.Apred (pol, att, e) when Sil.exp_equal e nexp -> (pol, att) :: attributes
     | _ -> attributes in
   IList.fold_left atom_get_attr [] prop.pi
 
@@ -1805,7 +1805,7 @@ let attributes_in_same_category attr1 attr2 =
 let get_attribute prop exp category =
   let atts = get_exp_attributes prop exp in
   try Some (IList.find
-              (fun att ->
+              (fun (_, att) ->
                  Sil.attribute_category_equal
                    (Sil.attribute_to_category att) category)
               atts)
@@ -1837,13 +1837,13 @@ let get_retval_attribute prop exp =
 
 let has_dangling_uninit_attribute prop exp =
   let la = get_exp_attributes prop exp in
-  IList.exists (fun a -> Sil.attribute_equal a (Sil.Adangling (Sil.DAuninit))) la
+  IList.exists (fun (pol, a) -> pol && Sil.attribute_equal a (Adangling DAuninit)) la
 
 (** Get all the attributes of the prop *)
 let get_all_attributes prop =
   let res = ref [] in
   let do_atom a = match atom_get_exp_attribute a with
-    | Some (e, att) -> res := (e, att) :: !res
+    | Some attr -> res := attr :: !res
     | None -> () in
   IList.iter do_atom prop.pi;
   IList.rev !res
@@ -1853,41 +1853,41 @@ let set_exp_attribute ?(footprint = false) ?(polarity = true) prop attr exp =
   prop_atom_and ~footprint prop (Sil.Apred (polarity, attr, exp))
 
 (** Replace an attribute associated to the expression *)
-let add_or_replace_exp_attribute_check_changed check_attribute_change prop exp att =
+let add_or_replace_exp_attribute_check_changed check_attribute_change prop pol0 att0 exp =
   let nexp = exp_normalize_prop prop exp in
-  let found = ref false in
   let atom_map a = match a with
-    | Sil.Apred (true, att_old, e) ->
-        if Sil.exp_equal nexp e && (attributes_in_same_category att_old att) then
+    | Sil.Apred (_, att, e) ->
+        if Sil.exp_equal nexp e && attributes_in_same_category att att0 then
           begin
-            found := true;
-            check_attribute_change att_old att;
-            Sil.Apred (true, att, e)
+            check_attribute_change att att0;
+            Sil.Apred (pol0, att0, e)
           end
         else a
     | _ -> a in
-  let pi' = IList.map atom_map (get_pi prop) in
-  if !found then replace_pi pi' prop
-  else set_exp_attribute prop att nexp
+  let pi = get_pi prop in
+  let pi' = IList.map_changed atom_map pi in
+  if pi == pi'
+  then set_exp_attribute prop ~polarity:pol0 att0 nexp
+  else replace_pi pi' prop
 
-let add_or_replace_exp_attribute prop exp att =
+let add_or_replace_exp_attribute prop pol att exp =
   (* wrapper for the most common case: do nothing *)
   let check_attr_changed = (fun _ _ -> ()) in
-  add_or_replace_exp_attribute_check_changed check_attr_changed prop exp att
+  add_or_replace_exp_attribute_check_changed check_attr_changed prop pol att exp
 
 (** mark Sil.Var's or Sil.Lvar's as undefined *)
 let mark_vars_as_undefined prop vars_to_mark callee_pname ret_annots loc path_pos =
   let att_undef = Sil.Aundef (callee_pname, ret_annots, loc, path_pos) in
   let mark_var_as_undefined exp prop =
     match exp with
-    | Sil.Var _ | Sil.Lvar _ -> add_or_replace_exp_attribute prop exp att_undef
+    | Sil.Var _ | Sil.Lvar _ -> add_or_replace_exp_attribute prop true att_undef exp
     | _ -> prop in
   IList.fold_left (fun prop id -> mark_var_as_undefined id prop) prop vars_to_mark
 
 let remove_attribute_by_filter ~f prop =
   let atom_remove atom pi = match atom with
-    | Sil.Apred (true, att_old, exp) ->
-        if f att_old exp then
+    | Sil.Apred (pol, att_old, exp) ->
+        if f pol att_old exp then
           pi
         else atom:: pi
     | _ -> atom:: pi in
@@ -1895,30 +1895,31 @@ let remove_attribute_by_filter ~f prop =
   replace_pi pi' prop
 
 (** Remove an attribute from all the atoms in the heap *)
-let remove_attribute att =
-  let f att_old _ = Sil.attribute_equal att_old att in
-  remove_attribute_by_filter ~f
+let remove_attribute prop pol0 att0 =
+  let f pol att _ = bool_equal pol0 pol && Sil.attribute_equal att0 att in
+  remove_attribute_by_filter ~f prop
 
 let remove_resource_attribute ra_kind ra_res =
-  let f att_old _ = match att_old with
-    | Sil.Aresource res_action ->
+  let f pol att_old _ = match att_old with
+    | Sil.Aresource res_action when pol ->
         Sil.res_act_kind_compare res_action.Sil.ra_kind ra_kind == 0
         && Sil.resource_compare res_action.Sil.ra_res ra_res == 0
     | _ -> false in
   remove_attribute_by_filter ~f
 
-let remove_attribute_from_exp att prop exp =
+let remove_attribute_from_exp prop pol att exp =
   let nexp = exp_normalize_prop prop exp in
-  let f att_old e = Sil.attribute_equal att_old att && Sil.exp_equal nexp e in
+  let f pol_old att_old e =
+    bool_equal pol pol_old && Sil.attribute_equal att_old att && Sil.exp_equal nexp e in
   remove_attribute_by_filter ~f 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_attribute prop rhs_exp, rhs_exp with
-  | Some att, Sil.Var _ ->
-      let prop = remove_attribute_from_exp att prop rhs_exp in
+  | Some (pol, att), Sil.Var _ ->
+      let prop = remove_attribute_from_exp prop pol att rhs_exp in
       let prop = conjoin_eq rhs_exp Sil.exp_zero prop in
-      add_or_replace_exp_attribute prop lhs_exp att
+      add_or_replace_exp_attribute prop true att lhs_exp
   | _ -> prop
 
 let rec nullify_exp_with_objc_null prop exp =
@@ -1930,8 +1931,8 @@ let rec nullify_exp_with_objc_null prop exp =
       nullify_exp_with_objc_null prop exp
   | Sil.Var _ ->
       (match get_objc_null_attribute prop exp with
-       | Some att ->
-           let prop' = remove_attribute_from_exp att prop exp in
+       | Some (pol, att) ->
+           let prop' = remove_attribute_from_exp prop pol att exp in
            conjoin_eq exp Sil.exp_zero prop'
        | _ -> prop)
   | _ -> prop
@@ -1939,7 +1940,7 @@ let rec nullify_exp_with_objc_null prop exp =
 (** Get all the attributes of the prop *)
 let get_atoms_with_attribute att prop =
   let atom_remove atom autoreleased_atoms = match atom with
-    | Sil.Apred (true, att_old, e) ->
+    | Sil.Apred (_, att_old, e) ->
         if Sil.attribute_equal att_old att then
           e:: autoreleased_atoms
         else autoreleased_atoms
@@ -1975,7 +1976,7 @@ let find_arithmetic_problem proc_node_session prop exp =
     match exp_normalize_prop prop e with
     | Sil.Const c when iszero_int_float c -> true
     | _ ->
-        res := add_or_replace_exp_attribute !res e (Sil.Adiv0 proc_node_session);
+        res := add_or_replace_exp_attribute !res true (Adiv0 proc_node_session) e;
         false in
   let rec walk = function
     | Sil.Var _ -> ()
@@ -2033,8 +2034,7 @@ let deallocate_stack_vars p pvars =
       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;
-          res :=
-            add_or_replace_exp_attribute !res (Sil.Var freshv) (Sil.Adangling Sil.DAaddr_stack_var)
+          res := add_or_replace_exp_attribute !res true (Adangling DAaddr_stack_var) (Var freshv)
         end in
     IList.iter do_var !fresh_address_vars;
     !res in
@@ -2832,7 +2832,7 @@ let find_equal_formal_path e prop =
   | Some (v, rev_fs) -> Some (v, IList.rev rev_fs)
   | None ->
       match get_objc_null_attribute prop e with
-      | Some (Sil.Aobjc_null (v,fs)) -> Some (v,fs)
+      | Some (true, Aobjc_null (v,fs)) -> Some (v,fs)
       | _ -> None
 
 (** translate an if-then-else expression *)

infer/src/backend/prop.mli

@@ -282,37 +282,37 @@ val atom_is_attribute : atom -> bool
 val attribute_map_resource : normal t -> (Sil.exp -> Sil.res_action -> Sil.res_action) -> normal t
 
 (** Return the exp and attribute marked in the atom if any, and return None otherwise *)
-val atom_get_exp_attribute : atom -> (Sil.exp * Sil.attribute) option
+val atom_get_exp_attribute : atom -> (bool * Sil.attribute * Sil.exp) option
 
 (** Get the attributes associated to the expression, if any *)
-val get_exp_attributes : 'a t -> exp -> attribute list
+val get_exp_attributes : 'a t -> exp -> (bool * attribute) list
 
 (** Get the undef attribute associated to the expression, if any *)
-val get_undef_attribute : 'a t -> exp -> attribute option
+val get_undef_attribute : 'a t -> exp -> (bool * attribute) option
 
 (** Get the resource attribute associated to the expression, if any *)
-val get_resource_attribute : 'a t -> exp -> attribute option
+val get_resource_attribute : 'a t -> exp -> (bool * attribute) option
 
 (** Get the taint attribute associated to the expression, if any *)
-val get_taint_attribute : 'a t -> exp -> attribute option
+val get_taint_attribute : 'a t -> exp -> (bool * attribute) option
 
 (** Get the autorelease attribute associated to the expression, if any *)
-val get_autorelease_attribute : 'a t -> exp -> attribute option
+val get_autorelease_attribute : 'a t -> exp -> (bool * attribute) option
 
 (** Get the div0 attribute associated to the expression, if any *)
-val get_div0_attribute : 'a t -> exp -> attribute option
+val get_div0_attribute : 'a t -> exp -> (bool * attribute) option
 
 (** Get the observer attribute associated to the expression, if any *)
-val get_observer_attribute : 'a t -> exp -> attribute option
+val get_observer_attribute : 'a t -> exp -> (bool * attribute) option
 
 (** Get the objc null attribute associated to the expression, if any *)
-val get_objc_null_attribute : 'a t -> exp -> attribute option
+val get_objc_null_attribute : 'a t -> exp -> (bool * attribute) option
 
 (** Get the retval null attribute associated to the expression, if any *)
-val get_retval_attribute : 'a t -> exp -> attribute option
+val get_retval_attribute : 'a t -> exp -> (bool * attribute) option
 
 (** Get all the attributes of the prop *)
-val get_all_attributes : 'a t -> (exp * attribute) list
+val get_all_attributes : 'a t -> (bool * attribute * exp) list
 
 val has_dangling_uninit_attribute : 'a t -> exp -> bool
 
@@ -321,17 +321,17 @@ val set_exp_attribute : ?footprint: bool -> ?polarity: bool ->
   normal t -> attribute -> exp -> normal t
 
 val add_or_replace_exp_attribute_check_changed : (Sil.attribute -> Sil.attribute -> unit) ->
-  normal t -> exp -> attribute -> normal t
+  normal t -> bool -> attribute -> exp -> normal t
 
 (** Replace an attribute associated to the expression *)
-val add_or_replace_exp_attribute : normal t -> exp -> attribute -> normal t
+val add_or_replace_exp_attribute : normal t -> bool -> attribute -> exp -> normal t
 
 (** mark Sil.Var's or Sil.Lvar's as undefined *)
 val mark_vars_as_undefined : normal t -> Sil.exp list -> Procname.t -> Typ.item_annotation ->
   Location.t -> Sil.path_pos -> normal t
 
 (** Remove an attribute from all the atoms in the heap *)
-val remove_attribute : Sil.attribute -> 'a t -> normal t
+val remove_attribute : 'a t -> bool -> Sil.attribute -> normal t
 
 val remove_resource_attribute : Sil.res_act_kind -> Sil.resource -> 'a t -> normal t
 
@@ -342,7 +342,7 @@ val replace_objc_null : normal t -> exp -> exp -> normal t
 val nullify_exp_with_objc_null : normal t -> exp -> normal t
 
 (** Remove an attribute from an exp in the heap *)
-val remove_attribute_from_exp : Sil.attribute -> 'a t -> exp -> normal t
+val remove_attribute_from_exp : 'a t -> bool -> Sil.attribute -> exp -> normal t
 
 (** Retireve all the atoms in the heap that contain a specific attribute *)
 val get_atoms_with_attribute : Sil.attribute -> 'a t -> Sil.exp list

infer/src/backend/rearrange.ml

@@ -744,7 +744,7 @@ let add_guarded_by_constraints prop lexp pdesc =
       (* or the prop says we already have the lock *)
       IList.exists
         (function
-          | Sil.Alocked -> true
+          | (true, Sil.Alocked) -> true
           | _ -> false)
         (Prop.get_exp_attributes prop guarded_by_exp) in
     let should_warn pdesc =
@@ -1200,8 +1200,9 @@ let check_dereference_error pdesc (prop : Prop.normal Prop.t) lexp loc =
                  end
                else
                  let is_nullable_attr = function
-                   | Sil.Aretval (pname, ret_attr)
-                   | Sil.Aundef (pname, ret_attr, _, _) when Annotations.ia_is_nullable ret_attr ->
+                   | (true, Sil.Aretval (pname, ret_attr))
+                   | (true, Sil.Aundef (pname, ret_attr, _, _))
+                     when Annotations.ia_is_nullable ret_attr ->
                        nullable_obj_str := Some (Procname.to_string pname);
                        true
                    | _ -> false in
@@ -1272,17 +1273,17 @@ let check_dereference_error pdesc (prop : Prop.normal Prop.t) lexp loc =
       else raise (Exceptions.Null_dereference (err_desc, __POS__))
     end;
   match attribute_opt with
-  | Some (Sil.Adangling dk) ->
+  | Some (true, Adangling dk) ->
       let deref_str = Localise.deref_str_dangling (Some dk) in
       let err_desc = Errdesc.explain_dereference deref_str prop (State.get_loc ()) in
       raise (Exceptions.Dangling_pointer_dereference (Some dk, err_desc, __POS__))
-  | Some (Sil.Aundef (s, _, undef_loc, _)) ->
+  | Some (true, Aundef (s, _, undef_loc, _)) ->
       if Config.angelic_execution then ()
       else
         let deref_str = Localise.deref_str_undef (s, undef_loc) in
         let err_desc = Errdesc.explain_dereference deref_str prop loc in
         raise (Exceptions.Skip_pointer_dereference (err_desc, __POS__))
-  | Some (Sil.Aresource ({ Sil.ra_kind = Sil.Rrelease } as ra)) ->
+  | Some (true, Aresource ({ ra_kind = Rrelease } as ra)) ->
       let deref_str = Localise.deref_str_freed ra in
       let err_desc = Errdesc.explain_dereference ~use_buckets: true deref_str prop loc in
       raise (Exceptions.Use_after_free (err_desc, __POS__))

infer/src/backend/symExec.ml

@@ -476,11 +476,11 @@ let check_already_dereferenced pname cond prop =
     raising an exception in that case *)
 let check_deallocate_static_memory prop_after =
   let check_deallocated_attribute = function
-    | Sil.Lvar pv, Sil.Aresource ({ Sil.ra_kind = Sil.Rrelease } as ra)
+    | true, Sil.Aresource ({ ra_kind = Rrelease } as ra), Sil.Lvar pv
       when Pvar.is_local pv || Pvar.is_global pv ->
         let freed_desc = Errdesc.explain_deallocate_stack_var pv ra in
         raise (Exceptions.Deallocate_stack_variable freed_desc)
-    | Sil.Const (Const.Cstr s), Sil.Aresource ({ Sil.ra_kind = Sil.Rrelease } as ra) ->
+    | true, Sil.Aresource ({ ra_kind = Rrelease } as ra), Sil.Const (Cstr s) ->
         let freed_desc = Errdesc.explain_deallocate_constant_string s ra in
         raise (Exceptions.Deallocate_static_memory freed_desc)
     | _ -> () in
@@ -738,7 +738,7 @@ let handle_objc_instance_method_call_or_skip actual_pars path callee_pname pre r
     | [ret_id] -> (
         match Prop.find_equal_formal_path receiver prop with
         | Some (v,fs) ->
-            Prop.add_or_replace_exp_attribute prop (Sil.Var ret_id) (Sil.Aobjc_null (v,fs))
+            Prop.add_or_replace_exp_attribute prop true (Aobjc_null (v,fs)) (Var ret_id)
         | None ->
             Prop.conjoin_eq (Sil.Var ret_id) Sil.exp_zero prop
       )
@@ -843,7 +843,7 @@ let add_constraints_on_retval pdesc prop ret_exp ~has_nullable_annot typ callee_
         | Typ.Tptr _ -> Prop.conjoin_neq exp Sil.exp_zero prop
         | _ -> prop in
     let add_tainted_post ret_exp callee_pname prop =
-      Prop.add_or_replace_exp_attribute prop ret_exp (Sil.Ataint callee_pname) in
+      Prop.add_or_replace_exp_attribute prop true (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 = { Sil.taint_source = pname; taint_kind = Tk_unknown; } in
-      Prop.add_or_replace_exp_attribute prop (Sil.Var lhs_id) (Sil.Ataint taint_info)
+      Prop.add_or_replace_exp_attribute prop true (Ataint taint_info) (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.add_or_replace_exp_attribute prop' (Sil.Var id) (Sil.Adangling Sil.DAuninit)
+              Prop.add_or_replace_exp_attribute prop' true (Adangling DAuninit) (Var id)
             else prop' in
           let prop''' =
             if Config.taint_analysis
@@ -932,8 +932,8 @@ let execute_letderef ?(report_deref_errors=true) pname pdesc tenv id rhs_exp typ
         [Prop.conjoin_eq (Sil.Var id) value prop]
     | None ->
         let exp_get_undef_attr exp =
-          let fold_undef_pname callee_opt attr =
-            if Option.is_none callee_opt && Sil.attr_is_undef attr then Some attr
+          let fold_undef_pname callee_opt (pol, attr) =
+            if Option.is_none callee_opt && pol && Sil.attr_is_undef attr then Some attr
             else callee_opt in
           IList.fold_left fold_undef_pname None (Prop.get_exp_attributes prop exp) in
         let prop' =
@@ -1362,7 +1362,7 @@ and add_constraints_on_actuals_by_ref tenv prop actuals_by_ref callee_pname call
 
 and check_untainted exp taint_kind caller_pname callee_pname prop =
   match Prop.get_taint_attribute prop exp with
-  | Some (Sil.Ataint taint_info) ->
+  | Some (true, Ataint taint_info) ->
       let err_desc =
         Errdesc.explain_tainted_value_reaching_sensitive_function
           prop
@@ -1374,7 +1374,7 @@ 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.add_or_replace_exp_attribute prop exp (Sil.Auntaint taint_info)
+      Prop.add_or_replace_exp_attribute prop true (Auntaint taint_info) exp
   | _ ->
       if !Config.footprint then
         let taint_info = { Sil.taint_source = callee_pname; taint_kind; } in
@@ -1389,9 +1389,9 @@ and unknown_or_scan_call ~is_scan ret_type_option ret_annots
   let remove_file_attribute prop =
     let do_exp p (e, _) =
       let do_attribute q = function
-        | Sil.Aresource res_action as res
+        | (pol, (Sil.Aresource res_action as res))
           when res_action.Sil.ra_res = Sil.Rfile ->
-            Prop.remove_attribute res q
+            Prop.remove_attribute q pol res
         | _ -> q in
       IList.fold_left do_attribute p (Prop.get_exp_attributes p e) in
     let filtered_args =

infer/src/backend/tabulation.ml

@@ -318,11 +318,11 @@ let check_dereferences callee_pname actual_pre sub spec_pre formal_params =
     else if Sil.exp_equal e_sub Sil.exp_minus_one
     then Some (Deref_minusone, desc true (Localise.deref_str_dangling None))
     else match Prop.get_resource_attribute actual_pre e_sub with
-      | Some (Sil.Aresource ({ Sil.ra_kind = Sil.Rrelease } as ra)) ->
+      | Some (true, Aresource ({ ra_kind = Rrelease } as ra)) ->
           Some (Deref_freed ra, desc true (Localise.deref_str_freed ra))
       | _ ->
           (match Prop.get_undef_attribute actual_pre e_sub with
-           | Some (Sil.Aundef (s, _, loc, pos)) ->
+           | Some (true, Aundef (s, _, loc, pos)) ->
                Some (Deref_undef (s, loc, pos), desc false (Localise.deref_str_undef (s, loc)))
            | _ -> None) in
   let check_hpred = function
@@ -360,8 +360,8 @@ let post_process_sigma (sigma: Sil.hpred list) loc : Sil.hpred list =
 
 (** check for interprocedural path errors in the post *)
 let check_path_errors_in_post caller_pname post post_path =
-  let check_attr (e, att) = match att with
-    | Sil.Adiv0 path_pos ->
+  let check_attr (pol, att, e) = match att with
+    | Sil.Adiv0 path_pos when pol ->
         if Prover.check_zero e then
           let desc = Errdesc.explain_divide_by_zero e (State.get_node ()) (State.get_loc ()) in
           let new_path, path_pos_opt =
@@ -382,7 +382,7 @@ let check_path_errors_in_post caller_pname post post_path =
 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.get_resource_attribute actual_pre e with
-    | Some (Sil.Aresource ({ Sil.ra_kind = Sil.Rrelease })) -> true
+    | Some (true, Aresource ({ ra_kind = Rrelease })) -> true
     | _ -> false in
   let atom_update_alloc_attribute = function
     | Sil.Apred (true, Aresource ra, e)
@@ -604,8 +604,9 @@ let prop_copy_footprint_pure p1 p2 =
     (* if [atom] represents an attribute [att], add the attribure to [prop] *)
     match Prop.atom_get_exp_attribute atom with
     | None -> prop
-    | Some (exp, att) ->
-        Prop.add_or_replace_exp_attribute_check_changed check_attr_dealloc_mismatch prop exp att in
+    | Some (pol, att, exp) ->
+        Prop.add_or_replace_exp_attribute_check_changed
+          check_attr_dealloc_mismatch prop pol att exp in
   IList.fold_left replace_attr (Prop.normalize res_noattr) pi2_attr
 
 (** check if an expression is an exception *)
@@ -836,7 +837,8 @@ let check_taint_on_variadic_function callee_pname caller_pname actual_params cal
       IList.iter(fun (e,_) ->
           L.d_str (" " ^ (Sil.exp_to_string e) ^ " ");
           match Prop.get_taint_attribute calling_prop e with
-          | Some (Sil.Ataint taint_info) -> report_taint_error e taint_info callee_pname caller_pname calling_prop
+          | Some (true, Ataint taint_info) ->
+              report_taint_error e taint_info callee_pname caller_pname calling_prop
           | _ -> ()) actual_params';
       L.d_strln" ]"
   | _ ->  ()
@@ -881,9 +883,9 @@ let mk_posts ret_ids prop callee_pname callee_attrs posts =
            "if (get() != null) get().something()" pattern *)
         let last_call_ret_non_null =
           IList.exists
-            (fun (exp, attr) ->
+            (fun (pol, attr, exp) ->
                match attr with
-               | Sil.Aretval (pname, _) when Procname.equal callee_pname pname ->
+               | Sil.Aretval (pname, _) when pol && Procname.equal callee_pname pname ->
                    Prover.check_disequal prop exp Sil.exp_zero
                | _ -> false)
             (Prop.get_all_attributes prop) in
@@ -903,9 +905,9 @@ 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.add_or_replace_exp_attribute prop_normal
-                  (Sil.Var ret_id)
-                  (Sil.Ataint { Sil.taint_source = callee_pname; taint_kind; })
+                Prop.add_or_replace_exp_attribute prop_normal true
+                  (Ataint { taint_source = callee_pname; taint_kind; })
+                  (Var ret_id)
                 |> Prop.expose in
               (prop', path) in
             IList.map taint_retval posts
@@ -936,10 +938,10 @@ let do_taint_check caller_pname callee_pname calling_prop missing_pi sub actual_
   (* build a map from exp -> [taint attrs, untaint attrs], keeping only exprs with both kinds of
      attrs (we will flag errors on those exprs) *)
   let collect_taint_untaint_exprs acc_map atom = match Prop.atom_get_exp_attribute atom with
-    | Some (e, Sil.Ataint _) ->
+    | Some (_, Ataint _, e) ->
         let taint_atoms, untaint_atoms = try Sil.ExpMap.find e acc_map with Not_found -> ([], []) in
         Sil.ExpMap.add e (atom :: taint_atoms, untaint_atoms) acc_map
-    | Some (e, Sil.Auntaint _) ->
+    | Some (_, Auntaint _, e) ->
         let taint_atoms, untaint_atoms = try Sil.ExpMap.find e acc_map with Not_found -> ([], []) in
         Sil.ExpMap.add e (taint_atoms, atom :: untaint_atoms) acc_map
     | _ -> acc_map in
@@ -955,7 +957,7 @@ let do_taint_check caller_pname callee_pname calling_prop missing_pi sub actual_
   let report_taint_errors e (taint_atoms, _untaint_atoms) =
     let report_one_error taint_atom =
       let taint_info = match Prop.atom_get_exp_attribute taint_atom with
-        | Some (_, Sil.Ataint taint_info) -> taint_info
+        | Some (_, Ataint taint_info, _) -> taint_info
         | _ -> failwith "Expected to get taint attr on atom" in
       report_taint_error e taint_info callee_pname caller_pname calling_prop in
     IList.iter report_one_error taint_atoms in

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.add_or_replace_exp_attribute prop_acc rhs att
+           Prop.add_or_replace_exp_attribute prop_acc true att rhs
        | _ -> prop_acc)
     prop (Prop.get_sigma prop)