Add support for additional float types

.gitignore

@@ -417,3 +417,4 @@ src/ext/canonicalize/.merlin
 src/ext/cqualann/.merlin
 src/ext/syntacticsearch/.merlin
 src/ext/makecfg/.merlin
+test/a.out

Makefile.in

@@ -164,6 +164,8 @@ $(OBJDIR)/machdep.ml : src/machdep-ml.c configure.ac Makefile.in
 	@echo "  sizeof_longlong: int;   (* Size of \"long long\" *)"   >> $@
 	@echo "  sizeof_ptr: int;        (* Size of pointers *)"        >> $@
 	@echo "  sizeof_float: int;      (* Size of \"float\" *)"       >> $@
+	@echo "  sizeof_float32x: int;   (* Size of \"_Float32x\" *)"   >> $@
+	@echo "  sizeof_float64x: int;   (* Size of \"_Float64x\" *)"   >> $@\
 	@echo "  sizeof_double: int;     (* Size of \"double\" *)"      >> $@
 	@echo "  sizeof_longdouble: int; (* Size of \"long double\" *)" >> $@
 	@echo "  sizeof_floatcomplex: int;      (* Size of \"float _Complex\" *)"       >> $@
@@ -181,6 +183,8 @@ $(OBJDIR)/machdep.ml : src/machdep-ml.c configure.ac Makefile.in
 	@echo "  alignof_ptr: int;       (* Alignment of pointers *)"   >> $@
 	@echo "  alignof_enum: int;      (* Alignment of enum types *)" >> $@
 	@echo "  alignof_float: int;     (* Alignment of \"float\" *)"  >> $@
+	@echo "  alignof_float32x: int;  (* Alignment of \"_Float32x\" *)"  >> $@
+	@echo "  alignof_float64x: int;  (* Alignment of \"_Float64x\" *)"  >> $@
 	@echo "  alignof_double: int;    (* Alignment of \"double\" *)" >> $@
 	@echo "  alignof_longdouble: int;  (* Alignment of \"long double\" *)" >> $@
 	@echo "  alignof_floatcomplex: int;     (* Alignment of \"float _Complex\" *)"  >> $@

src/frontc/cabs.ml

@@ -67,7 +67,11 @@ type typeSpecifier = (* Merge all specifiers into one type *)
   | Tint64 (* TODO needed? *)
   | Tint128 (* TODO needed? *)
   | Tfloat
+  | Tfloat32
+  | Tfloat64
   | Tfloat128 (* TODO needed? *)
+  | Tfloat32x
+  | Tfloat64x
   | Tdouble
   | Tsigned
   | Tsizet    (* used temporarily to translate offsetof() *)

src/frontc/cabs2cil.ml

