Merge pull request #193 from goblint/float16

sim642 · web-flow · commit 95aa21ca33d8 · 2025-09-02T16:44:09.000+03:00
Add `_Float16` support
diff --git a/src/cil.ml b/src/cil.ml
@@ -309,10 +309,12 @@ and fkind =
   | FDouble             (** [double] *)
   | FLongDouble         (** [long double] *)
   | FFloat128           (** [float128] *)
+  | FFloat16            (** [_Float16] *)
   | FComplexFloat       (** [float _Complex] *)
   | FComplexDouble      (** [double _Complex] *)
   | FComplexLongDouble  (** [long double _Complex]*)
   | FComplexFloat128    (** [_float128 _Complex]*)
+  | FComplexFloat16     (** [_Float16 _Complex]*)
 
 (** An attribute has a name and some optional parameters *)
 and attribute = Attr of string * attrparam list
@@ -1665,10 +1667,12 @@ let typeOfRealAndImagComponents t =
       | FDouble -> FDouble     (* [double] *)
       | FLongDouble -> FLongDouble (* [long double] *)
       | FFloat128 -> FFloat128
+      | FFloat16 -> FFloat16
       | FComplexFloat -> FFloat
       | FComplexDouble -> FDouble
       | FComplexLongDouble -> FLongDouble
       | FComplexFloat128 -> FFloat128
+      | FComplexFloat16 -> FFloat16
     in
     TFloat (newfkind fkind, attrs)
   | _ -> E.s (E.bug "unexpected non-numerical type for argument to __real__/__imag__ ")
@@ -1679,10 +1683,12 @@ let getComplexFkind = function
   | FDouble -> FComplexDouble
   | FLongDouble -> FComplexLongDouble
   | FFloat128 -> FComplexFloat128
+  | FFloat16 -> FComplexFloat16
   | FComplexFloat -> FComplexFloat
   | FComplexDouble -> FComplexDouble
   | FComplexLongDouble -> FComplexLongDouble
   | FComplexFloat128 -> FComplexFloat128
+  | FComplexFloat16 -> FComplexFloat16
 
 let var vi : lval = (Var vi, NoOffset)
 (* let assign vi e = Instrs(Set (var vi, e), lu) *)
@@ -1755,10 +1761,12 @@ let d_fkind () = function
   | FDouble -> text "double"
   | FLongDouble -> text "long double"
   | FFloat128 -> text "_Float128"
+  | FFloat16 -> text "_Float16"
   | FComplexFloat -> text "_Complex float"
   | FComplexDouble -> text "_Complex double"
   | FComplexLongDouble -> text "_Complex long double"
   | FComplexFloat128 -> text "_Complex _Float128"
+  | FComplexFloat16 -> text "_Complex _Float16"
 
 let d_storage () = function
     NoStorage -> nil
@@ -1855,10 +1863,12 @@ let d_const () c =
        | FDouble -> nil
        | FLongDouble -> chr 'L'
        | FFloat128 -> text "F128"
+       | FFloat16 -> text "F16"
        | FComplexFloat -> text "iF"
        | FComplexDouble -> chr 'i'
        | FComplexLongDouble -> text "iL"
-       | FComplexFloat128 -> text "iF128")
+       | FComplexFloat128 -> text "iF128"
+       | FComplexFloat16 -> text "iF16")
   | CEnum(_, s, ei) -> text s
 
 
