Add minimal syntactic support for type _Float16

This is part of C23 appendix H, and is starting to be used in system header files. `_Float16` is kept as a distinct FP type during elaboration, then rejected during conversion to CompCert C. The verified part of CompCert is unchanged.
AbsInt · Oct 20, 2024 · 7184253 · 7184253
1 parent 5f90f91
commit 7184253
Show file tree

Hide file tree

Showing 9 changed files with 30 additions and 5 deletions.
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
@@ -421,6 +421,9 @@ let convertIkind k a : coq_type =
 
 let convertFkind k a : coq_type =
   match k with
+  | C.FFloat16 ->
+      unsupported "'_Float16' type";
+      Tfloat (F32, a)
   | C.FFloat -> Tfloat (F32, a)
   | C.FDouble -> Tfloat (F64, a)
   | C.FLongDouble ->
@@ -695,6 +698,9 @@ let convertFloat f kind =
   match mant with
     | Z.Z0 ->
       begin match kind with
+      | FFloat16 ->
+          unsupported "'_Float16' type";
+	  Ctyping.econst_single (Float.to_single Float.zero)
       | FFloat ->
 	  Ctyping.econst_single (Float.to_single Float.zero)
       | FDouble | FLongDouble ->
@@ -712,6 +718,9 @@ let convertFloat f kind =
       let base = P.of_int (if f.C.hex then 2 else 10) in
 
       begin match kind with
+      | FFloat16 ->
+          unsupported "'_Float16' type";
+	  Ctyping.econst_single (Float.to_single Float.zero)
       | FFloat ->
 	  let f = Float32.from_parsed base mant exp in
           checkFloatOverflow f "float";

diff --git a/cparser/C.mli b/cparser/C.mli
@@ -46,11 +46,11 @@ type ikind =
 (** Kinds of floating-point numbers*)
 
 type fkind =
-    FFloat      (** [float] *)
+  | FFloat16    (** [_Float16] *)
+  | FFloat      (** [float] *)
   | FDouble     (** [double] *)
   | FLongDouble (** [long double] *)
 
