From d499d5fc8ea5ca63457cc419a05b8a5c5f89a171 Mon Sep 17 00:00:00 2001 From: Dulma Rodriguez Date: Thu, 3 Mar 2016 09:03:51 -0800 Subject: [PATCH] Translate C++ exceptions Reviewed By: akotulski Differential Revision: D3005619 fb-gh-sync-id: a64790b shipit-source-id: a64790b --- infer/src/clang/cTrans.ml | 13 +++- .../cpp/frontend/exceptions/Exceptions.cpp | 32 +++++++++ .../frontend/exceptions/Exceptions.cpp.dot | 67 +++++++++++++++++++ infer/tests/endtoend/cpp/ExceptionsTest.java | 61 +++++++++++++++++ infer/tests/frontend/cpp/ExceptionsTest.java | 38 +++++++++++ 5 files changed, 210 insertions(+), 1 deletion(-) create mode 100644 infer/tests/codetoanalyze/cpp/frontend/exceptions/Exceptions.cpp create mode 100644 infer/tests/codetoanalyze/cpp/frontend/exceptions/Exceptions.cpp.dot create mode 100644 infer/tests/endtoend/cpp/ExceptionsTest.java create mode 100644 infer/tests/frontend/cpp/ExceptionsTest.java diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml index 930159988..cff0e889a 100644 --- a/infer/src/clang/cTrans.ml +++ b/infer/src/clang/cTrans.ml @@ -2247,14 +2247,25 @@ struct | ObjCAtTryStmt (_, stmts) -> compoundStmt_trans trans_state stmts + | CXXTryStmt (_, stmts) -> + (Printing.log_stats + "\n!!!!WARNING: found statement %s. \nTranslation need to be improved.... \n" + (Ast_utils.string_of_stmt instr); + compoundStmt_trans trans_state stmts) | ObjCAtThrowStmt (stmt_info, stmts) -> returnStmt_trans trans_state stmt_info stmts + | CXXThrowExpr (stmt_info, stmts, _) -> + (Printing.log_stats + "\n!!!!WARNING: found statement %s. \nTranslation need to be improved.... \n" + (Ast_utils.string_of_stmt instr); + returnStmt_trans trans_state stmt_info stmts) | ObjCAtFinallyStmt (_, stmts) -> compoundStmt_trans trans_state stmts - | ObjCAtCatchStmt _ -> + | ObjCAtCatchStmt _ + | CXXCatchStmt _ -> compoundStmt_trans trans_state [] | PredefinedExpr (_, _, expr_info, _) -> diff --git a/infer/tests/codetoanalyze/cpp/frontend/exceptions/Exceptions.cpp b/infer/tests/codetoanalyze/cpp/frontend/exceptions/Exceptions.cpp new file mode 100644 index 000000000..a562dce45 --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/frontend/exceptions/Exceptions.cpp @@ -0,0 +1,32 @@ +/* + * 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 deref(int* p) { + if (p == 0) { + throw "Null pointer!"; + } + return *p; +} + +int deref_null(int* p) { + try { + return *p; + } catch (const char* msg) { + } +} + +int call_deref_with_null() { deref_null(nullptr); } + +int main() { + try { + return deref(0); + } catch (const char* msg) { + return -1; + } +} diff --git a/infer/tests/codetoanalyze/cpp/frontend/exceptions/Exceptions.cpp.dot b/infer/tests/codetoanalyze/cpp/frontend/exceptions/Exceptions.cpp.dot new file mode 100644 index 000000000..b651d2350 --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/frontend/exceptions/Exceptions.cpp.dot @@ -0,0 +1,67 @@ +digraph iCFG { +17 [label="17: Return Stmt \n n$0=_fun_deref(0:int *) [line 28]\n *&return:int =n$0 [line 28]\n REMOVE_TEMPS(n$0); [line 28]\n APPLY_ABSTRACTION; [line 28]\n " shape="box"] + + + 17 -> 16 ; +16 [label="16: Exit main \n " color=yellow style=filled] + + +15 [label="15: Start main\nFormals: \nLocals: \n DECLARE_LOCALS(&return); [line 26]\n " color=yellow style=filled] + + + 15 -> 17 ; +14 [label="14: Call _fun_deref_null \n n$0=_fun_deref_null(null:int *) [line 24]\n REMOVE_TEMPS(n$0); [line 24]\n APPLY_ABSTRACTION; [line 24]\n " shape="box"] + + + 14 -> 13 ; +13 [label="13: Exit call_deref_with_null \n " color=yellow style=filled] + + +12 [label="12: Start call_deref_with_null\nFormals: \nLocals: \n DECLARE_LOCALS(&return); [line 24]\n " color=yellow style=filled] + + + 12 -> 14 ; +11 [label="11: Return Stmt \n n$0=*&p:int * [line 19]\n n$1=*n$0:int [line 19]\n *&return:int =n$1 [line 19]\n REMOVE_TEMPS(n$0,n$1); [line 19]\n NULLIFY(&p,false); [line 19]\n APPLY_ABSTRACTION; [line 19]\n " shape="box"] + + + 11 -> 10 ; +10 [label="10: Exit deref_null \n " color=yellow style=filled] + + +9 [label="9: Start deref_null\nFormals: p:int *\nLocals: \n DECLARE_LOCALS(&return); [line 17]\n " color=yellow style=filled] + + + 9 -> 11 ; +8 [label="8: Return Stmt \n NULLIFY(&p,false); [line 12]\n *&return:int =\"Null pointer!\" [line 12]\n APPLY_ABSTRACTION; [line 12]\n " shape="box"] + + + 8 -> 2 ; +7 [label="7: Prune (false branch) \n PRUNE(((n$2 == 0) == 0), false); [line 11]\n REMOVE_TEMPS(n$2); [line 11]\n " shape="invhouse"] + + + 7 -> 4 ; +6 [label="6: Prune (true branch) \n PRUNE(((n$2 == 0) != 0), true); [line 11]\n REMOVE_TEMPS(n$2); [line 11]\n " shape="invhouse"] + + + 6 -> 8 ; +5 [label="5: BinaryOperatorStmt: EQ \n n$2=*&p:int * [line 11]\n " shape="box"] + + + 5 -> 6 ; + 5 -> 7 ; +4 [label="4: + \n " ] + + + 4 -> 3 ; +3 [label="3: Return Stmt \n n$0=*&p:int * [line 14]\n n$1=*n$0:int [line 14]\n *&return:int =n$1 [line 14]\n REMOVE_TEMPS(n$0,n$1); [line 14]\n NULLIFY(&p,false); [line 14]\n APPLY_ABSTRACTION; [line 14]\n " shape="box"] + + + 3 -> 2 ; +2 [label="2: Exit deref \n " color=yellow style=filled] + + +1 [label="1: Start deref\nFormals: p:int *\nLocals: \n DECLARE_LOCALS(&return); [line 10]\n " color=yellow style=filled] + + + 1 -> 5 ; +} diff --git a/infer/tests/endtoend/cpp/ExceptionsTest.java b/infer/tests/endtoend/cpp/ExceptionsTest.java new file mode 100644 index 000000000..03d09b0dd --- /dev/null +++ b/infer/tests/endtoend/cpp/ExceptionsTest.java @@ -0,0 +1,61 @@ +/* + * 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 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 ExceptionsTest { + + public static final String FILE = + "infer/tests/codetoanalyze/cpp/frontend/exceptions/Exceptions.cpp"; + + private static ImmutableList inferCmd; + + public static final String NULL_DEREFERENCE = "NULL_DEREFERENCE"; + + @ClassRule + public static DebuggableTemporaryFolder folder = new DebuggableTemporaryFolder(); + + @BeforeClass + public static void runInfer() throws InterruptedException, IOException { + inferCmd = InferRunner.createCPPInferCommand(folder, FILE); + } + + @Test + public void whenInferRunsOnDiv0FunctionsErrorIsFound() + throws InterruptedException, IOException, InferException { + String[] procedures = { "call_deref_with_null" }; + InferResults inferResults = InferRunner.runInferCPP(inferCmd); + assertThat( + "Results should not contain " + NULL_DEREFERENCE, + inferResults, + containsExactly( + NULL_DEREFERENCE, + FILE, + procedures + ) + ); + } +} diff --git a/infer/tests/frontend/cpp/ExceptionsTest.java b/infer/tests/frontend/cpp/ExceptionsTest.java new file mode 100644 index 000000000..c9093c5c1 --- /dev/null +++ b/infer/tests/frontend/cpp/ExceptionsTest.java @@ -0,0 +1,38 @@ +/* + * 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.cpp; + +import org.junit.Rule; +import org.junit.Test; + +import java.io.IOException; + +import utils.DebuggableTemporaryFolder; +import utils.InferException; +import utils.ClangFrontendUtils; + +public class ExceptionsTest { + + String basePath = "infer/tests/codetoanalyze/cpp/frontend/exceptions/"; + + @Rule + public DebuggableTemporaryFolder folder = new DebuggableTemporaryFolder(); + + void frontendTest(String fileRelative) throws InterruptedException, IOException, InferException { + ClangFrontendUtils.createAndCompareCppDotFiles(folder, basePath + fileRelative); + } + + @Test + public void testSimpleDeclDotFilesMatch() + throws InterruptedException, IOException, InferException { + frontendTest("Exceptions.cpp"); + } + +}