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

@@ -23,6 +23,7 @@ Date: June 2006
 #include <util/get_base_name.h>
 #include <util/prefix.h>
 #include <util/run.h>
+#include <util/string_utils.h>
 #include <util/symbol_table_builder.h>
 #include <util/tempdir.h>
 #include <util/tempfile.h>
@@ -353,10 +354,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 +428,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();
       }
 
@@ -645,18 +652,44 @@ optionalt<symbol_tablet> compilet::parse_source(const std::string &file_name)
   return std::move(file_symbol_table);
 }
 
+/// Combine the elements of \p values to a regular expression denoting
+/// alternatives. Each element of \p values may in turn be a sequence of
+/// comma-separated values, which are also expanded to contribute to the overall
+/// collection of alternatives.
+static std::string csv_to_pattern(const std::list<std::string> &values)
+{
+  std::string result;
+
+  for(const auto& csv : values)
+  {
+    for(const auto &name : split_string(csv, ','))
+    {
+      if(!result.empty())
+        result += '|';
+      result += name;
+    }
+  }
+
+  return result;
+}
+
 /// constructor
 compilet::compilet(cmdlinet &_cmdline, message_handlert &mh, bool Werror)
   : log(mh),
     cmdline(_cmdline),
     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")
+             ? csv_to_pattern(cmdline.get_values("export-file-local-symbol"))
+             : "")),
     file_local_mangle_suffix(
       cmdline.isset("mangle-suffix") ? cmdline.get_value("mangle-suffix") : "")
 {
+  log.warning() << "file-local: " << keep_file_local << messaget::eom;
   mode=COMPILE_LINK_EXECUTABLE;
   echo_file_name=false;
   wrote_object=false;

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
 };