Merge pull request #119 from goblint/issue_118

Add support on machines where long double and float128 do not have the same size

src/cil.ml

@@ -308,9 +308,11 @@ and fkind =
     FFloat              (** [float] *)
   | FDouble             (** [double] *)
   | FLongDouble         (** [long double] *)
+  | FFloat128           (** [float128] *)
   | FComplexFloat       (** [float _Complex] *)
   | FComplexDouble      (** [double _Complex] *)
   | FComplexLongDouble  (** [long double _Complex]*)
+  | FComplexFloat128    (** [_float128 _Complex]*)
 
 (** An attribute has a name and some optional parameters *)
 and attribute = Attr of string * attrparam list
@@ -1660,9 +1662,11 @@ let typeOfRealAndImagComponents t =
       | FFloat -> FFloat      (* [float] *)
       | FDouble -> FDouble     (* [double] *)
       | FLongDouble -> FLongDouble (* [long double] *)
+      | FFloat128 -> FFloat128
       | FComplexFloat -> FFloat
       | FComplexDouble -> FDouble
       | FComplexLongDouble -> FLongDouble
+      | FComplexFloat128 -> FFloat128
     in
     TFloat (newfkind fkind, attrs)
   | _ -> E.s (E.bug "unexpected non-numerical type for argument to __real__/__imag__ ")
@@ -1672,9 +1676,11 @@ let getComplexFkind = function
   | FFloat -> FComplexFloat
   | FDouble -> FComplexDouble
   | FLongDouble -> FComplexLongDouble
+  | FFloat128 -> FComplexFloat128
   | FComplexFloat -> FComplexFloat
   | FComplexDouble -> FComplexDouble
   | FComplexLongDouble -> FComplexLongDouble
+  | FComplexFloat128 -> FComplexFloat128
 
 let var vi : lval = (Var vi, NoOffset)
 (* let assign vi e = Instrs(Set (var vi, e), lu) *)
@@ -1746,9 +1752,11 @@ let d_fkind () = function
     FFloat -> text "float"
   | FDouble -> text "double"
   | FLongDouble -> text "long double"
+  | FFloat128 -> text "_Float128"
   | FComplexFloat -> text "_Complex float"
   | FComplexDouble -> text "_Complex double"
   | FComplexLongDouble -> text "_Complex long double"
+  | FComplexFloat128 -> text "_Complex _Float128"
 
 let d_storage () = function
     NoStorage -> nil
@@ -1844,9 +1852,11 @@ let d_const () c =
          FFloat -> chr 'f'
        | FDouble -> nil
        | FLongDouble -> chr 'L'
+       | FFloat128 -> text "F128"
        | FComplexFloat -> text "iF"
        | FComplexDouble -> chr 'i'
-       | FComplexLongDouble -> text "iL")
+       | FComplexLongDouble -> text "iL"
+       | FComplexFloat128 -> text "iF128")
   | CEnum(_, s, ei) -> text s
 
 
@@ -2093,6 +2103,7 @@ let floatKindForSize (s:int) =
   if s = !M.theMachine.M.sizeof_double then FDouble
   else if s = !M.theMachine.M.sizeof_float then FFloat
   else if s = !M.theMachine.M.sizeof_longdouble then FLongDouble
