Introduce popcount_exprt

ID_popcount was previously used without a dedicated class.

Author: tautschnig

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