From b87c98ad0e221c175ae0d09c3f15c354bf71721d Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 31 Oct 2025 10:26:02 +0000 Subject: [PATCH] Simplify WITH expression over structs with a single component When updating the sole member of a struct we can just use the new value. --- .../havoc_slice/functional_slice_bytes.desc | 2 ++ src/util/simplify_expr.cpp | 18 ++++++++++++------ 2 files changed, 14 insertions(+), 6 deletions(-) diff --git a/regression/cbmc/havoc_slice/functional_slice_bytes.desc b/regression/cbmc/havoc_slice/functional_slice_bytes.desc index 03778bda8ca..11b4c13035c 100644 --- a/regression/cbmc/havoc_slice/functional_slice_bytes.desc +++ b/regression/cbmc/havoc_slice/functional_slice_bytes.desc @@ -1,10 +1,12 @@ CORE functional.c -DN=4 -DSLICE_BYTES --program-only +WITH \[.*i!0@1#2:=\{ \.coeffs=byte_extract ^EXIT=0$ ^SIGNAL=0$ -- byte_update +WITH \[.*i!0@1#2:=\{ \{ \.coeffs=\{ -- We want these tests not to produce any byte_update expressions, but instead want updates at specific array indices. diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 1085d8957f0..8670a17b974 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -1470,14 +1470,14 @@ simplify_exprt::resultt<> simplify_exprt::simplify_with(const with_exprt &expr) expr.old().type().id() == ID_struct || expr.old().type().id() == ID_struct_tag) { + const struct_typet &old_type_followed = + expr.old().type().id() == ID_struct_tag + ? ns.follow_tag(to_struct_tag_type(expr.old().type())) + : to_struct_type(expr.old().type()); + const irep_idt &component_name = expr.where().get(ID_component_name); + if(expr.old().id() == ID_struct || expr.old().is_constant()) { - const irep_idt &component_name = expr.where().get(ID_component_name); - - const struct_typet &old_type_followed = - expr.old().type().id() == ID_struct_tag - ? ns.follow_tag(to_struct_tag_type(expr.old().type())) - : to_struct_type(expr.old().type()); if(!old_type_followed.has_component(component_name)) return unchanged(expr); @@ -1490,6 +1490,12 @@ simplify_exprt::resultt<> simplify_exprt::simplify_with(const with_exprt &expr) result.operands()[number] = expr.new_value(); return result; } + else if( + old_type_followed.components().size() == 1 && + old_type_followed.has_component(component_name)) + { + return struct_exprt{{expr.new_value()}, expr.type()}; + } } else if( expr.old().type().id() == ID_array || expr.old().type().id() == ID_vector)