-
Notifications
You must be signed in to change notification settings - Fork 269
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
New expression: count_leading_zeros_exprt
Rather than ad-hoc handling __builtin_clz and __lzcnt (and their variants) in the C front-end, make counting-leading-zeros available across the code base.
- Loading branch information
1 parent
631e7b0
commit 530b484
Showing
21 changed files
with
263 additions
and
141 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,10 @@ | ||
int main() | ||
{ | ||
#ifdef __GNUC__ | ||
_Static_assert( | ||
__builtin_clz(0xffU) == 8 * sizeof(unsigned) - 8, | ||
"GCC/Clang compile-time constant"); | ||
#endif | ||
|
||
return 0; | ||
} |
File renamed without changes.
This file was deleted.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,10 @@ | ||
CORE | ||
main.c | ||
|
||
^\[main.bit_count.\d+\] line 61 count leading zeros argument in __builtin_clz\(0u\): FAILURE$ | ||
^\*\* 1 of \d+ failed | ||
^VERIFICATION FAILED$ | ||
^EXIT=10$ | ||
^SIGNAL=0$ | ||
-- | ||
^warning: ignoring |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,55 @@ | ||
/*******************************************************************\ | ||
Module: Lowering of count_leading_zeros | ||
Author: Michael Tautschnig | ||
\*******************************************************************/ | ||
|
||
#include "expr_lowering.h" | ||
|
||
#include <util/arith_tools.h> | ||
#include <util/bitvector_expr.h> | ||
#include <util/invariant.h> | ||
#include <util/pointer_offset_size.h> | ||
#include <util/std_expr.h> | ||
|
||
exprt lower_clz(const count_leading_zeros_exprt &expr, const namespacet &ns) | ||
{ | ||
// x = x | (x >> 1); | ||
// x = x | (x >> 2); | ||
// x = x | (x >> 4); | ||
// x = x | (x >> 8); | ||
// etc. | ||
// return popcount(~x); | ||
|
||
// 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<std::size_t>(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 | (x >> shift) | ||
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))); | ||
// build the expression | ||
x = bitor_exprt{x, shifted_x}; | ||
} | ||
|
||
// the result is restricted to the result type | ||
return lower_popcount( | ||
popcount_exprt{ | ||
bitnot_exprt{typecast_exprt::conditional_cast(x, expr.op().type())}, | ||
expr.type()}, | ||
ns); | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.