@@ -2457,11 +2457,61 @@ let rec doSpecList (suggestedAnonName: string) (* This string will be part of
     | [A.Tunsigned; A.Tint128] -> TInt(IUInt128, [])
 
     | [A.Tfloat] -> TFloat(FFloat, [])
+    | [A.Tfloat32] ->
+      if !Machdep.theMachine.Machdep.sizeof_float = 4 then
+        TFloat(FFloat, [])
+      else
+        E.s (error "float32 only supported on machines where it is an alias for float")
+    | [A.Tfloat32x] ->
+      if !Machdep.theMachine.Machdep.sizeof_float32x = !Machdep.theMachine.Machdep.sizeof_float &&
+         !Machdep.theMachine.Machdep.alignof_float32x = !Machdep.theMachine.Machdep.alignof_float
+      then
+        TFloat(FFloat, [])
+      else if !Machdep.theMachine.Machdep.sizeof_float32x = !Machdep.theMachine.Machdep.sizeof_double &&
+        !Machdep.theMachine.Machdep.alignof_float32x = !Machdep.theMachine.Machdep.alignof_double
+      then
+        TFloat(FDouble, [])
+      else
+        E.s (error "float32x only supported on machines where it is an alias for a conventional type: size: %i align: %i "
+          !Machdep.theMachine.Machdep.sizeof_float32x
+          !Machdep.theMachine.Machdep.alignof_float32x
+          )
+
     | [A.Tdouble] -> TFloat(FDouble, [])
+    | [A.Tfloat64] ->
+      if !Machdep.theMachine.Machdep.sizeof_double = 8 then
+        TFloat(FDouble, [])
+      else
+        E.s (error "float64 only supported on machines where it is an alias for double")
+    | [A.Tfloat64x] ->
+      if !Machdep.theMachine.Machdep.sizeof_float64x = !Machdep.theMachine.Machdep.sizeof_float &&
+          !Machdep.theMachine.Machdep.alignof_float64x = !Machdep.theMachine.Machdep.alignof_float
+      then
+        TFloat(FFloat, [])
+      else if !Machdep.theMachine.Machdep.sizeof_float64x = !Machdep.theMachine.Machdep.sizeof_double &&
+        !Machdep.theMachine.Machdep.alignof_float64x = !Machdep.theMachine.Machdep.alignof_double
+      then
+        TFloat(FDouble, [])
+      else if !Machdep.theMachine.Machdep.sizeof_float64x = !Machdep.theMachine.Machdep.sizeof_longdouble &&
+        !Machdep.theMachine.Machdep.alignof_float64x = !Machdep.theMachine.Machdep.alignof_longdouble
+      then
+        TFloat(FLongDouble, [])
+      else
+        E.s (error "float64x only supported on machines where it is an alias for a conventional type: size: %i align: %i "
+          !Machdep.theMachine.Machdep.sizeof_float64x
+          !Machdep.theMachine.Machdep.alignof_float64x
+          )
 
     | [A.Tlong; A.Tdouble] -> TFloat(FLongDouble, [])
-    | [A.Tfloat128] -> TFloat(FLongDouble, []) (* TODO: Correct? *)
-
+    | [A.Tfloat128] ->
+      (* This is only correct w.r.t. to size and align. If we analyze floats, we need to be careful here *)
+      if !Machdep.theMachine.Machdep.sizeof_longdouble = 16 && !Machdep.theMachine.Machdep.alignof_longdouble = 16 then
+        TFloat(FLongDouble, [])
+      else
+        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 "
+        !Machdep.theMachine.Machdep.sizeof_longdouble
+        !Machdep.theMachine.Machdep.alignof_longdouble
+        )
      (* Now the other type specifiers *)
     | [A.Tdefault] -> E.s (error "Default outside generic associations")
     | [A.Tnamed n] -> begin

src/frontc/clexer.mll

@@ -139,6 +139,10 @@ let init_lexicon _ =
       ("float", fun loc -> FLOAT loc);
       ("__float128", fun loc -> FLOAT128 loc);
       ("_Float128", fun loc -> FLOAT128 loc);
+      ("_Float32", fun loc -> FLOAT32 loc);
+      ("_Float64", fun loc -> FLOAT64 loc);
+      ("_Float32x", fun loc -> FLOAT32X loc);
+      ("_Float64x", fun loc -> FLOAT64X loc);
       ("double", fun loc -> DOUBLE loc);
       ("void", fun loc -> VOID loc);
       ("enum", fun loc -> ENUM loc);

src/frontc/cparser.mly

@@ -252,6 +252,8 @@ let transformOffsetOf (speclist, dtype) member =
 %token EOF
 %token<Cabs.cabsloc> CHAR INT BOOL DOUBLE FLOAT VOID INT64 INT32
 %token<Cabs.cabsloc> INT128 FLOAT128 COMPLEX /* C99 */
+%token<Cabs.cabsloc> FLOAT32 FLOAT64 /* FloatN */
+%token<Cabs.cabsloc> FLOAT32X FLOAT64X /* FloatNx */
 %token<Cabs.cabsloc> GENERIC NORETURN /* C11 */
 %token<Cabs.cabsloc> ENUM STRUCT TYPEDEF UNION
 %token<Cabs.cabsloc> SIGNED UNSIGNED LONG SHORT
