Add message handler to remove_instanceof and _exceptions

This enables reporting errors from remove_instanceof usage of goto_convert.

Author: smowton

jbmc/src/janalyzer/janalyzer_parse_options.cpp

@@ -670,9 +670,9 @@ bool janalyzer_parse_optionst::process_goto_program(const optionst &options)
     remove_virtual_functions(goto_model);
     // remove Java throw and catch
     // This introduces instanceof, so order is important:
-    remove_exceptions(goto_model);
+    remove_exceptions(goto_model, get_message_handler());
     // remove rtti
-    remove_instanceof(goto_model);
+    remove_instanceof(goto_model, get_message_handler());
 
     // do partial inlining
     status() << "Partial Inlining" << eom;

jbmc/src/java_bytecode/remove_exceptions.cpp

@@ -88,10 +88,12 @@ class remove_exceptionst
   explicit remove_exceptionst(
     symbol_table_baset &_symbol_table,
     function_may_throwt _function_may_throw,
-    bool remove_added_instanceof)
+    bool remove_added_instanceof,
+    message_handlert &message_handler)
     : symbol_table(_symbol_table),
       function_may_throw(_function_may_throw),
-      remove_added_instanceof(remove_added_instanceof)
+      remove_added_instanceof(remove_added_instanceof),
+      message_handler(message_handler)
   {
   }
 
@@ -102,6 +104,7 @@ class remove_exceptionst
   symbol_table_baset &symbol_table;
   function_may_throwt function_may_throw;
   bool remove_added_instanceof;
+  message_handlert &message_handler;
 
   symbol_exprt get_inflight_exception_global();
 
@@ -342,7 +345,7 @@ void remove_exceptionst::add_exception_dispatch_sequence(
         t_exc->guard=check;
 
         if(remove_added_instanceof)
-          remove_instanceof(t_exc, goto_program, symbol_table);
+          remove_instanceof(t_exc, goto_program, symbol_table, message_handler);
       }
     }
   }
@@ -574,6 +577,7 @@ void remove_exceptionst::operator()(goto_programt &goto_program)
 void remove_exceptions(
   symbol_table_baset &symbol_table,
   goto_functionst &goto_functions,
+  message_handlert &message_handler,
   remove_exceptions_typest type)
 {
   const namespacet ns(symbol_table);
@@ -586,7 +590,8 @@ void remove_exceptions(
   remove_exceptionst remove_exceptions(
     symbol_table,
     function_may_throw,
-    type == remove_exceptions_typest::REMOVE_ADDED_INSTANCEOF);
+    type == remove_exceptions_typest::REMOVE_ADDED_INSTANCEOF,
+    message_handler);
   remove_exceptions(goto_functions);
 }
 
@@ -600,12 +605,14 @@ void remove_exceptions(
 /// \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
 /// \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,
+  message_handlert &message_handler,
   remove_exceptions_typest type)
 {
   remove_exceptionst::function_may_throwt any_function_may_throw =
@@ -614,12 +621,17 @@ void remove_exceptions(
   remove_exceptionst remove_exceptions(
     symbol_table,
     any_function_may_throw,
-    type == remove_exceptions_typest::REMOVE_ADDED_INSTANCEOF);
+    type == remove_exceptions_typest::REMOVE_ADDED_INSTANCEOF,
+    message_handler);
   remove_exceptions(goto_program);
 }
 
 /// removes throws/CATCH-POP/CATCH-PUSH
-void remove_exceptions(goto_modelt &goto_model, remove_exceptions_typest type)
+void remove_exceptions(
+  goto_modelt &goto_model,
+  message_handlert &message_handler,
+  remove_exceptions_typest type)
 {
-  remove_exceptions(goto_model.symbol_table, goto_model.goto_functions, type);
+  remove_exceptions(
+    goto_model.symbol_table, goto_model.goto_functions, message_handler, type);
 }

jbmc/src/java_bytecode/remove_exceptions.h

@@ -16,6 +16,8 @@ Date:   December 2016
 
 #include <goto-programs/goto_model.h>
 
+#include <util/message.h>
+
 #define INFLIGHT_EXCEPTION_VARIABLE_BASENAME "@inflight_exception"
 #define INFLIGHT_EXCEPTION_VARIABLE_NAME \
   "java::" INFLIGHT_EXCEPTION_VARIABLE_BASENAME
