From b95b71fa858465742f276ae18ca1e6d4052a3442 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Thu, 7 Jul 2016 08:48:29 -0700 Subject: [PATCH] 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 | 6 ++ infer/src/backend/config.mli | 1 + infer/src/backend/modelBuiltins.ml | 2 +- .../null_dereference/malloc_no_null_check.c | 16 +++++ .../endtoend/c/AssertKeepBranchTest.java | 1 - infer/tests/endtoend/c/UnsafeMallocTest.java | 62 +++++++++++++++++++ 6 files changed, 86 insertions(+), 2 deletions(-) create mode 100644 infer/tests/codetoanalyze/c/errors/null_dereference/malloc_no_null_check.c create mode 100644 infer/tests/endtoend/c/UnsafeMallocTest.java diff --git a/infer/src/backend/config.ml b/infer/src/backend/config.ml index 4197f24d0..9c157ab1b 100644 --- a/infer/src/backend/config.ml +++ b/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 diff --git a/infer/src/backend/config.mli b/infer/src/backend/config.mli index 54ef9cc13..31c90b202 100644 --- a/infer/src/backend/config.mli +++ b/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 diff --git a/infer/src/backend/modelBuiltins.ml b/infer/src/backend/modelBuiltins.ml index 332b233ee..52cf89673 100644 --- a/infer/src/backend/modelBuiltins.ml +++ b/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) diff --git a/infer/tests/codetoanalyze/c/errors/null_dereference/malloc_no_null_check.c b/infer/tests/codetoanalyze/c/errors/null_dereference/malloc_no_null_check.c new file mode 100644 index 000000000..6c7d327eb --- /dev/null +++ b/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 + +void test_malloc() { + char* x = malloc(1); + *x = 42; + free(x); +} diff --git a/infer/tests/endtoend/c/AssertKeepBranchTest.java b/infer/tests/endtoend/c/AssertKeepBranchTest.java index cadb14412..f45b43210 100644 --- a/infer/tests/endtoend/c/AssertKeepBranchTest.java +++ b/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; diff --git a/infer/tests/endtoend/c/UnsafeMallocTest.java b/infer/tests/endtoend/c/UnsafeMallocTest.java new file mode 100644 index 000000000..829282532 --- /dev/null +++ b/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 inferCommand; + + @ClassRule + public static DebuggableTemporaryFolder folder = new DebuggableTemporaryFolder(); + + @BeforeClass + public static void runInfer() throws InterruptedException, IOException { + inferCommand = InferRunner.createCInferCommand( + folder, + SOURCE_FILE, + ImmutableList.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" + ) + ); + } + +}