simplify the remove_exceptions API

jbmc/src/janalyzer/janalyzer_parse_options.cpp

@@ -673,7 +673,7 @@ bool janalyzer_parse_optionst::process_goto_program(const optionst &options)
 
     // remove Java throw and catch
     // This introduces instanceof, so order is important:
-    remove_exceptions(goto_model, nullptr, get_message_handler());
+    remove_exceptions_using_instanceof(goto_model, get_message_handler());
 
     // Java instanceof -> clsid comparison:
     class_hierarchyt class_hierarchy(goto_model.symbol_table);

jbmc/src/java_bytecode/remove_exceptions.cpp

@@ -87,15 +87,15 @@ class remove_exceptionst
 
   explicit remove_exceptionst(
     symbol_table_baset &_symbol_table,
-    const class_hierarchyt *class_hierarchy,
+    const class_hierarchyt *_class_hierarchy,
     function_may_throwt _function_may_throw,
-    bool remove_added_instanceof,
-    message_handlert &message_handler)
+    bool _remove_added_instanceof,
+    message_handlert &_message_handler)
     : symbol_table(_symbol_table),
-      class_hierarchy(class_hierarchy),
+      class_hierarchy(_class_hierarchy),
       function_may_throw(_function_may_throw),
-      remove_added_instanceof(remove_added_instanceof),
-      message_handler(message_handler)
+      remove_added_instanceof(_remove_added_instanceof),
+      message_handler(_message_handler)
   {
     if(remove_added_instanceof)
     {
@@ -590,27 +590,88 @@ void remove_exceptionst::operator()(goto_programt &goto_program)
   instrument_exceptions(goto_program);
 }
 
+/// removes throws/CATCH-POP/CATCH-PUSH
+void remove_exceptions_using_instanceof(
+  symbol_table_baset &symbol_table,
+  goto_functionst &goto_functions,
+  message_handlert &message_handler)
+{
+  const namespacet ns(symbol_table);
+  std::map<irep_idt, std::set<irep_idt>> exceptions_map;
+
+  uncaught_exceptions(goto_functions, ns, exceptions_map);
+
+  remove_exceptionst::function_may_throwt function_may_throw =
+    [&exceptions_map](const irep_idt &id) {
+      return !exceptions_map[id].empty();
+    };
+
+  remove_exceptionst remove_exceptions(
+    symbol_table, nullptr, function_may_throw, false, message_handler);
+
+  remove_exceptions(goto_functions);
+}
+
+/// removes throws/CATCH-POP/CATCH-PUSH from a single GOTO program, replacing
+/// them with explicit exception propagation.
+/// Note this is somewhat less accurate than the whole-goto-model version,
+/// because we can't inspect other functions to determine whether they throw
+/// or not, and therefore must assume they do and always introduce post-call
+/// exception dispatch.
+/// \param goto_program: program to remove exceptions from
+/// \param symbol_table: global symbol table. The `@inflight_exception` global
+///   may be added if not already present. It will not be initialised; that is
+///   the caller's responsibility.
+/// \param message_handler: logging output
+void remove_exceptions_using_instanceof(
+  goto_programt &goto_program,
+  symbol_table_baset &symbol_table,
+  message_handlert &message_handler)
+{
+  remove_exceptionst::function_may_throwt any_function_may_throw =
+    [](const irep_idt &) { return true; };
+
+  remove_exceptionst remove_exceptions(
+    symbol_table, nullptr, any_function_may_throw, false, message_handler);
+
+  remove_exceptions(goto_program);
+}
+
+/// removes throws/CATCH-POP/CATCH-PUSH, replacing them with explicit exception
+/// propagation.
+/// \param goto_model: model to remove exceptions from. The
+///   `@inflight_exception` global may be added to its symbol table if not
+///   already present. It will not be initialised; that is the caller's
+///   responsibility.
+/// \param message_handler: logging output
+void remove_exceptions_using_instanceof(
+  goto_modelt &goto_model,
+  message_handlert &message_handler)
+{
+  remove_exceptions_using_instanceof(
+    goto_model.symbol_table, goto_model.goto_functions, message_handler);
+}
+
 /// removes throws/CATCH-POP/CATCH-PUSH
 void remove_exceptions(
   symbol_table_baset &symbol_table,
-  const class_hierarchyt *class_hierarchy,
   goto_functionst &goto_functions,
-  message_handlert &message_handler,
-  remove_exceptions_typest type)
+  const class_hierarchyt &class_hierarchy,
+  message_handlert &message_handler)
 {
   const namespacet ns(symbol_table);
   std::map<irep_idt, std::set<irep_idt>> exceptions_map;
+
   uncaught_exceptions(goto_functions, ns, exceptions_map);
+
   remove_exceptionst::function_may_throwt function_may_throw =
     [&exceptions_map](const irep_idt &id) {
       return !exceptions_map[id].empty();
     };
+
   remove_exceptionst remove_exceptions(
-    symbol_table,
-    class_hierarchy,
-    function_may_throw,
-    type == remove_exceptions_typest::REMOVE_ADDED_INSTANCEOF,
-    message_handler);
+    symbol_table, &class_hierarchy, function_may_throw, true, message_handler);
+
   remove_exceptions(goto_functions);
 }
 
