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.
Comment on lines
+101
to
+105
| std::vector<symbolt> new_child_syms; | ||
| std::vector<symbol_tablet::symbolst::const_iterator> old_child_syms; | ||
| for(auto sym_it = model.symbol_table.symbols.begin(); | ||
| sym_it != model.symbol_table.symbols.end(); | ||
| ++sym_it) |
Comment on lines
+149
to
+152
| for(const auto &sym : new_child_syms) | ||
| model.symbol_table.insert(sym); | ||
| for(const auto &sym : old_child_syms) | ||
| model.symbol_table.erase(sym); |
Comment on lines
+103
to
+105
| for(auto sym_it = model.symbol_table.symbols.begin(); | ||
| sym_it != model.symbol_table.symbols.end(); | ||
| ++sym_it) |
Comment on lines
+114
to
+118
| 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; |
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.69%
========================================
Files 1714 1714
Lines 189501 189523 +22
Branches 73 73
========================================
+ Hits 152902 152927 +25
+ Misses 36599 36596 -3 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
…nctions The function_name_manglert renames file-local function symbols (when --export-file-local-symbols is in use) 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 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. <function>::param_name). After mangling, the function symbol becomes __CPROVER_file_local_<header>_<func> but the parameter symbol is still <func>::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 <kiro-agent@users.noreply.github.com>
tautschnig
force-pushed
the
extract/name-mangler-child-symbols
branch
from
11f9297 to
db8283b
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: