Merge pull request diffblue#3216 from smowton/smowton/feature/shared-class-hierarchy

Share a common class_hierarchyt instance across multiple users

Author: smowton

jbmc/src/janalyzer/janalyzer_parse_options.cpp

@@ -667,13 +667,17 @@ bool janalyzer_parse_optionst::process_goto_program(const optionst &options)
     status() << "Removing function pointers and virtual functions" << eom;
     remove_function_pointers(
       get_message_handler(), goto_model, cmdline.isset("pointer-check"));
+
     // Java virtual functions -> explicit dispatch tables:
     remove_virtual_functions(goto_model);
+
     // remove Java throw and catch
     // This introduces instanceof, so order is important:
-    remove_exceptions(goto_model, get_message_handler());
-    // remove rtti
-    remove_instanceof(goto_model, get_message_handler());
+    remove_exceptions(goto_model, nullptr, get_message_handler());
+
+    // Java instanceof -> clsid comparison:
+    class_hierarchyt class_hierarchy(goto_model.symbol_table);
+    remove_instanceof(goto_model, class_hierarchy, get_message_handler());
 
     // do partial inlining
     status() << "Partial Inlining" << eom;

jbmc/src/java_bytecode/remove_exceptions.cpp

@@ -87,21 +87,31 @@ class remove_exceptionst
 
   explicit remove_exceptionst(
     symbol_table_baset &_symbol_table,
+    const class_hierarchyt *class_hierarchy,
     function_may_throwt _function_may_throw,
     bool remove_added_instanceof,
     message_handlert &message_handler)
     : symbol_table(_symbol_table),
+      class_hierarchy(class_hierarchy),
       function_may_throw(_function_may_throw),
       remove_added_instanceof(remove_added_instanceof),
       message_handler(message_handler)
   {
+    if(remove_added_instanceof)
+    {
+      INVARIANT(
+        class_hierarchy != nullptr,
+        "remove_exceptions needs a class hierarchy to remove instanceof "
+        "statements (either supply one, or don't use REMOVE_ADDED_INSTANCEOF)");
+    }
   }
 
   void operator()(goto_functionst &goto_functions);
   void operator()(goto_programt &goto_program);
 
 protected:
   symbol_table_baset &symbol_table;
+  const class_hierarchyt *class_hierarchy;
   function_may_throwt function_may_throw;
   bool remove_added_instanceof;
   message_handlert &message_handler;
@@ -345,7 +355,14 @@ void remove_exceptionst::add_exception_dispatch_sequence(
         t_exc->guard=check;
 
         if(remove_added_instanceof)
-          remove_instanceof(t_exc, goto_program, symbol_table, message_handler);
+        {
+          remove_instanceof(
+            t_exc,
+            goto_program,
+            symbol_table,
+            *class_hierarchy,
+            message_handler);
+        }
       }
     }
   }
@@ -576,6 +593,7 @@ 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)
@@ -589,6 +607,7 @@ void remove_exceptions(
     };
   remove_exceptionst remove_exceptions(
     symbol_table,
+    class_hierarchy,
     function_may_throw,
     type == remove_exceptions_typest::REMOVE_ADDED_INSTANCEOF,
     message_handler);
@@ -605,13 +624,16 @@ 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 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)
 {
@@ -620,18 +642,35 @@ void remove_exceptions(
 
   remove_exceptionst remove_exceptions(
     symbol_table,
+    class_hierarchy,
     any_function_may_throw,
     type == remove_exceptions_typest::REMOVE_ADDED_INSTANCEOF,
     message_handler);
   remove_exceptions(goto_program);
 }
 
-/// removes throws/CATCH-POP/CATCH-PUSH
+/// 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 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)
 {
   remove_exceptions(
-    goto_model.symbol_table, goto_model.goto_functions, message_handler, type);
+    goto_model.symbol_table,
+    class_hierarchy,
+    goto_model.goto_functions,
+    message_handler,
+    type);
 }

jbmc/src/java_bytecode/remove_exceptions.h

@@ -14,6 +14,7 @@ Date:   December 2016
 #ifndef CPROVER_JAVA_BYTECODE_REMOVE_EXCEPTIONS_H
 #define CPROVER_JAVA_BYTECODE_REMOVE_EXCEPTIONS_H
 
+#include <goto-programs/class_hierarchy.h>
 #include <goto-programs/goto_model.h>
 
 #include <util/message.h>
