export-file-local-symbol A,B: selective export of file-local symbols

Previously, --export-file-local-symbols would mark (and mangle) all
file-local symbols. With --export-file-local-symbol A (or
--export-file-local-symbol A,B), only A (or A and B) will be mangled and
exported.

Author: tautschnig

doc/architectural/static-functions.md

@@ -92,7 +92,8 @@ We should now also write a harness for `private_function`. However,
 since that function is marked `static`, it is not possible for functions
 in external files to call it. We can write and link a harness by
 stripping the `static` attribute from `private_function` using goto-cc's
-`--export-file-local-symbols` flag.
+`--export-file-local-symbols` or `--export-file-local-symbol private_function`
+flag.
 
 \code{.sh}
 > goto-cc -c -o --export-file-local-symbols library_with_static.o library.c

regression/goto-cc-file-local/chain.sh

@@ -50,6 +50,9 @@ fi
 export_flag=""
 if is_in old-flag "$ALL_ARGS"; then
   export_flag="--export-function-local-symbols"
+elif is_in "export-[a-zA-Z0-9_,]*-only" "$ALL_ARGS"; then
+  suffix=${ALL_ARGS#*export-}
+  export_flag="--export-file-local-symbol ${suffix%-only*}"
 else
   export_flag="--export-file-local-symbols"
 fi

regression/goto-cc-file-local/selected-symbols/main.c

@@ -0,0 +1,14 @@
+static int foo(int x)
+{
+  return x + 1;
+}
+
+static int bar(int x)
+{
+  return x + 2;
+}
+
+static int baz(int x)
+{
+  return x + 2;
+}

regression/goto-cc-file-local/selected-symbols/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+export-foo,bar-only show-symbol-table
+^Symbol\.\.\.\.\.\.: __CPROVER_file_local_main_c_foo$
+^Symbol\.\.\.\.\.\.: __CPROVER_file_local_main_c_bar$
+^Symbol\.\.\.\.\.\.: baz$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^Symbol\.\.\.\.\.\.: __CPROVER_file_local_main_c_baz$

src/ansi-c/ansi_c_language.cpp

@@ -103,7 +103,7 @@ bool ansi_c_languaget::parse(
 bool ansi_c_languaget::typecheck(
   symbol_tablet &symbol_table,
   const std::string &module,
-  const bool keep_file_local)
+  const std::string &keep_file_local)
 {
   symbol_tablet new_symbol_table;
 

src/ansi-c/ansi_c_language.h

@@ -54,7 +54,7 @@ class ansi_c_languaget:public languaget
   bool typecheck(
     symbol_tablet &symbol_table,
     const std::string &module,
-    const bool keep_file_local) override;
+    const std::string &keep_file_local) override;
 
   bool can_keep_file_local() override
   {
@@ -64,7 +64,7 @@ class ansi_c_languaget:public languaget
   bool
   typecheck(symbol_tablet &symbol_table, const std::string &module) override
   {
-    return typecheck(symbol_table, module, true);
+    return typecheck(symbol_table, module, ".*");
   }
 
   void show_parse(std::ostream &out) override;

src/cpp/cpp_language.cpp

@@ -131,7 +131,7 @@ bool cpp_languaget::typecheck(
       cpp_parse_tree, new_symbol_table, module, get_message_handler()))
     return true;
 
-  remove_internal_symbols(new_symbol_table, get_message_handler(), false);
+  remove_internal_symbols(new_symbol_table, get_message_handler(), "");
 
   return linking(symbol_table, new_symbol_table, get_message_handler());
 }

src/goto-cc/compile.cpp

@@ -353,10 +353,13 @@ bool compilet::link(optionalt<symbol_tablet> &&symbol_table)
     convert_symbols(goto_model);
   }
 
-  if(keep_file_local)
+  if(!keep_file_local.empty())
   {
     function_name_manglert<file_name_manglert> mangler(
-      log.get_message_handler(), goto_model, file_local_mangle_suffix);
+      log.get_message_handler(),
+      goto_model,
+      file_local_mangle_suffix,
+      keep_file_local);
     mangler.mangle();
   }
 
@@ -424,10 +427,13 @@ optionalt<symbol_tablet> compilet::compile()
       else
         cfn = output_file_object;
 
-      if(keep_file_local)
+      if(!keep_file_local.empty())
       {
         function_name_manglert<file_name_manglert> mangler(
-          log.get_message_handler(), file_goto_model, file_local_mangle_suffix);
+          log.get_message_handler(),
+          file_goto_model,
+          file_local_mangle_suffix,
+          keep_file_local);
         mangler.mangle();
       }
 
