Translate OffsetOfExpr

Summary:
Translate `OffsetOfExpr` (http://clang.llvm.org/doxygen/classclang_1_1OffsetOfExpr.html) into
an expression that has an undefined value.

Reviewed By: dulmarod

Differential Revision: D3534392

fbshipit-source-id: be3dd6a

infer/src/clang/cTrans.ml

@@ -2312,6 +2312,11 @@ struct
          | _ -> assert false) (* More cases to come. With the assert false we can find them *)
     | _ -> assert false (* Expect that this doesn't happen *)
 
+  and offsetOfExpr_trans trans_state expr_info =
+    let tenv = trans_state.context.CContext.tenv in
+    let typ = CTypes_decl.get_type_from_expr_info expr_info tenv in
+    { empty_res_trans with exps = [CTrans_utils.undefined_expression (), typ] }
+
   (* 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.*)
@@ -2600,6 +2605,9 @@ struct
     | CXXNoexceptExpr (_, _, expr_info, cxx_noexcept_expr_info) ->
         booleanValue_trans trans_state expr_info cxx_noexcept_expr_info.Clang_ast_t.xnee_value
 
+    | OffsetOfExpr (_, _, expr_info) ->
+        offsetOfExpr_trans trans_state expr_info
+
     | s -> (Printing.log_stats
               "\n!!!!WARNING: found statement %s. \nACTION REQUIRED: \
                Translation need to be defined. Statement ignored.... \n"

infer/src/clang/cTrans_utils.ml

@@ -155,6 +155,8 @@ let empty_res_trans = {
   is_cpp_call_virtual = false;
 }
 
+let undefined_expression () = Sil.Var (Ident.create_fresh Ident.knormal)
+
 (** Collect the results of translating a list of instructions, and link up the nodes created. *)
 let collect_res_trans cfg l =
   let rec collect l rt =

infer/src/clang/cTrans_utils.mli

@@ -42,6 +42,8 @@ type trans_result = {
 
 val empty_res_trans: trans_result
 
+val undefined_expression: unit -> Sil.exp
+
 val collect_res_trans : Cfg.cfg -> trans_result list -> trans_result
 
 val extract_var_exp_or_fail : trans_state -> Sil.exp * Typ.t

infer/tests/codetoanalyze/c/frontend/offsetof_expr/offsetof_expr.c

@@ -0,0 +1,25 @@
+/*
+ * 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 <stddef.h>
+
+struct address {
+  char v1[2];
+  char v2[5];
+  int v3;
+};
+
+int test() {
+  int i = offsetof(struct address, v2);
+  if (i == 9) {
+    return 9 / 0;
+  } else {
+    return 4 / 0;
+  }
+}

infer/tests/codetoanalyze/c/frontend/offsetof_expr/offsetof_expr.c.dot

@@ -0,0 +1,43 @@
+/* @generated */
+digraph iCFG {
+10 [label="10:  DeclStmt \n   *&i:int =n$1 [line 19]\n " shape="box"]
+	
+
+	 10 -> 5 ;
+9 [label="9:  Return Stmt \n   *&return:int =(4 / 0) [line 23]\n " shape="box"]
+	
+
+	 9 -> 2 ;
+8 [label="8:  Return Stmt \n   *&return:int =(9 / 0) [line 21]\n " shape="box"]
+	
+
+	 8 -> 2 ;
+7 [label="7: Prune (false branch) \n   PRUNE(((n$0 == 9) == 0), false); [line 20]\n " shape="invhouse"]
+	
+
+	 7 -> 9 ;
+6 [label="6: Prune (true branch) \n   PRUNE(((n$0 == 9) != 0), true); [line 20]\n " shape="invhouse"]
+	
+
+	 6 -> 8 ;
+5 [label="5:  BinaryOperatorStmt: EQ \n   n$0=*&i:int  [line 20]\n " shape="box"]
+	
+
+	 5 -> 6 ;
+	 5 -> 7 ;
+4 [label="4:  between_join_and_exit \n  " shape="box"]
+	
+
+	 4 -> 2 ;
+3 [label="3: + \n  " ]
+	
+
+	 3 -> 4 ;
+2 [label="2: Exit test \n  " color=yellow style=filled]
+	
+
+1 [label="1: Start test\nFormals: \nLocals:  i:int  \n   DECLARE_LOCALS(&return,&i); [line 18]\n " color=yellow style=filled]
+	
+
+	 1 -> 10 ;
+}

infer/tests/endtoend/c/OffsetOfExprTest.java

@@ -0,0 +1,59 @@
+/*
+ * 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 static org.hamcrest.MatcherAssert.assertThat;
+import static utils.matchers.ResultContainsLineNumbers.containsLines;
+
+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 OffsetOfExprTest {
+
+  public static final String FILE =
+      "infer/tests/codetoanalyze/c/frontend/offsetof_expr/offsetof_expr.c";
+
+  private static ImmutableList<String> inferCmd;
+
+  public static final String DIVIDE_BY_ZERO = "DIVIDE_BY_ZERO";
+
+  @ClassRule
+  public static DebuggableTemporaryFolder folder =
+      new DebuggableTemporaryFolder();
+
+  @BeforeClass
+  public static void runInfer() throws InterruptedException, IOException {
+    inferCmd = InferRunner.createCInferCommand(
+      folder,
+      FILE);
+
+  }
+
+  @Test
+  public void matchErrors()
+      throws InterruptedException, IOException, InferException {
+    InferResults inferResults = InferRunner.runInferObjC(inferCmd);
+    assertThat(
+        "Results should contain the correct " + DIVIDE_BY_ZERO,
+        inferResults,
+        containsLines(new int[] {21, 23}));
+  }
+
+}

infer/tests/frontend/c/OffsetOfExprTest.java

@@ -0,0 +1,31 @@
+/*
+ * 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 frontend.c;
+
+import org.junit.Rule;
+import org.junit.Test;
+
+import java.io.IOException;
+
+import utils.ClangFrontendUtils;
+import utils.DebuggableTemporaryFolder;
+import utils.InferException;
+
+public class OffsetOfExprTest {
+  String FILE = "infer/tests/codetoanalyze/c/frontend/offsetof_expr/offsetof_expr.c";
+
+  @Rule
+  public DebuggableTemporaryFolder folder = new DebuggableTemporaryFolder();
+
+  @Test
+  public void frontendTest() throws InterruptedException, IOException, InferException {
+    ClangFrontendUtils.createAndCompareCDotFiles(folder, FILE);
+  }
+}