From d9e83d43cf92caa57396a67fdaa1633ed13a11be Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 13 Aug 2024 15:16:17 +0000
Subject: [PATCH] Library functions: mark them as compiled

When adding library functions to the goto model we no longer need their
function bodies as values in the symbol table. Marking them as
"compiled" will make sure we don't re-convert them in any subsequent run
(e.g., running cbmc after goto-instrument). Doing so would undo any
application of "drop-unused-functions." This was most notable with
contracts/dynamic frames, where we ended up reporting thousands of
properties as "SUCCESS" in library functions that were never actually
called. For some contracts examples this now reduces the number of
properties reported from over a thousand to tens of properties.
---
 regression/contracts-dfcc/chain.sh                       | 3 +++
 regression/contracts/chain.sh                            | 3 +++
 src/ansi-c/goto-conversion/link_to_library.cpp           | 9 +++++++--
 .../contracts/dynamic-frames/dfcc_library.cpp            | 1 +
 4 files changed, 14 insertions(+), 2 deletions(-)

diff --git a/regression/contracts-dfcc/chain.sh b/regression/contracts-dfcc/chain.sh
index c388dc26c914..54829580e44f 100755
--- a/regression/contracts-dfcc/chain.sh
+++ b/regression/contracts-dfcc/chain.sh
@@ -58,5 +58,8 @@ elif echo $args_inst | grep -q -- "--dump-c" ; then
 
   rm "${name}${dfcc_suffix}-mod.c"
 fi
+if ! echo "${args_cbmc}" | grep -q -- --function ; then
+  $goto_instrument --drop-unused-functions "${name}${dfcc_suffix}-mod.gb" "${name}${dfcc_suffix}-mod.gb"
+fi
 $goto_instrument --show-goto-functions "${name}${dfcc_suffix}-mod.gb"
 $cbmc "${name}${dfcc_suffix}-mod.gb" ${args_cbmc}
diff --git a/regression/contracts/chain.sh b/regression/contracts/chain.sh
index 37aa18a35b53..0cfcbb3fe20d 100755
--- a/regression/contracts/chain.sh
+++ b/regression/contracts/chain.sh
@@ -41,5 +41,8 @@ elif echo $args_inst | grep -q -- "--dump-c" ; then
 
   rm "${name}-mod.c"
 fi
+if ! echo "${args_cbmc}" | grep -q -- --function ; then
+  $goto_instrument --drop-unused-functions "${name}-mod.gb" "${name}-mod.gb"
+fi
 $goto_instrument --show-goto-functions "${name}-mod.gb"
 $cbmc "${name}-mod.gb" ${args_cbmc}
diff --git a/src/ansi-c/goto-conversion/link_to_library.cpp b/src/ansi-c/goto-conversion/link_to_library.cpp
index cc814e1965ad..9f7cfcb889a2 100644
--- a/src/ansi-c/goto-conversion/link_to_library.cpp
+++ b/src/ansi-c/goto-conversion/link_to_library.cpp
@@ -41,26 +41,31 @@ add_one_function(
   // convert to CFG
   if(
     library_model.symbol_table.symbols.find(missing_function) !=
-    library_model.symbol_table.symbols.end())
+      library_model.symbol_table.symbols.end() &&
+    library_model.symbol_table.lookup_ref(missing_function).value.is_not_nil())
   {
     goto_convert(
       missing_function,
       library_model.symbol_table,
       library_model.goto_functions,
       message_handler);
+    library_model.symbol_table.get_writeable_ref(missing_function)
+      .set_compiled();
   }
   // We might need a function that's outside our own library, but brought in via
   // some header file included by the library. Those functions already exist in
   // goto_model.symbol_table, but haven't been converted just yet.
   else if(
     goto_model.symbol_table.symbols.find(missing_function) !=
-    goto_model.symbol_table.symbols.end())
+      goto_model.symbol_table.symbols.end() &&
+    goto_model.symbol_table.lookup_ref(missing_function).value.is_not_nil())
   {
     goto_convert(
       missing_function,
       goto_model.symbol_table,
       library_model.goto_functions,
       message_handler);
+    goto_model.symbol_table.get_writeable_ref(missing_function).set_compiled();
   }
 
   // check whether additional initialization may be required
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp
index 63c4d8046008..242b330b4d30 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp
@@ -326,6 +326,7 @@ void dfcc_libraryt::load(std::set<irep_idt> &to_instrument)
   {
     goto_convert(
       id, goto_model.symbol_table, goto_model.goto_functions, message_handler);
+    goto_model.symbol_table.get_writeable_ref(id).set_compiled();
   }
 
   // check that all symbols have a goto_implementation