From 4ba864780ed21019133b3efdcda24845999fb450 Mon Sep 17 00:00:00 2001 From: Martino Luca Date: Tue, 19 Jul 2016 08:31:08 -0700 Subject: [PATCH] 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 | 8 +++ infer/src/clang/cTrans_utils.ml | 2 + infer/src/clang/cTrans_utils.mli | 2 + .../c/frontend/offsetof_expr/offsetof_expr.c | 25 ++++++++ .../offsetof_expr/offsetof_expr.c.dot | 43 ++++++++++++++ infer/tests/endtoend/c/OffsetOfExprTest.java | 59 +++++++++++++++++++ infer/tests/frontend/c/OffsetOfExprTest.java | 31 ++++++++++ 7 files changed, 170 insertions(+) create mode 100644 infer/tests/codetoanalyze/c/frontend/offsetof_expr/offsetof_expr.c create mode 100644 infer/tests/codetoanalyze/c/frontend/offsetof_expr/offsetof_expr.c.dot create mode 100644 infer/tests/endtoend/c/OffsetOfExprTest.java create mode 100644 infer/tests/frontend/c/OffsetOfExprTest.java diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml index 2c87f54ff..81495fd72 100644 --- a/infer/src/clang/cTrans.ml +++ b/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" diff --git a/infer/src/clang/cTrans_utils.ml b/infer/src/clang/cTrans_utils.ml index 903f027c2..4c7ead58e 100644 --- a/infer/src/clang/cTrans_utils.ml +++ b/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 = diff --git a/infer/src/clang/cTrans_utils.mli b/infer/src/clang/cTrans_utils.mli index 71415324c..0a6539f10 100644 --- a/infer/src/clang/cTrans_utils.mli +++ b/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 diff --git a/infer/tests/codetoanalyze/c/frontend/offsetof_expr/offsetof_expr.c b/infer/tests/codetoanalyze/c/frontend/offsetof_expr/offsetof_expr.c new file mode 100644 index 000000000..6d4b26437 --- /dev/null +++ b/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 + +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; + } +} diff --git a/infer/tests/codetoanalyze/c/frontend/offsetof_expr/offsetof_expr.c.dot b/infer/tests/codetoanalyze/c/frontend/offsetof_expr/offsetof_expr.c.dot new file mode 100644 index 000000000..0241d7949 --- /dev/null +++ b/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 ; +} diff --git a/infer/tests/endtoend/c/OffsetOfExprTest.java b/infer/tests/endtoend/c/OffsetOfExprTest.java new file mode 100644 index 000000000..6450e55f5 --- /dev/null +++ b/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 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})); + } + +} diff --git a/infer/tests/frontend/c/OffsetOfExprTest.java b/infer/tests/frontend/c/OffsetOfExprTest.java new file mode 100644 index 000000000..a95f85022 --- /dev/null +++ b/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); + } +}