goto-cc: also use the linker when processing multiple source files

The linker is able to do some type sanitisation across translation units, and
there is no reason behaviour should be different whether we link previously
compiled object files or a set of source files.

Author: tautschnig

regression/ansi-c/linking_conflicts1/test.desc

@@ -3,7 +3,6 @@ main.c
 other.c
 ^EXIT=(64|1)$
 ^SIGNAL=0$
-^CONVERSION ERROR$
 error: conflicting function declarations 'bar'
 error: conflicting function declarations 'bar2'
 --

regression/ansi-c/linking_conflicts2/test.desc

@@ -1,9 +1,8 @@
-CORE broken-test-c++-front-end
+CORE
 main.c
 other.c
 ^EXIT=(64|1)$
 ^SIGNAL=0$
-^CONVERSION ERROR$
 error: conflicting function declarations 'foo'
 --
 ^warning: ignoring

src/goto-cc/compile.cpp

@@ -42,6 +42,7 @@ Date: June 2006
 #include <langapi/language_file.h>
 #include <langapi/mode.h>
 
+#include <linking/linking.h>
 #include <linking/static_lifetime_init.h>
 
 #define DOTGRAPHSETTINGS  "color=black;" \
@@ -56,8 +57,6 @@ Date: June 2006
 /// \return true on error, false otherwise
 bool compilet::doit()
 {
-  goto_model.goto_functions.clear();
-
   add_compiler_specific_defines();
 
   // Parse command line for source and object file names
@@ -98,15 +97,15 @@ bool compilet::doit()
   const unsigned warnings_before=
     get_message_handler().get_message_count(messaget::M_WARNING);
 
-  if(!source_files.empty())
-    if(compile())
-      return true;
+  auto symbol_table_opt = compile();
+  if(!symbol_table_opt.has_value())
+    return true;
 
   if(mode==LINK_LIBRARY ||
      mode==COMPILE_LINK ||
      mode==COMPILE_LINK_EXECUTABLE)
   {
-    if(link())
+    if(link(*symbol_table_opt))
       return true;
   }
 
@@ -308,11 +307,14 @@ bool compilet::find_library(const std::string &name)
 
 /// parses object files and links them
 /// \return true on error, false otherwise
-bool compilet::link()
+bool compilet::link(optionalt<symbol_tablet> &&symbol_table)
 {
   // "compile" hitherto uncompiled functions
   statistics() << "Compiling functions" << eom;
-  convert_symbols(goto_model.goto_functions);
+  goto_modelt goto_model;
+  if(symbol_table.has_value())
+    goto_model.symbol_table = std::move(*symbol_table);
+  convert_symbols(goto_model);
 
   // parse object files
   for(const auto &file_name : object_files)
@@ -343,7 +345,7 @@ bool compilet::link()
       return true;
 
     // entry_point may (should) add some more functions.
-    convert_symbols(goto_model.goto_functions);
+    convert_symbols(goto_model);
   }
 
   if(keep_file_local)
@@ -359,11 +361,13 @@ bool compilet::link()
   return add_written_cprover_symbols(goto_model.symbol_table);
 }
 
-/// parses source files and writes object files, or keeps the symbols in the
-/// symbol_table depending on the doLink flag.
-/// \return true on error, false otherwise
-bool compilet::compile()
+/// Parses source files and writes object files, or keeps the symbols in the
+/// symbol_table if not compiling/assembling only.
+/// \return Symbol table, if parsing and type checking succeeded, else empty
+optionalt<symbol_tablet> compilet::compile()
 {
+  symbol_tablet symbol_table;
+
   while(!source_files.empty())
   {
     std::string file_name=source_files.front();
@@ -374,9 +378,9 @@ bool compilet::compile()
     if(echo_file_name)
       std::cout << get_base_name(file_name, false) << '\n' << std::flush;
 
-    bool r=parse_source(file_name); // don't break the program!
+    auto file_symbol_table = parse_source(file_name);
 
-    if(r)
+    if(!file_symbol_table.has_value())
     {
       const std::string &debug_outfile=
         cmdline.get_value("print-rejected-preprocessed-source");
@@ -388,15 +392,17 @@ bool compilet::compile()
         warning() << "Failed sources in " << debug_outfile << eom;
       }
 
-      return true; // parser/typecheck error
+      return {}; // parser/typecheck error
     }
 
     if(mode==COMPILE_ONLY || mode==ASSEMBLE_ONLY)
     {
       // output an object file for every source file
 
       // "compile" functions
-      convert_symbols(goto_model.goto_functions);
+      goto_modelt file_goto_model;
+      file_goto_model.symbol_table = std::move(*file_symbol_table);
+      convert_symbols(file_goto_model);
 
       std::string cfn;
 
@@ -416,21 +422,26 @@ bool compilet::compile()
       if(keep_file_local)
       {
         function_name_manglert<file_name_manglert> mangler(
-          get_message_handler(), goto_model, file_local_mangle_suffix);
+          get_message_handler(), file_goto_model, file_local_mangle_suffix);
         mangler.mangle();
       }
 
-      if(write_bin_object_file(cfn, goto_model))
-        return true;
-
-      if(add_written_cprover_symbols(goto_model.symbol_table))
-        return true;
+      if(write_bin_object_file(cfn, file_goto_model))
+        return {};
 
-      goto_model.clear(); // clean symbol table for next source file.
+      if(add_written_cprover_symbols(file_goto_model.symbol_table))
+        return {};
+    }
+    else
+    {
+      if(linking(symbol_table, *file_symbol_table, get_message_handler()))
+      {
+        return {};
+      }
     }
   }
 