@@ -34,12 +35,14 @@ enum class remove_exceptions_typest
 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);
 
 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);

jbmc/src/java_bytecode/remove_instanceof.cpp

@@ -24,12 +24,14 @@ class remove_instanceoft
 {
 public:
   remove_instanceoft(
-    symbol_table_baset &symbol_table, message_handlert &message_handler)
-    : symbol_table(symbol_table)
-    , ns(symbol_table)
-    , message_handler(message_handler)
+    symbol_table_baset &symbol_table,
+    const class_hierarchyt &class_hierarchy,
+    message_handlert &message_handler)
+    : symbol_table(symbol_table),
+      class_hierarchy(class_hierarchy),
+      ns(symbol_table),
+      message_handler(message_handler)
   {
-    class_hierarchy(symbol_table);
   }
 
   // Lower instanceof for a single function
@@ -40,8 +42,8 @@ class remove_instanceoft
 
 protected:
   symbol_table_baset &symbol_table;
+  const class_hierarchyt &class_hierarchy;
   namespacet ns;
-  class_hierarchyt class_hierarchy;
   message_handlert &message_handler;
 
   bool lower_instanceof(
@@ -233,21 +235,22 @@ bool remove_instanceoft::lower_instanceof(goto_programt &goto_program)
   return true;
 }
 
-
 /// Replace an instanceof in the expression or guard of the passed instruction
 /// of the given function body with an explicit class-identifier test.
 /// \remarks Extra auxiliary variables may be introduced into symbol_table.
 /// \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 class_hierarchy: class hierarchy analysis of symbol_table
 /// \param message_handler: logging output
 void remove_instanceof(
   goto_programt::targett target,
   goto_programt &goto_program,
   symbol_table_baset &symbol_table,
+  const class_hierarchyt &class_hierarchy,
   message_handlert &message_handler)
 {
-  remove_instanceoft rem(symbol_table, message_handler);
+  remove_instanceoft rem(symbol_table, class_hierarchy, message_handler);
   rem.lower_instanceof(goto_program, target);
 }
 
@@ -256,13 +259,15 @@ 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 class_hierarchy: class hierarchy analysis of symbol_table
 /// \param message_handler: logging output
 void remove_instanceof(
   goto_functionst::goto_functiont &function,
   symbol_table_baset &symbol_table,
+  const class_hierarchyt &class_hierarchy,
   message_handlert &message_handler)
 {
-  remove_instanceoft rem(symbol_table, message_handler);
+  remove_instanceoft rem(symbol_table, class_hierarchy, message_handler);
   rem.lower_instanceof(function.body);
 }
 
@@ -271,13 +276,15 @@ 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 class_hierarchy: class hierarchy analysis of symbol_table
 /// \param message_handler: logging output
 void remove_instanceof(
   goto_functionst &goto_functions,
   symbol_table_baset &symbol_table,
+  const class_hierarchyt &class_hierarchy,
   message_handlert &message_handler)
 {
-  remove_instanceoft rem(symbol_table, message_handler);
+  remove_instanceoft rem(symbol_table, class_hierarchy, message_handler);
   bool changed=false;
   for(auto &f : goto_functions.function_map)
     changed=rem.lower_instanceof(f.second.body) || changed;
@@ -289,12 +296,18 @@ 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 class_hierarchy: class hierarchy analysis of goto_model's symbol
+///   table
 /// \param message_handler: logging output
 /// symbols to.
 void remove_instanceof(
   goto_modelt &goto_model,
+  const class_hierarchyt &class_hierarchy,
   message_handlert &message_handler)
 {
   remove_instanceof(
-    goto_model.goto_functions, goto_model.symbol_table, message_handler);
+    goto_model.goto_functions,
+    goto_model.symbol_table,
+    class_hierarchy,
+    message_handler);
 }

jbmc/src/java_bytecode/remove_instanceof.h

@@ -79,6 +79,7 @@ Author: Chris Smowton, [email protected]
 #ifndef CPROVER_JAVA_BYTECODE_REMOVE_INSTANCEOF_H
 #define CPROVER_JAVA_BYTECODE_REMOVE_INSTANCEOF_H
 
+#include <goto-programs/class_hierarchy.h>
 #include <goto-programs/goto_functions.h>
 #include <goto-programs/goto_model.h>
 
