Add analysis cache

jbmc/src/java_bytecode/remove_exceptions.cpp

@@ -89,10 +89,12 @@ class remove_exceptionst
     symbol_table_baset &_symbol_table,
     function_may_throwt _function_may_throw,
     bool remove_added_instanceof,
+    class_hierarchyt &class_hierarchy,
     message_handlert &message_handler)
     : symbol_table(_symbol_table),
       function_may_throw(_function_may_throw),
       remove_added_instanceof(remove_added_instanceof),
+      class_hierarchy(class_hierarchy),
       message_handler(message_handler)
   {
   }
@@ -104,6 +106,7 @@ class remove_exceptionst
   symbol_table_baset &symbol_table;
   function_may_throwt function_may_throw;
   bool remove_added_instanceof;
+  class_hierarchyt &class_hierarchy;
   message_handlert &message_handler;
 
   symbol_exprt get_inflight_exception_global();
@@ -345,7 +348,12 @@ 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);
       }
     }
   }
@@ -575,24 +583,26 @@ void remove_exceptionst::operator()(goto_programt &goto_program)
 
 /// removes throws/CATCH-POP/CATCH-PUSH
 void remove_exceptions(
-  symbol_table_baset &symbol_table,
-  goto_functionst &goto_functions,
+  goto_modelt &goto_model,
   message_handlert &message_handler,
   remove_exceptions_typest type)
 {
-  const namespacet ns(symbol_table);
+  const namespacet ns(goto_model.symbol_table);
   std::map<irep_idt, std::set<irep_idt>> exceptions_map;
-  uncaught_exceptions(goto_functions, ns, exceptions_map);
+  uncaught_exceptions(goto_model.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,
+    goto_model.symbol_table,
     function_may_throw,
     type == remove_exceptions_typest::REMOVE_ADDED_INSTANCEOF,
+    goto_model.get_analysis_cache().get_or_create<class_hierarchyt>(
+      goto_model.symbol_table),
     message_handler);
-  remove_exceptions(goto_functions);
+  remove_exceptions(goto_model.goto_functions);
 }
 
 /// removes throws/CATCH-POP/CATCH-PUSH from a single GOTO program, replacing
@@ -601,37 +611,30 @@ void remove_exceptions(
 /// 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 goto_model_function: function to remove exceptions from.
+///   The `@inflight_exception` global may be added to its associated symbol
+///   table 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,
+  goto_model_functiont &goto_model_function,
   message_handlert &message_handler,
   remove_exceptions_typest type)
 {
   remove_exceptionst::function_may_throwt any_function_may_throw =
     [](const irep_idt &) { return true; };
 
+  auto &symbol_table = goto_model_function.get_symbol_table();
+
   remove_exceptionst remove_exceptions(
     symbol_table,
     any_function_may_throw,
     type == remove_exceptions_typest::REMOVE_ADDED_INSTANCEOF,
+    goto_model_function.get_analysis_cache().get_or_create<class_hierarchyt>(
+      symbol_table),
     message_handler);
-  remove_exceptions(goto_program);
-}
-
-/// removes throws/CATCH-POP/CATCH-PUSH
-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, message_handler, type);
+  remove_exceptions(goto_model_function.get_goto_function().body);
 }

jbmc/src/java_bytecode/remove_exceptions.h

@@ -32,8 +32,7 @@ enum class remove_exceptions_typest
 };
 
 void remove_exceptions(
-  goto_programt &goto_program,
-  symbol_table_baset &symbol_table,
+  goto_model_functiont &goto_model_function,
   message_handlert &message_handler,
   remove_exceptions_typest type =
     remove_exceptions_typest::DONT_REMOVE_INSTANCEOF);

jbmc/src/java_bytecode/remove_instanceof.cpp

@@ -11,7 +11,6 @@ Author: Chris Smowton, [email protected]
 
 #include "remove_instanceof.h"
 
-#include <goto-programs/class_hierarchy.h>
 #include <goto-programs/class_identifier.h>
 #include <goto-programs/goto_convert.h>
 
@@ -24,12 +23,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),
+      ns(symbol_table),
+      class_hierarchy(class_hierarchy),
+      message_handler(message_handler)
   {
-    class_hierarchy(symbol_table);
   }
 
   // Lower instanceof for a single function
@@ -41,7 +42,7 @@ class remove_instanceoft
 protected:
   symbol_table_baset &symbol_table;
   namespacet ns;
-  class_hierarchyt class_hierarchy;
+  const class_hierarchyt &class_hierarchy;
   message_handlert &message_handler;
 
   bool lower_instanceof(
@@ -245,44 +246,30 @@ 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);
 }
 
 /// Replace every instanceof in the passed function with an explicit
 /// class-identifier test.
