From ac069cfa04dc8222983835807bf12484c39b8cf1 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 10 Sep 2021 20:46:22 +0000
Subject: [PATCH] goto-analyzer --(un)reachable-functions should not rely on
 base names

Functions are called by their symbol names, not their base names. The
output may still safely use the base name for more user-friendly
results, but call trees should not rely on a match of base names and
symbol names.

Fixes: #6330
---
 .../project.c                                     |  9 +++++++++
 .../proof.c                                       |  7 +++++++
 .../test.desc                                     | 13 +++++++++++++
 .../test.sh                                       | 15 +++++++++++++++
 src/goto-analyzer/unreachable_instructions.cpp    |  8 ++------
 5 files changed, 46 insertions(+), 6 deletions(-)
 create mode 100644 regression/goto-cc-goto-analyzer/reachable-functions-export-file-local-symbols/project.c
 create mode 100644 regression/goto-cc-goto-analyzer/reachable-functions-export-file-local-symbols/proof.c
 create mode 100644 regression/goto-cc-goto-analyzer/reachable-functions-export-file-local-symbols/test.desc
 create mode 100755 regression/goto-cc-goto-analyzer/reachable-functions-export-file-local-symbols/test.sh

diff --git a/regression/goto-cc-goto-analyzer/reachable-functions-export-file-local-symbols/project.c b/regression/goto-cc-goto-analyzer/reachable-functions-export-file-local-symbols/project.c
new file mode 100644
index 00000000000..d8031af5eba
--- /dev/null
+++ b/regression/goto-cc-goto-analyzer/reachable-functions-export-file-local-symbols/project.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-goto-analyzer/reachable-functions-export-file-local-symbols/proof.c b/regression/goto-cc-goto-analyzer/reachable-functions-export-file-local-symbols/proof.c
new file mode 100644
index 00000000000..d058baa5227
--- /dev/null
+++ b/regression/goto-cc-goto-analyzer/reachable-functions-export-file-local-symbols/proof.c
@@ -0,0 +1,7 @@
+int __CPROVER_file_local_project_c_foo(int x);
+
+int main()
+{
+  int x = __CPROVER_file_local_project_c_foo(1);
+  assert(x == 2);
+}
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
new file mode 100644
index 00000000000..bf698744a96
--- /dev/null
+++ b/regression/goto-cc-goto-analyzer/reachable-functions-export-file-local-symbols/test.desc
@@ -0,0 +1,13 @@
+CORE
+test.c
+--reachable-functions
+^.* 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,
+that the symbol representing "foo" has a mangled name in the goto binary, which
+makes the symbol name different from its base name.
diff --git a/regression/goto-cc-goto-analyzer/reachable-functions-export-file-local-symbols/test.sh b/regression/goto-cc-goto-analyzer/reachable-functions-export-file-local-symbols/test.sh
new file mode 100755
index 00000000000..3060552f4cb
--- /dev/null
+++ b/regression/goto-cc-goto-analyzer/reachable-functions-export-file-local-symbols/test.sh
@@ -0,0 +1,15 @@
+#!/usr/bin/env bash
+set -e
+
+goto_cc=$1
+is_windows=$2
+
+if [[ "${is_windows}" == "true" ]]; then
+  ${goto_cc} "/c" "/Foproject.gb" --export-file-local-symbols project.c
+  ${goto_cc} "/c" "/Foproof.gb" --export-file-local-symbols proof.c
+  ${goto_cc} "/Fetest.gb" project.gb proof.gb
+else
+  ${goto_cc} -o project.gb --export-file-local-symbols project.c
+  ${goto_cc} -o proof.gb --export-file-local-symbols proof.c
+  ${goto_cc} -o test.gb project.gb proof.gb
+fi
diff --git a/src/goto-analyzer/unreachable_instructions.cpp b/src/goto-analyzer/unreachable_instructions.cpp
index f2c10da5f29..c50703da2ce 100644
--- a/src/goto-analyzer/unreachable_instructions.cpp
+++ b/src/goto-analyzer/unreachable_instructions.cpp
@@ -179,10 +179,8 @@ void unreachable_instructions(
 
     const symbolt &decl = ns.lookup(gf_entry.first);
 
-    // gf_entry.first may be a link-time renamed version, use the
-    // base_name instead; do not list inlined functions
     if(
-      called.find(decl.base_name) != called.end() ||
+      called.find(decl.name) != called.end() ||
       to_code_type(decl.type).get_inlined())
     {
       unreachable_instructions(goto_program, dead_map);
@@ -314,10 +312,8 @@ static void list_functions(
   {
     const symbolt &decl = ns.lookup(gf_entry.first);
 
-    // gf_entry.first may be a link-time renamed version, use the
-    // base_name instead; do not list inlined functions
     if(
-      unreachable == (called.find(decl.base_name) != called.end() ||
+      unreachable == (called.find(decl.name) != called.end() ||
                       to_code_type(decl.type).get_inlined()))
     {
       continue;