Drop unused functions before property instrumentation

[tautschnig]

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

• Each commit message has a non-empty body, explaining why the change was made.
• n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[Copilot]

Pull request overview

Note

Copilot was unable to run its full agentic suite in this review.

This PR moves remove_unused_functions() into the shared process_goto_program() pipeline so unused functions are dropped before property instrumentation, avoiding unnecessary instrumentation work on unreachable functions.

Changes:

• Run remove_unused_functions() in process_goto_program() before goto_check_c() when drop-unused-functions is enabled
• Remove the now-redundant remove_unused_functions() call (and include) from cbmc_parse_options.cpp

Reviewed changes

Copilot reviewed 2 out of 2 changed files in this pull request and generated 2 comments.

File	Description
src/goto-programs/process_goto_program.cpp	Drops unused functions earlier in the pipeline to reduce instrumentation workload
src/cbmc/cbmc_parse_options.cpp	Removes redundant unused-function removal and header include

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[Copilot]

The comment asserts that function pointers “have already been resolved” and “partial inlining has been performed above,” but those passes are often option-dependent in this pipeline. To avoid misleading future readers (and to keep the safety argument accurate), reword this comment to describe the actual preconditions required by remove_unused_functions() (e.g., “after any function-pointer removal / inlining passes that are enabled”) or explicitly tie the claim to the specific earlier steps that are unconditionally executed in this function.

Suggested change

	// instrumenting functions that will never be reached. This is safe
	// because function pointers have already been resolved and partial
	// inlining has been performed above.
	// instrumenting functions that will never be reached. This is done
	// after function-pointer removal and after any earlier cleanup /
	// inlining passes in this routine that are enabled.

[Copilot]

This is a behavior/performance-sensitive pipeline change (dropping functions before instrumentation). It would benefit from a regression test that fails if unreachable functions are still instrumented when --drop-unused-functions is enabled (e.g., a small program with an unreachable function containing code that would be instrumented, and an assertion on reported properties/checks or on the presence/absence of instrumentation artifacts for that function).

[codecov]

Codecov Report

❌ Patch coverage is 33.33333% with 2 lines in your changes missing coverage. Please review.
✅ Project coverage is 80.50%. Comparing base (b32074b) to head (d339b1d).

Files with missing lines	Patch %	Lines
src/goto-programs/process_goto_program.cpp	33.33%	2 Missing ⚠️

Additional details and impacted files

@@           Coverage Diff            @@
##           develop    #8975   +/-   ##
========================================
  Coverage    80.50%   80.50%           
========================================
  Files         1704     1704           
  Lines       188778   188778           
  Branches        73       73           
========================================
  Hits        151975   151975           
  Misses       36803    36803           

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
• 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

[kroening]

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.

I am wondering how remove_unused_functions() interacts with instrumenting an error label.