[objc] Do not fail in the bi-abduction with missing fields in ObjC

Reviewed By: sblackshear

Differential Revision: D6099481

fbshipit-source-id: 00e0889

infer/src/backend/tabulation.ml

@@ -1076,21 +1076,21 @@ let exe_spec tenv ret_id_opt (n, nspecs) caller_pdesc callee_pname loc prop path
           Invalid_res (Dereference_error (deref_error, desc, pjoin))
       | None
        -> let split = do_split () in
-          (* check if a missing_fld hpred is about a hidden field *)
+          (* check if a missing_fld hpred is from a dyn language (ObjC) *)
-          let hpred_missing_hidden = function
+          let hpred_missing_objc_class = function
-            | Sil.Hpointsto (_, Sil.Estruct ([(fld, _)], _), _)
+            | Sil.Hpointsto (_, Sil.Estruct (_, _), Exp.Sizeof {typ})
-             -> Typ.Fieldname.is_hidden fld
+             -> Typ.is_objc_class typ
             | _
              -> false
           in
           (* missing fields minus hidden fields *)
-          let missing_fld_nohidden =
+          let missing_fld_not_objc_class =
-            List.filter ~f:(fun hp -> not (hpred_missing_hidden hp)) missing_fld
+            List.filter ~f:(fun hp -> not (hpred_missing_objc_class hp)) missing_fld
           in
           if not !Config.footprint && split.missing_sigma <> [] then (
             L.d_strln "Implication error: missing_sigma not empty in re-execution" ;
             Invalid_res Missing_sigma_not_empty )
-          else if not !Config.footprint && missing_fld_nohidden <> [] then (
+          else if not !Config.footprint && missing_fld_not_objc_class <> [] then (
             L.d_strln "Implication error: missing_fld not empty in re-execution" ;
             Invalid_res Missing_fld_not_empty )
           else report_valid_res split

infer/tests/build_systems/codetoanalyze/objc_getters_setters/A.h

@@ -13,4 +13,6 @@
 
 @property(nullable, nonatomic, copy) NSData* metadata;
 
+- (int)getX;
+
 @end

infer/tests/build_systems/codetoanalyze/objc_getters_setters/A.m

@@ -8,6 +8,20 @@
  */
 #import "A.h"
 
-@implementation A
+@implementation A {
+
+  int _x;
+  NSString* _name;
+}
+
+- (instancetype)withMetadata:(NSString*)name {
+  self->_x = 5;
+  self->_name = name;
+  return self;
+}
+
+- (int)getX {
+  return _x;
+}
 
 @end

infer/tests/build_systems/codetoanalyze/objc_getters_setters/B.m

@@ -10,7 +10,9 @@
 #import "A.h"
 #import "B.h"
 
-@implementation B
+@implementation B {
+  A* _a;
+}
 
 - (int)npe_no_bad_footprint_in_getter:(A*)a {
   int* p = nil;
@@ -23,4 +25,25 @@
   a.metadata = metadata; // Doesn't crash here with Bad_footprint
   return *p; // NPE
 }
+
+- (instancetype)infer_field_get_spec:(NSData*)m {
+  A* a = [A alloc];
+  [a withMetadata:m]; // Doesn't crash here with Precondition_not_met, get
+                      // correct spec with a.x=5
+  self->_a = a;
+  return self;
+}
+
+- (int)npe_no_precondition_not_met:(NSData*)m {
+  [self infer_field_get_spec:m];
+  if ([self->_a getX] == 5) {
+    int* p_true = nil;
+    return *p_true; // NPE
+  } else {
+    int* p_false = nil;
+    return *p_false; // no NPE, because we know the value of a._x is 5 because
+                     // we get the correct spec in the method
+                     // infer_field_get_spec
+  }
+}
 @end

infer/tests/build_systems/objc_getters_setters/issues.exp

@@ -1,2 +1,3 @@
 build_systems/codetoanalyze/objc_getters_setters/B.m, B_npe_no_bad_footprint_in_getter:, 3, NULL_DEREFERENCE, [start of procedure npe_no_bad_footprint_in_getter:]
 build_systems/codetoanalyze/objc_getters_setters/B.m, B_npe_no_bad_footprint_in_setter:andMetadata:, 3, NULL_DEREFERENCE, [start of procedure npe_no_bad_footprint_in_setter:andMetadata:]
+build_systems/codetoanalyze/objc_getters_setters/B.m, B_npe_no_precondition_not_met:, 4, NULL_DEREFERENCE, [start of procedure npe_no_precondition_not_met:,start of procedure infer_field_get_spec:,start of procedure withMetadata:,return from a call to A_withMetadata:,return from a call to B_infer_field_get_spec:,start of procedure getX,return from a call to A_getX,Condition is true]