+  else if s = !M.theMachine.M.sizeof_float128 then FFloat128
   else raise Not_found
 
 (* Represents an integer as for a given kind.  Returns a flag saying
@@ -2251,9 +2262,11 @@ let rec alignOf_int t =
     | TFloat(FFloat, _) -> !M.theMachine.M.alignof_float
     | TFloat(FDouble, _) -> !M.theMachine.M.alignof_double
     | TFloat(FLongDouble, _) -> !M.theMachine.M.alignof_longdouble
+    | TFloat(FFloat128, _) -> !M.theMachine.M.alignof_float128
     | TFloat(FComplexFloat, _) -> !M.theMachine.M.alignof_floatcomplex
     | TFloat(FComplexDouble, _) -> !M.theMachine.M.alignof_doublecomplex
     | TFloat(FComplexLongDouble, _) -> !M.theMachine.M.alignof_longdoublecomplex
+    | TFloat(FComplexFloat128, _) -> !M.theMachine.M.alignof_float128complex
     | TNamed (t, _) -> alignOf_int t.ttype
     | TArray (t, _, _) -> alignOf_int t
     | TPtr _ | TBuiltin_va_list _ -> !M.theMachine.M.alignof_ptr
@@ -2407,9 +2420,11 @@ and bitsSizeOf t =
   | TInt (ik,_) -> 8 * (bytesSizeOfInt ik)
   | TFloat(FDouble, _) -> 8 * !M.theMachine.M.sizeof_double
   | TFloat(FLongDouble, _) -> 8 * !M.theMachine.M.sizeof_longdouble
+  | TFloat(FFloat128, _) -> 8 * !M.theMachine.M.sizeof_float128
   | TFloat(FFloat, _) -> 8 * !M.theMachine.M.sizeof_float
   | TFloat(FComplexDouble, _) ->  8 * !M.theMachine.M.sizeof_doublecomplex
   | TFloat(FComplexLongDouble, _) -> 8 * !M.theMachine.M.sizeof_longdoublecomplex
+  | TFloat(FComplexFloat128, _) -> 8 * !M.theMachine.M.sizeof_float128complex
   | TFloat(FComplexFloat, _) -> 8 * !M.theMachine.M.sizeof_floatcomplex
   | TEnum (ei, _) -> bitsSizeOf (TInt(ei.ekind, []))
   | TPtr _ -> 8 * !M.theMachine.M.sizeof_ptr

src/cil.mli

@@ -295,9 +295,11 @@ and fkind =
     FFloat              (** [float] *)
   | FDouble             (** [double] *)
   | FLongDouble         (** [long double] *)
+  | FFloat128           (** [float128] *)
   | FComplexFloat       (** [float _Complex] *)
   | FComplexDouble      (** [double _Complex] *)
   | FComplexLongDouble  (** [long double _Complex]*)
+  | FComplexFloat128    (** [_float128 _Complex]*)
 
 (** {b Attributes.} *)
 

src/frontc/cabs2cil.ml

@@ -1309,10 +1309,14 @@ let arithmeticConversion    (* c.f. ISO 6.3.1.8 *)
     (t2: typ) : typ =
   let resultingFType fkind1 t1 fkind2 t2 =
     (* t1 and t2 are the original types before unrollType, so TNamed is preserved if possible *)
-    let isComplex f = f = FComplexFloat || f = FComplexDouble || f = FComplexLongDouble in
+    let isComplex f = f = FComplexFloat || f = FComplexDouble || f = FComplexLongDouble || f = FComplexFloat128 in
     match fkind1, fkind2 with
+    | FComplexFloat128, _ -> t1
+    | _, FComplexFloat128 -> t2
     | FComplexLongDouble, _ -> t1
     | _, FComplexLongDouble -> t2
+    | FFloat128, other -> if isComplex other then TFloat(FComplexFloat128, []) else t1
+    | other, FFloat128 -> if isComplex other then TFloat(FComplexFloat128, []) else t2
     | FLongDouble, other -> if isComplex other then TFloat(FComplexLongDouble, []) else t1
     | other, FLongDouble -> if isComplex other then TFloat(FComplexLongDouble, []) else t2
     | FComplexDouble, other -> t1
@@ -2558,15 +2562,7 @@ let rec doSpecList (suggestedAnonName: string) (* This string will be part of
           )
 
     | [A.Tlong; A.Tdouble] -> TFloat(FLongDouble, [])
-    | [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
-        )
+    | [A.Tfloat128] -> TFloat(FFloat128, [])
      (* Now the other type specifiers *)
     | [A.Tdefault] -> E.s (error "Default outside generic associations")
     | [A.Tnamed n] -> begin
@@ -3681,7 +3677,11 @@ and doExp (asconst: bool)   (* This expression is used as a constant *)
             (* Maybe it ends in U or UL. Strip those *)
             let l = String.length str in
             let baseint, kind =
-              if hasSuffix str "L" then
+              if hasSuffix str "F128" then
+                String.sub str 0 (l - 4), FFloat128
+              else if hasSuffix str "Q" then
+                String.sub str 0 (l - 1), FFloat128
+              else if hasSuffix str "L" then
                 String.sub str 0 (l - 1), FLongDouble
               else if hasSuffix str "F" then
                 String.sub str 0 (l - 1), FFloat
@@ -3690,10 +3690,10 @@ and doExp (asconst: bool)   (* This expression is used as a constant *)
               else
                 str, FDouble
             in
-            if kind = FLongDouble then
+            if kind = FLongDouble || kind = FFloat128 then
               (* We only have 64-bit values in Ocaml *)
-              E.log "treating long double constant %s as double constant at %a.\n"
-                str d_loc !currentLoc;
+              E.log "treating %a constant %s as double constant at %a (only relevant if first argument of CReal is used).\n"
+                d_fkind kind str d_loc !currentLoc;
             try
               finishExp empty
                 (Const(CReal(float_of_string baseint, kind,
@@ -3711,7 +3711,11 @@ and doExp (asconst: bool)   (* This expression is used as a constant *)
             (* Maybe it ends in U or UL. Strip those *)
             let l = String.length str in
             let baseint, kind =
-              if hasSuffix str "iL" || hasSuffix str "Li" then
+              if hasSuffix str "iF128" || hasSuffix str "F128i" then
+                String.sub str 0 (l - 5), FComplexFloat128
+              else if hasSuffix str "Qi" || hasSuffix str "iQ" then
+                String.sub str 0 (l - 2), FComplexFloat128
+              else if hasSuffix str "iL" || hasSuffix str "Li" then
                 String.sub str 0 (l - 2), FComplexLongDouble
               else if hasSuffix str "iF" || hasSuffix str "Fi" then
                 String.sub str 0 (l - 2), FComplexFloat
@@ -3720,10 +3724,6 @@ and doExp (asconst: bool)   (* This expression is used as a constant *)
               else (* A.CONST_COMPLEX always has the suffix i *)
                 String.sub str 0 (l - 1), FComplexDouble
             in
-            if kind = FLongDouble then
-              (* We only have 64-bit values in Ocaml *)
-              E.log "treating long double constant %s as double constant at %a.\n"
-                str d_loc !currentLoc;
             try
               finishExp empty
                 (Const(CReal(float_of_string baseint, kind,
@@ -3799,10 +3799,12 @@ and doExp (asconst: bool)   (* This expression is used as a constant *)
           match fkind with
           | FFloat
           | FDouble
-          | FLongDouble -> 8
+          | FLongDouble
+          | FFloat128 -> 8
           | FComplexFloat
           | FComplexDouble
-          | FComplexLongDouble -> 9
+          | FComplexLongDouble
+          | FComplexFloat128 -> 9
           end
         | TEnum _ -> 3
         | TPtr _ -> 5
@@ -4468,7 +4470,7 @@ and doExp (asconst: bool)   (* This expression is used as a constant *)
                             (* if the t we determined here is complex, but the return types of all the fptrs are not, the return *)
                             (* type should not be complex *)
                             let isComplex t = match t with
-                              | TFloat(f, _) -> f = FComplexFloat || f = FComplexDouble || f = FComplexLongDouble
+                              | TFloat(f, _) -> f = FComplexFloat || f = FComplexDouble || f = FComplexLongDouble || f = FComplexFloat128
                               | _ -> false
                             in
                             if List.for_all (fun x -> not (isComplex x)) retTypes then

src/frontc/clexer.mll

@@ -453,7 +453,7 @@ let binexponent = ['p' 'P'] ['+' '-']? decdigit+
 let hexfloat = hexprefix hexfraction binexponent
              | hexprefix hexdigit+   binexponent
 
-let floatsuffix = ['f' 'F' 'l' 'L']
+let floatsuffix = ['f' 'F' 'l' 'L' 'q' 'Q'] | "f128" | "F128"
 let floatnum = (decfloat | hexfloat) floatsuffix?
 
 let complexnum = (decfloat | hexfloat) ((['i' 'I'] floatsuffix) | (floatsuffix? ['i' 'I']))

src/machdep-ml.c

@@ -106,8 +106,8 @@ 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_float32x, alignof_float64x, alignof_double, alignof_longdouble,
-    alignof_floatcomplex, alignof_doublecomplex, alignof_longdoublecomplex,
+    alignof_float, alignof_float32x, alignof_float64x, alignof_double, alignof_longdouble, alignof_float128,
+    alignof_floatcomplex, alignof_doublecomplex, alignof_longdoublecomplex, alignof_float128complex,
     sizeof_fun,
     alignof_fun, alignof_str, alignof_aligned, alignof_longlong,
     little_endian, char_is_unsigned, alignof_bool;
@@ -222,6 +222,15 @@ int main(int argc, char **argv)
     alignof_longdouble = (intptr_t)(&((struct s1*)0)->ld);
   }
 
+  // The alignment of float128
+  {
+    struct s1 {
+      char c;
+      _Float128 ld;
+    };
+    alignof_float128 = (intptr_t)(&((struct s1*)0)->ld);
+  }
+
   // The alignment of a float complex
   {
     struct floatstruct {
@@ -249,6 +258,16 @@ int main(int argc, char **argv)
     alignof_longdoublecomplex = (intptr_t)(&((struct s1*)0)->ld);
   }
 
+  // The alignment of float128 complex
+  {
+    struct s1 {
+      char c;
+      _Float128 _Complex ld;
+    };
+    alignof_float128complex = (intptr_t)(&((struct s1*)0)->ld);
+  }
+
+
   alignof_str = __alignof("a string");
   alignof_fun = __alignof(main);
 
@@ -285,7 +304,7 @@ 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 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 "
+	     "alignof_enum=%d float=%d,%d float32x=%d,%d float64x=%d,%d double=%d,%d long_double=%d,%d float128=%d,%d float_complex=%d,%d double_complex=%d,%d long_double_complex=%d,%d float128_complex=%d,%d void=%d "
 	     "bool=%d,%d fun=%d,%d alignof_string=%d max_alignment=%d size_t=%s "
 	     "wchar_t=%s char16_t=%s char32_t=%s char_signed=%s "
 	     "big_endian=%s __thread_is_keyword=%s __builtin_va_list=%s "
@@ -301,8 +320,12 @@ int main(int argc, char **argv)
              0, 0,
 #endif
 	     (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(long double), alignof_longdouble,
+      (int)sizeof(_Float128), alignof_float128,
+       (int)sizeof(float _Complex), alignof_floatcomplex, (int)sizeof(double _Complex), alignof_doublecomplex,
+	     (int)sizeof(long double _Complex), alignof_longdoublecomplex,
+       (int)sizeof(_Float128 _Complex), alignof_float128complex,
+       (int)sizeof(void),
 	     (int)sizeof(bool), alignof_bool,
 	     sizeof_fun, alignof_fun, alignof_str, alignof_aligned,
 	     underscore(TYPE_SIZE_T), underscore(TYPE_WCHAR_T), underscore(TYPE_CHAR16_T), underscore(TYPE_CHAR32_T),
@@ -335,9 +358,11 @@ int main(int argc, char **argv)
 #endif
       printf("\t sizeof_double              = %d;\n", (int)sizeof(double));
       printf("\t sizeof_longdouble          = %d;\n", (int)sizeof(long double));
+      printf("\t sizeof_float128            = %d;\n", (int)sizeof(_Float128));
       printf("\t sizeof_floatcomplex        = %d;\n", (int)sizeof(float _Complex));
       printf("\t sizeof_doublecomplex       = %d;\n", (int)sizeof(double _Complex));
       printf("\t sizeof_longdoublecomplex   = %d;\n", (int)sizeof(long double _Complex));
+      printf("\t sizeof_float128complex     = %d;\n", (int)sizeof(_Float128 _Complex));
       printf("\t sizeof_void                = %d;\n", (int)sizeof(void));
       printf("\t sizeof_fun                 = %d;\n", (int)sizeof_fun);
       printf("\t size_t                     = \"%s\";\n", TYPE_SIZE_T);
@@ -360,9 +385,11 @@ int main(int argc, char **argv)
 #endif
       printf("\t alignof_double             = %d;\n", alignof_double);
       printf("\t alignof_longdouble         = %d;\n", alignof_longdouble);
+      printf("\t alignof_float128           = %d;\n", alignof_float128);
       printf("\t alignof_floatcomplex       = %d;\n", alignof_floatcomplex);
       printf("\t alignof_doublecomplex      = %d;\n", alignof_doublecomplex);
       printf("\t alignof_longdoublecomplex  = %d;\n", alignof_longdoublecomplex);
+      printf("\t alignof_float128complex    = %d;\n", alignof_float128complex);
       printf("\t alignof_str                = %d;\n", alignof_str);
       printf("\t alignof_fun                = %d;\n", alignof_fun);
       printf("\t alignof_aligned            = %d;\n", alignof_aligned);

src/machdep.cppo.ml

@@ -15,9 +15,11 @@ type mach = {
   sizeof_float64x: int;   (* Size of "_Float64x" *)
   sizeof_double: int;     (* Size of "double" *)
   sizeof_longdouble: int; (* Size of "long double" *)
+  sizeof_float128: int;   (* Size of "_Float128" *)
   sizeof_floatcomplex: int;      (* Size of "float _Complex" *)
   sizeof_doublecomplex: int;     (* Size of "double _Complex" *)
   sizeof_longdoublecomplex: int; (* Size of "long double _Complex" *)
+  sizeof_float128complex: int; (* Size of "_Float128 _Complex" *)
   sizeof_void: int;       (* Size of "void" *)
   sizeof_fun: int;        (* Size of function *)
   size_t: string;         (* Type of "sizeof(T)" *)
@@ -36,9 +38,11 @@ type mach = {
   alignof_float64x: int;  (* Alignment of "_Float64x" *)
   alignof_double: int;    (* Alignment of "double" *)
   alignof_longdouble: int;  (* Alignment of "long double" *)
+  alignof_float128: int;  (* Alignment of "_Float128" *)
   alignof_floatcomplex: int;     (* Alignment of "float _Complex" *)
   alignof_doublecomplex: int;    (* Alignment of "double _Complex" *)
   alignof_longdoublecomplex: int;  (* Alignment of "long double _Complex" *)
+  alignof_float128complex: int;  (* Alignment of "_Float128 _Complex" *)
   alignof_str: int;       (* Alignment of strings *)
   alignof_fun: int;       (* Alignment of function *)
   alignof_aligned: int;   (* Alignment of anything with the "aligned" attribute *)

src/machdepenv.ml

@@ -83,8 +83,12 @@ let modelParse (s:string) : mach =
     alignof_doublecomplex = getAlignof entries "double_complex";
     sizeof_longdouble = getSizeof entries "long_double";
     alignof_longdouble = getAlignof entries "long_double";
+    sizeof_float128 = getSizeof entries "float128";
+    alignof_float128 = getAlignof entries "float128";
     sizeof_longdoublecomplex = getSizeof entries "long_double_complex";
     alignof_longdoublecomplex = getAlignof entries "long_double_complex";
+    sizeof_float128complex = getSizeof entries "float128_complex";
+    alignof_float128complex = getAlignof entries "float128_complex";
     sizeof_void = getSizeof entries "void";
     sizeof_fun = getSizeof entries "fun";
     alignof_fun = getAlignof entries "fun";

test/small1/float3.c

@@ -0,0 +1,14 @@
+#include <stdio.h>
+#include <string.h>
+int main() {
+  _Float128 f = 0.0q;
+  _Float128 g = 0.0F128;
+  _Float128 h = 0.0f128;
+  _Float128 i = 0.0Q;
+
+  _Complex _Float128 f1 = 0.0qi;
+  _Complex _Float128 g1 = 0.0iF128;
+  _Complex _Float128 h1 = 0.0f128i;
+  _Complex _Float128 i1 = 0.0iQ;
+  return 0;
+}

test/testcil.pl

@@ -272,6 +272,7 @@ sub addToGroup {
 addBadComment("test/globals2", "Bug. we print array size expressions that refer to variables that haven't been defined yet.");
 addTest("testrun/float");
 addTest("testrun/float2 ");
+addTest("test/float3 ");
 addTest("test/huff1");
 addTest("testrun/init");
 addTest("testrun/init1");