From 544fdf9d76692338687c50ea8b8b4e1262b6316b Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Sun, 26 Dec 2021 16:25:52 +0000
Subject: [PATCH] Linking: do not modify source symbol table

This makes the interface more intuitive and ensures that we do not leave
behind an inconsistent symbol table.
---
 src/linking/linking.cpp     | 29 ++++++++++++++++++-----------
 src/linking/linking.h       |  9 ++++-----
 src/linking/linking_class.h | 11 ++++++-----
 3 files changed, 28 insertions(+), 21 deletions(-)

diff --git a/src/linking/linking.cpp b/src/linking/linking.cpp
index b2f36405b8b..652eae1169f 100644
--- a/src/linking/linking.cpp
+++ b/src/linking/linking.cpp
@@ -421,7 +421,7 @@ void linkingt::link_warning(
             << type_to_string_verbose(new_symbol) << eom;
 }
 
-irep_idt linkingt::rename(const irep_idt id)
+irep_idt linkingt::rename(const irep_idt &id)
 {
   unsigned cnt=0;
 
@@ -1313,14 +1313,15 @@ void linkingt::do_type_dependencies(
   }
 }
 
-void linkingt::rename_symbols(
+std::unordered_map<irep_idt, irep_idt> linkingt::rename_symbols(
   const std::unordered_set<irep_idt> &needs_to_be_renamed)
 {
+  std::unordered_map<irep_idt, irep_idt> new_identifiers;
   namespacet src_ns(src_symbol_table);
 
   for(const irep_idt &id : needs_to_be_renamed)
   {
-    symbolt &new_symbol = src_symbol_table.get_writeable_ref(id);
+    const symbolt &new_symbol = src_ns.lookup(id);
 
     irep_idt new_identifier;
 
@@ -1329,21 +1330,24 @@ void linkingt::rename_symbols(
     else
       new_identifier=rename(id);
 
-    new_symbol.name=new_identifier;
+    new_identifiers.emplace(id, new_identifier);
 
-    #ifdef DEBUG
+#ifdef DEBUG
     debug() << "LINKING: renaming " << id << " to "
             << new_identifier << eom;
-    #endif
+#endif
 
     if(new_symbol.is_type)
       rename_symbol.insert_type(id, new_identifier);
     else
       rename_symbol.insert_expr(id, new_identifier);
   }
+
+  return new_identifiers;
 }
 
-void linkingt::copy_symbols()
+void linkingt::copy_symbols(
+  const std::unordered_map<irep_idt, irep_idt> &new_identifiers)
 {
   std::map<irep_idt, symbolt> src_symbols;
   // First apply the renaming
@@ -1353,7 +1357,10 @@ void linkingt::copy_symbols()
     // apply the renaming
     rename_symbol(symbol.type);
     rename_symbol(symbol.value);
-    // Add to vector
+    auto it = new_identifiers.find(named_symbol.first);
+    if(it != new_identifiers.end())
+      symbol.name = it->second;
+
     src_symbols.emplace(named_symbol.first, std::move(symbol));
   }
 
@@ -1435,15 +1442,15 @@ void linkingt::typecheck()
   do_type_dependencies(needs_to_be_renamed);
 
   // PHASE 2: actually rename them
-  rename_symbols(needs_to_be_renamed);
+  auto new_identifiers = rename_symbols(needs_to_be_renamed);
 
   // PHASE 3: copy new symbols to main table
-  copy_symbols();
+  copy_symbols(new_identifiers);
 }
 
 bool linking(
   symbol_tablet &dest_symbol_table,
-  symbol_tablet &new_symbol_table,
+  const symbol_tablet &new_symbol_table,
   message_handlert &message_handler)
 {
   linkingt linking(
diff --git a/src/linking/linking.h b/src/linking/linking.h
index b607a6aa805..672c79ee502 100644
--- a/src/linking/linking.h
+++ b/src/linking/linking.h
@@ -15,13 +15,12 @@ Author: Daniel Kroening, kroening@kroening.com
 class message_handlert;
 class symbol_tablet;
 
-// This merges the symbol table "new_symbol_table" into "dest_symbol_table",
-// applying appropriate renamings to symbols in "new_symbol_table"
-// when necessary.
-
+/// Merges the symbol table \p new_symbol_table into \p dest_symbol_table,
+/// renaming symbols from \p new_symbol_table when necessary.
+/// \return True, iff linking failed with unresolvable conflicts.
 bool linking(
   symbol_tablet &dest_symbol_table,
-  symbol_tablet &new_symbol_table,
+  const symbol_tablet &new_symbol_table,
   message_handlert &message_handler);
 
 #endif // CPROVER_LINKING_LINKING_H
diff --git a/src/linking/linking_class.h b/src/linking/linking_class.h
index f157770fe95..c445fb1dc94 100644
--- a/src/linking/linking_class.h
+++ b/src/linking/linking_class.h
@@ -30,7 +30,7 @@ class linkingt:public typecheckt
 public:
   linkingt(
     symbol_table_baset &_main_symbol_table,
-    symbol_table_baset &_src_symbol_table,
+    const symbol_table_baset &_src_symbol_table,
     message_handlert &_message_handler)
     : typecheckt(_message_handler),
       main_symbol_table(_main_symbol_table),
@@ -65,8 +65,9 @@ class linkingt:public typecheckt
 
   void do_type_dependencies(std::unordered_set<irep_idt> &);
 
-  void rename_symbols(const std::unordered_set<irep_idt> &needs_to_be_renamed);
-  void copy_symbols();
+  std::unordered_map<irep_idt, irep_idt>
+  rename_symbols(const std::unordered_set<irep_idt> &needs_to_be_renamed);
+  void copy_symbols(const std::unordered_map<irep_idt, irep_idt> &);
 
   void duplicate_non_type_symbol(
     symbolt &old_symbol,
@@ -169,14 +170,14 @@ class linkingt:public typecheckt
     const struct_typet &new_type);
 
   symbol_table_baset &main_symbol_table;
-  symbol_table_baset &src_symbol_table;
+  const symbol_table_baset &src_symbol_table;
 
   namespacet ns;
 
   // X -> Y iff Y uses X for new symbol type IDs X and Y
   typedef std::unordered_map<irep_idt, std::unordered_set<irep_idt>> used_byt;
 
-  irep_idt rename(irep_idt);
+  irep_idt rename(const irep_idt &);
 
   // the new IDs created by renaming
   std::unordered_set<irep_idt> renamed_ids;