Skip to content

Fix name mangler to preserve definition when mangled name already exists #8930

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
tautschnig wants to merge 1 commit into
base: develop
Choose a base branch
from
Open

Fix name mangler to preserve definition when mangled name already exists #8930

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 4 additions & 0 deletions regression/goto-cc-file-local/multi-file-compile-together/a.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
static void foo(int x)
{
__CPROVER_assert(0, "reachable");
}
6 changes: 6 additions & 0 deletions regression/goto-cc-file-local/multi-file-compile-together/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
void __CPROVER_file_local_a_c_foo(int);
int main()
{
__CPROVER_file_local_a_c_foo(0);
return 0;
}
12 changes: 12 additions & 0 deletions regression/goto-cc-file-local/multi-file-compile-together/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
CORE
main.c
assertion-check compile-and-link
^EXIT=10$
^SIGNAL=0$
^\[foo.assertion.1\] .* reachable: FAILURE$
--
^warning: ignoring
^\*\*\*\* WARNING: no body for function
--
Check that when files are compiled together with --export-file-local-symbols
the local_bitvector_analysis does not crash with an invariant violation
48 changes: 45 additions & 3 deletions src/goto-programs/name_mangler.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -84,7 +84,34 @@ class function_name_manglert
}

for(const auto &sym : new_syms)
model.symbol_table.insert(sym);
{
auto result = model.symbol_table.insert(sym);
if(!result.second)
{
Comment on lines 86 to +90
Copy link

Copilot AI Mar 30, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

old_syms stores iterators into model.symbol_table.symbols (an unordered_map). Inserting new_syms before erasing old_syms can trigger a rehash and invalidate those iterators, making the later erase(sym) undefined behaviour. Prefer storing the old symbol names (irep_idt) and erasing via a fresh find() after insertions, or erase old entries before inserting new ones (or reserve to prevent rehash).

Copilot uses AI. Check for mistakes.
symbolt &existing = result.first;
if(existing.value.is_nil())
{
// The existing symbol is a declaration (no body). This happens
// when user code forward-declares the mangled name. Replace it
// with the definition so that parameter identifiers and the
Comment on lines +91 to +96
Copy link

Copilot AI Mar 30, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The insert-collision handling treats any existing symbol with value.is_nil() as a forward declaration, but many non-function symbols can also have a nil value (e.g., uninitialised variables). Before overwriting, ensure the existing entry is actually a function declaration (e.g., existing.is_function() / existing.type.id()==ID_code) and otherwise emit a diagnostic rather than replacing an unrelated symbol.

Copilot uses AI. Check for mistakes.
// full type are preserved.
existing.type = sym.type;
existing.value = sym.value;
existing.is_file_local = sym.is_file_local;
existing.module = sym.module;
Copy link

Copilot AI Mar 30, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Updating existing.module (and any other fields used by symbol_table indices) in-place breaks symbol_tablet's internal symbol_module_map invariants: the module/base-name maps are populated at insert-time and symbol_tablet::erase() assumes these fields never change. To keep the symbol table consistent, avoid mutating module on an already-inserted symbol; instead erase the existing entry (by iterator) and re-insert the updated symbol, or keep module unchanged.

Suggested change
existing.module = sym.module;
// Do not change existing.module: it participates in symbol_table indices.

Copilot uses AI. Check for mistakes.
existing.mode = sym.mode;
existing.location = sym.location;
if(!sym.pretty_name.empty())
existing.pretty_name = sym.pretty_name;
}
else
{
log.warning() << "Mangled name '" << sym.name
<< "' already exists with a definition"
<< messaget::eom;
}
}
}
for(const auto &sym : old_syms)
model.symbol_table.erase(sym);

Expand All @@ -107,6 +134,12 @@ class function_name_manglert
{
if(!fun.second.body_available())
continue;
for(auto &identifier : fun.second.parameter_identifiers)
{
auto entry = rename.expr_map.find(identifier);
if(entry != rename.expr_map.end())
identifier = entry->second;
}
for(auto &ins : fun.second.body.instructions)
{
rename(ins.code_nonconst());
Expand All @@ -128,8 +161,17 @@ class function_name_manglert
auto inserted = model.goto_functions.function_map.emplace(
pair.second, std::move(found->second));
if(!inserted.second)
log.debug() << "Found a mangled name that already exists: "
<< std::string(pair.second.c_str()) << log.eom;
{
// The mangled name already has a function map entry (from a forward
// declaration). Replace its empty body and parameter_identifiers
// with those from the definition.
if(inserted.first->second.body.instructions.empty())
{
inserted.first->second.body.swap(found->second.body);
inserted.first->second.parameter_identifiers.swap(
found->second.parameter_identifiers);
}
}

model.goto_functions.function_map.erase(found);
}
Expand Down
Loading