From e13e3608b20093ce42d408b3079ad12b492b5edc Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 2 Mar 2021 12:06:22 +0000 Subject: [PATCH] New expression: find_first_set_exprt Rather than ad-hoc handling __builtin_ffs (and its variants) in the C front-end, make find-first-set available across the code base. --- .../__builtin_ffs-01/main.c | 22 +++--- .../__builtin_ffs-01/test.desc | 0 src/ansi-c/c_typecheck_expr.cpp | 18 +++++ src/ansi-c/expr2c.cpp | 1 + src/ansi-c/library/gcc.c | 51 ------------ src/solvers/flattening/boolbv.cpp | 2 + src/solvers/smt2/smt2_conv.cpp | 4 + src/util/bitvector_expr.cpp | 17 ++++ src/util/bitvector_expr.h | 77 +++++++++++++++++++ src/util/format_expr.cpp | 2 + src/util/irep_ids.def | 1 + src/util/simplify_expr.cpp | 25 ++++++ src/util/simplify_expr_class.h | 4 + 13 files changed, 163 insertions(+), 61 deletions(-) rename regression/{cbmc-library => cbmc}/__builtin_ffs-01/main.c (56%) rename regression/{cbmc-library => cbmc}/__builtin_ffs-01/test.desc (100%) 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 60588c9cdf6..392ea54a2d9 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 7e560ec7c47..fd58ba57e59 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -3124,6 +3124,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 f9be9aa8f53..c8f665ec2de 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -3987,6 +3987,7 @@ optionalt expr2ct::convert_function(const exprt &src) {ID_dynamic_object, "DYNAMIC_OBJECT"}, {ID_live_object, "LIVE_OBJECT"}, {ID_writeable_object, "WRITEABLE_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 64f952a32d5..e8a0e7f1d33 100644 --- a/src/ansi-c/library/gcc.c +++ b/src/ansi-c/library/gcc.c @@ -45,57 +45,6 @@ void __sync_synchronize(void) #endif } -/* FUNCTION: __builtin_ffs */ - -int __builtin_clz(unsigned int x); - -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); - -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); - -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 63b986794bc..d1241364589 100644 --- a/src/solvers/flattening/boolbv.cpp +++ b/src/solvers/flattening/boolbv.cpp @@ -240,6 +240,8 @@ bvt boolbvt::convert_bitvector(const exprt &expr) { return convert_overflow_result(*overflow_with_result); } + 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 5de4d950268..e7c6d3b1ee3 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -2301,6 +2301,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 if(expr.id() == ID_empty_union) { out << "()"; diff --git a/src/util/bitvector_expr.cpp b/src/util/bitvector_expr.cpp index 66230ae9847..adeaec40305 100644 --- a/src/util/bitvector_expr.cpp +++ b/src/util/bitvector_expr.cpp @@ -209,3 +209,20 @@ exprt mult_overflow_exprt::lower() const typecast_exprt{typecast_exprt{exact_result, lhs().type()}, ssize_type}, exact_result}; } + +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 360501ef5f1..516634c52de 100644 --- a/src/util/bitvector_expr.h +++ b/src/util/bitvector_expr.h @@ -1427,4 +1427,81 @@ inline overflow_result_exprt &to_overflow_result_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 b7091fd488c..d1be319123a 100644 --- a/src/util/format_expr.cpp +++ b/src/util/format_expr.cpp @@ -150,6 +150,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 2704262ec24..2c94928a59e 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -868,6 +868,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) IREP_ID_ONE(empty_union) IREP_ID_ONE(bitreverse) IREP_ID_ONE(saturating_minus) diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 98c73ef41cb..d91cb73e809 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 @@ -2758,6 +2779,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 4cffa7bb2e2..021b6b16400 100644 --- a/src/util/simplify_expr_class.h +++ b/src/util/simplify_expr_class.h @@ -45,6 +45,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; @@ -224,6 +225,9 @@ class simplify_exprt /// Try to simplify bit-reversing to a constant expression. NODISCARD resultt<> simplify_bitreverse(const bitreverse_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);