diff options
author | Prashanth Mundkur <prashanth.mundkur@gmail.com> | 2020-01-23 12:32:54 -0800 |
---|---|---|
committer | Prashanth Mundkur <prashanth.mundkur@gmail.com> | 2020-01-23 14:17:10 -0800 |
commit | 494a5f45d91cc0d04c89f0457bdcd0af18791c45 (patch) | |
tree | dafd2f0a002a1bf10cb11d0a8e9042549fb68e05 | |
parent | 0c19e38b8ea0c3dac1a684c59e6956097bf58dc8 (diff) | |
download | sail-riscv-494a5f45d91cc0d04c89f0457bdcd0af18791c45.zip sail-riscv-494a5f45d91cc0d04c89f0457bdcd0af18791c45.tar.gz sail-riscv-494a5f45d91cc0d04c89f0457bdcd0af18791c45.tar.bz2 |
Add lem stubs for softfloat externs.rsnikhil
-rw-r--r-- | Makefile | 4 | ||||
-rw-r--r-- | handwritten_support/0.11/riscv_extras_fdext.lem | 109 | ||||
-rw-r--r-- | handwritten_support/riscv_extras_fdext.lem | 109 | ||||
-rw-r--r-- | model/riscv_softfloat_interface.sail | 60 |
4 files changed, 250 insertions, 32 deletions
@@ -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); |