diff --git a/regression/cbmc-library/__builtin_ffs-01/main.c b/regression/cbmc/__builtin_ffs-01/main.c similarity index 56% rename from regression/cbmc-library/__builtin_ffs-01/main.c rename to regression/cbmc/__builtin_ffs-01/main.c index 60588c9cdf68..392ea54a2d9e 100644 --- a/regression/cbmc-library/__builtin_ffs-01/main.c +++ b/regression/cbmc/__builtin_ffs-01/main.c @@ -7,9 +7,11 @@ int __builtin_ffsl(long); int __builtin_ffsll(long long); #endif +#ifdef _MSC_VER +# define _Static_assert(x, m) static_assert(x, m) +#endif + int __VERIFIER_nondet_int(); -long __VERIFIER_nondet_long(); -long long __VERIFIER_nondet_long_long(); // http://graphics.stanford.edu/~seander/bithacks.html#ZerosOnRightMultLookup static const int multiply_de_bruijn_bit_position[32] = { @@ -18,14 +20,14 @@ static const int multiply_de_bruijn_bit_position[32] = { int main() { - assert(__builtin_ffs(0) == 0); - assert(__builtin_ffs(-1) == 1); - assert(__builtin_ffs(INT_MIN) == sizeof(int) * 8); - assert(__builtin_ffsl(INT_MIN) == sizeof(int) * 8); - assert(__builtin_ffsl(LONG_MIN) == sizeof(long) * 8); - assert(__builtin_ffsll(INT_MIN) == sizeof(int) * 8); - assert(__builtin_ffsll(LLONG_MIN) == sizeof(long long) * 8); - assert(__builtin_ffs(INT_MAX) == 1); + _Static_assert(__builtin_ffs(0) == 0, ""); + _Static_assert(__builtin_ffs(-1) == 1, ""); + _Static_assert(__builtin_ffs(INT_MIN) == sizeof(int) * 8, ""); + _Static_assert(__builtin_ffsl(INT_MIN) == sizeof(int) * 8, ""); + _Static_assert(__builtin_ffsl(LONG_MIN) == sizeof(long) * 8, ""); + _Static_assert(__builtin_ffsll(INT_MIN) == sizeof(int) * 8, ""); + _Static_assert(__builtin_ffsll(LLONG_MIN) == sizeof(long long) * 8, ""); + _Static_assert(__builtin_ffs(INT_MAX) == 1, ""); int i = __VERIFIER_nondet_int(); __CPROVER_assume(i != 0); diff --git a/regression/cbmc-library/__builtin_ffs-01/test.desc b/regression/cbmc/__builtin_ffs-01/test.desc similarity index 100% rename from regression/cbmc-library/__builtin_ffs-01/test.desc rename to regression/cbmc/__builtin_ffs-01/test.desc diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 2e5cf424c5db..cf41f64e8243 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -2747,6 +2747,24 @@ exprt c_typecheck_baset::do_special_functions( return std::move(ctz); } + else if( + identifier == "__builtin_ffs" || identifier == "__builtin_ffsl" || + identifier == "__builtin_ffsll") + { + 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); + + find_first_set_exprt ffs{expr.arguments().front(), expr.type()}; + ffs.add_source_location() = source_location; + + return std::move(ffs); + } 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 1bc078a3fa68..97d604b3a13c 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -3823,6 +3823,7 @@ optionalt expr2ct::convert_function(const exprt &src) {ID_count_leading_zeros, "__builtin_clz"}, {ID_count_trailing_zeros, "__builtin_ctz"}, {ID_dynamic_object, "DYNAMIC_OBJECT"}, + {ID_find_first_set, "__builtin_ffs"}, {ID_floatbv_div, "FLOAT/"}, {ID_floatbv_minus, "FLOAT-"}, {ID_floatbv_mult, "FLOAT*"}, diff --git a/src/ansi-c/library/gcc.c b/src/ansi-c/library/gcc.c index e3c6fab0deb7..7ebe5eb294f8 100644 --- a/src/ansi-c/library/gcc.c +++ b/src/ansi-c/library/gcc.c @@ -33,57 +33,6 @@ inline void __sync_synchronize(void) #endif } -/* FUNCTION: __builtin_ffs */ - -int __builtin_clz(unsigned int x); - -inline int __builtin_ffs(int x) -{ - if(x == 0) - return 0; - -#pragma CPROVER check push -#pragma CPROVER check disable "conversion" - unsigned int u = (unsigned int)x; -#pragma CPROVER check pop - - return sizeof(int) * 8 - __builtin_clz(u & ~(u - 1)); -} - -/* FUNCTION: __builtin_ffsl */ - -int __builtin_clzl(unsigned long x); - -inline int __builtin_ffsl(long x) -{ - if(x == 0) - return 0; - -#pragma CPROVER check push -#pragma CPROVER check disable "conversion" - unsigned long u = (unsigned long)x; -#pragma CPROVER check pop - - return sizeof(long) * 8 - __builtin_clzl(u & ~(u - 1)); -} - -/* FUNCTION: __builtin_ffsll */ - -int __builtin_clzll(unsigned long long x); - -inline int __builtin_ffsll(long long x) -{ - if(x == 0) - return 0; - -#pragma CPROVER check push -#pragma CPROVER check disable "conversion" - unsigned long long u = (unsigned long long)x; -#pragma CPROVER check pop - - return sizeof(long long) * 8 - __builtin_clzll(u & ~(u - 1)); -} - /* FUNCTION: __atomic_test_and_set */ void __atomic_thread_fence(int memorder); diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp index 774218167dc2..11308334583c 100644 --- a/src/solvers/flattening/boolbv.cpp +++ b/src/solvers/flattening/boolbv.cpp @@ -216,6 +216,8 @@ bvt boolbvt::convert_bitvector(const exprt &expr) return convert_bv( simplify_expr(to_count_trailing_zeros_expr(expr).lower(), ns)); } + else if(expr.id() == ID_find_first_set) + return convert_bv(simplify_expr(to_find_first_set_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 f4e19cb6666d..0145ec87e89d 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -2042,6 +2042,10 @@ void smt2_convt::convert_expr(const exprt &expr) { convert_expr(simplify_expr(to_count_trailing_zeros_expr(expr).lower(), ns)); } + else if(expr.id() == ID_find_first_set) + { + convert_expr(simplify_expr(to_find_first_set_expr(expr).lower(), ns)); + } else INVARIANT_WITH_DIAGNOSTICS( false, diff --git a/src/util/bitvector_expr.cpp b/src/util/bitvector_expr.cpp index 314c314a55ca..1c8f9efbe930 100644 --- a/src/util/bitvector_expr.cpp +++ b/src/util/bitvector_expr.cpp @@ -142,3 +142,20 @@ exprt count_trailing_zeros_exprt::lower() const return typecast_exprt::conditional_cast(result, type()); } + +exprt find_first_set_exprt::lower() const +{ + exprt x = op(); + const auto int_width = to_bitvector_type(x.type()).get_width(); + CHECK_RETURN(int_width >= 1); + + // bitwidth(x) - clz(x & ~((unsigned)x - 1)); + const unsignedbv_typet ut{int_width}; + minus_exprt minus_one{typecast_exprt::conditional_cast(x, ut), + from_integer(1, ut)}; + count_leading_zeros_exprt clz{bitand_exprt{ + x, bitnot_exprt{typecast_exprt::conditional_cast(minus_one, x.type())}}}; + minus_exprt result{from_integer(int_width, x.type()), clz.lower()}; + + return typecast_exprt::conditional_cast(result, type()); +} diff --git a/src/util/bitvector_expr.h b/src/util/bitvector_expr.h index 94f7f9b3af7f..53d235c76459 100644 --- a/src/util/bitvector_expr.h +++ b/src/util/bitvector_expr.h @@ -1008,4 +1008,81 @@ inline count_trailing_zeros_exprt &to_count_trailing_zeros_expr(exprt &expr) return ret; } +/// \brief Returns one plus the index of the least-significant one bit, or zero +/// if the operand is zero. +class find_first_set_exprt : public unary_exprt +{ +public: + find_first_set_exprt(exprt _op, typet _type) + : unary_exprt(ID_find_first_set, std::move(_op), std::move(_type)) + { + } + + explicit find_first_set_exprt(const exprt &_op) + : find_first_set_exprt(_op, _op.type()) + { + } + + 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 find_first_set_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_find_first_set; +} + +inline void validate_expr(const find_first_set_exprt &value) +{ + validate_operands(value, 1, "find_first_set must have one operand"); +} + +/// \brief Cast an exprt to a \ref find_first_set_exprt +/// +/// \a expr must be known to be \ref find_first_set_exprt. +/// +/// \param expr: Source expression +/// \return Object of type \ref find_first_set_exprt +inline const find_first_set_exprt &to_find_first_set_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_find_first_set); + const find_first_set_exprt &ret = + static_cast(expr); + validate_expr(ret); + return ret; +} + +/// \copydoc to_find_first_set_expr(const exprt &) +inline find_first_set_exprt &to_find_first_set_expr(exprt &expr) +{ + PRECONDITION(expr.id() == ID_find_first_set); + find_first_set_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 a7d34b610770..7d4887aafb97 100644 --- a/src/util/format_expr.cpp +++ b/src/util/format_expr.cpp @@ -146,6 +146,8 @@ static std::ostream &format_rec(std::ostream &os, const unary_exprt &src) os << "clz"; else if(src.id() == ID_count_trailing_zeros) os << "ctz"; + else if(src.id() == ID_find_first_set) + os << "ffs"; else return os << src.pretty(); diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index b6c569c1f5cd..f76b0255e776 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -854,6 +854,7 @@ IREP_ID_TWO(vector_gt, vector->) IREP_ID_TWO(vector_lt, vector-<) IREP_ID_ONE(shuffle_vector) IREP_ID_ONE(count_trailing_zeros) +IREP_ID_ONE(find_first_set) // 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 8a0756ce0777..f548450bcf70 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -197,6 +197,27 @@ simplify_exprt::simplify_ctz(const count_trailing_zeros_exprt &expr) return from_integer(n_trailing_zeros, expr.type()); } +simplify_exprt::resultt<> +simplify_exprt::simplify_ffs(const find_first_set_exprt &expr) +{ + const auto const_bits_opt = expr2bits( + expr.op(), + config.ansi_c.endianness == configt::ansi_ct::endiannesst::IS_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 first_one_bit = const_bits_opt->find('1'); + if(first_one_bit == std::string::npos) + first_one_bit = 0; + else + ++first_one_bit; + + return from_integer(first_one_bit, expr.type()); +} + /// Simplify String.endsWith function when arguments are constant /// \param expr: the expression to simplify /// \param ns: namespace @@ -2457,6 +2478,10 @@ simplify_exprt::resultt<> simplify_exprt::simplify_node(exprt node) { r = simplify_ctz(to_count_trailing_zeros_expr(expr)); } + else if(expr.id() == ID_find_first_set) + { + r = simplify_ffs(to_find_first_set_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 455113dd1637..86552ea5eb50 100644 --- a/src/util/simplify_expr_class.h +++ b/src/util/simplify_expr_class.h @@ -44,6 +44,7 @@ class div_exprt; class exprt; class extractbit_exprt; class extractbits_exprt; +class find_first_set_exprt; class floatbv_typecast_exprt; class function_application_exprt; class ieee_float_op_exprt; @@ -210,6 +211,9 @@ class simplify_exprt /// Try to simplify count-trailing-zeros to a constant expression. NODISCARD resultt<> simplify_ctz(const count_trailing_zeros_exprt &); + /// Try to simplify find-first-set to a constant expression. + NODISCARD resultt<> simplify_ffs(const find_first_set_exprt &); + // auxiliary bool simplify_if_implies( exprt &expr, const exprt &cond, bool truth, bool &new_truth);