@@ -32,11 +34,13 @@ enum class remove_exceptions_typest
 void remove_exceptions(
   goto_programt &goto_program,
   symbol_table_baset &symbol_table,
+  message_handlert &message_handler,
   remove_exceptions_typest type =
     remove_exceptions_typest::DONT_REMOVE_INSTANCEOF);
 
 void remove_exceptions(
   goto_modelt &goto_model,
+  message_handlert &message_handler,
   remove_exceptions_typest type =
     remove_exceptions_typest::DONT_REMOVE_INSTANCEOF);
 

jbmc/src/java_bytecode/remove_instanceof.cpp

@@ -23,8 +23,11 @@ Author: Chris Smowton, [email protected]
 class remove_instanceoft
 {
 public:
-  explicit remove_instanceoft(symbol_table_baset &symbol_table)
-  : symbol_table(symbol_table), ns(symbol_table)
+  remove_instanceoft(
+    symbol_table_baset &symbol_table, message_handlert &message_handler)
+    : symbol_table(symbol_table)
+    , ns(symbol_table)
+    , message_handler(message_handler)
   {
     class_hierarchy(symbol_table);
   }
@@ -39,6 +42,7 @@ class remove_instanceoft
   symbol_table_baset &symbol_table;
   namespacet ns;
   class_hierarchyt class_hierarchy;
+  message_handlert &message_handler;
 
   bool lower_instanceof(
     exprt &, goto_programt &, goto_programt::targett);
@@ -154,24 +158,15 @@ bool remove_instanceoft::lower_instanceof(
   // Replace the instanceof construct with instanceof_result:
   expr = instanceof_result_sym.symbol_expr();
 
-  std::ostringstream convert_output;
-  stream_message_handlert convert_message_handler(convert_output);
-  convert_message_handler.set_verbosity(messaget::message_levelt::M_WARNING);
-
   // Insert the new test block before it:
   goto_programt new_check_program;
   goto_convert(
     is_null_branch,
     symbol_table,
     new_check_program,
-    convert_message_handler,
+    message_handler,
     ID_java);
 
-  INVARIANT(
-    convert_output.str().empty(),
-    "remove_instanceof generated test should be goto-converted without error, "
-    "but goto_convert reported: " + convert_output.str());
-
   goto_program.destructive_insert(this_inst, new_check_program);
 
   return true;
@@ -245,12 +240,14 @@ bool remove_instanceoft::lower_instanceof(goto_programt &goto_program)
 /// \param target: The instruction to work on.
 /// \param goto_program: The function body containing the instruction.
 /// \param symbol_table: The symbol table to add symbols to.
+/// \param message_handler: logging output
 void remove_instanceof(
   goto_programt::targett target,
   goto_programt &goto_program,
-  symbol_table_baset &symbol_table)
+  symbol_table_baset &symbol_table,
+  message_handlert &message_handler)
 {
-  remove_instanceoft rem(symbol_table);
+  remove_instanceoft rem(symbol_table, message_handler);
   rem.lower_instanceof(goto_program, target);
 }
 
@@ -259,11 +256,13 @@ void remove_instanceof(
 /// \remarks Extra auxiliary variables may be introduced into symbol_table.
 /// \param function: The function to work on.
 /// \param symbol_table: The symbol table to add symbols to.
+/// \param message_handler: logging output
 void remove_instanceof(
   goto_functionst::goto_functiont &function,
-  symbol_table_baset &symbol_table)
+  symbol_table_baset &symbol_table,
+  message_handlert &message_handler)
 {
-  remove_instanceoft rem(symbol_table);
+  remove_instanceoft rem(symbol_table, message_handler);
   rem.lower_instanceof(function.body);
 }
 
@@ -272,11 +271,13 @@ void remove_instanceof(
 /// \remarks Extra auxiliary variables may be introduced into symbol_table.
 /// \param goto_functions: The functions to work on.
 /// \param symbol_table: The symbol table to add symbols to.
+/// \param message_handler: logging output
 void remove_instanceof(
   goto_functionst &goto_functions,
-  symbol_table_baset &symbol_table)
+  symbol_table_baset &symbol_table,
+  message_handlert &message_handler)
 {
-  remove_instanceoft rem(symbol_table);
+  remove_instanceoft rem(symbol_table, message_handler);
   bool changed=false;
   for(auto &f : goto_functions.function_map)
     changed=rem.lower_instanceof(f.second.body) || changed;
@@ -288,8 +289,12 @@ void remove_instanceof(
 /// class-identifier test.
 /// \remarks Extra auxiliary variables may be introduced into symbol_table.
 /// \param goto_model: The functions to work on and the symbol table to add
+/// \param message_handler: logging output
 /// symbols to.
-void remove_instanceof(goto_modelt &goto_model)
+void remove_instanceof(
+  goto_modelt &goto_model,
+  message_handlert &message_handler)
 {
-  remove_instanceof(goto_model.goto_functions, goto_model.symbol_table);
+  remove_instanceof(
+    goto_model.goto_functions, goto_model.symbol_table, message_handler);
 }

jbmc/src/java_bytecode/remove_instanceof.h

@@ -12,24 +12,28 @@ Author: Chris Smowton, [email protected]
 #ifndef CPROVER_JAVA_BYTECODE_REMOVE_INSTANCEOF_H
 #define CPROVER_JAVA_BYTECODE_REMOVE_INSTANCEOF_H
 
-#include <util/symbol_table.h>
-
 #include <goto-programs/goto_functions.h>
 #include <goto-programs/goto_model.h>
 
+#include <util/message.h>
+#include <util/symbol_table.h>
+
 void remove_instanceof(
   goto_programt::targett target,
   goto_programt &goto_program,
-  symbol_table_baset &symbol_table);
+  symbol_table_baset &symbol_table,
+  message_handlert &);
 
 void remove_instanceof(
   goto_functionst::goto_functiont &function,
-  symbol_table_baset &symbol_table);
+  symbol_table_baset &symbol_table,
+  message_handlert &);
 
 void remove_instanceof(
   goto_functionst &goto_functions,
-  symbol_table_baset &symbol_table);
+  symbol_table_baset &symbol_table,
+  message_handlert &);
 
