Skip to content

Commit 61d9fb4

Browse files
tautschnigtautschnig
committed
bitreverse_exprt: Expression to reverse the order of bits
Clang has a __builtin_bitreverse (and at some point GCC might as well: https://gcc.gnu.org/bugzilla/show_bug.cgi?id=50481).
1 parent 8b1b869 commit 61d9fb4

15 files changed

+233
-4
lines changed

‎regression/cbmc/clang_builtins/bitreverse.c

Lines changed: 64 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,64 @@
1+
#include <assert.h>
2+
#include <stdint.h>
3+
4+
#define test_bit_reverse(W) \
5+
uint##W##_t test_bit_reverse##W(uint##W##_t v) \
6+
{ \
7+
uint##W##_t result = 0; \
8+
int i; \
9+
for(i = 0; i < W; i++) \
10+
{ \
11+
if(v & (1ULL << i)) \
12+
result |= 1ULL << (W - i - 1); \
13+
} \
14+
return result; \
15+
} \
16+
int dummy_for_semicolon##W
17+
18+
test_bit_reverse(8);
19+
test_bit_reverse(16);
20+
test_bit_reverse(32);
21+
test_bit_reverse(64);
22+
23+
#ifndef __clang__
24+
unsigned char __builtin_bitreverse8(unsigned char);
25+
unsigned short __builtin_bitreverse16(unsigned short);
26+
unsigned int __builtin_bitreverse32(unsigned int);
27+
unsigned long long __builtin_bitreverse64(unsigned long long);
28+
#endif
29+
30+
void check_8(void)
31+
{
32+
uint8_t op;
33+
assert(__builtin_bitreverse8(op) == test_bit_reverse8(op));
34+
assert(__builtin_bitreverse8(1) == 0x80);
35+
}
36+
37+
void check_16(void)
38+
{
39+
uint16_t op;
40+
assert(__builtin_bitreverse16(op) == test_bit_reverse16(op));
41+
assert(__builtin_bitreverse16(1) == 0x8000);
42+
}
43+
44+
void check_32(void)
45+
{
46+
uint32_t op;
47+
assert(__builtin_bitreverse32(op) == test_bit_reverse32(op));
48+
assert(__builtin_bitreverse32(1) == 0x80000000);
49+
}
50+
51+
void check_64(void)
52+
{
53+
uint64_t op;
54+
assert(__builtin_bitreverse64(op) == test_bit_reverse64(op));
55+
assert(__builtin_bitreverse64(1) == 0x8000000000000000ULL);
56+
}
57+
58+
int main(void)
59+
{
60+
check_8();
61+
check_16();
62+
check_32();
63+
check_64();
64+
}

‎regression/cbmc/clang_builtins/bitreverse.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
bitreverse.c
3+
4+
^VERIFICATION SUCCESSFUL$
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--
8+
^warning: ignoring

‎src/ansi-c/c_typecheck_expr.cpp

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3238,6 +3238,27 @@ exprt c_typecheck_baset::do_special_functions(
32383238
std::move(result),
32393239
expr.source_location()};
32403240
}
3241+
else if(
3242+
identifier == "__builtin_bitreverse8" ||
3243+
identifier == "__builtin_bitreverse16" ||
3244+
identifier == "__builtin_bitreverse32" ||
3245+
identifier == "__builtin_bitreverse64")
3246+
{
3247+
// clang only
3248+
if(expr.arguments().size() != 1)
3249+
{
3250+
error().source_location = f_op.source_location();
3251+
error() << identifier << " expects one operand" << eom;
3252+
throw 0;
3253+
}
3254+
3255+
typecheck_function_call_arguments(expr);
3256+
3257+
bitreverse_exprt bitreverse{expr.arguments()[0]};
3258+
bitreverse.add_source_location() = source_location;
3259+
3260+
return std::move(bitreverse);
3261+
}
32413262
else
32423263
return nil_exprt();
32433264
}

‎src/ansi-c/clang_builtin_headers.h

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -54,6 +54,11 @@ void __builtin_nontemporal_load();
5454

5555
int __builtin_flt_rounds(void);
5656

57+
unsigned char __builtin_bitreverse8(unsigned char);
58+
unsigned short __builtin_bitreverse16(unsigned short);
59+
unsigned int __builtin_bitreverse32(unsigned int);
60+
unsigned long long __builtin_bitreverse64(unsigned long long);
61+
5762
unsigned char __builtin_rotateleft8(unsigned char, unsigned char);
5863
unsigned short __builtin_rotateleft16(unsigned short, unsigned short);
5964
unsigned int __builtin_rotateleft32(unsigned int, unsigned int);

‎src/ansi-c/expr2c.cpp

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3496,6 +3496,22 @@ std::string expr2ct::convert_conditional_target_group(const exprt &src)
34963496
return dest;
34973497
}
34983498

