From ebbbccb38afaf56498904fe43e396741c74c407a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 26 Jun 2025 19:50:46 +0000 Subject: [PATCH] Fix support for `with_exprt` with more than 3 operands A `with_exprt` needs to have at least 3 operands, but can encode multiple updates when using more operands (where any further operands need to come in pairs of two: an index/member and a new value). We already support this in several places, but were still missing support in others. This led to wrong verification results in Kani as recent changes in CBMC make increasing use of the value set (which is among those fixed in this commit). --- src/goto-programs/interpreter_evaluate.cpp | 38 +++--- src/pointer-analysis/value_set.cpp | 111 +++++++++++------- src/pointer-analysis/value_set_fi.cpp | 28 +++-- src/solvers/smt2/smt2_format.cpp | 11 +- .../strings/string_refinement_util.cpp | 9 +- src/util/simplify_expr.cpp | 3 +- 6 files changed, 123 insertions(+), 77 deletions(-) diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp index 72707e3692f..070ec496694 100644 --- a/src/goto-programs/interpreter_evaluate.cpp +++ b/src/goto-programs/interpreter_evaluate.cpp @@ -948,30 +948,34 @@ interpretert::mp_vectort interpretert::evaluate(const exprt &expr) const auto &wexpr=to_with_expr(expr); mp_vectort dest = evaluate(wexpr.old()); - mp_vectort where = evaluate(wexpr.where()); - mp_vectort new_value = evaluate(wexpr.new_value()); - const auto &subtype = to_array_type(expr.type()).element_type(); - - if(!new_value.empty() && where.size()==1 && !unbounded_size(subtype)) + for(std::size_t i = 1; i < wexpr.operands().size(); i += 2) { - // Ignore indices < 0, which the string solver sometimes produces - if(where[0]<0) - return {}; + mp_vectort where = evaluate(wexpr.operands()[i]); + mp_vectort new_value = evaluate(wexpr.operands()[i + 1]); + + const auto &subtype = to_array_type(expr.type()).element_type(); - mp_integer where_idx=where[0]; - mp_integer subtype_size=get_size(subtype); - mp_integer need_size=(where_idx+1)*subtype_size; + if(!new_value.empty() && where.size() == 1 && !unbounded_size(subtype)) + { + // Ignore indices < 0, which the string solver sometimes produces + if(where[0] < 0) + return {}; - if(dest.size()(need_size), 0); + mp_integer where_idx = where[0]; + mp_integer subtype_size = get_size(subtype); + mp_integer need_size = (where_idx + 1) * subtype_size; - for(std::size_t i=0; i((where_idx * subtype_size) + i)] = - new_value[i]; + if(dest.size() < need_size) + dest.resize(numeric_cast_v(need_size), 0); - return {}; + for(std::size_t i = 0; i < new_value.size(); ++i) + dest[numeric_cast_v((where_idx * subtype_size) + i)] = + new_value[i]; + } } + + return dest; } else if(expr.id()==ID_nil) { diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp index 626777ec8bf..a1e36ca96f6 100644 --- a/src/pointer-analysis/value_set.cpp +++ b/src/pointer-analysis/value_set.cpp @@ -973,26 +973,38 @@ void value_sett::get_value_set_rec( (expr.type().id() == ID_struct_tag || expr.type().id() == ID_struct) && !suffix.empty()) { - irep_idt component_name = with_expr.where().get(ID_component_name); - if(suffix_starts_with_field(suffix, id2string(component_name))) + bool any_matching_suffix = false; + bool all_matching_component_names = true; + for(std::size_t i = 1; i < with_expr.operands().size(); i += 2) { - // Looking for the member overwritten by this WITH expression - std::string remaining_suffix = - strip_first_field_from_suffix(suffix, id2string(component_name)); - get_value_set_rec( - with_expr.new_value(), - dest, - includes_nondet_pointer, - remaining_suffix, - original_type, - ns); + irep_idt component_name = + with_expr.operands()[i].get(ID_component_name); + if(suffix_starts_with_field(suffix, id2string(component_name))) + { + // Looking for the member overwritten by this WITH expression + any_matching_suffix = true; + std::string remaining_suffix = + strip_first_field_from_suffix(suffix, id2string(component_name)); + get_value_set_rec( + with_expr.operands()[i + 1], + dest, + includes_nondet_pointer, + remaining_suffix, + original_type, + ns); + } + else if( + all_matching_component_names && + (expr.type().id() != ID_struct || + !to_struct_type(expr.type()).has_component(component_name)) && + (expr.type().id() != ID_struct_tag || + !ns.follow_tag(to_struct_tag_type(expr.type())) + .has_component(component_name))) + { + all_matching_component_names = false; + } } - else if( - (expr.type().id() == ID_struct && - to_struct_type(expr.type()).has_component(component_name)) || - (expr.type().id() == ID_struct_tag && - ns.follow_tag(to_struct_tag_type(expr.type())) - .has_component(component_name))) + if(!any_matching_suffix && all_matching_component_names) { // Looking for a non-overwritten member, look through this expression get_value_set_rec( @@ -1003,7 +1015,7 @@ void value_sett::get_value_set_rec( original_type, ns); } - else + else if(!any_matching_suffix) { // Member we're looking for is not defined in this struct -- this // must be a reinterpret cast of some sort. Default to conservatively @@ -1015,13 +1027,16 @@ void value_sett::get_value_set_rec( suffix, original_type, ns); - get_value_set_rec( - with_expr.new_value(), - dest, - includes_nondet_pointer, - "", - original_type, - ns); + for(std::size_t i = 1; i < with_expr.operands().size(); i += 2) + { + get_value_set_rec( + with_expr.operands()[i + 1], + dest, + includes_nondet_pointer, + "", + original_type, + ns); + } } } else if(expr.type().id() == ID_array && !suffix.empty()) @@ -1040,13 +1055,16 @@ void value_sett::get_value_set_rec( suffix, original_type, ns); - get_value_set_rec( - with_expr.new_value(), - dest, - includes_nondet_pointer, - new_value_suffix, - original_type, - ns); + for(std::size_t i = 1; i < with_expr.operands().size(); i += 2) + { + get_value_set_rec( + with_expr.operands()[i + 1], + dest, + includes_nondet_pointer, + new_value_suffix, + original_type, + ns); + } } else { @@ -1059,13 +1077,16 @@ void value_sett::get_value_set_rec( suffix, original_type, ns); - get_value_set_rec( - with_expr.new_value(), - dest, - includes_nondet_pointer, - "", - original_type, - ns); + for(std::size_t i = 1; i < with_expr.operands().size(); i += 2) + { + get_value_set_rec( + with_expr.operands()[i + 1], + dest, + includes_nondet_pointer, + "", + original_type, + ns); + } } } else if(expr.id()==ID_array) @@ -1624,14 +1645,18 @@ void value_sett::assign( } else if(rhs.id()==ID_with) { + const with_exprt &with_expr = to_with_expr(rhs); const index_exprt op0_index( - to_with_expr(rhs).old(), + with_expr.old(), exprt(ID_unknown, c_index_type()), to_array_type(lhs.type()).element_type()); assign(lhs_index, op0_index, ns, is_simplified, add_to_sets); - assign( - lhs_index, to_with_expr(rhs).new_value(), ns, is_simplified, true); + for(std::size_t i = 1; i < with_expr.operands().size(); i += 2) + { + assign( + lhs_index, with_expr.operands()[i + 1], ns, is_simplified, true); + } } else { diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp index bf634d07264..dde28bba109 100644 --- a/src/pointer-analysis/value_set_fi.cpp +++ b/src/pointer-analysis/value_set_fi.cpp @@ -1058,17 +1058,21 @@ void value_set_fit::assign( { // see if this is the member we want const auto &rhs_with = to_with_expr(rhs); - const exprt &member_operand = rhs_with.where(); + bool member_found = false; + for(std::size_t i = 1; i < rhs_with.operands().size(); i += 2) + { + const exprt &member_operand = rhs_with.operands()[i]; - const irep_idt &component_name= - member_operand.get(ID_component_name); + const irep_idt &component_name = + member_operand.get(ID_component_name); - if(component_name==name) - { - // yes! just take op2 - rhs_member = rhs_with.new_value(); + if(component_name == name) + { + rhs_member = rhs_with.operands()[i + 1]; + member_found = true; + } } - else + if(!member_found) { // no! do op0 rhs_member=exprt(ID_member, subtype); @@ -1126,13 +1130,17 @@ void value_set_fit::assign( } else if(rhs.id()==ID_with) { + const with_exprt &with_expr = to_with_expr(rhs); const index_exprt op0_index( - to_with_expr(rhs).old(), + with_expr.old(), exprt(ID_unknown, c_index_type()), to_array_type(lhs.type()).element_type()); assign(lhs_index, op0_index, ns); - assign(lhs_index, to_with_expr(rhs).new_value(), ns); + for(std::size_t i = 1; i < with_expr.operands().size(); i += 2) + { + assign(lhs_index, with_expr.operands()[i + 1], ns); + } } else { diff --git a/src/solvers/smt2/smt2_format.cpp b/src/solvers/smt2/smt2_format.cpp index a4771c632fe..49dbb23194f 100644 --- a/src/solvers/smt2/smt2_format.cpp +++ b/src/solvers/smt2/smt2_format.cpp @@ -139,9 +139,14 @@ std::ostream &smt2_format_rec(std::ostream &out, const exprt &expr) else if(expr.id() == ID_with && expr.type().id() == ID_array) { const auto &with_expr = to_with_expr(expr); - out << "(store " << smt2_format(with_expr.old()) << ' ' - << smt2_format(with_expr.where()) << ' ' - << smt2_format(with_expr.new_value()) << ')'; + for(std::size_t i = 1; i < with_expr.operands().size(); i += 2) + out << "(store "; + out << smt2_format(with_expr.old()) << ' '; + for(std::size_t i = 1; i < with_expr.operands().size(); i += 2) + { + out << smt2_format(with_expr.operands()[i]) << ' ' + << smt2_format(with_expr.operands()[i + 1]) << ')'; + } } else if(expr.id() == ID_array_list) { diff --git a/src/solvers/strings/string_refinement_util.cpp b/src/solvers/strings/string_refinement_util.cpp index db1cc2a57c1..80b1fc600b0 100644 --- a/src/solvers/strings/string_refinement_util.cpp +++ b/src/solvers/strings/string_refinement_util.cpp @@ -70,9 +70,12 @@ sparse_arrayt::sparse_arrayt(const with_exprt &expr) while(can_cast_expr(ref.get())) { const auto &with_expr = expr_dynamic_cast(ref.get()); - const auto current_index = - numeric_cast_v(to_constant_expr(with_expr.where())); - entries[current_index] = with_expr.new_value(); + for(std::size_t i = 1; i < with_expr.operands().size(); i += 2) + { + const auto current_index = + numeric_cast_v(to_constant_expr(with_expr.operands()[i])); + entries[current_index] = with_expr.operands()[i + 1]; + } ref = with_expr.old(); } diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index b6f19abda7b..46eb3c11825 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -2157,7 +2157,7 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr) * value) */ - if(value.id()==ID_with) + if(value.id() == ID_with && value.operands().size() == 3) { const with_exprt &with=to_with_expr(value); @@ -2297,6 +2297,7 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr) if( expr_at_offset_C.id() == ID_with && + expr_at_offset_C.operands().size() == 3 && to_with_expr(expr_at_offset_C).where().is_zero()) { tmp.set_op(to_with_expr(expr_at_offset_C).old());