Skip to content

Commit 1a826a6

Browse files
michael-schwarzmichael-schwarz
authored
Merge pull request #60 from goblint/extended_float_types
Add support for additional float types
2 parents acb5cd3 + d393f04 commit 1a826a6

File tree

11 files changed

+152
-29
lines changed

11 files changed

+152
-29
lines changed

‎.gitignore‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -417,3 +417,4 @@ src/ext/canonicalize/.merlin
417417
src/ext/cqualann/.merlin
418418
src/ext/syntacticsearch/.merlin
419419
src/ext/makecfg/.merlin
420+
test/a.out

‎Makefile.in‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -164,6 +164,8 @@ $(OBJDIR)/machdep.ml : src/machdep-ml.c configure.ac Makefile.in
164164
@echo " sizeof_longlong: int; (* Size of \"long long\" *)" >> $@
165165
@echo " sizeof_ptr: int; (* Size of pointers *)" >> $@
166166
@echo " sizeof_float: int; (* Size of \"float\" *)" >> $@
167+
@echo " sizeof_float32x: int; (* Size of \"_Float32x\" *)" >> $@
168+
@echo " sizeof_float64x: int; (* Size of \"_Float64x\" *)" >> $@\
167169
@echo " sizeof_double: int; (* Size of \"double\" *)" >> $@
168170
@echo " sizeof_longdouble: int; (* Size of \"long double\" *)" >> $@
169171
@echo " sizeof_floatcomplex: int; (* Size of \"float _Complex\" *)" >> $@
@@ -181,6 +183,8 @@ $(OBJDIR)/machdep.ml : src/machdep-ml.c configure.ac Makefile.in
181183
@echo " alignof_ptr: int; (* Alignment of pointers *)" >> $@
182184
@echo " alignof_enum: int; (* Alignment of enum types *)" >> $@
183185
@echo " alignof_float: int; (* Alignment of \"float\" *)" >> $@
186+
@echo " alignof_float32x: int; (* Alignment of \"_Float32x\" *)" >> $@
187+
@echo " alignof_float64x: int; (* Alignment of \"_Float64x\" *)" >> $@
184188
@echo " alignof_double: int; (* Alignment of \"double\" *)" >> $@
185189
@echo " alignof_longdouble: int; (* Alignment of \"long double\" *)" >> $@
186190
@echo " alignof_floatcomplex: int; (* Alignment of \"float _Complex\" *)" >> $@

‎src/frontc/cabs.ml‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -67,7 +67,11 @@ type typeSpecifier = (* Merge all specifiers into one type *)
6767
| Tint64 (* TODO needed? *)
6868
| Tint128 (* TODO needed? *)
6969
| Tfloat
70+
| Tfloat32
71+
| Tfloat64
7072
| Tfloat128 (* TODO needed? *)
73+
| Tfloat32x
74+
| Tfloat64x
7175
| Tdouble
7276
| Tsigned
7377
| Tsizet (* used temporarily to translate offsetof() *)

‎src/frontc/cabs2cil.ml‎

