From 3083aca4e6a28ca717164bbf6164551e3479ae8d Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 30 Mar 2026 11:32:10 +0000 Subject: [PATCH] Fix name mangler to preserve definition when mangled name already exists When --export-file-local-symbols is used and files are compiled together, a forward declaration using the mangled name (e.g., __CPROVER_file_local_a_c_foo) may already exist in the symbol table and function map before the mangler runs. The mangler's symbol_table.insert() silently failed in this case, leaving the declaration's type (with empty parameter identifiers) in place instead of the definition's type. This caused an invariant violation in goto_symext::locality() when it tried to look up the empty parameter identifier. Fix the mangler to: 1. When insert fails and the existing symbol is a declaration (no body), update it with the definition's type/value. Log a warning when the existing symbol already has a definition. 2. When the mangled name already has an empty function map entry, swap in the definition's body and parameter_identifiers. 3. Rename parameter_identifiers when renaming functions (matching what link_goto_model already does). Fixes: #8254 Co-authored-by: Kiro --- .../multi-file-compile-together/a.c | 4 ++ .../multi-file-compile-together/main.c | 6 +++ .../multi-file-compile-together/test.desc | 12 +++++ src/goto-programs/name_mangler.h | 48 +++++++++++++++++-- 4 files changed, 67 insertions(+), 3 deletions(-) create mode 100644 regression/goto-cc-file-local/multi-file-compile-together/a.c create mode 100644 regression/goto-cc-file-local/multi-file-compile-together/main.c create mode 100644 regression/goto-cc-file-local/multi-file-compile-together/test.desc diff --git a/regression/goto-cc-file-local/multi-file-compile-together/a.c b/regression/goto-cc-file-local/multi-file-compile-together/a.c new file mode 100644 index 00000000000..ddb6442c297 --- /dev/null +++ b/regression/goto-cc-file-local/multi-file-compile-together/a.c @@ -0,0 +1,4 @@ +static void foo(int x) +{ + __CPROVER_assert(0, "reachable"); +} diff --git a/regression/goto-cc-file-local/multi-file-compile-together/main.c b/regression/goto-cc-file-local/multi-file-compile-together/main.c new file mode 100644 index 00000000000..f2f470ac890 --- /dev/null +++ b/regression/goto-cc-file-local/multi-file-compile-together/main.c @@ -0,0 +1,6 @@ +void __CPROVER_file_local_a_c_foo(int); +int main() +{ + __CPROVER_file_local_a_c_foo(0); + return 0; +} diff --git a/regression/goto-cc-file-local/multi-file-compile-together/test.desc b/regression/goto-cc-file-local/multi-file-compile-together/test.desc new file mode 100644 index 00000000000..e0f116b7e72 --- /dev/null +++ b/regression/goto-cc-file-local/multi-file-compile-together/test.desc @@ -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 diff --git a/src/goto-programs/name_mangler.h b/src/goto-programs/name_mangler.h index ebcdab0f62d..27024d37fde 100644 --- a/src/goto-programs/name_mangler.h +++ b/src/goto-programs/name_mangler.h @@ -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) + { + 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 + // full type are preserved. + existing.type = sym.type; + existing.value = sym.value; + existing.is_file_local = sym.is_file_local; + existing.module = sym.module; + 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); @@ -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()); @@ -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); }