diff --git a/regression/cbmc/__builtin_clz-01/test.desc b/regression/cbmc/__builtin_clz-01/test.desc index 7e7552cdc69..8da8468eb09 100644 --- a/regression/cbmc/__builtin_clz-01/test.desc +++ b/regression/cbmc/__builtin_clz-01/test.desc @@ -1,7 +1,7 @@ CORE main.c --bounds-check -^\[main.bit_count.\d+\] line 61 count leading zeros argument in __builtin_clz\(0u\): FAILURE$ +^\[main.bit_count.\d+\] line 61 count leading zeros is undefined for value zero in __builtin_clz\(0u\): FAILURE$ ^\*\* 1 of \d+ failed ^VERIFICATION FAILED$ ^EXIT=10$ diff --git a/regression/cbmc/__builtin_ctz-01/main.c b/regression/cbmc/__builtin_ctz-01/main.c new file mode 100644 index 00000000000..0eb5521f979 --- /dev/null +++ b/regression/cbmc/__builtin_ctz-01/main.c @@ -0,0 +1,49 @@ +#include +#include + +#ifndef __GNUC__ +int __builtin_ctz(unsigned int); +int __builtin_ctzl(unsigned long); +int __builtin_ctzll(unsigned long long); +#endif + +#ifdef _MSC_VER +# define _Static_assert(x, m) static_assert(x, m) +#endif + +unsigned __VERIFIER_nondet_unsigned(); + +// http://graphics.stanford.edu/~seander/bithacks.html#ZerosOnRightMultLookup +static const int multiply_de_bruijn_bit_position[32] = { + 0, 1, 28, 2, 29, 14, 24, 3, 30, 22, 20, 15, 25, 17, 4, 8, + 31, 27, 13, 23, 21, 19, 16, 7, 26, 12, 18, 6, 11, 5, 10, 9}; + +int main() +{ + _Static_assert(__builtin_ctz(1) == 0, ""); + _Static_assert(__builtin_ctz(UINT_MAX) == 0, ""); + _Static_assert( + __builtin_ctz(1U << (sizeof(unsigned) * 8 - 1)) == sizeof(unsigned) * 8 - 1, + ""); + _Static_assert( + __builtin_ctzl(1UL << (sizeof(unsigned) * 8 - 1)) == + sizeof(unsigned) * 8 - 1, + ""); + _Static_assert( + __builtin_ctzll(1ULL << (sizeof(unsigned) * 8 - 1)) == + sizeof(unsigned) * 8 - 1, + ""); + + unsigned u = __VERIFIER_nondet_unsigned(); + __CPROVER_assume(u != 0); + __CPROVER_assume(sizeof(u) == 4); + __CPROVER_assume(u > INT_MIN); + assert( + multiply_de_bruijn_bit_position + [((unsigned)((u & -u) * 0x077CB531U)) >> 27] == __builtin_ctz(u)); + + // a failing assertion should be generated as __builtin_ctz is undefined for 0 + __builtin_ctz(0U); + + return 0; +} diff --git a/regression/cbmc/__builtin_ctz-01/test.desc b/regression/cbmc/__builtin_ctz-01/test.desc new file mode 100644 index 00000000000..e8bed1dae70 --- /dev/null +++ b/regression/cbmc/__builtin_ctz-01/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--bounds-check +^\[main.bit_count.\d+\] line 46 count trailing zeros is undefined for value zero in __builtin_ctz\(0u\): FAILURE$ +^\*\* 1 of \d+ failed +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index f9a84059803..42d302cf5ab 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -174,7 +174,7 @@ class goto_checkt void bounds_check(const exprt &, const guardt &); void bounds_check_index(const index_exprt &, const guardt &); - void bounds_check_clz(const count_leading_zeros_exprt &, const guardt &); + void bounds_check_bit_count(const unary_exprt &, const guardt &); void div_by_zero_check(const div_exprt &, const guardt &); void mod_by_zero_check(const mod_exprt &, const guardt &); void mod_overflow_check(const mod_exprt &, const guardt &); @@ -1336,8 +1336,11 @@ void goto_checkt::bounds_check(const exprt &expr, const guardt &guard) if(expr.id() == ID_index) bounds_check_index(to_index_expr(expr), guard); - else if(expr.id() == ID_count_leading_zeros) - bounds_check_clz(to_count_leading_zeros_expr(expr), guard); + else if( + expr.id() == ID_count_leading_zeros || expr.id() == ID_count_trailing_zeros) + { + bounds_check_bit_count(to_unary_expr(expr), guard); + } } void goto_checkt::bounds_check_index( @@ -1519,13 +1522,22 @@ void goto_checkt::bounds_check_index( } } -void goto_checkt::bounds_check_clz( - const count_leading_zeros_exprt &expr, +void goto_checkt::bounds_check_bit_count( + const unary_exprt &expr, const guardt &guard) { + std::string name; + + if(expr.id() == ID_count_leading_zeros) + name = "leading"; + else if(expr.id() == ID_count_trailing_zeros) + name = "trailing"; + else + PRECONDITION(false); + add_guarded_property( notequal_exprt{expr.op(), from_integer(0, expr.op().type())}, - "count leading zeros argument", + "count " + name + " zeros is undefined for value zero", "bit count", expr.find_source_location(), expr, @@ -1788,7 +1800,8 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard) { pointer_primitive_check(expr, guard); } - else if(expr.id() == ID_count_leading_zeros) + else if( + expr.id() == ID_count_leading_zeros || expr.id() == ID_count_trailing_zeros) { bounds_check(expr, guard); } diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 267e336e148..c1ac5fddf57 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -2727,6 +2727,25 @@ exprt c_typecheck_baset::do_special_functions( return std::move(clz); } + else if( + identifier == "__builtin_ctz" || identifier == "__builtin_ctzl" || + identifier == "__builtin_ctzll") + { + if(expr.arguments().size() != 1) + { + error().source_location = f_op.source_location(); + error() << identifier << " expects one operand" << eom; + throw 0; + } + + typecheck_function_call_arguments(expr); + + count_trailing_zeros_exprt ctz{ + expr.arguments().front(), false, expr.type()}; + ctz.add_source_location() = source_location; + + return std::move(ctz); + } else if(identifier==CPROVER_PREFIX "equal") { if(expr.arguments().size()!=2) diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index a9c81526212..c42e9c028b2 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -3822,6 +3822,7 @@ optionalt expr2ct::convert_function(const exprt &src) {ID_complex_real, "__real__"}, {ID_concatenation, "CONCATENATION"}, {ID_count_leading_zeros, "__builtin_clz"}, + {ID_count_trailing_zeros, "__builtin_ctz"}, {ID_dynamic_object, "DYNAMIC_OBJECT"}, {ID_floatbv_div, "FLOAT/"}, {ID_floatbv_minus, "FLOAT-"}, diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp index 9348150fd09..5d3f5bfafac 100644 --- a/src/solvers/flattening/boolbv.cpp +++ b/src/solvers/flattening/boolbv.cpp @@ -218,6 +218,11 @@ bvt boolbvt::convert_bitvector(const exprt &expr) return convert_bv( simplify_expr(to_count_leading_zeros_expr(expr).lower(), ns)); } + else if(expr.id() == ID_count_trailing_zeros) + { + return convert_bv( + simplify_expr(to_count_trailing_zeros_expr(expr).lower(), ns)); + } return conversion_failed(expr); } diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 0f82affd811..57f52fd4d35 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -2035,6 +2035,10 @@ void smt2_convt::convert_expr(const exprt &expr) { convert_expr(simplify_expr(to_count_leading_zeros_expr(expr).lower(), ns)); } + else if(expr.id() == ID_count_trailing_zeros) + { + convert_expr(simplify_expr(to_count_trailing_zeros_expr(expr).lower(), ns)); + } else INVARIANT_WITH_DIAGNOSTICS( false, diff --git a/src/util/bitvector_expr.cpp b/src/util/bitvector_expr.cpp index 6fa6742db90..314c314a55c 100644 --- a/src/util/bitvector_expr.cpp +++ b/src/util/bitvector_expr.cpp @@ -125,3 +125,20 @@ exprt count_leading_zeros_exprt::lower() const bitnot_exprt{typecast_exprt::conditional_cast(x, op().type())}, type()} .lower(); } + +exprt count_trailing_zeros_exprt::lower() const +{ + exprt x = op(); + const auto int_width = to_bitvector_type(x.type()).get_width(); + CHECK_RETURN(int_width >= 1); + + // popcount(x ^ ((unsigned)x - 1)) - 1 + const unsignedbv_typet ut{int_width}; + minus_exprt minus_one{typecast_exprt::conditional_cast(x, ut), + from_integer(1, ut)}; + popcount_exprt popcount{ + bitxor_exprt{x, typecast_exprt::conditional_cast(minus_one, x.type())}}; + minus_exprt result{popcount.lower(), from_integer(1, x.type())}; + + return typecast_exprt::conditional_cast(result, type()); +} diff --git a/src/util/bitvector_expr.h b/src/util/bitvector_expr.h index 694dded3873..94f7f9b3af7 100644 --- a/src/util/bitvector_expr.h +++ b/src/util/bitvector_expr.h @@ -825,7 +825,7 @@ inline unary_overflow_exprt &to_unary_overflow_expr(exprt &expr) /// \brief The count leading zeros (counting the number of zero bits starting /// from the most-significant bit) expression. When \c zero_permitted is set to /// false, goto_checkt must generate an assertion that the operand does not -/// evaluates to zero. The result is always defined, even for zero (where the +/// evaluate to zero. The result is always defined, even for zero (where the /// result is the bit width). class count_leading_zeros_exprt : public unary_exprt { @@ -915,4 +915,97 @@ inline count_leading_zeros_exprt &to_count_leading_zeros_expr(exprt &expr) return ret; } +/// \brief The count trailing zeros (counting the number of zero bits starting +/// from the least-significant bit) expression. When \c zero_permitted is set to +/// false, goto_checkt must generate an assertion that the operand does not +/// evaluate to zero. The result is always defined, even for zero (where the +/// result is the bit width). +class count_trailing_zeros_exprt : public unary_exprt +{ +public: + count_trailing_zeros_exprt(exprt _op, bool _zero_permitted, typet _type) + : unary_exprt(ID_count_trailing_zeros, std::move(_op), std::move(_type)) + { + zero_permitted(_zero_permitted); + } + + explicit count_trailing_zeros_exprt(const exprt &_op) + : count_trailing_zeros_exprt(_op, true, _op.type()) + { + } + + bool zero_permitted() const + { + return !get_bool(ID_C_bounds_check); + } + + void zero_permitted(bool value) + { + set(ID_C_bounds_check, !value); + } + + static void check( + const exprt &expr, + const validation_modet vm = validation_modet::INVARIANT) + { + DATA_CHECK( + vm, + expr.operands().size() == 1, + "unary expression must have a single operand"); + DATA_CHECK( + vm, + can_cast_type(to_unary_expr(expr).op().type()), + "operand must be of bitvector type"); + } + + static void validate( + const exprt &expr, + const namespacet &, + const validation_modet vm = validation_modet::INVARIANT) + { + check(expr, vm); + } + + /// Lower a count_trailing_zeros_exprt to arithmetic and logic expressions. + /// \return Semantically equivalent expression + exprt lower() const; +}; + +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_count_trailing_zeros; +} + +inline void validate_expr(const count_trailing_zeros_exprt &value) +{ + validate_operands(value, 1, "count_trailing_zeros must have one operand"); +} + +/// \brief Cast an exprt to a \ref count_trailing_zeros_exprt +/// +/// \a expr must be known to be \ref count_trailing_zeros_exprt. +/// +/// \param expr: Source expression +/// \return Object of type \ref count_trailing_zeros_exprt +inline const count_trailing_zeros_exprt & +to_count_trailing_zeros_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_count_trailing_zeros); + const count_trailing_zeros_exprt &ret = + static_cast(expr); + validate_expr(ret); + return ret; +} + +/// \copydoc to_count_trailing_zeros_expr(const exprt &) +inline count_trailing_zeros_exprt &to_count_trailing_zeros_expr(exprt &expr) +{ + PRECONDITION(expr.id() == ID_count_trailing_zeros); + count_trailing_zeros_exprt &ret = + static_cast(expr); + validate_expr(ret); + return ret; +} + #endif // CPROVER_UTIL_BITVECTOR_EXPR_H diff --git a/src/util/format_expr.cpp b/src/util/format_expr.cpp index d43cd8b4f78..e5fa3adb19c 100644 --- a/src/util/format_expr.cpp +++ b/src/util/format_expr.cpp @@ -153,6 +153,8 @@ static std::ostream &format_rec(std::ostream &os, const unary_exprt &src) os << '-'; else if(src.id() == ID_count_leading_zeros) os << "clz"; + else if(src.id() == ID_count_trailing_zeros) + os << "ctz"; else return os << src.pretty(); diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index bdf33eb3535..b6c569c1f5c 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -853,6 +853,7 @@ IREP_ID_TWO(vector_le, vector-<=) IREP_ID_TWO(vector_gt, vector->) IREP_ID_TWO(vector_lt, vector-<) IREP_ID_ONE(shuffle_vector) +IREP_ID_ONE(count_trailing_zeros) // Projects depending on this code base that wish to extend the list of // available ids should provide a file local_irep_ids.def in their source tree diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index a23dde76f80..5913256f8e9 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -172,6 +172,28 @@ simplify_exprt::simplify_clz(const count_leading_zeros_exprt &expr) return from_integer(n_leading_zeros, expr.type()); } +simplify_exprt::resultt<> +simplify_exprt::simplify_ctz(const count_trailing_zeros_exprt &expr) +{ + const auto const_bits_opt = expr2bits( + expr.op(), byte_extract_id() == ID_byte_extract_little_endian, ns); + + if(!const_bits_opt.has_value()) + return unchanged(expr); + + // expr2bits generates a bit string starting with the least-significant bit + std::size_t n_trailing_zeros = const_bits_opt->find('1'); + if(n_trailing_zeros == std::string::npos) + { + if(!expr.zero_permitted()) + return unchanged(expr); + + n_trailing_zeros = const_bits_opt->size(); + } + + return from_integer(n_trailing_zeros, expr.type()); +} + /// Simplify String.endsWith function when arguments are constant /// \param expr: the expression to simplify /// \param ns: namespace @@ -2421,6 +2443,10 @@ simplify_exprt::resultt<> simplify_exprt::simplify_node(exprt node) { r = simplify_clz(to_count_leading_zeros_expr(expr)); } + else if(expr.id() == ID_count_trailing_zeros) + { + r = simplify_ctz(to_count_trailing_zeros_expr(expr)); + } else if(expr.id() == ID_function_application) { r = simplify_function_application(to_function_application_expr(expr)); diff --git a/src/util/simplify_expr_class.h b/src/util/simplify_expr_class.h index 030318ee443..455113dd163 100644 --- a/src/util/simplify_expr_class.h +++ b/src/util/simplify_expr_class.h @@ -38,6 +38,7 @@ class byte_extract_exprt; class byte_update_exprt; class concatenation_exprt; class count_leading_zeros_exprt; +class count_trailing_zeros_exprt; class dereference_exprt; class div_exprt; class exprt; @@ -206,6 +207,9 @@ class simplify_exprt /// Try to simplify count-leading-zeros to a constant expression. NODISCARD resultt<> simplify_clz(const count_leading_zeros_exprt &); + /// Try to simplify count-trailing-zeros to a constant expression. + NODISCARD resultt<> simplify_ctz(const count_trailing_zeros_exprt &); + // auxiliary bool simplify_if_implies( exprt &expr, const exprt &cond, bool truth, bool &new_truth);