From e5640227a8f004a5def8a34a2eac9dcd76dd4da9 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 10 Jan 2021 16:21:07 +0000 Subject: [PATCH 1/2] Declare __lzcnt* as Windows built-in This avoids warnings about missing declarations. --- src/ansi-c/windows_builtin_headers.h | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/ansi-c/windows_builtin_headers.h b/src/ansi-c/windows_builtin_headers.h index ea80f16ce22..39031072782 100644 --- a/src/ansi-c/windows_builtin_headers.h +++ b/src/ansi-c/windows_builtin_headers.h @@ -1 +1,4 @@ int __assume(int); +unsigned short __lzcnt16(unsigned short value); +unsigned int __lzcnt(unsigned int value); +unsigned __int64 __lzcnt64(unsigned __int64 value); From fef9e893911947d29e77520a319225cae13bfed6 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 6 Jan 2021 12:08:55 +0000 Subject: [PATCH 2/2] C front-end: evaluate __builtin_clz over constants The Linux kernel uses __builtin_clz{,l,ll} in expressions that are expected to be compile-time constants. To support this, evaluate such expressions during type checking. --- .../cbmc-library/__builtin_clz-02/main.c | 12 +++++++ .../cbmc-library/__builtin_clz-02/test.desc | 11 ++++++ src/ansi-c/c_typecheck_expr.cpp | 34 +++++++++++++++++++ 3 files changed, 57 insertions(+) create mode 100644 regression/cbmc-library/__builtin_clz-02/main.c create mode 100644 regression/cbmc-library/__builtin_clz-02/test.desc diff --git a/regression/cbmc-library/__builtin_clz-02/main.c b/regression/cbmc-library/__builtin_clz-02/main.c new file mode 100644 index 00000000000..16416024d60 --- /dev/null +++ b/regression/cbmc-library/__builtin_clz-02/main.c @@ -0,0 +1,12 @@ +#ifdef _MSC_VER +# define __builtin_clz(x) __lzcnt(x) +# define _Static_assert static_assert +#endif + +int main() +{ + _Static_assert( + __builtin_clz(0xffU) == 8 * sizeof(unsigned) - 8, "compile-time constant"); + + return 0; +} diff --git a/regression/cbmc-library/__builtin_clz-02/test.desc b/regression/cbmc-library/__builtin_clz-02/test.desc new file mode 100644 index 00000000000..cd32194efb5 --- /dev/null +++ b/regression/cbmc-library/__builtin_clz-02/test.desc @@ -0,0 +1,11 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +For this example, __builtin_clz is fully evaluated in the front-end. The +_Static_assert ensures this is the case, as type checking fails when +_Static_assert does not have a compile-time constant value. diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 5afe177e6c0..a59a541f801 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -2591,6 +2591,40 @@ exprt c_typecheck_baset::do_special_functions( return std::move(popcount_expr); } + else if( + identifier == "__builtin_clz" || identifier == "__builtin_clzl" || + identifier == "__builtin_clzll" || identifier == "__lzcnt16" || + identifier == "__lzcnt" || identifier == "__lzcnt64") + { + if(expr.arguments().size() != 1) + { + error().source_location = f_op.source_location(); + error() << identifier << " expects one operand" << eom; + throw 0; + } + + side_effect_expr_function_callt try_constant{expr}; + typecheck_function_call_arguments(try_constant); + exprt argument = try_constant.arguments().front(); + simplify(argument, *this); + const auto int_constant = numeric_cast(argument); + + if( + !int_constant.has_value() || *int_constant == 0 || + argument.type().id() != ID_unsignedbv) + { + return nil_exprt{}; + } + + const std::string binary_value = integer2binary( + *int_constant, to_unsignedbv_type(argument.type()).get_width()); + std::size_t n_leading_zeros = binary_value.find('1'); + CHECK_RETURN(n_leading_zeros != std::string::npos); + + return from_integer( + n_leading_zeros, + to_code_type(try_constant.function().type()).return_type()); + } else if(identifier==CPROVER_PREFIX "equal") { if(expr.arguments().size()!=2)