Merge pull request diffblue#3296 from JohnDumbell/jd/enhancement/find_free_suffix_improvement

Adding smallest_unused_suffix cache

Author: tautschnig

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -19,6 +19,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/string2int.h>
 #include <util/suffix.h>
 #include <util/symbol_table.h>
+#include <util/symbol_table_builder.h>
 
 #include <json/json_parser.h>
 
@@ -790,8 +791,11 @@ bool java_bytecode_languaget::typecheck(
       break;
     case LAZY_METHODS_MODE_EAGER:
       {
+        symbol_table_buildert symbol_table_builder =
+          symbol_table_buildert::wrap(symbol_table);
+
         journalling_symbol_tablet journalling_symbol_table =
-          journalling_symbol_tablet::wrap(symbol_table);
+          journalling_symbol_tablet::wrap(symbol_table_builder);
 
         // Convert all synthetic methods:
         for(const auto &function_id_and_type : synthetic_methods)
@@ -842,18 +846,21 @@ bool java_bytecode_languaget::generate_support_functions(
 {
   PRECONDITION(language_options_initialized);
 
+  symbol_table_buildert symbol_table_builder =
+    symbol_table_buildert::wrap(symbol_table);
+
   main_function_resultt res=
     get_main_symbol(symbol_table, main_class, get_message_handler());
   if(!res.is_success())
     return res.is_error();
 
   // Load the main function into the symbol table to get access to its
   // parameter names
-  convert_lazy_method(res.main_function.name, symbol_table);
+  convert_lazy_method(res.main_function.name, symbol_table_builder);
 
   // generate the test harness in __CPROVER__start and a call the entry point
   return java_entry_point(
-    symbol_table,
+    symbol_table_builder,
     main_class,
     get_message_handler(),
     assume_inputs_non_null,
@@ -880,12 +887,15 @@ bool java_bytecode_languaget::do_ci_lazy_method_conversion(
   symbol_tablet &symbol_table,
   method_bytecodet &method_bytecode)
 {
+  symbol_table_buildert symbol_table_builder =
+    symbol_table_buildert::wrap(symbol_table);
+
   const method_convertert method_converter =
-    [this, &symbol_table]
-      (const irep_idt &function_id, ci_lazy_methods_neededt lazy_methods_needed)
-    {
+    [this, &symbol_table_builder](
+      const irep_idt &function_id,
+      ci_lazy_methods_neededt lazy_methods_needed) {
       return convert_single_method(
-        function_id, symbol_table, std::move(lazy_methods_needed));
+        function_id, symbol_table_builder, std::move(lazy_methods_needed));
     };
 
   ci_lazy_methodst method_gather(

src/goto-cc/compile.cpp

@@ -22,6 +22,7 @@ Date: June 2006
 #include <util/file_util.h>
 #include <util/get_base_name.h>
 #include <util/suffix.h>
+#include <util/symbol_table_builder.h>
 #include <util/tempdir.h>
 #include <util/unicode.h>
 #include <util/version.h>
@@ -697,37 +698,40 @@ void compilet::add_compiler_specific_defines(configt &config) const
 
 void compilet::convert_symbols(goto_functionst &dest)
 {
+  symbol_table_buildert symbol_table_builder =
+    symbol_table_buildert::wrap(goto_model.symbol_table);
+
   goto_convert_functionst converter(
-    goto_model.symbol_table, get_message_handler());
+    symbol_table_builder, get_message_handler());
 
   // the compilation may add symbols!
 
   symbol_tablet::symbolst::size_type before=0;
 
-  while(before != goto_model.symbol_table.symbols.size())
+  while(before != symbol_table_builder.symbols.size())
   {
-    before = goto_model.symbol_table.symbols.size();
+    before = symbol_table_builder.symbols.size();
 
     typedef std::set<irep_idt> symbols_sett;
     symbols_sett symbols;
 
-    for(const auto &named_symbol : goto_model.symbol_table.symbols)
+    for(const auto &named_symbol : symbol_table_builder.symbols)
       symbols.insert(named_symbol.first);
 
     // the symbol table iterators aren't stable
     for(const auto &symbol : symbols)
     {
       symbol_tablet::symbolst::const_iterator s_it =
-        goto_model.symbol_table.symbols.find(symbol);
-      CHECK_RETURN(s_it != goto_model.symbol_table.symbols.end());
+        symbol_table_builder.symbols.find(symbol);
+      CHECK_RETURN(s_it != symbol_table_builder.symbols.end());
 
       if(
         s_it->second.is_function() && !s_it->second.is_compiled() &&
         s_it->second.value.is_not_nil())
       {
         debug() << "Compiling " << s_it->first << eom;
         converter.convert_function(s_it->first, dest.function_map[s_it->first]);
-        goto_model.symbol_table.get_writeable_ref(symbol).set_compiled();
+        symbol_table_builder.get_writeable_ref(symbol).set_compiled();
       }
     }
   }

src/goto-programs/goto_convert.cpp

@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
 #include "goto_convert.h"
 
 #include <util/arith_tools.h>
+#include <util/c_types.h>
 #include <util/cprover_prefix.h>
 #include <util/exception_utils.h>
 #include <util/expr_util.h>
@@ -20,8 +21,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/simplify_expr.h>
 #include <util/std_expr.h>
 #include <util/symbol_table.h>
-
-#include <util/c_types.h>
+#include <util/symbol_table_builder.h>
 
 #include "goto_convert_class.h"
 #include "destructor.h"
@@ -1939,7 +1939,9 @@ void goto_convert(
   message_handlert &message_handler,
   const irep_idt &mode)
 {
-  goto_convertt goto_convert(symbol_table, message_handler);
+  symbol_table_buildert symbol_table_builder =
+    symbol_table_buildert::wrap(symbol_table);
+  goto_convertt goto_convert(symbol_table_builder, message_handler);
   goto_convert.goto_convert(code, dest, mode);
 }
 

src/goto-programs/goto_convert_functions.cpp

@@ -11,10 +11,11 @@ Date: June 2003
 #include "goto_convert_functions.h"
 
 #include <util/base_type.h>
+#include <util/fresh_symbol.h>
+#include <util/prefix.h>
 #include <util/std_code.h>
 #include <util/symbol_table.h>
-#include <util/prefix.h>
-#include <util/fresh_symbol.h>
+#include <util/symbol_table_builder.h>
 
 #include "goto_inline.h"
 
@@ -217,18 +218,23 @@ void goto_convert(
   goto_modelt &goto_model,
   message_handlert &message_handler)
 {
+  symbol_table_buildert symbol_table_builder =
+    symbol_table_buildert::wrap(goto_model.symbol_table);
+
   goto_convert(
-    goto_model.symbol_table,
-    goto_model.goto_functions,
-    message_handler);
+    symbol_table_builder, goto_model.goto_functions, message_handler);
 }
 
 void goto_convert(
   symbol_table_baset &symbol_table,
   goto_functionst &functions,
   message_handlert &message_handler)
 {
-  goto_convert_functionst goto_convert_functions(symbol_table, message_handler);
+  symbol_table_buildert symbol_table_builder =
+    symbol_table_buildert::wrap(symbol_table);
+
+  goto_convert_functionst goto_convert_functions(
+    symbol_table_builder, message_handler);
 
   goto_convert_functions.goto_convert(functions);
 }
@@ -239,7 +245,11 @@ void goto_convert(
   goto_functionst &functions,
   message_handlert &message_handler)
 {
-  goto_convert_functionst goto_convert_functions(symbol_table, message_handler);
+  symbol_table_buildert symbol_table_builder =
+    symbol_table_buildert::wrap(symbol_table);
+
+  goto_convert_functionst goto_convert_functions(
+    symbol_table_builder, message_handler);
 
   goto_convert_functions.convert_function(
     identifier, functions.function_map[identifier]);

src/goto-programs/lazy_goto_functions_map.h

@@ -11,9 +11,10 @@
 #include "goto_functions.h"
 #include "goto_convert_functions.h"
 
-#include <util/message.h>
 #include <langapi/language_file.h>
 #include <util/journalling_symbol_table.h>
+#include <util/message.h>
+#include <util/symbol_table_builder.h>
 
 /// Provides a wrapper for a map of lazily loaded goto_functiont.
 /// This incrementally builds a goto-functions object, while permitting
@@ -142,8 +143,11 @@ class lazy_goto_functions_mapt final
   // const first
   reference ensure_function_loaded_internal(const key_type &name) const
   {
+    symbol_table_buildert symbol_table_builder =
+      symbol_table_buildert::wrap(symbol_table);
+
     journalling_symbol_tablet journalling_table =
-      journalling_symbol_tablet::wrap(symbol_table);
+      journalling_symbol_tablet::wrap(symbol_table_builder);
     reference named_function=ensure_entry_converted(name, journalling_table);
     mapped_type function=named_function.second;
     if(processed_functions.count(name)==0)

src/jsil/jsil_typecheck.h

@@ -14,9 +14,10 @@ Author: Michael Tautschnig, [email protected]
 
 #include <unordered_set>
 
-#include <util/typecheck.h>
 #include <util/namespace.h>
 #include <util/std_code.h>
+#include <util/symbol_table_base.h>
+#include <util/typecheck.h>
 
 class symbol_exprt;
 class codet;
@@ -34,12 +35,12 @@ class jsil_typecheckt:public typecheckt
 {
 public:
   jsil_typecheckt(
-    symbol_tablet &_symbol_table,
-    message_handlert &_message_handler):
-    typecheckt(_message_handler),
-    symbol_table(_symbol_table),
-    ns(symbol_table),
-    proc_name()
+    symbol_table_baset &_symbol_table,
+    message_handlert &_message_handler)
+    : typecheckt(_message_handler),
+      symbol_table(_symbol_table),
+      ns(symbol_table),
+      proc_name()
   {
   }
 
@@ -49,7 +50,7 @@ class jsil_typecheckt:public typecheckt
   virtual void typecheck_expr(exprt &expr);
 
 protected:
-  symbol_tablet &symbol_table;
+  symbol_table_baset &symbol_table;
   const namespacet ns;
   // prefix to variables which is set in typecheck_declaration
   irep_idt proc_name;

src/linking/linking_class.h

@@ -28,13 +28,13 @@ class linkingt:public typecheckt
 {
 public:
   linkingt(
-    symbol_tablet &_main_symbol_table,
-    symbol_tablet &_src_symbol_table,
-    message_handlert &_message_handler):
-    typecheckt(_message_handler),
-    main_symbol_table(_main_symbol_table),
-    src_symbol_table(_src_symbol_table),
-    ns(_main_symbol_table)
+    symbol_table_baset &_main_symbol_table,
+    symbol_table_baset &_src_symbol_table,
+    message_handlert &_message_handler)
+    : typecheckt(_message_handler),
+      main_symbol_table(_main_symbol_table),
+      src_symbol_table(_src_symbol_table),
+      ns(_main_symbol_table)
   {
   }
 
@@ -167,8 +167,8 @@ class linkingt:public typecheckt
     const struct_typet &old_type,
     const struct_typet &new_type);
 
-  symbol_tablet &main_symbol_table;
-  symbol_tablet &src_symbol_table;
+  symbol_table_baset &main_symbol_table;
+  symbol_table_baset &src_symbol_table;
 
   namespacet ns;
 

src/util/journalling_symbol_table.h

@@ -100,6 +100,11 @@ class journalling_symbol_tablet : public symbol_table_baset
     return result;
   }
 
+  std::size_t next_unused_suffix(const std::string &prefix) const override
+  {
+    return base_symbol_table.next_unused_suffix(prefix);
+  }
+
   virtual std::pair<symbolt &, bool> insert(symbolt symbol) override
   {
     std::pair<symbolt &, bool> result =

src/util/namespace.cpp

@@ -19,24 +19,6 @@ Author: Daniel Kroening, [email protected]
 #include "string2int.h"
 #include "symbol_table.h"
 
-/// Find smallest unused integer i so that prefix + std::to_string(i)
-/// does not exist in the list \p symbols.
-/// \param prefix: A string denoting the prefix we want to find the
-///   smallest suffix of.
-/// \param symbols: The list of symbols we look in for.
-/// \return The small unused suffix size.
-static std::size_t smallest_unused_suffix(
-  const std::string &prefix,
-  const symbol_tablet::symbolst &symbols)
-{
-  std::size_t max_nr = 0;
-
-  while(symbols.find(prefix + std::to_string(max_nr)) != symbols.end())
-    ++max_nr;
-
-  return max_nr;
-}
-
 namespace_baset::~namespace_baset()
 {
 }
@@ -168,10 +150,10 @@ std::size_t namespacet::smallest_unused_suffix(const std::string &prefix) const
   std::size_t m = 0;
 
   if(symbol_table1!=nullptr)
-    m = std::max(m, ::smallest_unused_suffix(prefix, symbol_table1->symbols));
+    m = std::max(m, symbol_table1->next_unused_suffix(prefix));
 
   if(symbol_table2!=nullptr)
-    m = std::max(m, ::smallest_unused_suffix(prefix, symbol_table2->symbols));
+    m = std::max(m, symbol_table2->next_unused_suffix(prefix));
 
   return m;
 }
@@ -221,7 +203,7 @@ multi_namespacet::smallest_unused_suffix(const std::string &prefix) const
   std::size_t m = 0;
 
   for(const auto &st : symbol_table_list)
-    m = std::max(m, ::smallest_unused_suffix(prefix, st->symbols));
+    m = std::max(m, st->next_unused_suffix(prefix));
 
   return m;
 }