Fixing shortcircuit in binary operator.

Reviewed By: dulmarod

Differential Revision: D3340811

fbshipit-source-id: 70fbbcf

infer/src/clang/ast_expressions.mli

@@ -45,6 +45,8 @@ val create_struct_type : string -> type_ptr
 
 val create_pointer_type : type_ptr -> type_ptr
 
+val create_integer_literal : string -> stmt
+
 val create_reference_type : type_ptr -> type_ptr
 
 val make_objc_ivar_decl : decl_info -> type_ptr -> named_decl_info -> decl

infer/src/clang/cTrans.ml

@@ -747,7 +747,7 @@ struct
     let sil_loc = CLocation.get_sil_location stmt_info context in
     let typ =
       CTypes_decl.type_ptr_to_sil_type context.CContext.tenv expr_info.Clang_ast_t.ei_type_ptr in
-    (match stmt_list with
+    match stmt_list with
     | [s1; s2] -> (* Assumption: We expect precisely 2 stmt corresponding to the 2 operands*)
         let rhs_owning_method = CTrans_utils.is_owning_method s2 in
         (* NOTE: we create a node only if required. In that case this node *)
@@ -797,7 +797,7 @@ struct
         let res_trans_to_parent = PriorityNode.compute_results_to_parent trans_state_pri sil_loc
             nname stmt_info all_res_trans in
         { res_trans_to_parent with exps = exp_to_parent }
-     | _ -> assert false) (* Binary operator should have two operands *)
+    | _ -> assert false (* Binary operator should have two operands *)
 
   and callExpr_trans trans_state si stmt_list expr_info =
     let context = trans_state.context in
@@ -1140,6 +1140,7 @@ struct
          }
      | _ -> assert false)
 
+  (* The GNU extension to the conditional operator which allows the middle operand to be omitted. *)
   and binaryConditionalOperator_trans trans_state stmt_info stmt_list expr_info =
     match stmt_list with
     | [stmt1; ostmt1; ostmt2; stmt2]
@@ -1240,7 +1241,7 @@ struct
         instrs = res_trans_s1.instrs@res_trans_s2.instrs;
         exps = [(e_cond, typ1)];
       } in
-    Printing.log_out "Translating Condition for Conditional/Loop \n";
+    Printing.log_out "Translating Condition for If-then-else/Loop/Conditional Operator \n";
     let open Clang_ast_t in
     match cond with
     | BinaryOperator(_, [s1; s2], _, boi) ->
@@ -2286,6 +2287,20 @@ struct
     let trans_state' = { trans_state with obj_bridged_cast_typ = Some typ } in
     instruction trans_state' stmt
 
+  and binaryOperator_trans_shortc trans_state stmt_info stmt_list expr_info binary_operator_info =
+    let open Clang_ast_t in
+    match binary_operator_info.boi_kind with
+    | `LAnd | `LOr  ->
+        (* For LAnd/LOr we compiles a binary expression bo into an semantic equivalent
+           conditional operator 'bo ? 1:0'.
+           The conditional operator takes care of shortcircuit when/where needed *)
+        let bo = BinaryOperator (stmt_info, stmt_list, expr_info, binary_operator_info) in
+        let stmt_list' =
+          [bo; Ast_expressions.create_integer_literal "1"; Ast_expressions.create_integer_literal "0"] in
+        conditionalOperator_trans trans_state stmt_info stmt_list' expr_info
+    | _  -> binaryOperator_trans trans_state binary_operator_info stmt_info expr_info stmt_list
+
+
   (* Translates a clang instruction into SIL instructions. It takes a       *)
   (* a trans_state containing current info on the translation and it returns *)
   (* a result_state.*)
@@ -2307,8 +2322,8 @@ struct
     | ArraySubscriptExpr(_, stmt_list, expr_info) ->
         arraySubscriptExpr_trans trans_state expr_info stmt_list
 
