Model CHECK macro and fix the model for builtin_expect

Reviewed By: akotulski

Differential Revision: D3264368

fb-gh-sync-id: 1f79e19
fbshipit-source-id: 1f79e19

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) {
+long infer__builtin_expect(long e, long x) { return e; }
-  if (e == x) {
-    return x;
-  } else {
-    return e;
-  }
-}
 
 void* infer__builtin___memset_chk(void* dest,
                                   int val,

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 = "<pseudo-object type>"
 
 let count = "count"

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

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 sil_loc context trans_state.succ_nodes
-        CTrans_utils.trans_assertion_failure sil_loc context
-      else
-        CTrans_utils.trans_assume_false sil_loc context trans_state.succ_nodes
     else
       let act_params =
         let params = IList.tl (collect_exprs result_trans_subexprs) in
@@ -912,6 +909,9 @@ 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
+    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          *)
@@ -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 sil_loc context trans_state.succ_nodes)
-        Some (CTrans_utils.trans_assertion_failure sil_loc context)
-      else Some (CTrans_utils.trans_assume_false sil_loc context trans_state.succ_nodes)
     else None
 
 

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
 

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

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_assertion: Location.t -> CContext.t -> Cfg.Node.t list ->  trans_result
-
-val trans_assume_false : Location.t -> CContext.t -> Cfg.Node.t list ->  trans_result
 
 val is_owning_method : Clang_ast_t.stmt -> bool
 

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 <assert.h>
+
+// 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;
+}

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 <glog/logging.h>
+
+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;
+}

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<String> 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
+        )
+    );
+  }
+
+}

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<String> inferCmd;
 

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");
+  }
+
+}

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 {