Replace direct use of EXC_SUFFIX with a universal catch

Author: smowton

src/java_bytecode/java_entry_point.cpp

@@ -307,11 +307,9 @@ void java_record_outputs(
   codet output(ID_output);
   output.operands().resize(2);
 
-  assert(symbol_table.has_symbol(id2string(function.name)+EXC_SUFFIX));
-
   // retrieve the exception variable
   const symbolt exc_symbol=symbol_table.lookup(
-    id2string(function.name)+EXC_SUFFIX);
+    JAVA_ENTRY_POINT_EXCEPTION_SYMBOL);
 
   output.op0()=address_of_exprt(
     index_exprt(string_constantt(exc_symbol.base_name),
@@ -613,17 +611,19 @@ bool java_entry_point(
     call_main.lhs()=return_symbol.symbol_expr();
   }
 
-  if(!symbol_table.has_symbol(id2string(symbol.name)+EXC_SUFFIX))
-  {
-    // add the exceptional return value
-    auxiliary_symbolt exc_symbol;
-    exc_symbol.mode=ID_java;
-    exc_symbol.is_static_lifetime=true;
-    exc_symbol.name=id2string(symbol.name)+EXC_SUFFIX;
-    exc_symbol.base_name=id2string(symbol.name)+EXC_SUFFIX;
-    exc_symbol.type=java_reference_type(empty_typet());
-    symbol_table.add(exc_symbol);
-  }
+  // add the exceptional return value
+  auxiliary_symbolt exc_symbol;
+  exc_symbol.mode=ID_java;
+  exc_symbol.name=JAVA_ENTRY_POINT_EXCEPTION_SYMBOL;
+  exc_symbol.base_name=exc_symbol.name;
+  exc_symbol.type=java_reference_type(empty_typet());
+  symbol_table.add(exc_symbol);
+
+  // Zero-initialise the top-level exception catch variable:
+  init_code.copy_to_operands(
+    code_assignt(
+      exc_symbol.symbol_expr(),
+      null_pointer_exprt(to_pointer_type(exc_symbol.type))));
 
   // create code that allocates the objects used as test arguments and
   // non-deterministically initializes them
@@ -638,8 +638,48 @@ bool java_entry_point(
       pointer_type_selector);
   call_main.arguments()=main_arguments;
 
+  // Create target labels for the toplevel exception handler:
+  code_labelt toplevel_catch("toplevel_catch", code_skipt());
+  code_labelt after_catch("after_catch", code_skipt());
+
+  code_blockt call_block;
+
+  // Push a universal exception handler:
+  side_effect_expr_catcht push_universal_handler;
+  irept catch_type_list(ID_exception_list);
+  irept catch_target_list(ID_label);
+  // Catch all exceptions:
+  // This is equivalent to catching Throwable, but also works if some of
+  // the class hierarchy is missing so that we can't determine that
+  // the thrown instance is an indirect child of Throwable
+  catch_type_list.get_sub().push_back(irept());
+  catch_target_list.get_sub().push_back(irept(toplevel_catch.get_label()));
+  push_universal_handler.set(ID_exception_list, catch_type_list);
+  push_universal_handler.set(ID_label, catch_target_list);
+
+  call_block.copy_to_operands(code_expressiont(push_universal_handler));
+
   // we insert the call to the method AFTER the argument initialization code
-  init_code.move_to_operands(call_main);
+  call_block.move_to_operands(call_main);
+
+  // Pop the handler:
+  side_effect_expr_catcht pop_handler;
+  pop_handler.set(ID_exception_list, get_nil_irep());
+  pop_handler.set(ID_label, get_nil_irep());
+
+  //call_block.copy_to_operands(code_expressiont(pop_handler));
+  init_code.move_to_operands(call_block);
+
+  // Normal return: skip the exception handler:
+  init_code.copy_to_operands(code_gotot(after_catch.get_label()));
+
+  // Exceptional return: catch and assign to exc_symbol.
+  side_effect_expr_landingpadt landingpad(exc_symbol.symbol_expr());
+  init_code.copy_to_operands(toplevel_catch);
+  init_code.copy_to_operands(code_expressiont(landingpad));
+
+  // Converge normal and exceptional return:
+  init_code.move_to_operands(after_catch);
 
   // declare certain (which?) variables as test outputs
   java_record_outputs(symbol, main_arguments, init_code, symbol_table);

src/java_bytecode/java_entry_point.h

@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
 #include <java_bytecode/select_pointer_type.h>
 
 #define JAVA_ENTRY_POINT_RETURN_SYMBOL "return'"
+#define JAVA_ENTRY_POINT_EXCEPTION_SYMBOL "uncaught_exception'"
 
 bool java_entry_point(
   class symbol_tablet &symbol_table,