Make Aobjc_null attribute a binary predicate

Summary:
Change the Aobjc_null attribute from a family of unary predicates, one
for each Pvar.t * Ident.fieldname list, to a single binary predicate.

This diff should not change behavior except for printing of Aobjc_null
attributes.  Also, operations such as free variables, etc. should now
behave correctly with respect to variables occurring in the arguments of
Aobjc_null.

Reviewed By: cristianoc

Differential Revision: D3669392

fbshipit-source-id: fe4434a

infer/src/IR/Sil.re

@@ -106,7 +106,7 @@ type attribute =
   /** value appeared in second argument of division at given path position */
   | Adiv0 of path_pos
   /** attributed exp is null due to a call to a method with given path as null receiver */
-  | Aobjc_null of Pvar.t (list Ident.fieldname)
+  | Aobjc_null
   /** value was returned from a call to the given procedure, plus the annots of the return value */
   | Aretval of Procname.t Typ.item_annotation
   /** denotes an object registered as an observers to a notification center */
@@ -481,7 +481,7 @@ let attribute_to_category att =>
   | Aunlocked => AClock
   | Aautorelease => ACautorelease
   | Adiv0 _ => ACdiv0
-  | Aobjc_null _ => ACobjc_null
+  | Aobjc_null => ACobjc_null
   | Aretval _ => ACretval
   | Aundef _ => ACundef
   | Aobserver
@@ -528,15 +528,9 @@ let attribute_compare (att1: attribute) (att2: attribute) :int =>
   | (Adiv0 pp1, Adiv0 pp2) => path_pos_compare pp1 pp2
   | (Adiv0 _, _) => (-1)
   | (_, Adiv0 _) => 1
-  | (Aobjc_null v1 fs1, Aobjc_null v2 fs2) =>
-    let n = Pvar.compare v1 v2;
-    if (n != 0) {
-      n
-    } else {
-      IList.compare Ident.fieldname_compare fs1 fs2
-    }
-  | (Aobjc_null _, _) => (-1)
-  | (_, Aobjc_null _) => 1
+  | (Aobjc_null, Aobjc_null) => 0
+  | (Aobjc_null, _) => (-1)
+  | (_, Aobjc_null) => 1
   | (Aretval pn1 annots1, Aretval pn2 annots2) =>
     let n = Procname.compare pn1 pn2;
     if (n != 0) {
@@ -1056,9 +1050,7 @@ let attribute_to_string pe =>
   | Alocked => "LOCKED"
   | Aunlocked => "UNLOCKED"
   | Adiv0 (_, _) => "DIV0"
-  | Aobjc_null v fs =>
-    "OBJC_NULL[" ^
-      String.concat "." [Pvar.to_string v, ...IList.map Ident.fieldname_to_string fs] ^ "]"
+  | Aobjc_null => "OBJC_NULL"
   | Aretval pn _ => "RET" ^ Binop.str pe Lt ^ Procname.to_string pn ^ Binop.str pe Gt
   | Aobserver => "OBSERVER"
   | Aunsubscribed_observer => "UNSUBSCRIBED_OBSERVER";

infer/src/IR/Sil.rei

@@ -94,7 +94,7 @@ type attribute =
   /** value appeared in second argument of division at given path position */
   | Adiv0 of path_pos
   /** attributed exp is null due to a call to a method with given path as null receiver */
-  | Aobjc_null of Pvar.t (list Ident.fieldname)
+  | Aobjc_null
   /** value was returned from a call to the given procedure, plus the annots of the return value */
   | Aretval of Procname.t Typ.item_annotation
   /** denotes an object registered as an observers to a notification center */

infer/src/backend/errdesc.ml

@@ -848,9 +848,8 @@ let create_dereference_desc
       | Some (DExp.Dpvar pvar)
       | Some (DExp.Dpvaraddr pvar) ->
           (match Prop.get_objc_null_attribute prop (Sil.Lvar pvar) with
-           | Some (Apred (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
+           | Some (Apred (Aobjc_null, [_; vfs])) ->
+               Localise.parameter_field_not_null_checked_desc desc vfs
            | _ ->
                desc)
       | Some (DExp.Dretcall (Dconst (Cfun pname), this_dexp :: _, loc, _ ))

infer/src/backend/prop.ml

@@ -2821,7 +2821,7 @@ let find_equal_formal_path e prop =
               | Sil.Hpointsto (Sil.Lvar pvar1, Sil.Eexp (exp2, Sil.Iformal(_, _) ), _)
                 when Sil.exp_equal exp2 e &&
                      (Pvar.is_local pvar1 || Pvar.is_seed pvar1) ->
-                  Some (pvar1, [])
+                  Some (Sil.Lvar pvar1)
               | Sil.Hpointsto (exp1, Sil.Estruct (fields, _), _) ->
                   IList.fold_right (fun (field, strexp) res ->
                       match res with
@@ -2830,15 +2830,15 @@ let find_equal_formal_path e prop =
                           match strexp with
                           | Sil.Eexp (exp2, _) when Sil.exp_equal exp2 e ->
                               (match find_in_sigma exp1 seen_hpreds with
-                               | Some (v, rev_fs) -> Some (v, field :: rev_fs)
+                               | Some vfs -> Some (Sil.Lfield (vfs, field, Typ.Tvoid))
                                | None -> None)
                           | _ -> None) fields None
               | _ -> None) (get_sigma prop) None in
   match find_in_sigma e [] with
-  | Some (v, rev_fs) -> Some (v, IList.rev rev_fs)
+  | Some vfs -> Some vfs
   | None ->
       match get_objc_null_attribute prop e with
-      | Some (Apred (Aobjc_null (v,fs), _)) -> Some (v,fs)
+      | Some (Apred (Aobjc_null, [_; vfs])) -> Some vfs
       | _ -> None
 
 (** translate an if-then-else expression *)

infer/src/backend/prop.mli

@@ -497,7 +497,7 @@ 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 -> 'a t -> (Pvar.t * Ident.fieldname list) option
+val find_equal_formal_path : exp -> 'a t -> exp option
 
 (** return the set of subexpressions of [strexp] *)
 val strexp_get_exps : Sil.strexp -> Sil.ExpSet.t

infer/src/backend/symExec.ml

@@ -737,8 +737,8 @@ let handle_objc_instance_method_call_or_skip actual_pars path callee_pname pre r
     match ret_ids with
     | [ret_id] -> (
         match Prop.find_equal_formal_path receiver prop with
-        | Some (v,fs) ->
-            Prop.add_or_replace_attribute prop (Apred (Aobjc_null (v,fs), [Sil.Var ret_id]))
+        | Some vfs ->
+            Prop.add_or_replace_attribute prop (Apred (Aobjc_null, [Sil.Var ret_id; vfs]))
         | None ->
             Prop.conjoin_eq (Sil.Var ret_id) Sil.exp_zero prop
       )