Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Add minimal syntactic support for type _Float16 #525

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Add minimal syntactic support for type _Float16 #525

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 9 additions & 0 deletions cfrontend/C2C.ml
View file
Open in desktop
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
6 changes: 3 additions & 3 deletions cparser/C.mli
View file
Open in desktop
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] *)
| FDouble (** [double] *)
| FFloat16 (** [_Float16] *)
| FFloat (** [float], [_Float32] *)
| FDouble (** [double], [_Float64] *)
| FLongDouble (** [long double] *)


(** Constants *)

type float_cst = {
Expand Down
1 change: 1 addition & 0 deletions cparser/Cabs.v
View file
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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