Remove assumptions about exception handlers

regression/cbmc-java/exceptions19/exception_handler.j

@@ -0,0 +1,25 @@
+.class exception_handler
+.super java/lang/Object
+
+.method public <init>()V
+        aload_0
+        invokevirtual java/lang/Object/<init>()V
+        return
+.end method
+
+.method public f()V
+        .limit stack 4
+        .limit locals 4
+
+      begin:
+        new java/lang/Exception
+        dup
+        invokespecial java/lang/Exception.<init>()V
+        athrow
+      start:
+        dup
+      end:
+        astore_1
+        return
+.catch all from begin to end using start
+.end method

regression/cbmc-java/exceptions19/test.desc

@@ -0,0 +1,8 @@
+CORE
+exception_handler.class
+--function exception_handler.f
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/goto-programs/remove_exceptions.cpp

@@ -90,8 +90,8 @@ void remove_exceptionst::add_exceptional_returns(
   if(goto_program.empty())
     return;
 
-  // the entry function has already been added to the symbol table
-  // if you find it, initialise it
+  // some methods (e.g. the entry method) have already been added to
+  // the symbol table; if you find it, initialise it
   if(symbol_table.has_symbol(id2string(function_id)+EXC_SUFFIX))
   {
     const symbolt &symbol=

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -20,6 +20,7 @@ Author: Daniel Kroening, [email protected]
 #include <linking/zero_initializer.h>
 
 #include <goto-programs/cfg.h>
+#include <goto-programs/remove_exceptions.h>
 #include <analyses/cfg_dominators.h>
 
 #include "java_bytecode_convert_method.h"
@@ -472,7 +473,8 @@ void java_bytecode_convert_methodt::convert(
 
   tmp_vars.clear();
   if((!m.is_abstract) && (!m.is_native))
-    method_symbol.value=convert_instructions(m, code_type);
+    method_symbol.value=convert_instructions(
+      m, code_type, method_symbol.name);
 
   // Replace the existing stub symbol with the real deal:
   const auto s_it=symbol_table.symbols.find(method.get_name());
@@ -1119,7 +1121,8 @@ Function: java_bytecode_convert_methodt::convert_instructions
 
 codet java_bytecode_convert_methodt::convert_instructions(
   const methodt &method,
-  const code_typet &method_type)
+  const code_typet &method_type,
+  const irep_idt &method_name)
 {
   const instructionst &instructions=method.instructions;
 
@@ -1305,48 +1308,29 @@ codet java_bytecode_convert_methodt::convert_instructions(
       statement=std::string(id2string(statement), 0, statement.size()-2);
     }
 
-    // we throw away the first statement in an exception handler
-    // as we don't know if a function call had a normal or exceptional return
     auto it=method.exception_table.begin();
     for(; it!=method.exception_table.end(); ++it)
     {
       if(cur_pc==it->handler_pc)
       {
-        exprt exc_var=variable(
-          arg0, statement[0],
-          i_it->address,
-          NO_CAST);
-
-        // throw away the operands
-        pop_residue(bytecode_info.pop);
-
-        // add a CATCH-PUSH signaling a handler
-        side_effect_expr_catcht catch_handler_expr;
-        // pack the exception variable so that it can be used
-        // later for instrumentation
-        catch_handler_expr.get_sub().resize(1);
-        catch_handler_expr.get_sub()[0]=exc_var;
-
-        code_expressiont catch_handler(catch_handler_expr);
-        code_labelt newlabel(label(std::to_string(cur_pc)),
-                             code_blockt());
-
-        code_blockt label_block=to_code_block(newlabel.code());
-        code_blockt handler_block;
-        handler_block.move_to_operands(c);
-        handler_block.move_to_operands(catch_handler);
-        handler_block.move_to_operands(label_block);
-        c=handler_block;
-        break;
+        // at the beginning of a handler, clear the stack and
+        // push the corresponding exceptional return variable
+        stack.clear();
+        auxiliary_symbolt new_symbol;
+        new_symbol.is_static_lifetime=true;
+        // generate the name of the exceptional return variable
+        const std::string &exceptional_var_name=
+          id2string(method_name)+
+          EXC_SUFFIX;
+        new_symbol.base_name=exceptional_var_name;
+        new_symbol.name=exceptional_var_name;
+        new_symbol.type=typet(ID_pointer, empty_typet());
+        new_symbol.mode=ID_java;
+        symbol_table.add(new_symbol);
+        stack.push_back(new_symbol.symbol_expr());
       }
     }
 
-    if(it!=method.exception_table.end())
-    {
-      // go straight to the next statement
-      continue;
-    }
-
     exprt::operandst op=pop(bytecode_info.pop);
     exprt::operandst results;
     results.resize(bytecode_info.push, nil_exprt());
@@ -2533,9 +2517,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
       address_mapt::iterator a_it2=address_map.find(address);
       assert(a_it2!=address_map.end());
 
-      // we don't worry about exception handlers as we don't load the
-      // operands from the stack anyway -- we keep explicit global
-      // exception variables
+      // clear the stack if this is an exception handler
       for(const auto &exception_row : method.exception_table)
       {
         if(address==exception_row.handler_pc)
@@ -2604,7 +2586,6 @@ codet java_bytecode_convert_methodt::convert_instructions(
               c.copy_to_operands(*o_it);
         }
       }
-
       a_it2->second.stack=stack;
     }
   }

src/java_bytecode/java_bytecode_convert_method_class.h

@@ -214,7 +214,8 @@ class java_bytecode_convert_methodt:public messaget
 
   codet convert_instructions(
     const methodt &,
-    const code_typet &);
+    const code_typet &,
+    const irep_idt &);
 
   const bytecode_infot &get_bytecode_info(const irep_idt &statement);
 

src/java_bytecode/java_entry_point.cpp

@@ -589,14 +589,17 @@ bool java_entry_point(
     call_main.lhs()=return_symbol.symbol_expr();
   }
 
-  // add the exceptional return value
-  auxiliary_symbolt exc_symbol;
-  exc_symbol.mode=ID_C;
-  exc_symbol.is_static_lifetime=false;
-  exc_symbol.name=id2string(symbol.name)+EXC_SUFFIX;
-  exc_symbol.base_name=id2string(symbol.name)+EXC_SUFFIX;
-  exc_symbol.type=typet(ID_pointer, empty_typet());
-  symbol_table.add(exc_symbol);
+  if(!symbol_table.has_symbol(id2string(symbol.name)+EXC_SUFFIX))
+  {
+    // add the exceptional return value
+    auxiliary_symbolt exc_symbol;
+    exc_symbol.mode=ID_C;
+    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=typet(ID_pointer, empty_typet());
+    symbol_table.add(exc_symbol);
+  }
 
   exprt::operandst main_arguments=
     java_build_arguments(