Translate C++ exceptions

Reviewed By: akotulski

Differential Revision: D3005619

fb-gh-sync-id: a64790b
shipit-source-id: a64790b

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, _) ->

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;
+  }
+}

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 ;
+}

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<String> 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
+        )
+    );
+  }
+}

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");
+  }
+
+}