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.
Comment on lines
+376
to
+417
| if(mode == COMPILE_LINK_EXECUTABLE || mode == COMPILE_LINK) | ||
| { | ||
| std::set<irep_idt> called_functions; | ||
| for(const auto &f : goto_model.goto_functions.function_map) | ||
| { | ||
| if(!f.second.body_available()) | ||
| continue; | ||
| for(const auto &ins : f.second.body.instructions) | ||
| { | ||
| if(ins.is_function_call()) | ||
| { | ||
| const auto &callee = ins.call_function(); | ||
| if(callee.id() == ID_symbol) | ||
| called_functions.insert(to_symbol_expr(callee).get_identifier()); | ||
| } | ||
| } | ||
| } | ||
|
|
||
| for(const auto &name : called_functions) | ||
| { | ||
| auto it = goto_model.goto_functions.function_map.find(name); | ||
| if(it == goto_model.goto_functions.function_map.end()) | ||
| continue; // unresolved (would already be an error elsewhere) | ||
| if(it->second.body_available()) | ||
| continue; | ||
| // Skip well-known CBMC library functions that are legitimately | ||
| // nondet-returning (malloc, __CPROVER_allocate, etc.) — those | ||
| // are intentional, not accidental. | ||
| const std::string s = id2string(name); | ||
| if( | ||
| s.substr(0, 10) == "__CPROVER_" || s == "malloc" || s == "free" || | ||
| s == "calloc" || s == "realloc") | ||
| continue; | ||
| log.warning() | ||
| << "symbol '" << s << "' is called but has no linked body; " | ||
| << "cbmc will treat it as a nondet-return stub. " | ||
| << "If this symbol is `static` in the target translation " | ||
| << "unit, compile with --export-file-local-symbols and call " | ||
| << "it via its `__CPROVER_file_local_<file>_<sym>` mangled " | ||
| << "name." << messaget::eom; | ||
| } | ||
| } |
Comment on lines
+385
to
+390
| if(ins.is_function_call()) | ||
| { | ||
| const auto &callee = ins.call_function(); | ||
| if(callee.id() == ID_symbol) | ||
| called_functions.insert(to_symbol_expr(callee).get_identifier()); | ||
| } |
| final-link wall | ||
| ^EXIT=0$ | ||
| ^SIGNAL=0$ | ||
| symbol '_recv' is called but has no linked body; cbmc will treat it as a nondet-return stub |
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 189531 +30
Branches 73 73
========================================
+ Hits 152902 152936 +34
+ Misses 36599 36595 -4 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
tautschnig
force-pushed
the
extract/goto-cc-warn-unlinked-body
branch
from
16a9642 to
5d8b4d4
Compare
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. Motivation: a kernel `static` symbol bound to an empty external stub because the caller's `extern` declaration used the unmangled name. The warning points at the `--export-file-local-symbols` workaround 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.sh` is updated to pass `-Wall` so our kernel-scan pipeline surfaces these warnings in the goto-cc output; users who would rather not see them simply omit `-Wall`. Tested: - Minimal scenario (static function called from external caller under different TU) emits the warning as expected. - All five integration/linux regression scripts continue to pass with `-Wall` now on in compile_file.sh. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
tautschnig
force-pushed
the
extract/goto-cc-warn-unlinked-body
branch
from
5d8b4d4 to
632660a
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.