From c4fdaf8f688269bf778fda861e2fc3f3e9ad4416 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 7 Dec 2022 14:36:45 +0000
Subject: [PATCH] Remove internal symbols: keep all symbols used in contracts

In beb1353cf2 we had chosen to only keep code-typed symbols, but indeed
we also need to retain objects (only) referred to from contracts.

Also add debug-level status information of what symbols are being
removed (which is information I have previously needed more than once in
debugging, and it's also now the only actual use of the messaget that we
already had in place).

Fixes: #7414
---
 regression/ansi-c/static5/main.c        | 24 ++++++++++++++++++++++++
 regression/ansi-c/static5/test.desc     |  8 ++++++++
 src/linking/remove_internal_symbols.cpp | 16 ++++++----------
 3 files changed, 38 insertions(+), 10 deletions(-)
 create mode 100644 regression/ansi-c/static5/main.c
 create mode 100644 regression/ansi-c/static5/test.desc

diff --git a/regression/ansi-c/static5/main.c b/regression/ansi-c/static5/main.c
new file mode 100644
index 00000000000..1a65cd2f622
--- /dev/null
+++ b/regression/ansi-c/static5/main.c
@@ -0,0 +1,24 @@
+typedef struct vtable_s
+{
+  int (*f)(void);
+} vtable_t;
+
+int return_0()
+{
+  return 0;
+}
+
+static vtable_t vtable_0 = {.f = &return_0};
+
+void foo(vtable_t *vtable)
+  __CPROVER_requires((void *)0 == vtable || &vtable_0 == vtable)
+{
+  if(vtable->f)
+    vtable->f();
+}
+
+int main()
+{
+  vtable_t *vtable;
+  foo(vtable);
+}
diff --git a/regression/ansi-c/static5/test.desc b/regression/ansi-c/static5/test.desc
new file mode 100644
index 00000000000..0107e934e51
--- /dev/null
+++ b/regression/ansi-c/static5/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--verbosity 10
+^Removing unused symbol
+^EXIT=0$
+^SIGNAL=0$
+--
+^Removing unused symbol vtable_0$
diff --git a/src/linking/remove_internal_symbols.cpp b/src/linking/remove_internal_symbols.cpp
index dc5218ae7fc..5c36f61ab50 100644
--- a/src/linking/remove_internal_symbols.cpp
+++ b/src/linking/remove_internal_symbols.cpp
@@ -76,16 +76,11 @@ static void get_symbols(
 
       for(const auto &s : new_symbols)
       {
-        // keep functions called in contracts within scope.
-        // should we keep local variables from the contract as well?
-        const symbolt *new_symbol = nullptr;
-        if(!ns.lookup(s, new_symbol))
-        {
-          if(new_symbol->type.id() == ID_code)
-          {
-            working_set.push_back(new_symbol);
-          }
-        }
+        const symbolt *symbol_ptr;
+        // identifiers for parameters of prototypes need not exist, and neither
+        // does __CPROVER_return_value
+        if(!ns.lookup(s, symbol_ptr))
+          working_set.push_back(symbol_ptr);
       }
     }
   }
@@ -239,6 +234,7 @@ void remove_internal_symbols(
     if(exported.find(it->first)==exported.end())
     {
       symbol_table_baset::symbolst::const_iterator next = std::next(it);
+      log.debug() << "Removing unused symbol " << it->first << messaget::eom;
       symbol_table.erase(it);
       it=next;
     }