Re-use known declarations when parsing the built-in library

When doing cross-platform verification we should not rely on 1) system headers
being present and 2) system headers matching the declarations that were used
while compiling the program to be verified. Thus re-use the symbol table that
has been generated from the input program when compiling functions of the
built-in library.

This will address a number of SV-COMP benchmarks that CBMC currently fails on
for they use augmented standard-library types.

Author: tautschnig

regression/cbmc/library1/main.c

@@ -0,0 +1,16 @@
+struct _IO_FILE;
+typedef struct _IO_FILE FILE;
+struct _IO_FILE
+{
+  char dummy;
+};
+
+extern FILE *fopen(char const* fname, char const* mode);
+
+int main()
+{
+  FILE *f;
+  f = fopen("some_file", "r");
+  __CPROVER_assert(f == 0, "");
+  return 0;
+}

regression/cbmc/library1/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+implicit function declaration
+syntax error

src/ansi-c/ansi_c_language.cpp

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/config.h>
 #include <util/get_base_name.h>
+#include <util/find_symbols.h>
 
 #include <linking/linking.h>
 #include <linking/remove_internal_symbols.h>
@@ -52,6 +53,15 @@ bool ansi_c_languaget::preprocess(
 bool ansi_c_languaget::parse(
   std::istream &instream,
   const std::string &path)
+{
+  symbol_tablet st;
+  return parse(instream, path, st);
+}
+
+bool ansi_c_languaget::parse(
+  std::istream &instream,
+  const std::string &path,
+  const symbol_tablet &symbol_table)
 {
   // store the path
   parse_path=path;
@@ -78,6 +88,7 @@ bool ansi_c_languaget::parse(
   ansi_c_parser.cpp98=false; // it's not C++
   ansi_c_parser.cpp11=false; // it's not C++
   ansi_c_parser.mode=config.ansi_c.mode;
+  ansi_c_parser.set_symbol_table(symbol_table);
 
   ansi_c_scanner_init();
 
@@ -95,6 +106,27 @@ bool ansi_c_languaget::parse(
   // save result
   parse_tree.swap(ansi_c_parser.parse_tree);
 
+  // copy depended-on symbols from the existing symbol table
+  std::list<irep_idt> needed_syms;
+  for(const auto &scope_syms : ansi_c_parser.root_scope().name_map)
+  {
+    if(scope_syms.second.from_symbol_table)
+      needed_syms.push_back(scope_syms.second.prefixed_name);
+  }
+  while(!needed_syms.empty())
+  {
+    const irep_idt id = needed_syms.front();
+    needed_syms.pop_front();
+    const symbolt &symbol = symbol_table.lookup_ref(id);
+
+    if(symbol.is_type && !new_symbol_table.add(symbol))
+    {
+      find_symbols_sett deps;
+      find_type_symbols(symbol.type, deps);
+      needed_syms.insert(needed_syms.end(), deps.begin(), deps.end());
+    }
+  }
+
   // save some memory
   ansi_c_parser.clear();
 
@@ -105,8 +137,6 @@ bool ansi_c_languaget::typecheck(
   symbol_tablet &symbol_table,
   const std::string &module)
 {
-  symbol_tablet new_symbol_table;
-
   if(ansi_c_typecheck(
     parse_tree,
     new_symbol_table,
@@ -118,10 +148,10 @@ bool ansi_c_languaget::typecheck(
 
   remove_internal_symbols(new_symbol_table);
 
-  if(linking(symbol_table, new_symbol_table, get_message_handler()))
-    return true;
+  bool retval = linking(symbol_table, new_symbol_table, get_message_handler());
+  new_symbol_table.clear();
 
-  return false;
+  return retval;
 }
 
 bool ansi_c_languaget::generate_support_functions(
@@ -196,6 +226,7 @@ bool ansi_c_languaget::to_expr(
   ansi_c_parser.in=&i_preprocessed;
   ansi_c_parser.set_message_handler(get_message_handler());
   ansi_c_parser.mode=config.ansi_c.mode;
+  ansi_c_parser.set_symbol_table(ns.get_symbol_table());
   ansi_c_scanner_init();
 
   bool result=ansi_c_parser.parse();

src/ansi-c/ansi_c_language.h

@@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]
 #include <memory>
 
 #include <util/make_unique.h>
+#include <util/symbol_table.h>
 
 #include <langapi/language.h>
 
@@ -30,6 +31,9 @@ class ansi_c_languaget:public languaget
     std::istream &instream,
     const std::string &path) override;
 
+  bool
+  parse(std::istream &instream, const std::string &path, const symbol_tablet &);
+
   bool generate_support_functions(
     symbol_tablet &symbol_table) override;
 
@@ -75,6 +79,7 @@ class ansi_c_languaget:public languaget
 protected:
   ansi_c_parse_treet parse_tree;
   std::string parse_path;
+  symbol_tablet new_symbol_table;
 };
 
 std::unique_ptr<languaget> new_ansi_c_language();

src/ansi-c/ansi_c_parser.cpp

@@ -8,7 +8,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "ansi_c_parser.h"
 
-#include <iostream>
+#include <util/symbol_table.h>
 
 #include "c_storage_spec.h"
 
@@ -42,6 +42,24 @@ ansi_c_id_classt ansi_c_parsert::lookup(
     }
   }
 
+  // if a symbol table has been provided, try to resolve global-scoped symbols
+  if(!tag && !label && symbol_table)
+  {
+    const symbolt *symbol = symbol_table->lookup(scope_name);
+    if(symbol)
+    {
+      ansi_c_identifiert &i = root_scope().name_map[scope_name];
+      i.from_symbol_table = true;
+      i.id_class = symbol->is_type && symbol->is_macro
+                    ? ansi_c_id_classt::ANSI_C_TYPEDEF
+                    : ansi_c_id_classt::ANSI_C_SYMBOL;
+      i.prefixed_name = symbol->name;
+      i.base_name = symbol->base_name;
+      identifier = i.prefixed_name;
+      return i.id_class;
+    }
+  }
+
   // Not found.
   // If it's a tag, we will add to current scope.
   if(tag)
@@ -150,6 +168,10 @@ void ansi_c_parsert::add_declarator(
     ansi_c_identifiert &identifier=scope.name_map[base_name];
     identifier.id_class=id_class;
     identifier.prefixed_name=prefixed_name;
+    // it may already have been put in the scope from an existing symbol table
+    // via lookup; now that we know it's being declared here we don't need or
+    // want the entry from the symbol table
+    identifier.from_symbol_table = false;
   }
 
   ansi_c_declaration.declarators().push_back(new_declarator);

src/ansi-c/ansi_c_parser.h

@@ -35,7 +35,8 @@ class ansi_c_parsert:public parsert
     mode(modet::NONE),
     cpp98(false),
     cpp11(false),
-    for_has_scope(false)
+    for_has_scope(false),
+    symbol_table(nullptr)
   {
   }
 
@@ -59,6 +60,8 @@ class ansi_c_parsert:public parsert
     // set up global scope
     scopes.clear();
     scopes.push_back(scopet());
+
+    symbol_table = nullptr;
   }
 
   // internal state of the scanner
@@ -139,6 +142,14 @@ class ansi_c_parsert:public parsert
     lookup(base_name, identifier, false, true);
     return identifier;
   }
+
+  void set_symbol_table(const symbol_tablet &st)
+  {
+    symbol_table = &st;
+  }
+
+private:
+  const symbol_tablet *symbol_table;
 };
 
 extern ansi_c_parsert ansi_c_parser;

src/ansi-c/ansi_c_scope.h

@@ -29,9 +29,11 @@ class ansi_c_identifiert
 {
 public:
   ansi_c_id_classt id_class;
+  bool from_symbol_table;
   irep_idt base_name, prefixed_name;
 
-  ansi_c_identifiert():id_class(ansi_c_id_classt::ANSI_C_UNKNOWN)
+  ansi_c_identifiert()
+    : id_class(ansi_c_id_classt::ANSI_C_UNKNOWN), from_symbol_table(false)
   {
   }
 };

src/ansi-c/cprover_library.cpp

@@ -14,6 +14,9 @@ Author: Daniel Kroening, [email protected]
 
 #include "ansi_c_language.h"
 
+static void
+add_library(const std::string &src, symbol_tablet &, message_handlert &);
+
 struct cprover_library_entryt
 {
   const char *function;
@@ -78,7 +81,7 @@ void add_cprover_library(
   add_library(library_text, symbol_table, message_handler);
 }
 
-void add_library(
+static void add_library(
   const std::string &src,
   symbol_tablet &symbol_table,
   message_handlert &message_handler)
@@ -90,7 +93,7 @@ void add_library(
 
   ansi_c_languaget ansi_c_language;
   ansi_c_language.set_message_handler(message_handler);
-  ansi_c_language.parse(in, "");
+  ansi_c_language.parse(in, "", symbol_table);
 
   ansi_c_language.typecheck(symbol_table, "<built-in-library>");
 }

src/ansi-c/cprover_library.h

@@ -19,11 +19,6 @@ std::string get_cprover_library_text(
   const std::set<irep_idt> &functions,
   const symbol_tablet &);
 
-void add_library(
-  const std::string &src,
-  symbol_tablet &,
-  message_handlert &);
-
 void add_cprover_library(
   const std::set<irep_idt> &functions,
   symbol_tablet &,