File tree 8 files changed +88
-15
lines changed
regression/ansi-c/gcc_builtins1
8 files changed +88
-15
lines changed Original file line number Diff line number Diff line change 1
1
#ifdef __GNUC__
2
2
3
- enum { E1 = __builtin_isinf (1.0 ) };
4
- enum { E2 = __builtin_isnan (1.0 ) };
5
- enum { E3 = __builtin_isinf (__builtin_inf ()) };
6
- enum { E4 = __builtin_signbit (-1.0 ) };
7
- enum { E5 = __builtin_classify_type (1 ) };
8
- enum { E6 = sizeof (int ) };
9
- enum { E7 = __alignof__(int ) };
10
- enum { E8 = (int )1.0 };
11
- enum { E9 = __builtin_popcount (123 ) };
3
+ enum { E01 = __builtin_isinf (1.0 ) };
4
+ enum { E02 = __builtin_isnan (1.0 ) };
5
+ enum { E03 = __builtin_isinf (__builtin_inf ()) };
6
+ enum { E04 = __builtin_signbit (-1.0 ) }; // clang doesn't do this one
7
+ enum { E05 = __builtin_classify_type (1 ) };
8
+ enum { E06 = sizeof (int ) };
9
+ enum { E07 = __alignof__(int ) };
10
+ enum { E08 = (int )1.0 };
11
+ enum { E09 = __builtin_popcount (123 ) };
12
+ enum { E10 = __builtin_bswap16 (0xaabb ) };
13
+ enum { E11 = __builtin_bswap32 (0xaabb ) };
14
+ enum { E12 = __builtin_bswap64 (0xaabb ) };
12
15
13
16
#endif
14
17
Original file line number Diff line number Diff line change @@ -2480,6 +2480,25 @@ exprt c_typecheck_baset::do_special_functions(
2480
2480
2481
2481
return pointer_object_expr;
2482
2482
}
2483
+ else if (identifier==" __builtin_bswap16" ||
2484
+ identifier==" __builtin_bswap32" ||
2485
+ identifier==" __builtin_bswap64" )
2486
+ {
2487
+ typecheck_function_call_arguments (expr);
2488
+
2489
+ if (expr.arguments ().size ()!=1 )
2490
+ {
2491
+ err_location (f_op);
2492
+ error () << identifier << " expects one operand" << eom;
2493
+ throw 0 ;
2494
+ }
2495
+
2496
+ exprt bswap_expr (ID_bswap, expr.type ());
2497
+ bswap_expr.operands ()=expr.arguments ();
2498
+ bswap_expr.add_source_location ()=source_location;
2499
+
2500
+ return bswap_expr;
2501
+ }
2483
2502
else if (identifier==CPROVER_PREFIX " isnanf" ||
2484
2503
identifier==CPROVER_PREFIX " isnand" ||
2485
2504
identifier==CPROVER_PREFIX " isnanld" ||
Original file line number Diff line number Diff line change @@ -4401,6 +4401,9 @@ std::string expr2ct::convert(
4401
4401
else if (src.id ()==ID_isinf)
4402
4402
return convert_function (src, " isinf" , precedence=16 );
4403
4403
4404
+ else if (src.id ()==ID_bswap)
4405
+ return convert_function (src, " bswap" , precedence=16 );
4406
+
4404
4407
else if (src.id ()==ID_isnormal)
4405
4408
return convert_function (src, " isnormal" , precedence=16 );
4406
4409
Original file line number Diff line number Diff line change @@ -154,17 +154,17 @@ int __builtin_parityl(unsigned long);
154
154
int __builtin_parityll (unsigned long long );
155
155
void __builtin_trap (void );
156
156
void __builtin___clear_cache (char * begin , char * end );
157
- int __builtin_clz (unsigned int x );
157
+ int __builtin_clz (unsigned int );
158
158
int __builtin_clzll (unsigned long long );
159
- int __builtin_ctz (unsigned int x );
159
+ int __builtin_ctz (unsigned int );
160
160
int __builtin_ctzll (unsigned long long );
161
- int __builtin_parity (unsigned int x );
161
+ int __builtin_parity (unsigned int );
162
162
int __builtin_ffsl (unsigned long );
163
163
int __builtin_clzl (unsigned long );
164
164
int __builtin_ctzl (unsigned long );
165
- short int __builtin_bswap16 (short int x );
166
- long int __builtin_bswap32 (long int x );
167
- long long int __builtin_bswap64 (long long int x );
165
+ short unsigned int __builtin_bswap16 (short unsigned int );
166
+ long unsigned int __builtin_bswap32 (long unsigned int );
167
+ long long unsigned int __builtin_bswap64 (long long unsigned int );
168
168
int __builtin_classify_type ();
169
169
int __builtin_isinf (double );
170
170
int __builtin_isinff (float );
Original file line number Diff line number Diff line change @@ -732,3 +732,4 @@ verilog_unsigned_vector
732
732
verilog_array
733
733
low
734
734
high
735
+ bswap
Original file line number Diff line number Diff line change @@ -2549,6 +2549,8 @@ bool simplify_exprt::simplify_node(exprt &expr)
2549
2549
else if (expr.id ()==ID_ieee_float_equal ||
2550
2550
expr.id ()==ID_ieee_float_notequal)
2551
2551
result=simplify_ieee_float_relation (expr) && result;
2552
+ else if (expr.id ()==ID_bswap)
2553
+ result=simplify_bswap (expr) && result;
2552
2554
else if (expr.id ()==ID_isinf)
2553
2555
result=simplify_isinf (expr) && result;
2554
2556
else if (expr.id ()==ID_isnan)
Original file line number Diff line number Diff line change @@ -100,6 +100,7 @@ class simplify_exprt
100
100
bool simplify_dereference (exprt &expr);
101
101
bool simplify_address_of (exprt &expr);
102
102
bool simplify_pointer_offset (exprt &expr);
103
+ bool simplify_bswap (exprt &expr);
103
104
bool simplify_isinf (exprt &expr);
104
105
bool simplify_isnan (exprt &expr);
105
106
bool simplify_isnormal (exprt &expr);
Original file line number Diff line number Diff line change 23
23
24
24
/* ******************************************************************\
25
25
26
+ Function: simplify_exprt::simplify_bswap
27
+
28
+ Inputs:
29
+
30
+ Outputs:
31
+
32
+ Purpose:
33
+
34
+ \*******************************************************************/
35
+
36
+ bool simplify_exprt::simplify_bswap (exprt &expr)
37
+ {
38
+ if (expr.type ().id ()==ID_unsignedbv &&
39
+ expr.operands ().size ()==1 &&
40
+ expr.op0 ().type ()==expr.type () &&
41
+ expr.op0 ().is_constant ())
42
+ {
43
+ std::size_t width=to_bitvector_type (expr.type ()).get_width ();
44
+ mp_integer value;
45
+ to_integer (expr.op0 (), value);
46
+ std::vector<mp_integer> bytes;
47
+
48
+ // take apart
49
+ for (std::size_t bit=0 ; bit<width; bit+=8 )
50
+ bytes.push_back ((value>>bit)%256 );
51
+
52
+ // put back together, but backwards
53
+ mp_integer new_value=0 ;
54
+ for (std::size_t bit=0 ; bit<width; bit+=8 )
55
+ {
56
+ assert (!bytes.empty ());
57
+ new_value+=bytes.back ()<<bit;
58
+ bytes.pop_back ();
59
+ }
60
+
61
+ expr=from_integer (new_value, expr.type ());
62
+ return false ;
63
+ }
64
+
65
+ return true ;
66
+ }
67
+
68
+ /* ******************************************************************\
69
+
26
70
Function: simplify_exprt::simplify_mult
27
71
28
72
Inputs:
You can’t perform that action at this time.
0 commit comments