Add move insert to symbol_table

Make insertions strong exception-safe
Use emplace instead of insert

Author: NathanJPhillips

src/java_bytecode/java_utils.cpp

@@ -86,9 +86,9 @@ void generate_class_stub(
   new_symbol.mode=ID_java;
   new_symbol.is_type=true;
 
-  symbolt *class_symbol;
+  auto res=symbol_table.insert(std::move(new_symbol));
 
-  if(symbol_table.move(new_symbol, class_symbol))
+  if(!res)
   {
     messaget message(message_handler);
     message.warning() <<
@@ -99,7 +99,7 @@ void generate_class_stub(
   else
   {
     // create the class identifier etc
-    java_root_class(*class_symbol);
+    java_root_class(*res);
   }
 }
 

src/util/fresh_symbol.cpp

@@ -29,27 +29,22 @@ symbolt &get_fresh_aux_symbol(
 {
   static size_t temporary_counter=0;
   auxiliary_symbolt new_symbol;
-  symbolt *symbol_ptr;
 
-  do
+  optionalt<std::reference_wrapper<symbolt>> res;
+  // Loop until find a name that doesn't clash with a non-auxilliary symbol
+  while(!res)
   {
     // Distinguish local variables with the same name
     new_symbol.base_name=
-      basename_prefix+
-      "$"+
-      std::to_string(++temporary_counter);
+      basename_prefix+"$"+std::to_string(++temporary_counter);
     if(name_prefix.empty())
       new_symbol.name=new_symbol.base_name;
     else
-      new_symbol.name=
-        name_prefix+
-        "::"+
-        id2string(new_symbol.base_name);
+      new_symbol.name=name_prefix+"::"+id2string(new_symbol.base_name);
     new_symbol.type=type;
     new_symbol.location=source_location;
     new_symbol.mode=symbol_mode;
+    res=symbol_table.insert(std::move(new_symbol));
   }
-  while(symbol_table.move(new_symbol, symbol_ptr));
-
-  return *symbol_ptr;
+  return *res;
 }

src/util/symbol_table.cpp

@@ -16,17 +16,31 @@ Author: Daniel Kroening, [email protected]
 ///   there is a symbol with the same name already in the symbol table.
 bool symbol_tablet::add(const symbolt &symbol)
 {
-  if(!symbols.insert(std::pair<irep_idt, symbolt>(symbol.name, symbol)).second)
+  std::pair<symbolst::iterator, bool> result=
+    symbols.emplace(symbol.name, symbol);
+  if(!result.second)
     return true;
-
-  symbol_base_map.insert(
-    std::pair<irep_idt, irep_idt>(symbol.base_name, symbol.name));
-  symbol_module_map.insert(
-    std::pair<irep_idt, irep_idt>(symbol.module, symbol.name));
-
+  add_base_and_module(result.first);
   return false;
 }
 
+/// Move a new symbol to the symbol table
+/// \remark: This is a nicer interface than move but achieves the same result
+/// \param symbol: The symbol to be added to the symbol table
+/// \return Returns an optional reference to the newly inserted symbol, without
+///   a value if a symbol with the same name already exists in the symbol table
+optionalt<std::reference_wrapper<symbolt>> symbol_tablet::insert(
+  symbolt &&symbol)
+{
+  // Add the symbol to the table or retrieve existing symbol with the same name
+  std::pair<symbolst::iterator, bool> result=
+    symbols.emplace(symbol.name, std::move(symbol));
+  if(!result.second)
+    return optionalt<std::reference_wrapper<symbolt>>();
+  add_base_and_module(result.first);
+  return std::ref(result.first->second);
+}
+
 /// Move a symbol into the symbol table. If there is already a symbol with the
 /// same name then symbol is unchanged, new_symbol points to the symbol with the
 /// same name and true is returned. Otherwise, the symbol is moved into the
@@ -55,17 +69,41 @@ bool symbol_tablet::move(symbolt &symbol, symbolt *&new_symbol)
     return true;
   }
 
-  symbol_base_map.emplace(symbol.base_name, symbol.name);
-  symbol_module_map.emplace(symbol.module, symbol.name);
-
   // Move the provided symbol into the symbol table
   result.first->second.swap(symbol);
+
+  add_base_and_module(result.first);
+
   // Return the address of the new symbol in the table
   new_symbol=&result.first->second;
 
   return false;
 }
 
+void symbol_tablet::add_base_and_module(symbolst::iterator added_symbol)
+{
+  symbolt &symbol=added_symbol->second;
+  try
+  {
+    symbol_base_mapt::iterator base_result=
+      symbol_base_map.emplace(symbol.base_name, symbol.name);
+    try
+    {
+      symbol_module_map.emplace(symbol.module, symbol.name);
+    }
+    catch(...)
+    {
+      symbol_base_map.erase(base_result);
+      throw;
+    }
+  }
+  catch(...)
+  {
+    symbols.erase(added_symbol);
+    throw;
+  }
+}
+
 /// Remove a symbol from the symbol table
 /// \param name: The name of the symbol to remove
 /// \return Returns a boolean indicating whether the process failed

src/util/symbol_table.h

@@ -23,6 +23,8 @@ Author: Daniel Kroening, [email protected]
 #include <map>
 #include <unordered_map>
 
+#include <util/optional.h>
+
 #include "symbol.h"
 
 #define forall_symbols(it, expr) \
@@ -60,12 +62,15 @@ class symbol_tablet
 
   bool add(const symbolt &symbol);
 
+  optionalt<std::reference_wrapper<symbolt>> insert(symbolt &&symbol);
   bool move(symbolt &symbol, symbolt *&new_symbol);
-
   // this will go away, use add instead
   bool move(symbolt &symbol)
   { symbolt *new_symbol; return move(symbol, new_symbol); }
+private:
+  void add_base_and_module(symbolst::iterator added_symbol);
 
+public:
   void clear()
   {
     symbols.clear();