3499+
std::string expr2ct::convert_bitreverse(const bitreverse_exprt &src)
3500+
{
3501+
if(auto type_ptr = type_try_dynamic_cast<unsignedbv_typet>(src.type()))
3502+
{
3503+
const std::size_t width = type_ptr->get_width();
3504+
if(width == 8 || width == 16 || width == 32 || width == 64)
3505+
{
3506+
return convert_function(
3507+
src, "__builtin_bitreverse" + std::to_string(width));
3508+
}
3509+
}
3510+
3511+
unsigned precedence;
3512+
return convert_norep(src, precedence);
3513+
}
3514+
34993515
std::string expr2ct::convert_with_precedence(
35003516
const exprt &src,
35013517
unsigned &precedence)
@@ -3904,6 +3920,9 @@ std::string expr2ct::convert_with_precedence(
39043920
return convert_conditional_target_group(src);
39053921
}
39063922

3923+
else if(src.id() == ID_bitreverse)
3924+
return convert_bitreverse(to_bitreverse_expr(src));
3925+
39073926
auto function_string_opt = convert_function(src);
39083927
if(function_string_opt.has_value())
39093928
return *function_string_opt;

‎src/ansi-c/expr2c_class.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -277,6 +277,7 @@ class expr2ct
277277
bool include_padding_components);
278278

279279
std::string convert_conditional_target_group(const exprt &src);
280+
std::string convert_bitreverse(const bitreverse_exprt &src);
280281
};
281282

282283
#endif // CPROVER_ANSI_C_EXPR2C_CLASS_H

‎src/solvers/flattening/boolbv.cpp

Lines changed: 7 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -155,11 +155,14 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
155155
return convert_replication(to_replication_expr(expr));
156156
else if(expr.id()==ID_extractbits)
157157
return convert_extractbits(to_extractbits_expr(expr));
158-
else if(expr.id()==ID_bitnot || expr.id()==ID_bitand ||
159-
expr.id()==ID_bitor || expr.id()==ID_bitxor ||
160-
expr.id()==ID_bitxnor || expr.id()==ID_bitnor ||
161-
expr.id()==ID_bitnand)
158+
else if(
159+
expr.id() == ID_bitnot || expr.id() == ID_bitand || expr.id() == ID_bitor ||
160+
expr.id() == ID_bitxor || expr.id() == ID_bitxnor ||
161+
expr.id() == ID_bitnor || expr.id() == ID_bitnand ||
162+
expr.id() == ID_bitreverse)
163+
{
162164
return convert_bitwise(expr);
165+
}
163166
else if(expr.id() == ID_unary_minus)
164167
return convert_unary_minus(to_unary_minus_expr(expr));
165168
else if(expr.id()==ID_unary_plus)

‎src/solvers/flattening/boolbv_bitwise.cpp

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -60,6 +60,15 @@ bvt boolbvt::convert_bitwise(const exprt &expr)
6060

6161
return bv;
6262
}
63+
else if(expr.id() == ID_bitreverse)
64+
{
65+
const exprt &op = to_bitreverse_expr(expr).op();
66+
bvt bv = convert_bv(op, width);
67+
68+
std::reverse(bv.begin(), bv.end());
69+
70+
return bv;
71+
}
6372

6473
UNIMPLEMENTED;
6574
}

‎src/solvers/smt2/smt2_conv.cpp

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2134,6 +2134,10 @@ void smt2_convt::convert_expr(const exprt &expr)
21342134
{
21352135
out << "()";
21362136
}
2137+
else if(expr.id() == ID_bitreverse)
2138+
{
2139+
convert_expr(simplify_expr(to_bitreverse_expr(expr).lower(), ns));
2140+
}
21372141
else
21382142
INVARIANT_WITH_DIAGNOSTICS(
21392143
false,

‎src/util/bitvector_expr.cpp

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -142,3 +142,17 @@ exprt count_trailing_zeros_exprt::lower() const
142142

143143
return typecast_exprt::conditional_cast(result, type());
144144
}
145+
146+
exprt bitreverse_exprt::lower() const
147+
{
148+
const std::size_t int_width = to_bitvector_type(type()).get_width();
149+
150+
exprt::operandst result_bits;
151+
result_bits.reserve(int_width);
152+
153+
const exprt operand = op();
154+
for(std::size_t i = 0; i < int_width; ++i)
155+
result_bits.push_back(extractbit_exprt{operand, i});
156+
157+
return concatenation_exprt{result_bits, type()};
158+
}

‎src/util/bitvector_expr.h

Lines changed: 48 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1008,4 +1008,52 @@ inline count_trailing_zeros_exprt &to_count_trailing_zeros_expr(exprt &expr)
10081008
return ret;
10091009
}
10101010