@@ -627,25 +688,22 @@ void remove_exceptions(
 /// \param class_hierarchy: class hierarchy analysis of symbol_table.
 ///   Only needed if type == REMOVE_ADDED_INSTANCEOF; otherwise may be null.
 /// \param message_handler: logging output
-/// \param type: specifies whether instanceof operations generated by this pass
-///   should be lowered to class-identifier comparisons (using
-///   remove_instanceof).
 void remove_exceptions(
   goto_programt &goto_program,
   symbol_table_baset &symbol_table,
-  const class_hierarchyt *class_hierarchy,
-  message_handlert &message_handler,
-  remove_exceptions_typest type)
+  const class_hierarchyt &class_hierarchy,
+  message_handlert &message_handler)
 {
   remove_exceptionst::function_may_throwt any_function_may_throw =
     [](const irep_idt &) { return true; };
 
   remove_exceptionst remove_exceptions(
     symbol_table,
-    class_hierarchy,
+    &class_hierarchy,
     any_function_may_throw,
-    type == remove_exceptions_typest::REMOVE_ADDED_INSTANCEOF,
+    true,
     message_handler);
+
   remove_exceptions(goto_program);
 }
 
@@ -658,19 +716,14 @@ void remove_exceptions(
 /// \param class_hierarchy: class hierarchy analysis of symbol_table.
 ///   Only needed if type == REMOVE_ADDED_INSTANCEOF; otherwise may be null.
 /// \param message_handler: logging output
-/// \param type: specifies whether instanceof operations generated by this pass
-///   should be lowered to class-identifier comparisons (using
-///   remove_instanceof).
 void remove_exceptions(
   goto_modelt &goto_model,
-  const class_hierarchyt *class_hierarchy,
-  message_handlert &message_handler,
-  remove_exceptions_typest type)
+  const class_hierarchyt &class_hierarchy,
+  message_handlert &message_handler)
 {
   remove_exceptions(
     goto_model.symbol_table,
-    class_hierarchy,
     goto_model.goto_functions,
-    message_handler,
-    type);
+    class_hierarchy,
+    message_handler);
 }

jbmc/src/java_bytecode/remove_exceptions.h

@@ -23,28 +23,34 @@ Date:   December 2016
 #define INFLIGHT_EXCEPTION_VARIABLE_NAME \
   "java::" INFLIGHT_EXCEPTION_VARIABLE_BASENAME
 
-// Removes 'throw x' and CATCH-PUSH/CATCH-POP
-// and adds the required instrumentation (GOTOs and assignments)
-
-enum class remove_exceptions_typest
-{
-  REMOVE_ADDED_INSTANCEOF,
-  DONT_REMOVE_INSTANCEOF,
-};
-
+/// Removes 'throw x' and CATCH-PUSH/CATCH-POP
+/// and adds the required instrumentation (GOTOs and assignments)
+/// This introduces instanceof expressions.
+void remove_exceptions_using_instanceof(
+  goto_programt &,
+  symbol_table_baset &,
+  message_handlert &);
+
+/// Removes 'throw x' and CATCH-PUSH/CATCH-POP
+/// and adds the required instrumentation (GOTOs and assignments)
+/// This introduces instanceof expressions.
+void remove_exceptions_using_instanceof(goto_modelt &, message_handlert &);
+
+/// Removes 'throw x' and CATCH-PUSH/CATCH-POP
+/// and adds the required instrumentation (GOTOs and assignments)
+/// This does not introduce instanceof expressions.
 void remove_exceptions(
-  goto_programt &goto_program,
-  symbol_table_baset &symbol_table,
-  const class_hierarchyt *class_hierarchy,
-  message_handlert &message_handler,
-  remove_exceptions_typest type =
-    remove_exceptions_typest::DONT_REMOVE_INSTANCEOF);
-
+  goto_programt &,
+  symbol_table_baset &,
+  const class_hierarchyt &,
+  message_handlert &);
+
+/// Removes 'throw x' and CATCH-PUSH/CATCH-POP
+/// and adds the required instrumentation (GOTOs and assignments)
+/// This does not introduce instanceof expressions.
 void remove_exceptions(
-  goto_modelt &goto_model,
-  const class_hierarchyt *class_hierarchy,
-  message_handlert &message_handler,
-  remove_exceptions_typest type =
-    remove_exceptions_typest::DONT_REMOVE_INSTANCEOF);
+  goto_modelt &,
+  const class_hierarchyt &,
+  message_handlert &);
 
 #endif

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -748,9 +748,8 @@ void jbmc_parse_optionst::process_goto_function(
       remove_exceptions(
         goto_function.body,
         symbol_table,
-        class_hierarchy.get(),
-        get_message_handler(),
-        remove_exceptions_typest::REMOVE_ADDED_INSTANCEOF);
+        *class_hierarchy.get(),
+        get_message_handler());
     }
 
     auto function_is_stub = [&symbol_table, &model](const irep_idt &id) {
@@ -891,12 +890,8 @@ bool jbmc_parse_optionst::process_goto_functions(
       return false;
 
     // remove catch and throw
-    // (introduces instanceof but request it is removed)
     remove_exceptions(
-      goto_model,
-      class_hierarchy.get(),
-      get_message_handler(),
-      remove_exceptions_typest::REMOVE_ADDED_INSTANCEOF);
+      goto_model, *class_hierarchy.get(), get_message_handler());
 
     // instrument library preconditions
     instrument_preconditions(goto_model);

jbmc/src/jdiff/jdiff_parse_options.cpp

@@ -354,7 +354,7 @@ bool jdiff_parse_optionst::process_goto_program(
 
     // remove Java throw and catch
     // This introduces instanceof, so order is important:
-    remove_exceptions(goto_model, nullptr, get_message_handler());
+    remove_exceptions_using_instanceof(goto_model, get_message_handler());
 
     // Java instanceof -> clsid comparison:
     class_hierarchyt class_hierarchy(goto_model.symbol_table);