export-file-local-symbol(s): support file-local objects

Previously, only function names were mangled and exported. To enable
access to file-local objects (of static lifetime), also support mangling
their names.

Author: tautschnig

regression/goto-cc-file-local/objects/main.c

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

regression/goto-cc-file-local/objects/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+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::x$

src/goto-cc/compile.cpp

@@ -356,7 +356,7 @@ bool compilet::link(optionalt<symbol_tablet> &&symbol_table)
 
   if(!keep_file_local.empty())
   {
-    function_name_manglert<file_name_manglert> mangler(
+    file_local_name_manglert<file_name_manglert> mangler(
       log.get_message_handler(),
       goto_model,
       file_local_mangle_suffix,
@@ -430,7 +430,7 @@ optionalt<symbol_tablet> compilet::compile()
 
       if(!keep_file_local.empty())
       {
-        function_name_manglert<file_name_manglert> mangler(
+        file_local_name_manglert<file_name_manglert> mangler(
           log.get_message_handler(),
           file_goto_model,
           file_local_mangle_suffix,

src/goto-programs/name_mangler.h

@@ -27,15 +27,15 @@
 /// mangled name of its \ref symbolt argument, incorporating the second
 /// argument into the mangled name if possible.
 template <class MangleFun>
-class function_name_manglert
+class file_local_name_manglert
 {
 public:
   /// \param mh: handler to construct a log from
   /// \param gm: mangle names in gm's symbol table and goto program
   /// \param extra_info: a string to be included in each mangled name
   /// \param needs_mangling: a regular expression describing names that need to
   ///   be mangled.
-  function_name_manglert(
+  file_local_name_manglert(
     message_handlert &mh,
     goto_modelt &gm,
     const std::string &extra_info,
@@ -48,7 +48,7 @@ class function_name_manglert
   {
   }
 
-  /// \brief Mangle all file-local function symbols in the program
+  /// \brief Mangle all file-local non-type global-scoped symbols in the program
   ///
   /// The way in which the symbols will be mangled is decided by which mangler
   /// type this object is instantiated with, e.g. DJB_manglert mangles the path
@@ -66,11 +66,14 @@ class function_name_manglert
     {
       const symbolt &sym = sym_it->second;
 
-      if(sym.type.id() != ID_code) // is not a function
+      if(!sym.is_file_local)
         continue;
-      if(sym.value.is_nil()) // has no body
+      if(sym.is_type)
         continue;
-      if(!sym.is_file_local)
+      // no name mangling for functions without body
+      if(sym.type.id() == ID_code && sym.value.is_nil())
+        continue;
+      if(sym.type.id() != ID_code && !sym.is_static_lifetime)
         continue;
       if(!std::regex_match(id2string(sym.name), needs_mangling))
         continue;
@@ -85,7 +88,8 @@ class function_name_manglert
       old_syms.push_back(sym_it);
 
       rename.insert(sym.symbol_expr(), new_sym.symbol_expr());
-      renamed_funs.insert(std::make_pair(sym.name, mangled));
+      if(sym.type.id() == ID_code)
+        renamed_funs.insert(std::make_pair(sym.name, mangled));
 
       log.debug() << "Mangling: " << sym.name << " -> " << mangled << log.eom;
     }

src/linking/remove_internal_symbols.cpp

@@ -189,8 +189,12 @@ void remove_internal_symbols(
     {
       // 'extern' symbols are only exported if there
       // is an initializer.
-      if((has_initializer || !symbol.is_extern) &&
-         !is_file_local)
+      if(
+        (has_initializer || !symbol.is_extern) &&
+        (!is_file_local ||
+         (symbol.is_static_lifetime && !keep_file_local.empty() &&
+          std::regex_match(
+            id2string(symbol.name), std::regex(keep_file_local)))))
       {
         get_symbols(ns, symbol, exported);
       }