From 21f8b0def5af71724f8da26c60ac233efc99ca31 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 29 Nov 2025 20:29:11 +0100 Subject: [PATCH] Remove SSA thread suffix in goto trace address-of expressions SSA thread suffixes (e.g., "!0", "@1") are internal SSA identifiers that should be removed when displaying trace information to users. Similar SSA suffix removal logic already existed in `src/goto-programs/graphml_witness.cpp` (the `remove_l0_l1` function), but this logic was not being applied to expressions in the goto trace formatting code. Fixes: #902 --- .../pointer-function-parameters-2/test.desc | 10 +- .../pointer-function-parameters/test.desc | 4 +- src/goto-programs/goto_trace.cpp | 94 +++++++++++++++---- 3 files changed, 81 insertions(+), 27 deletions(-) diff --git a/regression/cbmc-cover/pointer-function-parameters-2/test.desc b/regression/cbmc-cover/pointer-function-parameters-2/test.desc index c107c04e1ce..abe8e8a2c22 100644 --- a/regression/cbmc-cover/pointer-function-parameters-2/test.desc +++ b/regression/cbmc-cover/pointer-function-parameters-2/test.desc @@ -6,14 +6,14 @@ main.c a=\(\(signed int \*\*\)NULL\) tmp(\$\d+)?=[^,]* tmp(\$\d+)?=[^,]* -a=&tmp(\$\d+)?!0 +a=&tmp(\$\d+)? tmp(\$\d+)?=\(\(signed int \*\)NULL\) tmp(\$\d+)?=[^,]* -a=&tmp(\$\d+)?!0 -tmp(\$\d+)?=&tmp\$\d+!0 +a=&tmp(\$\d+)? +tmp(\$\d+)?=&tmp(\$\d+)? tmp(\$\d+)?=(-[0-9]+|[012356789][0-9]*|4[0-9]+) -a=&tmp(\$\d+)?!0 -tmp(\$\d+)?=&tmp(\$\d+)?!0 +a=&tmp(\$\d+)? +tmp(\$\d+)?=&tmp(\$\d+)? tmp(\$\d+)?=4 ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/cbmc-cover/pointer-function-parameters/test.desc b/regression/cbmc-cover/pointer-function-parameters/test.desc index d721ba12a6b..a2816054f16 100644 --- a/regression/cbmc-cover/pointer-function-parameters/test.desc +++ b/regression/cbmc-cover/pointer-function-parameters/test.desc @@ -4,8 +4,8 @@ main.c ^\*\* 5 of 5 covered \(100\.0%\)$ ^Test suite:$ ^(tmp(\$\d+)?=[^,]*, a=\(\(signed int \*\)NULL\))|(a=\(\(signed int \*\)NULL\), tmp(\$\d+)?=[^,]*)$ -^(a=&tmp(\$\d+)?!0@1, tmp(\$\d+)?=4)|(tmp(\$\d+)?=4, a=&tmp(\$\d+)?!0@1)$ -^(a=&tmp(\$\d+)?!0@1, tmp(\$\d+)?=([012356789]\d*|4\d+|-\d+))|(tmp(\$\d+)?=([012356789]\d*|4\d+|-\d+), a=&tmp(\$\d+)?!0@1)$ +^(a=&tmp(\$\d+)?, tmp(\$\d+)?=4)|(tmp(\$\d+)?=4, a=&tmp(\$\d+)?)$ +^(a=&tmp(\$\d+)?, tmp(\$\d+)?=([012356789]\d*|4\d+|-\d+))|(tmp(\$\d+)?=([012356789]\d*|4\d+|-\d+), a=&tmp(\$\d+)?)$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp index c3e283978fa..d4a653c35be 100644 --- a/src/goto-programs/goto_trace.cpp +++ b/src/goto-programs/goto_trace.cpp @@ -21,6 +21,7 @@ Author: Daniel Kroening #include #include #include +#include #include #include @@ -52,6 +53,34 @@ std::optional goto_trace_stept::get_lhs_object() const return get_object_rec(full_lhs); } +/// Remove SSA index suffixes (like !0, @1, etc.) from symbol identifiers +/// in the expression tree. This is used to clean up expressions before +/// displaying them in traces. +static void remove_l0_l1(exprt &expr) +{ + if(expr.id() == ID_symbol) + { + if(is_ssa_expr(expr)) + expr = to_ssa_expr(expr).get_original_expr(); + else + { + std::string identifier = id2string(to_symbol_expr(expr).get_identifier()); + + std::string::size_type l0_l1 = identifier.find_first_of("!@"); + if(l0_l1 != std::string::npos) + { + identifier.resize(l0_l1); + to_symbol_expr(expr).set_identifier(identifier); + } + } + + return; + } + + Forall_operands(it, expr) + remove_l0_l1(*it); +} + void goto_tracet::output( const class namespacet &ns, std::ostream &out) const @@ -106,9 +135,11 @@ void goto_trace_stept::output( if(is_assignment()) { - out << " " << format(full_lhs) - << " = " << format(full_lhs_value) - << '\n'; + exprt clean_lhs = full_lhs; + exprt clean_value = full_lhs_value; + remove_l0_l1(clean_lhs); + remove_l0_l1(clean_value); + out << " " << format(clean_lhs) << " = " << format(clean_value) << '\n'; } if(!pc->source_location().is_nil()) @@ -127,7 +158,9 @@ void goto_trace_stept::output( if(!comment.empty()) out << " " << comment << '\n'; - out << " " << format(original_condition) << '\n'; + exprt clean_condition = original_condition; + remove_l0_l1(clean_condition); + out << " " << format(clean_condition) << '\n'; out << '\n'; } } @@ -299,13 +332,20 @@ static void trace_value( if(lhs_object.has_value()) identifier=lhs_object->get_identifier(); - out << from_expr(ns, identifier, full_lhs) << '='; + // Create copies to clean up SSA suffixes + exprt clean_lhs = full_lhs; + remove_l0_l1(clean_lhs); + + out << from_expr(ns, identifier, clean_lhs) << '='; if(value.is_nil()) out << "(assignment removed)"; else { - out << from_expr(ns, identifier, value); + exprt clean_value = value; + remove_l0_l1(clean_value); + + out << from_expr(ns, identifier, clean_value); // the binary representation out << ' ' << messaget::faint << '(' @@ -414,8 +454,9 @@ void show_compact_goto_trace( if(step.pc->is_assert()) { - out << " " - << from_expr(ns, step.function_id, step.original_condition) + exprt clean_condition = step.original_condition; + remove_l0_l1(clean_condition); + out << " " << from_expr(ns, step.function_id, clean_condition) << '\n'; } @@ -471,10 +512,13 @@ void show_compact_goto_trace( } { - auto arg_strings = make_range(step.function_arguments) - .map([&ns, &step](const exprt &arg) { - return from_expr(ns, step.function_id, arg); - }); + auto arg_strings = + make_range(step.function_arguments) + .map([&ns, &step](const exprt &arg) { + exprt clean_arg = arg; + remove_l0_l1(clean_arg); + return from_expr(ns, step.function_id, clean_arg); + }); out << '('; join_strings(out, arg_strings.begin(), arg_strings.end(), ", "); @@ -542,8 +586,9 @@ void show_full_goto_trace( if(step.pc->is_assert()) { - out << " " - << from_expr(ns, step.function_id, step.original_condition) + exprt clean_condition = step.original_condition; + remove_l0_l1(clean_condition); + out << " " << from_expr(ns, step.function_id, clean_condition) << '\n'; } @@ -560,8 +605,9 @@ void show_full_goto_trace( if(!step.pc->source_location().is_nil()) out << " " << step.pc->source_location() << '\n'; - out << " " << from_expr(ns, step.function_id, step.original_condition) - << '\n'; + exprt clean_condition = step.original_condition; + remove_l0_l1(clean_condition); + out << " " << from_expr(ns, step.function_id, clean_condition) << '\n'; } break; @@ -630,7 +676,9 @@ void show_full_goto_trace( if(l_it!=step.io_args.begin()) out << ';'; - out << ' ' << from_expr(ns, step.function_id, *l_it); + exprt clean_arg = *l_it; + remove_l0_l1(clean_arg); + out << ' ' << from_expr(ns, step.function_id, clean_arg); // the binary representation out << " (" << trace_numeric_value(*l_it, ns, options) << ')'; @@ -652,7 +700,9 @@ void show_full_goto_trace( if(l_it!=step.io_args.begin()) out << ';'; - out << ' ' << from_expr(ns, step.function_id, *l_it); + exprt clean_arg = *l_it; + remove_l0_l1(clean_arg); + out << ' ' << from_expr(ns, step.function_id, clean_arg); // the binary representation out << " (" << trace_numeric_value(*l_it, ns, options) << ')'; @@ -676,7 +726,9 @@ void show_full_goto_trace( else out << ", "; - out << from_expr(ns, step.function_id, arg); + exprt clean_arg = arg; + remove_l0_l1(clean_arg); + out << from_expr(ns, step.function_id, clean_arg); } out << ") (depth " << function_depth << ") ####\n"; @@ -770,7 +822,9 @@ static void show_goto_stack_trace( else out << ", "; - out << from_expr(ns, step.function_id, arg); + exprt clean_arg = arg; + remove_l0_l1(clean_arg); + out << from_expr(ns, step.function_id, clean_arg); } out << ')';