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

tautschnig · tautschnig · commit 103c84eb09e6 · 2021-09-10T21:45:51.000Z
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.
diff --git a/doc/architectural/static-functions.md b/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
diff --git a/regression/goto-cc-file-local/chain.sh b/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
diff --git a/regression/goto-cc-file-local/selected-symbols/main.c b/regression/goto-cc-file-local/selected-symbols/main.c
@@ -0,0 +1,11 @@
+static int foo(int x) {
+  return x+1;
+}
+
+static int bar(int x) {
+  return x+2;
+}
+
+static int baz(int x) {
+  return x+2;
+}
diff --git a/regression/goto-cc-file-local/selected-symbols/test.desc b/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$
diff --git a/src/ansi-c/ansi_c_language.cpp b/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;
 
diff --git a/src/ansi-c/ansi_c_language.h b/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
   {
diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp
@@ -356,7 +356,7 @@ bool compilet::link(optionalt<symbol_tablet> &&symbol_table)
   if(keep_file_local)
   {
     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();
   }
 
@@ -427,7 +427,7 @@ optionalt<symbol_tablet> compilet::compile()
       if(keep_file_local)
       {
         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 +652,8 @@ 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") : "")
 {
diff --git a/src/goto-cc/compile.h b/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;
diff --git a/src/goto-cc/gcc_cmdline.cpp b/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
 };
 
diff --git a/src/goto-cc/ms_cl_cmdline.cpp b/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,7 @@ 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)
         {
diff --git a/src/goto-programs/name_mangler.h b/src/goto-programs/name_mangler.h
@@ -31,13 +31,14 @@ 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 +66,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 +139,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
diff --git a/src/langapi/language.h b/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,
diff --git a/src/langapi/language_file.cpp b/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?
 
diff --git a/src/langapi/language_file.h b/src/langapi/language_file.h
@@ -109,7 +109,7 @@ 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);
+  typecheck(symbol_tablet &symbol_table, const std::string &keep_file_local = "");
 
   bool final(symbol_table_baset &symbol_table);
 
@@ -144,12 +144,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
diff --git a/src/linking/remove_internal_symbols.cpp b/src/linking/remove_internal_symbols.cpp
@@ -99,12 +99,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 +176,8 @@ 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);
       }
diff --git a/src/linking/remove_internal_symbols.h b/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
diff --git a/src/statement-list/statement_list_language.cpp b/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;
 
diff --git a/src/statement-list/statement_list_language.h b/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;

Original file line number	Diff line number	Diff line change
`@@ -103,7 +103,7 @@ bool ansi_c_languaget::parse(`
`103`	`103`	`bool ansi_c_languaget::typecheck(`
`104`	`104`	`symbol_tablet &symbol_table,`
`105`	`105`	`const std::string &module,`
`106`		`- const bool keep_file_local)`
	`106`	`+ const std::string &keep_file_local)`
`107`	`107`	`{`
`108`	`108`	`symbol_tablet new_symbol_table;`
`109`	`109`
Original file line number	Diff line number	Diff line change
`@@ -54,7 +54,7 @@ class ansi_c_languaget:public languaget`
`54`	`54`	`bool typecheck(`
`55`	`55`	`symbol_tablet &symbol_table,`
`56`	`56`	`const std::string &module,`
`57`		`- const bool keep_file_local) override;`
	`57`	`+ const std::string &keep_file_local) override;`
`58`	`58`
`59`	`59`	`bool can_keep_file_local() override`
`60`	`60`	`{`
Original file line number	Diff line number	Diff line change
`@@ -356,7 +356,7 @@ bool compilet::link(optionalt<symbol_tablet> &&symbol_table)`
`356`	`356`	`if(keep_file_local)`
`357`	`357`	`{`
`358`	`358`	`function_name_manglert<file_name_manglert> mangler(`
`359`		`- log.get_message_handler(), goto_model, file_local_mangle_suffix);`
	`359`	`+ log.get_message_handler(), goto_model, file_local_mangle_suffix, keep_file_local);`
`360`	`360`	`mangler.mangle();`
`361`	`361`	`}`
`362`	`362`
`@@ -427,7 +427,7 @@ optionalt<symbol_tablet> compilet::compile()`
`427`	`427`	`if(keep_file_local)`
`428`	`428`	`{`
`429`	`429`	`function_name_manglert<file_name_manglert> mangler(`
`430`		`- log.get_message_handler(), file_goto_model, file_local_mangle_suffix);`
	`430`	`+ log.get_message_handler(), file_goto_model, file_local_mangle_suffix, keep_file_local);`
`431`	`431`	`mangler.mangle();`
`432`	`432`	`}`
`433`	`433`
`@@ -652,8 +652,8 @@ compilet::compilet(cmdlinet &_cmdline, message_handlert &mh, bool Werror)`
`652`	`652`	`warning_is_fatal(Werror),`
`653`	`653`	`keep_file_local(`
`654`	`654`	`// function-local is the old name and is still in use, but is misleading`
`655`		`- cmdline.isset("export-function-local-symbols") \|\|`
`656`		`- cmdline.isset("export-file-local-symbols")),`
	`655`	`+ (cmdline.isset("export-function-local-symbols") \|\|`
	`656`	`+ cmdline.isset("export-file-local-symbols")) ? ".*" : (cmdline.isset("export-file-local-symbol") ? cmdline.get_value("export-file-local-symbol") : "")),`
`657`	`657`	`file_local_mangle_suffix(`
`658`	`658`	`cmdline.isset("mangle-suffix") ? cmdline.get_value("mangle-suffix") : "")`
`659`	`659`	`{`