goto-cc: warn on called-but-not-linked-body symbols#9057
Open
tautschnig wants to merge 1 commit into
Open
Conversation
There was a problem hiding this comment.
Pull request overview
Note
Copilot was unable to run its full agentic suite in this review.
Adds a new goto-cc link-time warning for functions that are called from linked function bodies but have no linked body themselves, helping catch vacuous CBMC verification caused by nondet-return stubs.
Changes:
- Detects “called-but-no-body” functions during linking and emits a warning with remediation guidance.
- Adds a regression test covering the file-local static / extern-mismatch scenario (LIM-009 motivator).
Reviewed changes
Copilot reviewed 4 out of 4 changed files in this pull request and generated 3 comments.
| File | Description |
|---|---|
| src/goto-cc/compile.cpp | Adds link-time scan of calls and warning emission for missing bodies (with CBMC-library allowlist). |
| regression/goto-cc-file-local/warn-static-called-via-extern/test.desc | New regression expectations for the warning. |
| regression/goto-cc-file-local/warn-static-called-via-extern/main.c | Harness that calls an unmangled extern symbol, inducing missing-body link behavior. |
| regression/goto-cc-file-local/warn-static-called-via-extern/impl.c | Defines the real static implementation to reproduce the file-local mismatch. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
tautschnig
force-pushed
the
extract/goto-cc-warn-unlinked-body
branch
from
b3492a5 to
16a9642
Compare
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## develop #9057 +/- ##
========================================
Coverage 80.68% 80.69%
========================================
Files 1714 1714
Lines 189501 189541 +40
Branches 73 73
========================================
+ Hits 152904 152942 +38
- Misses 36597 36599 +2 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
tautschnig
force-pushed
the
extract/goto-cc-warn-unlinked-body
branch
3 times, most recently
from
632660a to
4505192
Compare
Emits a warning at executable link time when a `static` function whose body, under --export-file-local-symbols, lives at the mangled name __CPROVER_file_local_<file>_<sym>, while the program also calls the *unmangled* <sym> -- typically through an `extern` declaration in another translation unit. The unmangled call does not bind to the mangled body, so <sym> has no body at link time and cbmc replaces the call with a nondet-return stub; any verification depending on that function is then silently vacuous. The warning is deliberately narrow: it fires only when both halves of that signature are present -- a bodiless called <sym> and a __CPROVER_file_local_..._<sym> with a body. Ordinary bodiless library symbols (printf, memcpy, __assert_fail, the __builtin_* family, ...) have no file-local twin and so never trigger it, which avoids an arbitrary allowlist that would rot over time. The scan is restricted to executable links (a `gcc -shared` link legitimately leaves symbols unresolved) and is skipped unless warnings are actually shown (verbosity >= warning, which -Wall/-Wextra raise it to, or --verbosity sets directly), since it is a non-trivial double loop whose output would otherwise be discarded. It is factored into warn_file_local_stub_calls() to keep link() within the size guideline, and call targets are looked through a no-op typecast before matching. regression/goto-cc-file-local: - warn-static-called-via-extern: the warning fires and names the mangled symbol; - no-warn-unrelated-stub: a bodiless external with no file-local twin does not warn, even when a file-local body is present; - warn-suppressed-low-verbosity: the same scenario at --verbosity 1 emits no warning, exercising the verbosity gating. chain.sh now honours an explicit --verbosity passed in the test arguments (defaulting to --verbosity 10 as before). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
tautschnig
force-pushed
the
extract/goto-cc-warn-unlinked-body
branch
from
4505192 to
787c04d
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Emits a warning at link time for each function that is called from a function body in the linked binary but has no body of its own. CBMC will treat such calls as nondet-return stubs; if the missing body is the subject of analysis, the verification is silently vacuous. LIM-009 in integration/linux/CBMC_LIMITATIONS.md is the concrete motivator: a kernel
staticsymbol bound to an empty external stub because the caller'sexterndeclaration used the unmangled name. The warning points at the--export-file-local-symbolsworkaround and the__CPROVER_file_local_<file>_<sym>mangled-name convention so a developer seeing this message has an actionable path to a fix.Skips well-known CBMC library functions (
__CPROVER_*, malloc, free, calloc, realloc) which are intentionally nondet-returning, not accidental.Gated on
-Wall/-Wextra(following the existing goto-cc warning emission threshold in gcc_mode).integration/linux/scan/compile_file.shis updated to pass-Wallso our kernel-scan pipeline surfaces these warnings in the goto-cc output; users who would rather not see them simply omit-Wall.Had this warning existed during the original LIM-009 investigation, the symbol-linkage bug would have surfaced the first time scan.py built a linked binary, instead of taking a week of diagnostic work to unmask. Shipping it here as an orthogonal improvement that benefits every downstream goto-cc user, not just the Linux integration.
Tested:
-Wallnow on in compile_file.sh.