1011+
/// \brief Reverse the order of bits in a bit-vector.
1012+
class bitreverse_exprt : public unary_exprt
1013+
{
1014+
public:
1015+
explicit bitreverse_exprt(exprt op)
1016+
: unary_exprt(ID_bitreverse, std::move(op))
1017+
{
1018+
}
1019+
1020+
/// Lower a bitreverse_exprt to arithmetic and logic expressions.
1021+
/// \return Semantically equivalent expression
1022+
exprt lower() const;
1023+
};
1024+
1025+
template <>
1026+
inline bool can_cast_expr<bitreverse_exprt>(const exprt &base)
1027+
{
1028+
return base.id() == ID_bitreverse;
1029+
}
1030+
1031+
inline void validate_expr(const bitreverse_exprt &value)
1032+
{
1033+
validate_operands(value, 1, "Bit-wise reverse must have one operand");
1034+
}
1035+
1036+
/// \brief Cast an exprt to a \ref bitreverse_exprt
1037+
///
1038+
/// \a expr must be known to be \ref bitreverse_exprt.
1039+
///
1040+
/// \param expr: Source expression
1041+
/// \return Object of type \ref bitreverse_exprt
1042+
inline const bitreverse_exprt &to_bitreverse_expr(const exprt &expr)
1043+
{
1044+
PRECONDITION(expr.id() == ID_bitreverse);
1045+
const bitreverse_exprt &ret = static_cast<const bitreverse_exprt &>(expr);
1046+
validate_expr(ret);
1047+
return ret;
1048+
}
1049+
1050+
/// \copydoc to_bitreverse_expr(const exprt &)
1051+
inline bitreverse_exprt &to_bitreverse_expr(exprt &expr)
1052+
{
1053+
PRECONDITION(expr.id() == ID_bitreverse);
1054+
bitreverse_exprt &ret = static_cast<bitreverse_exprt &>(expr);
1055+
validate_expr(ret);
1056+
return ret;
1057+
}
1058+
10111059
#endif // CPROVER_UTIL_BITVECTOR_EXPR_H

‎src/util/irep_ids.def

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -864,6 +864,7 @@ IREP_ID_TWO(vector_lt, vector-<)
864864
IREP_ID_ONE(shuffle_vector)
865865
IREP_ID_ONE(count_trailing_zeros)
866866
IREP_ID_ONE(empty_union)
867+
IREP_ID_ONE(bitreverse)
867868

868869
// Projects depending on this code base that wish to extend the list of
869870
// available ids should provide a file local_irep_ids.def in their source tree

‎src/util/simplify_expr.cpp

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2542,6 +2542,10 @@ simplify_exprt::resultt<> simplify_exprt::simplify_node(exprt node)
25422542
{
25432543
r = simplify_overflow_unary(to_unary_overflow_expr(expr));
25442544
}
2545+
else if(expr.id() == ID_bitreverse)
2546+
{
2547+
r = simplify_bitreverse(to_bitreverse_expr(expr));
2548+
}
25452549

25462550
if(!no_change_join_operands)
25472551
r = changed(r);

‎src/util/simplify_expr_class.h

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -33,6 +33,7 @@ class binary_exprt;
3333
class binary_overflow_exprt;
3434
class binary_relation_exprt;
3535
class bitnot_exprt;
36+
class bitreverse_exprt;
3637
class bswap_exprt;
3738
class byte_extract_exprt;
3839
class byte_update_exprt;
@@ -210,6 +211,9 @@ class simplify_exprt
210211
/// Try to simplify count-trailing-zeros to a constant expression.
211212
NODISCARD resultt<> simplify_ctz(const count_trailing_zeros_exprt &);
212213

214+
/// Try to simplify bit-reversing to a constant expression.
215+
NODISCARD resultt<> simplify_bitreverse(const bitreverse_exprt &);
216+
213217
// auxiliary
214218
bool simplify_if_implies(
215219
exprt &expr, const exprt &cond, bool truth, bool &new_truth);

‎src/util/simplify_expr_int.cpp

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1822,3 +1822,27 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_rhs_is_constant(
18221822
#endif
18231823
return unchanged(expr);
18241824
}
1825+
1826+
simplify_exprt::resultt<>
1827+
simplify_exprt::simplify_bitreverse(const bitreverse_exprt &expr)
1828+
{
1829+
auto const_bits_opt = expr2bits(
1830+
expr.op(),
1831+
config.ansi_c.endianness == configt::ansi_ct::endiannesst::IS_LITTLE_ENDIAN,
1832+
ns);
1833+
1834+
if(!const_bits_opt.has_value())
1835+
return unchanged(expr);
1836+
1837+
std::reverse(const_bits_opt->begin(), const_bits_opt->end());
1838+
1839+
auto result = bits2expr(
1840+
*const_bits_opt,
1841+
expr.type(),
1842+
config.ansi_c.endianness == configt::ansi_ct::endiannesst::IS_LITTLE_ENDIAN,
1843+
ns);
1844+
if(!result.has_value())
1845+
return unchanged(expr);
1846+
1847+
return std::move(*result);
1848+
}

0 commit comments

Comments
 (0)