Declare a lazy_class_to_declared_symbols_mapt class

This is to avoid computing the map several times and make sure it is
never computed if it is not actually needed.

Author: romainbrenguier

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -112,6 +112,23 @@ static prefix_filtert get_context(const optionst &options)
   return prefix_filtert(std::move(context_include), std::move(context_exclude));
 }
 
+std::unordered_multimap<irep_idt, symbolt> &
+lazy_class_to_declared_symbols_mapt::get(const symbol_tablet &symbol_table)
+{
+  if(!initialized)
+  {
+    map = class_to_declared_symbols(symbol_table);
+    initialized = true;
+  }
+  return map;
+}
+
+void lazy_class_to_declared_symbols_mapt::reinitialize()
+{
+  initialized = false;
+  map.clear();
+}
+
 /// Consume options that are java bytecode specific.
 void java_bytecode_languaget::set_language_options(const optionst &options)
 {
@@ -995,12 +1012,17 @@ bool java_bytecode_languaget::do_ci_lazy_method_conversion(
   symbol_table_buildert symbol_table_builder =
     symbol_table_buildert::wrap(symbol_table);
 
+  lazy_class_to_declared_symbols_mapt class_to_declared_symbols;
+
   const method_convertert method_converter =
-    [this, &symbol_table_builder](
+    [this, &symbol_table_builder, &class_to_declared_symbols](
       const irep_idt &function_id,
       ci_lazy_methods_neededt lazy_methods_needed) {
       return convert_single_method(
-        function_id, symbol_table_builder, std::move(lazy_methods_needed));
+        function_id,
+        symbol_table_builder,
+        std::move(lazy_methods_needed),
+        class_to_declared_symbols);
     };
 
   ci_lazy_methodst method_gather(
@@ -1134,7 +1156,8 @@ static void notify_static_method_calls(
 bool java_bytecode_languaget::convert_single_method(
   const irep_idt &function_id,
   symbol_table_baset &symbol_table,
-  optionalt<ci_lazy_methods_neededt> needed_lazy_methods)
+  optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
+  lazy_class_to_declared_symbols_mapt &class_to_declared_symbols)
 {
   // Do not convert if method is not in context
   if(method_in_context && !(*method_in_context)(id2string(function_id)))
@@ -1212,16 +1235,14 @@ bool java_bytecode_languaget::convert_single_method(
         class_name, "user_specified_clinit must be declared by a class.");
       INVARIANT(
         static_values_json.has_value(), "static-values JSON must be available");
-      const auto class_to_declared_symbols_map =
-        class_to_declared_symbols(symbol_table);
       writable_symbol.value = get_user_specified_clinit_body(
         *class_name,
         *static_values_json,
         symbol_table,
         needed_lazy_methods,
         max_user_array_length,
         references,
-        class_to_declared_symbols_map);
+        class_to_declared_symbols.get(symbol_table));
       break;
     }
     case synthetic_method_typet::STUB_CLASS_STATIC_INITIALIZER:

jbmc/src/java_bytecode/java_bytecode_language.h

@@ -115,6 +115,30 @@ enum lazy_methods_modet
   LAZY_METHODS_MODE_EXTERNAL_DRIVER
 };
 
+/// Map classes to the symbols they declare but is only computed once it is
+/// needed and the map is then kept.
+/// Note that it only includes function and field symbols (and not for example,
+/// local variables), these are produced in the convert-class phase.
+/// Calling `get` before the symbol table is properly filled with these symbols,
+/// would make later calls return an outdated map. The
+/// lazy_class_to_declared_symbols_mapt would then need to be reinitialized.
+/// Similarly if some transformation creates or deletes function or field
+/// symbols the map would get out of date and would need to be reinitialized.
+class lazy_class_to_declared_symbols_mapt
+{
+public:
+  lazy_class_to_declared_symbols_mapt() = default;
+
+  std::unordered_multimap<irep_idt, symbolt> &
+  get(const symbol_tablet &symbol_table);
+
+  void reinitialize();
+
+private:
+  bool initialized = false;
+  std::unordered_multimap<irep_idt, symbolt> map;
+};
+
 #define JAVA_CLASS_MODEL_SUFFIX "@class_model"
 
 class java_bytecode_languaget:public languaget
@@ -201,13 +225,18 @@ class java_bytecode_languaget:public languaget
     const irep_idt &function_id,
     symbol_table_baset &symbol_table)
   {
+    lazy_class_to_declared_symbols_mapt class_to_declared_symbols{};
     convert_single_method(
-      function_id, symbol_table, optionalt<ci_lazy_methods_neededt>());
+      function_id,
+      symbol_table,
+      optionalt<ci_lazy_methods_neededt>(),
+      class_to_declared_symbols);
   }
   bool convert_single_method(
     const irep_idt &function_id,
     symbol_table_baset &symbol_table,
-    optionalt<ci_lazy_methods_neededt> needed_lazy_methods);
+    optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
+    lazy_class_to_declared_symbols_mapt &class_to_declared_symbols);
 
   bool do_ci_lazy_method_conversion(symbol_tablet &);
   const select_pointer_typet &get_pointer_type_selector() const;