Clean up CATCH instruction code

The three types of CATCH instruction (push-handler, pop-handler and handler-landingpad)
are now represented by distinct codet subclasses, and the codet and GOTO representations
have been made uniform (the goto-convert step is a simple copy with instruction type CATCH).

The Java version of push-catch gives <type-tag, label> pairs and then later populates
GOTO targets for them, while the C++ version, being block-structured by nature,
omits the labels and directly populates the GOTO instruction targets.

Author: smowton

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,12 +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_exception_landingpad(
-    side_effect_exprt &expr,
-    goto_programt &dest);
   void remove_assignment(
     side_effect_exprt &expr,
     goto_programt &dest,
@@ -246,10 +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_java_exception_landingpad(
-    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);

src/goto-programs/goto_convert_exceptions.cpp

@@ -93,69 +93,6 @@ void goto_convertt::convert_msc_leave(
   t->source_location=code.source_location();
 }
 
-void goto_convertt::convert_java_try_catch(
-  const codet &code,
-  goto_programt &dest)
-{
-  assert(!code.operands().empty());
-
-  // add the CATCH instruction to 'dest'
-  goto_programt::targett catch_instruction=dest.add_instruction();
-  catch_instruction->make_catch();
-  catch_instruction->code.set_statement(ID_catch);
-  catch_instruction->source_location=code.source_location();
-  catch_instruction->function=code.source_location().get_function();
-
-  // the CATCH instruction is annotated with a list of exception IDs
-  const irept exceptions=code.op0().find(ID_exception_list);
-  if(exceptions.is_not_nil())
-  {
-    irept::subt exceptions_sub=exceptions.get_sub();
-    irept::subt &exception_list=
-      catch_instruction->code.add(ID_exception_list).get_sub();
-    exception_list.resize(exceptions_sub.size());
-    for(size_t i=0; i<exceptions_sub.size(); ++i)
-      exception_list[i].id(exceptions_sub[i].id());
-  }
-
-  // the CATCH instruction is also annotated with a list of handle labels
-  const irept handlers=code.op0().find(ID_label);
-  if(handlers.is_not_nil())
-  {
-    irept::subt handlers_sub=handlers.get_sub();
-    irept::subt &handlers_list=
-      catch_instruction->code.add(ID_label).get_sub();
-    handlers_list.resize(handlers_sub.size());
-    for(size_t i=0; i<handlers_sub.size(); ++i)
-      handlers_list[i].id(handlers_sub[i].id());
-  }
-
-  // add a SKIP target for the end of everything
-  goto_programt end;
-  goto_programt::targett end_target=end.add_instruction();
-  end_target->make_skip();
-  end_target->source_location=code.source_location();
-  end_target->function=code.source_location().get_function();
-
-  // add the end-target
-  dest.destructive_append(end);
-}
-
-/// Lower a side_effect_exprt describing an exception
-/// landing-pad (catch site) into GOTO code
-/// \param code: code to convert
-///   (must be a code_expressiont(side_effect_expr_landingpadt))
-/// \param [out] dest: code appended to this GOTO program
-void goto_convertt::convert_java_exception_landingpad(
-  const codet &code,
-  goto_programt &dest)
-{
-  PRECONDITION(code.get_statement()==ID_expression);
-  PRECONDITION(
-    to_side_effect_expr(code.op0()).get_statement()==ID_exception_landingpad);
-  copy(code, CATCH, dest);
-}
-
 void goto_convertt::convert_try_catch(
   const codet &code,
   goto_programt &dest)
@@ -165,13 +102,14 @@ void goto_convertt::convert_try_catch(
   // add the CATCH-push instruction to 'dest'
   goto_programt::targett catch_push_instruction=dest.add_instruction();
   catch_push_instruction->make_catch();
-  catch_push_instruction->code.set_statement(ID_catch);
   catch_push_instruction->source_location=code.source_location();
 
+  code_push_catcht push_catch_code;
+
   // the CATCH-push instruction is annotated with a list of IDs,
   // one per target
-  irept::subt &exception_list=
-    catch_push_instruction->code.add(ID_exception_list).get_sub();
+  code_push_catcht::exception_listt &exception_list=
+    push_catch_code.exception_list();
 
   // add a SKIP target for the end of everything
   goto_programt end;
@@ -184,7 +122,7 @@ void goto_convertt::convert_try_catch(
   // add the CATCH-pop to the end of the 'try' block
   goto_programt::targett catch_pop_instruction=dest.add_instruction();
   catch_pop_instruction->make_catch();
-  catch_pop_instruction->code.set_statement(ID_catch);
+  catch_pop_instruction->code=code_pop_catcht();
 
   // add a goto to the end of the 'try' block
   dest.add_instruction()->make_goto(end_target);
@@ -194,7 +132,8 @@ void goto_convertt::convert_try_catch(
     const codet &block=to_code(code.operands()[i]);
 
     // grab the ID and add to CATCH instruction
-    exception_list.push_back(irept(block.get(ID_exception_id)));
+    exception_list.push_back(
+      code_push_catcht::exception_list_entryt(block.get(ID_exception_id)));
 
     goto_programt tmp;
     convert(block, tmp);
@@ -205,6 +144,8 @@ void goto_convertt::convert_try_catch(
     dest.add_instruction()->make_goto(end_target);
   }
 
+  catch_push_instruction->code=push_catch_code;
+
   // add the end-target
   dest.destructive_append(end);
 }

src/goto-programs/goto_convert_side_effect.cpp

@@ -636,34 +636,6 @@ void goto_convertt::remove_statement_expression(
   static_cast<exprt &>(expr)=tmp_symbol_expr;
 }
 
-void goto_convertt::remove_push_catch(
-  side_effect_exprt &expr,
-  goto_programt &dest)
-{
-  // we only get here for ID_push_catch, which is only used for Java
-  convert_java_try_catch(code_expressiont(expr), dest);
-
-  // the result can't be used, these are void
-  expr.make_nil();
-}
-
-/// Lower a side_effect_exprt describing an exception
-/// landing-pad (catch site) into GOTO code
-/// \param expr: expression to convert
-/// \param [out] dest: code appended to this GOTO program
-void goto_convertt::remove_exception_landingpad(
-  side_effect_exprt &expr,
-  goto_programt &dest)
-{
-  PRECONDITION(expr.get_statement()==ID_exception_landingpad);
-
-  // Similar to the above, only currently used in Java.
-  convert_java_exception_landingpad(code_expressiont(expr), dest);
-
-  // the result can't be used, these are void
-  expr.make_nil();
-}
-
 void goto_convertt::remove_side_effect(
   side_effect_exprt &expr,
   goto_programt &dest,
@@ -724,10 +696,6 @@ void goto_convertt::remove_side_effect(
     // the result can't be used, these are void
     expr.make_nil();
   }
-  else if(statement==ID_push_catch)
-    remove_push_catch(expr, dest);
-  else if(statement==ID_exception_landingpad)
-    remove_exception_landingpad(expr, dest);
   else
   {
     error().source_location=expr.find_source_location();

src/goto-programs/goto_program.cpp

@@ -158,41 +158,42 @@ std::ostream &goto_programt::output_instruction(
 
   case CATCH:
   {
-    if(instruction.code.get_statement()==ID_expression &&
-       instruction.code.op0().id()==ID_side_effect)
+    if(instruction.code.get_statement()==ID_exception_landingpad)
     {
-      const auto &landingpad=
-        to_side_effect_expr_landingpad(instruction.code.op0());
+      const auto &landingpad=to_code_landingpad(instruction.code);
       out << "EXCEPTION LANDING PAD ("
           << from_type(ns, identifier, landingpad.catch_expr().type())
           << ' '
           << from_expr(ns, identifier, landingpad.catch_expr())
           << ")";
     }
-    else if(instruction.code.get_statement()==ID_catch)
+    else if(instruction.code.get_statement()==ID_push_catch)
     {
-      if(!instruction.targets.empty())
+      out << "CATCH-PUSH ";
+
+      unsigned i=0;
+      const irept::subt &exception_list=
+        instruction.code.find(ID_exception_list).get_sub();
+      assert(instruction.targets.size()==exception_list.size());
+      for(instructiont::targetst::const_iterator
+            gt_it=instruction.targets.begin();
+          gt_it!=instruction.targets.end();
+          gt_it++,
+            i++)
       {
-        out << "CATCH-PUSH ";
-
-        unsigned i=0;
-        const irept::subt &exception_list=
-          instruction.code.find(ID_exception_list).get_sub();
-        assert(instruction.targets.size()==exception_list.size());
-        for(instructiont::targetst::const_iterator
-              gt_it=instruction.targets.begin();
-            gt_it!=instruction.targets.end();
-            gt_it++,
-              i++)
-        {
-          if(gt_it!=instruction.targets.begin())
-            out << ", ";
-          out << exception_list[i].id() << "->"
-              << (*gt_it)->target_number;
-        }
+        if(gt_it!=instruction.targets.begin())
+          out << ", ";
+        out << exception_list[i].id() << "->"
+            << (*gt_it)->target_number;
       }
-      else
-        out << "CATCH-POP";
+    }
+    else if(instruction.code.get_statement()==ID_pop_catch)
+    {
+      out << "CATCH-POP";
+    }
+    else
+    {
+      out << "! unexpected CATCH opcode " << instruction.code.get_statement();
     }
 
     out << '\n';