@@ -981,7 +983,11 @@ type_spec:   /* ISO 6.7.2 */
 |   INT64           { Tint64, $1 }
 |   INT128          { Tint128, $1 }
 |   FLOAT           { Tfloat, $1 }
+|   FLOAT32         { Tfloat32, $1 }
+|   FLOAT64         { Tfloat64, $1 }
 |   FLOAT128        { Tfloat128, $1 }
+|   FLOAT32X        { Tfloat32x, $1 }
+|   FLOAT64X        { Tfloat64x, $1 }
 |   DOUBLE          { Tdouble, $1 }
 /* |   COMPLEX FLOAT   { Tfloat, $2 } */
 /* |   COMPLEX FLOAT128{ Tfloat128, $2 } */

src/frontc/cprint.ml

@@ -167,7 +167,11 @@ and print_type_spec = function
   | Tint64 -> print "__int64 "
   | Tint128 -> print "__int128 "
   | Tfloat -> print "float "
+  | Tfloat32 -> print "_Float32"
+  | Tfloat64 -> print "_Float64"
   | Tfloat128 -> print "__float128"
+  | Tfloat32x -> print "_Float32x"
+  | Tfloat64x -> print "_Float64x"
   | Tdouble -> print "double "
   | Tsigned -> printu "signed"
   | Tunsigned -> print "unsigned "

src/machdep-ml.c.in

