From 21aaf9c53b2bb0c6d376c2ce436d6dd7f5442a47 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 1 Feb 2021 18:53:04 +0100 Subject: bits to float --- riscV/Builtins1.v | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) (limited to 'riscV/Builtins1.v') diff --git a/riscV/Builtins1.v b/riscV/Builtins1.v index 86bcb2ac..47bacffa 100644 --- a/riscV/Builtins1.v +++ b/riscV/Builtins1.v @@ -22,23 +22,31 @@ Require ExtValues. Inductive platform_builtin : Type := | BI_bits_of_float -| BI_bits_of_double. +| BI_bits_of_double +| BI_float_of_bits +| BI_double_of_bits. Local Open Scope string_scope. Definition platform_builtin_table : list (string * platform_builtin) := ("__builtin_bits_of_float", BI_bits_of_float) :: ("__builtin_bits_of_double", BI_bits_of_double) + :: ("__builtin_float_of_bits", BI_float_of_bits) + :: ("__builtin_double_of_bits", BI_double_of_bits) :: nil. Definition platform_builtin_sig (b: platform_builtin) : signature := match b with | BI_bits_of_float => mksignature (Tsingle :: nil) Tint cc_default | BI_bits_of_double => mksignature (Tfloat :: nil) Tlong cc_default + | BI_float_of_bits => mksignature (Tint :: nil) Tsingle cc_default + | BI_double_of_bits => mksignature (Tlong :: nil) Tfloat cc_default end. Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (platform_builtin_sig b)) := match b with | BI_bits_of_float => mkbuiltin_n1t Tsingle Tint Float32.to_bits | BI_bits_of_double => mkbuiltin_n1t Tfloat Tlong Float.to_bits + | BI_float_of_bits => mkbuiltin_n1t Tint Tsingle Float32.of_bits + | BI_double_of_bits => mkbuiltin_n1t Tlong Tfloat Float.of_bits end. -- cgit