Skip to content

Commit 52e9737

Browse files
author
Daniel Kroening
committed
new gcc floating-point type identifiers, Fixes: #2151
Documentation on the new types: https://gcc.gnu.org/onlinedocs/gcc/Floating-Types.html The commit also moves other gcc-specific types to ansi-c/gcc_types.h
1 parent 41d7a45 commit 52e9737

18 files changed

+467
-147
lines changed

‎regression/ansi-c/float_constant1/main.c

+11
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,17 @@ STATIC_ASSERT(0X1.0P-95F == 2.524355e-29f);
1010
// nothing before the dot
1111
STATIC_ASSERT(0X.0p+1f == 0);
1212

13+
// 32-bit, 64-bit and 128-bit constants, GCC proper only,
14+
// clang doesn't have it
15+
#if defined(__GNUC__) && !defined(__clang__)
16+
STATIC_ASSERT(__builtin_types_compatible_p(_Float32, __typeof(1.0f32)));
17+
STATIC_ASSERT(__builtin_types_compatible_p(_Float64, __typeof(1.0f64)));
18+
STATIC_ASSERT(__builtin_types_compatible_p(_Float128, __typeof(1.0f128)));
19+
STATIC_ASSERT(__builtin_types_compatible_p(_Float32x, __typeof(1.0f32x)));
20+
STATIC_ASSERT(__builtin_types_compatible_p(_Float64x, __typeof(1.0f64x)));
21+
STATIC_ASSERT(__builtin_types_compatible_p(_Float128x, __typeof(1.0f128x)));
22+
#endif
23+
1324
#ifdef __GNUC__
1425
_Complex c;
1526
#endif

‎regression/ansi-c/gcc_types_compatible_p1/main.c

+4
Original file line numberDiff line numberDiff line change
@@ -97,6 +97,10 @@ STATIC_ASSERT(!__builtin_types_compatible_p(unsigned, signed));
9797

9898
#ifndef __clang__
9999
// clang doesn't have these
100+
STATIC_ASSERT(!__builtin_types_compatible_p(_Float32, float));
101+
STATIC_ASSERT(!__builtin_types_compatible_p(_Float64, double));
102+
STATIC_ASSERT(!__builtin_types_compatible_p(_Float32x, float));
103+
STATIC_ASSERT(!__builtin_types_compatible_p(_Float64x, double));
100104
STATIC_ASSERT(!__builtin_types_compatible_p(__float80, double));
101105
STATIC_ASSERT(!__builtin_types_compatible_p(__float128, long double));
102106
STATIC_ASSERT(!__builtin_types_compatible_p(__float128, double));

‎src/ansi-c/Makefile

+1
Original file line numberDiff line numberDiff line change
@@ -27,6 +27,7 @@ SRC = anonymous_member.cpp \
2727
cprover_library.cpp \
2828
designator.cpp \
2929
expr2c.cpp \
30+
gcc_types.cpp \
3031
literals/convert_character_literal.cpp \
3132
literals/convert_float_literal.cpp \
3233
literals/convert_integer_literal.cpp \

‎src/ansi-c/ansi_c_convert_type.cpp

+47-7
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,8 @@ Author: Daniel Kroening, [email protected]
2020
#include <util/arith_tools.h>
2121
#include <util/std_types.h>
2222