@@ -1,11 +1,11 @@
 /*
  *
- * Copyright (c) 2001-2002, 
+ * Copyright (c) 2001-2002,
  *  George C. Necula    <necula@cs.berkeley.edu>
  *  Scott McPeak        <smcpeak@cs.berkeley.edu>
  *  Wes Weimer          <weimer@cs.berkeley.edu>
  * All rights reserved.
- * 
+ *
  * Redistribution and use in source and binary forms, with or without
  * modification, are permitted provided that the following conditions are
  * met:
@@ -91,7 +91,7 @@ int main(int argc, char **argv)
 {
   int env = argc == 2 && !strcmp(argv[1], "--env");
   int alignof_short, alignof_int, alignof_long, alignof_ptr, alignof_enum,
-    alignof_float, alignof_double, alignof_longdouble,
+    alignof_float, alignof_float32x, alignof_float64x, alignof_double, alignof_longdouble,
     alignof_floatcomplex, alignof_doublecomplex, alignof_longdoublecomplex,
     sizeof_fun,
     alignof_fun, alignof_str, alignof_aligned, alignof_longlong,
@@ -114,7 +114,7 @@ int main(int argc, char **argv)
     };
     alignof_int = (intptr_t)(&((struct intstruct*)0)->i);
   }
-  
+
   // The alignment of a bool
   {
     struct boolstruct {
@@ -123,7 +123,7 @@ int main(int argc, char **argv)
     };
     alignof_bool = (intptr_t)(&((struct boolstruct*)0)->b);
   }
-  
+
   // The alignment of a long
   {
     struct longstruct {
@@ -132,7 +132,7 @@ int main(int argc, char **argv)
     };
     alignof_long = (intptr_t)(&((struct longstruct*)0)->l);
   }
-    
+
   // The alignment of long long
   {
     struct longlong {
@@ -145,7 +145,7 @@ int main(int argc, char **argv)
   // The alignment of a ptr
   {
     struct ptrstruct {
-      char c; 
+      char c;
       int * p;
     };
     alignof_ptr = (intptr_t)(&((struct ptrstruct*)0)->p);
@@ -154,12 +154,12 @@ int main(int argc, char **argv)
   // The alignment of an enum
   {
     struct enumstruct {
-      char c; 
+      char c;
       enum e2 { THREE, FOUR, FIVE } e;
     };
     alignof_enum = (intptr_t)(&((struct enumstruct*)0)->e);
   }
-    
+
   // The alignment of a float
   {
     struct floatstruct {
@@ -168,15 +168,33 @@ int main(int argc, char **argv)
     };
     alignof_float = (intptr_t)(&((struct floatstruct*)0)->f);
   }
-
+
+  // The alignment of a _Float32x
+  {
+    struct floatstruct {
+      char c;
+      _Float32x f;
+    };
+    alignof_float32x = (intptr_t)(&((struct floatstruct*)0)->f);
+  }
+
+  // The alignment of a _Float64x
+  {
+    struct floatstruct {
+      char c;
+      _Float64x f;
+    };
+    alignof_float64x = (intptr_t)(&((struct floatstruct*)0)->f);
+  }
+
   // The alignment of double
   {
     struct s1 {
       char c;
       double d;
     };
     alignof_double = (intptr_t)(&((struct s1*)0)->d);
-  }    
+  }
 
   // The alignment of long  double
   {
@@ -185,8 +203,8 @@ int main(int argc, char **argv)
       long double ld;
     };
     alignof_longdouble = (intptr_t)(&((struct s1*)0)->ld);
-  }    
-    
+  }
+
   // The alignment of a float complex
   {
     struct floatstruct {
@@ -250,21 +268,24 @@ int main(int argc, char **argv)
     {
       fprintf(stderr, "Generating CIL_MACHINE machine dependency information string (for CIL)\n");
       printf("short=%d,%d int=%d,%d long=%d,%d long_long=%d,%d pointer=%d,%d "
-	     "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 "
+	     "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 "
 	     "bool=%d,%d fun=%d,%d alignof_string=%d max_alignment=%d size_t=%s "
 	     "wchar_t=%s char_signed=%s "
 	     "big_endian=%s __thread_is_keyword=%s __builtin_va_list=%s "
 	     "underscore_name=%s\n",
 	     (int)sizeof(short), alignof_short, (int)sizeof(int), alignof_int,
-	     (int)sizeof(long), alignof_long, (int)sizeof(long long), alignof_longlong, 
-	     (int)sizeof(int *), alignof_ptr, alignof_enum,
-	     (int)sizeof(float), alignof_float, (int)sizeof(double), alignof_double, 
+	     (int)sizeof(long), alignof_long, (int)sizeof(long long), alignof_longlong,
+	     (int)sizeof(int *), alignof_ptr,
+	     alignof_enum,
+	     (int)sizeof(_Float32x), alignof_float32x,
+	     (int)sizeof(_Float64x), alignof_float64x,
+	     (int)sizeof(float), alignof_float, (int)sizeof(double), alignof_double,
 	     (int)sizeof(long double), alignof_longdouble, (int)sizeof(float _Complex), alignof_floatcomplex, (int)sizeof(double _Complex), alignof_doublecomplex,
 	     (int)sizeof(long double _Complex), alignof_longdoublecomplex, (int)sizeof(void),
 	     (int)sizeof(bool), alignof_bool,
-	     sizeof_fun, alignof_fun, alignof_str, alignof_aligned, 
-	     underscore(TYPE_SIZE_T), underscore(TYPE_WCHAR_T), 
-	     char_is_unsigned ? "false" : "true", 
+	     sizeof_fun, alignof_fun, alignof_str, alignof_aligned,
+	     underscore(TYPE_SIZE_T), underscore(TYPE_WCHAR_T),
+	     char_is_unsigned ? "false" : "true",
 	     little_endian ? "false" : "true",
 	     THREAD_IS_KEYWORD, HAVE_BUILTIN_VA_LIST, UNDERSCORE_NAME);
     }
@@ -285,6 +306,8 @@ int main(int argc, char **argv)
       printf("\t sizeof_longlong            = %d;\n", (int)sizeof(LONGLONG));
       printf("\t sizeof_ptr                 = %d;\n", (int)sizeof(int *));
       printf("\t sizeof_float               = %d;\n", (int)sizeof(float));
+      printf("\t sizeof_float32x            = %d;\n", (int)sizeof(_Float32x));
+      printf("\t sizeof_float64x            = %d;\n", (int)sizeof(_Float64x));
       printf("\t sizeof_double              = %d;\n", (int)sizeof(double));
       printf("\t sizeof_longdouble          = %d;\n", (int)sizeof(long double));
       printf("\t sizeof_floatcomplex        = %d;\n", (int)sizeof(float _Complex));
@@ -302,6 +325,8 @@ int main(int argc, char **argv)
       printf("\t alignof_ptr                = %d;\n", alignof_ptr);
       printf("\t alignof_enum               = %d;\n", alignof_enum);
       printf("\t alignof_float              = %d;\n", alignof_float);
+      printf("\t alignof_float32x           = %d;\n", alignof_float32x);
+      printf("\t alignof_float64x           = %d;\n", alignof_float64x);
       printf("\t alignof_double             = %d;\n", alignof_double);
       printf("\t alignof_longdouble         = %d;\n", alignof_longdouble);
       printf("\t alignof_floatcomplex       = %d;\n", alignof_floatcomplex);
@@ -317,4 +342,4 @@ int main(int argc, char **argv)
       printf("\t little_endian              = %s;\n", little_endian ? "true" : "false");
     }
   return 0;
-} 
+}

src/machdepenv.ml

@@ -9,7 +9,7 @@ let preparse (s:string) : (string, string list) H.t =
   let spaceRegexp = R.regexp "[ \t]+" in
   let specRegexp = R.regexp "^\\([a-zA-Z_0-9]+\\)[ \t]*=\\(.*\\)$" in
   let specs = R.split spaceRegexp s in
-  let addSpec spec = 
+  let addSpec spec =
     if R.string_match specRegexp spec 0 then begin
       let name = R.matched_group 1 spec in
       let value = R.matched_group 2 spec in
@@ -22,19 +22,19 @@ let preparse (s:string) : (string, string list) H.t =
   specTable
 
 let errorWrap name f =
-  try 
+  try
     f name
   with Not_found -> raise (Failure (name ^ " not specified"))
   | _ -> raise (Failure ("invalid format for " ^ name))
 
-let getNthString n specTable name = 
+let getNthString n specTable name =
   let l = H.find specTable name in
   L.nth l n
 
 let getNthInt n specTable name =
   errorWrap name (fun name -> int_of_string (getNthString n specTable name))
 
-let getNthBool n specTable name = 
+let getNthBool n specTable name =
   errorWrap name (fun name -> bool_of_string (getNthString n specTable name))
 
 let getBool = getNthBool 0
@@ -44,10 +44,10 @@ let getAlignof = getNthInt 1
 
 let respace = Str.global_replace (Str.regexp "_") " "
 
-let modelParse (s:string) : mach = 
+let modelParse (s:string) : mach =
   let entries =
     try
-      preparse s 
+      preparse s
     with Failure msg -> raise (Failure msg)
     | _ -> raise (Failure "invalid machine specification")
   in
@@ -71,6 +71,10 @@ let modelParse (s:string) : mach =
     alignof_enum = getInt entries "alignof_enum";
     sizeof_float = getSizeof entries "float";
     alignof_float = getAlignof entries "float";
+    sizeof_float32x = getSizeof entries "float32x";
+    alignof_float32x = getAlignof entries "float32x";
+    sizeof_float64x = getSizeof entries "float64x";
+    alignof_float64x = getAlignof entries "float64x";
     sizeof_floatcomplex = getSizeof entries "float_complex";
     alignof_floatcomplex = getAlignof entries "float_complex";
     sizeof_double = getSizeof entries "double";

test/small1/c11-extendedFloat.c

@@ -0,0 +1,20 @@
+// Technically not C11 but ISO/IEC TS 18661-3:2015
+#include "testharness.h"
+
+_Float32 f32;
+_Float64 f64;
+_Float32x f32x;
+_Float64x f64x;
+
+
+int main() {
+    if(sizeof(f32) != 4) {
+        E(1);
+    }
+
+    if(sizeof(f64) != 8) {
+        E(2);
+    }
+
+    SUCCESS;
+}