@@ -652,8 +658,12 @@ compilet::compilet(cmdlinet &_cmdline, message_handlert &mh, bool Werror)
     warning_is_fatal(Werror),
     keep_file_local(
       // function-local is the old name and is still in use, but is misleading
-      cmdline.isset("export-function-local-symbols") ||
-      cmdline.isset("export-file-local-symbols")),
+      (cmdline.isset("export-function-local-symbols") ||
+       cmdline.isset("export-file-local-symbols"))
+        ? ".*"
+        : (cmdline.isset("export-file-local-symbol")
+             ? cmdline.get_value("export-file-local-symbol")
+             : "")),
     file_local_mangle_suffix(
       cmdline.isset("mangle-suffix") ? cmdline.get_value("mangle-suffix") : "")
 {

src/goto-cc/compile.h

@@ -111,7 +111,7 @@ class compilet
   bool warning_is_fatal;
 
   /// \brief Whether to keep implementations of file-local symbols
-  const bool keep_file_local;
+  const std::string keep_file_local;
 
   /// \brief String to include in all mangled names
   const std::string file_local_mangle_suffix;

src/goto-cc/gcc_cmdline.cpp

@@ -28,6 +28,7 @@ const char *goto_cc_options_with_separated_argument[]=
   "--print-rejected-preprocessed-source",
   "--mangle-suffix",
   "--object-bits",
+  "--export-file-local-symbol",
   nullptr
 };
 

src/goto-cc/ms_cl_cmdline.cpp

@@ -47,6 +47,7 @@ const char *non_ms_cl_options[]=
   "--validate-goto-model",
   "--export-file-local-symbols",
   "--mangle-suffix",
+  "--export-file-local-symbol",
   nullptr
 };
 // clang-format on