-  return false;
+  return std::move(symbol_table);
 }
 
 /// parses a source file (low-level parsing)
@@ -600,37 +611,37 @@ bool compilet::write_bin_object_file(
   return false;
 }
 
-/// parses a source file
-/// \return true on error, false otherwise
-bool compilet::parse_source(const std::string &file_name)
+/// Parses and type checks a source file located at \p file_name.
+/// \return A symbol table if, and only if, parsing and type checking succeeded.
+optionalt<symbol_tablet> compilet::parse_source(const std::string &file_name)
 {
   language_filest language_files;
   language_files.set_message_handler(get_message_handler());
 
   if(parse(file_name, language_files))
-    return true;
+    return {};
 
   // we just typecheck one file here
-  if(language_files.typecheck(goto_model.symbol_table, keep_file_local))
+  symbol_tablet file_symbol_table;
+  if(language_files.typecheck(file_symbol_table, keep_file_local))
   {
     error() << "CONVERSION ERROR" << eom;
-    return true;
+    return {};
   }
 
-  if(language_files.final(goto_model.symbol_table))
+  if(language_files.final(file_symbol_table))
   {
     error() << "CONVERSION ERROR" << eom;
-    return true;
+    return {};
   }
 
-  return false;
+  return std::move(file_symbol_table);
 }
 
 /// constructor
 /// \return nothing
 compilet::compilet(cmdlinet &_cmdline, message_handlert &mh, bool Werror)
   : messaget(mh),
-    ns(goto_model.symbol_table),
     cmdline(_cmdline),
     warning_is_fatal(Werror),
     keep_file_local(
@@ -678,7 +689,7 @@ void compilet::add_compiler_specific_defines() const
     std::string("__GOTO_CC_VERSION__=") + CBMC_VERSION);
 }
 
-void compilet::convert_symbols(goto_functionst &dest)
+void compilet::convert_symbols(goto_modelt &goto_model)
 {
   symbol_table_buildert symbol_table_builder =
     symbol_table_buildert::wrap(goto_model.symbol_table);
@@ -712,7 +723,8 @@ void compilet::convert_symbols(goto_functionst &dest)
         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]);
+        converter.convert_function(
+          s_it->first, goto_model.goto_functions.function_map[s_it->first]);
         symbol_table_builder.get_writeable_ref(symbol).set_compiled();
       }
     }

src/goto-cc/compile.h

@@ -26,9 +26,6 @@ class languaget;
 class compilet : public messaget
 {
 public:
-  // compilation results
-  goto_modelt goto_model;
-
   // configuration
   bool echo_file_name;
   bool validate_goto_model = false;
@@ -63,10 +60,10 @@ class compilet : public messaget
   bool parse(const std::string &filename, language_filest &);
   bool parse_stdin(languaget &);
   bool doit();
-  bool compile();
-  bool link();
+  optionalt<symbol_tablet> compile();
+  bool link(optionalt<symbol_tablet> &&symbol_table);
 
-  bool parse_source(const std::string &);
+  optionalt<symbol_tablet> parse_source(const std::string &);
 
   /// Writes the goto functions of \p src_goto_model to a binary format object
   /// file.
@@ -133,7 +130,7 @@ class compilet : public messaget
 
   void add_compiler_specific_defines() const;
 
-  void convert_symbols(goto_functionst &dest);
+  void convert_symbols(goto_modelt &);
 
   bool add_written_cprover_symbols(const symbol_tablet &symbol_table);
   std::map<irep_idt, symbolt> written_macros;