new gcc floating-point type identifiers

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

Author: Daniel Kroening

regression/ansi-c/float_constant1/main.c

@@ -10,6 +10,16 @@ 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 only
+#ifdef __GNUC__
+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

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));

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 \

src/ansi-c/ansi_c_convert_type.cpp

@@ -20,6 +20,8 @@ Author: Daniel Kroening, [email protected]
 #include <util/arith_tools.h>
 #include <util/std_types.h>
 
+#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,27 +323,49 @@ 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 ||
        gcc_int128_cnt || bv_cnt ||
        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;
     }
 

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();

src/ansi-c/c_typecheck_type.cpp

@@ -21,6 +21,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "ansi_c_convert_type.h"
 #include "c_qualifiers.h"
+#include "gcc_types.h"
 #include "padding.h"
 #include "type2name.h"
 

src/ansi-c/gcc_types.cpp

@@ -0,0 +1,169 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#include <util/config.h>
+#include <util/c_types.h>
+
+#include "gcc_types.h"
+
+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;
+}

src/ansi-c/gcc_types.h

@@ -0,0 +1,27 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#ifndef CPROVER_ANSI_C_GCC_TYPES_H
+#define CPROVER_ANSI_C_GCC_TYPES_H
+
+#include <util/std_types.h>
+
+// 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