Merge pull request #4563 from tautschnig/fix-name-mangling

Export-function-local-symbols name mangling: rename initial values

Author: tautschnig

regression/Makefile

@@ -25,6 +25,7 @@ DIRS = cbmc \
        goto-cc-goto-analyzer \
        systemc \
        contracts \
+       goto-cc-file-local \
        # Empty last line
 
 # Run all test directories in sequence

regression/goto-cc-file-local/Makefile

@@ -0,0 +1,35 @@
+default: tests.log
+
+include ../../src/config.inc
+include ../../src/common
+
+ifeq ($(BUILD_ENV_),MSVC)
+	exe=../../../src/goto-cc/goto-cl
+	is_windows=true
+else
+	exe=../../../src/goto-cc/goto-cc
+	is_windows=false
+endif
+
+test:
+	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/cbmc/cbmc $(is_windows)'
+
+tests.log:
+	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/cbmc/cbmc $(is_windows)'
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;
+
+clean:
+	@for dir in *; do \
+		$(RM) tests.log; \
+		if [ -d "$$dir" ]; then \
+			cd "$$dir"; \
+			$(RM) *.out *.gb; \
+			cd ..; \
+		fi \
+	done

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

@@ -4,6 +4,8 @@
 #
 # Author: Kareem Khazem <[email protected]>
 
+set -e
+
 is_in()
 {
   [[ "$2" =~ $1 ]] && return 0 || return 1
@@ -81,6 +83,7 @@ done
 
 if is_in final-link "$ALL_ARGS"; then
   OUT_FILE=final-link.gb
+  rm -f ${OUT_FILE}
   if [[ "${is_windows}" == "true" ]]; then
     "${goto_cc}"                        \
         --export-function-local-symbols \

regression/goto-cc-file-local/function-pointer/main.c

@@ -0,0 +1,14 @@
+#include <assert.h>
+
+static int foo()
+{
+  return 3;
+}
+
+int (*fptrs[])(void) = {foo};
+
+int main()
+{
+  int x = fptrs[0]();
+  assert(x == 3);
+}

regression/goto-cc-file-local/function-pointer/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+final-link assertion-check
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^\*\*\*\* WARNING: no body for function

src/goto-programs/name_mangler.h

@@ -84,6 +84,20 @@ class function_name_manglert
     for(const auto &sym : old_syms)
       model.symbol_table.erase(sym);
 
+    for(const auto &sym_pair : model.symbol_table)
+    {
+      const symbolt &sym = sym_pair.second;
+
+      exprt e = sym.value;
+      typet t = sym.type;
+      if(rename(e) && rename(t))
+        continue;
+
+      symbolt &new_sym = model.symbol_table.get_writeable_ref(sym.name);
+      new_sym.value = e;
+      new_sym.type = t;
+    }
+
     for(auto &fun : model.goto_functions.function_map)
     {
       if(!fun.second.body_available())

src/util/rename_symbol.h

@@ -43,14 +43,18 @@ class rename_symbolt
     type_map.insert(std::pair<irep_idt, irep_idt>(old_id, new_id));
   }
 
-  void operator()(exprt &dest) const
+  /// Rename symbols in \p dest.
+  /// \return True if, and only if, the expression was not modified.
+  bool operator()(exprt &dest) const
   {
-    rename(dest);
+    return rename(dest);
   }
 
-  void operator()(typet &dest) const
+  /// Rename symbols in \p dest.
+  /// \return True if, and only if, the type was not modified.
+  bool operator()(typet &dest) const
   {
-    rename(dest);
+    return rename(dest);
   }
 
   rename_symbolt();