-/// \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.
+/// \remarks Extra auxiliary variables may be introduced into
+///   goto_model_function's symbol_table.
+/// \param goto_model_function: The function to work on.
 /// \param message_handler: logging output
 void remove_instanceof(
-  goto_functionst::goto_functiont &function,
-  symbol_table_baset &symbol_table,
+  goto_model_functiont &goto_model_function,
   message_handlert &message_handler)
 {
-  remove_instanceoft rem(symbol_table, message_handler);
-  rem.lower_instanceof(function.body);
-}
+  symbol_table_baset &symbol_table = goto_model_function.get_symbol_table();
+  const class_hierarchyt &class_hierarchy(
+    goto_model_function.get_analysis_cache().get_or_create<class_hierarchyt>(
+      symbol_table));
 
-/// Replace every instanceof in every function with an explicit
-/// class-identifier test.
-/// \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,
-  message_handlert &message_handler)
-{
-  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;
-  if(changed)
-    goto_functions.compute_location_numbers();
+  remove_instanceoft rem(symbol_table, class_hierarchy, message_handler);
+  rem.lower_instanceof(goto_model_function.get_goto_function().body);
 }
 
 /// Replace every instanceof in every function with an explicit
@@ -295,6 +282,14 @@ void remove_instanceof(
   goto_modelt &goto_model,
   message_handlert &message_handler)
 {
-  remove_instanceof(
-    goto_model.goto_functions, goto_model.symbol_table, message_handler);
+  const class_hierarchyt &class_hierarchy(
+    goto_model.get_analysis_cache().get_or_create<class_hierarchyt>(
+      goto_model.symbol_table));
+  remove_instanceoft rem(
+    goto_model.symbol_table, class_hierarchy, message_handler);
+  bool changed=false;
+  for(auto &f : goto_model.goto_functions.function_map)
+    changed=rem.lower_instanceof(f.second.body) || changed;
+  if(changed)
+    goto_model.goto_functions.compute_location_numbers();
 }

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,16 +90,15 @@ 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,
+  goto_model_functiont &goto_model_function,
   message_handlert &);
 
 void remove_instanceof(
-  goto_functionst &goto_functions,
-  symbol_table_baset &symbol_table,
+  goto_modelt &goto_model,
   message_handlert &);
 
 void remove_instanceof(goto_modelt &model, message_handlert &);

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -702,7 +702,7 @@ void jbmc_parse_optionst::process_goto_function(
   try
   {
     // Removal of RTTI inspection:
-    remove_instanceof(goto_function, symbol_table, get_message_handler());
+    remove_instanceof(function, get_message_handler());
     // Java virtual functions -> explicit dispatch tables:
     remove_virtual_functions(function);
 
@@ -714,8 +714,7 @@ void jbmc_parse_optionst::process_goto_function(
       // the results are slightly worse than running it in whole-program mode
       // (e.g. dead catch sites will be retained)
       remove_exceptions(
-        goto_function.body,
-        symbol_table,
+        function,
         get_message_handler(),
         remove_exceptions_typest::REMOVE_ADDED_INSTANCEOF);
     }

jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp

@@ -136,12 +136,17 @@ void load_and_test_method(
   goto_functionst::goto_functiont &goto_function =
     functions.function_map.at(function_name);
 
+  wrapper_goto_modelt goto_model(symbol_table, functions);
   goto_model_functiont model_function(
-    symbol_table, functions, function_name, goto_function);
+    symbol_table,
+    functions,
+    function_name,
+    goto_function,
+    goto_model.get_analysis_cache());
 
   // Emulate some of the passes that we'd normally do before replace_java_nondet
   // is called.
-  remove_instanceof(goto_function, symbol_table, null_message_handler);
+  remove_instanceof(model_function, null_message_handler);
 
   remove_virtual_functions(model_function);
 
@@ -292,4 +297,4 @@ SCENARIO(
     //      load_and_test_method("replaceNondetReturnUnboxed:()I", functions, symbol_table);
     //    }
   }
-}
+}

src/goto-programs/abstract_goto_model.h

@@ -13,6 +13,7 @@ Author: Diffblue Ltd.
 #define CPROVER_GOTO_PROGRAMS_ABSTRACT_GOTO_MODEL_H
 
 #include "goto_functions.h"
+#include <util/object_cache.h>
 #include <util/symbol_table.h>
 
 /// Abstract interface to eager or lazy GOTO models
@@ -49,6 +50,10 @@ class abstract_goto_modelt
   /// underneath them, so this should only be used to lend a reference to code
   /// that cannot also call get_goto_function.
   virtual const symbol_tablet &get_symbol_table() const = 0;
+
+  /// Accessor to get the analysis cache. Caches heavy-to-build data structures
+  /// in a place that can be accessible from any pass.
+  virtual object_cachet &get_analysis_cache() = 0;
 };
 
 #endif

src/goto-programs/class_hierarchy.h

@@ -59,6 +59,13 @@ class class_hierarchyt
   class_hierarchyt() = default;
   class_hierarchyt(const class_hierarchyt &) = delete;
   class_hierarchyt &operator=(const class_hierarchyt &) = delete;
+  class_hierarchyt(class_hierarchyt &&) = default;
+  class_hierarchyt &operator=(class_hierarchyt &&) = default;
+
+  explicit class_hierarchyt(const symbol_tablet &symbol_table)
+  {
+    (*this)(symbol_table);
+  }
 
   // transitively gets all children
   idst get_children_trans(const irep_idt &id) const