Nullify variables with objc flags if they appear in conditions

Summary:
public To deal with ObjC nullability and give meaningful error
messages, we introduced the ObjC_NULL attribute in the symbolic execution to
mean that the object carrying the attribute is null because it was the result
of a method call from a null object. However, one cannot add attributes to null,
so we had to delay nullifying the object in order to have the attribute until we
can assign it to a program variable. However, if the temp variable was used in a condition,
we were not taking into account that its meaning is null. This diff addresses that and fixes
many FPs that we have encounter.

Reviewed By: ddino

Differential Revision: D2765167

fb-gh-sync-id: c0878dd

infer/src/backend/prop.ml

@@ -1897,6 +1897,21 @@ let replace_objc_null prop lhs_exp rhs_exp =
       add_or_replace_exp_attribute prop lhs_exp att
   | _ -> prop
 
+let rec nullify_exp_with_objc_null prop exp =
+  match exp with
+  | Sil.BinOp (op, exp1, exp2) ->
+      let prop' = nullify_exp_with_objc_null prop exp1 in
+      nullify_exp_with_objc_null prop' exp2
+  | Sil.UnOp (op, exp, _) ->
+      nullify_exp_with_objc_null prop exp
+  | Sil.Var name ->
+      (match get_objc_null_attribute prop exp with
+       | Some att ->
+           let prop' = remove_attribute_from_exp att prop exp in
+           conjoin_eq exp Sil.exp_zero prop'
+       | _ -> prop)
+  | _ -> prop
+
 (** Get all the attributes of the prop *)
 let get_atoms_with_attribute att prop =
   let atom_remove atom autoreleased_atoms = match atom with

infer/src/backend/prop.mli

@@ -312,6 +312,8 @@ val remove_attribute : Sil.attribute -> 'a t -> normal t
 (** [replace_objc_null lhs rhs]. If rhs has the objc_null attribute, replace the attribute and set the lhs = 0 *)
 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
 

infer/src/backend/symExec.ml

@@ -953,6 +953,7 @@ let rec sym_exec cfg tenv pdesc _instr (_prop: Prop.normal Prop.t) path
       execute_set pname pdesc tenv lhs_exp typ rhs_exp loc _prop
       |> ret_old_path
   | Sil.Prune (cond, loc, true_branch, ik) ->
+      let _prop = Prop.nullify_exp_with_objc_null _prop cond in
       let check_condition_always_true_false () =
         let report_condition_always_true_false i =
           let skip_loop = match ik with

infer/tests/codetoanalyze/objc/errors/npe/ObjCMethodCallInCondition.m

@@ -0,0 +1,41 @@
+/*
+ * Copyright (c) 2015 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ */
+
+#import <Foundation/NSObject.h>
+#import <Foundation/NSData.h>
+
+@interface A : NSObject
+
+@property (nonatomic) A* child;
+
+@property (nonatomic) A* url;
+
+@end
+
+@implementation A
+
+- (void)testLength:(NSData *)imageData
+{
+    unsigned char *pixels = (unsigned char *)[imageData bytes];
+
+    if (imageData.length > 0) {
+        pixels[0] = 255;
+    }
+}
+
+A* testUrl(A* context)
+{
+    if (context.url) {
+        A* entityMemObject = context.child;
+        return entityMemObject->_child;
+    }
+    return nil;
+}
+
+@end

infer/tests/endtoend/objc/NPEObjCMethodInConditionTest.java

@@ -0,0 +1,64 @@
+/*
+ * Copyright (c) 2013 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ */
+
+package endtoend.objc;
+
+import static org.hamcrest.MatcherAssert.assertThat;
+import static utils.matchers.ResultContainsExactly.containsExactly;
+
+import com.google.common.collect.ImmutableList;
+
+import org.junit.BeforeClass;
+import org.junit.ClassRule;
+import org.junit.Test;
+
+import java.io.IOException;
+
+import utils.DebuggableTemporaryFolder;
+import utils.InferException;
+import utils.InferResults;
+import utils.InferRunner;
+
+public class NPEObjCMethodInConditionTest {
+
+  public static final String NPE_FILE =
+      "infer/tests/codetoanalyze/objc/errors/npe/ObjCMethodCallInCondition.m";
+
+  private static ImmutableList<String> inferCmdNPD;
+
+  public static final String PARAMETER_NOT_NULL_CHECKED = "PARAMETER_NOT_NULL_CHECKED";
+
+  @ClassRule
+  public static DebuggableTemporaryFolder folderNPD = new DebuggableTemporaryFolder();
+
+  @BeforeClass
+  public static void runInfer() throws InterruptedException, IOException {
+    inferCmdNPD = InferRunner.createiOSInferCommandWithMLBuckets(
+        folderNPD,
+        NPE_FILE,
+        "cf",
+        true);
+  }
+
+  @Test
+  public void whenInferRunsOncaptureManagerSessionDidStartThenNoNPEFound()
+      throws InterruptedException, IOException, InferException {
+    InferResults inferResults = InferRunner.runInferObjC(inferCmdNPD);
+    String[] procedures = {};
+    assertThat(
+        "Results should not contain parameter not null checked",
+        inferResults,
+        containsExactly(
+            PARAMETER_NOT_NULL_CHECKED,
+            NPE_FILE,
+            procedures
+        )
+    );
+  }
+}