Merge pull request #6844 from remi-delmas-3000/force-load-cprover-library

Allow to force-load symbols from the cprover library

Author: tautschnig

src/ansi-c/ansi_c_language.cpp

@@ -104,6 +104,15 @@ bool ansi_c_languaget::typecheck(
   symbol_tablet &symbol_table,
   const std::string &module,
   const bool keep_file_local)
+{
+  return typecheck(symbol_table, module, keep_file_local, {});
+}
+
+bool ansi_c_languaget::typecheck(
+  symbol_tablet &symbol_table,
+  const std::string &module,
+  const bool keep_file_local,
+  const std::set<irep_idt> &keep)
 {
   symbol_tablet new_symbol_table;
 
@@ -117,7 +126,7 @@ bool ansi_c_languaget::typecheck(
   }
 
   remove_internal_symbols(
-    new_symbol_table, this->get_message_handler(), keep_file_local);
+    new_symbol_table, this->get_message_handler(), keep_file_local, keep);
 
   if(linking(symbol_table, new_symbol_table, get_message_handler()))
     return true;

src/ansi-c/ansi_c_language.h

@@ -56,6 +56,12 @@ class ansi_c_languaget:public languaget
     const std::string &module,
     const bool keep_file_local) override;
 
+  bool typecheck(
+    symbol_tablet &symbol_table,
+    const std::string &module,
+    const bool keep_file_local,
+    const std::set<irep_idt> &keep);
+
   bool can_keep_file_local() override
   {
     return true;

src/ansi-c/cprover_library.cpp

@@ -17,7 +17,8 @@ Author: Daniel Kroening, [email protected]
 
 static std::string get_cprover_library_text(
   const std::set<irep_idt> &functions,
-  const symbol_tablet &symbol_table)
+  const symbol_tablet &symbol_table,
+  const bool force_load)
 {
   std::ostringstream library_text;
 
@@ -52,14 +53,15 @@ static std::string get_cprover_library_text(
   /// \endcond
 
   return get_cprover_library_text(
-    functions, symbol_table, cprover_library, library_text.str());
+    functions, symbol_table, cprover_library, library_text.str(), force_load);
 }
 
 std::string get_cprover_library_text(
   const std::set<irep_idt> &functions,
   const symbol_tablet &symbol_table,
   const struct cprover_library_entryt cprover_library[],
-  const std::string &prologue)
+  const std::string &prologue,
+  const bool force_load)
 {
   // the default mode is ios_base::out which means subsequent write to the
   // stream will overwrite the original content
@@ -77,8 +79,9 @@ std::string get_cprover_library_text(
       symbol_tablet::symbolst::const_iterator old=
         symbol_table.symbols.find(id);
 
-      if(old!=symbol_table.symbols.end() &&
-         old->second.value.is_nil())
+      if(
+        force_load ||
+        (old != symbol_table.symbols.end() && old->second.value.is_nil()))
       {
         count++;
         library_text << e->model << '\n';
@@ -100,17 +103,17 @@ void cprover_c_library_factory(
   if(config.ansi_c.lib==configt::ansi_ct::libt::LIB_NONE)
     return;
 
-  std::string library_text;
-
-  library_text=get_cprover_library_text(functions, symbol_table);
+  std::string library_text =
+    get_cprover_library_text(functions, symbol_table, false);
 
   add_library(library_text, symbol_table, message_handler);
 }
 
 void add_library(
   const std::string &src,
   symbol_tablet &symbol_table,
-  message_handlert &message_handler)
+  message_handlert &message_handler,
+  const std::set<irep_idt> &keep)
 {
   if(src.empty())
     return;
@@ -121,5 +124,15 @@ void add_library(
   ansi_c_language.set_message_handler(message_handler);
   ansi_c_language.parse(in, "");
 
-  ansi_c_language.typecheck(symbol_table, "<built-in-library>");
+  ansi_c_language.typecheck(symbol_table, "<built-in-library>", true, keep);
+}
+
+void cprover_c_library_factory_force_load(
+  const std::set<irep_idt> &functions,
+  symbol_tablet &symbol_table,
+  message_handlert &message_handler)
+{
+  std::string library_text =
+    get_cprover_library_text(functions, symbol_table, true);
+  add_library(library_text, symbol_table, message_handler, functions);
 }

src/ansi-c/cprover_library.h

@@ -27,16 +27,28 @@ std::string get_cprover_library_text(
   const std::set<irep_idt> &functions,
   const symbol_tablet &,
   const struct cprover_library_entryt[],
-  const std::string &prologue);
+  const std::string &prologue,
+  const bool force_load = false);
 
+/// Parses and typechecks the given src and adds its contents to the
+/// symbol table. Symbols with names found in `keep` will survive
+/// the symbol table cleanup pass and be found in the symbol_table.
 void add_library(
   const std::string &src,
   symbol_tablet &,
-  message_handlert &);
+  message_handlert &,
+  const std::set<irep_idt> &keep = {});
 
 void cprover_c_library_factory(
   const std::set<irep_idt> &functions,
   symbol_tablet &,
   message_handlert &);
 
+/// Load the requested function symbols from the cprover library
+/// and add them to the symbol table regardless of
+/// the library config flags and usage.
+void cprover_c_library_factory_force_load(
+  const std::set<irep_idt> &functions,
+  symbol_tablet &symbol_table,
+  message_handlert &message_handler);
 #endif // CPROVER_ANSI_C_CPROVER_LIBRARY_H

src/linking/remove_internal_symbols.cpp

@@ -108,6 +108,30 @@ void remove_internal_symbols(
   symbol_tablet &symbol_table,
   message_handlert &mh,
   const bool keep_file_local)
+{
+  remove_internal_symbols(symbol_table, mh, keep_file_local, {});
+}
+
+/// Removes internal symbols from a symbol table
+/// A symbol is EXPORTED if it is a
+/// * non-static function with body that is not extern inline
+/// * symbol used in an EXPORTED symbol
+/// * type used in an EXPORTED symbol
+///
+///          Read
+///          http://gcc.gnu.org/ml/gcc/2006-11/msg00006.html
+///          on "extern inline"
+/// \param symbol_table: symbol table to clean up
+/// \param mh: log handler
+/// \param keep_file_local: keep file-local functions with bodies even if we
+///                         would otherwise remove them
+/// \param keep: set of symbol names to keep in the symbol table regardless
+///              of usage or kind
+void remove_internal_symbols(
+  symbol_tablet &symbol_table,
+  message_handlert &mh,
+  const bool keep_file_local,
+  const std::set<irep_idt> &keep)
 {
   namespacet ns(symbol_table);
   find_symbols_sett exported;
@@ -130,6 +154,8 @@ void remove_internal_symbols(
   special.insert("__placement_new_array");
   special.insert("__delete");
   special.insert("__delete_array");
+  // plus any extra symbols we wish to keep
+  special.insert(keep.begin(), keep.end());
 
   for(symbol_tablet::symbolst::const_iterator
       it=symbol_table.symbols.begin();

src/linking/remove_internal_symbols.h

@@ -12,11 +12,21 @@ Author: Daniel Kroening
 #ifndef CPROVER_LINKING_REMOVE_INTERNAL_SYMBOLS_H
 #define CPROVER_LINKING_REMOVE_INTERNAL_SYMBOLS_H
 
+#include <util/irep.h>
+
+#include <set>
+
 class message_handlert;
 
 void remove_internal_symbols(
   class symbol_tablet &symbol_table,
   message_handlert &,
   const bool);
 
+void remove_internal_symbols(
+  class symbol_tablet &symbol_table,
+  message_handlert &,
+  const bool keep_file_local,
+  const std::set<irep_idt> &keep);
+
 #endif // CPROVER_LINKING_REMOVE_INTERNAL_SYMBOLS_H