Represent attributes with atoms, not disequalities

Summary:
Replace disequalities to Attribute expressions with predicate symbol
application pure atomic formulas.

This diff should preserve existing behavior, up to the comparison order
of attribute disequalities versus predicate applications.

Reviewed By: sblackshear

Differential Revision: D3647049

fbshipit-source-id: c39a901

infer/src/IR/Cfg.re

@@ -962,6 +962,7 @@ let remove_abducted_retvars p =>
             fun
             | Sil.Aeq lhs rhs
             | Sil.Aneq lhs rhs => exp_contains lhs || exp_contains rhs
+            | Sil.Apred _ _ e => exp_contains e
           )
           pi
       };

infer/src/IR/Sil.re

@@ -137,9 +137,7 @@ and exp =
       The [dynamic_length], tracked by symbolic execution, may differ from the [static_length]
       obtained from the type definition, e.g. when an array is over-allocated.  For struct types,
       the [dynamic_length] is that of the final extensible array, if any. */
-  | Sizeof of Typ.t dynamic_length Subtype.t
-  /** attribute used in disequalities to annotate a value */
-  | Attribute of attribute;
+  | Sizeof of Typ.t dynamic_length Subtype.t;
 
 
 /** Kind of prune instruction */
@@ -204,7 +202,8 @@ type offset = | Off_fld of Ident.fieldname Typ.t | Off_index of exp;
 /** an atom is a pure atomic formula */
 type atom =
   | Aeq of exp exp /** equality */
-  | Aneq of exp exp /** disequality*/;
+  | Aneq of exp exp /** disequality */
+  | Apred of bool attribute exp /** possibly negated predicate symbol applied to an exp */;
 
 
 /** kind of lseg or dllseg predicates */
@@ -660,9 +659,6 @@ let rec exp_compare (e1: exp) (e2: exp) :int =>
         Subtype.compare s1 s2
       }
     }
-  | (Attribute att1, Attribute att2) => attribute_compare att1 att2
-  | (Attribute _, _) => (-1)
-  | (_, Attribute _) => 1
   };
 
 let exp_equal e1 e2 => exp_compare e1 e2 == 0;
@@ -697,8 +693,8 @@ let atom_compare a b =>
       } else {
         exp_compare e2 f2
       }
-    | (Aeq _, Aneq _) => (-1)
-    | (Aneq _, Aeq _) => 1
+    | (Aeq _, _) => (-1)
+    | (_, Aeq _) => 1
     | (Aneq e1 e2, Aneq f1 f2) =>
       let n = exp_compare e1 f1;
       if (n != 0) {
@@ -706,6 +702,20 @@ let atom_compare a b =>
       } else {
         exp_compare e2 f2
       }
+    | (Aneq _, _) => (-1)
+    | (_, Aneq _) => 1
+    | (Apred b1 a1 e1, Apred b2 a2 e2) =>
+      let n = bool_compare b1 b2;
+      if (n != 0) {
+        n
+      } else {
+        let n = attribute_compare a1 a2;
+        if (n != 0) {
+          n
+        } else {
+          exp_compare e1 e2
+        }
+      }
     }
   };
 
@@ -1086,7 +1096,6 @@ let rec _pp_exp pe0 pp_t f e0 => {
     | Sizeof t l s =>
       let pp_len f l => Option.map_default (F.fprintf f "[%a]" pp_exp) () l;
       F.fprintf f "sizeof(%a%a%a)" pp_t t pp_len l Subtype.pp s
-    | Attribute att => F.fprintf f "%s" (attribute_to_string pe att)
     }
   };
   color_post_wrapper changed pe0 f
@@ -1266,19 +1275,22 @@ let pp_atom pe0 f a => {
     | PP_HTML => F.fprintf f "%a = %a" (pp_exp pe) e1 (pp_exp pe) e2
     | PP_LATEX => F.fprintf f "%a{=}%a" (pp_exp pe) e1 (pp_exp pe) e2
     }
-  | Aneq (Attribute _ as ea) e
-  | Aneq e (Attribute _ as ea) => F.fprintf f "%a(%a)" (pp_exp pe) ea (pp_exp pe) e
   | Aneq e1 e2 =>
     switch pe.pe_kind {
     | PP_TEXT
     | PP_HTML => F.fprintf f "%a != %a" (pp_exp pe) e1 (pp_exp pe) e2
     | PP_LATEX => F.fprintf f "%a{\\neq}%a" (pp_exp pe) e1 (pp_exp pe) e2
     }
