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

Open
wants to merge 1 commit into
base: develop
Choose a base branch
from
Open

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 @@
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)

Check warning on line 952 in src/goto-programs/interpreter_evaluate.cpp

View check run for this annotation

Codecov / codecov/patch

src/goto-programs/interpreter_evaluate.cpp#L952 

Added line #L952 was not covered by tests
{
// 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]);

Check warning on line 955 in src/goto-programs/interpreter_evaluate.cpp

View check run for this annotation

Codecov / codecov/patch

src/goto-programs/interpreter_evaluate.cpp#L954-L955 

Added lines #L954 - L955 were not covered by tests

const auto &subtype = to_array_type(expr.type()).element_type();

Check warning on line 957 in src/goto-programs/interpreter_evaluate.cpp

View check run for this annotation

Codecov / codecov/patch

src/goto-programs/interpreter_evaluate.cpp#L957 

Added line #L957 was not covered by tests

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))

Check warning on line 959 in src/goto-programs/interpreter_evaluate.cpp

View check run for this annotation

Codecov / codecov/patch

src/goto-programs/interpreter_evaluate.cpp#L959 

Added line #L959 was not covered by tests
{
// Ignore indices < 0, which the string solver sometimes produces
if(where[0] < 0)
return {};

Check warning on line 963 in src/goto-programs/interpreter_evaluate.cpp

View check run for this annotation

Codecov / codecov/patch

src/goto-programs/interpreter_evaluate.cpp#L962-L963 

Added lines #L962 - L963 were not covered by tests

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;

Check warning on line 967 in src/goto-programs/interpreter_evaluate.cpp

View check run for this annotation

Codecov / codecov/patch

src/goto-programs/interpreter_evaluate.cpp#L965-L967 

Added lines #L965 - L967 were not covered by tests

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);

Check warning on line 970 in src/goto-programs/interpreter_evaluate.cpp

View check run for this annotation

Codecov / codecov/patch

src/goto-programs/interpreter_evaluate.cpp#L969-L970 

Added lines #L969 - L970 were not covered by tests

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];
}

Check warning on line 975 in src/goto-programs/interpreter_evaluate.cpp

View check run for this annotation

Codecov / codecov/patch

src/goto-programs/interpreter_evaluate.cpp#L972-L975 

Added lines #L972 - L975 were not covered by tests
}

return dest;

Check warning on line 978 in src/goto-programs/interpreter_evaluate.cpp

View check run for this annotation

Codecov / codecov/patch

src/goto-programs/interpreter_evaluate.cpp#L978 

Added line #L978 was not covered by tests
}
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 @@
(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 @@
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 @@
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)

Check warning on line 1030 in src/pointer-analysis/value_set.cpp

View check run for this annotation

Codecov / codecov/patch

src/pointer-analysis/value_set.cpp#L1030 

Added line #L1030 was not covered by tests
{
get_value_set_rec(
with_expr.operands()[i + 1],

Check warning on line 1033 in src/pointer-analysis/value_set.cpp

View check run for this annotation

Codecov / codecov/patch

src/pointer-analysis/value_set.cpp#L1032-L1033 

Added lines #L1032 - L1033 were not covered by tests
dest,
includes_nondet_pointer,
"",
original_type,
ns);
}
}
}
else if(expr.type().id() == ID_array && !suffix.empty())
Expand All @@ -1040,13 +1055,16 @@
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 @@
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 @@
}
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 @@
{
// 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)

Check warning on line 1062 in src/pointer-analysis/value_set_fi.cpp

View check run for this annotation

Codecov / codecov/patch

src/pointer-analysis/value_set_fi.cpp#L1062 

Added line #L1062 was not covered by tests
{
const exprt &member_operand = rhs_with.operands()[i];

Check warning on line 1064 in src/pointer-analysis/value_set_fi.cpp

View check run for this annotation

Codecov / codecov/patch

src/pointer-analysis/value_set_fi.cpp#L1064 

Added line #L1064 was not covered by tests

const irep_idt &component_name=
member_operand.get(ID_component_name);
const irep_idt &component_name =
member_operand.get(ID_component_name);

Check warning on line 1067 in src/pointer-analysis/value_set_fi.cpp

View check run for this annotation

Codecov / codecov/patch

src/pointer-analysis/value_set_fi.cpp#L1066-L1067 

Added lines #L1066 - L1067 were not covered by tests

if(component_name==name)
{
// yes! just take op2
rhs_member = rhs_with.new_value();
if(component_name == name)

Check warning on line 1069 in src/pointer-analysis/value_set_fi.cpp

View check run for this annotation

Codecov / codecov/patch

src/pointer-analysis/value_set_fi.cpp#L1069 

Added line #L1069 was not covered by tests
{
rhs_member = rhs_with.operands()[i + 1];

Check warning on line 1071 in src/pointer-analysis/value_set_fi.cpp

View check run for this annotation

Codecov / codecov/patch

src/pointer-analysis/value_set_fi.cpp#L1071 

Added line #L1071 was not covered by tests
member_found = true;
}
}
else
if(!member_found)

Check warning on line 1075 in src/pointer-analysis/value_set_fi.cpp

View check run for this annotation

Codecov / codecov/patch

src/pointer-analysis/value_set_fi.cpp#L1075 

Added line #L1075 was not covered by tests
{
// no! do op0
rhs_member=exprt(ID_member, subtype);
Expand Down Expand Up @@ -1126,13 +1130,17 @@
}
else if(rhs.id()==ID_with)
{
const with_exprt &with_expr = to_with_expr(rhs);

Check warning on line 1133 in src/pointer-analysis/value_set_fi.cpp

View check run for this annotation

Codecov / codecov/patch

src/pointer-analysis/value_set_fi.cpp#L1133 

Added line #L1133 was not covered by tests
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)

Check warning on line 1140 in src/pointer-analysis/value_set_fi.cpp

View check run for this annotation

Codecov / codecov/patch

src/pointer-analysis/value_set_fi.cpp#L1140 

Added line #L1140 was not covered by tests
{
assign(lhs_index, with_expr.operands()[i + 1], ns);

Check warning on line 1142 in src/pointer-analysis/value_set_fi.cpp

View check run for this annotation

Codecov / codecov/patch

src/pointer-analysis/value_set_fi.cpp#L1142 

Added line #L1142 was not covered by tests
}
}
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 @@
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)

Check warning on line 145 in src/solvers/smt2/smt2_format.cpp

View check run for this annotation

Codecov / codecov/patch

src/solvers/smt2/smt2_format.cpp#L142-L145 

Added lines #L142 - L145 were not covered by tests
{
out << smt2_format(with_expr.operands()[i]) << ' '
Copy link
Member

Choose a reason for hiding this comment

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

That actually works?

Copy link
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?

Copy link
Member

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

Copy link
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]) << ')';

Check warning on line 148 in src/solvers/smt2/smt2_format.cpp

View check run for this annotation

Codecov / codecov/patch

src/solvers/smt2/smt2_format.cpp#L147-L148 

Added lines #L147 - L148 were not covered by tests
}
}
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)
Copy link
Member

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.

Copy link
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
Loading