Remove typecheckt interface from linkingt

There is no particular benefit in this inheritance. Also prepare for
maintaining state across multiple calls to the linker by making the
source symbol table an argument specific to each linking call.

Author: tautschnig

regression/cbmc/incomplete-structs/test.desc

@@ -1,9 +1,6 @@
 CORE new-smt-backend
 typesmain.c
 types1.c types2.c types3.c
-reason for conflict at \*#this.u: number of members is different \(3/0\)
-reason for conflict at \*#this.u: number of members is different \(0/3\)
-struct U   \(incomplete\)
 warning: pointer parameter types differ between declaration and definition "bar"
 warning: pointer parameter types differ between declaration and definition "foo"
 ^VERIFICATION SUCCESSFUL$

src/goto-programs/link_goto_model.cpp

@@ -10,16 +10,16 @@ Author: Michael Tautschnig, Daniel Kroening
 /// Link Goto Programs
 
 #include "link_goto_model.h"
+#include <linking/linking_class.h>
 
-#include <unordered_set>
-
-#include <util/symbol.h>
+#include <util/message.h>
 #include <util/rename_symbol.h>
-
-#include <linking/linking_class.h>
+#include <util/symbol.h>
 
 #include "goto_model.h"
 
+#include <unordered_set>
+
 static void rename_symbols_in_function(
   goto_functionst::goto_functiont &function,
   irep_idt &new_function_name,
@@ -119,9 +119,9 @@ optionalt<replace_symbolt::expr_mapt> link_goto_model(
       weak_symbols.insert(symbol_pair.first);
   }
 
-  linkingt linking(dest.symbol_table, src.symbol_table, message_handler);
+  linkingt linking(dest.symbol_table, message_handler);
 
-  if(linking.typecheck_main())
+  if(linking.link(src.symbol_table))
   {
     messaget log{message_handler};
     log.error() << "typechecking main failed" << messaget::eom;

src/linking/linking.cpp

@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/c_types.h>
 #include <util/find_symbols.h>
 #include <util/mathematical_types.h>
+#include <util/message.h>
 #include <util/pointer_expr.h>
 #include <util/pointer_offset_size.h>
 #include <util/simplify_expr.h>
@@ -201,7 +202,8 @@ bool linkingt::detailed_conflict_report_rec(
   bool conclusive = false;
 
 #ifdef DEBUG
-  debug() << "<BEGIN DEPTH " << depth << ">" << eom;
+  messaget log{message_handler};
+  log.debug() << "<BEGIN DEPTH " << depth << ">" << messaget::eom;
 #endif
 
   std::string msg;
@@ -455,18 +457,23 @@ bool linkingt::detailed_conflict_report_rec(
 
   if(conclusive && !msg.empty())
   {
-    error() << '\n';
-    error() << "reason for conflict at "
-            << expr_to_string(irep_idt(), conflict_path) << ": " << msg << '\n';
-
-    error() << '\n';
-    error() << type_to_string_verbose(old_symbol, t1) << '\n';
-    error() << type_to_string_verbose(new_symbol, t2) << '\n';
+#ifndef DEBUG
+    messaget log{message_handler};
+#endif
+    log.error() << '\n';
+    log.error() << "reason for conflict at "
+                << expr_to_string(irep_idt(), conflict_path) << ": " << msg
+                << '\n';
+
+    log.error() << '\n';
+    log.error() << type_to_string_verbose(old_symbol, t1) << '\n';
+    log.error() << type_to_string_verbose(new_symbol, t2) << '\n'
+                << messaget::eom;
   }
 
   #ifdef DEBUG
-  debug() << "<END DEPTH " << depth << ">" << eom;
-  #endif
+  log.debug() << "<END DEPTH " << depth << ">" << messaget::eom;
+#endif
 
   return conclusive;
 }
@@ -476,37 +483,39 @@ void linkingt::link_error(
     const symbolt &new_symbol,
     const std::string &msg)
 {
-  error().source_location=new_symbol.location;
-
-  error() << "error: " << msg << " '" << old_symbol.display_name() << "'"
-          << '\n';
-  error() << "old definition in module '" << old_symbol.module << "' "
-          << old_symbol.location << '\n'
-          << type_to_string_verbose(old_symbol) << '\n';
-  error() << "new definition in module '" << new_symbol.module << "' "
-          << new_symbol.location << '\n'
-          << type_to_string_verbose(new_symbol) << eom;
+  messaget log{message_handler};
+  log.error().source_location = new_symbol.location;
+
+  log.error() << "error: " << msg << " '" << old_symbol.display_name() << "'"
+              << '\n';
+  log.error() << "old definition in module '" << old_symbol.module << "' "
+              << old_symbol.location << '\n'
+              << type_to_string_verbose(old_symbol) << '\n';
+  log.error() << "new definition in module '" << new_symbol.module << "' "
+              << new_symbol.location << '\n'
+              << type_to_string_verbose(new_symbol) << messaget::eom;
 }
 
 void linkingt::link_warning(
     const symbolt &old_symbol,
     const symbolt &new_symbol,
     const std::string &msg)
 {
-  warning().source_location=new_symbol.location;
-
-  warning() << "warning: " << msg << " \""
-            << old_symbol.display_name()
-            << "\"" << '\n';
-  warning() << "old definition in module " << old_symbol.module << " "
-            << old_symbol.location << '\n'
-            << type_to_string_verbose(old_symbol) << '\n';
-  warning() << "new definition in module " << new_symbol.module << " "
-            << new_symbol.location << '\n'
-            << type_to_string_verbose(new_symbol) << eom;
+  messaget log{message_handler};
+  log.warning().source_location = new_symbol.location;
+
+  log.warning() << "warning: " << msg << " \"" << old_symbol.display_name()
+                << "\"" << '\n';
+  log.warning() << "old definition in module " << old_symbol.module << " "
+                << old_symbol.location << '\n'
+                << type_to_string_verbose(old_symbol) << '\n';
+  log.warning() << "new definition in module " << new_symbol.module << " "
+                << new_symbol.location << '\n'
+                << type_to_string_verbose(new_symbol) << messaget::eom;
 }
 
-irep_idt linkingt::rename(const irep_idt &id)
+irep_idt
+linkingt::rename(const symbol_table_baset &src_symbol_table, const irep_idt &id)
 {
   unsigned cnt=0;
 
@@ -738,11 +747,6 @@ void linkingt::duplicate_code_symbol(
           {
             warn_msg="pointer parameter types differ between "
                      "declaration and definition";
-            detailed_conflict_report(
-              old_symbol,
-              new_symbol,
-              conflicts.front().first,
-              conflicts.front().second);
           }
 
           replace=new_symbol.value.is_not_nil();
@@ -855,12 +859,12 @@ void linkingt::duplicate_code_symbol(
     else if(old_symbol.type == new_symbol.type)
     {
       // keep the one in old_symbol -- libraries come last!
-      debug().source_location = new_symbol.location;
-
-      debug() << "function '" << old_symbol.name << "' in module '"
-              << new_symbol.module
-              << "' is shadowed by a definition in module '"
-              << old_symbol.module << "'" << eom;
+      messaget log{message_handler};
+      log.debug().source_location = new_symbol.location;
+      log.debug() << "function '" << old_symbol.name << "' in module '"
+                  << new_symbol.module
+                  << "' is shadowed by a definition in module '"
+                  << old_symbol.module << "'" << messaget::eom;
     }
     else
       link_error(
@@ -1146,16 +1150,18 @@ void linkingt::duplicate_object_symbol(
       }
       else
       {
-        warning().source_location=new_symbol.location;
-
-        warning() << "warning: conflicting initializers for"
-                  << " variable \"" << old_symbol.name << "\"\n";
-        warning() << "using old value in module " << old_symbol.module << " "
-                  << old_symbol.value.find_source_location() << '\n'
-                  << expr_to_string(old_symbol.name, tmp_old) << '\n';
-        warning() << "ignoring new value in module " << new_symbol.module << " "
-                  << new_symbol.value.find_source_location() << '\n'
-                  << expr_to_string(new_symbol.name, tmp_new) << eom;
+        messaget log{message_handler};
+        log.warning().source_location = new_symbol.location;
+
+        log.warning() << "warning: conflicting initializers for"
+                      << " variable \"" << old_symbol.name << "\"\n";
+        log.warning() << "using old value in module " << old_symbol.module
+                      << " " << old_symbol.value.find_source_location() << '\n'
+                      << expr_to_string(old_symbol.name, tmp_old) << '\n';
+        log.warning() << "ignoring new value in module " << new_symbol.module
+                      << " " << new_symbol.value.find_source_location() << '\n'
+                      << expr_to_string(new_symbol.name, tmp_new)
+                      << messaget::eom;
       }
     }
   }
@@ -1363,13 +1369,16 @@ bool linkingt::needs_renaming_type(
   return true; // different
 }
 
-void linkingt::do_type_dependencies(
-  std::unordered_set<irep_idt> &needs_to_be_renamed)
+static void do_type_dependencies(
+  const symbol_table_baset &src_symbol_table,
+  std::unordered_set<irep_idt> &needs_to_be_renamed,
+  message_handlert &message_handler)
 {
   // Any type that uses a symbol that will be renamed also
   // needs to be renamed, and so on, until saturation.
 
-  used_byt used_by;
+  // X -> Y iff Y uses X for new symbol type IDs X and Y
+  std::unordered_map<irep_idt, std::unordered_set<irep_idt>> used_by;
 
   for(const auto &symbol_pair : src_symbol_table.symbols)
   {
@@ -1401,14 +1410,16 @@ void linkingt::do_type_dependencies(
       {
         queue.push_back(dep);
         #ifdef DEBUG
-        debug() << "LINKING: needs to be renamed (dependency): "
-                << dep << eom;
-        #endif
+        messaget log{message_handler};
+        log.debug() << "LINKING: needs to be renamed (dependency): " << dep
+                    << messaget::eom;
+#endif
       }
   }
 }
 
 std::unordered_map<irep_idt, irep_idt> linkingt::rename_symbols(
+  const symbol_table_baset &src_symbol_table,
   const std::unordered_set<irep_idt> &needs_to_be_renamed)
 {
   std::unordered_map<irep_idt, irep_idt> new_identifiers;
@@ -1423,13 +1434,14 @@ std::unordered_map<irep_idt, irep_idt> linkingt::rename_symbols(
     if(new_symbol.is_type)
       new_identifier=type_to_name(src_ns, id, new_symbol.type);
     else
-      new_identifier=rename(id);
+      new_identifier = rename(src_symbol_table, id);
 
     new_identifiers.emplace(id, new_identifier);
 
 #ifdef DEBUG
-    debug() << "LINKING: renaming " << id << " to "
-            << new_identifier << eom;
+    messaget log{message_handler};
+    log.debug() << "LINKING: renaming " << id << " to " << new_identifier
+                << messaget::eom;
 #endif
 
     if(new_symbol.is_type)
@@ -1442,6 +1454,7 @@ std::unordered_map<irep_idt, irep_idt> linkingt::rename_symbols(
 }
 
 void linkingt::copy_symbols(
+  const symbol_table_baset &src_symbol_table,
   const std::unordered_map<irep_idt, irep_idt> &new_identifiers)
 {
   std::map<irep_idt, symbolt> src_symbols;
@@ -1506,8 +1519,11 @@ void linkingt::copy_symbols(
   }
 }
 
-void linkingt::typecheck()
+bool linkingt::link(const symbol_table_baset &src_symbol_table)
 {
+  const unsigned errors_before =
+    message_handler.get_message_count(messaget::M_ERROR);
+
   // We do this in three phases. We first figure out which symbols need to
   // be renamed, and then build the renaming, and finally apply this
   // renaming in the second pass over the symbol table.
@@ -1527,28 +1543,31 @@ void linkingt::typecheck()
     {
       needs_to_be_renamed.insert(symbol_pair.first);
       #ifdef DEBUG
-      debug() << "LINKING: needs to be renamed: " << symbol_pair.first << eom;
-      #endif
+      messaget log{message_handler};
+      log.debug() << "LINKING: needs to be renamed: " << symbol_pair.first
+                  << messaget::eom;
+#endif
     }
   }
 
   // renaming types may trigger further renaming
-  do_type_dependencies(needs_to_be_renamed);
+  do_type_dependencies(src_symbol_table, needs_to_be_renamed, message_handler);
 
   // PHASE 2: actually rename them
-  auto new_identifiers = rename_symbols(needs_to_be_renamed);
+  auto new_identifiers = rename_symbols(src_symbol_table, needs_to_be_renamed);
 
   // PHASE 3: copy new symbols to main table
-  copy_symbols(new_identifiers);
+  copy_symbols(src_symbol_table, new_identifiers);
+
+  return message_handler.get_message_count(messaget::M_ERROR) != errors_before;
 }
 
 bool linking(
   symbol_table_baset &dest_symbol_table,
   const symbol_table_baset &new_symbol_table,
   message_handlert &message_handler)
 {
-  linkingt linking(
-    dest_symbol_table, new_symbol_table, message_handler);
+  linkingt linking(dest_symbol_table, message_handler);
 
-  return linking.typecheck_main();
+  return linking.link(new_symbol_table);
 }