@@ -2108,6 +2118,7 @@ let floatKindForSize (s:int) =
   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 if s = !M.theMachine.M.sizeof_float16 then FFloat16
   else raise Not_found
 
 (* Represents an integer as for a given kind.  Returns a flag saying
@@ -2267,10 +2278,12 @@ let rec alignOf_int t =
     | TFloat(FDouble, _) -> !M.theMachine.M.alignof_double
     | TFloat(FLongDouble, _) -> !M.theMachine.M.alignof_longdouble
     | TFloat(FFloat128, _) -> !M.theMachine.M.alignof_float128
+    | TFloat(FFloat16, _) -> !M.theMachine.M.alignof_float16
     | 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
+    | TFloat(FComplexFloat16, _) -> !M.theMachine.M.alignof_float16complex
     | TNamed (t, _) -> alignOf_int t.ttype
     | TArray (t, _, _) -> alignOf_int t
     | TPtr _ | TBuiltin_va_list _ -> !M.theMachine.M.alignof_ptr
@@ -2425,10 +2438,12 @@ and bitsSizeOf t =
   | 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(FFloat16, _) -> 8 * !M.theMachine.M.sizeof_float16
   | 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(FComplexFloat16, _) -> 8 * !M.theMachine.M.sizeof_float16complex
   | TFloat(FComplexFloat, _) -> 8 * !M.theMachine.M.sizeof_floatcomplex
   | TEnum (ei, _) -> bitsSizeOf (TInt(ei.ekind, []))
   | TPtr _ -> 8 * !M.theMachine.M.sizeof_ptr
diff --git a/src/cil.mli b/src/cil.mli
@@ -296,10 +296,12 @@ and fkind =
   | FDouble             (** [double] *)
   | FLongDouble         (** [long double] *)
   | FFloat128           (** [float128] *)
+  | FFloat16            (** [_Float16] *)
   | FComplexFloat       (** [float _Complex] *)
   | FComplexDouble      (** [double _Complex] *)
   | FComplexLongDouble  (** [long double _Complex]*)
   | FComplexFloat128    (** [_float128 _Complex]*)
+  | FComplexFloat16     (** [_Float16 _Complex]*)
 
 (** {b Attributes.} *)
 
diff --git a/src/frontc/cabs.ml b/src/frontc/cabs.ml
@@ -72,6 +72,7 @@ type typeSpecifier = (* Merge all specifiers into one type *)
   | Tfloat128 (* TODO needed? *)
   | Tfloat32x
   | Tfloat64x
+  | Tfloat16
   | Tdouble
   | Tsigned
   | Tsizet    (* used temporarily to translate offsetof() *)
diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml
@@ -1373,7 +1373,7 @@ 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 || f = FComplexFloat128 in
+    let isComplex f = f = FComplexFloat || f = FComplexDouble || f = FComplexLongDouble || f = FComplexFloat128 || f = FComplexFloat16 in
     match fkind1, fkind2 with
     | FComplexFloat128, _ -> t1
     | _, FComplexFloat128 -> t2
@@ -1389,7 +1389,11 @@ let arithmeticConversion    (* c.f. ISO 6.3.1.8 *)
     | other, FDouble -> if isComplex other then TFloat(FComplexDouble, []) else t2
     | FComplexFloat, other -> t1
     | other, FComplexFloat -> t2
-    | FFloat, FFloat -> t1
+    | FFloat, other -> if isComplex other then TFloat(FComplexFloat, []) else t1
+    | other, FFloat -> if isComplex other then TFloat(FComplexFloat, []) else t2
+    | FComplexFloat16, other -> t1
+    | other, FComplexFloat16 -> t2
+    | FFloat16, FFloat16 -> t1
   in
   match unrollType t1, unrollType t2 with
   | TFloat(fkind1, _), TFloat(fkind2, _) -> resultingFType fkind1 t1 fkind2 t2
@@ -2620,6 +2624,7 @@ let rec doSpecList (suggestedAnonName: string) (* This string will be part of
 
     | [A.Tlong; A.Tdouble] -> TFloat(FLongDouble, [])
     | [A.Tfloat128] -> TFloat(FFloat128, [])
+    | [A.Tfloat16] -> TFloat(FFloat16, [])
      (* Now the other type specifiers *)
     | [A.Tdefault] -> E.s (error "Default outside generic associations")
     | [A.Tnamed n] -> begin
@@ -3739,6 +3744,8 @@ and doExp (asconst: bool)   (* This expression is used as a constant *)
             let baseint, kind =
               if hasSuffix str "F128" then
                 String.sub str 0 (l - 4), FFloat128
+              else if hasSuffix str "F16" then
+                String.sub str 0 (l - 3), FFloat16
               else if hasSuffix str "Q" then
                 String.sub str 0 (l - 1), FFloat128
               else if hasSuffix str "L" then
@@ -3773,6 +3780,8 @@ and doExp (asconst: bool)   (* This expression is used as a constant *)
             let baseint, kind =
               if hasSuffix str "iF128" || hasSuffix str "F128i" then
                 String.sub str 0 (l - 5), FComplexFloat128
+              else if hasSuffix str "iF16" || hasSuffix str "F16i" then
+                String.sub str 0 (l - 4), FComplexFloat16
               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
@@ -3860,11 +3869,13 @@ and doExp (asconst: bool)   (* This expression is used as a constant *)
           | FFloat
           | FDouble
           | FLongDouble
-          | FFloat128 -> 8
+          | FFloat128
+          | FFloat16 -> 8
           | FComplexFloat
           | FComplexDouble
           | FComplexLongDouble
-          | FComplexFloat128 -> 9
+          | FComplexFloat128
+          | FComplexFloat16 -> 9
           end
         | TEnum _ -> 3
         | TPtr _ -> 5
@@ -4530,7 +4541,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 || f = FComplexFloat128
+                              | TFloat(f, _) -> f = FComplexFloat || f = FComplexDouble || f = FComplexLongDouble || f = FComplexFloat128 || f = FComplexFloat16
                               | _ -> false
                             in
                             if List.for_all (fun x -> not (isComplex x)) retTypes then
diff --git a/src/frontc/clexer.mll b/src/frontc/clexer.mll
@@ -143,6 +143,7 @@ let init_lexicon _ =
       ("_Float64", fun loc -> FLOAT64 loc);
       ("_Float32x", fun loc -> FLOAT32X loc);
       ("_Float64x", fun loc -> FLOAT64X loc);
+      ("_Float16", fun loc -> FLOAT16 loc);
       ("double", fun loc -> DOUBLE loc);
       ("void", fun loc -> VOID loc);
       ("enum", fun loc -> ENUM loc);
diff --git a/src/frontc/cparser.mly b/src/frontc/cparser.mly
@@ -265,6 +265,7 @@ let transformOffsetOf (speclist, dtype) member =
 %token<Cabs.cabsloc> INT128 FLOAT128 COMPLEX /* C99 */
 %token<Cabs.cabsloc> FLOAT32 FLOAT64 /* FloatN */
 %token<Cabs.cabsloc> FLOAT32X FLOAT64X /* FloatNx */
+%token<Cabs.cabsloc> FLOAT16
 %token<Cabs.cabsloc> GENERIC NORETURN /* C11 */
 %token<Cabs.cabsloc> AUTOTYPE /* GCC */
 %token<Cabs.cabsloc> ENUM STRUCT TYPEDEF UNION
@@ -1097,6 +1098,7 @@ type_spec:   /* ISO 6.7.2 */
 |   FLOAT128        { Tfloat128, $1 }
 |   FLOAT32X        { Tfloat32x, $1 }
 |   FLOAT64X        { Tfloat64x, $1 }
+|   FLOAT16         { Tfloat16, $1 }
 |   DOUBLE          { Tdouble, $1 }
 |   AUTOTYPE        { Tauto, $1 }
 /* |   COMPLEX FLOAT   { Tfloat, $2 } */
diff --git a/src/frontc/cprint.ml b/src/frontc/cprint.ml
@@ -175,6 +175,7 @@ and print_type_spec = function
   | Tfloat128 -> print "__float128"
   | Tfloat32x -> print "_Float32x"
   | Tfloat64x -> print "_Float64x"
+  | Tfloat16 -> print "_Float16"
   | Tdouble -> print "double "
   | Tsigned -> printu "signed"
   | Tunsigned -> print "unsigned "
diff --git a/src/machdep-ml.c b/src/machdep-ml.c
@@ -86,6 +86,12 @@ typedef int bool;
 #define UNDERSCORE_NAME "false"
 #endif
 
+#ifdef HAVE_FLOAT16_DEF
+#define HAVE_FLOAT16 "true"
+#else
+#define HAVE_FLOAT16 "false"
+#endif
+
 #endif
 
 
@@ -106,8 +112,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_float128,
-    alignof_floatcomplex, alignof_doublecomplex, alignof_longdoublecomplex, alignof_float128complex,
+    alignof_float, alignof_float32x, alignof_float64x, alignof_double, alignof_longdouble, alignof_float128, alignof_float16,
+    alignof_floatcomplex, alignof_doublecomplex, alignof_longdoublecomplex, alignof_float128complex, alignof_float16complex,
     sizeof_fun,
     alignof_fun, alignof_str, alignof_aligned, alignof_longlong,
     little_endian, char_is_unsigned, alignof_bool;
@@ -231,6 +237,19 @@ int main(int argc, char **argv)
     alignof_float128 = (intptr_t)(&((struct s1*)0)->ld);
   }
 
+#ifdef HAVE_FLOAT16_DEF
+  // The alignment of float16
+  {
+    struct s1 {
+      char c;
+      _Float16 ld;
+    };
+    alignof_float16 = (intptr_t)(&((struct s1*)0)->ld);
+  }
+#else
+  alignof_float16 = 0;
+#endif
+
   // The alignment of a float complex
   {
     struct floatstruct {
@@ -267,6 +286,19 @@ int main(int argc, char **argv)
     alignof_float128complex = (intptr_t)(&((struct s1*)0)->ld);
   }
 
+#ifdef HAVE_FLOAT16_DEF
+  // The alignment of float16 complex
+  {
+    struct s1 {
+      char c;
+      _Float16 _Complex ld;
+    };
+    alignof_float16complex = (intptr_t)(&((struct s1*)0)->ld);
+  }
+#else
+  alignof_float16complex = 0;
+#endif
+
 
   alignof_str = __alignof("a string");
   alignof_fun = __alignof(main);
@@ -304,11 +336,11 @@ 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 float128=%d,%d float_complex=%d,%d double_complex=%d,%d long_double_complex=%d,%d float128_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 float16=%d,%d float_complex=%d,%d double_complex=%d,%d long_double_complex=%d,%d float128_complex=%d,%d float16_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 "
-	     "underscore_name=%s\n",
+	     "underscore_name=%s have_float16=%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,
@@ -322,16 +354,26 @@ int main(int argc, char **argv)
 	     (int)sizeof(float), alignof_float, (int)sizeof(double), alignof_double,
 	     (int)sizeof(long double), alignof_longdouble,
       (int)sizeof(_Float128), alignof_float128,
+#ifdef HAVE_FLOAT16_DEF
+       (int)sizeof(_Float16), alignof_float16,
+#else
+       0, 0,
+#endif
        (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,
+#ifdef HAVE_FLOAT16_DEF
+       (int)sizeof(_Float16 _Complex), alignof_float16complex,
+#else
+       0, 0,
+#endif
        (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),
 	     char_is_unsigned ? "false" : "true",
 	     little_endian ? "false" : "true",
-	     THREAD_IS_KEYWORD, HAVE_BUILTIN_VA_LIST, UNDERSCORE_NAME);
+	     THREAD_IS_KEYWORD, HAVE_BUILTIN_VA_LIST, UNDERSCORE_NAME, HAVE_FLOAT16);
     }
   else
     {
@@ -359,10 +401,20 @@ int main(int argc, char **argv)
       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));