+  | Apred b a e => F.fprintf f "%s%s(%a)" (b ? "" : "!") (attribute_to_string pe a) (pp_exp pe) e
   };
   color_post_wrapper changed pe0 f
 };
 
 
+/** dump an attribute */
+let d_attribute (a: attribute) => L.add_print_action (L.PTattribute, Obj.repr a);
+
+
 /** dump an atom */
 let d_atom (a: atom) => L.add_print_action (L.PTatom, Obj.repr a);
 
@@ -1923,7 +1935,8 @@ let hpred_list_expmap (f: (exp, option inst) => (exp, option inst)) (hlist: list
 let atom_expmap (f: exp => exp) =>
   fun
   | Aeq e1 e2 => Aeq (f e1) (f e2)
-  | Aneq e1 e2 => Aneq (f e1) (f e2);
+  | Aneq e1 e2 => Aneq (f e1) (f e2)
+  | Apred b a e => Apred b a (f e);
 
 let atom_list_expmap (f: exp => exp) (alist: list atom) => IList.map (atom_expmap f) alist;
 
@@ -1964,7 +1977,6 @@ let rec root_of_lexp lexp =>
   | Lfield e _ _ => root_of_lexp e
   | Lindex e _ => root_of_lexp e
   | Sizeof _ => lexp
-  | Attribute _ => lexp
   };
 
 
@@ -2053,15 +2065,15 @@ let rec exp_fpv =
   /* TODO: Sizeof length expressions may contain variables, do not ignore them. */
   /* | Sizeof _ None _ => [] */
   /* | Sizeof _ (Some l) _ => exp_fpv l */
-  | Sizeof _ _ _ => []
-  | Attribute _ => [];
+  | Sizeof _ _ _ => [];
 
 let exp_list_fpv el => IList.flatten (IList.map exp_fpv el);
 
 let atom_fpv =
   fun
   | Aeq e1 e2 => exp_fpv e1 @ exp_fpv e2
-  | Aneq e1 e2 => exp_fpv e1 @ exp_fpv e2;
+  | Aneq e1 e2 => exp_fpv e1 @ exp_fpv e2
+  | Apred _ _ e => exp_fpv e;
 
 let rec strexp_fpv =
   fun
@@ -2253,8 +2265,7 @@ let rec exp_fav_add fav =>
   /* TODO: Sizeof length expressions may contain variables, do not ignore them. */
   /* | Sizeof _ None _ => () */
   /* | Sizeof _ (Some l) _ => exp_fav_add fav l; */
-  | Sizeof _ _ _ => ()
-  | Attribute _ => ();
+  | Sizeof _ _ _ => ();
 
 let exp_fav = fav_imperative_to_functional exp_fav_add;
 
@@ -2272,7 +2283,8 @@ let atom_fav_add fav =>
   | Aneq e1 e2 => {
       exp_fav_add fav e1;
       exp_fav_add fav e2
-    };
+    }
+  | Apred _ _ e => exp_fav_add fav e;
 
 let atom_fav = fav_imperative_to_functional atom_fav_add;
 
@@ -2710,7 +2722,6 @@ let rec exp_sub_ids (f: Ident.t => exp) exp =>
       }
     | None => exp
     }
-  | Attribute _ => exp
   };
 
 let rec apply_sub subst id =>
@@ -3204,7 +3215,8 @@ let atom_replace_exp epairs =>
       let e1' = exp_replace_exp epairs e1;
       let e2' = exp_replace_exp epairs e2;
       Aneq e1' e2'
-    };
+    }
+  | Apred b a e => Apred b a (exp_replace_exp epairs e);
 
 let rec strexp_replace_exp epairs =>
   fun
@@ -3326,7 +3338,6 @@ let exp_get_vars exp => {
     /* | Sizeof _ None _ => vars */
     /* | Sizeof _ (Some l) _ => exp_get_vars_ l vars */
     | Sizeof _ _ _ => vars
-    | Attribute _ => vars
     };
   exp_get_vars_ exp ([], [])
 };
