From ddde9dc85fcec1140015759b2dc234ac84944052 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 23 Feb 2018 13:51:20 +0000 Subject: [PATCH 1/2] Introduce popcount_exprt ID_popcount was previously used without a dedicated class. --- src/ansi-c/c_typecheck_expr.cpp | 3 +- src/util/simplify_expr.cpp | 18 +++++------ src/util/simplify_expr_class.h | 3 +- src/util/std_expr.h | 57 +++++++++++++++++++++++++++++++++ 4 files changed, 69 insertions(+), 12 deletions(-) diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index f78b49cfea1..12f324d0c86 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -2355,8 +2355,7 @@ exprt c_typecheck_baset::do_special_functions( throw 0; } - exprt popcount_expr(ID_popcount, expr.type()); - popcount_expr.operands()=expr.arguments(); + popcount_exprt popcount_expr(expr.arguments().front(), expr.type()); popcount_expr.add_source_location()=source_location; return popcount_expr; diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 71a3140d99a..3ff5a7c5ced 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -136,20 +136,19 @@ bool simplify_exprt::simplify_sign(exprt &expr) return true; } -bool simplify_exprt::simplify_popcount(exprt &expr) +bool simplify_exprt::simplify_popcount(popcount_exprt &expr) { - if(expr.operands().size()!=1) - return true; + const exprt &op = expr.op(); - if(expr.op0().is_constant()) + if(op.is_constant()) { - const typet &type=ns.follow(expr.op0().type()); + const typet &type=ns.follow(op.type()); if(type.id()==ID_signedbv || type.id()==ID_unsignedbv) { mp_integer value; - if(!to_integer(expr.op0(), value)) + if(!to_integer(op, value)) { std::size_t result; @@ -157,7 +156,8 @@ bool simplify_exprt::simplify_popcount(exprt &expr) if(value.is_odd()) result++; - expr=from_integer(result, expr.type()); + exprt simp_result = from_integer(result, expr.type()); + expr.swap(simp_result); return false; } @@ -2334,8 +2334,8 @@ bool simplify_exprt::simplify_node(exprt &expr) result=simplify_abs(expr) && result; else if(expr.id()==ID_sign) result=simplify_sign(expr) && result; - else if(expr.id()==ID_popcount) - result=simplify_popcount(expr) && result; + else if(expr.id() == ID_popcount) + result = simplify_popcount(to_popcount_expr(expr)) && result; #ifdef DEBUGX if(!result diff --git a/src/util/simplify_expr_class.h b/src/util/simplify_expr_class.h index 05b963934d3..3bcda0ac352 100644 --- a/src/util/simplify_expr_class.h +++ b/src/util/simplify_expr_class.h @@ -29,6 +29,7 @@ class if_exprt; class index_exprt; class member_exprt; class namespacet; +class popcount_exprt; class tvt; #define forall_value_list(it, value_list) \ @@ -107,7 +108,7 @@ class simplify_exprt bool simplify_isnormal(exprt &expr); bool simplify_abs(exprt &expr); bool simplify_sign(exprt &expr); - bool simplify_popcount(exprt &expr); + bool simplify_popcount(popcount_exprt &expr); // auxiliary bool simplify_if_implies( diff --git a/src/util/std_expr.h b/src/util/std_expr.h index 0191c9593bf..c427e001841 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -4807,4 +4807,61 @@ class exists_exprt:public binary_exprt } }; +/*! \brief The popcount (counting the number of bits set to 1) expression +*/ +class popcount_exprt: public unary_exprt +{ +public: + popcount_exprt(): unary_exprt(ID_popcount) + { + } + + popcount_exprt(const exprt &_op, const typet &_type) + : unary_exprt(ID_popcount, _op, _type) + { + } + + explicit popcount_exprt(const exprt &_op) + : unary_exprt(ID_popcount, _op, _op.type()) + { + } +}; + +/*! \brief Cast a generic exprt to a \ref popcount_exprt + * + * This is an unchecked conversion. \a expr must be known to be \ref + * popcount_exprt. + * + * \param expr Source expression + * \return Object of type \ref popcount_exprt + * + * \ingroup gr_std_expr +*/ +inline const popcount_exprt &to_popcount_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_popcount); + DATA_INVARIANT(expr.operands().size() == 1, "popcount must have one operand"); + return static_cast(expr); +} + +/*! \copydoc to_popcount_expr(const exprt &) + * \ingroup gr_std_expr +*/ +inline popcount_exprt &to_popcount_expr(exprt &expr) +{ + PRECONDITION(expr.id() == ID_popcount); + DATA_INVARIANT(expr.operands().size() == 1, "popcount must have one operand"); + return static_cast(expr); +} + +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_popcount; +} +inline void validate_expr(const popcount_exprt &value) +{ + validate_operands(value, 1, "popcount must have one operand"); +} + #endif // CPROVER_UTIL_STD_EXPR_H From 716103ee1dc0b9097fb791f424ad9a8449dd81d9 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 26 Feb 2018 13:43:10 +0000 Subject: [PATCH 2/2] Implement popcount in SAT back-end Previously only constants were supported via expression simplification. The implementation uses lowering to supported expressions and could thus equally be used in other back-ends. --- regression/cbmc/gcc_popcount1/main.c | 41 +++++++++++++++++ regression/cbmc/gcc_popcount1/test.desc | 8 ++++ regression/cbmc/gcc_popcount2/main.c | 44 ++++++++++++++++++ regression/cbmc/gcc_popcount2/test.desc | 10 +++++ src/solvers/Makefile | 1 + src/solvers/flattening/boolbv.cpp | 3 ++ src/solvers/lowering/expr_lowering.h | 23 ++++++++++ src/solvers/lowering/popcount.cpp | 59 +++++++++++++++++++++++++ 8 files changed, 189 insertions(+) create mode 100644 regression/cbmc/gcc_popcount1/main.c create mode 100644 regression/cbmc/gcc_popcount1/test.desc create mode 100644 regression/cbmc/gcc_popcount2/main.c create mode 100644 regression/cbmc/gcc_popcount2/test.desc create mode 100644 src/solvers/lowering/expr_lowering.h create mode 100644 src/solvers/lowering/popcount.cpp diff --git a/regression/cbmc/gcc_popcount1/main.c b/regression/cbmc/gcc_popcount1/main.c new file mode 100644 index 00000000000..a7b3386c4c8 --- /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 00000000000..9efefbc7362 --- /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 00000000000..1173e7d160a --- /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 00000000000..61ed2b2c833 --- /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 e49c9d3c3f6..73c973836ce 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 245941c0404..d8a475239c6 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 00000000000..3edd4964ef7 --- /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 00000000000..3a6e6fd5b2d --- /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; +}