+#ifdef HAVE_FLOAT16_DEF
+      printf("\t sizeof_float16             = %d;\n", (int)sizeof(_Float16));
+#else
+      printf("\t sizeof_float16             = %d;\n", 0);
+#endif
       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));
+#ifdef HAVE_FLOAT16_DEF
+      printf("\t sizeof_float16complex      = %d;\n", (int)sizeof(_Float16 _Complex));
+#else
+      printf("\t sizeof_float16complex      = %d;\n", 0);
+#endif
       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);
@@ -386,10 +438,20 @@ int main(int argc, char **argv)
       printf("\t alignof_double             = %d;\n", alignof_double);
       printf("\t alignof_longdouble         = %d;\n", alignof_longdouble);
       printf("\t alignof_float128           = %d;\n", alignof_float128);
+#ifdef HAVE_FLOAT16_DEF
+      printf("\t alignof_float16            = %d;\n", alignof_float16);
+#else
+      printf("\t alignof_float16            = %d;\n", 0);
+#endif
       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);
+#ifdef HAVE_FLOAT16_DEF
+      printf("\t alignof_float16complex     = %d;\n", alignof_float16complex);
+#else
+      printf("\t alignof_float16complex     = %d;\n", alignof_float16complex);
+#endif
       printf("\t alignof_str                = %d;\n", alignof_str);
       printf("\t alignof_fun                = %d;\n", alignof_fun);
       printf("\t alignof_aligned            = %d;\n", alignof_aligned);
@@ -398,6 +460,7 @@ int main(int argc, char **argv)
       printf("\t __builtin_va_list          = %s;\n", HAVE_BUILTIN_VA_LIST);
       printf("\t __thread_is_keyword        = %s;\n", THREAD_IS_KEYWORD);
       printf("\t little_endian              = %s;\n", little_endian ? "true" : "false");
+      printf("\t have_float16               = %s;\n", HAVE_FLOAT16);
     }
   return 0;
 }
diff --git a/src/machdep.cppo.ml b/src/machdep.cppo.ml
diff --git a/src/machdepConfigure.ml b/src/machdepConfigure.ml
diff --git a/src/machdepenv.ml b/src/machdepenv.ml
