Add --keep-implementations switch to goto-cc

The --keep-implementations switch takes a comma-separated list of
identifiers. When this switch is passed to goto-cc, the compiler will
not remove the symbols and definitions for the named functions, even
when they appear to be unused.

This patch is to support running CBMC on projects that define many of
their functions as static. Prior to this commit, users could not test
the correctness of functions marked as static because the function
definitions would not be exported by goto-cc.

Author: karkhaz

regression/CMakeLists.txt

@@ -50,3 +50,4 @@ add_subdirectory(goto-cc-goto-analyzer)
 add_subdirectory(systemc)
 add_subdirectory(contracts)
 add_subdirectory(goto-harness)
+add_subdirectory(goto-cc-static)

regression/goto-cc-static/CMakeLists.txt

@@ -0,0 +1,9 @@
+if(WIN32)
+    set(is_windows true)
+else()
+    set(is_windows false)
+endif()
+
+add_test_pl_tests(
+    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:cbmc> ${is_windows}"
+)

regression/goto-cc-static/chain.sh

@@ -0,0 +1,29 @@
+#!/usr/bin/env bash
+
+goto_cc=$1
+cbmc=$2
+is_windows=$3
+
+to_keep=""
+if [ $# -gt 3 ]; then
+  if [ $4!='' ]; then
+    to_keep="--keep-implementations $4"
+  fi
+fi
+
+cbmc_options=""
+if [ $# -gt 4 ]; then
+  cbmc_options=${*:5:$#-5}
+fi
+
+name=${*:$#}
+name=${name%.c}
+
+if [[ "${is_windows}" == "true" ]]; then
+  "${goto_cc}" ${to_keep} "${name}.c"
+  mv "${name}.exe" "${name}.gb"
+else
+  "${goto_cc}" ${to_keep} "${name}.c" -o "${name}.gb"
+fi
+
+"${cbmc}" ${cbmc_options} "${name}.gb" ${cbmc_options}

regression/goto-cc-static/keep_static-1/main.c

@@ -0,0 +1,8 @@
+static int foo()
+{
+  return 3;
+}
+
+int main()
+{
+}

regression/goto-cc-static/keep_static-1/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+foo --show-symbol-table
+
+^EXIT=0$
+^SIGNAL=0$
+^Symbol......: foo$
+--
+^warning: ignoring

regression/goto-cc-static/keep_static-2/main.c

@@ -0,0 +1,8 @@
+static int foo()
+{
+  return 3;
+}
+
+int main()
+{
+}

regression/goto-cc-static/keep_static-2/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+main --show-symbol-table
+
+^EXIT=0$
+^SIGNAL=0$
+^Symbol......: main$
+--
+^Symbol......: foo$

regression/goto-cc-static/keep_static-3/main.c

@@ -0,0 +1,18 @@
+static int baz()
+{
+  return 3;
+}
+
+static int bar()
+{
+  return 3;
+}
+
+static int foo()
+{
+  return 3;
+}
+
+int main()
+{
+}

regression/goto-cc-static/keep_static-3/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+foo,bar --show-symbol-table
+
+^EXIT=0$
+^SIGNAL=0$
+^Symbol......: foo$
+^Symbol......: bar$
+--
+^Symbol......: baz$

src/ansi-c/ansi_c_language.cpp

@@ -119,7 +119,7 @@ bool ansi_c_languaget::prv_typecheck(
     return true;
   }
 
-  if(remove_internal_symbols(new_symbol_table, *this))
+  if(remove_internal_symbols(new_symbol_table, symbols_to_keep, *this))
     return true;
 
   if(linking(symbol_table, new_symbol_table, get_message_handler()))

src/goto-cc/compile.cpp

@@ -593,7 +593,7 @@ bool compilet::parse_source(const std::string &file_name)
     return true;
 
   // we just typecheck one file here
-  if(language_files.typecheck(goto_model.symbol_table))
+  if(language_files.typecheck(goto_model.symbol_table, symbols_to_keep))
   {
     error() << "CONVERSION ERROR" << eom;
     return true;
@@ -613,13 +613,20 @@ bool compilet::parse_source(const std::string &file_name)
 compilet::compilet(cmdlinet &_cmdline, message_handlert &mh, bool Werror)
   : messaget(mh),
     ns(goto_model.symbol_table),
+    symbols_to_keep(),
     cmdline(_cmdline),
     warning_is_fatal(Werror)
 {
   mode=COMPILE_LINK_EXECUTABLE;
   echo_file_name=false;
   wrote_object=false;
   working_directory=get_current_working_directory();
+  if(cmdline.isset("keep-implementations"))
+  {
+    std::list<std::string> csv =
+      cmdline.get_comma_separated_values("keep-implementations");
+    symbols_to_keep.insert(csv.begin(), csv.end());
+  }
 }
 
 /// cleans up temporary files

src/goto-cc/compile.h

@@ -92,6 +92,9 @@ class compilet : public messaget
         to_code_type(pair.second.type).parameters().size()});
   }
 
+  /// \brief Non-exported symbols that this compiler should NOT remove.
+  std::set<std::string> symbols_to_keep;
+
 protected:
   cmdlinet &cmdline;
   bool warning_is_fatal;

src/goto-cc/gcc_cmdline.cpp

@@ -27,6 +27,7 @@ const char *goto_cc_options_with_separated_argument[]=
   "--native-compiler",
   "--native-linker",
   "--print-rejected-preprocessed-source",
+  "--keep-implementations",
   nullptr
 };
 

src/goto-cc/gcc_mode.cpp

@@ -387,6 +387,20 @@ int gcc_modet::doit()
     return EX_OK; // Exit!
   }
 
