From 7184253a063a0d27542c44ff1fa5061056993586 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 4 Oct 2024 14:32:27 +0200 Subject: [PATCH] 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. --- cfrontend/C2C.ml | 9 +++++++++ cparser/C.mli | 4 ++-- cparser/Cabs.v | 1 + cparser/Cprint.ml | 2 ++ cparser/Cutil.ml | 7 ++++++- cparser/Elab.ml | 1 + cparser/Lexer.mll | 2 ++ cparser/Parser.vy | 5 ++++- cparser/pre_parser.mly | 4 +++- 9 files changed, 30 insertions(+), 5 deletions(-) diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index a2670ae693..f44eb63812 100644 --- 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 index 1388fab949..24f0e6f94a 100644 --- 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 index 59cd30abbc..f27640114c 100644 --- 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 index 054487841e..8155cf0943 100644 --- 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 index 5b099d7fa6..0ef96ddd13 100644 --- 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 index b4c0a20727..3060568b23 100644 --- 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 index 95374afe90..5d377053df 100644 --- 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 index cb1873b886..b69979675a 100644 --- a/cparser/Parser.vy +++ b/cparser/Parser.vy @@ -35,7 +35,8 @@ Require Cabs. %token 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 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 index 00ca0ade7e..fd1559f74b 100644 --- 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