goto-cc: warn on called-but-not-linked-body symbols

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);
+}

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();
+}

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

src/goto-cc/compile.cpp

@@ -16,6 +16,7 @@ Date: June 2006
 #include <util/cmdline.h>
 #include <util/config.h>
 #include <util/get_base_name.h>
+#include <util/prefix.h>
 #include <util/run.h>
 #include <util/symbol_table_builder.h>
 #include <util/tempdir.h>
@@ -359,6 +360,67 @@ bool compilet::link(std::optional<symbol_tablet> &&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<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(
+        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_<file>_<sym>" << messaget::quote_end
+        << " mangled "
+        << "name." << messaget::eom;
+    }
+  }
+
   if(write_bin_object_file(output_file_executable, goto_model))
     return true;