Implement exception catching

regression/cbmc-java/exceptions22/test.desc

@@ -0,0 +1,11 @@
+CORE
+test.class
+
+^EXIT=0$
+^SIGNAL=0$
+VERIFICATION SUCCESSFUL
+--
+^warning: ignoring
+--
+This test checks that a thrown exception is caught, and is not erroneously rethrown
+on function exit such that another surrounding try block can catch it again.

regression/cbmc-java/exceptions22/test.java

@@ -0,0 +1,20 @@
+public class test {
+  public static void main () {
+    try {
+      f();
+    }
+    catch(Exception e) {
+      assert(false); // Should be unreachable
+    }
+  }
+
+  public static void f() {
+    try {
+      throw new Exception();
+    }
+    catch(Exception e) {
+      // Should prevent main's catch handler from being invoked
+    }
+  }
+}
+

regression/cbmc-java/finally1/test.desc

@@ -0,0 +1,9 @@
+CORE
+test.class
+
+^EXIT=10$
+^SIGNAL=0$
+assertion at file test\.java line 7 function java::test\.main:\(\)V bytecode-index 9: FAILURE
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-java/finally1/test.java

@@ -0,0 +1,11 @@
+public class test {
+ public static void main() throws Exception {
+   try {
+     throw new Exception();
+   }
+   finally {
+     assert(false);
+   }
+ }
+}
+

regression/cbmc-java/finally2/test.desc

@@ -0,0 +1,9 @@
+CORE
+test.class
+
+^EXIT=10$
+^SIGNAL=0$
+assertion at file test\.java line 8 function java::test\.main:\(\)V bytecode-index 9: FAILURE
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-java/finally2/test.java

@@ -0,0 +1,12 @@
+public class test {
+ public static void main() throws Exception {
+   try {
+     throw new Exception();
+   }
+   catch(Exception e) { }
+   finally {
+     assert(false);
+   }
+ }
+}
+

regression/cbmc-java/finally3/test.desc

@@ -0,0 +1,10 @@
+CORE
+test.class
+
+^EXIT=10$
+^SIGNAL=0$
+assertion at file test\.java line 7 function java::test\.main:\(\)V bytecode-index 9: SUCCESS
+assertion at file test\.java line 10 function java::test\.main:\(\)V bytecode-index 22: FAILURE
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-java/finally3/test.java

@@ -0,0 +1,14 @@
+public class test {
+ public static void main() throws Exception {
+   try {
+     throw new NullPointerException();
+   }
+   catch(ArithmeticException e) {
+     assert(false);
+   }
+   finally {
+     assert(false);
+   }
+ }
+}
+

regression/cbmc-java/finally4/test.desc

@@ -0,0 +1,9 @@
+CORE
+test.class
+
+^EXIT=10$
+^SIGNAL=0$
+assertion at file test\.java line 11 function java::test\.main:\(\)V bytecode-index 7: FAILURE
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-java/finally4/test.java

@@ -0,0 +1,15 @@
+public class test {
+ public static void main() throws Exception {
+   try {
+     int x = 1;
+     x++;
+   }
+   catch(ArithmeticException e) {
+     assert(false);
+   }
+   finally {
+     assert(false);
+   }
+ }
+}
+

regression/cbmc-java/finally5/test.desc

@@ -0,0 +1,9 @@
+CORE
+test.class
+
+^EXIT=10$
+^SIGNAL=0$
+assertion at file test\.java line 7 function java::test\.main:\(\)V bytecode-index 12: FAILURE
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-java/finally5/test.java

@@ -0,0 +1,15 @@
+public class test {
+ public static void main() throws Exception {
+   try {
+     f();
+   }
+   finally {
+     assert(false);
+   }
+ }
+
+ public static void f() throws Exception {
+   throw new Exception();
+ }
+}
+

regression/cbmc-java/finally6/test.desc

@@ -0,0 +1,9 @@
+CORE
+test.class
+
+^EXIT=10$
+^SIGNAL=0$
+assertion at file test\.java line 8 function java::test\.main:\(\)V bytecode-index 12: FAILURE
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-java/finally6/test.java

@@ -0,0 +1,16 @@
+public class test {
+ public static void main() throws Exception {
+   try {
+     f();
+   }
+   catch(Exception e) { }
+   finally {
+     assert(false);
+   }
+ }
+
+ public static void f() throws Exception {
+   throw new Exception();
+ }
+}
+

regression/cbmc-java/finally7/test.desc

@@ -0,0 +1,10 @@
+CORE
+test.class
+
+^EXIT=10$
+^SIGNAL=0$
+assertion at file test\.java line 7 function java::test\.main:\(\)V bytecode-index 12: SUCCESS
+assertion at file test\.java line 10 function java::test\.main:\(\)V bytecode-index 25: FAILURE
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-java/finally7/test.java

@@ -0,0 +1,18 @@
+public class test {
+ public static void main() throws Exception {
+   try {
+     f();
+   }
+   catch(ArithmeticException e) {
+     assert(false);
+   }
+   finally {
+     assert(false);
+   }
+ }
+
+ public static void f() throws NullPointerException {
+   throw new NullPointerException();
+ }
+}
+

