Use the linker when adding library functions

This enables type checking of missing functions vs library-provided functions,
and also enables type sanitisation as done by the linker.

Co-authored-by: Peter Schrammel <[email protected]>

Author: tautschnig

regression/cbmc-library/__errno_location-01/main.c

@@ -1,9 +1,9 @@
 #include <assert.h>
 #include <errno.h>
 
-int main()
+int main(int arc, char *argv[])
 {
-  __errno_location();
-  assert(0);
+  // errno expands to use of __errno_location() with glibc
+  assert(errno == 0);
   return 0;
 }

regression/cbmc-library/__errno_location-01/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --pointer-check --bounds-check
 ^EXIT=0$

regression/cbmc-library/memcpy-07/main.c

@@ -1,4 +1,5 @@
 // #include <string.h> intentionally omitted
+void *memcpy();
 
 struct c
 {

regression/cbmc/String_Abstraction17/strcpy-no-decl.c

@@ -1,4 +1,5 @@
-void *malloc(unsigned);
+#include <stdlib.h>
+// string.h intentionally omitted
 
 char *make_str()
 {

regression/cbmc/String_Abstraction17/test.desc

@@ -1,11 +1,13 @@
 CORE
 strcpy-no-decl.c
 --string-abstraction --validate-goto-model
-Condition: strlen type inconsistency
-^EXIT=(127|134)$
+^EXIT=10$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-While this test currently passes when omitting --validate-goto-model, we should
-expect a report of type inconsistencies as no forward declarations are present.
+The linker is able to fix up type inconsistencies of the missing function
+declarations, but the absence of a declaration of strlen results in not picking
+up the library model. Consequently the assumption does not work as intended, and
+verification fails. Adding #include <string.h> makes verification pass as
+expected.

regression/goto-cc-goto-analyzer/instrument_preconditions_locations/s2n_hash_inlined.c

@@ -1,3 +1,5 @@
+#include <stdlib.h>
+
 // This file is highly reduced from some open source projects.
 // The following four lines are adapted from the openssl library
 // Full repository here:

src/ansi-c/cprover_library.cpp

@@ -98,7 +98,8 @@ std::string get_cprover_library_text(
 
 void cprover_c_library_factory(
   const std::set<irep_idt> &functions,
-  symbol_table_baset &symbol_table,
+  const symbol_table_baset &symbol_table,
+  symbol_table_baset &dest_symbol_table,
   message_handlert &message_handler)
 {
   if(config.ansi_c.lib==configt::ansi_ct::libt::LIB_NONE)
@@ -107,7 +108,7 @@ void cprover_c_library_factory(
   std::string library_text =
     get_cprover_library_text(functions, symbol_table, false);
 
-  add_library(library_text, symbol_table, message_handler);
+  add_library(library_text, dest_symbol_table, message_handler);
 }
 
 void add_library(

src/ansi-c/cprover_library.h

@@ -41,6 +41,7 @@ void add_library(
 
 void cprover_c_library_factory(
   const std::set<irep_idt> &functions,
+  const symbol_table_baset &,
   symbol_table_baset &,
   message_handlert &);
 

src/cpp/cprover_library.cpp

@@ -37,7 +37,8 @@ static std::string get_cprover_library_text(
 
 void cprover_cpp_library_factory(
   const std::set<irep_idt> &functions,
-  symbol_table_baset &symbol_table,
+  const symbol_table_baset &symbol_table,
+  symbol_table_baset &dest_symbol_table,
   message_handlert &message_handler)
 {
   if(config.ansi_c.lib == configt::ansi_ct::libt::LIB_NONE)
@@ -46,5 +47,5 @@ void cprover_cpp_library_factory(
   const std::string library_text =
     get_cprover_library_text(functions, symbol_table);
 
-  add_library(library_text, symbol_table, message_handler);
+  add_library(library_text, dest_symbol_table, message_handler);
 }

src/cpp/cprover_library.h

@@ -18,6 +18,7 @@ class symbol_table_baset;
 
 void cprover_cpp_library_factory(
   const std::set<irep_idt> &functions,
+  const symbol_table_baset &,
   symbol_table_baset &,
   message_handlert &);
 

src/goto-programs/link_to_library.cpp

@@ -11,38 +11,100 @@ Author: Daniel Kroening, [email protected]
 
 #include "link_to_library.h"
 
+#include <linking/static_lifetime_init.h>
+
 #include "compute_called_functions.h"
 #include "goto_convert_functions.h"
 #include "goto_model.h"
+#include "link_goto_model.h"
+
+/// Try to add \p missing_function from \p library to \p goto_model.
+static optionalt<replace_symbolt::expr_mapt> add_one_function(
+  goto_modelt &goto_model,
+  message_handlert &message_handler,
+  const std::function<void(
+    const std::set<irep_idt> &,
+    const symbol_tablet &,
+    symbol_tablet &,
+    message_handlert &)> &library,
+  const irep_idt &missing_function)
+{
+  goto_modelt library_model;
+  library(
+    {missing_function},
+    goto_model.symbol_table,
+    library_model.symbol_table,
+    message_handler);
+
+  // convert to CFG
+  if(
+    library_model.symbol_table.symbols.find(missing_function) !=
+    library_model.symbol_table.symbols.end())
+  {
+    goto_convert(
+      missing_function,
+      library_model.symbol_table,
+      library_model.goto_functions,
+      message_handler);
+  }
+
+  // check whether additional initialization may be required
+  if(
+    goto_model.goto_functions.function_map.find(INITIALIZE_FUNCTION) !=
+    goto_model.goto_functions.function_map.end())
+  {
+    for(const auto &entry : library_model.symbol_table)
+    {
+      if(
+        entry.second.is_static_lifetime && !entry.second.is_type &&
+        !entry.second.is_macro && entry.second.type.id() != ID_code &&
+        !goto_model.symbol_table.has_symbol(entry.first))
+      {
+        goto_model.unload(INITIALIZE_FUNCTION);
+        break;
+      }
+    }
+  }
+
+  return link_goto_model(goto_model, std::move(library_model), message_handler);
+}
 
 /// Complete missing function definitions using the \p library.
 /// \param goto_model: goto model that may contain function calls and symbols
 ///   with missing function bodies
 /// \param message_handler: message handler to report library processing
 ///   problems
-/// \param library: generator function that produces function definitions for a
-///   given set of symbol names that have no body.
+/// \param library: generator function that produces function definitions (in
+///   the symbol table that is the third parameter) for a given set of symbol
+///   names (first parameter) that have no body in the source symbol table
+///   (second parameter).
 void link_to_library(
   goto_modelt &goto_model,
   message_handlert &message_handler,
-  const std::function<
-    void(const std::set<irep_idt> &, symbol_tablet &, message_handlert &)>
-    &library)
+  const std::function<void(
+    const std::set<irep_idt> &,
+    const symbol_tablet &,
+    symbol_tablet &,
+    message_handlert &)> &library)
 {
   // this needs a fixedpoint, as library functions
   // may depend on other library functions
 
   std::set<irep_idt> added_functions;
+  // Linking in library functions (now seeing full definitions rather than
+  // forward declarations, or perhaps even cases of missing forward
+  // declarations) may result in type changes to objects.
+  replace_symbolt::expr_mapt object_type_updates;
+  const bool had_init =
+    goto_model.goto_functions.function_map.find(INITIALIZE_FUNCTION) !=
+    goto_model.goto_functions.function_map.end();
 
   while(true)
   {
     std::unordered_set<irep_idt> called_functions =
       compute_called_functions(goto_model.goto_functions);
 
-    // eliminate those for which we already have a body
-
-    std::set<irep_idt> missing_functions;
-
+    bool changed = false;
     for(const auto &id : called_functions)
     {
       goto_functionst::function_mapt::const_iterator f_it =
@@ -59,30 +121,44 @@ void link_to_library(
         // already added
       }
       else
-        missing_functions.insert(id);
+      {
+        changed = true;
+        added_functions.insert(id);
+
+        auto updates_opt =
+          add_one_function(goto_model, message_handler, library, id);
+        if(!updates_opt.has_value())
+        {
+          messaget log{message_handler};
+          log.warning() << "Linking library function '" << id << "' failed"
+                        << messaget::eom;
+          continue;
+        }
+        object_type_updates.insert(updates_opt->begin(), updates_opt->end());
+      }
     }
 
     // done?
-    if(missing_functions.empty())
+    if(!changed)
       break;
+  }
 
-    library(missing_functions, goto_model.symbol_table, message_handler);
-
-    // convert to CFG
-    for(const auto &id : missing_functions)
-    {
-      if(
-        goto_model.symbol_table.symbols.find(id) !=
-        goto_model.symbol_table.symbols.end())
-      {
-        goto_convert(
-          id,
-          goto_model.symbol_table,
-          goto_model.goto_functions,
-          message_handler);
-      }
-
-      added_functions.insert(id);
-    }
+  if(
+    had_init &&
+    goto_model.goto_functions.function_map.find(INITIALIZE_FUNCTION) ==
+      goto_model.goto_functions.function_map.end())
+  {
+    static_lifetime_init(
+      goto_model.symbol_table,
+      goto_model.symbol_table.lookup_ref(INITIALIZE_FUNCTION).location);
+    goto_convert(
+      INITIALIZE_FUNCTION,
+      goto_model.symbol_table,
+      goto_model.goto_functions,
+      message_handler);
+    goto_model.goto_functions.update();
   }
+
+  if(!object_type_updates.empty())
+    finalize_linking(goto_model, object_type_updates);
 }

src/goto-programs/link_to_library.h

@@ -24,7 +24,10 @@ class symbol_tablet;
 void link_to_library(
   goto_modelt &,
   message_handlert &,
-  const std::function<
-    void(const std::set<irep_idt> &, symbol_tablet &, message_handlert &)> &);
+  const std::function<void(
+    const std::set<irep_idt> &,
+    const symbol_tablet &,
+    symbol_tablet &,
+    message_handlert &)> &);
 
 #endif // CPROVER_GOTO_PROGRAMS_LINK_TO_LIBRARY_H