goto-programs: name_mangler — also rename child symbols of mangled functions#9059
Open
tautschnig wants to merge 1 commit into
Open
goto-programs: name_mangler — also rename child symbols of mangled functions#9059tautschnig wants to merge 1 commit into
tautschnig wants to merge 1 commit into
Conversation
There was a problem hiding this comment.
Pull request overview
Note
Copilot was unable to run its full agentic suite in this review.
Fixes file-local symbol mangling so that not only the function symbol is renamed, but also any scoped “child” symbols (parameters / locals) that are named under the function scope, preventing link-time conflicts when multiple TUs include the same header under --export-file-local-symbols.
Changes:
- Add a second pass in
function_name_manglert::mangle()to rename child symbols of renamed functions and clear theiris_file_localflag. - Add a regression test reproducing the child-symbol collision and asserting the mangled child symbol name appears in the final symbol table.
Reviewed changes
Copilot reviewed 5 out of 5 changed files in this pull request and generated 4 comments.
Show a summary per file
| File | Description |
|---|---|
| src/goto-programs/name_mangler.h | Adds child-symbol renaming logic alongside function-symbol mangling. |
| regression/goto-cc-file-local/child-symbols-mangled/test.desc | New regression test driver asserting mangled child symbol presence. |
| regression/goto-cc-file-local/child-symbols-mangled/lib.h | Header defining a file-local function whose parameter symbol must be mangled too. |
| regression/goto-cc-file-local/child-symbols-mangled/file1.c | TU including the header and calling the helper. |
| regression/goto-cc-file-local/child-symbols-mangled/file2.c | Second TU including the header and calling the helper. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
tautschnig
force-pushed
the
extract/name-mangler-child-symbols
branch
from
b879d4e to
11f9297
Compare
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## develop #9059 +/- ##
========================================
Coverage 80.68% 80.68%
========================================
Files 1714 1714
Lines 189547 189573 +26
Branches 73 73
========================================
+ Hits 152939 152963 +24
- Misses 36608 36610 +2 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
tautschnig
force-pushed
the
extract/name-mangler-child-symbols
branch
2 times, most recently
from
db8283b to
325848e
Compare
…nctions function_name_manglert renames file-local function symbols (when --export-file-local-symbols is used) to a mangled form __CPROVER_file_local_<file>_<sym>, so the same function from multiple TUs ends up under a unique, unifiable name. Bug: the pass renamed the function symbol but not the parameter and local-variable symbols whose names are scoped under it (`<function>::<name>`, and longer chains such as `<function>::1::<var>` for body locals). After mangling, the function became __CPROVER_file_local_<file>_<func> while its parameter symbol was still `<func>::param`. Two TUs that include the same header then carry identically-named child symbols; CBMC's linker either applies a `$link1` 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 that renames their child symbols in lockstep. A child symbol is scoped `<function>::<rest>`, and renamed file-local function names never contain "::" themselves, so the scope up to the first "::" identifies the owning function via a single map lookup. Each child's name prefix is updated to the mangled function name and its is_file_local flag is cleared (the parent just became globally-mangled-and-unifiable; the linker's RENAME_NEW rule for file-local symbols would otherwise force per-TU divergence on each duplicate child). The rename map also covers the parameter identifiers in the function type, so symbol_expr references inside instruction bodies are updated too. Two further consistency fixes: - The originals are now erased from the symbol table by name via symbol_tablet::remove rather than by stored iterator. The earlier code held unordered_map iterators across insert loops that can rehash and invalidate them, making the subsequent erase undefined behaviour. - goto_functiont::parameter_identifiers is a separate vector that the rename does not touch, so a renamed function kept the stale `<old_func>::param` names while the symbol table held `<mangled>::param`. It is now re-derived from the renamed code_typet when the function is relocated in the function_map, so the in-memory model is self-consistent (previously this was masked only by goto-cc's write-out / read-back). regression/goto-cc-file-local/child-symbols-mangled covers two TUs including a shared header with a file-local function that has both a parameter and a body local: test.desc checks the mangled child symbols in the symbol table, and test-assertion.desc links a third TU with an entry point and runs cbmc on the linked model to confirm it is usable (catching broken symbol_expr references, not just symbol-table keys). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
tautschnig
force-pushed
the
extract/name-mangler-child-symbols
branch
from
325848e to
bb0ca29
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.
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
_ 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._CPROVER_file_local
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: