From 632660a1ec9fe5c08ffe6a46c5ef5622ac21efbe Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 11 May 2026 22:50:11 +0000 Subject: [PATCH] goto-cc: warn on called-but-not-linked-body symbols 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__` 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 --- .../warn-static-called-via-extern/impl.c | 8 +++ .../warn-static-called-via-extern/main.c | 15 +++++ .../warn-static-called-via-extern/test.desc | 8 +++ src/goto-cc/compile.cpp | 62 +++++++++++++++++++ 4 files changed, 93 insertions(+) create mode 100644 regression/goto-cc-file-local/warn-static-called-via-extern/impl.c create mode 100644 regression/goto-cc-file-local/warn-static-called-via-extern/main.c create mode 100644 regression/goto-cc-file-local/warn-static-called-via-extern/test.desc diff --git a/regression/goto-cc-file-local/warn-static-called-via-extern/impl.c b/regression/goto-cc-file-local/warn-static-called-via-extern/impl.c new file mode 100644 index 00000000000..0ec55456ea6 --- /dev/null +++ b/regression/goto-cc-file-local/warn-static-called-via-extern/impl.c @@ -0,0 +1,8 @@ +static int _recv(int x) +{ + return x + 1; +} +int kernel_entry(void) +{ + return _recv(7); +} diff --git a/regression/goto-cc-file-local/warn-static-called-via-extern/main.c b/regression/goto-cc-file-local/warn-static-called-via-extern/main.c new file mode 100644 index 00000000000..8a392658cb8 --- /dev/null +++ b/regression/goto-cc-file-local/warn-static-called-via-extern/main.c @@ -0,0 +1,15 @@ +// The harness calls _recv via an `extern` (unmangled) declaration. _recv is +// actually `static` in impl.c, so with --export-file-local-symbols it is +// mangled to __CPROVER_file_local_impl_c__recv and does NOT satisfy the +// extern call. At link time _recv therefore has no body: goto-cc warns that +// it will be treated as a nondet-return stub (LIM-009). Verification against +// such a stub would be silently vacuous, which is what the warning flags. +extern int _recv(int); +int harness(void) +{ + return _recv(0); +} +int main(void) +{ + return harness(); +} diff --git a/regression/goto-cc-file-local/warn-static-called-via-extern/test.desc b/regression/goto-cc-file-local/warn-static-called-via-extern/test.desc new file mode 100644 index 00000000000..bfd23a27b8a --- /dev/null +++ b/regression/goto-cc-file-local/warn-static-called-via-extern/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +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 +-- +^warning: ignoring diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp index 0a49ec521ab..a4162f577c0 100644 --- a/src/goto-cc/compile.cpp +++ b/src/goto-cc/compile.cpp @@ -16,6 +16,7 @@ Date: June 2006 #include #include #include +#include #include #include #include @@ -359,6 +360,67 @@ bool compilet::link(std::optional &&symbol_table) mangler.mangle(); } + // Warn about functions that are CALLED from a linked body but have + // no body of their own. At verification time, cbmc replaces each + // such call with a nondet-return stub; if the caller is a + // harness's entry function and the missing body is the subject of + // the analysis, the verification is silently vacuous. LIM-009 in + // integration/linux/CBMC_LIMITATIONS.md documents the concrete + // failure mode: a kernel `static` symbol bound to an empty extern + // stub because the caller's `extern` declaration used the + // unmangled name. + // + // We collect the set of functions actually called from any body, + // then diff against the set of functions with bodies, and report + // each missing-body call-target with a suggestion pointing at + // --export-file-local-symbols. + if(mode == COMPILE_LINK_EXECUTABLE || mode == COMPILE_LINK) + { + std::set 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( + has_prefix(s, CPROVER_PREFIX) || 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 " << messaget::quote_begin + << CPROVER_PREFIX "file_local__" << messaget::quote_end + << " mangled " + << "name." << messaget::eom; + } + } + if(write_bin_object_file(output_file_executable, goto_model)) return true;