+  if(cmdline.isset("keep-implementations"))
+  {
+    const std::list<std::string> csv =
+      cmdline.get_comma_separated_values("keep-implementations");
+    if(csv.empty())
+    {
+      error() << "Supply a comma-separated list of functions and variables to"
+                 " keep their implementations"
+              << eom;
+      return EX_USAGE;
+    }
+    compiler.symbols_to_keep.insert(csv.begin(), csv.end());
+  }
+
   if(
     cmdline.isset("dumpmachine") || cmdline.isset("dumpspecs") ||
     cmdline.isset("dumpversion") || cmdline.isset("print-sysroot") ||

src/goto-cc/ms_cl_mode.cpp

@@ -65,6 +65,20 @@ int ms_cl_modet::doit()
 
   debug() << "Visual Studio mode " << ms_cl_version << eom;
 
+  if(cmdline.isset("keep-implementations"))
+  {
+    const std::list<std::string> csv =
+      cmdline.get_comma_separated_values("keep-implementations");
+    if(csv.empty())
+    {
+      error() << "Supply a comma-separated list of functions and variables to"
+                 " keep their implementations"
+              << eom;
+      return EX_USAGE;
+    }
+    compiler.symbols_to_keep.insert(csv.begin(), csv.end());
+  }
+
   // model validation
   compiler.validate_goto_model = cmdline.isset("validate-goto-model");
 

src/langapi/language_file.cpp

@@ -82,7 +82,9 @@ bool language_filest::parse()
   return false;
 }
 