-
 (** Constants *)
 
 type float_cst = {

diff --git a/cparser/Cabs.v b/cparser/Cabs.v
@@ -48,6 +48,7 @@ Inductive typeSpecifier := (* Merge all specifiers into one type *)
   | Tint
   | Tlong
   | Tfloat
+  | Tfloat16
   | Tdouble
   | Tsigned
   | Tunsigned

diff --git a/cparser/Cprint.ml b/cparser/Cprint.ml
@@ -56,6 +56,7 @@ let const pp = function
     else
       fprintf pp "%s.%sE%s" v.intPart v.fracPart v.exp;
     begin match fk with
+      | FFloat16 -> () (* no syntax for FP16 literals; should not happen *)
       | FFloat -> fprintf pp "F"
       | FLongDouble -> fprintf pp "L"
       | FDouble -> ()
@@ -123,6 +124,7 @@ let name_of_ikind = function
   | IULongLong -> "unsigned long long"
 
 let name_of_fkind = function
+  | FFloat16 -> "_Float16"
   | FFloat -> "float"
   | FDouble -> "double"
   | FLongDouble -> "long double"

diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml
@@ -461,6 +461,7 @@ let alignof_ikind = function
   | ILongLong | IULongLong -> !config.alignof_longlong
 
 let alignof_fkind = function
+  | FFloat16 -> 2
   | FFloat -> !config.alignof_float
   | FDouble -> !config.alignof_double
   | FLongDouble -> !config.alignof_longdouble
@@ -515,6 +516,7 @@ let sizeof_ikind = function
   | ILongLong | IULongLong -> !config.sizeof_longlong
 
 let sizeof_fkind = function
+  | FFloat16 -> 2
   | FFloat -> !config.sizeof_float
   | FDouble -> !config.sizeof_double
   | FLongDouble -> !config.sizeof_longdouble
@@ -865,6 +867,7 @@ let integer_rank = function
 (* Ranking of float kinds *)
 
 let float_rank = function
+  | FFloat16 -> 0
   | FFloat -> 1
   | FDouble -> 2
   | FLongDouble -> 3
@@ -922,7 +925,9 @@ let binary_conversion env t1 t2 =
   | TFloat(FDouble, _), (TInt _ | TFloat _)     -> t1
   | (TInt _ | TFloat _), TFloat(FDouble, _)     -> t2
   | TFloat(FFloat, _), (TInt _ | TFloat _)      -> t1
-  | (TInt _), TFloat(FFloat, _)      -> t2
+  | (TInt _ | TFloat _), TFloat(FFloat, _)      -> t2
+  | TFloat(FFloat16, _), (TInt _ | TFloat _)    -> t1
+  | (TInt _), TFloat(FFloat16, _)               -> t2
   | TInt(k1, _), TInt(k2, _)  ->
       if k1 = k2 then t1 else begin
         match is_signed_ikind k1, is_signed_ikind k2 with

diff --git a/cparser/Elab.ml b/cparser/Elab.ml
@@ -815,6 +815,7 @@ let rec elab_specifier ?(only = false) loc env specifier =
     | [Cabs.Tunsigned; Cabs.Tlong; Cabs.Tlong; Cabs.Tint] -> simple (TInt(IULongLong, []))
 
     | [Cabs.Tfloat] -> simple (TFloat(FFloat, []))
+    | [Cabs.Tfloat16] -> simple (TFloat(FFloat16, [])) 
     | [Cabs.Tdouble] -> simple (TFloat(FDouble, []))
 
     | [Cabs.Tlong; Cabs.Tdouble] -> simple (TFloat(FLongDouble, []))

diff --git a/cparser/Lexer.mll b/cparser/Lexer.mll
@@ -37,6 +37,7 @@ let () =
       ("_Bool", fun loc -> UNDERSCORE_BOOL loc);
       ("_Generic", fun loc -> GENERIC loc);
       ("_Complex", fun loc -> reserved_keyword loc "_Complex");
+      ("_Float16", fun loc -> FLOAT16 loc);
       ("_Imaginary", fun loc -> reserved_keyword loc "_Imaginary");
       ("_Static_assert", fun loc -> STATIC_ASSERT loc);
       ("__alignof", fun loc -> ALIGNOF loc);
@@ -638,6 +639,7 @@ and singleline_comment = parse
       | Pre_parser.EQEQ loc -> loop (Parser.EQEQ loc)
       | Pre_parser.EXTERN loc -> loop (Parser.EXTERN loc)
       | Pre_parser.FLOAT loc -> loop (Parser.FLOAT loc)
+      | Pre_parser.FLOAT16 loc -> loop (Parser.FLOAT16 loc)
       | Pre_parser.FOR loc -> loop (Parser.FOR loc)
       | Pre_parser.GENERIC loc -> loop (Parser.GENERIC loc)
       | Pre_parser.GEQ loc -> loop (Parser.GEQ loc)

diff --git a/cparser/Parser.vy b/cparser/Parser.vy
@@ -35,7 +35,8 @@ Require Cabs.
 
 %token<Cabs.loc> LPAREN RPAREN LBRACK RBRACK LBRACE RBRACE DOT COMMA
   SEMICOLON ELLIPSIS TYPEDEF EXTERN STATIC RESTRICT AUTO REGISTER INLINE
-  NORETURN CHAR SHORT INT LONG SIGNED UNSIGNED FLOAT DOUBLE CONST VOLATILE VOID
+  NORETURN CHAR SHORT INT LONG SIGNED UNSIGNED FLOAT FLOAT16 DOUBLE
+  CONST VOLATILE VOID
   STRUCT UNION ENUM UNDERSCORE_BOOL PACKED ALIGNAS ATTRIBUTE ASM
 
 %token<Cabs.loc> CASE DEFAULT IF_ ELSE SWITCH WHILE DO FOR GOTO CONTINUE BREAK
@@ -441,6 +442,8 @@ type_specifier:
     { (Cabs.Tlong, loc) }
 | loc = FLOAT
     { (Cabs.Tfloat, loc) }
+| loc = FLOAT16
+    { (Cabs.Tfloat16, loc) }
 | loc = DOUBLE
     { (Cabs.Tdouble, loc) }
 | loc = SIGNED

diff --git a/cparser/pre_parser.mly b/cparser/pre_parser.mly
@@ -55,7 +55,8 @@
   COLON AND MUL_ASSIGN DIV_ASSIGN MOD_ASSIGN ADD_ASSIGN SUB_ASSIGN LEFT_ASSIGN
   RIGHT_ASSIGN AND_ASSIGN XOR_ASSIGN OR_ASSIGN LPAREN RPAREN LBRACK RBRACK
   LBRACE RBRACE DOT COMMA SEMICOLON ELLIPSIS TYPEDEF EXTERN STATIC RESTRICT
-  AUTO REGISTER INLINE NORETURN CHAR SHORT INT LONG SIGNED UNSIGNED FLOAT DOUBLE
+  AUTO REGISTER INLINE NORETURN CHAR SHORT INT LONG SIGNED UNSIGNED 
+  FLOAT FLOAT16 DOUBLE
   UNDERSCORE_BOOL CONST VOLATILE VOID STRUCT UNION ENUM CASE DEFAULT IF ELSE
   SWITCH WHILE DO FOR GOTO CONTINUE BREAK RETURN BUILTIN_VA_ARG ALIGNOF
   ATTRIBUTE ALIGNAS PACKED ASM BUILTIN_OFFSETOF STATIC_ASSERT GENERIC
@@ -510,6 +511,7 @@ type_specifier_no_typedef_name:
 | INT
 | LONG
 | FLOAT
+| FLOAT16
 | DOUBLE
 | SIGNED
 | UNSIGNED