23+
#include "gcc_types.h"
24+
2325
void ansi_c_convert_typet::read(const typet &type)
2426
{
2527
clear();
@@ -80,8 +82,20 @@ void ansi_c_convert_typet::read_rec(const typet &type)
8082
int32_cnt++;
8183
else if(type.id()==ID_int64)
8284
int64_cnt++;
85+
else if(type.id()==ID_gcc_float16)
86+
gcc_float16_cnt++;
87+
else if(type.id()==ID_gcc_float32)
88+
gcc_float32_cnt++;
89+
else if(type.id()==ID_gcc_float32x)
90+
gcc_float32x_cnt++;
91+
else if(type.id()==ID_gcc_float64)
92+
gcc_float64_cnt++;
93+
else if(type.id()==ID_gcc_float64x)
94+
gcc_float64x_cnt++;
8395
else if(type.id()==ID_gcc_float128)
8496
gcc_float128_cnt++;
97+
else if(type.id()==ID_gcc_float128x)
98+
gcc_float128x_cnt++;
8599
else if(type.id()==ID_gcc_int128)
86100
gcc_int128_cnt++;
87101
else if(type.id()==ID_gcc_attribute_mode)
@@ -248,7 +262,11 @@ void ansi_c_convert_typet::write(typet &type)
248262
unsigned_cnt || int_cnt || c_bool_cnt || proper_bool_cnt ||
249263
short_cnt || char_cnt || complex_cnt || long_cnt ||
250264
int8_cnt || int16_cnt || int32_cnt || int64_cnt ||
251-
gcc_float128_cnt || gcc_int128_cnt || bv_cnt)
265+
gcc_float16_cnt ||
266+
gcc_float32_cnt || gcc_float32x_cnt ||
267+
gcc_float64_cnt || gcc_float64x_cnt ||
268+
gcc_float128_cnt || gcc_float128x_cnt ||
269+
gcc_int128_cnt || bv_cnt)
252270
{
253271
error().source_location=source_location;
254272
error() << "illegal type modifier for defined type" << eom;
@@ -305,27 +323,49 @@ void ansi_c_convert_typet::write(typet &type)
305323
<< "found " << type.pretty() << eom;
306324
throw 0;
307325
}
308-
else if(gcc_float128_cnt)
326+
else if(gcc_float16_cnt ||
327+
gcc_float32_cnt || gcc_float32x_cnt ||
328+
gcc_float64_cnt || gcc_float64x_cnt ||
329+
gcc_float128_cnt || gcc_float128x_cnt)
309330
{
310331
if(signed_cnt || unsigned_cnt || int_cnt || c_bool_cnt || proper_bool_cnt ||
311332
int8_cnt || int16_cnt || int32_cnt || int64_cnt ||
312333
gcc_int128_cnt || bv_cnt ||
313334
short_cnt || char_cnt)
314335
{
315336
error().source_location=source_location;
316-
error() << "cannot combine integer type with float" << eom;
337+
error() << "cannot combine integer type with floating-point type" << eom;
317338
throw 0;
318339
}
319340

320-
if(long_cnt || double_cnt || float_cnt)
341+
if(long_cnt+double_cnt+
342+
float_cnt+gcc_float16_cnt+
343+
gcc_float32_cnt+gcc_float32x_cnt+
344+
gcc_float64_cnt+gcc_float64x_cnt+
345+
gcc_float128_cnt+gcc_float128x_cnt>=2)
321346
{
322347
error().source_location=source_location;
323348
error() << "conflicting type modifiers" << eom;
324349
throw 0;
325350
}
326351

327-
// _not_ the same as long double
328-
type=gcc_float128_type();
352+
// _not_ the same as float, double, long double
353+
if(gcc_float16_cnt)
354+
type=gcc_float16_type();
355+
else if(gcc_float32_cnt)
356+
type=gcc_float32_type();
357+
else if(gcc_float32x_cnt)
358+
type=gcc_float32x_type();
359+
else if(gcc_float64_cnt)
360+
type=gcc_float64_type();
361+
else if(gcc_float64x_cnt)
362+
type=gcc_float64x_type();
363+
else if(gcc_float128_cnt)
364+
type=gcc_float128_type();
365+
else if(gcc_float128x_cnt)
366+
type=gcc_float128x_type();
367+
else
368+
UNREACHABLE;
329369
}
330370
else if(double_cnt || float_cnt)
331371
{
@@ -335,7 +375,7 @@ void ansi_c_convert_typet::write(typet &type)
335375
short_cnt || char_cnt)
336376
{
337377
error().source_location=source_location;
338-
error() << "cannot combine integer type with float" << eom;
378+
error() << "cannot combine integer type with floating-point type" << eom;
339379
throw 0;
340380
}
341381

‎src/ansi-c/ansi_c_convert_type.h

