Skip to content

Fix support for with_exprt with more than 3 operands #8668

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
tautschnig wants to merge 1 commit into from
Closed

Fix support for with_exprt with more than 3 operands #8668

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
38 changes: 21 additions & 17 deletions src/goto-programs/interpreter_evaluate.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
dest.resize(numeric_cast_v<std::size_t>(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<new_value.size(); ++i)
dest[numeric_cast_v<std::size_t>((where_idx * subtype_size) + i)] =
new_value[i];
if(dest.size() < need_size)
dest.resize(numeric_cast_v<std::size_t>(need_size), 0);

return {};
for(std::size_t i = 0; i < new_value.size(); ++i)
dest[numeric_cast_v<std::size_t>((where_idx * subtype_size) + i)] =
new_value[i];
}
}

return dest;
}
else if(expr.id()==ID_nil)
{
Expand Down
111 changes: 68 additions & 43 deletions src/pointer-analysis/value_set.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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(
Expand All @@ -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
Expand All @@ -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())
Expand All @@ -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
{
Expand All @@ -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)
Expand Down Expand Up @@ -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
{
Expand Down
28 changes: 18 additions & 10 deletions src/pointer-analysis/value_set_fi.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down Expand Up @@ -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
{
Expand Down
11 changes: 8 additions & 3 deletions src/solvers/smt2/smt2_format.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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]) << ' '

@kroening kroening Jul 2, 2025

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That actually works?

@tautschnig tautschnig Jul 3, 2025

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is code is never used so I don't know for sure, but which reason do you have to believe it does not?

@kroening kroening Jul 5, 2025

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

store appears to exist as a three-operand variant only: https://smt-lib.org/theories-ArraysEx.shtml

@tautschnig tautschnig Jul 5, 2025

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, sure, but note how the prior loop creates (store (store (store ... (lines 142 and 143).

<< smt2_format(with_expr.operands()[i + 1]) << ')';
}
}
else if(expr.id() == ID_array_list)
{
Expand Down
9 changes: 6 additions & 3 deletions src/solvers/strings/string_refinement_util.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -70,9 +70,12 @@ sparse_arrayt::sparse_arrayt(const with_exprt &expr)
while(can_cast_expr<with_exprt>(ref.get()))
{
const auto &with_expr = expr_dynamic_cast<with_exprt>(ref.get());
const auto current_index =
numeric_cast_v<std::size_t>(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<std::size_t>(to_constant_expr(with_expr.operands()[i]));
entries[current_index] = with_expr.operands()[i + 1];
}
ref = with_expr.old();
}

Expand Down
3 changes: 2 additions & 1 deletion src/util/simplify_expr.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)

@kroening kroening Jul 2, 2025

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It may be worth considering to rewrite with expressions with >3 operands to the 3 operand variant.

@tautschnig tautschnig Jul 3, 2025

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If we make the simplifier do this, we might as well refrain from constructing those in the first place? I'm actually inclined to create such a PR as an alternative to this one.

{
const with_exprt &with=to_with_expr(value);

Expand Down Expand Up @@ -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());
Expand Down