From 1f18a3da408ac65ef7a26c422e75046f2460105b Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 10 Sep 2021 20:09:25 +0000
Subject: [PATCH] export-file-local_symbols:: update base name and pretty name

Name mangling via --export-file-local-symbols used to introduce symbols
the name of which did not match the base name. Forward declarations of
the mangled name, however, did introduce a symbol where (mangled) name
and base name match. When linking later found the definition
corresponding to such a forward declaration, the base name (and pretty
name) were not updated. As a consequence the order of linking produced
two different final symbol tables.

Note that Crangler may be a superior alternative avoiding such problems,
but there is ample code that still uses `--export-file-local-symbols`.
---
 regression/goto-cc-file-local/base-name-1/file1.c   |  7 +++++++
 regression/goto-cc-file-local/base-name-1/file2.c   |  9 +++++++++
 regression/goto-cc-file-local/base-name-1/test.desc | 13 +++++++++++++
 regression/goto-cc-file-local/base-name-2/file1.c   |  9 +++++++++
 regression/goto-cc-file-local/base-name-2/file2.c   |  7 +++++++
 regression/goto-cc-file-local/base-name-2/test.desc | 13 +++++++++++++
 .../test.desc                                       |  3 +--
 src/goto-programs/name_mangler.h                    |  3 +++
 8 files changed, 62 insertions(+), 2 deletions(-)
 create mode 100644 regression/goto-cc-file-local/base-name-1/file1.c
 create mode 100644 regression/goto-cc-file-local/base-name-1/file2.c
 create mode 100644 regression/goto-cc-file-local/base-name-1/test.desc
 create mode 100644 regression/goto-cc-file-local/base-name-2/file1.c
 create mode 100644 regression/goto-cc-file-local/base-name-2/file2.c
 create mode 100644 regression/goto-cc-file-local/base-name-2/test.desc

diff --git a/regression/goto-cc-file-local/base-name-1/file1.c b/regression/goto-cc-file-local/base-name-1/file1.c
new file mode 100644
index 00000000000..3cdccb87301
--- /dev/null
+++ b/regression/goto-cc-file-local/base-name-1/file1.c
@@ -0,0 +1,7 @@
+int __CPROVER_file_local_file2_c_foo(int x);
+
+int main()
+{
+  int x = __CPROVER_file_local_file2_c_foo(1);
+  __CPROVER_assert(x == 2, "x == 2");
+}
diff --git a/regression/goto-cc-file-local/base-name-1/file2.c b/regression/goto-cc-file-local/base-name-1/file2.c
new file mode 100644
index 00000000000..d8031af5eba
--- /dev/null
+++ b/regression/goto-cc-file-local/base-name-1/file2.c
@@ -0,0 +1,9 @@
+static int foo(int x)
+{
+  return x + 1;
+}
+
+static int bar(int x)
+{
+  return x + 2;
+}
diff --git a/regression/goto-cc-file-local/base-name-1/test.desc b/regression/goto-cc-file-local/base-name-1/test.desc
new file mode 100644
index 00000000000..2b4d4092811
--- /dev/null
+++ b/regression/goto-cc-file-local/base-name-1/test.desc
@@ -0,0 +1,13 @@
+CORE
+file1.c
+final-link show-symbol-table assertion-check
+^Base name\.\.\.: __CPROVER_file_local_.*_foo$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^Base name\.\.\.: foo$
+--
+The linking order must not affect the base name of the mangled symbol. See
+base-name-2 for a test that will yield a different linking order (while still
+producing the same base name).
diff --git a/regression/goto-cc-file-local/base-name-2/file1.c b/regression/goto-cc-file-local/base-name-2/file1.c
new file mode 100644
index 00000000000..d8031af5eba
--- /dev/null
+++ b/regression/goto-cc-file-local/base-name-2/file1.c
@@ -0,0 +1,9 @@
+static int foo(int x)
+{
+  return x + 1;
+}
+
+static int bar(int x)
+{
+  return x + 2;
+}
diff --git a/regression/goto-cc-file-local/base-name-2/file2.c b/regression/goto-cc-file-local/base-name-2/file2.c
new file mode 100644
index 00000000000..81b647d5f83
--- /dev/null
+++ b/regression/goto-cc-file-local/base-name-2/file2.c
@@ -0,0 +1,7 @@
+int __CPROVER_file_local_file1_c_foo(int x);
+
+int main()
+{
+  int x = __CPROVER_file_local_file1_c_foo(1);
+  __CPROVER_assert(x == 2, "x == 2");
+}
diff --git a/regression/goto-cc-file-local/base-name-2/test.desc b/regression/goto-cc-file-local/base-name-2/test.desc
new file mode 100644
index 00000000000..e2e8684025b
--- /dev/null
+++ b/regression/goto-cc-file-local/base-name-2/test.desc
@@ -0,0 +1,13 @@
+CORE
+file1.c
+final-link show-symbol-table assertion-check
+^Base name\.\.\.: __CPROVER_file_local_.*_foo$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^Base name\.\.\.: foo$
+--
+The linking order must not affect the base name of the mangled symbol. See
+base-name-1 for a test that will yield a different linking order (while still
+producing the same base name).
diff --git a/regression/goto-cc-goto-analyzer/reachable-functions-export-file-local-symbols/test.desc b/regression/goto-cc-goto-analyzer/reachable-functions-export-file-local-symbols/test.desc
index bf698744a96..b856adf9f18 100644
--- a/regression/goto-cc-goto-analyzer/reachable-functions-export-file-local-symbols/test.desc
+++ b/regression/goto-cc-goto-analyzer/reachable-functions-export-file-local-symbols/test.desc
@@ -1,11 +1,10 @@
 CORE
 test.c
 --reachable-functions
-^.* foo 1 4$
+^.* __CPROVER_file_local_project_c_foo 1 4$
 ^EXIT=0$
 ^SIGNAL=0$
 --
-^.* [a-zA-Z0-9_]+foo \d+ \d+$
 --
 This test checks that after building the goto binary (see test.sh) with
 --export-file-local-symbols function "foo" is still reported as reachable. Note,
diff --git a/src/goto-programs/name_mangler.h b/src/goto-programs/name_mangler.h
index ab6382a834d..df206bfbb63 100644
--- a/src/goto-programs/name_mangler.h
+++ b/src/goto-programs/name_mangler.h
@@ -70,6 +70,9 @@ class function_name_manglert
       symbolt new_sym;
       new_sym = sym;
       new_sym.name = mangled;
+      new_sym.base_name = mangled;
+      if(new_sym.pretty_name.empty())
+        new_sym.pretty_name = sym.base_name;
       new_sym.is_file_local = false;
 
       new_syms.push_back(new_sym);