From d339b1d86196ff8900873d560f793ddd1bb8d1a4 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 15 Apr 2026 07:25:10 +0000
Subject: [PATCH] Drop unused functions before property instrumentation

Move remove_unused_functions() into process_goto_program(), before
goto_check_c(). For an example from Collections-C, all ~370 functions in
the goto model were instrumented with pointer/bounds/overflow checks,
then most were dropped. Now we drop first, instrumenting only the ~20
reachable functions.

This is safe because function pointers have already been resolved
and partial inlining has been performed at this point. The option
guard (drop-unused-functions) ensures other tools that don't set
this option are unaffected.

Remove the now-redundant remove_unused_functions() call from
cbmc_parse_options.cpp.

Impact on Collections-C:
  Monolithic: 93s -> 62s
  Paths:      92s -> 60s

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
---
 src/cbmc/cbmc_parse_options.cpp            |  8 --------
 src/goto-programs/process_goto_program.cpp | 11 +++++++++++
 2 files changed, 11 insertions(+), 8 deletions(-)

diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index 6548067d791..c715e89b491 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -23,7 +23,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-programs/process_goto_program.h>
 #include <goto-programs/read_goto_binary.h>
 #include <goto-programs/remove_skip.h>
-#include <goto-programs/remove_unused_functions.h>
 #include <goto-programs/set_properties.h>
 #include <goto-programs/show_goto_functions.h>
 #include <goto-programs/show_properties.h>
@@ -919,13 +918,6 @@ bool cbmc_parse_optionst::process_goto_program(
   // needs to be done before pointer analysis
   add_failed_symbols(goto_model.symbol_table);
 
-  if(options.get_bool_option("drop-unused-functions"))
-  {
-    // Entry point will have been set before and function pointers removed
-    log.status() << "Removing unused functions" << messaget::eom;
-    remove_unused_functions(goto_model, log.get_message_handler());
-  }
-
   // remove skips such that trivial GOTOs are deleted and not considered
   // for coverage annotation:
   remove_skip(goto_model);
diff --git a/src/goto-programs/process_goto_program.cpp b/src/goto-programs/process_goto_program.cpp
index 4b7e712ee68..989a02dc905 100644
--- a/src/goto-programs/process_goto_program.cpp
+++ b/src/goto-programs/process_goto_program.cpp
@@ -22,6 +22,7 @@ Author: Martin Brain, martin.brain@cs.ox.ac.uk
 #include <goto-programs/remove_complex.h>
 #include <goto-programs/remove_function_pointers.h>
 #include <goto-programs/remove_returns.h>
+#include <goto-programs/remove_unused_functions.h>
 #include <goto-programs/remove_vector.h>
 #include <goto-programs/rewrite_rw_ok.h>
 #include <goto-programs/rewrite_union.h>
@@ -74,6 +75,16 @@ bool process_goto_program(
   if(options.get_bool_option("rewrite-rw-ok"))
     rewrite_rw_ok(goto_model);
 
+  // Drop unused functions before property instrumentation to avoid
+  // instrumenting functions that will never be reached. This is safe
+  // because function pointers have already been resolved and partial
+  // inlining has been performed above.
+  if(options.get_bool_option("drop-unused-functions"))
+  {
+    log.status() << "Removing unused functions" << messaget::eom;
+    remove_unused_functions(goto_model, log.get_message_handler());
+  }
+
   // add generic checks
   log.status() << "Generic Property Instrumentation" << messaget::eom;
   goto_check_c(options, goto_model, log.get_message_handler());