From a14192fd851c658c58090c6e9e035acb92fb7b0e Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 10 Mar 2021 16:05:09 +0000 Subject: [PATCH] Make lower_popcount a method of popcount_exprt Expression lowering may be useful well outside the solvers/ context. Making it a method of the class being lowered also serves as a way of describing the semantics of the expression. This is mainly a refactoring, no changes in behaviour are intended. --- scripts/expected_doxygen_warnings.txt | 4 +- src/solvers/Makefile | 1 - src/solvers/flattening/boolbv.cpp | 2 +- src/solvers/lowering/expr_lowering.h | 7 --- src/solvers/lowering/popcount.cpp | 61 --------------------------- src/solvers/smt2/smt2_conv.cpp | 3 +- src/util/bitvector_expr.cpp | 47 +++++++++++++++++++++ src/util/bitvector_expr.h | 4 ++ 8 files changed, 55 insertions(+), 74 deletions(-) delete mode 100644 src/solvers/lowering/popcount.cpp diff --git a/scripts/expected_doxygen_warnings.txt b/scripts/expected_doxygen_warnings.txt index abea5a1e46c2..f0d6c3e73cbd 100644 --- a/scripts/expected_doxygen_warnings.txt +++ b/scripts/expected_doxygen_warnings.txt @@ -21,13 +21,13 @@ warning: Include graph for 'goto_instrument_parse_options.cpp' not generated, too many nodes (97), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'goto_functions.h' not generated, too many nodes (66), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'goto_model.h' not generated, too many nodes (110), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. -warning: Included by graph for 'arith_tools.h' not generated, too many nodes (182), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. +warning: Included by graph for 'arith_tools.h' not generated, too many nodes (181), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'c_types.h' not generated, too many nodes (110), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'config.h' not generated, too many nodes (87), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'exception_utils.h' not generated, too many nodes (61), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'expr.h' not generated, too many nodes (87), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'expr_util.h' not generated, too many nodes (61), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. -warning: Included by graph for 'invariant.h' not generated, too many nodes (187), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. +warning: Included by graph for 'invariant.h' not generated, too many nodes (186), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'irep.h' not generated, too many nodes (62), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'message.h' not generated, too many nodes (117), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'namespace.h' not generated, too many nodes (109), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. diff --git a/src/solvers/Makefile b/src/solvers/Makefile index 1b70e5960b77..c8569eb084f9 100644 --- a/src/solvers/Makefile +++ b/src/solvers/Makefile @@ -141,7 +141,6 @@ SRC = $(BOOLEFORCE_SRC) \ floatbv/float_approximation.cpp \ lowering/byte_operators.cpp \ lowering/functions.cpp \ - lowering/popcount.cpp \ bdd/miniBDD/miniBDD.cpp \ prop/bdd_expr.cpp \ prop/cover_goals.cpp \ diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp index 589444ac17b5..5529ec544684 100644 --- a/src/solvers/flattening/boolbv.cpp +++ b/src/solvers/flattening/boolbv.cpp @@ -227,7 +227,7 @@ bvt boolbvt::convert_bitvector(const exprt &expr) else if(expr.id()==ID_power) return convert_power(to_binary_expr(expr)); else if(expr.id() == ID_popcount) - return convert_bv(lower_popcount(to_popcount_expr(expr), ns)); + return convert_bv(to_popcount_expr(expr).lower()); return conversion_failed(expr); } diff --git a/src/solvers/lowering/expr_lowering.h b/src/solvers/lowering/expr_lowering.h index bcd82263916a..1ee186bedbf0 100644 --- a/src/solvers/lowering/expr_lowering.h +++ b/src/solvers/lowering/expr_lowering.h @@ -14,7 +14,6 @@ Author: Michael Tautschnig class byte_extract_exprt; class byte_update_exprt; class namespacet; -class popcount_exprt; /// Rewrite a byte extract expression to more fundamental operations. /// \param src: Byte extract expression @@ -44,10 +43,4 @@ exprt lower_byte_operators(const exprt &src, const namespacet &ns); bool has_byte_operator(const exprt &src); -/// 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 deleted file mode 100644 index 0cb340af3aee..000000000000 --- a/src/solvers/lowering/popcount.cpp +++ /dev/null @@ -1,61 +0,0 @@ -/*******************************************************************\ - -Module: Lowering of popcount - -Author: Michael Tautschnig - -\*******************************************************************/ - -#include "expr_lowering.h" - -#include -#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 auto x_width = pointer_offset_bits(x.type(), ns); - CHECK_RETURN(x_width.has_value() && *x_width >= 1); - const std::size_t bits = address_bits(*x_width); - const std::size_t new_width = numeric_cast_v(power(2, bits)); - - const bool need_typecast = - new_width > *x_width || x.type().id() != ID_unsignedbv; - - if(need_typecast) - x = typecast_exprt(x, 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'); - const mp_integer value = binary2integer(bitstring, false); - const constant_exprt bitmask(integer2bvrep(value, new_width), 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 - return typecast_exprt(x, expr.type()); -} diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index fbbf83dfdaf3..0ce62235126f 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -1984,8 +1984,7 @@ void smt2_convt::convert_expr(const exprt &expr) } else if(expr.id() == ID_popcount) { - exprt lowered = lower_popcount(to_popcount_expr(expr), ns); - convert_expr(lowered); + convert_expr(to_popcount_expr(expr).lower()); } else INVARIANT_WITH_DIAGNOSTICS( diff --git a/src/util/bitvector_expr.cpp b/src/util/bitvector_expr.cpp index 76d1e71eaf4c..1d9ab256d4d2 100644 --- a/src/util/bitvector_expr.cpp +++ b/src/util/bitvector_expr.cpp @@ -9,6 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "bitvector_expr.h" #include "arith_tools.h" +#include "bitvector_types.h" #include "mathematical_types.h" shift_exprt::shift_exprt( @@ -40,3 +41,49 @@ extractbits_exprt::extractbits_exprt( from_integer(_upper, integer_typet()), from_integer(_lower, integer_typet())); } + +exprt popcount_exprt::lower() const +{ + // 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 = op(); + const auto x_width = to_bitvector_type(x.type()).get_width(); + CHECK_RETURN(x_width >= 1); + const std::size_t bits = address_bits(x_width); + const std::size_t new_width = numeric_cast_v(power(2, bits)); + + const bool need_typecast = + new_width > x_width || x.type().id() != ID_unsignedbv; + + if(need_typecast) + x = typecast_exprt(x, 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'); + const mp_integer value = binary2integer(bitstring, false); + const constant_exprt bitmask(integer2bvrep(value, new_width), 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 + return typecast_exprt::conditional_cast(x, type()); +} diff --git a/src/util/bitvector_expr.h b/src/util/bitvector_expr.h index 243be4c92e0b..61510f3bf3e9 100644 --- a/src/util/bitvector_expr.h +++ b/src/util/bitvector_expr.h @@ -641,6 +641,10 @@ class popcount_exprt : public unary_exprt : unary_exprt(ID_popcount, _op, _op.type()) { } + + /// Lower a popcount_exprt to arithmetic and logic expressions. + /// \return Semantically equivalent expression + exprt lower() const; }; template <>