Lines changed: 52 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2457,11 +2457,61 @@ let rec doSpecList (suggestedAnonName: string) (* This string will be part of
24572457
| [A.Tunsigned; A.Tint128] -> TInt(IUInt128, [])
24582458

24592459
| [A.Tfloat] -> TFloat(FFloat, [])
2460+
| [A.Tfloat32] ->
2461+
if !Machdep.theMachine.Machdep.sizeof_float = 4 then
2462+
TFloat(FFloat, [])
2463+
else
2464+
E.s (error "float32 only supported on machines where it is an alias for float")
2465+
| [A.Tfloat32x] ->
2466+
if !Machdep.theMachine.Machdep.sizeof_float32x = !Machdep.theMachine.Machdep.sizeof_float &&
2467+
!Machdep.theMachine.Machdep.alignof_float32x = !Machdep.theMachine.Machdep.alignof_float
2468+
then
2469+
TFloat(FFloat, [])
2470+
else if !Machdep.theMachine.Machdep.sizeof_float32x = !Machdep.theMachine.Machdep.sizeof_double &&
2471+
!Machdep.theMachine.Machdep.alignof_float32x = !Machdep.theMachine.Machdep.alignof_double
2472+
then
2473+
TFloat(FDouble, [])
2474+
else
2475+
E.s (error "float32x only supported on machines where it is an alias for a conventional type: size: %i align: %i "
2476+
!Machdep.theMachine.Machdep.sizeof_float32x
2477+
!Machdep.theMachine.Machdep.alignof_float32x
2478+
)
2479+
24602480
| [A.Tdouble] -> TFloat(FDouble, [])
2481+
| [A.Tfloat64] ->
2482+
if !Machdep.theMachine.Machdep.sizeof_double = 8 then
2483+
TFloat(FDouble, [])
2484+
else
2485+
E.s (error "float64 only supported on machines where it is an alias for double")
2486+
| [A.Tfloat64x] ->
2487+
if !Machdep.theMachine.Machdep.sizeof_float64x = !Machdep.theMachine.Machdep.sizeof_float &&
2488+
!Machdep.theMachine.Machdep.alignof_float64x = !Machdep.theMachine.Machdep.alignof_float
2489+
then
2490+
TFloat(FFloat, [])
2491+
else if !Machdep.theMachine.Machdep.sizeof_float64x = !Machdep.theMachine.Machdep.sizeof_double &&
2492+
!Machdep.theMachine.Machdep.alignof_float64x = !Machdep.theMachine.Machdep.alignof_double
2493+
then
2494+
TFloat(FDouble, [])
2495+
else if !Machdep.theMachine.Machdep.sizeof_float64x = !Machdep.theMachine.Machdep.sizeof_longdouble &&
2496+
!Machdep.theMachine.Machdep.alignof_float64x = !Machdep.theMachine.Machdep.alignof_longdouble
2497+
then
2498+
TFloat(FLongDouble, [])
2499+
else
2500+
E.s (error "float64x only supported on machines where it is an alias for a conventional type: size: %i align: %i "
2501+
!Machdep.theMachine.Machdep.sizeof_float64x
2502+
!Machdep.theMachine.Machdep.alignof_float64x
2503+
)
24612504

24622505
| [A.Tlong; A.Tdouble] -> TFloat(FLongDouble, [])
2463-
| [A.Tfloat128] -> TFloat(FLongDouble, []) (* TODO: Correct? *)
2464-
2506+
| [A.Tfloat128] ->
2507+
(* This is only correct w.r.t. to size and align. If we analyze floats, we need to be careful here *)
2508+
if !Machdep.theMachine.Machdep.sizeof_longdouble = 16 && !Machdep.theMachine.Machdep.alignof_longdouble = 16 then
2509+
TFloat(FLongDouble, [])
2510+
else
2511+
E.s (error "float128 only supported on machines where it is an alias (w.r.t. to size and align) of long double: size: %i align: %i "
2512+
!Machdep.theMachine.Machdep.sizeof_longdouble
2513+
!Machdep.theMachine.Machdep.alignof_longdouble
2514+
)
24652515
(* Now the other type specifiers *)
24662516
| [A.Tdefault] -> E.s (error "Default outside generic associations")
24672517
| [A.Tnamed n] -> begin

‎src/frontc/clexer.mll‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -139,6 +139,10 @@ let init_lexicon _ =
139139
("float", fun loc -> FLOAT loc);
140140
("__float128", fun loc -> FLOAT128 loc);
141141
("_Float128", fun loc -> FLOAT128 loc);
142+
("_Float32", fun loc -> FLOAT32 loc);
143+
("_Float64", fun loc -> FLOAT64 loc);
144+
("_Float32x", fun loc -> FLOAT32X loc);
145+
("_Float64x", fun loc -> FLOAT64X loc);
142146
("double", fun loc -> DOUBLE loc);
143147
("void", fun loc -> VOID loc);
144148
("enum", fun loc -> ENUM loc);

‎src/frontc/cparser.mly‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -252,6 +252,8 @@ let transformOffsetOf (speclist, dtype) member =
252252
%token EOF
253253
%token<Cabs.cabsloc> CHAR INT BOOL DOUBLE FLOAT VOID INT64 INT32
254254
%token<Cabs.cabsloc> INT128 FLOAT128 COMPLEX /* C99 */
255+
%token<Cabs.cabsloc> FLOAT32 FLOAT64 /* FloatN */
256+
%token<Cabs.cabsloc> FLOAT32X FLOAT64X /* FloatNx */
255257
%token<Cabs.cabsloc> GENERIC NORETURN /* C11 */
256258
%token<Cabs.cabsloc> ENUM STRUCT TYPEDEF UNION
257259
%token<Cabs.cabsloc> SIGNED UNSIGNED LONG SHORT
@@ -981,7 +983,11 @@ type_spec: /* ISO 6.7.2 */
981983
| INT64 { Tint64, $1 }
982984
| INT128 { Tint128, $1 }
983985
| FLOAT { Tfloat, $1 }
986+
| FLOAT32 { Tfloat32, $1 }
987+
| FLOAT64 { Tfloat64, $1 }
984988
| FLOAT128 { Tfloat128, $1 }
989+
| FLOAT32X { Tfloat32x, $1 }
990+
| FLOAT64X { Tfloat64x, $1 }
985991
| DOUBLE { Tdouble, $1 }
986992
/* | COMPLEX FLOAT { Tfloat, $2 } */
987993
/* | COMPLEX FLOAT128{ Tfloat128, $2 } */

‎src/frontc/cprint.ml‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -167,7 +167,11 @@ and print_type_spec = function
167167
| Tint64 -> print "__int64 "
168168
| Tint128 -> print "__int128 "
169169
| Tfloat -> print "float "
170+
| Tfloat32 -> print "_Float32"
171+
| Tfloat64 -> print "_Float64"
170172
| Tfloat128 -> print "__float128"
173+
| Tfloat32x -> print "_Float32x"
174+
| Tfloat64x -> print "_Float64x"
171175
| Tdouble -> print "double "
172176
| Tsigned -> printu "signed"
173177
| Tunsigned -> print "unsigned "

‎src/machdep-ml.c.in‎

Lines changed: 46 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,11 @@
11
/*
22
*
3-
* Copyright (c) 2001-2002,
3+
* Copyright (c) 2001-2002,
44
* George C. Necula <necula@cs.berkeley.edu>
55
* Scott McPeak <smcpeak@cs.berkeley.edu>
66
* Wes Weimer <weimer@cs.berkeley.edu>
77
* All rights reserved.
8-
*
8+
*
99
* Redistribution and use in source and binary forms, with or without
1010
* modification, are permitted provided that the following conditions are
1111
* met:
@@ -91,7 +91,7 @@ int main(int argc, char **argv)
9191
{
9292
int env = argc == 2 && !strcmp(argv[1], "--env");
9393
int alignof_short, alignof_int, alignof_long, alignof_ptr, alignof_enum,
94-
alignof_float, alignof_double, alignof_longdouble,
94+
alignof_float, alignof_float32x, alignof_float64x, alignof_double, alignof_longdouble,
9595
alignof_floatcomplex, alignof_doublecomplex, alignof_longdoublecomplex,
9696
sizeof_fun,
9797
alignof_fun, alignof_str, alignof_aligned, alignof_longlong,
@@ -114,7 +114,7 @@ int main(int argc, char **argv)
114114
};
115115
alignof_int = (intptr_t)(&((struct intstruct*)0)->i);
116116
}
117-
117+
118118
// The alignment of a bool
119119
{
120120
struct boolstruct {
@@ -123,7 +123,7 @@ int main(int argc, char **argv)
123123
};
124124
alignof_bool = (intptr_t)(&((struct boolstruct*)0)->b);
125125
}
126-
126+
127127
// The alignment of a long
128128
{
129129
struct longstruct {
@@ -132,7 +132,7 @@ int main(int argc, char **argv)
132132
};
133133
alignof_long = (intptr_t)(&((struct longstruct*)0)->l);
134134
}
135-
135+
136136
// The alignment of long long
137137
{
138138
struct longlong {
@@ -145,7 +145,7 @@ int main(int argc, char **argv)
145145
// The alignment of a ptr
146146
{
147147
struct ptrstruct {
148-
char c;
148+
char c;
149149
int * p;
150150
};
151151
alignof_ptr = (intptr_t)(&((struct ptrstruct*)0)->p);
@@ -154,12 +154,12 @@ int main(int argc, char **argv)
154154
// The alignment of an enum
155155
{
156156
struct enumstruct {
157-
char c;
157+
char c;
158158
enum e2 { THREE, FOUR, FIVE } e;
159159
};
160160
alignof_enum = (intptr_t)(&((struct enumstruct*)0)->e);
161161
}
162-
162+
163163
// The alignment of a float
164164
{
165165
struct floatstruct {
@@ -168,15 +168,33 @@ int main(int argc, char **argv)
168168
};
169169
alignof_float = (intptr_t)(&((struct floatstruct*)0)->f);
170170
}
171-
171+
172+
// The alignment of a _Float32x
173+
{
174+
struct floatstruct {
175+
char c;
176+
_Float32x f;
177+
};
178+
alignof_float32x = (intptr_t)(&((struct floatstruct*)0)->f);
179+
}
180+
181+
// The alignment of a _Float64x
182+
{
183+
struct floatstruct {
184+
char c;
185+
_Float64x f;
186+
};
187+
alignof_float64x = (intptr_t)(&((struct floatstruct*)0)->f);
188+
}
189+
172190
// The alignment of double
173191
{
174192
struct s1 {
175193
char c;
176194
double d;
177195
};
178196
alignof_double = (intptr_t)(&((struct s1*)0)->d);
179-
}
197+
}
180198

181199
// The alignment of long double
182200
{
@@ -185,8 +203,8 @@ int main(int argc, char **argv)
185203
long double ld;
186204
};
187205
alignof_longdouble = (intptr_t)(&((struct s1*)0)->ld);
188-
}
189-
206+
}
207+
190208
// The alignment of a float complex
191209
{
192210
struct floatstruct {
@@ -250,21 +268,24 @@ int main(int argc, char **argv)
250268
{
251269
fprintf(stderr, "Generating CIL_MACHINE machine dependency information string (for CIL)\n");
252270
printf("short=%d,%d int=%d,%d long=%d,%d long_long=%d,%d pointer=%d,%d "
253-
"alignof_enum=%d float=%d,%d double=%d,%d long_double=%d,%d float_complex=%d,%d double_complex=%d,%d long_double_complex=%d,%d void=%d "
271+
"alignof_enum=%d float=%d,%d float32x=%d,%d float64x=%d,%d double=%d,%d long_double=%d,%d float_complex=%d,%d double_complex=%d,%d long_double_complex=%d,%d void=%d "
254272
"bool=%d,%d fun=%d,%d alignof_string=%d max_alignment=%d size_t=%s "
255273
"wchar_t=%s char_signed=%s "
256274
"big_endian=%s __thread_is_keyword=%s __builtin_va_list=%s "
257275
"underscore_name=%s\n",
258276
(int)sizeof(short), alignof_short, (int)sizeof(int), alignof_int,
259-
(int)sizeof(long), alignof_long, (int)sizeof(long long), alignof_longlong,
260-
(int)sizeof(int *), alignof_ptr, alignof_enum,
261-
(int)sizeof(float), alignof_float, (int)sizeof(double), alignof_double,
277+
(int)sizeof(long), alignof_long, (int)sizeof(long long), alignof_longlong,
278+
(int)sizeof(int *), alignof_ptr,
279+
alignof_enum,
280+
(int)sizeof(_Float32x), alignof_float32x,
281+
(int)sizeof(_Float64x), alignof_float64x,
282+
(int)sizeof(float), alignof_float, (int)sizeof(double), alignof_double,
262283
(int)sizeof(long double), alignof_longdouble, (int)sizeof(float _Complex), alignof_floatcomplex, (int)sizeof(double _Complex), alignof_doublecomplex,
263284
(int)sizeof(long double _Complex), alignof_longdoublecomplex, (int)sizeof(void),
264285
(int)sizeof(bool), alignof_bool,
265-
sizeof_fun, alignof_fun, alignof_str, alignof_aligned,
266-
underscore(TYPE_SIZE_T), underscore(TYPE_WCHAR_T),
267-
char_is_unsigned ? "false" : "true",
286+
sizeof_fun, alignof_fun, alignof_str, alignof_aligned,
287+
underscore(TYPE_SIZE_T), underscore(TYPE_WCHAR_T),
288+
char_is_unsigned ? "false" : "true",
268289
little_endian ? "false" : "true",
269290
THREAD_IS_KEYWORD, HAVE_BUILTIN_VA_LIST, UNDERSCORE_NAME);
270291
}
@@ -285,6 +306,8 @@ int main(int argc, char **argv)
285306
printf("\t sizeof_longlong = %d;\n", (int)sizeof(LONGLONG));
286307
printf("\t sizeof_ptr = %d;\n", (int)sizeof(int *));
287308
printf("\t sizeof_float = %d;\n", (int)sizeof(float));
309+
printf("\t sizeof_float32x = %d;\n", (int)sizeof(_Float32x));
310+
printf("\t sizeof_float64x = %d;\n", (int)sizeof(_Float64x));
288311
printf("\t sizeof_double = %d;\n", (int)sizeof(double));
289312
printf("\t sizeof_longdouble = %d;\n", (int)sizeof(long double));
290313
printf("\t sizeof_floatcomplex = %d;\n", (int)sizeof(float _Complex));
@@ -302,6 +325,8 @@ int main(int argc, char **argv)
302325
printf("\t alignof_ptr = %d;\n", alignof_ptr);
303326
printf("\t alignof_enum = %d;\n", alignof_enum);
304327
printf("\t alignof_float = %d;\n", alignof_float);
328+
printf("\t alignof_float32x = %d;\n", alignof_float32x);
329+
printf("\t alignof_float64x = %d;\n", alignof_float64x);
305330
printf("\t alignof_double = %d;\n", alignof_double);
306331
printf("\t alignof_longdouble = %d;\n", alignof_longdouble);
307332
printf("\t alignof_floatcomplex = %d;\n", alignof_floatcomplex);
@@ -317,4 +342,4 @@ int main(int argc, char **argv)
317342
printf("\t little_endian = %s;\n", little_endian ? "true" : "false");
318343
}
319344
return 0;
320-
}
345+
}

‎src/machdepenv.ml‎

Lines changed: 10 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ let preparse (s:string) : (string, string list) H.t =
99
let spaceRegexp = R.regexp "[ \t]+" in
1010
let specRegexp = R.regexp "^\\([a-zA-Z_0-9]+\\)[ \t]*=\\(.*\\)$" in
1111
let specs = R.split spaceRegexp s in
12-
let addSpec spec =
12+
let addSpec spec =
1313
if R.string_match specRegexp spec 0 then begin
1414
let name = R.matched_group 1 spec in
1515
let value = R.matched_group 2 spec in
@@ -22,19 +22,19 @@ let preparse (s:string) : (string, string list) H.t =
2222
specTable
2323

2424
let errorWrap name f =
25-
try
25+
try
2626
f name
2727
with Not_found -> raise (Failure (name ^ " not specified"))
2828
| _ -> raise (Failure ("invalid format for " ^ name))
2929

30-
let getNthString n specTable name =
30+
let getNthString n specTable name =
3131
let l = H.find specTable name in
3232
L.nth l n
3333

3434
let getNthInt n specTable name =
3535
errorWrap name (fun name -> int_of_string (getNthString n specTable name))
3636

37-
let getNthBool n specTable name =
37+
let getNthBool n specTable name =
3838
errorWrap name (fun name -> bool_of_string (getNthString n specTable name))
3939

4040
let getBool = getNthBool 0
@@ -44,10 +44,10 @@ let getAlignof = getNthInt 1
4444

4545
let respace = Str.global_replace (Str.regexp "_") " "
4646

47-
let modelParse (s:string) : mach =
47+
let modelParse (s:string) : mach =
4848
let entries =
4949
try
50-
preparse s
50+
preparse s
5151
with Failure msg -> raise (Failure msg)
5252
| _ -> raise (Failure "invalid machine specification")
5353
in
@@ -71,6 +71,10 @@ let modelParse (s:string) : mach =
7171
alignof_enum = getInt entries "alignof_enum";
7272
sizeof_float = getSizeof entries "float";
7373
alignof_float = getAlignof entries "float";
74+
sizeof_float32x = getSizeof entries "float32x";
75+
alignof_float32x = getAlignof entries "float32x";
76+
sizeof_float64x = getSizeof entries "float64x";
77+
alignof_float64x = getAlignof entries "float64x";
7478
sizeof_floatcomplex = getSizeof entries "float_complex";
7579
alignof_floatcomplex = getAlignof entries "float_complex";
7680
sizeof_double = getSizeof entries "double";

‎test/small1/c11-extendedFloat.c‎

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
// Technically not C11 but ISO/IEC TS 18661-3:2015
2+
#include "testharness.h"
3+
4+
_Float32 f32;
5+
_Float64 f64;
6+
_Float32x f32x;
7+
_Float64x f64x;
8+
9+
10+
int main() {
11+
if(sizeof(f32) != 4) {
12+
E(1);
13+
}
14+
15+
if(sizeof(f64) != 8) {
16+
E(2);
17+
}
18+
19+
SUCCESS;
20+
}

0 commit comments

Comments
 (0)