-void remove_instanceof(goto_modelt &model);
+void remove_instanceof(goto_modelt &model, message_handlert &);
 
 #endif

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -755,7 +755,7 @@ void jbmc_parse_optionst::process_goto_function(
   try
   {
     // Removal of RTTI inspection:
-    remove_instanceof(goto_function, symbol_table);
+    remove_instanceof(goto_function, symbol_table, get_message_handler());
     // Java virtual functions -> explicit dispatch tables:
     remove_virtual_functions(function);
 
@@ -769,6 +769,7 @@ void jbmc_parse_optionst::process_goto_function(
       remove_exceptions(
         goto_function.body,
         symbol_table,
+        get_message_handler(),
         remove_exceptions_typest::REMOVE_ADDED_INSTANCEOF);
     }
 
@@ -916,7 +917,9 @@ bool jbmc_parse_optionst::process_goto_functions(
     // remove catch and throw
     // (introduces instanceof but request it is removed)
     remove_exceptions(
-      goto_model, remove_exceptions_typest::REMOVE_ADDED_INSTANCEOF);
+      goto_model,
+      get_message_handler(),
+      remove_exceptions_typest::REMOVE_ADDED_INSTANCEOF);
 
     // instrument library preconditions
     instrument_preconditions(goto_model);

jbmc/src/jdiff/jdiff_parse_options.cpp

@@ -346,9 +346,9 @@ bool jdiff_parse_optionst::process_goto_program(
     // Java virtual functions -> explicit dispatch tables:
     remove_virtual_functions(goto_model);
     // remove catch and throw
-    remove_exceptions(goto_model);
+    remove_exceptions(goto_model, get_message_handler());
     // Java instanceof -> clsid comparison:
-    remove_instanceof(goto_model);
+    remove_instanceof(goto_model, get_message_handler());
 
     mm_io(goto_model);
 

jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp

@@ -95,7 +95,7 @@ TEST_CASE(
     goto_model_functiont model_function(
       symbol_table, functions, function_name, goto_function);
 
-    remove_instanceof(goto_function, symbol_table);
+    remove_instanceof(goto_function, symbol_table, null_message_handler);
 
     remove_virtual_functions(model_function);