@@ -3343,7 +3354,6 @@ let exp_get_offsets exp => {
     | Exn _
     | Closure _
     | Lvar _
-    | Attribute _
     | Sizeof _ None _ => offlist_past
     | Sizeof _ (Some l) _ => f offlist_past l
     | Cast _ sub_exp => f offlist_past sub_exp

infer/src/IR/Sil.rei

@@ -125,9 +125,7 @@ and exp =
       The [dynamic_length], tracked by symbolic execution, may differ from the [static_length]
       obtained from the type definition, e.g. when an array is over-allocated.  For struct types,
       the [dynamic_length] is that of the final extensible array, if any. */
-  | Sizeof of Typ.t dynamic_length Subtype.t
-  /** attribute used in disequalities to annotate a value */
-  | Attribute of attribute;
+  | Sizeof of Typ.t dynamic_length Subtype.t;
 
 
 /** Sets of expressions. */
@@ -198,7 +196,8 @@ type offset = | Off_fld of Ident.fieldname Typ.t | Off_index of exp;
 /** an atom is a pure atomic formula */
 type atom =
   | Aeq of exp exp /** equality */
-  | Aneq of exp exp /** disequality*/;
+  | Aneq of exp exp /** disequality */
+  | Apred of bool attribute exp /** possibly negated predicate symbol applied to an exp */;
 
 
 /** kind of lseg or dllseg predicates */
@@ -591,6 +590,10 @@ let d_instr_list: list instr => unit;
 let pp_atom: printenv => F.formatter => atom => unit;
 
 
+/** Dump an attribute. */
+let d_attribute: attribute => unit;
+
+
 /** Dump an atom. */
 let d_atom: atom => unit;
 

infer/src/backend/abs.ml

@@ -776,7 +776,6 @@ let abstract_pure_part p ~(from_abstract_footprint: bool) =
       IList.fold_left
         (fun pi a ->
            match a with
-           | Sil.Aneq (Sil.Var _, _) -> a:: pi
            (* we only use Lt and Le because Gt and Ge are inserted in terms of Lt and Le. *)
            | Sil.Aeq (Sil.Const (Const.Cint i), Sil.BinOp (Binop.Lt, _, _))
            | Sil.Aeq (Sil.BinOp (Binop.Lt, _, _), Sil.Const (Const.Cint i))
@@ -788,7 +787,10 @@ let abstract_pure_part p ~(from_abstract_footprint: bool) =
                 | Sil.Var _
                 | Sil.Const _ -> a :: pi
                 | _ -> pi)
-           | _ -> pi)
+           | Sil.Aneq (Var _, _)
+           | Sil.Apred (_, _, Var _) -> a :: pi
+           | Sil.Aeq _ | Aneq _ | Apred _ -> pi
+        )
         [] pi_filtered in
     IList.rev new_pure in
 
@@ -817,7 +819,12 @@ let abstract_gc p =
         let intersect_e2 _ = IList.intersect Ident.compare (Sil.fav_to_list fav_e2) (Sil.fav_to_list fav_p_without_pi) in
         let no_fav_e1 = Sil.fav_is_empty fav_e1 in
         let no_fav_e2 = Sil.fav_is_empty fav_e2 in
-        (no_fav_e1 || intersect_e1 ()) && (no_fav_e2 || intersect_e2 ()) in
+        (no_fav_e1 || intersect_e1 ()) && (no_fav_e2 || intersect_e2 ())
+    | Sil.Apred (_, _, e) ->
+        let fav_e = Sil.exp_fav e in
+        Sil.fav_is_empty fav_e
+        ||
+        IList.intersect Ident.compare (Sil.fav_to_list fav_e) (Sil.fav_to_list fav_p_without_pi) in
   let new_pi = IList.filter strong_filter pi in
   let prop = Prop.normalize (Prop.replace_pi new_pi p) in
   match Prop.prop_iter_create prop with
@@ -1094,7 +1101,7 @@ let check_junk ?original_prop pname tenv prop =
                   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) ->
