From 61c99bf1b136e5aeb1adb6a29909d0fa88f0d9c8 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 9 Dec 2025 12:41:15 +0000 Subject: [PATCH] Fix goto-instrument --dump-c parameter/local variable name collision Local variables are automatically renamed with a unique suffix when a name collision is detected, producing valid compilable C code. Co-authored-by: Kiro autonomous agent Fixes: #6268 --- .../dump-param-local-collision/main.c | 25 ++++++++ .../dump-param-local-collision/test.desc | 19 ++++++ src/goto-instrument/goto_program2code.cpp | 58 +++++++++++++++++++ src/goto-instrument/goto_program2code.h | 3 + 4 files changed, 105 insertions(+) create mode 100644 regression/goto-instrument/dump-param-local-collision/main.c create mode 100644 regression/goto-instrument/dump-param-local-collision/test.desc diff --git a/regression/goto-instrument/dump-param-local-collision/main.c b/regression/goto-instrument/dump-param-local-collision/main.c new file mode 100644 index 00000000000..555a2393157 --- /dev/null +++ b/regression/goto-instrument/dump-param-local-collision/main.c @@ -0,0 +1,25 @@ +// Test case for parameter/local variable name collision in goto-instrument --dump-c +// This should generate valid C code with renamed local variables + +int help(int x) +{ + unsigned int x; // Should be renamed to x$1 in output + x = 42; + return (int)x; +} + +int test_two_params(int y, int z) +{ + int y; // Should be renamed to y$1 + int z; // Should be renamed to z$1 + y = 10; + z = 20; + return y + z; +} + +int main() +{ + int result = help(1); + result += test_two_params(5, 6); + return result; +} diff --git a/regression/goto-instrument/dump-param-local-collision/test.desc b/regression/goto-instrument/dump-param-local-collision/test.desc new file mode 100644 index 00000000000..96b997a1abc --- /dev/null +++ b/regression/goto-instrument/dump-param-local-collision/test.desc @@ -0,0 +1,19 @@ +CORE +main.c +--dump-c +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +This test ensures that goto-instrument --dump-c produces valid C code when a +local variable has the same name as a function parameter. Previously, this +would generate invalid C code like: + int help(int x) { unsigned int x; } +which causes a compilation error. The fix renames the local variable to avoid +the collision, e.g.: + int help(int x) { unsigned int x$1; } + +The generated C code should be valid and compilable. + +Related to issue #6268 (similar to issue #6242 but for a different case). diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp index 87eee70ed89..7de2f175bd6 100644 --- a/src/goto-instrument/goto_program2code.cpp +++ b/src/goto-instrument/goto_program2code.cpp @@ -37,6 +37,9 @@ void goto_program2codet::operator()() // gather variable scope information build_dead_map(); + // gather function parameter names to avoid collision with local variables + build_param_names(); + // see whether var args are in use, identify va_list symbol scan_for_varargs(); @@ -101,6 +104,27 @@ void goto_program2codet::build_dead_map() } } +void goto_program2codet::build_param_names() +{ + param_names.clear(); + + // Get function parameters from the symbol table + const symbolt *func_symbol = nullptr; + if(!ns.lookup(func_name, func_symbol) && func_symbol->type.id() == ID_code) + { + const code_typet &code_type = to_code_type(func_symbol->type); + const code_typet::parameterst ¶meters = code_type.parameters(); + + // Store the base names of parameters (as they appear in C output) + for(const auto ¶m : parameters) + { + const irep_idt ¶m_base_name = param.get_base_name(); + if(!param_base_name.empty()) + param_names.insert(param_base_name); + } + } +} + void goto_program2codet::scan_for_varargs() { va_list_expr.clear(); @@ -455,6 +479,40 @@ goto_programt::const_targett goto_program2codet::convert_decl( code_frontend_declt d = code_frontend_declt{target->decl_symbol()}; symbol_exprt &symbol = d.symbol(); + // Check if the local variable's base name conflicts with a function + // parameter's base name or with another local variable's base name. If so, + // rename the local variable to avoid collision. + const symbolt *local_symbol_ptr = nullptr; + if(!ns.lookup(symbol.get_identifier(), local_symbol_ptr)) + { + const symbolt &local_symbol = *local_symbol_ptr; + irep_idt base_name = local_symbol.base_name; + + if( + !base_name.empty() && + (param_names.find(base_name) != param_names.end() || + used_local_names.find(base_name) != used_local_names.end())) + { + // Generate a unique base name by appending a suffix + irep_idt new_base_name; + unsigned suffix = 1; + do + { + new_base_name = id2string(base_name) + "$" + std::to_string(suffix); + ++suffix; + } while(param_names.find(new_base_name) != param_names.end() || + used_local_names.find(new_base_name) != used_local_names.end()); + + // Update the symbol in the symbol table with the new base name + symbolt &sym = symbol_table.get_writeable_ref(symbol.get_identifier()); + sym.base_name = new_base_name; + base_name = new_base_name; + } + + // Track this local variable's base name + used_local_names.insert(base_name); + } + goto_programt::const_targett next=target; ++next; CHECK_RETURN(next != goto_program.instructions.end()); diff --git a/src/goto-instrument/goto_program2code.h b/src/goto-instrument/goto_program2code.h index 8bb837cb48a..bf867cfa276 100644 --- a/src/goto-instrument/goto_program2code.h +++ b/src/goto-instrument/goto_program2code.h @@ -100,11 +100,14 @@ class goto_program2codet std::unordered_set local_static_set; std::unordered_set type_names_set; std::unordered_set const_removed; + std::unordered_set param_names; + std::unordered_set used_local_names; void copy_source_location(goto_programt::const_targett, codet &dst); void build_loop_map(); void build_dead_map(); + void build_param_names(); void scan_for_varargs(); void cleanup_code(codet &code, const irep_idt parent_stmt);