From db8283bb213de97dd548f8bf3ea60973eddf00c8 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 15 May 2026 02:07:51 +0000 Subject: [PATCH] =?UTF-8?q?goto-programs:=20name=5Fmangler=20=E2=80=94=20a?= =?UTF-8?q?lso=20rename=20child=20symbols=20of=20mangled=20functions?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The function_name_manglert renames file-local function symbols (when --export-file-local-symbols is in use) to a mangled form __CPROVER_file_local__ so the same function from multiple TUs ends up under a unique unifiable name. Bug: the mangle pass renames the function symbol but does not rename the parameter and local-variable symbols whose names are scoped under the function's name (e.g. ::param_name). After mangling, the function symbol becomes __CPROVER_file_local_
_ but the parameter symbol is still ::param. At link time, two TUs that include the same header end up with identical parameter symbol names; CBMC's linker then either applies a suffix to disambiguate them (breaking parameter-name agreement in the function type) or reports 'conflicting function declarations' depending on what else differs. Fix: in mangle(), after identifying the file-local functions to rename, do a second pass to rename child symbols whose names start with . Each child gets its name prefix updated to the mangled function name and its is_file_local flag cleared (the parent function transitioned to globally-mangled-and-unifiable, and the linker's RENAME_NEW rule for file-local symbols would otherwise force per-TU divergence on each duplicate child). The rename map covers function-type parameter identifiers too, so symbol_expr references inside the function body's goto-instructions are updated consistently. Practical effect: kernel TUs compiled with --export-file-local-symbols can now be linked together with synthesised harness TUs that pull in the same kernel headers, without spurious 'conflicting function declarations' on parameter symbols of static-inline kernel header functions. Limitation surfaced during validation: even with the parameter mangling fixed, linking real kernel TUs against harness TUs that include extensive kernel headers still surfaces a separate class of conflict where one TU has a forward-declared struct () and the other has the full struct definition inlined into the function type irep. CBMC's irep equality is naive byte-comparison and rejects this even though both refer to the same C type. That is a deeper issue (type-completeness agreement between TUs) requiring further investigation; this commit does not address it. The fix here is still a prerequisite for any solution to the deeper issue. Validated: all 98 CORE ctest entries pass. All integration/linux regressions pass: - scan/run.sh cases 1-9 - test-per-file.sh - test-per-file-mode.sh cases 1-4 - smoke-all-lts.sh (4/4) Co-authored-by: Kiro --- .../child-symbols-mangled/file1.c | 5 ++ .../child-symbols-mangled/file2.c | 5 ++ .../child-symbols-mangled/lib.h | 9 +++ .../child-symbols-mangled/test.desc | 8 +++ src/goto-programs/name_mangler.h | 61 +++++++++++++++++++ 5 files changed, 88 insertions(+) create mode 100644 regression/goto-cc-file-local/child-symbols-mangled/file1.c create mode 100644 regression/goto-cc-file-local/child-symbols-mangled/file2.c create mode 100644 regression/goto-cc-file-local/child-symbols-mangled/lib.h create mode 100644 regression/goto-cc-file-local/child-symbols-mangled/test.desc diff --git a/regression/goto-cc-file-local/child-symbols-mangled/file1.c b/regression/goto-cc-file-local/child-symbols-mangled/file1.c new file mode 100644 index 00000000000..fe5a1e24198 --- /dev/null +++ b/regression/goto-cc-file-local/child-symbols-mangled/file1.c @@ -0,0 +1,5 @@ +#include "lib.h" +int caller1(int a) +{ + return helper(a); +} diff --git a/regression/goto-cc-file-local/child-symbols-mangled/file2.c b/regression/goto-cc-file-local/child-symbols-mangled/file2.c new file mode 100644 index 00000000000..c12cc894eb8 --- /dev/null +++ b/regression/goto-cc-file-local/child-symbols-mangled/file2.c @@ -0,0 +1,5 @@ +#include "lib.h" +int caller2(int b) +{ + return helper(b); +} diff --git a/regression/goto-cc-file-local/child-symbols-mangled/lib.h b/regression/goto-cc-file-local/child-symbols-mangled/lib.h new file mode 100644 index 00000000000..15a7783dec7 --- /dev/null +++ b/regression/goto-cc-file-local/child-symbols-mangled/lib.h @@ -0,0 +1,9 @@ +// A file-local function defined in a shared header: when two translation +// units include it and are compiled with --export-file-local-symbols, both +// mangle `helper` to the same __CPROVER_file_local_lib_h_helper name. Its +// parameter symbol (helper::x) must be mangled in lockstep, otherwise the +// two TUs carry identically-named parameter symbols that clash at link time. +static int helper(int x) +{ + return x + 1; +} diff --git a/regression/goto-cc-file-local/child-symbols-mangled/test.desc b/regression/goto-cc-file-local/child-symbols-mangled/test.desc new file mode 100644 index 00000000000..a042a967247 --- /dev/null +++ b/regression/goto-cc-file-local/child-symbols-mangled/test.desc @@ -0,0 +1,8 @@ +CORE +file1.c +final-link show-symbol-table +^EXIT=0$ +^SIGNAL=0$ +__CPROVER_file_local_lib_h_helper::x +-- +^warning: ignoring diff --git a/src/goto-programs/name_mangler.h b/src/goto-programs/name_mangler.h index ebcdab0f62d..0c9d9971ce3 100644 --- a/src/goto-programs/name_mangler.h +++ b/src/goto-programs/name_mangler.h @@ -83,10 +83,71 @@ class function_name_manglert log.debug() << "Mangling: " << sym.name << " -> " << mangled << log.eom; } + // Second pass: rename scoped child symbols of renamed + // functions. Parameter symbols and function-local + // variables are stored in the symbol table under names of + // the form `::` (and longer + // scope chains for nested locals). Without renaming + // these, two translation units that include the same + // kernel header end up with identically-named parameter + // symbols (e.g. `security_netlink_send::sk` from both + // TUs); the linker then either accepts them with a + // `$link1` suffix on one (unifying the function symbol + // under its external name) or rejects them as + // 'conflicting function declarations' depending on + // whether the parameter types match exactly. The fix is + // to rename child symbols in lockstep with the parent + // function so the per-TU mangling is complete. + std::vector new_child_syms; + std::vector old_child_syms; + for(auto sym_it = model.symbol_table.symbols.begin(); + sym_it != model.symbol_table.symbols.end(); + ++sym_it) + { + const std::string sym_name = id2string(sym_it->first); + // Skip the function symbols themselves; they were + // handled above and any name match here would already be + // in `renamed_funs`. + if(renamed_funs.find(sym_it->first) != renamed_funs.end()) + continue; + + for(const auto &pair : renamed_funs) + { + const std::string old_prefix = id2string(pair.first) + "::"; + if(sym_name.compare(0, old_prefix.size(), old_prefix) != 0) + continue; + + const irep_idt new_name = + id2string(pair.second) + "::" + sym_name.substr(old_prefix.size()); + symbolt new_child = sym_it->second; + new_child.name = new_name; + // Clear file_local on the child symbols too: the parent + // function has just transitioned from file-local to + // globally-mangled and unifiable, and the linker's + // file-local renaming rule (RENAME_NEW for any + // file_local symbol it sees on the new side of a link) + // would otherwise force `$link1` suffixes on each + // duplicate child symbol — defeating the unification we + // just set up. The new mangled name is unique across + // TUs that share the header but should unify cleanly + // when two TUs include the SAME header (because both + // ends of the link produce identical mangled names). + new_child.is_file_local = false; + new_child_syms.push_back(new_child); + old_child_syms.push_back(sym_it); + rename.insert(sym_it->second.symbol_expr(), new_child.symbol_expr()); + break; + } + } + for(const auto &sym : new_syms) model.symbol_table.insert(sym); for(const auto &sym : old_syms) model.symbol_table.erase(sym); + for(const auto &sym : new_child_syms) + model.symbol_table.insert(sym); + for(const auto &sym : old_child_syms) + model.symbol_table.erase(sym); for(auto it = model.symbol_table.begin(); it != model.symbol_table.end(); ++it)