simplify the remove_exceptions API

This removes the usage of a pointer an the potential to call the variant
that does remove_instanceof without class hierarchy.

Author: Daniel Kroening

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(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,14 +87,14 @@ 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,
+    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),
+      remove_added_instanceof(_remove_added_instanceof),
       message_handler(message_handler)
   {
     if(remove_added_instanceof)
@@ -593,24 +593,85 @@ void remove_exceptionst::operator()(goto_programt &goto_program)
 /// 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)
+  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, 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(
+  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(
+  goto_modelt &goto_model,
+  message_handlert &message_handler)
+{
+  remove_exceptions(
+    goto_model.symbol_table, goto_model.goto_functions, message_handler);
+}
+
+/// removes throws/CATCH-POP/CATCH-PUSH
+void remove_exceptions_and_instanceof(
+  symbol_table_baset &symbol_table,
+  goto_functionst &goto_functions,
+  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, true, message_handler);
+
   remove_exceptions(goto_functions);
 }
 
@@ -630,22 +691,22 @@ void remove_exceptions(
 /// \param type: specifies whether instanceof operations generated by this pass
 ///   should be lowered to class-identifier comparisons (using
 ///   remove_instanceof).
-void remove_exceptions(
+void remove_exceptions_and_instanceof(
   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);
 }
 
@@ -661,16 +722,14 @@ void remove_exceptions(
 /// \param type: specifies whether instanceof operations generated by this pass
 ///   should be lowered to class-identifier comparisons (using
 ///   remove_instanceof).
-void remove_exceptions(
+void remove_exceptions_and_instanceof(
   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(
+  remove_exceptions_and_instanceof(
     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,
-};
-
-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);
-
+/// Removes 'throw x' and CATCH-PUSH/CATCH-POP
+/// and adds the required instrumentation (GOTOs and assignments)
+/// This may 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_programt &,
+  symbol_table_baset &,
+  message_handlert &);
+
+/// Removes 'throw x' and CATCH-PUSH/CATCH-POP
+/// and adds the required instrumentation (GOTOs and assignments)
+/// This may introduce instanceof expressions.
+void remove_exceptions(goto_modelt &, message_handlert &);
+
+/// Removes 'throw x' and CATCH-PUSH/CATCH-POP
+/// and adds the required instrumentation (GOTOs and assignments)
+/// Any instanceof expressions are expanded.
+void remove_exceptions_and_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)
+/// Any instanceof expressions are expanded.
+void remove_exceptions_and_instanceof(
+  goto_modelt &,
+  const class_hierarchyt &,
+  message_handlert &);
 
 #endif

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -745,12 +745,11 @@ void jbmc_parse_optionst::process_goto_function(
       // symex doesn't have to cope with exception-handling constructs; however
       // the results are slightly worse than running it in whole-program mode
       // (e.g. dead catch sites will be retained)
-      remove_exceptions(
+      remove_exceptions_and_instanceof(
         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) {
@@ -890,13 +889,9 @@ bool jbmc_parse_optionst::process_goto_functions(
     if(using_symex_driven_loading)
       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);
+    // remove catch and throw and remove the introduced instanceof
+    remove_exceptions_and_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(goto_model, get_message_handler());
 
     // Java instanceof -> clsid comparison:
     class_hierarchyt class_hierarchy(goto_model.symbol_table);