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.
This commit is contained in:
parent
ddde9dc85f
commit
716103ee1d
|
@ -0,0 +1,41 @@
|
|||
#include <assert.h>
|
||||
|
||||
#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;
|
||||
}
|
|
@ -0,0 +1,8 @@
|
|||
CORE
|
||||
main.c
|
||||
|
||||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
^VERIFICATION SUCCESSFUL$
|
||||
--
|
||||
^warning: ignoring
|
|
@ -0,0 +1,44 @@
|
|||
#include <assert.h>
|
||||
|
||||
#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;
|
||||
}
|
|
@ -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
|
|
@ -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 \
|
||||
|
|
|
@ -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);
|
||||
}
|
||||
|
|
|
@ -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 <util/expr.h>
|
||||
|
||||
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 */
|
|
@ -0,0 +1,59 @@
|
|||
/*******************************************************************\
|
||||
|
||||
Module: Lowering of popcount
|
||||
|
||||
Author: Michael Tautschnig
|
||||
|
||||
\*******************************************************************/
|
||||
|
||||
#include "expr_lowering.h"
|
||||
|
||||
#include <util/arith_tools.h>
|
||||
#include <util/invariant.h>
|
||||
#include <util/pointer_offset_size.h>
|
||||
#include <util/std_expr.h>
|
||||
|
||||
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;
|
||||
}
|
Loading…
Reference in New Issue