-                      L.d_str "ATTRIBUTE: "; Sil.d_exp (Sil.Attribute a); L.d_ln ();
+                      L.d_str "ATTRIBUTE: "; Sil.d_attribute a; L.d_ln ();
                       res := Some a
                   | _ ->
                       (match Prop.get_undef_attribute prop e with

infer/src/backend/dom.ml

@@ -718,6 +718,10 @@ end = struct
           when (exp_contains_only_normal_ids e' && not (Ident.is_normal id)) ->
             build_other_atoms (fun e0 -> Prop.mk_neq e0 e') side e
 
+        | Sil.Apred (b, a, (Var id as e))
+          when not (Ident.is_normal id) ->
+            build_other_atoms (fun e0 -> Prop.mk_pred b a e0) side e
+
         | Sil.Aeq((Sil.Var id as e), e') | Sil.Aeq(e', (Sil.Var id as e))
           when (exp_contains_only_normal_ids e' && not (Ident.is_normal id)) ->
             build_other_atoms (fun e0 -> Prop.mk_eq e0 e') side e
@@ -734,7 +738,7 @@ end = struct
             let construct e0 = Prop.mk_inequality (Sil.BinOp(Binop.Lt, e', e0)) in
             build_other_atoms construct side e
 
-        | _ -> None
+        | Sil.Aeq _ | Aneq _ | Apred _ -> None
       end
 
   type data_opt = ExtFresh | ExtDefault of Sil.exp
@@ -828,8 +832,6 @@ let rec exp_construct_fresh side e =
       e
   | Sil.Sizeof (typ, Some len, st) ->
       Sil.Sizeof (typ, Some (exp_construct_fresh side len), st)
-  | Sil.Attribute _ ->
-      e
 
 let strexp_construct_fresh side =
   let f (e, inst_opt) = (exp_construct_fresh side e, inst_opt) in
@@ -1667,7 +1669,9 @@ let pi_partial_join mode
       when (exp_is_const e') ->
         true
     | Sil.Aneq _ -> false
-    | e -> Prop.atom_is_inequality e in
+    | Sil.Aeq _ as e -> Prop.atom_is_inequality e
+    | Sil.Apred (_, _, e) ->
+        exp_is_const e in
   begin
     if Config.trace_join then begin
       L.d_str "pi1: "; Prop.d_pi pi1; L.d_ln ();

infer/src/backend/dotty.ml

@@ -1307,7 +1307,9 @@ let atom_to_xml_light (a: Sil.atom) : Io_infer.Xml.node =
     | Sil.Aeq _ ->
         "equality"
     | Sil.Aneq _ ->
-        "disequality" in
+        "disequality"
+    | Sil.Apred _ ->
+        "pred" in
   Io_infer.Xml.create_tree "stack-variable" [("type", kind_info); ("instance", atom_to_xml_string a)] []
 
 let xml_pure_info prop =

infer/src/backend/logging.ml

@@ -17,6 +17,7 @@ module F = Format
 (** type of printable elements *)
 type print_type =
   | PTatom
+  | PTattribute
   | PTdecrease_indent
   | PTexp
   | PTexp_list

infer/src/backend/logging.mli

@@ -15,6 +15,7 @@ open! Utils
 (** type of printable elements *)
 type print_type =
   | PTatom
+  | PTattribute
   | PTdecrease_indent
   | PTexp
   | PTexp_list

infer/src/backend/match.ml

@@ -82,8 +82,6 @@ let rec exp_match e1 sub vars e2 : (Sil.subst * Ident.t list) option =
       (match exp_match base1 sub vars base2 with
        | None -> None
        | Some (sub', vars') -> exp_match idx1 sub' vars' idx2)
-  | Sil.Attribute _, _ | _, Sil.Attribute _ ->
-      check_equal sub vars e1 e2
 
 let exp_list_match es1 sub vars es2 =
   let f res_acc (e1, e2) = match res_acc with

infer/src/backend/modelBuiltins.ml

@@ -763,8 +763,7 @@ let execute_alloc mk can_return_null
         evaluate_char_sizeof len
     | Sil.Sizeof (Typ.Tarray (Typ.Tint ik, Some len), None, _) when Typ.ikind_is_char ik ->
         evaluate_char_sizeof (Sil.Const (Const.Cint len))
-    | Sil.Sizeof _ -> e
-    | Sil.Attribute _ -> e in
+    | Sil.Sizeof _ -> e in
   let size_exp, procname = match args with
     | [(Sil.Sizeof
           (Typ.Tstruct

infer/src/backend/printer.ml

@@ -172,6 +172,9 @@ let force_delayed_print fmt =
   | (L.PTatom, a) ->
       let (a: Sil.atom) = Obj.obj a in
       Sil.pp_atom pe_default fmt a
+  | (L.PTattribute, a) ->
+      let (a: Sil.attribute) = Obj.obj a in
+      F.pp_print_string fmt (Sil.attribute_to_string pe_default a)
   | (L.PTdecrease_indent, n) ->
       let (n: int) = Obj.obj n in
       for _ = 1 to n do F.fprintf fmt "@]" done

infer/src/backend/prop.ml

@@ -830,9 +830,7 @@ let sym_eval abs e =
     | Sil.Lindex (e1, e2) ->
         let e1' = eval e1 in
         let e2' = eval e2 in
-        Sil.Lindex(e1', e2')
-    | Sil.Attribute _ ->
-        e in
+        Sil.Lindex(e1', e2') in
   let e' = eval e in
   (* L.d_str "sym_eval "; Sil.d_exp e; L.d_str" --> "; Sil.d_exp e'; L.d_ln (); *)
   e'
@@ -1035,7 +1033,9 @@ let atom_normalize sub a0 =
     | Sil.Aeq (e1, e2) ->
         handle_boolean_operation true e1 e2
     | Sil.Aneq (e1, e2) ->
-        handle_boolean_operation false e1 e2 in
+        handle_boolean_operation false e1 e2
+    | Sil.Apred (b, a, e) ->
+        Sil.Apred (b, a, exp_normalize sub e) in
   if atom_is_inequality a' then inequality_normalize a' else a'
 
 (** Negate an atom *)
@@ -1046,6 +1046,7 @@ let atom_negate = function
       mk_inequality (Sil.exp_le e2 e1)
   | Sil.Aeq (e1, e2) -> Sil.Aneq (e1, e2)
   | Sil.Aneq (e1, e2) -> Sil.Aeq (e1, e2)
+  | Sil.Apred (b, a, e) -> Sil.Apred (not b, a, e)
 
 let rec strexp_normalize sub se =
   match se with
@@ -1476,6 +1477,13 @@ let mk_eq e1 e2 =
        let ne2 = exp_normalize Sil.sub_empty e2 in
        atom_normalize Sil.sub_empty (Sil.Aeq (ne1, ne2))) ()
 
+(** Construct a pred. *)
+let mk_pred b a e =
+  Config.run_with_abs_val_equal_zero
+    (fun () ->
+       let ne = exp_normalize Sil.sub_empty e in
+       atom_normalize Sil.sub_empty (Apred (b, a, ne))) ()
+
 (** Construct a points-to predicate for a single program variable.
     If [expand_structs] is true, initialize the fields of structs with fresh variables. *)
 let mk_ptsto_lvar tenv expand_structs inst ((pvar: Pvar.t), texp, expo) : Sil.hpred =
@@ -1608,7 +1616,8 @@ let compute_reachable_atoms pi exps =
     | _ -> false in
   IList.filter
     (function
-      | Sil.Aeq (lhs, rhs) | Sil.Aneq (lhs, rhs) -> exp_contains lhs || exp_contains rhs)
+      | Sil.Aeq (lhs, rhs) | Sil.Aneq (lhs, rhs) -> exp_contains lhs || exp_contains rhs
+      | Sil.Apred (_, _, e) -> exp_contains e)
     pi
 
 (** Eliminates all empty lsegs from sigma, and collect equalities
@@ -1772,8 +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.Aneq (Sil.Attribute att, e)
-  | Sil.Aneq (e, Sil.Attribute att) -> Some (e, att)
+  | Sil.Apred (true, att, e) -> Some (e, att)
   | _ -> None
 
 (** Check whether an atom is used to mark an attribute *)
@@ -1785,8 +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.Aneq (e, Sil.Attribute att)
-    | Sil.Aneq (Sil.Attribute att, e) when Sil.exp_equal e nexp -> att:: attributes
+    | Sil.Apred (true, att, e) when Sil.exp_equal e nexp -> att :: attributes
     | _ -> attributes in
   IList.fold_left atom_get_attr [] prop.pi
 
@@ -1842,29 +1849,26 @@ let get_all_attributes prop =
   IList.rev !res
 
 (** Set an attribute associated to the expression *)
-let set_exp_attribute prop exp att =
-  let exp_att = Sil.Attribute att in
-  conjoin_neq exp exp_att prop
+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 nexp = exp_normalize_prop prop exp in
   let found = ref false in
   let atom_map a = match a with
-    | Sil.Aneq (e, Sil.Attribute att_old)
-    | Sil.Aneq (Sil.Attribute att_old, e) ->
+    | Sil.Apred (true, att_old, e) ->
         if Sil.exp_equal nexp e && (attributes_in_same_category att_old att) then
           begin
             found := true;
             check_attribute_change att_old att;
-            let e1, e2 = exp_reorder e (Sil.Attribute att) in
-            Sil.Aneq (e1, e2)
+            Sil.Apred (true, att, 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 nexp att
+  else set_exp_attribute prop att nexp
 
 let add_or_replace_exp_attribute prop exp att =
   (* wrapper for the most common case: do nothing *)
@@ -1882,9 +1886,8 @@ let mark_vars_as_undefined prop vars_to_mark callee_pname ret_annots loc path_po
 
 let remove_attribute_by_filter ~f prop =
   let atom_remove atom pi = match atom with
-    | Sil.Aneq (e, Sil.Attribute att_old)
-    | Sil.Aneq (Sil.Attribute att_old, e) ->
-        if f att_old e then
+    | Sil.Apred (true, att_old, exp) ->
+        if f att_old exp then
           pi
         else atom:: pi
     | _ -> atom:: pi in
@@ -1936,8 +1939,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.Aneq (e, Sil.Attribute att_old)
-    | Sil.Aneq (Sil.Attribute att_old, e) ->
+    | Sil.Apred (true, att_old, e) ->
         if Sil.attribute_equal att_old att then
           e:: autoreleased_atoms
         else autoreleased_atoms
@@ -1948,16 +1950,11 @@ let get_atoms_with_attribute att prop =
 let attribute_map_resource prop f =
   let pi = get_pi prop in
   let attribute_map e = function
-    | Sil.Aresource ra ->
-        Sil.Aresource (f e ra)
+    | Sil.Aresource ra -> Sil.Aresource (f e ra)
     | att -> att in
-  let atom_map a = match a with
-    | Sil.Aneq (e, Sil.Attribute att)
-    | Sil.Aneq (Sil.Attribute att, e) ->
-        let att' = attribute_map e att in
-        let e1, e2 = exp_reorder e (Sil.Attribute att') in
-        Sil.Aneq (e1, e2)
-    | _ -> a in
+  let atom_map = function
+    | Sil.Apred (b, att, e) -> Sil.Apred (b, attribute_map e att, e)
+    | atom -> atom in
   let pi' = IList.map atom_map pi in
   replace_pi pi' prop
 
@@ -1998,8 +1995,7 @@ let find_arithmetic_problem proc_node_session prop exp =
     | Sil.Lfield (e, _, _) -> walk e
     | Sil.Lindex (e1, e2) -> walk e1; walk e2
     | Sil.Sizeof (_, None, _) -> ()
-    | Sil.Sizeof (_, Some len, _) -> walk len
-    | Sil.Attribute _ -> () in
+    | Sil.Sizeof (_, Some len, _) -> walk len in
   walk exp;
   try Some (Div0 (IList.find check_zero !exps_divided)), !res
   with Not_found ->
@@ -2294,13 +2290,14 @@ let rec exp_captured_ren ren = function
       let e1' = exp_captured_ren ren e1 in
       let e2' = exp_captured_ren ren e2 in
       Sil.Lindex(e1', e2')
-  | Sil.Attribute _ as e -> e
 
 let atom_captured_ren ren = function
   | Sil.Aeq (e1, e2) ->
       Sil.Aeq (exp_captured_ren ren e1, exp_captured_ren ren e2)
   | Sil.Aneq (e1, e2) ->
       Sil.Aneq (exp_captured_ren ren e1, exp_captured_ren ren e2)
+  | Sil.Apred (b, a, e) ->
+      Sil.Apred (b, a, exp_captured_ren ren e)
 
 let rec strexp_captured_ren ren = function
   | Sil.Eexp (e, inst) ->

infer/src/backend/prop.mli

@@ -222,6 +222,9 @@ val mk_neq : exp -> exp -> atom
 (** Construct an equality. *)
 val mk_eq : exp -> exp -> atom
 
+(** Construct a pred. *)
+val mk_pred : bool -> attribute -> exp -> atom
+
 (** create a strexp of the given type, populating the structures if [expand_structs] is true *)
 val create_strexp_of_type :
   Tenv.t option -> struct_init_mode -> Typ.t -> Sil.exp option -> Sil.inst -> Sil.strexp
@@ -313,7 +316,9 @@ val get_all_attributes : 'a t -> (exp * attribute) list
 
 val has_dangling_uninit_attribute : 'a t -> exp -> bool
 
-val set_exp_attribute : normal t -> exp -> attribute -> normal t
+(** Set an attribute associated to the expression *)
+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

infer/src/backend/propgraph.ml

@@ -28,7 +28,7 @@ let from_prop p = p
 (** Return [true] if root node *)
 let rec is_root = function
   | Sil.Var id -> Ident.is_normal id
-  | Sil.Exn _ | Sil.Closure _ | Sil.Const _ | Sil.Lvar _ | Sil.Attribute _ -> true
+  | Sil.Exn _ | Sil.Closure _ | Sil.Const _ | Sil.Lvar _ -> true
   | Sil.Cast (_, e) -> is_root e
   | Sil.UnOp _ | Sil.BinOp _ | Sil.Lfield _ | Sil.Lindex _ | Sil.Sizeof _ -> false
 
@@ -49,6 +49,7 @@ let edge_get_source = function
   | Ehpred (Sil.Hdllseg(_, _, e1, _, _, _, _)) -> e1 (* only one direction supported for now *)
   | Eatom (Sil.Aeq (e1, _)) -> e1
   | Eatom (Sil.Aneq (e1, _)) -> e1
+  | Eatom (Sil.Apred (_, _, e)) -> e
   | Esub_entry (x, _) -> Sil.Var x
 
 (** Return the successor nodes of the edge *)
@@ -56,6 +57,7 @@ let edge_get_succs = function
   | Ehpred hpred -> Sil.ExpSet.elements (Prop.hpred_get_targets hpred)
   | Eatom (Sil.Aeq (_, e2)) -> [e2]
   | Eatom (Sil.Aneq (_, e2)) -> [e2]
+  | Eatom (Sil.Apred _) -> []
   | Esub_entry (_, e) -> [e]
 
 let get_sigma footprint_part g =
@@ -157,6 +159,8 @@ let compute_edge_diff (oldedge: edge) (newedge: edge) : Obj.t list = match olded
       compute_exp_diff e1 e2
   | Eatom (Sil.Aneq (_, e1)), Eatom (Sil.Aneq (_, e2)) ->
       compute_exp_diff e1 e2
+  | Eatom (Sil.Apred (_, _, e1)), Eatom (Sil.Apred (_, _, e2)) ->
+      compute_exp_diff e1 e2
   | Esub_entry (_, e1), Esub_entry (_, e2) ->
       compute_exp_diff e1 e2
   | _ -> [Obj.repr newedge]

infer/src/backend/prover.ml

@@ -363,7 +363,8 @@ end = struct
           leqs := (e1, e2) :: !leqs (* <= *)
       | Sil.Aeq (Sil.BinOp (Binop.Lt, e1, e2), Sil.Const (Const.Cint i)) when IntLit.isone i ->
           lts := (e1, e2) :: !lts (* < *)
-      | Sil.Aeq _ -> () in
+      | Sil.Aeq _
+      | Sil.Apred _ -> () in
     IList.iter process_atom pi;
     saturate { leqs = !leqs; lts = !lts; neqs = !neqs }
 
@@ -554,7 +555,7 @@ let check_zero e =
 let is_root prop base_exp exp =
   let rec f offlist_past e = match e with
     | Sil.Var _ | Sil.Const _ | Sil.UnOp _ | Sil.BinOp _ | Sil.Exn _ | Sil.Closure _ | Sil.Lvar _
-    | Sil.Sizeof _ | Sil.Attribute _ ->
+    | Sil.Sizeof _ ->
         if check_equal prop base_exp e
         then Some offlist_past
         else None
@@ -740,6 +741,7 @@ let check_atom prop a0 =
     when IntLit.isone i -> check_lt_normalized prop e1 e2
   | Sil.Aeq (e1, e2) -> check_equal prop e1 e2
   | Sil.Aneq (e1, e2) -> check_disequal prop e1 e2
+  | Sil.Apred _ -> IList.exists (Sil.atom_equal a) (Prop.get_pi prop)
 
 (** Check [prop |- e1<=e2]. Result [false] means "don't know". *)
 let check_le prop e1 e2 =
@@ -856,7 +858,8 @@ let check_inconsistency_base prop =
     | Sil.Aneq (e1, e2) ->
         (match e1, e2 with
          | Sil.Const c1, Sil.Const c2 -> Const.equal c1 c2
-         | _ -> (Sil.exp_compare e1 e2 = 0)) in
+         | _ -> (Sil.exp_compare e1 e2 = 0))
+    | Sil.Apred _ -> false in
   let inconsistent_inequalities () =
     let ineq = Inequalities.from_prop prop in
     (*
@@ -2108,13 +2111,12 @@ let rec pre_check_pure_implication calc_missing subs pi1 pi2 =
         )
   | Sil.Aeq _ :: pi2' -> (* must be an inequality *)
       pre_check_pure_implication calc_missing subs pi1 pi2'
-  | Sil.Aneq (Sil.Var v, _):: pi2' ->
-      if not (Ident.is_primed v || calc_missing)
-      then raise (IMPL_EXC("ineq e2=f2 in rhs with e2 not primed var", (Sil.sub_empty, Sil.sub_empty), EXC_FALSE))
-      else pre_check_pure_implication calc_missing subs pi1 pi2'
-  | Sil.Aneq _ :: pi2' ->
-      if calc_missing then pre_check_pure_implication calc_missing subs pi1 pi2'
-      else raise (IMPL_EXC ("ineq e2=f2 in rhs with e2 not primed var", (Sil.sub_empty, Sil.sub_empty), EXC_FALSE))
+  | (Sil.Aneq (e, _) | Apred (_, _, e)) :: pi2' ->
+      if calc_missing || (match e with Var v -> Ident.is_primed v | _ -> false) then
+        pre_check_pure_implication calc_missing subs pi1 pi2'
+      else
+        raise (IMPL_EXC ("ineq e2=f2 in rhs with e2 not primed var",
+                         (Sil.sub_empty, Sil.sub_empty), EXC_FALSE))
 
 (** Perform the array bound checks delayed (to instantiate variables) by the prover.
     If there is a provable violation of the array bounds, set the prover status to Bounds_check

infer/src/backend/rearrange.ml

@@ -793,8 +793,7 @@ let add_guarded_by_constraints prop lexp pdesc =
           end
         else
           (* private method. add locked proof obligation to [pdesc] *)
-          let locked_attr = Sil.Attribute Alocked in
-          Prop.conjoin_neq ~footprint:true guarded_by_exp locked_attr prop
+          Prop.set_exp_attribute ~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

infer/src/backend/symExec.ml

@@ -356,8 +356,6 @@ let rec prune ~positive condition prop =
       assert false
   | Sil.Closure _ ->
       assert false
-  | Sil.Attribute _ ->
-      assert false
 
 and prune_inter ~positive condition1 condition2 prop =
   let res = ref Propset.empty in
@@ -1380,9 +1378,8 @@ and check_untainted exp taint_kind caller_pname callee_pname prop =
   | _ ->
       if !Config.footprint then
         let taint_info = { Sil.taint_source = callee_pname; taint_kind; } in
-        let untaint_attr = Sil.Attribute (Sil.Auntaint taint_info) in
         (* add untained(n_lexp) to the footprint *)
-        Prop.conjoin_neq ~footprint:true exp untaint_attr prop
+        Prop.set_exp_attribute ~footprint:true prop (Auntaint taint_info) exp
       else prop
 
 (** execute a call for an unknown or scan function *)

infer/src/backend/tabulation.ml

@@ -385,14 +385,12 @@ let post_process_post
     | Some (Sil.Aresource ({ Sil.ra_kind = Sil.Rrelease })) -> true
     | _ -> false in
   let atom_update_alloc_attribute = function
-    | Sil.Aneq (e , Sil.Attribute (Sil.Aresource ra))
-    | Sil.Aneq (Sil.Attribute (Sil.Aresource ra), e)
+    | Sil.Apred (true, Aresource ra, e)
       when not (ra.Sil.ra_kind = Sil.Rrelease && actual_pre_has_freed_attribute e) ->
         (* unless it was already freed before the call *)
         let vpath, _ = Errdesc.vpath_find post e in
         let ra' = { ra with Sil.ra_pname = callee_pname; Sil.ra_loc = loc; Sil.ra_vpath = vpath } in
-        let c = Sil.Attribute (Sil.Aresource ra') in
-        Sil.Aneq (e, c)
+        Sil.Apred (true, Aresource ra', e)
     | a -> a in
   let prop' = Prop.replace_sigma (post_process_sigma (Prop.get_sigma post) loc) post in
   let pi' = IList.map atom_update_alloc_attribute (Prop.get_pi prop') in
@@ -1263,7 +1261,7 @@ let exe_call_postprocess ret_ids trace_call callee_pname callee_attrs loc result
       let ret_var = Sil.Var ret_id in
       let mark_id_as_retval (p, path) =
         let att_retval = Sil.Aretval (callee_pname, ret_annot) in
-        Prop.set_exp_attribute p ret_var att_retval, path in
+        Prop.set_exp_attribute p att_retval ret_var, path in
       IList.map mark_id_as_retval res
   | _ -> res
 

infer/src/checkers/addressTaken.ml

@@ -33,7 +33,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     | Sil.Exn _
     | Sil.Closure _
     | Sil.Const (Cint _ | Cfun _ | Cstr _ | Cfloat _ | Cclass _ | Cptr_to_fld _)
-    | Sil.Var _ | Sil.Sizeof _ | Sil.Attribute _ ->
+    | Sil.Var _ | Sil.Sizeof _ ->
         astate
 
   let exec_instr astate _ _ = function

infer/src/checkers/checkers.ml

@@ -519,8 +519,7 @@ let callback_check_field_access { Callbacks.proc_desc } =
     | Sil.Lindex (e1, e2) ->
         do_exp is_read e1;
         do_exp is_read e2
-    | Sil.Sizeof _ -> ()
-    | Sil.Attribute _ -> () in
+    | Sil.Sizeof _ -> () in
   let do_read_exp = do_exp true in
   let do_write_exp = do_exp false in
   let do_instr _ = function