Merge pull request #1883 from tautschnig/implement-popcount

Implement popcount

Author: Daniel Kroening

regression/cbmc/gcc_popcount1/main.c

@@ -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;
+}

regression/cbmc/gcc_popcount1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc/gcc_popcount2/main.c

@@ -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;
+}

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

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;

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 \

src/solvers/flattening/boolbv.cpp

@@ -27,6 +27,7 @@ Author: Daniel Kroening, [email protected]
 #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);
 }

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 <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 */

src/solvers/lowering/popcount.cpp

@@ -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;
+}

src/util/simplify_expr.cpp

@@ -136,28 +136,28 @@ 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;
 
         for(result=0; value!=0; value=value>>1)
           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

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(

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<const popcount_exprt &>(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<popcount_exprt &>(expr);
+}
+
+template <>
+inline bool can_cast_expr<popcount_exprt>(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