aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile4
-rw-r--r--handwritten_support/0.11/riscv_extras_fdext.lem109
-rw-r--r--handwritten_support/riscv_extras_fdext.lem109
-rw-r--r--model/riscv_softfloat_interface.sail60
4 files changed, 250 insertions, 32 deletions
diff --git a/Makefile b/Makefile
index dcd738e..e4ac825 100644
--- a/Makefile
+++ b/Makefile
@@ -146,7 +146,7 @@ else
C_FLAGS += -O3 -flto
endif
-RISCV_EXTRAS_LEM_FILES = riscv_extras.lem mem_metadata.lem
+RISCV_EXTRAS_LEM_FILES = riscv_extras.lem mem_metadata.lem riscv_extras_fdext.lem
# Feature detect if we are on the latest development version of Sail
# and use an updated lem file if so. This is just until the opam
# version catches up with changes to the barrier type.
@@ -274,7 +274,7 @@ endif
generated_definitions/lem/$(ARCH)/riscv.lem: $(SAIL_SRCS) Makefile
mkdir -p generated_definitions/lem/$(ARCH) generated_definitions/isabelle/$(ARCH)
- $(SAIL) $(SAIL_FLAGS) -lem -lem_output_dir generated_definitions/lem/$(ARCH) -isa_output_dir generated_definitions/isabelle/$(ARCH) -o riscv -lem_mwords -lem_lib Riscv_extras -lem_lib Mem_metadata $(SAIL_SRCS)
+ $(SAIL) $(SAIL_FLAGS) -lem -lem_output_dir generated_definitions/lem/$(ARCH) -isa_output_dir generated_definitions/isabelle/$(ARCH) -o riscv -lem_mwords -lem_lib Riscv_extras -lem_lib Riscv_extras_fdext -lem_lib Mem_metadata $(SAIL_SRCS)
echo "declare {isabelle} rename field sync_exception_ext = sync_exception_ext_exception" >> generated_definitions/lem/$(ARCH)/riscv_types.lem
generated_definitions/isabelle/$(ARCH)/Riscv.thy: generated_definitions/isabelle/$(ARCH)/ROOT generated_definitions/lem/$(ARCH)/riscv.lem $(RISCV_EXTRAS_LEM) Makefile
diff --git a/handwritten_support/0.11/riscv_extras_fdext.lem b/handwritten_support/0.11/riscv_extras_fdext.lem
new file mode 100644
index 0000000..3c79089
--- /dev/null
+++ b/handwritten_support/0.11/riscv_extras_fdext.lem
@@ -0,0 +1,109 @@
+open import Pervasives
+open import Pervasives_extra
+open import Sail2_instr_kinds
+open import Sail2_values
+open import Sail2_operators_mwords
+open import Sail2_prompt_monad
+open import Sail2_prompt
+
+type bitvector 'a = mword 'a
+
+(* stub functions emulating the C softfloat interface *)
+
+val softfloat_f32_add : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
+let softfloat_f32_add _ _ _ = ()
+
+val softfloat_f32_sub : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
+let softfloat_f32_sub _ _ _ = ()
+
+val softfloat_f32_mul : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
+let softfloat_f32_mul _ _ _ = ()
+
+val softfloat_f32_div : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
+let softfloat_f32_div _ _ _ = ()
+
+val softfloat_f64_add : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
+let softfloat_f64_add _ _ _ = ()
+
+val softfloat_f64_sub : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
+let softfloat_f64_sub _ _ _ = ()
+
+val softfloat_f64_mul : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
+let softfloat_f64_mul _ _ _ = ()
+
+val softfloat_f64_div : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
+let softfloat_f64_div _ _ _ = ()
+
+
+val softfloat_f32_muladd : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> bitvector 's -> unit
+let softfloat_f32_muladd _ _ _ _ = ()
+
+val softfloat_f64_muladd : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> bitvector 's -> unit
+let softfloat_f64_muladd _ _ _ _ = ()
+
+
+val softfloat_f32_sqrt : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f32_sqrt _ _ = ()
+
+val softfloat_f64_sqrt : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f64_sqrt _ _ = ()
+
+
+val softfloat_f32_to_i32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f32_to_i32 _ _ = ()
+
+val softfloat_f32_to_ui32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f32_to_ui32 _ _ = ()
+
+val softfloat_i32_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_i32_to_f32 _ _ = ()
+
+val softfloat_ui32_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_ui32_to_f32 _ _ = ()
+
+val softfloat_f32_to_i64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f32_to_i64 _ _ = ()
+
+val softfloat_f32_to_ui64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f32_to_ui64 _ _ = ()
+
+val softfloat_i64_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_i64_to_f32 _ _ = ()
+
+val softfloat_ui64_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_ui64_to_f32 _ _ = ()
+
+
+val softfloat_f64_to_i32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f64_to_i32 _ _ = ()
+
+val softfloat_f64_to_ui32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f64_to_ui32 _ _ = ()
+
+val softfloat_i32_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_i32_to_f64 _ _ = ()
+
+val softfloat_ui32_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_ui32_to_f64 _ _ = ()
+
+val softfloat_f64_to_i64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f64_to_i64 _ _ = ()
+
+val softfloat_f64_to_ui64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f64_to_ui64 _ _ = ()
+
+val softfloat_i64_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_i64_to_f64 _ _ = ()
+
+val softfloat_ui64_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_ui64_to_f64 _ _ = ()
+
+
+val softfloat_f32_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f32_to_f64 _ _ = ()
+
+val softfloat_f64_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f64_to_f32 _ _ = ()
+
+
+
diff --git a/handwritten_support/riscv_extras_fdext.lem b/handwritten_support/riscv_extras_fdext.lem
new file mode 100644
index 0000000..3c79089
--- /dev/null
+++ b/handwritten_support/riscv_extras_fdext.lem
@@ -0,0 +1,109 @@
+open import Pervasives
+open import Pervasives_extra
+open import Sail2_instr_kinds
+open import Sail2_values
+open import Sail2_operators_mwords
+open import Sail2_prompt_monad
+open import Sail2_prompt
+
+type bitvector 'a = mword 'a
+
+(* stub functions emulating the C softfloat interface *)
+
+val softfloat_f32_add : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
+let softfloat_f32_add _ _ _ = ()
+
+val softfloat_f32_sub : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
+let softfloat_f32_sub _ _ _ = ()
+
+val softfloat_f32_mul : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
+let softfloat_f32_mul _ _ _ = ()
+
+val softfloat_f32_div : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
+let softfloat_f32_div _ _ _ = ()
+
+val softfloat_f64_add : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
+let softfloat_f64_add _ _ _ = ()
+
+val softfloat_f64_sub : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
+let softfloat_f64_sub _ _ _ = ()
+
+val softfloat_f64_mul : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
+let softfloat_f64_mul _ _ _ = ()
+
+val softfloat_f64_div : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
+let softfloat_f64_div _ _ _ = ()
+
+
+val softfloat_f32_muladd : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> bitvector 's -> unit
+let softfloat_f32_muladd _ _ _ _ = ()
+
+val softfloat_f64_muladd : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> bitvector 's -> unit
+let softfloat_f64_muladd _ _ _ _ = ()
+
+
+val softfloat_f32_sqrt : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f32_sqrt _ _ = ()
+
+val softfloat_f64_sqrt : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f64_sqrt _ _ = ()
+
+
+val softfloat_f32_to_i32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f32_to_i32 _ _ = ()
+
+val softfloat_f32_to_ui32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f32_to_ui32 _ _ = ()
+
+val softfloat_i32_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_i32_to_f32 _ _ = ()
+
+val softfloat_ui32_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_ui32_to_f32 _ _ = ()
+
+val softfloat_f32_to_i64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f32_to_i64 _ _ = ()
+
+val softfloat_f32_to_ui64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f32_to_ui64 _ _ = ()
+
+val softfloat_i64_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_i64_to_f32 _ _ = ()
+
+val softfloat_ui64_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_ui64_to_f32 _ _ = ()
+
+
+val softfloat_f64_to_i32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f64_to_i32 _ _ = ()
+
+val softfloat_f64_to_ui32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f64_to_ui32 _ _ = ()
+
+val softfloat_i32_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_i32_to_f64 _ _ = ()
+
+val softfloat_ui32_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_ui32_to_f64 _ _ = ()
+
+val softfloat_f64_to_i64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f64_to_i64 _ _ = ()
+
+val softfloat_f64_to_ui64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f64_to_ui64 _ _ = ()
+
+val softfloat_i64_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_i64_to_f64 _ _ = ()
+
+val softfloat_ui64_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_ui64_to_f64 _ _ = ()
+
+
+val softfloat_f32_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f32_to_f64 _ _ = ()
+
+val softfloat_f64_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f64_to_f32 _ _ = ()
+
+
+
diff --git a/model/riscv_softfloat_interface.sail b/model/riscv_softfloat_interface.sail
index 5258c79..1cc16a9 100644
--- a/model/riscv_softfloat_interface.sail
+++ b/model/riscv_softfloat_interface.sail
@@ -38,56 +38,56 @@ register float_fflags : bits(64)
/* **************************************************************** */
/* ADD/SUB/MUL/DIV */
-val extern_f32Add = {c: "softfloat_f32add", ocaml: "Softfloat.f32_add"} : (bits_rm, bits_S, bits_S) -> unit
+val extern_f32Add = {c: "softfloat_f32add", ocaml: "Softfloat.f32_add", lem: "softfloat_f32_add"} : (bits_rm, bits_S, bits_S) -> unit
val riscv_f32Add : (bits_rm, bits_S, bits_S) -> (bits_fflags, bits_S) effect {rreg}
function riscv_f32Add (rm, v1, v2) = {
extern_f32Add(rm, v1, v2);
(float_fflags[4 .. 0], float_result[31 .. 0])
}
-val extern_f32Sub = {c: "softfloat_f32sub", ocaml: "Softfloat.f32_sub"} : (bits_rm, bits_S, bits_S) -> unit
+val extern_f32Sub = {c: "softfloat_f32sub", ocaml: "Softfloat.f32_sub", lem: "softfloat_f32_sub"} : (bits_rm, bits_S, bits_S) -> unit
val riscv_f32Sub : (bits_rm, bits_S, bits_S) -> (bits_fflags, bits_S) effect {rreg}
function riscv_f32Sub (rm, v1, v2) = {
extern_f32Sub(rm, v1, v2);
(float_fflags[4 .. 0], float_result[31 .. 0])
}
-val extern_f32Mul = {c: "softfloat_f32mul", ocaml: "Softfloat.f32_mul"} : (bits_rm, bits_S, bits_S) -> unit
+val extern_f32Mul = {c: "softfloat_f32mul", ocaml: "Softfloat.f32_mul", lem: "softfloat_f32_mul"} : (bits_rm, bits_S, bits_S) -> unit
val riscv_f32Mul : (bits_rm, bits_S, bits_S) -> (bits_fflags, bits_S) effect {rreg}
function riscv_f32Mul (rm, v1, v2) = {
extern_f32Mul(rm, v1, v2);
(float_fflags[4 .. 0], float_result[31 .. 0])
}
-val extern_f32Div = {c: "softfloat_f32div", ocaml: "Softfloat.f32_div"} : (bits_rm, bits_S, bits_S) -> unit
+val extern_f32Div = {c: "softfloat_f32div", ocaml: "Softfloat.f32_div", lem: "softfloat_f32_div"} : (bits_rm, bits_S, bits_S) -> unit
val riscv_f32Div : (bits_rm, bits_S, bits_S) -> (bits_fflags, bits_S) effect {rreg}
function riscv_f32Div (rm, v1, v2) = {
extern_f32Div(rm, v1, v2);
(float_fflags[4 .. 0], float_result[31 .. 0])
}
-val extern_f64Add = {c: "softfloat_f64add", ocaml: "Softfloat.f64_add"} : (bits_rm, bits_D, bits_D) -> unit
+val extern_f64Add = {c: "softfloat_f64add", ocaml: "Softfloat.f64_add", lem: "softfloat_f64_add"} : (bits_rm, bits_D, bits_D) -> unit
val riscv_f64Add : (bits_rm, bits_D, bits_D) -> (bits_fflags, bits_D) effect {rreg}
function riscv_f64Add (rm, v1, v2) = {
extern_f64Add(rm, v1, v2);
(float_fflags[4 .. 0], float_result)
}
-val extern_f64Sub = {c: "softfloat_f64sub", ocaml: "Softfloat.f64_sub"} : (bits_rm, bits_D, bits_D) -> unit
+val extern_f64Sub = {c: "softfloat_f64sub", ocaml: "Softfloat.f64_sub", lem: "softfloat_f64_sub"} : (bits_rm, bits_D, bits_D) -> unit
val riscv_f64Sub : (bits_rm, bits_D, bits_D) -> (bits_fflags, bits_D) effect {rreg}
function riscv_f64Sub (rm, v1, v2) = {
extern_f64Sub(rm, v1, v2);
(float_fflags[4 .. 0], float_result)
}
-val extern_f64Mul = {c: "softfloat_f64mul", ocaml: "Softfloat.f64_mul"} : (bits_rm, bits_D, bits_D) -> unit
+val extern_f64Mul = {c: "softfloat_f64mul", ocaml: "Softfloat.f64_mul", lem: "softfloat_f64_mul"} : (bits_rm, bits_D, bits_D) -> unit
val riscv_f64Mul : (bits_rm, bits_D, bits_D) -> (bits_fflags, bits_D) effect {rreg}
function riscv_f64Mul (rm, v1, v2) = {
extern_f64Mul(rm, v1, v2);
(float_fflags[4 .. 0], float_result)
}
-val extern_f64Div = {c: "softfloat_f64div", ocaml: "Softfloat.f64_div"} : (bits_rm, bits_D, bits_D) -> unit
+val extern_f64Div = {c: "softfloat_f64div", ocaml: "Softfloat.f64_div", lem: "softfloat_f64_div"} : (bits_rm, bits_D, bits_D) -> unit
val riscv_f64Div : (bits_rm, bits_D, bits_D) -> (bits_fflags, bits_D) effect {rreg}
function riscv_f64Div (rm, v1, v2) = {
extern_f64Div(rm, v1, v2);
@@ -97,14 +97,14 @@ function riscv_f64Div (rm, v1, v2) = {
/* **************************************************************** */
/* MULTIPLY-ADD */
-val extern_f32MulAdd = {c: "softfloat_f32muladd", ocaml: "Softfloat.f32_muladd"} : (bits_rm, bits_S, bits_S, bits_S) -> unit
+val extern_f32MulAdd = {c: "softfloat_f32muladd", ocaml: "Softfloat.f32_muladd", lem: "softfloat_f32_muladd"} : (bits_rm, bits_S, bits_S, bits_S) -> unit
val riscv_f32MulAdd : (bits_rm, bits_S, bits_S, bits_S) -> (bits_fflags, bits_S) effect {rreg}
function riscv_f32MulAdd (rm, v1, v2, v3) = {
extern_f32MulAdd(rm, v1, v2, v3);
(float_fflags[4 .. 0], float_result[31 .. 0])
}
-val extern_f64MulAdd = {c: "softfloat_f64muladd", ocaml: "Softfloat.f64_muladd"} : (bits_rm, bits_D, bits_D, bits_D) -> unit
+val extern_f64MulAdd = {c: "softfloat_f64muladd", ocaml: "Softfloat.f64_muladd", lem: "softfloat_f64_muladd"} : (bits_rm, bits_D, bits_D, bits_D) -> unit
val riscv_f64MulAdd : (bits_rm, bits_D, bits_D, bits_D) -> (bits_fflags, bits_D) effect {rreg}
function riscv_f64MulAdd (rm, v1, v2, v3) = {
extern_f64MulAdd(rm, v1, v2, v3);
@@ -114,14 +114,14 @@ function riscv_f64MulAdd (rm, v1, v2, v3) = {
/* **************************************************************** */
/* SQUARE ROOT */
-val extern_f32Sqrt = {c: "softfloat_f32sqrt", ocaml: "Softfloat.f32_sqrt"} : (bits_rm, bits_S) -> unit
+val extern_f32Sqrt = {c: "softfloat_f32sqrt", ocaml: "Softfloat.f32_sqrt", lem: "softfloat_f32_sqrt"} : (bits_rm, bits_S) -> unit
val riscv_f32Sqrt : (bits_rm, bits_S) -> (bits_fflags, bits_S) effect {rreg}
function riscv_f32Sqrt (rm, v) = {
extern_f32Sqrt(rm, v);
(float_fflags[4 .. 0], float_result[31 .. 0])
}
-val extern_f64Sqrt = {c: "softfloat_f64sqrt", ocaml: "Softfloat.f64_sqrt"} : (bits_rm, bits_D) -> unit
+val extern_f64Sqrt = {c: "softfloat_f64sqrt", ocaml: "Softfloat.f64_sqrt", lem: "softfloat_f64_sqrt"} : (bits_rm, bits_D) -> unit
val riscv_f64Sqrt : (bits_rm, bits_D) -> (bits_fflags, bits_D) effect {rreg}
function riscv_f64Sqrt (rm, v) = {
extern_f64Sqrt(rm, v);
@@ -131,126 +131,126 @@ function riscv_f64Sqrt (rm, v) = {
/* **************************************************************** */
/* CONVERSIONS */
-val extern_f32ToI32 = {c: "softfloat_f32toi32", ocaml: "Softfloat.f32_to_i32"} : (bits_rm, bits_S) -> unit
+val extern_f32ToI32 = {c: "softfloat_f32toi32", ocaml: "Softfloat.f32_to_i32", lem: "softfloat_f32_to_i32"} : (bits_rm, bits_S) -> unit
val riscv_f32ToI32 : (bits_rm, bits_S) -> (bits_fflags, bits_W) effect {rreg}
function riscv_f32ToI32 (rm, v) = {
extern_f32ToI32(rm, v);
(float_fflags[4 .. 0], float_result[31 .. 0])
}
-val extern_f32ToUi32 = {c: "softfloat_f32toui32", ocaml: "Softfloat.f32_to_ui32"} : (bits_rm, bits_S) -> unit
+val extern_f32ToUi32 = {c: "softfloat_f32toui32", ocaml: "Softfloat.f32_to_ui32", lem: "softfloat_f32_to_ui32"} : (bits_rm, bits_S) -> unit
val riscv_f32ToUi32 : (bits_rm, bits_S) -> (bits_fflags, bits_WU) effect {rreg}
function riscv_f32ToUi32 (rm, v) = {
extern_f32ToUi32(rm, v);
(float_fflags[4 .. 0], float_result[31 .. 0])
}
-val extern_i32ToF32 = {c: "softfloat_i32tof32", ocaml: "Softfloat.i32_to_f32"} : (bits_rm, bits_W) -> unit
+val extern_i32ToF32 = {c: "softfloat_i32tof32", ocaml: "Softfloat.i32_to_f32", lem: "softfloat_i32_to_f32"} : (bits_rm, bits_W) -> unit
val riscv_i32ToF32 : (bits_rm, bits_W) -> (bits_fflags, bits_S) effect {rreg}
function riscv_i32ToF32 (rm, v) = {
extern_i32ToF32(rm, v);
(float_fflags[4 .. 0], float_result[31 .. 0])
}
-val extern_ui32ToF32 = {c: "softfloat_ui32tof32", ocaml: "Softfloat.ui32_to_f32"} : (bits_rm, bits_WU) -> unit
+val extern_ui32ToF32 = {c: "softfloat_ui32tof32", ocaml: "Softfloat.ui32_to_f32", lem: "softfloat_ui32_to_f32"} : (bits_rm, bits_WU) -> unit
val riscv_ui32ToF32 : (bits_rm, bits_WU) -> (bits_fflags, bits_S) effect {rreg}
function riscv_ui32ToF32 (rm, v) = {
extern_ui32ToF32(rm, v);
(float_fflags[4 .. 0], float_result[31 .. 0])
}
-val extern_f32ToI64 = {c: "softfloat_f32toi64", ocaml: "Softfloat.f32_to_i64"} : (bits_rm, bits_S) -> unit
+val extern_f32ToI64 = {c: "softfloat_f32toi64", ocaml: "Softfloat.f32_to_i64", lem: "softfloat_f32_to_i64"} : (bits_rm, bits_S) -> unit
val riscv_f32ToI64 : (bits_rm, bits_S) -> (bits_fflags, bits_L) effect {rreg}
function riscv_f32ToI64 (rm, v) = {
extern_f32ToI64(rm, v);
(float_fflags[4 .. 0], float_result)
}
-val extern_f32ToUi64 = {c: "softfloat_f32toui64", ocaml: "Softfloat.f32_to_ui64"} : (bits_rm, bits_S) -> unit
+val extern_f32ToUi64 = {c: "softfloat_f32toui64", ocaml: "Softfloat.f32_to_ui64", lem: "softfloat_f32_to_ui64"} : (bits_rm, bits_S) -> unit
val riscv_f32ToUi64 : (bits_rm, bits_S) -> (bits_fflags, bits_LU) effect {rreg}
function riscv_f32ToUi64 (rm, v) = {
extern_f32ToUi64(rm, v);
(float_fflags[4 .. 0], float_result)
}
-val extern_i64ToF32 = {c: "softfloat_i64tof32", ocaml: "Softfloat.i64_to_f32"} : (bits_rm, bits_L) -> unit
+val extern_i64ToF32 = {c: "softfloat_i64tof32", ocaml: "Softfloat.i64_to_f32", lem: "softfloat_i64_to_f32"} : (bits_rm, bits_L) -> unit
val riscv_i64ToF32 : (bits_rm, bits_L) -> (bits_fflags, bits_S) effect {rreg}
function riscv_i64ToF32 (rm, v) = {
extern_i64ToF32(rm, v);
(float_fflags[4 .. 0], float_result[31 .. 0])
}
-val extern_ui64ToF32 = {c: "softfloat_ui64tof32", ocaml: "Softfloat.ui64_to_f32"} : (bits_rm, bits_L) -> unit
+val extern_ui64ToF32 = {c: "softfloat_ui64tof32", ocaml: "Softfloat.ui64_to_f32", lem: "softfloat_ui64_to_f32"} : (bits_rm, bits_L) -> unit
val riscv_ui64ToF32 : (bits_rm, bits_LU) -> (bits_fflags, bits_S) effect {rreg}
function riscv_ui64ToF32 (rm, v) = {
extern_ui64ToF32(rm, v);
(float_fflags[4 .. 0], float_result[31 .. 0])
}
-val extern_f64ToI32 = {c: "softfloat_f64toi32", ocaml: "Softfloat.f64_to_i32"} : (bits_rm, bits_D) -> unit
+val extern_f64ToI32 = {c: "softfloat_f64toi32", ocaml: "Softfloat.f64_to_i32", lem: "softfloat_f64_to_i32"} : (bits_rm, bits_D) -> unit
val riscv_f64ToI32 : (bits_rm, bits_D) -> (bits_fflags, bits_W) effect {rreg}
function riscv_f64ToI32 (rm, v) = {
extern_f64ToI32(rm, v);
(float_fflags[4 .. 0], float_result[31 .. 0])
}
-val extern_f64ToUi32 = {c: "softfloat_f64toui32", ocaml: "Softfloat.f64_to_ui32"} : (bits_rm, bits_D) -> unit
+val extern_f64ToUi32 = {c: "softfloat_f64toui32", ocaml: "Softfloat.f64_to_ui32", lem: "softfloat_f64_to_ui32"} : (bits_rm, bits_D) -> unit
val riscv_f64ToUi32 : (bits_rm, bits_D) -> (bits_fflags, bits_WU) effect {rreg}
function riscv_f64ToUi32 (rm, v) = {
extern_f64ToUi32(rm, v);
(float_fflags[4 .. 0], float_result[31 .. 0])
}
-val extern_i32ToF64 = {c: "softfloat_i32tof64", ocaml: "Softfloat.i32_to_f64"} : (bits_rm, bits_W) -> unit
+val extern_i32ToF64 = {c: "softfloat_i32tof64", ocaml: "Softfloat.i32_to_f64", lem: "softfloat_i32_to_f64"} : (bits_rm, bits_W) -> unit
val riscv_i32ToF64 : (bits_rm, bits_W) -> (bits_fflags, bits_D) effect {rreg}
function riscv_i32ToF64 (rm, v) = {
extern_i32ToF64(rm, v);
(float_fflags[4 .. 0], float_result)
}
-val extern_ui32ToF64 = {c: "softfloat_ui32tof64", ocaml: "Softfloat.ui32_to_f64"} : (bits_rm, bits_WU) -> unit
+val extern_ui32ToF64 = {c: "softfloat_ui32tof64", ocaml: "Softfloat.ui32_to_f64", lem: "softfloat_ui32_to_f64"} : (bits_rm, bits_WU) -> unit
val riscv_ui32ToF64 : (bits_rm, bits_WU) -> (bits_fflags, bits_D) effect {rreg}
function riscv_ui32ToF64 (rm, v) = {
extern_ui32ToF64(rm, v);
(float_fflags[4 .. 0], float_result)
}
-val extern_f64ToI64 = {c: "softfloat_f64toi64", ocaml: "Softfloat.f64_to_i64"} : (bits_rm, bits_D) -> unit
+val extern_f64ToI64 = {c: "softfloat_f64toi64", ocaml: "Softfloat.f64_to_i64", lem: "softfloat_f64_to_i64"} : (bits_rm, bits_D) -> unit
val riscv_f64ToI64 : (bits_rm, bits_D) -> (bits_fflags, bits_L) effect {rreg}
function riscv_f64ToI64 (rm, v) = {
extern_f64ToI64(rm, v);
(float_fflags[4 .. 0], float_result)
}
-val extern_f64ToUi64 = {c: "softfloat_f64toui64", ocaml: "Softfloat.f64_to_ui64"} : (bits_rm, bits_D) -> unit
+val extern_f64ToUi64 = {c: "softfloat_f64toui64", ocaml: "Softfloat.f64_to_ui64", lem: "softfloat_f64_to_ui64"} : (bits_rm, bits_D) -> unit
val riscv_f64ToUi64 : (bits_rm, bits_D) -> (bits_fflags, bits_LU) effect {rreg}
function riscv_f64ToUi64 (rm, v) = {
extern_f64ToUi64(rm, v);
(float_fflags[4 .. 0], float_result)
}
-val extern_i64ToF64 = {c: "softfloat_i64tof64", ocaml: "Softfloat.i64_to_f64"} : (bits_rm, bits_L) -> unit
+val extern_i64ToF64 = {c: "softfloat_i64tof64", ocaml: "Softfloat.i64_to_f64", lem: "softfloat_i64_to_f64"} : (bits_rm, bits_L) -> unit
val riscv_i64ToF64 : (bits_rm, bits_L) -> (bits_fflags, bits_D) effect {rreg}
function riscv_i64ToF64 (rm, v) = {
extern_i64ToF64(rm, v);
(float_fflags[4 .. 0], float_result)
}
-val extern_ui64ToF64 = {c: "softfloat_ui64tof64", ocaml: "Softfloat.ui64_to_f64"} : (bits_rm, bits_LU) -> unit
+val extern_ui64ToF64 = {c: "softfloat_ui64tof64", ocaml: "Softfloat.ui64_to_f64", lem: "softfloat_ui64_to_f64"} : (bits_rm, bits_LU) -> unit
val riscv_ui64ToF64 : (bits_rm, bits_LU) -> (bits_fflags, bits_D) effect {rreg}
function riscv_ui64ToF64 (rm, v) = {
extern_ui64ToF64(rm, v);
(float_fflags[4 .. 0], float_result)
}
-val extern_f32ToF64 = {c: "softfloat_f32tof64", ocaml: "Softfloat.f32_to_f64"} : (bits_rm, bits_S) -> unit
+val extern_f32ToF64 = {c: "softfloat_f32tof64", ocaml: "Softfloat.f32_to_f64", lem: "softfloat_f32_to_f64"} : (bits_rm, bits_S) -> unit
val riscv_f32ToF64 : (bits_rm, bits_S) -> (bits_fflags, bits_D) effect {rreg}
function riscv_f32ToF64 (rm, v) = {
extern_f32ToF64(rm, v);
(float_fflags[4 .. 0], float_result)
}
-val extern_f64ToF32 = {c: "softfloat_f64tof32", ocaml: "Softfloat.f64_to_f32"} : (bits_rm, bits_D) -> unit
+val extern_f64ToF32 = {c: "softfloat_f64tof32", ocaml: "Softfloat.f64_to_f32", lem: "softfloat_f64_to_f32"} : (bits_rm, bits_D) -> unit
val riscv_f64ToF32 : (bits_rm, bits_D) -> (bits_fflags, bits_S) effect {rreg}
function riscv_f64ToF32 (rm, v) = {
extern_f64ToF32(rm, v);
generated by cgit v1.1 at 2024-07-24 09:22:53 +0000