+11-2
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,12 @@ class ansi_c_convert_typet:public messaget
2828
// extensions
2929
unsigned int8_cnt, int16_cnt, int32_cnt, int64_cnt,
3030
ptr32_cnt, ptr64_cnt,
31-
gcc_float128_cnt, gcc_int128_cnt, bv_cnt,
31+
gcc_float16_cnt,
32+
gcc_float32_cnt, gcc_float32x_cnt,
33+
gcc_float64_cnt, gcc_float64x_cnt,
34+
gcc_float128_cnt, gcc_float128x_cnt,
35+
gcc_int128_cnt,
36+
bv_cnt,
3237
floatbv_cnt, fixedbv_cnt;
3338

3439
typet gcc_attribute_mode;
@@ -63,7 +68,11 @@ class ansi_c_convert_typet:public messaget
6368
long_cnt=double_cnt=float_cnt=c_bool_cnt=proper_bool_cnt=complex_cnt=
6469
int8_cnt=int16_cnt=int32_cnt=int64_cnt=
6570
ptr32_cnt=ptr64_cnt=
66-
gcc_float128_cnt=gcc_int128_cnt=bv_cnt=floatbv_cnt=fixedbv_cnt=0;
71+
gcc_float16_cnt=
72+
gcc_float32_cnt=gcc_float32x_cnt=
73+
gcc_float64_cnt=gcc_float64x_cnt=
74+
gcc_float128_cnt=gcc_float128x_cnt=
75+
gcc_int128_cnt=bv_cnt=floatbv_cnt=fixedbv_cnt=0;
6776
vector_size.make_nil();
6877
alignment.make_nil();
6978
bv_width.make_nil();

‎src/ansi-c/c_typecheck_type.cpp

+1
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,7 @@ Author: Daniel Kroening, [email protected]
2121

2222
#include "ansi_c_convert_type.h"
2323
#include "c_qualifiers.h"
24+
#include "gcc_types.h"
2425
#include "padding.h"
2526
#include "type2name.h"
2627

‎src/ansi-c/gcc_types.cpp