-    | BinaryOperator(stmt_info, stmt_list, expr_info, binary_operator_info) ->
-        binaryOperator_trans trans_state binary_operator_info stmt_info expr_info stmt_list
+    | BinaryOperator (stmt_info, stmt_list, expr_info, binary_operator_info) ->
+        binaryOperator_trans_shortc trans_state stmt_info stmt_list expr_info binary_operator_info
 
     | CallExpr(stmt_info, stmt_list, ei) ->
         (match is_dispatch_function stmt_list with
@@ -2373,7 +2388,7 @@ struct
     | NullStmt _ ->
         nullStmt_trans trans_state.succ_nodes
 
-    | CompoundAssignOperator(stmt_info, stmt_list, expr_info, binary_operator_info, _) ->
+    | CompoundAssignOperator (stmt_info, stmt_list, expr_info, binary_operator_info, _) ->
         binaryOperator_trans trans_state binary_operator_info stmt_info expr_info stmt_list
 
     | DeclStmt(stmt_info, _, decl_list) ->

infer/tests/codetoanalyze/c/errors/local_vars/local_vars.c

@@ -7,7 +7,7 @@
  * of patent rights can be found in the PATENTS file in the same directory.
  */
 
-int m(int z) {
+int m1(int z) {
   int y = 0;
   int x = 5;
   if (z < 10) {
@@ -15,6 +15,20 @@ int m(int z) {
     if (x == 7)
       return x / y;
   }
+  if (x == 6)
+    return x / y;
+  else
+    return 0;
+}
+
+int m2(int z) {
+    int y = 0;
+    int x = 5;
+    if (z < 10) {
+        int x = 7;
+        if (x == 6)
+            return x / y;
+    }
     if (x == 5)
         return x / y;
     else

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

@@ -0,0 +1,65 @@
+/*
+ * 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.
+ */
+
+struct data {
+  int flag;
+};
+
+static struct data d;
+
+int f(int x) {
+  struct data* p = x ? &d : 0;
+  return (p && p->flag);
+}
+
+int f_error(int x) {
+  struct data* p = x ? &d : 0;
+  return p->flag && p; // NULL_DEREF
+}
+
+int g(int x) {
+  struct data* p = x ? &d : 0;
+  return !(p && p->flag); // OK
+}
+
+int h(int x) {
+  struct data* p = x ? &d : 0;
+  return !(p && p->flag); // OK
+}
+
+int g_error(int x) {
+  struct data* p = x ? &d : 0;
+  return !(p->flag && p); // NULL_DEREF
+}
+
+int k(int x) {
+  struct data* p = x ? &d : 0;
+  return !(p && p->flag); // OK
+}
+
+int l(int x) {
+  struct data* p = x ? &d : 0;
+  return !p || p->flag; // OK
+}
+
+int l_error(int x) {
+  struct data* p = x ? &d : 0;
+  return p || p->flag; // NULL_DEREF
+}
+
+int m(int x) {
+  struct data* p = x ? &d : 0;
+  return (!p || p->flag) && !(p && p->flag);
+  ; // OK
+}
+
+int n(int x) {
+  struct data* p = x ? &d : 0;
+  return p && (p->flag || !(p->flag)); // OK
+}

infer/tests/endtoend/c/LocalVarsTest.java

@@ -10,8 +10,7 @@
 package endtoend.c;
 
 import static org.hamcrest.MatcherAssert.assertThat;
-import static utils.matchers.ResultContainsErrorInMethod.contains;
-import static utils.matchers.ResultContainsOnlyTheseErrors.containsOnly;
+import static utils.matchers.ResultContainsExactly.containsExactly;
 
 import org.junit.BeforeClass;
 import org.junit.Test;
@@ -36,55 +35,12 @@ public class LocalVarsTest {
   }
 
   @Test
-  public void whenInferRunsOnLocal_vars_mThenDivideByZeroIsFound()
+  public void whenInferRunsOnLocalVarsThenOnlyTheExpectedErrorsAreFound()
       throws InterruptedException, IOException, InferException {
-    assertThat(
-        "Results should contain divide by zero error",
-        inferResults,
-        contains(
-            DIVIDE_BY_ZERO,
-            local_vars_file,
-            "m"
-        )
-    );
-  }
-
-  @Test
-  public void whenInferRunsOnLocal_vars_mmThenDivideByZeroIsFound()
-      throws InterruptedException, IOException, InferException {
-    assertThat(
-        "Results should contain divide by zero error",
-        inferResults,
-        contains(
-            DIVIDE_BY_ZERO,
-            local_vars_file,
-            "mm"
-        )
-    );
-  }
-
-  @Test
-  public void whenInferRunsOnLocal_vars_tThenDivideByZeroIsFound()
-      throws InterruptedException, IOException, InferException {
-    assertThat(
-        "Results should contain divide by zero error",
-        inferResults,
-        contains(
-            DIVIDE_BY_ZERO,
-            local_vars_file,
-            "t"
-        )
-    );
-  }
-
-
-  @Test
-  public void whenInferRunsOnNullPointerDereferenceThenOnlyTheExpectedErrorsAreFound()
-      throws InterruptedException, IOException, InferException {
-    String[] expectedProcedures = {"m", "mm", "t"};
+    String[] expectedProcedures = {"m1", "m2", "mm", "t"};
     assertThat(
         "No unexpected errors should be found", inferResults,
-        containsOnly(
+        containsExactly(
             DIVIDE_BY_ZERO,
             local_vars_file,
             expectedProcedures));

infer/tests/endtoend/c/NullDereferenceShortCircuitTest.java

@@ -0,0 +1,58 @@
+/*
+ * 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 org.junit.BeforeClass;
+import org.junit.Test;
+
+import java.io.IOException;
+
+import utils.InferException;
+import utils.InferResults;
+
+public class NullDereferenceShortCircuitTest {
+
+  public static final String SOURCE_FILE =
+      "null_dereference/short.c";
+
+
+  public static final String NULL_DEREFERENCE = "NULL_DEREFERENCE";
+
+  private static InferResults inferResults;
+
+  @BeforeClass
+  public static void runInfer() throws InterruptedException, IOException {
+    inferResults = InferResults.loadCInferResults(
+        NullDereferenceShortCircuitTest.class,
+        SOURCE_FILE);
+  }
+
+  @Test
+  public void nullDereferenceTest() throws InterruptedException, IOException, InferException {
+    String[] procedures = {
+        "f_error",
+        "g_error",
+        "l_error"
+    };
+    System.out.println(inferResults.toString());
+    assertThat(
+        "Results should contain null pointer dereference error",
+        inferResults,
+        containsExactly(
+            NULL_DEREFERENCE,
+            SOURCE_FILE,
+            procedures
+        )
+    );
+  }
+}