src/cbmc/cbmc_parse_options.cpp

@@ -815,7 +815,7 @@ bool cbmc_parse_optionst::process_goto_program(
       cmdline.isset("pointer-check"));
     // Java virtual functions -> explicit dispatch tables:
     remove_virtual_functions(symbol_table, goto_functions);
-    // remove catch and throw
+    // remove catch and throw (introduces instanceof)
     remove_exceptions(symbol_table, goto_functions);
     // Similar removal of RTTI inspection:
     remove_instanceof(symbol_table, goto_functions);

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -356,6 +356,7 @@ bool goto_analyzer_parse_optionst::process_goto_program(
     // Java virtual functions -> explicit dispatch tables:
     remove_virtual_functions(goto_model);
     // remove Java throw and catch
+    // This introduces instanceof, so order is important:
     remove_exceptions(goto_model);
     // remove rtti
     remove_instanceof(goto_model);

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -806,6 +806,7 @@ void goto_instrument_parse_optionst::do_indirect_call_and_rtti_removal(
   status() << "Virtual function removal" << eom;
   remove_virtual_functions(symbol_table, goto_functions);
   status() << "Catch and throw removal" << eom;
+  // This introduces instanceof, so order is important:
   remove_exceptions(symbol_table, goto_functions);
   status() << "Java instanceof removal" << eom;
   remove_instanceof(symbol_table, goto_functions);

src/goto-programs/goto_convert.cpp

@@ -58,31 +58,24 @@ static void finish_catch_push_targets(goto_programt &dest)
   // in the second pass set the targets
   Forall_goto_program_instructions(it, dest)
   {
-    if(it->is_catch())
+    if(it->is_catch() && it->code.get_statement()==ID_push_catch)
     {
-      bool handler_added=true;
-      irept exceptions=it->code.find(ID_exception_list);
+      // Populate `targets` with a GOTO instruction target per
+      // exception handler if it isn't already populated.
+      // (Java handlers, for example, need this finish step; C++
+      //  handlers will already be populated by now)
 
-      if(exceptions.is_nil() &&
-         it->code.has_operands())
-        exceptions=it->code.op0().find(ID_exception_list);
-
-      const irept::subt &exception_list=exceptions.get_sub();
-
-      if(!exception_list.empty())
+      if(it->targets.empty())
       {
-        // in this case we have a CATCH_PUSH
-        irept handlers=it->code.find(ID_label);
-        if(handlers.is_nil() &&
-           it->code.has_operands())
-          handlers=it->code.op0().find(ID_label);
-        const irept::subt &handler_list=handlers.get_sub();
-
-        // some handlers may not have been converted (if there was no
-        // exception to be caught); in such a situation we abort
+        bool handler_added=true;
+        const code_push_catcht::exception_listt &handler_list=
+          to_code_push_catch(it->code).exception_list();
+
         for(const auto &handler : handler_list)
         {
-          if(label_targets.find(handler.id())==label_targets.end())
+          // some handlers may not have been converted (if there was no
+          // exception to be caught); in such a situation we abort
+          if(label_targets.find(handler.get_label())==label_targets.end())
           {
             handler_added=false;
             break;
@@ -93,14 +86,7 @@ static void finish_catch_push_targets(goto_programt &dest)
           continue;
 
         for(const auto &handler : handler_list)
-        {
-          std::map<irep_idt,
-                   goto_programt::targett>::const_iterator handler_it=
-            label_targets.find(handler.id());
-          assert(handler_it!=label_targets.end());
-          // set the target
-          it->targets.push_back(handler_it->second);
-        }
+          it->targets.push_back(label_targets.at(handler.get_label()));
       }
     }
   }
@@ -566,6 +552,10 @@ void goto_convertt::convert(
     forall_operands(it, code)
       convert(to_code(*it), dest);
   }
+  else if(statement==ID_push_catch ||
+          statement==ID_pop_catch ||
+          statement==ID_exception_landingpad)
+    copy(code, CATCH, dest);
   else
     copy(code, OTHER, dest);
 

src/goto-programs/goto_convert_class.h

@@ -97,9 +97,6 @@ class goto_convertt:public messaget
     side_effect_exprt &expr,
     goto_programt &dest,
     bool result_is_used);
-  void remove_push_catch(
-    side_effect_exprt &expr,
-    goto_programt &dest);
   void remove_assignment(
     side_effect_exprt &expr,
     goto_programt &dest,
@@ -243,7 +240,6 @@ class goto_convertt:public messaget
   void convert_msc_try_except(const codet &code, goto_programt &dest);
   void convert_msc_leave(const codet &code, goto_programt &dest);
   void convert_try_catch(const codet &code, goto_programt &dest);
-  void convert_java_try_catch(const codet &code, goto_programt &dest);
   void convert_CPROVER_try_catch(const codet &code, goto_programt &dest);
   void convert_CPROVER_try_finally(const codet &code, goto_programt &dest);
   void convert_CPROVER_throw(const codet &code, goto_programt &dest);