add option to assume that malloc never returns null

Summary:
Call infer with `--unsafe-malloc` or set `unsafe-malloc: true,` in .inferconfig to
have infer assume that `malloc()` never returns null.

closes #389

Reviewed By: jberdine

Differential Revision: D3522169

fbshipit-source-id: 6b88a16

infer/src/backend/config.ml

@@ -1005,6 +1005,11 @@ and unit_test =
   CLOpt.mk_bool ~deprecated:["unit_test"] ~long:"unit-test"
     "Print unit test code"
 
+and unsafe_malloc =
+  CLOpt.mk_bool ~long:"unsafe-malloc"
+    ~exes:CLOpt.[Analyze;Toplevel]
+    "Assume that malloc(3) never returns null."
+
 and verbose_out =
   CLOpt.mk_string ~deprecated:["verbose_out"] ~long:"verbose-out" ~default:""
     ~exes:CLOpt.[Java] ~meta:"file" "Set the path to the javac verbose output"
@@ -1347,6 +1352,7 @@ and trace_join = !trace_join
 and trace_rearrange = !trace_rearrange
 and type_size = !type_size
 and unit_test = !unit_test
+and unsafe_malloc = !unsafe_malloc
 and whole_seconds = !whole_seconds
 and worklist_mode = !worklist_mode
 and write_dotty = !write_dotty

infer/src/backend/config.mli

@@ -227,6 +227,7 @@ val trace_join : bool
 val trace_rearrange : bool
 val type_size : bool
 val unit_test : bool
+val unsafe_malloc : bool
 val whole_seconds : bool
 val worklist_mode : int
 val write_dotty : bool

infer/src/backend/modelBuiltins.ml

@@ -1114,7 +1114,7 @@ let _ = Builtin.register
     "fwscanf" (execute_scan_function 2)
 let _ = Builtin.register
     (* malloc from C library *)
-    "malloc" (execute_alloc Sil.Mmalloc true)
+    "malloc" (execute_alloc Sil.Mmalloc (not Config.unsafe_malloc))
 let malloc_no_fail = Builtin.register
     (* malloc from ObjC library *)
     "malloc_no_fail" (execute_alloc Sil.Mmalloc false)

infer/tests/codetoanalyze/c/errors/null_dereference/malloc_no_null_check.c

@@ -0,0 +1,16 @@
+/*
+ * Copyright (c) 2016 - 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.
+ */
+
+#include <stdlib.h>
+
+void test_malloc() {
+  char* x = malloc(1);
+  *x = 42;
+  free(x);
+}

infer/tests/endtoend/c/AssertKeepBranchTest.java

@@ -11,7 +11,6 @@ package endtoend.c;
 
 import static org.hamcrest.MatcherAssert.assertThat;
 import static utils.matchers.ResultContainsExactly.containsExactly;
-import static utils.matchers.ResultContainsNoErrorInMethod.doesNotContain;
 
 import com.google.common.collect.ImmutableList;
 

infer/tests/endtoend/c/UnsafeMallocTest.java

@@ -0,0 +1,62 @@
+/*
+ * Copyright (c) 2016 - 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.c;
+
+import com.google.common.collect.ImmutableList;
+
+import static org.hamcrest.MatcherAssert.assertThat;
+import static utils.matchers.ResultContainsNoErrorInMethod.doesNotContain;
+
+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 UnsafeMallocTest {
+
+  public static final String SOURCE_FILE =
+      "infer/tests/codetoanalyze/c/errors/null_dereference/malloc_no_null_check.c";
+
+  public static final String NULL_DEREFERENCE = "NULL_DEREFERENCE";
+  private static ImmutableList<String> inferCommand;
+
+  @ClassRule
+  public static DebuggableTemporaryFolder folder = new DebuggableTemporaryFolder();
+
+  @BeforeClass
+  public static void runInfer() throws InterruptedException, IOException {
+    inferCommand = InferRunner.createCInferCommand(
+      folder,
+      SOURCE_FILE,
+      ImmutableList.<String>of("--unsafe-malloc"));
+  }
+
+  @Test
+  public void unsafeMallocTest() throws InterruptedException, IOException, InferException {
+    InferResults inferResults = InferRunner.runInferC(inferCommand);
+
+    assertThat(
+        "Results should not contain null pointer dereference error",
+        inferResults,
+        doesNotContain(
+            NULL_DEREFERENCE,
+            SOURCE_FILE,
+            "test_malloc"
+        )
+    );
+  }
+
+}