-bool language_filest::typecheck(symbol_tablet &symbol_table)
+bool language_filest::typecheck(
+  symbol_tablet &symbol_table,
+  const std::set<std::string> &symbols_to_keep)
 {
   // typecheck interfaces
 
@@ -129,7 +131,7 @@ bool language_filest::typecheck(symbol_tablet &symbol_table)
   {
     if(file.second.modules.empty())
     {
-      if(file.second.language->typecheck(symbol_table, ""))
+      if(file.second.language->typecheck(symbol_table, "", symbols_to_keep))
         return true;
       // register lazy methods.
       // TODO: learn about modules and generalise this
@@ -145,7 +147,7 @@ bool language_filest::typecheck(symbol_tablet &symbol_table)
 
   for(auto &module : module_map)
   {
-    if(typecheck_module(symbol_table, module.second))
+    if(typecheck_module(symbol_table, module.second, symbols_to_keep))
       return true;
   }
 
@@ -195,7 +197,8 @@ bool language_filest::interfaces(
 
 bool language_filest::typecheck_module(
   symbol_tablet &symbol_table,
-  const std::string &module)
+  const std::string &module,
+  const std::set<std::string> &symbols_to_keep)
 {
   // check module map
 
@@ -207,12 +210,13 @@ bool language_filest::typecheck_module(
     return true;
   }
 
-  return typecheck_module(symbol_table, it->second);
+  return typecheck_module(symbol_table, it->second, symbols_to_keep);
 }
 
 bool language_filest::typecheck_module(
   symbol_tablet &symbol_table,
-  language_modulet &module)
+  language_modulet &module,
+  const std::set<std::string> &symbols_to_keep)
 {
   // already typechecked?
 
@@ -240,7 +244,7 @@ bool language_filest::typecheck_module(
       it!=dependency_set.end();
       it++)
   {
-    if(typecheck_module(symbol_table, *it))
+    if(typecheck_module(symbol_table, *it, symbols_to_keep))
     {
       module.in_progress=false;
       return true;
@@ -251,7 +255,8 @@ bool language_filest::typecheck_module(
 
   status() << "Type-checking " << module.name << eom;
 
-  if(module.file->language->typecheck(symbol_table, module.name))
+  if(module.file->language->typecheck(
+       symbol_table, module.name, symbols_to_keep))
   {
     module.in_progress=false;
     return true;

src/langapi/language_file.h

@@ -107,7 +107,9 @@ class language_filest:public messaget
 
   bool generate_support_functions(symbol_tablet &symbol_table);
 
-  bool typecheck(symbol_tablet &symbol_table);
+  bool typecheck(
+    symbol_tablet &symbol_table,
+    const std::set<std::string> &symbols_to_keep = {});
 
   bool final(symbol_table_baset &symbol_table);
 
@@ -141,11 +143,13 @@ class language_filest:public messaget
 protected:
   bool typecheck_module(
     symbol_tablet &symbol_table,
-    language_modulet &module);
+    language_modulet &module,
+    const std::set<std::string> &symbols_to_keep);
 
   bool typecheck_module(
     symbol_tablet &symbol_table,
-    const std::string &module);
+    const std::string &module,
+    const std::set<std::string> &symbols_to_keep);
 };
 
 #endif // CPROVER_UTIL_LANGUAGE_FILE_H

src/linking/remove_internal_symbols.cpp

@@ -19,6 +19,8 @@ Author: Daniel Kroening
 
 #include "static_lifetime_init.h"
 
+#include <algorithm>
+
 static void get_symbols(
   const namespacet &ns,
   const symbolt &in_symbol,
@@ -66,12 +68,17 @@ static void get_symbols(
 /// * non-static function with body that is not extern inline
 /// * symbol used in an EXPORTED symbol
 /// * type used in an EXPORTED symbol
+/// * we also consider a symbol to be EXPORTED if it is a member of
+///   `symbols_to_keep`.
 ///
 ///          Read
 ///          http://gcc.gnu.org/ml/gcc/2006-11/msg00006.html
 ///          on "extern inline"
 /// \param symbol_table: symbol table to clean up
-bool remove_internal_symbols(symbol_tablet &symbol_table, messaget &log)
+bool remove_internal_symbols(
+  symbol_tablet &symbol_table,
+  const std::set<std::string> &symbols_to_keep,
+  messaget &log)
 {
   namespacet ns(symbol_table);
   find_symbols_sett exported;
@@ -89,6 +96,10 @@ bool remove_internal_symbols(symbol_tablet &symbol_table, messaget &log)
   special.insert(CPROVER_PREFIX "dead_object");
   special.insert(CPROVER_PREFIX "rounding_mode");
 
+  find_symbols_sett user_kept;
+  user_kept.insert(symbols_to_keep.begin(), symbols_to_keep.end());
+  find_symbols_sett user_found;
+
   for(symbol_tablet::symbolst::const_iterator
       it=symbol_table.symbols.begin();
       it!=symbol_table.symbols.end();
@@ -101,6 +112,14 @@ bool remove_internal_symbols(symbol_tablet &symbol_table, messaget &log)
     // not marked yet
     const symbolt &symbol=it->second;
 
+    if(user_kept.find(symbol.name) != user_kept.end())
+    {
+      log.debug() << "Keeping symbol '" << symbol.name << "'" << log.eom;
+      get_symbols(ns, symbol, exported);
+      user_found.insert(symbol.name);
+      continue;
+    }
+
     if(special.find(symbol.name)!=special.end())
     {
       get_symbols(ns, symbol, exported);
@@ -147,6 +166,25 @@ bool remove_internal_symbols(symbol_tablet &symbol_table, messaget &log)
     }
   }
 
+#if 0
+  std::vector<irep_idt> diff;
+  std::set_difference(
+      user_kept.begin(),
+      user_kept.end(),
+      user_found.begin(),
+      user_found.end(),
+      std::inserter(diff, diff.begin()));
+  if(!diff.empty())
+  {
+    log.error() << "Several symbols requested to be kept were not found"
+                   " in the object file: [";
+    for(const auto &sym : diff)
+      log.error() << sym << ", ";
+    log.error() << "]" << log.eom;
+    return true;
+  }
+#endif
+
   // remove all that are _not_ exported!
   for(symbol_tablet::symbolst::const_iterator
       it=symbol_table.symbols.begin();