From 52e9737c104c068bc912c9cb3fa0fb3b04aa7c8a Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 3 May 2018 09:38:04 +0100 Subject: [PATCH] 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 --- regression/ansi-c/float_constant1/main.c | 11 ++ .../ansi-c/gcc_types_compatible_p1/main.c | 4 + src/ansi-c/Makefile | 1 + src/ansi-c/ansi_c_convert_type.cpp | 54 +++++- src/ansi-c/ansi_c_convert_type.h | 13 +- src/ansi-c/c_typecheck_type.cpp | 1 + src/ansi-c/gcc_types.cpp | 169 ++++++++++++++++++ src/ansi-c/gcc_types.h | 27 +++ src/ansi-c/literals/convert_float_literal.cpp | 64 +++---- src/ansi-c/literals/parse_float.cpp | 124 ++++++++----- src/ansi-c/literals/parse_float.h | 29 +-- src/ansi-c/parser.y | 20 ++- src/ansi-c/scanner.l | 44 ++++- src/cpp/cpp_convert_type.cpp | 2 + src/util/c_types.cpp | 35 ---- src/util/c_types.h | 3 - src/util/ieee_float.h | 7 + src/util/irep_ids.def | 6 + 18 files changed, 467 insertions(+), 147 deletions(-) create mode 100644 src/ansi-c/gcc_types.cpp create mode 100644 src/ansi-c/gcc_types.h diff --git a/regression/ansi-c/float_constant1/main.c b/regression/ansi-c/float_constant1/main.c index 3661c8a064f..4f109a85d6e 100644 --- a/regression/ansi-c/float_constant1/main.c +++ b/regression/ansi-c/float_constant1/main.c @@ -10,6 +10,17 @@ STATIC_ASSERT(0X1.0P-95F == 2.524355e-29f); // nothing before the dot STATIC_ASSERT(0X.0p+1f == 0); +// 32-bit, 64-bit and 128-bit constants, GCC proper only, +// clang doesn't have it +#if defined(__GNUC__) && !defined(__clang__) +STATIC_ASSERT(__builtin_types_compatible_p(_Float32, __typeof(1.0f32))); +STATIC_ASSERT(__builtin_types_compatible_p(_Float64, __typeof(1.0f64))); +STATIC_ASSERT(__builtin_types_compatible_p(_Float128, __typeof(1.0f128))); +STATIC_ASSERT(__builtin_types_compatible_p(_Float32x, __typeof(1.0f32x))); +STATIC_ASSERT(__builtin_types_compatible_p(_Float64x, __typeof(1.0f64x))); +STATIC_ASSERT(__builtin_types_compatible_p(_Float128x, __typeof(1.0f128x))); +#endif + #ifdef __GNUC__ _Complex c; #endif diff --git a/regression/ansi-c/gcc_types_compatible_p1/main.c b/regression/ansi-c/gcc_types_compatible_p1/main.c index 09b469b291f..d27ddfdac6b 100644 --- a/regression/ansi-c/gcc_types_compatible_p1/main.c +++ b/regression/ansi-c/gcc_types_compatible_p1/main.c @@ -97,6 +97,10 @@ STATIC_ASSERT(!__builtin_types_compatible_p(unsigned, signed)); #ifndef __clang__ // clang doesn't have these +STATIC_ASSERT(!__builtin_types_compatible_p(_Float32, float)); +STATIC_ASSERT(!__builtin_types_compatible_p(_Float64, double)); +STATIC_ASSERT(!__builtin_types_compatible_p(_Float32x, float)); +STATIC_ASSERT(!__builtin_types_compatible_p(_Float64x, double)); STATIC_ASSERT(!__builtin_types_compatible_p(__float80, double)); STATIC_ASSERT(!__builtin_types_compatible_p(__float128, long double)); STATIC_ASSERT(!__builtin_types_compatible_p(__float128, double)); diff --git a/src/ansi-c/Makefile b/src/ansi-c/Makefile index ada37c47f0c..d57c0934a7d 100644 --- a/src/ansi-c/Makefile +++ b/src/ansi-c/Makefile @@ -27,6 +27,7 @@ SRC = anonymous_member.cpp \ cprover_library.cpp \ designator.cpp \ expr2c.cpp \ + gcc_types.cpp \ literals/convert_character_literal.cpp \ literals/convert_float_literal.cpp \ literals/convert_integer_literal.cpp \ diff --git a/src/ansi-c/ansi_c_convert_type.cpp b/src/ansi-c/ansi_c_convert_type.cpp index 3c00f08f39d..0ac703eebee 100644 --- a/src/ansi-c/ansi_c_convert_type.cpp +++ b/src/ansi-c/ansi_c_convert_type.cpp @@ -20,6 +20,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include "gcc_types.h" + void ansi_c_convert_typet::read(const typet &type) { clear(); @@ -80,8 +82,20 @@ void ansi_c_convert_typet::read_rec(const typet &type) int32_cnt++; else if(type.id()==ID_int64) int64_cnt++; + else if(type.id()==ID_gcc_float16) + gcc_float16_cnt++; + else if(type.id()==ID_gcc_float32) + gcc_float32_cnt++; + else if(type.id()==ID_gcc_float32x) + gcc_float32x_cnt++; + else if(type.id()==ID_gcc_float64) + gcc_float64_cnt++; + else if(type.id()==ID_gcc_float64x) + gcc_float64x_cnt++; else if(type.id()==ID_gcc_float128) gcc_float128_cnt++; + else if(type.id()==ID_gcc_float128x) + gcc_float128x_cnt++; else if(type.id()==ID_gcc_int128) gcc_int128_cnt++; else if(type.id()==ID_gcc_attribute_mode) @@ -248,7 +262,11 @@ void ansi_c_convert_typet::write(typet &type) unsigned_cnt || int_cnt || c_bool_cnt || proper_bool_cnt || short_cnt || char_cnt || complex_cnt || long_cnt || int8_cnt || int16_cnt || int32_cnt || int64_cnt || - gcc_float128_cnt || gcc_int128_cnt || bv_cnt) + gcc_float16_cnt || + gcc_float32_cnt || gcc_float32x_cnt || + gcc_float64_cnt || gcc_float64x_cnt || + gcc_float128_cnt || gcc_float128x_cnt || + gcc_int128_cnt || bv_cnt) { error().source_location=source_location; error() << "illegal type modifier for defined type" << eom; @@ -305,7 +323,10 @@ void ansi_c_convert_typet::write(typet &type) << "found " << type.pretty() << eom; throw 0; } - else if(gcc_float128_cnt) + else if(gcc_float16_cnt || + gcc_float32_cnt || gcc_float32x_cnt || + gcc_float64_cnt || gcc_float64x_cnt || + gcc_float128_cnt || gcc_float128x_cnt) { if(signed_cnt || unsigned_cnt || int_cnt || c_bool_cnt || proper_bool_cnt || int8_cnt || int16_cnt || int32_cnt || int64_cnt || @@ -313,19 +334,38 @@ void ansi_c_convert_typet::write(typet &type) short_cnt || char_cnt) { error().source_location=source_location; - error() << "cannot combine integer type with float" << eom; + error() << "cannot combine integer type with floating-point type" << eom; throw 0; } - if(long_cnt || double_cnt || float_cnt) + if(long_cnt+double_cnt+ + float_cnt+gcc_float16_cnt+ + gcc_float32_cnt+gcc_float32x_cnt+ + gcc_float64_cnt+gcc_float64x_cnt+ + gcc_float128_cnt+gcc_float128x_cnt>=2) { error().source_location=source_location; error() << "conflicting type modifiers" << eom; throw 0; } - // _not_ the same as long double - type=gcc_float128_type(); + // _not_ the same as float, double, long double + if(gcc_float16_cnt) + type=gcc_float16_type(); + else if(gcc_float32_cnt) + type=gcc_float32_type(); + else if(gcc_float32x_cnt) + type=gcc_float32x_type(); + else if(gcc_float64_cnt) + type=gcc_float64_type(); + else if(gcc_float64x_cnt) + type=gcc_float64x_type(); + else if(gcc_float128_cnt) + type=gcc_float128_type(); + else if(gcc_float128x_cnt) + type=gcc_float128x_type(); + else + UNREACHABLE; } else if(double_cnt || float_cnt) { @@ -335,7 +375,7 @@ void ansi_c_convert_typet::write(typet &type) short_cnt || char_cnt) { error().source_location=source_location; - error() << "cannot combine integer type with float" << eom; + error() << "cannot combine integer type with floating-point type" << eom; throw 0; } diff --git a/src/ansi-c/ansi_c_convert_type.h b/src/ansi-c/ansi_c_convert_type.h index 47c6c70564b..b1ad279fa36 100644 --- a/src/ansi-c/ansi_c_convert_type.h +++ b/src/ansi-c/ansi_c_convert_type.h @@ -28,7 +28,12 @@ class ansi_c_convert_typet:public messaget // extensions unsigned int8_cnt, int16_cnt, int32_cnt, int64_cnt, ptr32_cnt, ptr64_cnt, - gcc_float128_cnt, gcc_int128_cnt, bv_cnt, + gcc_float16_cnt, + gcc_float32_cnt, gcc_float32x_cnt, + gcc_float64_cnt, gcc_float64x_cnt, + gcc_float128_cnt, gcc_float128x_cnt, + gcc_int128_cnt, + bv_cnt, floatbv_cnt, fixedbv_cnt; typet gcc_attribute_mode; @@ -63,7 +68,11 @@ class ansi_c_convert_typet:public messaget long_cnt=double_cnt=float_cnt=c_bool_cnt=proper_bool_cnt=complex_cnt= int8_cnt=int16_cnt=int32_cnt=int64_cnt= ptr32_cnt=ptr64_cnt= - gcc_float128_cnt=gcc_int128_cnt=bv_cnt=floatbv_cnt=fixedbv_cnt=0; + gcc_float16_cnt= + gcc_float32_cnt=gcc_float32x_cnt= + gcc_float64_cnt=gcc_float64x_cnt= + gcc_float128_cnt=gcc_float128x_cnt= + gcc_int128_cnt=bv_cnt=floatbv_cnt=fixedbv_cnt=0; vector_size.make_nil(); alignment.make_nil(); bv_width.make_nil(); diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp index dcb40a0e897..1aae265fd53 100644 --- a/src/ansi-c/c_typecheck_type.cpp +++ b/src/ansi-c/c_typecheck_type.cpp @@ -21,6 +21,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "ansi_c_convert_type.h" #include "c_qualifiers.h" +#include "gcc_types.h" #include "padding.h" #include "type2name.h" diff --git a/src/ansi-c/gcc_types.cpp b/src/ansi-c/gcc_types.cpp new file mode 100644 index 00000000000..5ac8a9b4220 --- /dev/null +++ b/src/ansi-c/gcc_types.cpp @@ -0,0 +1,169 @@ +/*******************************************************************\ + +Module: + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +#include "gcc_types.h" + +#include +#include + +bitvector_typet gcc_float16_type() +{ + if(config.ansi_c.use_fixed_for_float) + { + fixedbv_typet result; + result.set_width(16); + result.set_integer_bits(16/2); + result.set(ID_C_c_type, ID_gcc_float16); + return result; + } + else + { + floatbv_typet result= + ieee_float_spect::half_precision().to_type(); + result.set(ID_C_c_type, ID_gcc_float16); + return result; + } +} + +bitvector_typet gcc_float32_type() +{ + // not same as float! + + if(config.ansi_c.use_fixed_for_float) + { + fixedbv_typet result; + result.set_width(config.ansi_c.single_width); + result.set_integer_bits(config.ansi_c.single_width/2); + result.set(ID_C_c_type, ID_gcc_float32); + return result; + } + else + { + floatbv_typet result= + ieee_float_spect::single_precision().to_type(); + result.set(ID_C_c_type, ID_gcc_float32); + return result; + } +} + +bitvector_typet gcc_float32x_type() +{ + // not same as float! + + if(config.ansi_c.use_fixed_for_float) + { + fixedbv_typet result; + result.set_width(config.ansi_c.single_width); + result.set_integer_bits(config.ansi_c.single_width/2); + result.set(ID_C_c_type, ID_gcc_float32x); + return result; + } + else + { + floatbv_typet result= + ieee_float_spect::single_precision().to_type(); + result.set(ID_C_c_type, ID_gcc_float32x); + return result; + } +} + +bitvector_typet gcc_float64_type() +{ + // not same as double! + if(config.ansi_c.use_fixed_for_float) + { + fixedbv_typet result; + result.set_width(config.ansi_c.double_width); + result.set_integer_bits(config.ansi_c.double_width/2); + result.set(ID_C_c_type, ID_gcc_float64); + return result; + } + else + { + floatbv_typet result= + ieee_float_spect::double_precision().to_type(); + result.set(ID_C_c_type, ID_gcc_float64); + return result; + } +} + +bitvector_typet gcc_float64x_type() +{ + // not same as double! + if(config.ansi_c.use_fixed_for_float) + { + fixedbv_typet result; + result.set_width(config.ansi_c.double_width); + result.set_integer_bits(config.ansi_c.double_width/2); + result.set(ID_C_c_type, ID_gcc_float64x); + return result; + } + else + { + floatbv_typet result= + ieee_float_spect::double_precision().to_type(); + result.set(ID_C_c_type, ID_gcc_float64x); + return result; + } +} + +bitvector_typet gcc_float128_type() +{ + // not same as long double! + + if(config.ansi_c.use_fixed_for_float) + { + fixedbv_typet result; + result.set_width(128); + result.set_integer_bits(128/2); + result.set(ID_C_c_type, ID_gcc_float128); + return result; + } + else + { + floatbv_typet result= + ieee_float_spect::quadruple_precision().to_type(); + result.set(ID_C_c_type, ID_gcc_float128); + return result; + } +} + +bitvector_typet gcc_float128x_type() +{ + // not same as long double! + + if(config.ansi_c.use_fixed_for_float) + { + fixedbv_typet result; + result.set_width(128); + result.set_integer_bits(128/2); + result.set(ID_C_c_type, ID_gcc_float128x); + return result; + } + else + { + floatbv_typet result= + ieee_float_spect::quadruple_precision().to_type(); + result.set(ID_C_c_type, ID_gcc_float128x); + return result; + } +} + +unsignedbv_typet gcc_unsigned_int128_type() +{ + unsignedbv_typet result(128); + result.set(ID_C_c_type, ID_unsigned_int128); + return result; +} + +signedbv_typet gcc_signed_int128_type() +{ + signedbv_typet result(128); + result.set(ID_C_c_type, ID_signed_int128); + return result; +} diff --git a/src/ansi-c/gcc_types.h b/src/ansi-c/gcc_types.h new file mode 100644 index 00000000000..95f4b4957d7 --- /dev/null +++ b/src/ansi-c/gcc_types.h @@ -0,0 +1,27 @@ +/*******************************************************************\ + +Module: + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +#ifndef CPROVER_ANSI_C_GCC_TYPES_H +#define CPROVER_ANSI_C_GCC_TYPES_H + +#include + +// These are gcc-specific; most are not implemented by clang +// https://gcc.gnu.org/onlinedocs/gcc/Floating-Types.html + +bitvector_typet gcc_float16_type(); +bitvector_typet gcc_float32_type(); +bitvector_typet gcc_float32x_type(); +bitvector_typet gcc_float64_type(); +bitvector_typet gcc_float64x_type(); +bitvector_typet gcc_float128_type(); +bitvector_typet gcc_float128x_type(); +unsignedbv_typet gcc_unsigned_int128_type(); +signedbv_typet gcc_signed_int128_type(); + +#endif // CPROVER_ANSI_C_GCC_TYPES_H diff --git a/src/ansi-c/literals/convert_float_literal.cpp b/src/ansi-c/literals/convert_float_literal.cpp index 626b046b5fa..19a9467b3cc 100644 --- a/src/ansi-c/literals/convert_float_literal.cpp +++ b/src/ansi-c/literals/convert_float_literal.cpp @@ -22,26 +22,11 @@ Author: Daniel Kroening, kroening@kroening.com #include #include "parse_float.h" +#include "../gcc_types.h" exprt convert_float_literal(const std::string &src) { - mp_integer significand; - mp_integer exponent; - bool is_float, is_long, is_imaginary; - bool is_decimal, is_float80, is_float128; // GCC extensions - unsigned base; - - parse_float( - src, - significand, - exponent, - base, - is_float, - is_long, - is_imaginary, - is_decimal, - is_float80, - is_float128); + parse_floatt parsed_float(src); exprt result=exprt(ID_constant); @@ -51,20 +36,29 @@ exprt convert_float_literal(const std::string &src) // This can be overridden with // config.ansi_c.single_precision_constant. - if(is_float) + if(parsed_float.is_float) result.type()=float_type(); - else if(is_long) + else if(parsed_float.is_long) result.type()=long_double_type(); - else if(is_float80) + else if(parsed_float.is_float16) + result.type()=gcc_float16_type(); + else if(parsed_float.is_float32) + result.type()=gcc_float32_type(); + else if(parsed_float.is_float32x) + result.type()=gcc_float32x_type(); + else if(parsed_float.is_float64) + result.type()=gcc_float64_type(); + else if(parsed_float.is_float64x) + result.type()=gcc_float64x_type(); + else if(parsed_float.is_float80) { result.type()=ieee_float_spect(64, 15).to_type(); result.type().set(ID_C_c_type, ID_long_double); } - else if(is_float128) - { - result.type()=ieee_float_spect::quadruple_precision().to_type(); - result.type().set(ID_C_c_type, ID_gcc_float128); - } + else if(parsed_float.is_float128) + result.type()=gcc_float128_type(); + else if(parsed_float.is_float128x) + result.type()=gcc_float128x_type(); else { // default @@ -74,7 +68,7 @@ exprt convert_float_literal(const std::string &src) result.type()=double_type(); // default } - if(is_decimal) + if(parsed_float.is_decimal) { // TODO - should set ID_gcc_decimal32/ID_gcc_decimal64/ID_gcc_decimal128, // but these aren't handled anywhere @@ -94,15 +88,15 @@ exprt convert_float_literal(const std::string &src) fraction_bits=width-std::stoi(id2string(integer_bits)); mp_integer factor=mp_integer(1)<=power(2, width-1)) { @@ -123,10 +117,10 @@ exprt convert_float_literal(const std::string &src) { ieee_floatt a(to_floatbv_type(result.type())); - if(base==10) - a.from_base10(significand, exponent); - else if(base==2) // hex - a.build(significand, exponent); + if(parsed_float.exponent_base==10) + a.from_base10(parsed_float.significand, parsed_float.exponent); + else if(parsed_float.exponent_base==2) // hex + a.build(parsed_float.significand, parsed_float.exponent); else assert(false); @@ -135,7 +129,7 @@ exprt convert_float_literal(const std::string &src) integer2binary(a.pack(), a.spec.width())); } - if(is_imaginary) + if(parsed_float.is_imaginary) { const complex_typet complex_type(result.type()); return complex_exprt(from_integer(0, result.type()), result, complex_type); diff --git a/src/ansi-c/literals/parse_float.cpp b/src/ansi-c/literals/parse_float.cpp index d6b85acecbb..b56f9e44f93 100644 --- a/src/ansi-c/literals/parse_float.cpp +++ b/src/ansi-c/literals/parse_float.cpp @@ -11,15 +11,11 @@ Author: Daniel Kroening, kroening@kroening.com #include "parse_float.h" +#include #include +#include -void parse_float( - const std::string &src, - mp_integer &significand, - mp_integer &exponent, - unsigned &exponent_base, - bool &is_float, bool &is_long, bool &is_imaginary, - bool &is_decimal, bool &is_float80, bool &is_float128) +parse_floatt::parse_floatt(const std::string &src) { // {digits}{dot}{digits}{exponent}?{floatsuffix}? // {digits}{dot}{exponent}?{floatsuffix}? @@ -30,7 +26,14 @@ void parse_float( // 0x{hexdigits}{dot}{hexdigits}[pP]{exponent}{floatsuffix}? // 0x{hexdigits}{dot}[pP]{exponent}{floatsuffix}? - const char *p=src.c_str(); + // These are case-insensitive, and we handle this + // by first converting to lower case. + + std::string src_lower=src; + std::transform(src_lower.begin(), src_lower.end(), + src_lower.begin(), ::tolower); + + const char *p=src_lower.c_str(); std::string str_whole_number, str_fraction_part, @@ -40,7 +43,7 @@ void parse_float( // is this hex? - if(src.size()>=2 && src[0]=='0' && tolower(src[1])=='x') + if(src_lower.size()>=2 && src_lower[0]=='0' && src_lower[1]=='x') { // skip the 0x p+=2; @@ -48,7 +51,7 @@ void parse_float( exponent_base=2; // get whole number part - while(*p!='.' && *p!=0 && *p!='p' && *p!='P') + while(*p!='.' && *p!=0 && *p!='p') { str_whole_number+=*p; p++; @@ -59,14 +62,14 @@ void parse_float( p++; // get fraction part - while(*p!=0 && *p!='p' && *p!='P') + while(*p!=0 && *p!='p') { str_fraction_part+=*p; p++; } - // skip P - if(*p=='p' || *p=='P') + // skip p + if(*p=='p') p++; // skip + @@ -74,8 +77,8 @@ void parse_float( p++; // get exponent - while(*p!=0 && *p!='f' && *p!='F' && *p!='l' && *p!='L' && - *p!='w' && *p!='W' && *p!='q' && *p!='Q' && *p!='d' && *p!='D') + while(*p!=0 && *p!='f' && *p!='l' && + *p!='w' && *p!='q' && *p!='d') { str_exponent+=*p; p++; @@ -104,10 +107,10 @@ void parse_float( else { // get whole number part - while(*p!='.' && *p!=0 && *p!='e' && *p!='E' && - *p!='f' && *p!='F' && *p!='l' && *p!='L' && - *p!='w' && *p!='W' && *p!='q' && *p!='Q' && *p!='d' && *p!='D' && - *p!='i' && *p!='I' && *p!='j' && *p!='J') + while(*p!='.' && *p!=0 && *p!='e' && + *p!='f' && *p!='l' && + *p!='w' && *p!='q' && *p!='d' && + *p!='i' && *p!='j') { str_whole_number+=*p; p++; @@ -118,17 +121,17 @@ void parse_float( p++; // get fraction part - while(*p!=0 && *p!='e' && *p!='E' && - *p!='f' && *p!='F' && *p!='l' && *p!='L' && - *p!='w' && *p!='W' && *p!='q' && *p!='Q' && *p!='d' && *p!='D' && - *p!='i' && *p!='I' && *p!='j' && *p!='J') + while(*p!=0 && *p!='e' && + *p!='f' && *p!='l' && + *p!='w' && *p!='q' && *p!='d' && + *p!='i' && *p!='j') { str_fraction_part+=*p; p++; } - // skip E - if(*p=='e' || *p=='E') + // skip e + if(*p=='e') p++; // skip + @@ -136,9 +139,9 @@ void parse_float( p++; // get exponent - while(*p!=0 && *p!='f' && *p!='F' && *p!='l' && *p!='L' && - *p!='w' && *p!='W' && *p!='q' && *p!='Q' && *p!='d' && *p!='D' && - *p!='i' && *p!='I' && *p!='j' && *p!='J') + while(*p!=0 && *p!='f' && *p!='l' && + *p!='w' && *p!='q' && *p!='d' && + *p!='i' && *p!='j') { str_exponent+=*p; p++; @@ -162,27 +165,50 @@ void parse_float( } // get flags - is_float=is_long=is_imaginary=is_decimal=is_float80=is_float128=false; - - while(*p!=0) + is_float=is_long=false; + is_imaginary=is_decimal=false; + is_float16=false; + is_float32=is_float32x=false; + is_float64=is_float64x=false; + is_float80=false; + is_float128=is_float128x=false; + + if(strcmp(p, "f16")==0) + is_float16=true; + else if(strcmp(p, "f32")==0) + is_float32=true; + else if(strcmp(p, "f32x")==0) + is_float32x=true; + else if(strcmp(p, "f64")==0) + is_float64=true; + else if(strcmp(p, "f64x")==0) + is_float64x=true; + else if(strcmp(p, "f128")==0) + is_float128=true; + else if(strcmp(p, "f128x")==0) + is_float128x=true; + else { - if(*p=='f' || *p=='F') - is_float=true; - else if(*p=='l' || *p=='L') - is_long=true; - else if(*p=='i' || *p=='I' || *p=='j' || *p=='J') - is_imaginary=true; - // http://gcc.gnu.org/onlinedocs/gcc/Decimal-Float.html - else if(*p=='d' || *p=='D') - // a suffix with just d or D but nothing else is a GCC extension with no - // particular effect -- and forbidden by Clang - is_decimal=is_decimal || *(p+1)!=0; - // http://gcc.gnu.org/onlinedocs/gcc/Floating-Types.html - else if(*p=='w' || *p=='W') - is_float80=true; - else if(*p=='q' || *p=='Q') - is_float128=true; - - p++; + while(*p!=0) + { + if(*p=='f') + is_float=true; + else if(*p=='l') + is_long=true; + else if(*p=='i' || *p=='j') + is_imaginary=true; + // http://gcc.gnu.org/onlinedocs/gcc/Decimal-Float.html + else if(*p=='d') + // a suffix with just d or D but nothing else is a GCC extension with no + // particular effect -- and forbidden by Clang + is_decimal=is_decimal || *(p+1)!=0; + // http://gcc.gnu.org/onlinedocs/gcc/Floating-Types.html + else if(*p=='w') + is_float80=true; + else if(*p=='q') + is_float128=true; + + p++; + } } } diff --git a/src/ansi-c/literals/parse_float.h b/src/ansi-c/literals/parse_float.h index b750c0cd77b..8268d475ec4 100644 --- a/src/ansi-c/literals/parse_float.h +++ b/src/ansi-c/literals/parse_float.h @@ -16,16 +16,23 @@ Author: Daniel Kroening, kroening@kroening.com #include -void parse_float( - const std::string &src, - mp_integer &significand, - mp_integer &exponent, - unsigned &exponent_base, // 2 (hex) or 10 - bool &is_float, - bool &is_long, - bool &is_imaginary, // a gcc extension - bool &is_decimal, // a gcc extension - bool &is_float80, // a gcc extension - bool &is_float128); // a gcc extension +class parse_floatt +{ +public: + mp_integer significand, exponent; + unsigned exponent_base; // 2 (hex) or 10 + + bool is_float, is_long; + + // gcc extensions + bool is_imaginary, is_decimal, is_float16, + is_float32, is_float32x, + is_float64, is_float64x, + is_float80, + is_float128, is_float128x; + + // parse! + explicit parse_floatt(const std::string &); +}; #endif // CPROVER_ANSI_C_LITERALS_PARSE_FLOAT_H diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y index ce04136d8e2..7f590e90e2d 100644 --- a/src/ansi-c/parser.y +++ b/src/ansi-c/parser.y @@ -121,8 +121,14 @@ extern char *yyansi_ctext; %token TOK_PTR64 "__ptr64" %token TOK_TYPEOF "typeof" %token TOK_GCC_AUTO_TYPE "__auto_type" +%token TOK_GCC_FLOAT16 "_Float16" +%token TOK_GCC_FLOAT32 "_Float32" +%token TOK_GCC_FLOAT32X "_Float32x" %token TOK_GCC_FLOAT80 "__float80" -%token TOK_GCC_FLOAT128 "__float128" +%token TOK_GCC_FLOAT64 "_Float64" +%token TOK_GCC_FLOAT64X "_Float64x" +%token TOK_GCC_FLOAT128 "_Float128" +%token TOK_GCC_FLOAT128X "_Float128x" %token TOK_GCC_INT128 "__int128" %token TOK_GCC_DECIMAL32 "_Decimal32" %token TOK_GCC_DECIMAL64 "_Decimal64" @@ -1388,9 +1394,15 @@ basic_type_name: | TOK_SHORT { $$=$1; set($$, ID_short); } | TOK_LONG { $$=$1; set($$, ID_long); } | TOK_FLOAT { $$=$1; set($$, ID_float); } - | TOK_GCC_FLOAT80 { $$=$1; set($$, ID_gcc_float80); } - | TOK_GCC_FLOAT128 { $$=$1; set($$, ID_gcc_float128); } - | TOK_GCC_INT128 { $$=$1; set($$, ID_gcc_int128); } + | TOK_GCC_FLOAT16 { $$=$1; set($$, ID_gcc_float16); } + | TOK_GCC_FLOAT32 { $$=$1; set($$, ID_gcc_float32); } + | TOK_GCC_FLOAT32X { $$=$1; set($$, ID_gcc_float32x); } + | TOK_GCC_FLOAT64 { $$=$1; set($$, ID_gcc_float64); } + | TOK_GCC_FLOAT64X { $$=$1; set($$, ID_gcc_float64x); } + | TOK_GCC_FLOAT80 { $$=$1; set($$, ID_gcc_float80); } + | TOK_GCC_FLOAT128 { $$=$1; set($$, ID_gcc_float128); } + | TOK_GCC_FLOAT128X { $$=$1; set($$, ID_gcc_float128x); } + | TOK_GCC_INT128 { $$=$1; set($$, ID_gcc_int128); } | TOK_GCC_DECIMAL32 { $$=$1; set($$, ID_gcc_decimal32); } | TOK_GCC_DECIMAL64 { $$=$1; set($$, ID_gcc_decimal64); } | TOK_GCC_DECIMAL128 { $$=$1; set($$, ID_gcc_decimal128); } diff --git a/src/ansi-c/scanner.l b/src/ansi-c/scanner.l index 05ded108347..9151ea2263f 100644 --- a/src/ansi-c/scanner.l +++ b/src/ansi-c/scanner.l @@ -202,7 +202,7 @@ hexfloat1 "0"[xX]{hexdigit}*"."{hexdigit}+[pP][+-]?{integer} hexfloat2 "0"[xX]{hexdigit}*"."[pP][+-]?{integer} hexfloat3 "0"[xX]{hexdigit}*[pP][+-]?{integer} float_suffix [fFlLiIjJ]* -gcc_ext_float_suffix [wWqQ]|[dD][fFdDlL]? +gcc_ext_float_suffix [wWqQ]|[dD][fFdDlL]?|"f16"|"f32"|"f64"|"f128"|"f32x"|"f64x"|"f128x" float {float1}|{float2}|{float3}|{hexfloat1}|{hexfloat2}|{hexfloat3} float_s {float}{float_suffix}|{integer}[fF] gcc_ext_float_s {float}{gcc_ext_float_suffix} @@ -459,6 +459,41 @@ void ansi_c_scanner_init() return make_identifier(); } +"_Float16" { // clang doesn't have it + if(PARSER.mode==configt::ansi_ct::flavourt::GCC) + { loc(); return TOK_GCC_FLOAT16; } + else + return make_identifier(); + } + +"_Float32" { // clang doesn't have it + if(PARSER.mode==configt::ansi_ct::flavourt::GCC) + { loc(); return TOK_GCC_FLOAT32; } + else + return make_identifier(); + } + +"_Float32x" { // clang doesn't have it + if(PARSER.mode==configt::ansi_ct::flavourt::GCC) + { loc(); return TOK_GCC_FLOAT32X; } + else + return make_identifier(); + } + +"_Float64" { // clang doesn't have it + if(PARSER.mode==configt::ansi_ct::flavourt::GCC) + { loc(); return TOK_GCC_FLOAT64; } + else + return make_identifier(); + } + +"_Float64x" { // clang doesn't have it + if(PARSER.mode==configt::ansi_ct::flavourt::GCC) + { loc(); return TOK_GCC_FLOAT64X; } + else + return make_identifier(); + } + "__float80" { // clang doesn't have it if(PARSER.mode==configt::ansi_ct::flavourt::GCC) { loc(); return TOK_GCC_FLOAT80; } @@ -474,6 +509,13 @@ void ansi_c_scanner_init() return make_identifier(); } +"_Float128x" { // clang doesn't have it + if(PARSER.mode==configt::ansi_ct::flavourt::GCC) + { loc(); return TOK_GCC_FLOAT128X; } + else + return make_identifier(); + } + "__int128" { if(PARSER.mode==configt::ansi_ct::flavourt::GCC || PARSER.mode==configt::ansi_ct::flavourt::APPLE) { loc(); return TOK_GCC_INT128; } diff --git a/src/cpp/cpp_convert_type.cpp b/src/cpp/cpp_convert_type.cpp index e3dfff685d4..1b7bab029eb 100644 --- a/src/cpp/cpp_convert_type.cpp +++ b/src/cpp/cpp_convert_type.cpp @@ -19,6 +19,8 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include +#include + #include "cpp_declaration.h" #include "cpp_name.h" diff --git a/src/util/c_types.cpp b/src/util/c_types.cpp index b02dfdec7e7..78d0ad08238 100644 --- a/src/util/c_types.cpp +++ b/src/util/c_types.cpp @@ -258,27 +258,6 @@ bitvector_typet long_double_type() } } -bitvector_typet gcc_float128_type() -{ - // not same as long double! - - if(config.ansi_c.use_fixed_for_float) - { - fixedbv_typet result; - result.set_width(128); - result.set_integer_bits(128/2); - result.set(ID_C_c_type, ID_gcc_float128); - return result; - } - else - { - floatbv_typet result= - ieee_float_spect::quadruple_precision().to_type(); - result.set(ID_C_c_type, ID_gcc_float128); - return result; - } -} - signedbv_typet pointer_diff_type() { // The pointer-diff type varies. This is signed int on some systems, @@ -309,20 +288,6 @@ typet void_type() return empty_typet(); } -unsignedbv_typet gcc_unsigned_int128_type() -{ - unsignedbv_typet result(128); - result.set(ID_C_c_type, ID_unsigned_int128); - return result; -} - -signedbv_typet gcc_signed_int128_type() -{ - signedbv_typet result(128); - result.set(ID_C_c_type, ID_signed_int128); - return result; -} - std::string c_type_as_string(const irep_idt &c_type) { if(c_type==ID_signed_int) diff --git a/src/util/c_types.h b/src/util/c_types.h index 39e76a6c7b3..b80851ce97a 100644 --- a/src/util/c_types.h +++ b/src/util/c_types.h @@ -32,9 +32,6 @@ unsignedbv_typet char32_t_type(); bitvector_typet float_type(); bitvector_typet double_type(); bitvector_typet long_double_type(); -bitvector_typet gcc_float128_type(); -unsignedbv_typet gcc_unsigned_int128_type(); -signedbv_typet gcc_signed_int128_type(); unsignedbv_typet size_type(); signedbv_typet signed_size_type(); signedbv_typet pointer_diff_type(); diff --git a/src/util/ieee_float.h b/src/util/ieee_float.h index 5c975f3782e..2127c89386a 100644 --- a/src/util/ieee_float.h +++ b/src/util/ieee_float.h @@ -59,6 +59,13 @@ class ieee_float_spect class floatbv_typet to_type() const; + // this is binary16 in IEEE 754-2008 + static ieee_float_spect half_precision() + { + // 16 bits in total + return ieee_float_spect(10, 5); + } + // the well-know standard formats static ieee_float_spect single_precision() { diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index 78ff9b00e16..98fe80ca395 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -308,8 +308,14 @@ IREP_ID_ONE(gcc_builtin_va_arg) IREP_ID_ONE(gcc_builtin_types_compatible_p) IREP_ID_ONE(gcc_builtin_va_arg_next) IREP_ID_ONE(gcc_builtin_va_list) +IREP_ID_ONE(gcc_float16) +IREP_ID_ONE(gcc_float32) +IREP_ID_ONE(gcc_float32x) +IREP_ID_ONE(gcc_float64) +IREP_ID_ONE(gcc_float64x) IREP_ID_ONE(gcc_float80) IREP_ID_ONE(gcc_float128) +IREP_ID_ONE(gcc_float128x) IREP_ID_ONE(gcc_int128) IREP_ID_ONE(gcc_decimal32) IREP_ID_ONE(gcc_decimal64)