Skip to content

Commit 719baf6

Browse files
kroeningkroening
committed
SMT-LIB2: shifts with wider shift distances
This fixes the case of converting shifts where the shift distance is wider than the shift operand to SMT-LIB2. SMT-LIB2 requies that the width of the shift operand and the shift distance is the same. To not loose leading this of the shift distance, use the bigger one of the two as the width of the shift, and truncate the result when needed.
1 parent 56d8598 commit 719baf6

2 files changed

Lines changed: 131 additions & 24 deletions

File tree

‎src/solvers/smt2/smt2_conv.cpp‎

Lines changed: 62 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -1780,21 +1780,21 @@ void smt2_convt::convert_expr(const exprt &expr)
17801780
type.id()==ID_signedbv ||
17811781
type.id()==ID_bv)
17821782
{
1783-
if(shift_expr.id() == ID_ashr)
1784-
out << "(bvashr ";
1785-
else if(shift_expr.id() == ID_lshr)
1786-
out << "(bvlshr ";
1787-
else if(shift_expr.id() == ID_shl)
1788-
out << "(bvshl ";
1789-
else
1790-
UNREACHABLE;
1791-
1792-
convert_expr(shift_expr.op());
1793-
out << " ";
1794-
17951783
// SMT2 requires the shift distance to have the same width as
17961784
// the value that is shifted -- odd!
17971785

1786+
auto emit_operator = [this](const exprt &shift_expr)
1787+
{
1788+
if(shift_expr.id() == ID_ashr)
1789+
out << "(bvashr ";
1790+
else if(shift_expr.id() == ID_lshr)
1791+
out << "(bvlshr ";
1792+
else if(shift_expr.id() == ID_shl)
1793+
out << "(bvshl ";
1794+
else
1795+
UNREACHABLE;
1796+
};
1797+
17981798
const auto &distance_type = shift_expr.distance().type();
17991799
if(distance_type.id() == ID_integer || distance_type.id() == ID_natural)
18001800
{
@@ -1804,29 +1804,70 @@ void smt2_convt::convert_expr(const exprt &expr)
18041804
// shift distance must be bit vector
18051805
std::size_t width_op0 = boolbv_width(shift_expr.op().type());
18061806
exprt tmp=from_integer(i, unsignedbv_typet(width_op0));
1807+
1808+
emit_operator(shift_expr);
1809+
convert_expr(shift_expr.op());
1810+
out << ' ';
18071811
convert_expr(tmp);
1812+
out << ')'; // bv*sh
18081813
}
18091814
else if(
18101815
distance_type.id() == ID_signedbv ||
18111816
distance_type.id() == ID_unsignedbv ||
18121817
distance_type.id() == ID_c_enum || distance_type.id() == ID_c_bool)
18131818
{
1814-
std::size_t width_op0 = boolbv_width(shift_expr.op().type());
1815-
std::size_t width_op1 = boolbv_width(distance_type);
1819+
std::size_t width_op = boolbv_width(shift_expr.op().type());
1820+
std::size_t width_distance = boolbv_width(distance_type);
1821+
std::size_t width_result = boolbv_width(shift_expr.type());
1822+
1823+
if(width_result != width_op)
1824+
UNEXPECTEDCASE(
1825+
"unsupported result width for " + shift_expr.id_string());
18161826

1817-
if(width_op0==width_op1)
1827+
// we use the larger of the two widths
1828+
if(width_op == width_distance)
1829+
{
1830+
emit_operator(shift_expr);
1831+
convert_expr(shift_expr.op());
1832+
out << ' ';
18181833
convert_expr(shift_expr.distance());
1819-
else if(width_op0>width_op1)
1834+
out << ')'; // bv*sh
1835+
}
1836+
else if(width_op > width_distance)
18201837
{
1821-
out << "((_ zero_extend " << width_op0-width_op1 << ") ";
1838+
emit_operator(shift_expr);
1839+
convert_expr(shift_expr.op());
1840+
out << ' ';
1841+
out << "((_ zero_extend " << width_op - width_distance << ") ";
18221842
convert_expr(shift_expr.distance());
1823-
out << ")"; // zero_extend
1843+
out << ')'; // zero_extend
1844+
out << ')'; // bv*sh
18241845
}
1825-
else // width_op0<width_op1
1846+
else // width_op<width_distance -- distance is wider
18261847
{
1827-
out << "((_ extract " << width_op0-1 << " 0) ";
1848+
// enlarge the shift to match the distance operand,
1849+
// then extract again
1850+
out << "((_ extract " << width_op - 1 << " 0) ";
1851+
emit_operator(shift_expr);
1852+
1853+
// use sign extension when needed
1854+
if(shift_expr.op().type().id() == ID_signedbv)
1855+
{
1856+
out << "((_ sign_extend " << width_distance - width_op << ") ";
1857+
convert_expr(shift_expr.op());
1858+
out << ')'; // sign_extend
1859+
}
1860+
else
1861+
{
1862+
out << "((_ zero_extend " << width_distance - width_op << ") ";
1863+
convert_expr(shift_expr.op());
1864+
out << ')'; // zero_extend
1865+
}
1866+
1867+
out << ' ';
18281868
convert_expr(shift_expr.distance());
1829-
out << ")"; // extract
1869+
out << ')'; // bv*sh
1870+
out << ')'; // extract
18301871
}
18311872
}
18321873
else
@@ -1835,8 +1876,6 @@ void smt2_convt::convert_expr(const exprt &expr)
18351876
"unsupported distance type for " + shift_expr.id_string() + ": " +
18361877
distance_type.id_string());
18371878
}
1838-
1839-
out << ")"; // bv*sh
18401879
}
18411880
else
18421881
UNEXPECTEDCASE(

‎unit/solvers/smt2/smt2_conv.cpp‎

Lines changed: 69 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,76 @@
11
// Author: Diffblue Ltd.
22

3-
#include <testing-utils/use_catch.h>
3+
#include <util/bitvector_expr.h>
4+
#include <util/namespace.h>
5+
#include <util/symbol_table.h>
46

57
#include <solvers/smt2/smt2_conv.h>
8+
#include <testing-utils/use_catch.h>
9+
10+
#include <sstream>
11+
12+
/// helper class for testing smt2_convt
13+
class smt2_conv_testt : public smt2_convt
14+
{
15+
public:
16+
smt2_conv_testt(const namespacet &_ns, std::ostream &_out)
17+
: smt2_convt{_ns, "", "", "", smt2_convt::solvert::GENERIC, _out}
18+
{
19+
}
20+
21+
void convert_expr_public(const exprt &expr)
22+
{
23+
convert_expr(expr);
24+
}
25+
};
26+
27+
static std::string smt2(const exprt &expr)
28+
{
29+
symbol_tablet symbol_table;
30+
namespacet ns{symbol_table};
31+
std::ostringstream out;
32+
smt2_conv_testt smt2_conv{ns, out};
33+
std::size_t length = out.str().size();
34+
smt2_conv.convert_expr_public(expr);
35+
return std::string{out.str(), length, std::string::npos};
36+
}
37+
38+
TEST_CASE("smt2_convt conversion for shifts", "[core][solvers][smt2]")
39+
{
40+
GIVEN("An shift expression with equal-with operands")
41+
{
42+
auto op = symbol_exprt{"op", unsignedbv_typet{8}};
43+
auto distance = symbol_exprt{"dist", unsignedbv_typet{8}};
44+
auto shift = shl_exprt{op, distance};
45+
REQUIRE(smt2(shift) == "(bvshl op dist)");
46+
}
47+
48+
GIVEN("An shift expression with an unsigned shift operand and wider distance")
49+
{
50+
auto op = symbol_exprt{"op", unsignedbv_typet{8}};
51+
auto distance = symbol_exprt{"dist", unsignedbv_typet{10}};
52+
auto shift = shl_exprt{op, distance};
53+
REQUIRE(
54+
smt2(shift) == "((_ extract 7 0) (bvshl ((_ zero_extend 2) op) dist))");
55+
}
56+
57+
GIVEN("An shift expression with a signed shift operand and wider distance")
58+
{
59+
auto op = symbol_exprt{"op", signedbv_typet{8}};
60+
auto distance = symbol_exprt{"dist", unsignedbv_typet{10}};
61+
auto shift = ashr_exprt{op, distance};
62+
REQUIRE(
63+
smt2(shift) == "((_ extract 7 0) (bvashr ((_ sign_extend 2) op) dist))");
64+
}
65+
66+
GIVEN("An shift expression with a wider shift operand")
67+
{
68+
auto op = symbol_exprt{"op", unsignedbv_typet{10}};
69+
auto distance = symbol_exprt{"dist", unsignedbv_typet{8}};
70+
auto shift = shl_exprt{op, distance};
71+
REQUIRE(smt2(shift) == "(bvshl op ((_ zero_extend 2) dist))");
72+
}
73+
}
674

775
TEST_CASE(
876
"smt2_convt::convert_identifier character escaping.",

0 commit comments

Comments
 (0)