Tighten type of Aobjc_null to reduce recursion

Summary:
The Aobjc_null attribute does not need a fully general exp.  This diff
refines this to a possibly-empty path of fields starting from a pvar,
which reduces interdependence between Sil types.

Reviewed By: dulmarod

Differential Revision: D3548043

fbshipit-source-id: 49d16ab

infer/src/IR/Sil.re

@@ -454,8 +454,8 @@ and attribute =
   | Aunlocked
   /** value appeared in second argument of division at given path position */
   | Adiv0 of path_pos
-  /** the exp. is null because of a call to a method with exp as a null receiver */
-  | Aobjc_null of exp
+  /** 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)
   /** 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 */
@@ -1039,7 +1039,13 @@ let rec attribute_compare (att1: attribute) (att2: attribute) :int =>
   | (Adiv0 pp1, Adiv0 pp2) => path_pos_compare pp1 pp2
   | (Adiv0 _, _) => (-1)
   | (_, Adiv0 _) => 1
-  | (Aobjc_null exp1, Aobjc_null exp2) => exp_compare exp1 exp2
+  | (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
   | (Aretval pn1 annots1, Aretval pn2 annots2) =>
@@ -1739,15 +1745,9 @@ and attribute_to_string pe =>
   | Alocked => "LOCKED"
   | Aunlocked => "UNLOCKED"
   | Adiv0 (_, _) => "DIV0"
-  | Aobjc_null exp => {
-      let info_s =
-        switch exp {
-        | Lvar var => "FORMAL " ^ Pvar.to_string var
-        | Lfield _ => "FIELD " ^ exp_to_string exp
-        | _ => ""
-        };
-      "OBJC_NULL[" ^ info_s ^ "]"
-    }
+  | Aobjc_null v fs =>
+    "OBJC_NULL[" ^
+      String.concat "." [Pvar.to_string v, ...IList.map Ident.fieldname_to_string fs] ^ "]"
   | Aretval pn _ => "RET" ^ str_binop pe Lt ^ Procname.to_string pn ^ str_binop pe Gt
   | Aobserver => "OBSERVER"
   | Aunsubscribed_observer => "UNSUBSCRIBED_OBSERVER"
@@ -3382,13 +3382,6 @@ let rec exp_sub_ids (f: Ident.t => exp) exp =>
     } else {
       Closure {...c, captured_vars}
     }
-  | Const (Cattribute (Aobjc_null e)) =>
-    let e' = exp_sub_ids f e;
-    if (e' === e) {
-      exp
-    } else {
-      Const (Cattribute (Aobjc_null e'))
-    }
   | Const (Cint _ | Cfun _ | Cstr _ | Cfloat _ | Cattribute _ | Cclass _ | Cptr_to_fld _) => exp
   | Cast t e =>
     let e' = exp_sub_ids f e;

infer/src/IR/Sil.rei

@@ -181,8 +181,8 @@ and attribute =
   | Aunlocked
   /** value appeared in second argument of division at given path position */
   | Adiv0 of path_pos
-  /** the exp. is null because of a call to a method with exp as a null receiver */
-  | Aobjc_null of exp
+  /** 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)
   /** 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

@@ -849,8 +849,11 @@ let create_dereference_desc
       | Some (Sil.Dpvar pvar)
       | Some (Sil.Dpvaraddr pvar) ->
           (match Prop.get_objc_null_attribute prop (Sil.Lvar pvar) with
-           | Some (Sil.Aobjc_null info) -> Localise.parameter_field_not_null_checked_desc desc info
-           | _ -> desc)
+           | Some (Sil.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
+           | _ ->
+               desc)
       | Some (Sil.Dretcall (Dconst (Cfun pname), this_dexp :: _, loc, _ ))
         when is_vector_method pname ->
           Localise.desc_empty_vector_access (Some pname) (Sil.dexp_to_string this_dexp) loc

infer/src/backend/prop.ml

@@ -2786,7 +2786,7 @@ let trans_land_lor op ((idl1, stml1), e1) ((idl2, stml2), e2) loc =
       ((id:: idl1@idl2, stml1@instrs2), Sil.Var id)
     end
 
-(** Input of this mehtod is an exp in a prop. Output is a formal variable or path from a
+(** 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 =
@@ -2803,7 +2803,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 (Sil.Lvar pvar1)
+                  Some (pvar1, [])
               | Sil.Hpointsto (exp1, Sil.Estruct (fields, _), _) ->
                   IList.fold_right (fun (field, strexp) res ->
                       match res with
@@ -2812,15 +2812,16 @@ 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 exp' -> Some (Sil.Lfield (exp', field, Typ.Tvoid))
+                               | Some (v, rev_fs) -> Some (v, field :: rev_fs)
                                | None -> None)
                           | _ -> None) fields None
               | _ -> None) (get_sigma prop) None in
   match find_in_sigma e [] with
-  | Some res -> Some res
-  | None -> match get_objc_null_attribute prop e with
-    | Some (Sil.Aobjc_null exp) -> Some exp
-    | _ -> None
+  | 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)
+      | _ -> None
 
 (** translate an if-then-else expression *)
 let trans_if_then_else ((idl1, stml1), e1) ((idl2, stml2), e2) ((idl3, stml3), e3) loc =

infer/src/backend/prop.mli

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

infer/src/backend/symExec.ml

@@ -733,11 +733,13 @@ let handle_objc_instance_method_call_or_skip actual_pars path callee_pname pre r
     | _ -> 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
-         | Some info ->
-             Prop.add_or_replace_exp_attribute prop (Sil.Var ret_id) (Sil.Aobjc_null info)
-         | None -> Prop.conjoin_eq (Sil.Var ret_id) Sil.exp_zero prop)
+    | [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))
+        | None ->
+            Prop.conjoin_eq (Sil.Var ret_id) Sil.exp_zero prop
+      )
     | _ -> prop in
   if is_receiver_null then
     (* objective-c instance method with a null receiver just return objc_null(res) *)