@@ -62,7 +63,8 @@ bool ms_cl_cmdlinet::parse(const std::vector<std::string> &arguments)
 
       if(
         arguments[i] == "--verbosity" || arguments[i] == "--function" ||
-        arguments[i] == "--mangle-suffix")
+        arguments[i] == "--mangle-suffix" ||
+        arguments[i] == "--export-file-local-symbol")
       {
         if(i < arguments.size() - 1)
         {

src/goto-programs/name_mangler.h

@@ -31,13 +31,18 @@ class function_name_manglert
 {
 public:
   /// \param mh: handler to construct a log from
-  /// \param gm: mangle all names in gm's symbol table and goto program
+  /// \param gm: mangle names in gm's symbol table and goto program
   /// \param extra_info: a string to be included in each mangled name
   function_name_manglert(
     message_handlert &mh,
     goto_modelt &gm,
-    const std::string &extra_info)
-    : log(mh), model(gm), mangle_fun(), extra_info(extra_info)
+    const std::string &extra_info,
+    const std::string &needs_mangling)
+    : log(mh),
+      model(gm),
+      mangle_fun(),
+      extra_info(extra_info),
+      needs_mangling(needs_mangling)
   {
   }
 
@@ -65,6 +70,8 @@ class function_name_manglert
         continue;
       if(!sym.is_file_local)
         continue;
+      if(!std::regex_match(id2string(sym.name), needs_mangling))
+        continue;
 
       const irep_idt mangled = mangle_fun(sym, extra_info);
       symbolt new_sym;
@@ -136,6 +143,7 @@ class function_name_manglert
   goto_modelt &model;
   MangleFun mangle_fun;
   const std::string &extra_info;
+  const std::regex needs_mangling;
 };
 
 /// \brief Mangle identifiers by including their filename

src/langapi/language.h

@@ -140,7 +140,7 @@ class languaget:public messaget
   virtual bool typecheck(
     symbol_tablet &symbol_table,
     const std::string &module,
-    const bool keep_file_local)
+    const std::string &keep_file_local)
   {
     INVARIANT(
       false,

src/langapi/language_file.cpp

@@ -82,7 +82,7 @@ bool language_filest::parse()
 
 bool language_filest::typecheck(
   symbol_tablet &symbol_table,
-  const bool keep_file_local)
+  const std::string &keep_file_local)
 {
   // typecheck interfaces
 
@@ -204,7 +204,7 @@ bool language_filest::interfaces(
 bool language_filest::typecheck_module(
   symbol_tablet &symbol_table,
   const std::string &module,
-  const bool keep_file_local)
+  const std::string &keep_file_local)
 {
   // check module map
 
@@ -222,7 +222,7 @@ bool language_filest::typecheck_module(
 bool language_filest::typecheck_module(
   symbol_tablet &symbol_table,
   language_modulet &module,
-  const bool keep_file_local)
+  const std::string &keep_file_local)
 {
   // already typechecked?
 

src/langapi/language_file.h

@@ -108,8 +108,9 @@ class language_filest:public messaget
 
   bool generate_support_functions(symbol_tablet &symbol_table);
 
-  bool
-  typecheck(symbol_tablet &symbol_table, const bool keep_file_local = false);
+  bool typecheck(
+    symbol_tablet &symbol_table,
+    const std::string &keep_file_local = "");
 
   bool final(symbol_table_baset &symbol_table);
 
@@ -144,12 +145,12 @@ class language_filest:public messaget
   bool typecheck_module(
     symbol_tablet &symbol_table,
     language_modulet &module,
-    const bool keep_file_local);
+    const std::string &keep_file_local);
 
   bool typecheck_module(
     symbol_tablet &symbol_table,
     const std::string &module,
-    const bool keep_file_local);
+    const std::string &keep_file_local);
 };
 
 #endif // CPROVER_UTIL_LANGUAGE_FILE_H

src/linking/remove_internal_symbols.cpp

@@ -22,6 +22,8 @@ Author: Daniel Kroening
 
 #include "static_lifetime_init.h"
 
+#include <regex>
+
 static void get_symbols(
   const namespacet &ns,
   const symbolt &in_symbol,
@@ -99,12 +101,12 @@ static void get_symbols(
 ///          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
+/// \param keep_file_local: regular expression over symbols to keep even if we
 ///                         would otherwise remove them
 void remove_internal_symbols(
   symbol_tablet &symbol_table,
   message_handlert &mh,
-  const bool keep_file_local)
+  const std::string &keep_file_local)
 {
   namespacet ns(symbol_table);
   find_symbols_sett exported;
@@ -176,7 +178,9 @@ void remove_internal_symbols(
       {
         get_symbols(ns, symbol, exported);
       }
-      else if(has_body && is_file_local && keep_file_local)
+      else if(
+        has_body && is_file_local && !keep_file_local.empty() &&
+        std::regex_match(id2string(symbol.name), std::regex(keep_file_local)))
       {
         get_symbols(ns, symbol, exported);
       }

src/linking/remove_internal_symbols.h

@@ -12,11 +12,13 @@ Author: Daniel Kroening
 #ifndef CPROVER_LINKING_REMOVE_INTERNAL_SYMBOLS_H
 #define CPROVER_LINKING_REMOVE_INTERNAL_SYMBOLS_H
 
+#include <string>
+
 class message_handlert;
 
 void remove_internal_symbols(
   class symbol_tablet &symbol_table,
   message_handlert &,
-  const bool);
+  const std::string &);
 
 #endif // CPROVER_LINKING_REMOVE_INTERNAL_SYMBOLS_H

src/statement-list/statement_list_language.cpp

@@ -36,7 +36,7 @@ bool statement_list_languaget::generate_support_functions(
 bool statement_list_languaget::typecheck(
   symbol_tablet &symbol_table,
   const std::string &module,
-  const bool keep_file_local)
+  const std::string &keep_file_local)
 {
   symbol_tablet new_symbol_table;
 
@@ -85,7 +85,7 @@ bool statement_list_languaget::typecheck(
   symbol_tablet &symbol_table,
   const std::string &module)
 {
-  return typecheck(symbol_table, module, true);
+  return typecheck(symbol_table, module, ".*");
 }
 
 bool statement_list_languaget::from_expr(

src/statement-list/statement_list_language.h

@@ -43,13 +43,14 @@ class statement_list_languaget : public languaget
   ///   If the symbol table is not empty when calling this function, its
   ///   contents are merged with the new entries.
   /// \param module: Name of the file that has been parsed.
-  /// \param keep_file_local: Set to true if local variables of this module
-  ///   should be included in the table.
+  /// \param keep_file_local: Set to non-empty string that is used as regular
+  ///   expression over local variable names that must not be cleaned from the
+  ///   symbol table.
   /// \return False if no errors occurred, true otherwise.
   bool typecheck(
     symbol_tablet &symbol_table,
     const std::string &module,
-    const bool keep_file_local) override;
+    const std::string &keep_file_local) override;
 
   bool
   typecheck(symbol_tablet &symbol_table, const std::string &module) override;