diff --git a/infer/models/c/src/infer_builtins.c b/infer/models/c/src/infer_builtins.c index c387e6cbb..76cd92922 100644 --- a/infer/models/c/src/infer_builtins.c +++ b/infer/models/c/src/infer_builtins.c @@ -84,13 +84,7 @@ clock_t __infer_nondet_clock_t() { return t; } -long infer__builtin_expect(long e, long x) { - if (e == x) { - return x; - } else { - return e; - } -} +long infer__builtin_expect(long e, long x) { return e; } void* infer__builtin___memset_chk(void* dest, int val, diff --git a/infer/src/clang/cFrontend_config.ml b/infer/src/clang/cFrontend_config.ml index 6f26769e8..b0dd95ae6 100644 --- a/infer/src/clang/cFrontend_config.ml +++ b/infer/src/clang/cFrontend_config.ml @@ -151,6 +151,8 @@ let handleFailureInFunction = "handleFailureInFunction:file:lineNumber:descripti let fbAssertWithSignalAndLogFunctionHelper = "FBAssertWithSignalAndLogFunctionHelper" +let google_LogMessageFatal = "google::LogMessageFatal_LogMessageFatal" + let pseudo_object_type = "" let count = "count" diff --git a/infer/src/clang/cFrontend_config.mli b/infer/src/clang/cFrontend_config.mli index 5a6d955ba..06a0ec274 100644 --- a/infer/src/clang/cFrontend_config.mli +++ b/infer/src/clang/cFrontend_config.mli @@ -143,6 +143,8 @@ val handleFailureInMethod : string val handleFailureInFunction : string +val google_LogMessageFatal : string + val pseudo_object_type : string val count : string diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml index 9225369a9..9a74018f4 100644 --- a/infer/src/clang/cTrans.ml +++ b/infer/src/clang/cTrans.ml @@ -855,10 +855,7 @@ struct res_trans_callee :: res_trans_p in let sil_fe, is_cf_retain_release = CTrans_models.builtin_predefined_model fun_exp_stmt sil_fe in if CTrans_models.is_assert_log sil_fe then - if Config.report_custom_error then - CTrans_utils.trans_assertion_failure sil_loc context - else - CTrans_utils.trans_assume_false sil_loc context trans_state.succ_nodes + CTrans_utils.trans_assertion sil_loc context trans_state.succ_nodes else let act_params = let params = IList.tl (collect_exprs result_trans_subexprs) in @@ -912,7 +909,10 @@ struct let callee_pname = match sil_method with | Sil.Const (Sil.Cfun pn) -> pn | _ -> assert false (* method pointer not implemented, this shouldn't happen *) in - (* As we may have nodes coming from different parameters we need to *) + if CTrans_models.is_assert_log sil_method then + CTrans_utils.trans_assertion sil_loc context trans_state_pri.succ_nodes + else + (* As we may have nodes coming from different parameters we need to *) (* call instruction for each parameter and collect the results *) (* afterwards. The 'instructions' function does not do that *) let trans_state_param = @@ -1015,9 +1015,7 @@ struct | _ -> None (* assertions *) else if CTrans_models.is_handleFailureInMethod selector then - if Config.report_custom_error then - Some (CTrans_utils.trans_assertion_failure sil_loc context) - else Some (CTrans_utils.trans_assume_false sil_loc context trans_state.succ_nodes) + Some (CTrans_utils.trans_assertion sil_loc context trans_state.succ_nodes) else None diff --git a/infer/src/clang/cTrans_models.ml b/infer/src/clang/cTrans_models.ml index f80792dbd..1b727d807 100644 --- a/infer/src/clang/cTrans_models.ml +++ b/infer/src/clang/cTrans_models.ml @@ -78,6 +78,9 @@ let is_assert_log_s funct = funct = CFrontend_config.assert_fail || funct = CFrontend_config.fbAssertWithSignalAndLogFunctionHelper +let is_assert_log_method m = + m = CFrontend_config.google_LogMessageFatal + let is_handleFailureInMethod funct = funct = CFrontend_config.handleFailureInMethod || funct = CFrontend_config.handleFailureInFunction @@ -114,9 +117,11 @@ let builtin_predefined_model fun_stmt sil_fe = (** If the function is a builtin model, return the model, otherwise return the function *) let is_assert_log sil_fe = match sil_fe with - | Sil.Const (Sil.Cfun pn) when is_assert_log_s (Procname.to_string pn) -> true + | Sil.Const (Sil.Cfun (Procname.ObjC_Cpp _ as pn)) -> is_assert_log_method (Procname.to_string pn) + | Sil.Const (Sil.Cfun (Procname.C _ as pn)) -> is_assert_log_s (Procname.to_string pn) | _ -> false + let is_objc_memory_model_controlled o = Core_foundation_model.is_objc_memory_model_controlled o diff --git a/infer/src/clang/cTrans_utils.ml b/infer/src/clang/cTrans_utils.ml index 15ba865c8..964043d63 100644 --- a/infer/src/clang/cTrans_utils.ml +++ b/infer/src/clang/cTrans_utils.ml @@ -464,6 +464,11 @@ let trans_assume_false sil_loc context succ_nodes = Cfg.Node.set_succs_exn context.CContext.cfg prune_node succ_nodes []; { empty_res_trans with root_nodes = [prune_node]; leaf_nodes = [prune_node] } +let trans_assertion sil_loc context succ_nodes = + if Config.report_custom_error then + trans_assertion_failure sil_loc context + else trans_assume_false sil_loc context succ_nodes + let define_condition_side_effects e_cond instrs_cond sil_loc = let (e', typ) = extract_exp_from_list e_cond "\nWARNING: Missing expression in IfStmt. Need to be fixed\n" in match e' with diff --git a/infer/src/clang/cTrans_utils.mli b/infer/src/clang/cTrans_utils.mli index 8cef73974..f5349a74f 100644 --- a/infer/src/clang/cTrans_utils.mli +++ b/infer/src/clang/cTrans_utils.mli @@ -85,9 +85,7 @@ val cast_operation : trans_state -> Clang_ast_t.cast_kind -> (Sil.exp * Sil.typ) list -> Sil.typ -> Location.t -> bool -> Ident.t list * Sil.instr list * (Sil.exp * Sil.typ) -val trans_assertion_failure : Location.t -> CContext.t -> trans_result - -val trans_assume_false : Location.t -> CContext.t -> Cfg.Node.t list -> trans_result +val trans_assertion: Location.t -> CContext.t -> Cfg.Node.t list -> trans_result val is_owning_method : Clang_ast_t.stmt -> bool diff --git a/infer/tests/codetoanalyze/c/errors/assertions/assertion_example.c b/infer/tests/codetoanalyze/c/errors/assertions/assertion_example.c new file mode 100644 index 000000000..e022631df --- /dev/null +++ b/infer/tests/codetoanalyze/c/errors/assertions/assertion_example.c @@ -0,0 +1,18 @@ +/* + * 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 + +// We should report here no NPE, but also we should report div0 to show that we +// get the +// non-assertion branch. +int report_div0_and_no_npe(int* p) { + assert(p); + return *p / 0; +} diff --git a/infer/tests/codetoanalyze/c/frontend/conditional_operator/assert_example.c b/infer/tests/codetoanalyze/c/frontend/assertions/assert_example.c similarity index 100% rename from infer/tests/codetoanalyze/c/frontend/conditional_operator/assert_example.c rename to infer/tests/codetoanalyze/c/frontend/assertions/assert_example.c diff --git a/infer/tests/codetoanalyze/c/frontend/conditional_operator/assert_example.c.dot b/infer/tests/codetoanalyze/c/frontend/assertions/assert_example.c.dot similarity index 100% rename from infer/tests/codetoanalyze/c/frontend/conditional_operator/assert_example.c.dot rename to infer/tests/codetoanalyze/c/frontend/assertions/assert_example.c.dot diff --git a/infer/tests/codetoanalyze/cpp/errors/assertions/check_examples.cpp b/infer/tests/codetoanalyze/cpp/errors/assertions/check_examples.cpp new file mode 100644 index 000000000..45e907c3a --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/errors/assertions/check_examples.cpp @@ -0,0 +1,58 @@ +/* + * 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. + */ + +/*WARNING: This is not being tested in the endtoend tests because it requires + glog library. + Only to be run manually */ + +#include + +int log_fatal_example() { + int* p = nullptr; + if (p == nullptr) { + LOG(FATAL) << "this will crash\n"; + } + return *p; // program should never get here +} + +int check_example(int* a) { + CHECK(a); + return *a; // no null deref flagged by Infer +} + +int log_non_fatal_example() { + int* a = nullptr; + LOG_IF(INFO, a) << "well\n"; + LOG_IF(WARNING, a) << "well\n"; + LOG_IF(ERROR, a) << "well\n"; + return *a; // null deref flagged by Infer +} + +int log_if_fatal_example() { + int* a = nullptr; + LOG_IF(FATAL, !a) << "well\n"; + return *a; // no null deref +} + +// Still not modelled + +int check_ne_example(int x) { + CHECK_NE(x, 5); + return x; +} + +int check_eq_example(int x, int y) { + CHECK_EQ(x, y); + return x; +} + +int check_not_null_example(int* p) { + CHECK_NOTNULL(p); + return *p; +} diff --git a/infer/tests/endtoend/c/AssertKeepBranchTest.java b/infer/tests/endtoend/c/AssertKeepBranchTest.java new file mode 100644 index 000000000..cadb14412 --- /dev/null +++ b/infer/tests/endtoend/c/AssertKeepBranchTest.java @@ -0,0 +1,61 @@ +/* + * 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.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; + +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 AssertKeepBranchTest { + + public static final String source_file = "assertions/assertion_example.c"; + + private static ImmutableList inferCmd; + + public static final String DIVIDE_BY_ZERO = "DIVIDE_BY_ZERO"; + + private static InferResults inferResults; + + @BeforeClass + public static void runInfer() throws InterruptedException, IOException { + inferResults = InferResults.loadCInferResults(AssertKeepBranchTest.class, source_file); + } + + @Test + public void whenRunsOnAssertionExampleThenDiv0AndNoNPEIsFound() + throws InterruptedException, IOException, InferException { + String[] methods = { + "report_div0_and_no_npe", + }; + assertThat( + "Results should contain " + DIVIDE_BY_ZERO, + inferResults, + containsExactly( + DIVIDE_BY_ZERO, + source_file, + methods + ) + ); + } + +} diff --git a/infer/tests/endtoend/c/AssertTest.java b/infer/tests/endtoend/c/AssertTest.java index 29cc961ba..2a13621b3 100644 --- a/infer/tests/endtoend/c/AssertTest.java +++ b/infer/tests/endtoend/c/AssertTest.java @@ -28,7 +28,7 @@ import utils.InferRunner; public class AssertTest { public static final String source_file = - "infer/tests/codetoanalyze/c/frontend/conditional_operator/assert_example.c"; + "infer/tests/codetoanalyze/c/frontend/assertions/assert_example.c"; private static ImmutableList inferCmd; diff --git a/infer/tests/frontend/c/AssertionTest.java b/infer/tests/frontend/c/AssertionTest.java new file mode 100644 index 000000000..1ca08a9b2 --- /dev/null +++ b/infer/tests/frontend/c/AssertionTest.java @@ -0,0 +1,41 @@ +/* + * 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 frontend.c; + +import org.junit.Ignore; +import org.junit.Rule; +import org.junit.Test; + +import java.io.IOException; + +import utils.DebuggableTemporaryFolder; +import utils.InferException; +import utils.ClangFrontendUtils; + +public class AssertionTest { + + String conditionalOperatorBasePath = "infer/tests/codetoanalyze/c/frontend/assertions/"; + + @Rule + public DebuggableTemporaryFolder folder = new DebuggableTemporaryFolder(); + + void frontendTest(String fileRelative) throws InterruptedException, IOException, InferException { + ClangFrontendUtils.createAndCompareCDotFiles( + folder, + conditionalOperatorBasePath + fileRelative); + } + + @Ignore @Test + public void whenCaptureRunOnAssertExampleThenDotFilesAreTheSame() + throws InterruptedException, IOException, InferException { + frontendTest("assert_example.c"); + } + +} diff --git a/infer/tests/frontend/c/ConditionalOperatorTest.java b/infer/tests/frontend/c/ConditionalOperatorTest.java index 379f14a27..010d38c5f 100644 --- a/infer/tests/frontend/c/ConditionalOperatorTest.java +++ b/infer/tests/frontend/c/ConditionalOperatorTest.java @@ -48,12 +48,6 @@ public class ConditionalOperatorTest { frontendTest("cond2.c"); } - @Ignore @Test - public void whenCaptureRunOnAssertExampleThenDotFilesAreTheSame() - throws InterruptedException, IOException, InferException { - frontendTest("assert_example.c"); - } - @Test public void whenCaptureRunOnIntNegationThenDotFilesAreTheSame() throws InterruptedException, IOException, InferException {