+169
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,169 @@
1+
/*******************************************************************\
2+
3+
Module:
4+
5+
Author: Daniel Kroening, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#include "gcc_types.h"
10+
11+
#include <util/config.h>
12+
#include <util/c_types.h>
13+
14+
bitvector_typet gcc_float16_type()
15+
{
16+
if(config.ansi_c.use_fixed_for_float)
17+
{
18+
fixedbv_typet result;
19+
result.set_width(16);
20+
result.set_integer_bits(16/2);
21+
result.set(ID_C_c_type, ID_gcc_float16);
22+
return result;
23+
}
24+
else
25+
{
26+
floatbv_typet result=
27+
ieee_float_spect::half_precision().to_type();
28+
result.set(ID_C_c_type, ID_gcc_float16);
29+
return result;
30+
}
31+
}
32+
33+
bitvector_typet gcc_float32_type()
34+
{
35+
// not same as float!
36+
37+
if(config.ansi_c.use_fixed_for_float)
38+
{
39+
fixedbv_typet result;
40+
result.set_width(config.ansi_c.single_width);
41+
result.set_integer_bits(config.ansi_c.single_width/2);
42+
result.set(ID_C_c_type, ID_gcc_float32);
43+
return result;
44+
}
45+
else
46+
{
47+
floatbv_typet result=
48+
ieee_float_spect::single_precision().to_type();
49+
result.set(ID_C_c_type, ID_gcc_float32);
50+
return result;
51+
}
52+
}
53+
54+
bitvector_typet gcc_float32x_type()
55+
{
56+
// not same as float!
57+
58+
if(config.ansi_c.use_fixed_for_float)
59+
{
60+
fixedbv_typet result;
61+
result.set_width(config.ansi_c.single_width);
62+
result.set_integer_bits(config.ansi_c.single_width/2);
63+
result.set(ID_C_c_type, ID_gcc_float32x);
64+
return result;
65+
}
66+
else
67+
{
68+
floatbv_typet result=
69+
ieee_float_spect::single_precision().to_type();
70+
result.set(ID_C_c_type, ID_gcc_float32x);
71+
return result;
72+
}
73+
}
74+
75+
bitvector_typet gcc_float64_type()
76+
{
77+
// not same as double!
78+
if(config.ansi_c.use_fixed_for_float)
79+
{
80+
fixedbv_typet result;
81+
result.set_width(config.ansi_c.double_width);
82+
result.set_integer_bits(config.ansi_c.double_width/2);
83+
result.set(ID_C_c_type, ID_gcc_float64);
84+
return result;
85+
}
86+
else
87+
{
88+
floatbv_typet result=
89+
ieee_float_spect::double_precision().to_type();
90+
result.set(ID_C_c_type, ID_gcc_float64);
91+
return result;
92+
}
93+
}
94+
95+
bitvector_typet gcc_float64x_type()
96+
{
97+
// not same as double!
98+
if(config.ansi_c.use_fixed_for_float)
99+
{
100+
fixedbv_typet result;
101+
result.set_width(config.ansi_c.double_width);
102+
result.set_integer_bits(config.ansi_c.double_width/2);
103+
result.set(ID_C_c_type, ID_gcc_float64x);
104+
return result;
105+
}
106+
else
107+
{
108+
floatbv_typet result=
109+
ieee_float_spect::double_precision().to_type();
110+
result.set(ID_C_c_type, ID_gcc_float64x);
111+
return result;
112+
}
113+
}
114+
115+
bitvector_typet gcc_float128_type()
116+
{
117+
// not same as long double!
118+
119+
if(config.ansi_c.use_fixed_for_float)
120+
{
121+
fixedbv_typet result;
122+
result.set_width(128);
123+
result.set_integer_bits(128/2);
124+
result.set(ID_C_c_type, ID_gcc_float128);
125+
return result;
126+
}
127+
else
128+
{
129+
floatbv_typet result=
130+
ieee_float_spect::quadruple_precision().to_type();
131+
result.set(ID_C_c_type, ID_gcc_float128);
132+
return result;
133+
}
134+
}
135+
136+
bitvector_typet gcc_float128x_type()
137+
{
138+
// not same as long double!
139+
140+
if(config.ansi_c.use_fixed_for_float)
141+
{
142+
fixedbv_typet result;
143+
result.set_width(128);
144+
result.set_integer_bits(128/2);
145+
result.set(ID_C_c_type, ID_gcc_float128x);
146+
return result;
147+
}
148+
else
149+
{
150+
floatbv_typet result=
151+
ieee_float_spect::quadruple_precision().to_type();
152+
result.set(ID_C_c_type, ID_gcc_float128x);
153+
return result;
154+
}
155+
}
156+
157+
unsignedbv_typet gcc_unsigned_int128_type()
158+
{
159+
unsignedbv_typet result(128);
160+
result.set(ID_C_c_type, ID_unsigned_int128);
161+
return result;
162+
}
163+
164+
signedbv_typet gcc_signed_int128_type()
165+
{
166+
signedbv_typet result(128);
167+
result.set(ID_C_c_type, ID_signed_int128);
168+
return result;
169+
}

‎src/ansi-c/gcc_types.h

+27
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
/*******************************************************************\
2+
3+
Module:
4+
5+
Author: Daniel Kroening, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#ifndef CPROVER_ANSI_C_GCC_TYPES_H
10+
#define CPROVER_ANSI_C_GCC_TYPES_H
11+
12+
#include <util/std_types.h>
13+
14+
// These are gcc-specific; most are not implemented by clang
15+
// https://gcc.gnu.org/onlinedocs/gcc/Floating-Types.html
16+
17+
bitvector_typet gcc_float16_type();
18+
bitvector_typet gcc_float32_type();
19+
bitvector_typet gcc_float32x_type();
20+
bitvector_typet gcc_float64_type();
21+
bitvector_typet gcc_float64x_type();
22+
bitvector_typet gcc_float128_type();
23+
bitvector_typet gcc_float128x_type();
24+
unsignedbv_typet gcc_unsigned_int128_type();
25+
signedbv_typet gcc_signed_int128_type();
26+
27+
#endif // CPROVER_ANSI_C_GCC_TYPES_H

0 commit comments

Comments
 (0)