diff --git a/regression/cbmc/gcc_popcount1/main.c b/regression/cbmc/gcc_popcount1/main.c new file mode 100644 index 0000000000..a7b3386c4c --- /dev/null +++ b/regression/cbmc/gcc_popcount1/main.c @@ -0,0 +1,41 @@ +#include + +#ifndef __GNUC__ +int __builtin_popcount(unsigned int); +int __builtin_popcountl(unsigned long); +int __builtin_popcountll(unsigned long long); +#endif + +unsigned int __VERIFIER_nondet_unsigned(); +unsigned long __VERIFIER_nondet_unsigned_long(); +unsigned long long __VERIFIER_nondet_unsigned_long_long(); + +// Hacker's Delight +// http://www.hackersdelight.org/permissions.htm +int pop4(unsigned long long x) +{ + int n = 0; + + // variant with additional bounding to make sure symbolic execution always + // terminates without having to specify an unwinding bound + for(int i = 0; x != 0 && i < sizeof(x) * 8; ++i) + { + ++n; + x = x & (x - 1); + } + + return n; +} + +int main() +{ + assert(pop4(42) == 3); + assert(__builtin_popcount(42) == 3); + assert(__builtin_popcountl(42) == 3); + assert(__builtin_popcountll(42) == 3); + + unsigned int u = __VERIFIER_nondet_unsigned(); + assert(pop4(u) == __builtin_popcount(u)); + + return 0; +} diff --git a/regression/cbmc/gcc_popcount1/test.desc b/regression/cbmc/gcc_popcount1/test.desc new file mode 100644 index 0000000000..9efefbc736 --- /dev/null +++ b/regression/cbmc/gcc_popcount1/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc/gcc_popcount2/main.c b/regression/cbmc/gcc_popcount2/main.c new file mode 100644 index 0000000000..1173e7d160 --- /dev/null +++ b/regression/cbmc/gcc_popcount2/main.c @@ -0,0 +1,44 @@ +#include + +#ifndef __GNUC__ +int __builtin_popcount(unsigned int); +int __builtin_popcountl(unsigned long); +int __builtin_popcountll(unsigned long long); +#endif + +unsigned int __VERIFIER_nondet_unsigned(); +unsigned long __VERIFIER_nondet_unsigned_long(); +unsigned long long __VERIFIER_nondet_unsigned_long_long(); + +// Hacker's Delight +// http://www.hackersdelight.org/permissions.htm +int pop4(unsigned long long x) +{ + int n = 0; + + // variant with additional bounding to make sure symbolic execution always + // terminates without having to specify an unwinding bound + for(int i = 0; x != 0 && i < sizeof(x) * 8; ++i) + { + ++n; + x = x & (x - 1); + } + + return n; +} + +int main() +{ + unsigned long ul = __VERIFIER_nondet_unsigned_long(); + assert(pop4(ul) == __builtin_popcountl(ul)); + + unsigned long long ull = __VERIFIER_nondet_unsigned_long_long(); + assert(pop4(ull) == __builtin_popcountll(ull)); + + // expected to fail as bits may have been cut off + assert( + sizeof(ull) != sizeof(unsigned int) && + pop4(ull) == __builtin_popcount(ull)); + + return 0; +} diff --git a/regression/cbmc/gcc_popcount2/test.desc b/regression/cbmc/gcc_popcount2/test.desc new file mode 100644 index 0000000000..61ed2b2c83 --- /dev/null +++ b/regression/cbmc/gcc_popcount2/test.desc @@ -0,0 +1,10 @@ +THOROUGH +main.c + +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +\[main\.assertion\.1\] assertion sizeof\(ull\) != sizeof\(unsigned int\) && pop4\(ull\) == __builtin_popcount\(ull\): FAILURE$ +^\*\* 1 of 3 failed +-- +^warning: ignoring diff --git a/src/solvers/Makefile b/src/solvers/Makefile index e49c9d3c3f..73c973836c 100644 --- a/src/solvers/Makefile +++ b/src/solvers/Makefile @@ -157,6 +157,7 @@ SRC = $(BOOLEFORCE_SRC) \ floatbv/float_bv.cpp \ floatbv/float_utils.cpp \ floatbv/float_approximation.cpp \ + lowering/popcount.cpp \ miniBDD/miniBDD.cpp \ prop/aig.cpp \ prop/aig_prop.cpp \ diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp index 245941c040..d8a475239c 100644 --- a/src/solvers/flattening/boolbv.cpp +++ b/src/solvers/flattening/boolbv.cpp @@ -27,6 +27,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "boolbv_type.h" #include "../floatbv/float_utils.h" +#include "../lowering/expr_lowering.h" bool boolbvt::literal( const exprt &expr, @@ -305,6 +306,8 @@ bvt boolbvt::convert_bitvector(const exprt &expr) float_utils.debug2(bv0, bv1); return bv; } + else if(expr.id() == ID_popcount) + return convert_bv(lower_popcount(to_popcount_expr(expr), ns)); return conversion_failed(expr); } diff --git a/src/solvers/lowering/expr_lowering.h b/src/solvers/lowering/expr_lowering.h new file mode 100644 index 0000000000..3edd4964ef --- /dev/null +++ b/src/solvers/lowering/expr_lowering.h @@ -0,0 +1,23 @@ +/*******************************************************************\ + +Module: Lower expressions to arithmetic and logic expressions + +Author: Michael Tautschnig + +\*******************************************************************/ + +#ifndef CPROVER_SOLVERS_LOWERING_EXPR_LOWERING_H +#define CPROVER_SOLVERS_LOWERING_EXPR_LOWERING_H + +#include + +class namespacet; +class popcount_exprt; + +/// Lower a popcount_exprt to arithmetic and logic expressions +/// \param expr Input expression to be translated +/// \param ns Namespace for type lookups +/// \return Semantically equivalent expression +exprt lower_popcount(const popcount_exprt &expr, const namespacet &ns); + +#endif /* CPROVER_SOLVERS_LOWERING_EXPR_LOWERING_H */ diff --git a/src/solvers/lowering/popcount.cpp b/src/solvers/lowering/popcount.cpp new file mode 100644 index 0000000000..3a6e6fd5b2 --- /dev/null +++ b/src/solvers/lowering/popcount.cpp @@ -0,0 +1,59 @@ +/*******************************************************************\ + +Module: Lowering of popcount + +Author: Michael Tautschnig + +\*******************************************************************/ + +#include "expr_lowering.h" + +#include +#include +#include +#include + +exprt lower_popcount(const popcount_exprt &expr, const namespacet &ns) +{ + // Hacker's Delight, variant pop0: + // x = (x & 0x55555555) + ((x >> 1) & 0x55555555); + // x = (x & 0x33333333) + ((x >> 2) & 0x33333333); + // x = (x & 0x0F0F0F0F) + ((x >> 4) & 0x0F0F0F0F); + // x = (x & 0x00FF00FF) + ((x >> 8) & 0x00FF00FF); + // etc. + // return x; + // http://www.hackersdelight.org/permissions.htm + + // make sure the operand width is a power of two + exprt x = expr.op(); + const mp_integer x_width = pointer_offset_bits(x.type(), ns); + CHECK_RETURN(x_width > 0); + const std::size_t bits = address_bits(x_width); + const std::size_t new_width = integer2size_t(power(2, bits)); + const bool need_typecast = + new_width > x_width || x.type().id() != ID_unsignedbv; + if(need_typecast) + x.make_typecast(unsignedbv_typet(new_width)); + + // repeatedly compute x = (x & bitmask) + ((x >> shift) & bitmask) + for(std::size_t shift = 1; shift < new_width; shift <<= 1) + { + // x >> shift + lshr_exprt shifted_x( + x, from_integer(shift, unsignedbv_typet(address_bits(shift) + 1))); + // bitmask is a string of alternating shift-many bits starting from lsb set + // to 1 + std::string bitstring; + bitstring.reserve(new_width); + for(std::size_t i = 0; i < new_width / (2 * shift); ++i) + bitstring += std::string(shift, '0') + std::string(shift, '1'); + constant_exprt bitmask(bitstring, x.type()); + // build the expression + x = plus_exprt(bitand_exprt(x, bitmask), bitand_exprt(shifted_x, bitmask)); + } + + // the result is restricted to the result type + x.make_typecast(expr.type()); + + return x; +}