Skip to content

Commit

Permalink
Add minimal syntactic support for type _Float16 (#525)
Browse files Browse the repository at this point in the history 
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.
  • Loading branch information
@xavierleroy
xavierleroy authored Oct 22, 2024
1 parent bf8a3e1 commit a735bfb
Show file tree
Hide file tree
Showing 9 changed files with 30 additions and 5 deletions.
9 changes: 9 additions & 0 deletions cfrontend/C2C.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 ->
Expand Down Expand Up @@ -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 ->
Expand All @@ -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";
Expand Down
4 changes: 2 additions & 2 deletions cparser/C.mli
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 = {
Expand Down
1 change: 1 addition & 0 deletions cparser/Cabs.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -48,6 +48,7 @@ Inductive typeSpecifier := (* Merge all specifiers into one type *)
| Tint
| Tlong
| Tfloat
| Tfloat16
| Tdouble
| Tsigned
| Tunsigned
Expand Down
2 changes: 2 additions & 0 deletions cparser/Cprint.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 -> ()
Expand Down Expand Up @@ -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"
Expand Down
7 changes: 6 additions & 1 deletion cparser/Cutil.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -865,6 +867,7 @@ let integer_rank = function
(* Ranking of float kinds *)

let float_rank = function
| FFloat16 -> 0
| FFloat -> 1
| FDouble -> 2
| FLongDouble -> 3
Expand Down Expand Up @@ -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
Expand Down
1 change: 1 addition & 0 deletions cparser/Elab.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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, []))
Expand Down
2 changes: 2 additions & 0 deletions cparser/Lexer.mll
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down Expand Up @@ -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)
Expand Down
5 changes: 4 additions & 1 deletion cparser/Parser.vy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
4 changes: 3 additions & 1 deletion cparser/pre_parser.mly
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -510,6 +511,7 @@ type_specifier_no_typedef_name:
| INT
| LONG
| FLOAT
| FLOAT16
| DOUBLE
| SIGNED
| UNSIGNED
Expand Down

1 comment on commit a735bfb

@monniaux
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thank you. This fixes the problems we had running the test suite on MacOS ARM.

Please sign in to comment.