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

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 &,

src/ansi-c/library/cprover.h

@@ -38,6 +38,7 @@ void __CPROVER_cover(__CPROVER_bool condition);
 
 void __CPROVER_input(const char *id, ...);
 void __CPROVER_output(const char *id, ...);
+int __CPROVER_printf(const char *fmt, ...);
 
 // concurrency-related
 void __CPROVER_atomic_begin();

src/ansi-c/library/err.c

@@ -1,14 +1,6 @@
 /* FUNCTION: err */
 
-#ifndef __CPROVER_ERR_H_INCLUDED
-#include <err.h>
-#define __CPROVER_ERR_H_INCLUDED
-#endif
-
-#ifndef __CPROVER_STDLIB_H_INCLUDED
-#include <stdlib.h>
-#define __CPROVER_STDLIB_H_INCLUDED
-#endif
+void abort(void);
 
 void err(int eval, const char *fmt, ...)
 {
@@ -19,15 +11,7 @@ void err(int eval, const char *fmt, ...)
 
 /* FUNCTION: err */
 
-#ifndef __CPROVER_ERR_H_INCLUDED
-#include <err.h>
-#define __CPROVER_ERR_H_INCLUDED
-#endif
-
-#ifndef __CPROVER_STDLIB_H_INCLUDED
-#include <stdlib.h>
-#define __CPROVER_STDLIB_H_INCLUDED
-#endif
+void abort(void);
 
 void errx(int eval, const char *fmt, ...)
 {
@@ -38,23 +22,13 @@ void errx(int eval, const char *fmt, ...)
 
 /* FUNCTION: warn */
 
-#ifndef __CPROVER_ERR_H_INCLUDED
-#include <err.h>
-#define __CPROVER_ERR_H_INCLUDED
-#endif
-
 void warn(const char *fmt, ...)
 {
   (void)*fmt;
 }
 
 /* FUNCTION: warnx */
 
-#ifndef __CPROVER_ERR_H_INCLUDED
-#include <err.h>
-#define __CPROVER_ERR_H_INCLUDED
-#endif
-
 void warnx(const char *fmt, ...)
 {
   (void)*fmt;

src/ansi-c/library/fcntl.c

@@ -1,10 +1,5 @@
 /* FUNCTION: fcntl */
 
-#ifndef __CPROVER_FCNTL_H_INCLUDED
-#include <fcntl.h>
-#define __CPROVER_FCNTL_H_INCLUDED
-#endif
-
 int __VERIFIER_nondet_int();
 
 int fcntl(int fd, int cmd, ...)