Skip to content

smt2: fix encoding of with expressions #3639

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

Merged
merged 3 commits into from
Dec 29, 2018
Merged

smt2: fix encoding of with expressions #3639

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
783019a
smt2: fix for with on structs with one member
Dec 29, 2018
1453075
smt2: fix typos in comments
Dec 29, 2018
fbc74de
smt2: fix with expressions for fixed-width arrays
Dec 29, 2018
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
3 changes: 0 additions & 3 deletions scripts/delete_failing_smt2_solver_tests
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -37,14 +37,12 @@ rm Float8/test.desc
rm Linking4/test.desc
rm Linking7/test.desc
rm Linking7/member-name-mismatch.desc
rm Malloc19/test.desc
rm Malloc23/test.desc
rm Malloc24/test.desc
rm Memory_leak2/test.desc
rm Multi_Dimensional_Array2/test.desc
rm Overflow_Leftshift1/test.desc
rm Overflow_Subtraction1/test.desc
rm Pointer_Arithmetic10/test.desc
rm Pointer_Arithmetic11/test.desc
rm Pointer_byte_extract2/test.desc
rm Pointer_byte_extract3/test.desc
Expand Down Expand Up @@ -88,7 +86,6 @@ rm pointer-function-parameters-struct-simple-recursion-2/test.desc
rm pointer-function-parameters-struct-simple-recursion-3/test.desc
rm scanf1/test.desc
rm stack-trace/test.desc
rm struct10/test.desc
rm struct6/test.desc
rm struct7/test.desc
rm struct9/test.desc
Expand Down
20 changes: 11 additions & 9 deletions src/solvers/smt2/smt2_conv.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3476,7 +3476,7 @@ void smt2_convt::convert_with(const with_exprt &expr)
{
std::size_t s=expr.operands().size();

// strip of the trailing two operands
// strip off the trailing two operands
with_exprt tmp = expr;
tmp.operands().resize(s-2);

Expand Down Expand Up @@ -3515,7 +3515,7 @@ void smt2_convt::convert_with(const with_exprt &expr)
std::size_t sub_width=boolbv_width(array_type.subtype());
std::size_t index_width=boolbv_width(expr.where().type());

// We mask out the updated bit with AND,
// We mask out the updated bits with AND,
// and then OR-in the shifted new value.

out << "(let ((distance? ";
Expand All @@ -3540,15 +3540,16 @@ void smt2_convt::convert_with(const with_exprt &expr)

out << "(bvor ";
out << "(bvand ";
out << "(bvlshr (_ bv" << power(2, array_width)-1 << " "
<< array_width << ") ";
out << "distance?) ";
out << "(bvnot ";
out << "(bvshl (_ bv" << power(2, sub_width) - 1 << " " << array_width
<< ") ";
out << "distance?)) "; // bvnot, bvlshl
convert_expr(expr.old());
out << ") "; // bvand
out << "(bvlshr ";
out << "(bvshl ";
out << "((_ zero_extend " << array_width-sub_width << ") ";
convert_expr(expr.new_value());
out << ") distance?)))"; // zero_extend, bvlshr, bvor, let
out << ") distance?)))"; // zero_extend, bvshl, bvor, let
}
}
else if(expr_type.id()==ID_struct)
Expand Down Expand Up @@ -3588,8 +3589,9 @@ void smt2_convt::convert_with(const with_exprt &expr)

if(m.width==struct_width)
{
// the struct is the same as the member, no concat needed
out << "?withop";
// the struct is the same as the member, no concat needed,
// ?withop won't be used
convert_expr(value);
}
else if(m.offset==0)
{
Expand Down