Skip to content

Commit f9058e7

Browse files
kroeningkroening
authored
Merge pull request diffblue#2246 from diffblue/z3-fpa
smt2: bswap and popcount
2 parents 6b0f265 + d4abbea commit f9058e7

File tree

6 files changed

+84
-12
lines changed

6 files changed

+84
-12
lines changed

‎src/ansi-c/c_typecheck_expr.cpp‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2186,7 +2186,8 @@ exprt c_typecheck_baset::do_special_functions(
21862186
throw 0;
21872187
}
21882188

2189-
bswap_exprt bswap_expr(expr.arguments().front(), expr.type());
2189+
// these are hard-wired to 8 bits according to the gcc manual
2190+
bswap_exprt bswap_expr(expr.arguments().front(), 8, expr.type());
21902191
bswap_expr.add_source_location()=source_location;
21912192

21922193
return bswap_expr;

‎src/solvers/flattening/boolbv_bswap.cpp‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -8,15 +8,14 @@ Author: Michael Tautschnig
88

99
#include "boolbv.h"
1010

11-
#include <util/config.h>
1211
#include <util/invariant.h>
1312

1413
bvt boolbvt::convert_bswap(const bswap_exprt &expr)
1514
{
1615
const std::size_t width = boolbv_width(expr.type());
1716

1817
// width must be multiple of bytes
19-
const std::size_t byte_bits = config.ansi_c.char_width;
18+
const std::size_t byte_bits = expr.get_bits_per_byte();
2019
if(width % byte_bits != 0)
2120
return conversion_failed(expr);
2221

‎src/solvers/smt2/smt2_conv.cpp‎

Lines changed: 64 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -29,9 +29,10 @@ Author: Daniel Kroening, [email protected]
2929
#include <util/string_constant.h>
3030

3131
#include <solvers/flattening/boolbv_width.h>
32-
#include <solvers/flattening/flatten_byte_operators.h>
3332
#include <solvers/flattening/c_bit_field_replacement_type.h>
33+
#include <solvers/flattening/flatten_byte_operators.h>
3434
#include <solvers/floatbv/float_bv.h>
35+
#include <solvers/lowering/expr_lowering.h>
3536

3637
// Mark different kinds of error condition
3738
// General
@@ -1809,6 +1810,68 @@ void smt2_convt::convert_expr(const exprt &expr)
18091810
"smt2_convt::convert_expr: `"+expr.id_string()+
18101811
"' is not yet supported");
18111812
}
1813+
else if(expr.id() == ID_bswap)
1814+
{
1815+
if(expr.operands().size() != 1)
1816+
INVALIDEXPR("bswap gets one operand");
1817+
1818+
if(expr.op0().type() != expr.type())
1819+
INVALIDEXPR("bswap gets one operand with same type");
1820+
1821+
// first 'let' the operand
1822+
out << "(let ((bswap_op ";
1823+
convert_expr(expr.op0());
1824+
out << ")) ";
1825+
1826+
if(expr.type().id() == ID_signedbv || expr.type().id() == ID_unsignedbv)
1827+
{
1828+
const std::size_t width = to_bitvector_type(expr.type()).get_width();
1829+
1830+
// width must be multiple of bytes
1831+
if(width % 8 != 0)
1832+
INVALIDEXPR("bswap must get bytes");
1833+
1834+
const std::size_t bytes = width / 8;
1835+
1836+
if(bytes <= 1)
1837+
out << "bswap_op";
1838+
else
1839+
{
1840+
// do a parallel 'let' for each byte
1841+
out << "(let (";
1842+
1843+
for(std::size_t byte = 0; byte < bytes; byte++)
1844+
{
1845+
if(byte != 0)
1846+
out << ' ';
1847+
out << "(bswap_byte_" << byte << ' ';
1848+
out << "((_ extract " << (byte * 8 + 7) << " " << (byte * 8)
1849+
<< ") bswap_op)";
1850+
out << ')';
1851+
}
1852+
1853+
out << ") ";
1854+
1855+
// now stitch back together with 'concat'
1856+
out << "(concat";
1857+
1858+
for(std::size_t byte = 0; byte < bytes; byte++)
1859+
out << " bswap_byte_" << byte;
1860+
1861+
out << ')'; // concat
1862+
out << ')'; // let bswap_byte_*
1863+
}
1864+
}
1865+
else
1866+
UNEXPECTEDCASE("bswap must get bitvector operand");
1867+
1868+
out << ')'; // let bswap_op
1869+
}
1870+
else if(expr.id() == ID_popcount)
1871+
{
1872+
exprt lowered = lower_popcount(to_popcount_expr(expr), ns);
1873+
convert_expr(lowered);
1874+
}
18121875
else
18131876
UNEXPECTEDCASE(
18141877
"smt2_convt::convert_expr: `"+expr.id_string()+"' is unsupported");