@@ -89,18 +90,24 @@ void remove_instanceof(
   goto_programt::targett target,
   goto_programt &goto_program,
   symbol_table_baset &symbol_table,
+  const class_hierarchyt &class_hierarchy,
   message_handlert &);
 
 void remove_instanceof(
   goto_functionst::goto_functiont &function,
   symbol_table_baset &symbol_table,
+  const class_hierarchyt &class_hierarchy,
   message_handlert &);
 
 void remove_instanceof(
   goto_functionst &goto_functions,
   symbol_table_baset &symbol_table,
+  const class_hierarchyt &class_hierarchy,
   message_handlert &);
 
-void remove_instanceof(goto_modelt &model, message_handlert &);
+void remove_instanceof(
+  goto_modelt &model,
+  const class_hierarchyt &class_hierarchy,
+  message_handlert &);
 
 #endif

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -552,6 +552,9 @@ int jbmc_parse_optionst::doit()
       *this, options, get_message_handler());
     lazy_goto_model.initialize(cmdline, options);
 
+    class_hierarchy =
+      util_make_unique<class_hierarchyt>(lazy_goto_model.symbol_table);
+
     // The precise wording of this error matches goto-symex's complaint when no
     // __CPROVER_start exists (if we just go ahead and run it anyway it will
     // trip an invariant when it tries to load it)
@@ -629,12 +632,13 @@ int jbmc_parse_optionst::get_goto_program(
       *this, options, get_message_handler());
     lazy_goto_model.initialize(cmdline, options);
 
+    class_hierarchy =
+      util_make_unique<class_hierarchyt>(lazy_goto_model.symbol_table);
+
     // Show the class hierarchy
     if(cmdline.isset("show-class-hierarchy"))
     {
-      class_hierarchyt hierarchy;
-      hierarchy(lazy_goto_model.symbol_table);
-      show_class_hierarchy(hierarchy, ui_message_handler);
+      show_class_hierarchy(*class_hierarchy, ui_message_handler);
       return CPROVER_EXIT_SUCCESS;
     }
 
@@ -729,7 +733,8 @@ void jbmc_parse_optionst::process_goto_function(
   try
   {
     // Removal of RTTI inspection:
-    remove_instanceof(goto_function, symbol_table, get_message_handler());
+    remove_instanceof(
+      goto_function, symbol_table, *class_hierarchy, get_message_handler());
     // Java virtual functions -> explicit dispatch tables:
     remove_virtual_functions(function);
 
@@ -743,6 +748,7 @@ 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);
     }
@@ -888,6 +894,7 @@ bool jbmc_parse_optionst::process_goto_functions(
     // (introduces instanceof but request it is removed)
     remove_exceptions(
       goto_model,
+      class_hierarchy.get(),
       get_message_handler(),
       remove_exceptions_typest::REMOVE_ADDED_INSTANCEOF);
 

jbmc/src/jbmc/jbmc_parse_options.h

@@ -123,6 +123,8 @@ class jbmc_parse_optionst:
   object_factory_parameterst object_factory_params;
   bool stub_objects_are_not_null;
 
+  std::unique_ptr<class_hierarchyt> class_hierarchy;
+
   void get_command_line_options(optionst &);
   int get_goto_program(
     std::unique_ptr<goto_modelt> &goto_model, const optionst &);

jbmc/src/jdiff/jdiff_parse_options.cpp

@@ -345,16 +345,20 @@ bool jdiff_parse_optionst::process_goto_program(
   try
   {
     // remove function pointers
-    status() << "Removal of function pointers and virtual functions" << eom;
+    status() << "Removing function pointers and virtual functions" << eom;
     remove_function_pointers(
       get_message_handler(), goto_model, cmdline.isset("pointer-check"));
 
     // Java virtual functions -> explicit dispatch tables:
     remove_virtual_functions(goto_model);
-    // remove catch and throw
-    remove_exceptions(goto_model, get_message_handler());
+
+    // remove Java throw and catch
+    // This introduces instanceof, so order is important:
+    remove_exceptions(goto_model, nullptr, get_message_handler());
+
     // Java instanceof -> clsid comparison:
-    remove_instanceof(goto_model, get_message_handler());
+    class_hierarchyt class_hierarchy(goto_model.symbol_table);
+    remove_instanceof(goto_model, class_hierarchy, get_message_handler());
 
     mm_io(goto_model);