From 52e037f77c89ffdcb6c3a98d71c433820b1b34f5 Mon Sep 17 00:00:00 2001 From: Dulma Churchill Date: Thu, 23 Jun 2016 10:10:04 -0700 Subject: [PATCH] Translate AttributedStmt and Fallthrough attribute Reviewed By: akotulski Differential Revision: D3469616 fbshipit-source-id: fe18937 --- infer/src/clang/cTrans.ml | 11 +++ .../frontend/attributes/clang_fallthrough.cpp | 27 ++++++ .../attributes/clang_fallthrough.cpp.dot | 84 +++++++++++++++++++ infer/tests/endtoend/cpp/FallthroughTest.java | 62 ++++++++++++++ infer/tests/frontend/cpp/AttributesTest.java | 38 +++++++++ 5 files changed, 222 insertions(+) create mode 100644 infer/tests/codetoanalyze/cpp/frontend/attributes/clang_fallthrough.cpp create mode 100644 infer/tests/codetoanalyze/cpp/frontend/attributes/clang_fallthrough.cpp.dot create mode 100644 infer/tests/endtoend/cpp/FallthroughTest.java create mode 100644 infer/tests/frontend/cpp/AttributesTest.java diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml index 76a65ad9e..7029844e7 100644 --- a/infer/src/clang/cTrans.ml +++ b/infer/src/clang/cTrans.ml @@ -2293,6 +2293,14 @@ struct conditionalOperator_trans trans_state stmt_info stmt_list' expr_info | _ -> binaryOperator_trans trans_state binary_operator_info stmt_info expr_info stmt_list + and attributedStmt_trans trans_state stmts attrs = + let open Clang_ast_t in + match stmts, attrs with + | [stmt], [attr] -> + (match stmt, attr with + | NullStmt _, FallThroughAttr _ -> nullStmt_trans trans_state.succ_nodes + | _ -> assert false) (* More cases to come. With the assert false we can find them *) + | _ -> assert false (* Expect that this doesn't happen *) (* Translates a clang instruction into SIL instructions. It takes a *) (* a trans_state containing current info on the translation and it returns *) @@ -2574,6 +2582,9 @@ struct let trans_state' = { trans_state with priority = Free } in lambdaExpr_trans trans_state' expr_info decl + | AttributedStmt (_, stmts, attrs) -> + attributedStmt_trans trans_state stmts attrs + | s -> (Printing.log_stats "\n!!!!WARNING: found statement %s. \nACTION REQUIRED: \ Translation need to be defined. Statement ignored.... \n" diff --git a/infer/tests/codetoanalyze/cpp/frontend/attributes/clang_fallthrough.cpp b/infer/tests/codetoanalyze/cpp/frontend/attributes/clang_fallthrough.cpp new file mode 100644 index 000000000..a92ba5b36 --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/frontend/attributes/clang_fallthrough.cpp @@ -0,0 +1,27 @@ +/* + * 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. + */ + +int h() { return 3; } + +int switch_with_fallthrough(int n) { + int res = 5; + switch (n) { + case 22: + case 33: + [[clang::fallthrough]]; + case 66: + [[clang::fallthrough]]; + case 77: + res = h(); + break; + } + return res; +} + +int test_fallthrough() { return 1 / (switch_with_fallthrough(66) - 3); } diff --git a/infer/tests/codetoanalyze/cpp/frontend/attributes/clang_fallthrough.cpp.dot b/infer/tests/codetoanalyze/cpp/frontend/attributes/clang_fallthrough.cpp.dot new file mode 100644 index 000000000..a9661a909 --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/frontend/attributes/clang_fallthrough.cpp.dot @@ -0,0 +1,84 @@ +/* @generated */ +digraph iCFG { +20 [label="20: Return Stmt \n n$0=_fun_switch_with_fallthrough(66:int ) [line 27]\n *&return:int =(1 / (n$0 - 3)) [line 27]\n " shape="box"] + + + 20 -> 19 ; +19 [label="19: Exit test_fallthrough \n " color=yellow style=filled] + + +18 [label="18: Start test_fallthrough\nFormals: \nLocals: \n DECLARE_LOCALS(&return); [line 27]\n " color=yellow style=filled] + + + 18 -> 20 ; +17 [label="17: DeclStmt \n *&res:int =5 [line 13]\n " shape="box"] + + + 17 -> 7 ; +16 [label="16: Prune (false branch) \n PRUNE(((n$1 == 22) == 0), false); [line 15]\n " shape="invhouse"] + + + 16 -> 13 ; + 16 -> 14 ; +15 [label="15: Prune (true branch) \n PRUNE(((n$1 == 22) != 0), true); [line 15]\n " shape="invhouse"] + + + 15 -> 8 ; +14 [label="14: Prune (false branch) \n PRUNE(((n$1 == 33) == 0), false); [line 16]\n " shape="invhouse"] + + + 14 -> 11 ; + 14 -> 12 ; +13 [label="13: Prune (true branch) \n PRUNE(((n$1 == 33) != 0), true); [line 16]\n " shape="invhouse"] + + + 13 -> 8 ; +12 [label="12: Prune (false branch) \n PRUNE(((n$1 == 66) == 0), false); [line 18]\n " shape="invhouse"] + + + 12 -> 9 ; + 12 -> 10 ; +11 [label="11: Prune (true branch) \n PRUNE(((n$1 == 66) != 0), true); [line 18]\n " shape="invhouse"] + + + 11 -> 8 ; +10 [label="10: Prune (false branch) \n PRUNE(((n$1 == 77) == 0), false); [line 20]\n " shape="invhouse"] + + + 10 -> 6 ; +9 [label="9: Prune (true branch) \n PRUNE(((n$1 == 77) != 0), true); [line 20]\n " shape="invhouse"] + + + 9 -> 8 ; +8 [label="8: BinaryOperatorStmt: Assign \n n$2=_fun_h() [line 21]\n *&res:int =n$2 [line 21]\n " shape="box"] + + + 8 -> 6 ; +7 [label="7: Switch_stmt \n n$1=*&n:int [line 14]\n " shape="box"] + + + 7 -> 15 ; + 7 -> 16 ; +6 [label="6: Return Stmt \n n$0=*&res:int [line 24]\n *&return:int =n$0 [line 24]\n " shape="box"] + + + 6 -> 5 ; +5 [label="5: Exit switch_with_fallthrough \n " color=yellow style=filled] + + +4 [label="4: Start switch_with_fallthrough\nFormals: n:int \nLocals: res:int \n DECLARE_LOCALS(&return,&res); [line 12]\n " color=yellow style=filled] + + + 4 -> 17 ; +3 [label="3: Return Stmt \n *&return:int =3 [line 10]\n " shape="box"] + + + 3 -> 2 ; +2 [label="2: Exit h \n " color=yellow style=filled] + + +1 [label="1: Start h\nFormals: \nLocals: \n DECLARE_LOCALS(&return); [line 10]\n " color=yellow style=filled] + + + 1 -> 3 ; +} diff --git a/infer/tests/endtoend/cpp/FallthroughTest.java b/infer/tests/endtoend/cpp/FallthroughTest.java new file mode 100644 index 000000000..63447dd63 --- /dev/null +++ b/infer/tests/endtoend/cpp/FallthroughTest.java @@ -0,0 +1,62 @@ +/* + * 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.cpp; + +import static org.hamcrest.MatcherAssert.assertThat; +import static utils.matchers.ResultContainsExactly.containsExactly; + +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 FallthroughTest { + + public static final String SOURCE_FILE = + "infer/tests/codetoanalyze/cpp/frontend/attributes/clang_fallthrough.cpp"; + + public static final String DIVIDE_BY_ZERO = "DIVIDE_BY_ZERO"; + private static ImmutableList inferCmd; + + @ClassRule + public static DebuggableTemporaryFolder folder = + new DebuggableTemporaryFolder(); + + @BeforeClass + public static void runInfer() throws InterruptedException, IOException { + inferCmd = InferRunner.createCPPInferCommand(folder, SOURCE_FILE); + } + + @Test + public void whenInferRunsOnDivideByZeroThenDivideByZeroIsFound() + throws InterruptedException, IOException, InferException { + InferResults inferResults = InferRunner.runInferC(inferCmd); + String[] procedures = {"test_fallthrough"}; + assertThat( + "Results should contain divide by zero error", + inferResults, + containsExactly( + DIVIDE_BY_ZERO, + SOURCE_FILE, + procedures + ) + ); + } + + +} diff --git a/infer/tests/frontend/cpp/AttributesTest.java b/infer/tests/frontend/cpp/AttributesTest.java new file mode 100644 index 000000000..4cc63f1c4 --- /dev/null +++ b/infer/tests/frontend/cpp/AttributesTest.java @@ -0,0 +1,38 @@ +/* + * Copyright (c) 2015 - 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.cpp; + +import org.junit.Rule; +import org.junit.Test; + +import java.io.IOException; + +import utils.DebuggableTemporaryFolder; +import utils.InferException; +import utils.ClangFrontendUtils; + +public class AttributesTest { + + String basePath = "infer/tests/codetoanalyze/cpp/frontend/attributes/"; + + @Rule + public DebuggableTemporaryFolder folder = new DebuggableTemporaryFolder(); + + void frontendTest(String fileRelative) throws InterruptedException, IOException, InferException { + ClangFrontendUtils.createAndCompareCppDotFiles(folder, basePath + fileRelative); + } + + @Test + public void testClangFallthroughDotFilesMatch() + throws InterruptedException, IOException, InferException { + frontendTest("clang_fallthrough.cpp"); + } + +}