‎src/util/irep_ids.def‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -664,6 +664,7 @@ IREP_ID_TWO(overlay_class, java::com.diffblue.OverlayClassImplementation)
664664
IREP_ID_TWO(overlay_method, java::com.diffblue.OverlayMethodImplementation)
665665
IREP_ID_TWO(C_annotations, #annotations)
666666
IREP_ID_ONE(final)
667+
IREP_ID_ONE(bits_per_byte)
667668

668669
// Projects depending on this code base that wish to extend the list of
669670
// available ids should provide a file local_irep_ids.h in their source tree and

‎src/util/simplify_expr_int.cpp‎

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -28,18 +28,19 @@ bool simplify_exprt::simplify_bswap(bswap_exprt &expr)
2828
{
2929
if(expr.type().id() == ID_unsignedbv && expr.op().is_constant())
3030
{
31+
auto bits_per_byte = expr.get_bits_per_byte();
3132
std::size_t width=to_bitvector_type(expr.type()).get_width();
3233
mp_integer value;
3334
to_integer(expr.op(), value);
3435
std::vector<mp_integer> bytes;
3536

3637
// take apart
37-
for(std::size_t bit=0; bit<width; bit+=8)
38-
bytes.push_back((value >> bit)%256);
38+
for(std::size_t bit = 0; bit < width; bit += bits_per_byte)
39+
bytes.push_back((value >> bit)%power(2, bits_per_byte));
3940

4041
// put back together, but backwards
4142
mp_integer new_value=0;
42-
for(std::size_t bit=0; bit<width; bit+=8)
43+
for(std::size_t bit = 0; bit < width; bit += bits_per_byte)
4344
{
4445
assert(!bytes.empty());
4546
new_value+=bytes.back()<<bit;

‎src/util/std_expr.h‎

Lines changed: 12 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -506,18 +506,25 @@ inline void validate_expr(const unary_minus_exprt &value)
506506
class bswap_exprt: public unary_exprt
507507
{
508508
public:
509-
bswap_exprt(): unary_exprt(ID_bswap)
509+
bswap_exprt(const exprt &_op, std::size_t bits_per_byte, const typet &_type)
510+
: unary_exprt(ID_bswap, _op, _type)
510511
{
512+
set_bits_per_byte(bits_per_byte);
511513
}
512514

513-
bswap_exprt(const exprt &_op, const typet &_type)
514-
: unary_exprt(ID_bswap, _op, _type)
515+
explicit bswap_exprt(const exprt &_op, std::size_t &_bits_per_byte)
516+
: unary_exprt(ID_bswap, _op, _op.type())
515517
{
516518
}
517519

518-
explicit bswap_exprt(const exprt &_op)
519-
: unary_exprt(ID_bswap, _op, _op.type())
520+
std::size_t get_bits_per_byte() const
521+
{
522+
return get_size_t(ID_bits_per_byte);
523+
}
524+
525+
void set_bits_per_byte(std::size_t bits_per_byte)
520526
{
527+
set(ID_bits_per_byte, bits_per_byte);
521528
}
522529
};
523530

0 commit comments

Comments
 (0)