From 0cab9e68ac24efce8a9ef4165319eb75b2ba38c0 Mon Sep 17 00:00:00 2001 From: Tim Hutt Date: Wed, 4 Sep 2024 15:08:54 +0100 Subject: [PATCH 1/2] Fix all Sail compilation warnings Add `pure`/`impure` annotations and remove some duplicate function declarations. --- model/prelude.sail | 38 +++----- model/riscv_platform.sail | 50 +++++----- model/riscv_softfloat_interface.sail | 132 +++++++++++++-------------- model/riscv_sys_control.sail | 8 +- model/riscv_sys_regs.sail | 30 +++--- 5 files changed, 124 insertions(+), 134 deletions(-) diff --git a/model/prelude.sail b/model/prelude.sail index 3555296b3..ea83700b7 100644 --- a/model/prelude.sail +++ b/model/prelude.sail @@ -41,47 +41,37 @@ overload BitStr = {bits_str, bit_str} overload operator ^ = {xor_vec, concat_str} -val sub_vec = {c: "sub_bits", _: "sub_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) +val sub_vec = pure {c: "sub_bits", _: "sub_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) -val sub_vec_int = {c: "sub_bits_int", _: "sub_vec_int"} : forall 'n. (bits('n), int) -> bits('n) +val sub_vec_int = pure {c: "sub_bits_int", _: "sub_vec_int"} : forall 'n. (bits('n), int) -> bits('n) overload operator - = {sub_vec, sub_vec_int} -val quot_round_zero = {ocaml: "quot_round_zero", interpreter: "quot_round_zero", lem: "hardware_quot", c: "tdiv_int", coq: "Z.quot"} : (int, int) -> int -val rem_round_zero = {ocaml: "rem_round_zero", interpreter: "rem_round_zero", lem: "hardware_mod", c: "tmod_int", coq: "Z.rem"} : (int, int) -> int +val quot_round_zero = pure {ocaml: "quot_round_zero", interpreter: "quot_round_zero", lem: "hardware_quot", c: "tdiv_int", coq: "Z.quot"} : (int, int) -> int +val rem_round_zero = pure {ocaml: "rem_round_zero", interpreter: "rem_round_zero", lem: "hardware_mod", c: "tmod_int", coq: "Z.rem"} : (int, int) -> int /* The following defines % as euclidean modulus */ overload operator % = {emod_int} -val min_int = {ocaml: "min_int", interpreter: "min_int", lem: "min", coq: "min_atom", c: "min_int"} : forall 'x 'y. - (int('x), int('y)) -> {'z, ('x <= 'y & 'z == 'x) | ('x > 'y & 'z == 'y). int('z)} - -val max_int = {ocaml: "max_int", interpreter: "max_int", lem: "max", coq: "max_atom", c: "max_int"} : forall 'x 'y. - (int('x), int('y)) -> {'z, ('x >= 'y & 'z == 'x) | ('x < 'y & 'z == 'y). int('z)} - overload min = {min_int} - overload max = {max_int} -val pow2 = "pow2" : forall 'n. int('n) -> int(2 ^ 'n) - -val print = "print_endline" : string -> unit -val print_string = "print_string" : (string, string) -> unit +val print_string = impure "print_string" : (string, string) -> unit -val print_instr = {ocaml: "Platform.print_instr", interpreter: "print_endline", c: "print_instr", lem: "print_dbg", _: "print_endline"} : string -> unit -val print_reg = {ocaml: "Platform.print_reg", interpreter: "print_endline", c: "print_reg", lem: "print_dbg", _: "print_endline"} : string -> unit -val print_mem = {ocaml: "Platform.print_mem_access", interpreter: "print_endline", c: "print_mem_access", lem: "print_dbg", _: "print_endline"} : string -> unit -val print_platform = {ocaml: "Platform.print_platform", interpreter: "print_endline", c: "print_platform", lem: "print_dbg", _: "print_endline"} : string -> unit +val print_instr = impure {ocaml: "Platform.print_instr", interpreter: "print_endline", c: "print_instr", lem: "print_dbg", _: "print_endline"} : string -> unit +val print_reg = impure {ocaml: "Platform.print_reg", interpreter: "print_endline", c: "print_reg", lem: "print_dbg", _: "print_endline"} : string -> unit +val print_mem = impure {ocaml: "Platform.print_mem_access", interpreter: "print_endline", c: "print_mem_access", lem: "print_dbg", _: "print_endline"} : string -> unit +val print_platform = impure {ocaml: "Platform.print_platform", interpreter: "print_endline", c: "print_platform", lem: "print_dbg", _: "print_endline"} : string -> unit -val print_step = {ocaml: "Platform.print_step", c: "print_step"} : unit -> unit +val print_step = impure {ocaml: "Platform.print_step", c: "print_step"} : unit -> unit function print_step() = () -val get_config_print_instr = {ocaml: "Platform.get_config_print_instr", c:"get_config_print_instr"} : unit -> bool -val get_config_print_reg = {ocaml: "Platform.get_config_print_reg", c:"get_config_print_reg"} : unit -> bool -val get_config_print_mem = {ocaml: "Platform.get_config_print_mem", c:"get_config_print_mem"} : unit -> bool +val get_config_print_instr = pure {ocaml: "Platform.get_config_print_instr", c:"get_config_print_instr"} : unit -> bool +val get_config_print_reg = pure {ocaml: "Platform.get_config_print_reg", c:"get_config_print_reg"} : unit -> bool +val get_config_print_mem = pure {ocaml: "Platform.get_config_print_mem", c:"get_config_print_mem"} : unit -> bool -val get_config_print_platform = {ocaml: "Platform.get_config_print_platform", c:"get_config_print_platform"} : unit -> bool +val get_config_print_platform = pure {ocaml: "Platform.get_config_print_platform", c:"get_config_print_platform"} : unit -> bool // defaults for other backends function get_config_print_instr () = false function get_config_print_reg () = false diff --git a/model/riscv_platform.sail b/model/riscv_platform.sail index 2dc6e7528..b7a498c59 100644 --- a/model/riscv_platform.sail +++ b/model/riscv_platform.sail @@ -14,13 +14,13 @@ - it relies on externs to get platform address information and doesn't hardcode them */ -val elf_tohost = { +val elf_tohost = pure { ocaml: "Elf_loader.elf_tohost", interpreter: "Elf_loader.elf_tohost", c: "elf_tohost" } : unit -> int -val elf_entry = { +val elf_entry = pure { ocaml: "Elf_loader.elf_entry", interpreter: "Elf_loader.elf_entry", c: "elf_entry" @@ -29,42 +29,42 @@ val elf_entry = { // Cache block size is 2^cache_block_size_exp. Max is `max_mem_access` (4096) // because this model performs `cbo.zero` with a single write, and the behaviour // with cache blocks larger than a page is not clearly defined. -val plat_cache_block_size_exp = {c: "plat_cache_block_size_exp", ocaml: "Platform.cache_block_size_exp", interpreter: "Platform.cache_block_size_exp", lem: "plat_cache_block_size_exp"} : unit -> range(0, 12) +val plat_cache_block_size_exp = pure {c: "plat_cache_block_size_exp", ocaml: "Platform.cache_block_size_exp", interpreter: "Platform.cache_block_size_exp", lem: "plat_cache_block_size_exp"} : unit -> range(0, 12) /* Main memory */ -val plat_ram_base = {c: "plat_ram_base", ocaml: "Platform.dram_base", interpreter: "Platform.dram_base", lem: "plat_ram_base"} : unit -> xlenbits -val plat_ram_size = {c: "plat_ram_size", ocaml: "Platform.dram_size", interpreter: "Platform.dram_size", lem: "plat_ram_size"} : unit -> xlenbits +val plat_ram_base = pure {c: "plat_ram_base", ocaml: "Platform.dram_base", interpreter: "Platform.dram_base", lem: "plat_ram_base"} : unit -> xlenbits +val plat_ram_size = pure {c: "plat_ram_size", ocaml: "Platform.dram_size", interpreter: "Platform.dram_size", lem: "plat_ram_size"} : unit -> xlenbits /* whether the MMU should update dirty bits in PTEs */ -val plat_enable_dirty_update = {ocaml: "Platform.enable_dirty_update", - interpreter: "Platform.enable_dirty_update", - c: "plat_enable_dirty_update", - lem: "plat_enable_dirty_update"} : unit -> bool +val plat_enable_dirty_update = pure {ocaml: "Platform.enable_dirty_update", + interpreter: "Platform.enable_dirty_update", + c: "plat_enable_dirty_update", + lem: "plat_enable_dirty_update"} : unit -> bool /* whether the platform supports misaligned accesses without trapping to M-mode. if false, * misaligned loads/stores are trapped to Machine mode. */ -val plat_enable_misaligned_access = {ocaml: "Platform.enable_misaligned_access", - interpreter: "Platform.enable_misaligned_access", - c: "plat_enable_misaligned_access", - lem: "plat_enable_misaligned_access"} : unit -> bool +val plat_enable_misaligned_access = pure {ocaml: "Platform.enable_misaligned_access", + interpreter: "Platform.enable_misaligned_access", + c: "plat_enable_misaligned_access", + lem: "plat_enable_misaligned_access"} : unit -> bool /* whether mtval stores the bits of a faulting instruction on illegal instruction exceptions */ -val plat_mtval_has_illegal_inst_bits = {ocaml: "Platform.mtval_has_illegal_inst_bits", - interpreter: "Platform.mtval_has_illegal_inst_bits", - c: "plat_mtval_has_illegal_inst_bits", - lem: "plat_mtval_has_illegal_inst_bits"} : unit -> bool +val plat_mtval_has_illegal_inst_bits = pure {ocaml: "Platform.mtval_has_illegal_inst_bits", + interpreter: "Platform.mtval_has_illegal_inst_bits", + c: "plat_mtval_has_illegal_inst_bits", + lem: "plat_mtval_has_illegal_inst_bits"} : unit -> bool /* ROM holding reset vector and device-tree DTB */ -val plat_rom_base = {ocaml: "Platform.rom_base", interpreter: "Platform.rom_base", c: "plat_rom_base", lem: "plat_rom_base"} : unit -> xlenbits -val plat_rom_size = {ocaml: "Platform.rom_size", interpreter: "Platform.rom_size", c: "plat_rom_size", lem: "plat_rom_size"} : unit -> xlenbits +val plat_rom_base = pure {ocaml: "Platform.rom_base", interpreter: "Platform.rom_base", c: "plat_rom_base", lem: "plat_rom_base"} : unit -> xlenbits +val plat_rom_size = pure {ocaml: "Platform.rom_size", interpreter: "Platform.rom_size", c: "plat_rom_size", lem: "plat_rom_size"} : unit -> xlenbits /* Location of clock-interface, which should match with the spec in the DTB */ -val plat_clint_base = {ocaml: "Platform.clint_base", interpreter: "Platform.clint_base", c: "plat_clint_base", lem: "plat_clint_base"} : unit -> xlenbits -val plat_clint_size = {ocaml: "Platform.clint_size", interpreter: "Platform.clint_size", c: "plat_clint_size", lem: "plat_clint_size"} : unit -> xlenbits +val plat_clint_base = pure {ocaml: "Platform.clint_base", interpreter: "Platform.clint_base", c: "plat_clint_base", lem: "plat_clint_base"} : unit -> xlenbits +val plat_clint_size = pure {ocaml: "Platform.clint_size", interpreter: "Platform.clint_size", c: "plat_clint_size", lem: "plat_clint_size"} : unit -> xlenbits /* Location of HTIF ports */ -val plat_htif_tohost = {ocaml: "Platform.htif_tohost", c: "plat_htif_tohost", lem: "plat_htif_tohost"} : unit -> xlenbits +val plat_htif_tohost = pure {ocaml: "Platform.htif_tohost", c: "plat_htif_tohost", lem: "plat_htif_tohost"} : unit -> xlenbits function plat_htif_tohost () = to_bits(sizeof(xlen), elf_tohost ()) // todo: fromhost @@ -124,7 +124,7 @@ function within_htif_readable forall 'n, 0 < 'n <= max_mem_access . (addr : xlen /* CLINT (Core Local Interruptor), based on Spike. */ -val plat_insns_per_tick = {ocaml: "Platform.insns_per_tick", interpreter: "Platform.insns_per_tick", c: "plat_insns_per_tick", lem: "plat_insns_per_tick"} : unit -> int +val plat_insns_per_tick = pure {ocaml: "Platform.insns_per_tick", interpreter: "Platform.insns_per_tick", c: "plat_insns_per_tick", lem: "plat_insns_per_tick"} : unit -> int // assumes a single hart, since this typically is a vector of per-hart registers. register mtimecmp : bits(64) // memory-mapped internal clint register. @@ -284,8 +284,8 @@ function tick_clock() = { /* Basic terminal character I/O. */ -val plat_term_write = {ocaml: "Platform.term_write", c: "plat_term_write", lem: "plat_term_write"} : bits(8) -> unit -val plat_term_read = {ocaml: "Platform.term_read", c: "plat_term_read", lem: "plat_term_read"} : unit -> bits(8) +val plat_term_write = impure {ocaml: "Platform.term_write", c: "plat_term_write", lem: "plat_term_write"} : bits(8) -> unit +val plat_term_read = impure {ocaml: "Platform.term_read", c: "plat_term_read", lem: "plat_term_read"} : unit -> bits(8) /* Spike's HTIF device interface, which multiplexes the above MMIO devices. */ diff --git a/model/riscv_softfloat_interface.sail b/model/riscv_softfloat_interface.sail index 3a673feb8..79a46784c 100644 --- a/model/riscv_softfloat_interface.sail +++ b/model/riscv_softfloat_interface.sail @@ -47,84 +47,84 @@ register float_fflags : bits(64) /* **************************************************************** */ /* ADD/SUB/MUL/DIV */ -val extern_f16Add = {c: "softfloat_f16add", ocaml: "Softfloat.f16_add", lem: "softfloat_f16_add"} : (bits_rm, bits_H, bits_H) -> unit +val extern_f16Add = pure {c: "softfloat_f16add", ocaml: "Softfloat.f16_add", lem: "softfloat_f16_add"} : (bits_rm, bits_H, bits_H) -> unit val riscv_f16Add : (bits_rm, bits_H, bits_H) -> (bits_fflags, bits_H) function riscv_f16Add (rm, v1, v2) = { extern_f16Add(rm, v1, v2); (float_fflags[4 .. 0], float_result[15 .. 0]) } -val extern_f16Sub = {c: "softfloat_f16sub", ocaml: "Softfloat.f16_sub", lem: "softfloat_f16_sub"} : (bits_rm, bits_H, bits_H) -> unit +val extern_f16Sub = pure {c: "softfloat_f16sub", ocaml: "Softfloat.f16_sub", lem: "softfloat_f16_sub"} : (bits_rm, bits_H, bits_H) -> unit val riscv_f16Sub : (bits_rm, bits_H, bits_H) -> (bits_fflags, bits_H) function riscv_f16Sub (rm, v1, v2) = { extern_f16Sub(rm, v1, v2); (float_fflags[4 .. 0], float_result[15 .. 0]) } -val extern_f16Mul = {c: "softfloat_f16mul", ocaml: "Softfloat.f16_mul", lem: "softfloat_f16_mul"} : (bits_rm, bits_H, bits_H) -> unit +val extern_f16Mul = pure {c: "softfloat_f16mul", ocaml: "Softfloat.f16_mul", lem: "softfloat_f16_mul"} : (bits_rm, bits_H, bits_H) -> unit val riscv_f16Mul : (bits_rm, bits_H, bits_H) -> (bits_fflags, bits_H) function riscv_f16Mul (rm, v1, v2) = { extern_f16Mul(rm, v1, v2); (float_fflags[4 .. 0], float_result[15 .. 0]) } -val extern_f16Div = {c: "softfloat_f16div", ocaml: "Softfloat.f16_div", lem: "softfloat_f16_div"} : (bits_rm, bits_H, bits_H) -> unit +val extern_f16Div = pure {c: "softfloat_f16div", ocaml: "Softfloat.f16_div", lem: "softfloat_f16_div"} : (bits_rm, bits_H, bits_H) -> unit val riscv_f16Div : (bits_rm, bits_H, bits_H) -> (bits_fflags, bits_H) function riscv_f16Div (rm, v1, v2) = { extern_f16Div(rm, v1, v2); (float_fflags[4 .. 0], float_result[15 .. 0]) } -val extern_f32Add = {c: "softfloat_f32add", ocaml: "Softfloat.f32_add", lem: "softfloat_f32_add"} : (bits_rm, bits_S, bits_S) -> unit +val extern_f32Add = pure {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) 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", lem: "softfloat_f32_sub"} : (bits_rm, bits_S, bits_S) -> unit +val extern_f32Sub = pure {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) 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", lem: "softfloat_f32_mul"} : (bits_rm, bits_S, bits_S) -> unit +val extern_f32Mul = pure {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) 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", lem: "softfloat_f32_div"} : (bits_rm, bits_S, bits_S) -> unit +val extern_f32Div = pure {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) 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", lem: "softfloat_f64_add"} : (bits_rm, bits_D, bits_D) -> unit +val extern_f64Add = pure {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) 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", lem: "softfloat_f64_sub"} : (bits_rm, bits_D, bits_D) -> unit +val extern_f64Sub = pure {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) 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", lem: "softfloat_f64_mul"} : (bits_rm, bits_D, bits_D) -> unit +val extern_f64Mul = pure {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) 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", lem: "softfloat_f64_div"} : (bits_rm, bits_D, bits_D) -> unit +val extern_f64Div = pure {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) function riscv_f64Div (rm, v1, v2) = { extern_f64Div(rm, v1, v2); @@ -134,21 +134,21 @@ function riscv_f64Div (rm, v1, v2) = { /* **************************************************************** */ /* MULTIPLY-ADD */ -val extern_f16MulAdd = {c: "softfloat_f16muladd", ocaml: "Softfloat.f16_muladd", lem: "softfloat_f16_muladd"} : (bits_rm, bits_H, bits_H, bits_H) -> unit +val extern_f16MulAdd = pure {c: "softfloat_f16muladd", ocaml: "Softfloat.f16_muladd", lem: "softfloat_f16_muladd"} : (bits_rm, bits_H, bits_H, bits_H) -> unit val riscv_f16MulAdd : (bits_rm, bits_H, bits_H, bits_H) -> (bits_fflags, bits_H) function riscv_f16MulAdd (rm, v1, v2, v3) = { extern_f16MulAdd(rm, v1, v2, v3); (float_fflags[4 .. 0], float_result[15 .. 0]) } -val extern_f32MulAdd = {c: "softfloat_f32muladd", ocaml: "Softfloat.f32_muladd", lem: "softfloat_f32_muladd"} : (bits_rm, bits_S, bits_S, bits_S) -> unit +val extern_f32MulAdd = pure {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) 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", lem: "softfloat_f64_muladd"} : (bits_rm, bits_D, bits_D, bits_D) -> unit +val extern_f64MulAdd = pure {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) function riscv_f64MulAdd (rm, v1, v2, v3) = { extern_f64MulAdd(rm, v1, v2, v3); @@ -158,21 +158,21 @@ function riscv_f64MulAdd (rm, v1, v2, v3) = { /* **************************************************************** */ /* SQUARE ROOT */ -val extern_f16Sqrt = {c: "softfloat_f16sqrt", ocaml: "Softfloat.f16_sqrt", lem: "softfloat_f16_sqrt"} : (bits_rm, bits_H) -> unit +val extern_f16Sqrt = pure {c: "softfloat_f16sqrt", ocaml: "Softfloat.f16_sqrt", lem: "softfloat_f16_sqrt"} : (bits_rm, bits_H) -> unit val riscv_f16Sqrt : (bits_rm, bits_H) -> (bits_fflags, bits_H) function riscv_f16Sqrt (rm, v) = { extern_f16Sqrt(rm, v); (float_fflags[4 .. 0], float_result[15 .. 0]) } -val extern_f32Sqrt = {c: "softfloat_f32sqrt", ocaml: "Softfloat.f32_sqrt", lem: "softfloat_f32_sqrt"} : (bits_rm, bits_S) -> unit +val extern_f32Sqrt = pure {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) 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", lem: "softfloat_f64_sqrt"} : (bits_rm, bits_D) -> unit +val extern_f64Sqrt = pure {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) function riscv_f64Sqrt (rm, v) = { extern_f64Sqrt(rm, v); @@ -182,56 +182,56 @@ function riscv_f64Sqrt (rm, v) = { /* **************************************************************** */ /* CONVERSIONS */ -val extern_f16ToI32 = {c: "softfloat_f16toi32", ocaml: "Softfloat.f16_to_i32", lem: "softfloat_f16_to_i32"} : (bits_rm, bits_H) -> unit +val extern_f16ToI32 = pure {c: "softfloat_f16toi32", ocaml: "Softfloat.f16_to_i32", lem: "softfloat_f16_to_i32"} : (bits_rm, bits_H) -> unit val riscv_f16ToI32 : (bits_rm, bits_H) -> (bits_fflags, bits_W) function riscv_f16ToI32 (rm, v) = { extern_f16ToI32(rm, v); (float_fflags[4 .. 0], float_result[31 .. 0]) } -val extern_f16ToUi32 = {c: "softfloat_f16toui32", ocaml: "Softfloat.f16_to_ui32", lem: "softfloat_f16_to_ui32"} : (bits_rm, bits_H) -> unit +val extern_f16ToUi32 = pure {c: "softfloat_f16toui32", ocaml: "Softfloat.f16_to_ui32", lem: "softfloat_f16_to_ui32"} : (bits_rm, bits_H) -> unit val riscv_f16ToUi32 : (bits_rm, bits_H) -> (bits_fflags, bits_WU) function riscv_f16ToUi32 (rm, v) = { extern_f16ToUi32(rm, v); (float_fflags[4 .. 0], float_result[31 .. 0]) } -val extern_i32ToF16 = {c: "softfloat_i32tof16", ocaml: "Softfloat.i32_to_f16", lem: "softfloat_i32_to_f16"} : (bits_rm, bits_W) -> unit +val extern_i32ToF16 = pure {c: "softfloat_i32tof16", ocaml: "Softfloat.i32_to_f16", lem: "softfloat_i32_to_f16"} : (bits_rm, bits_W) -> unit val riscv_i32ToF16 : (bits_rm, bits_W) -> (bits_fflags, bits_H) function riscv_i32ToF16 (rm, v) = { extern_i32ToF16(rm, v); (float_fflags[4 .. 0], float_result[15 .. 0]) } -val extern_ui32ToF16 = {c: "softfloat_ui32tof16", ocaml: "Softfloat.ui32_to_f16", lem: "softfloat_ui32_to_f16"} : (bits_rm, bits_WU) -> unit +val extern_ui32ToF16 = pure {c: "softfloat_ui32tof16", ocaml: "Softfloat.ui32_to_f16", lem: "softfloat_ui32_to_f16"} : (bits_rm, bits_WU) -> unit val riscv_ui32ToF16 : (bits_rm, bits_WU) -> (bits_fflags, bits_H) function riscv_ui32ToF16 (rm, v) = { extern_ui32ToF16(rm, v); (float_fflags[4 .. 0], float_result[15 .. 0]) } -val extern_f16ToI64 = {c: "softfloat_f16toi64", ocaml: "Softfloat.f16_to_i64", lem: "softfloat_f16_to_i64"} : (bits_rm, bits_H) -> unit +val extern_f16ToI64 = pure {c: "softfloat_f16toi64", ocaml: "Softfloat.f16_to_i64", lem: "softfloat_f16_to_i64"} : (bits_rm, bits_H) -> unit val riscv_f16ToI64 : (bits_rm, bits_H) -> (bits_fflags, bits_L) function riscv_f16ToI64 (rm, v) = { extern_f16ToI64(rm, v); (float_fflags[4 .. 0], float_result) } -val extern_f16ToUi64 = {c: "softfloat_f16toui64", ocaml: "Softfloat.f16_to_ui64", lem: "softfloat_f16_to_ui64"} : (bits_rm, bits_H) -> unit +val extern_f16ToUi64 = pure {c: "softfloat_f16toui64", ocaml: "Softfloat.f16_to_ui64", lem: "softfloat_f16_to_ui64"} : (bits_rm, bits_H) -> unit val riscv_f16ToUi64 : (bits_rm, bits_H) -> (bits_fflags, bits_LU) function riscv_f16ToUi64 (rm, v) = { extern_f16ToUi64(rm, v); (float_fflags[4 .. 0], float_result) } -val extern_i64ToF16 = {c: "softfloat_i64tof16", ocaml: "Softfloat.i64_to_f16", lem: "softfloat_i64_to_f16"} : (bits_rm, bits_L) -> unit +val extern_i64ToF16 = pure {c: "softfloat_i64tof16", ocaml: "Softfloat.i64_to_f16", lem: "softfloat_i64_to_f16"} : (bits_rm, bits_L) -> unit val riscv_i64ToF16 : (bits_rm, bits_L) -> (bits_fflags, bits_H) function riscv_i64ToF16 (rm, v) = { extern_i64ToF16(rm, v); (float_fflags[4 .. 0], float_result[15 .. 0]) } -val extern_ui64ToF16 = {c: "softfloat_ui64tof16", ocaml: "Softfloat.ui64_to_f16", lem: "softfloat_ui64_to_f16"} : (bits_rm, bits_L) -> unit +val extern_ui64ToF16 = pure {c: "softfloat_ui64tof16", ocaml: "Softfloat.ui64_to_f16", lem: "softfloat_ui64_to_f16"} : (bits_rm, bits_L) -> unit val riscv_ui64ToF16 : (bits_rm, bits_LU) -> (bits_fflags, bits_H) function riscv_ui64ToF16 (rm, v) = { extern_ui64ToF16(rm, v); @@ -239,154 +239,154 @@ function riscv_ui64ToF16 (rm, v) = { } -val extern_f32ToI32 = {c: "softfloat_f32toi32", ocaml: "Softfloat.f32_to_i32", lem: "softfloat_f32_to_i32"} : (bits_rm, bits_S) -> unit +val extern_f32ToI32 = pure {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) 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", lem: "softfloat_f32_to_ui32"} : (bits_rm, bits_S) -> unit +val extern_f32ToUi32 = pure {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) 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", lem: "softfloat_i32_to_f32"} : (bits_rm, bits_W) -> unit +val extern_i32ToF32 = pure {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) 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", lem: "softfloat_ui32_to_f32"} : (bits_rm, bits_WU) -> unit +val extern_ui32ToF32 = pure {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) 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", lem: "softfloat_f32_to_i64"} : (bits_rm, bits_S) -> unit +val extern_f32ToI64 = pure {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) 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", lem: "softfloat_f32_to_ui64"} : (bits_rm, bits_S) -> unit +val extern_f32ToUi64 = pure {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) 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", lem: "softfloat_i64_to_f32"} : (bits_rm, bits_L) -> unit +val extern_i64ToF32 = pure {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) 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", lem: "softfloat_ui64_to_f32"} : (bits_rm, bits_L) -> unit +val extern_ui64ToF32 = pure {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) 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", lem: "softfloat_f64_to_i32"} : (bits_rm, bits_D) -> unit +val extern_f64ToI32 = pure {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) 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", lem: "softfloat_f64_to_ui32"} : (bits_rm, bits_D) -> unit +val extern_f64ToUi32 = pure {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) 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", lem: "softfloat_i32_to_f64"} : (bits_rm, bits_W) -> unit +val extern_i32ToF64 = pure {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) 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", lem: "softfloat_ui32_to_f64"} : (bits_rm, bits_WU) -> unit +val extern_ui32ToF64 = pure {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) 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", lem: "softfloat_f64_to_i64"} : (bits_rm, bits_D) -> unit +val extern_f64ToI64 = pure {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) 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", lem: "softfloat_f64_to_ui64"} : (bits_rm, bits_D) -> unit +val extern_f64ToUi64 = pure {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) 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", lem: "softfloat_i64_to_f64"} : (bits_rm, bits_L) -> unit +val extern_i64ToF64 = pure {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) 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", lem: "softfloat_ui64_to_f64"} : (bits_rm, bits_LU) -> unit +val extern_ui64ToF64 = pure {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) function riscv_ui64ToF64 (rm, v) = { extern_ui64ToF64(rm, v); (float_fflags[4 .. 0], float_result) } -val extern_f16ToF32 = {c: "softfloat_f16tof32", ocaml: "Softfloat.f16_to_f32", lem: "softfloat_f16_to_f32"} : (bits_rm, bits_H) -> unit +val extern_f16ToF32 = pure {c: "softfloat_f16tof32", ocaml: "Softfloat.f16_to_f32", lem: "softfloat_f16_to_f32"} : (bits_rm, bits_H) -> unit val riscv_f16ToF32 : (bits_rm, bits_H) -> (bits_fflags, bits_S) function riscv_f16ToF32 (rm, v) = { extern_f16ToF32(rm, v); (float_fflags[4 .. 0], float_result[31 .. 0]) } -val extern_f16ToF64 = {c: "softfloat_f16tof64", ocaml: "Softfloat.f16_to_f64", lem: "softfloat_f16_to_f64"} : (bits_rm, bits_H) -> unit +val extern_f16ToF64 = pure {c: "softfloat_f16tof64", ocaml: "Softfloat.f16_to_f64", lem: "softfloat_f16_to_f64"} : (bits_rm, bits_H) -> unit val riscv_f16ToF64 : (bits_rm, bits_H) -> (bits_fflags, bits_D) function riscv_f16ToF64 (rm, v) = { extern_f16ToF64(rm, v); (float_fflags[4 .. 0], float_result) } -val extern_f32ToF64 = {c: "softfloat_f32tof64", ocaml: "Softfloat.f32_to_f64", lem: "softfloat_f32_to_f64"} : (bits_rm, bits_S) -> unit +val extern_f32ToF64 = pure {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) function riscv_f32ToF64 (rm, v) = { extern_f32ToF64(rm, v); (float_fflags[4 .. 0], float_result) } -val extern_f32ToF16 = {c: "softfloat_f32tof16", ocaml: "Softfloat.f32_to_f16", lem: "softfloat_f32_to_f16"} : (bits_rm, bits_S) -> unit +val extern_f32ToF16 = pure {c: "softfloat_f32tof16", ocaml: "Softfloat.f32_to_f16", lem: "softfloat_f32_to_f16"} : (bits_rm, bits_S) -> unit val riscv_f32ToF16 : (bits_rm, bits_S) -> (bits_fflags, bits_H) function riscv_f32ToF16 (rm, v) = { extern_f32ToF16(rm, v); (float_fflags[4 .. 0], float_result[15 .. 0]) } -val extern_f64ToF16 = {c: "softfloat_f64tof16", ocaml: "Softfloat.f64_to_f16", lem: "softfloat_f64_to_f16"} : (bits_rm, bits_D) -> unit +val extern_f64ToF16 = pure {c: "softfloat_f64tof16", ocaml: "Softfloat.f64_to_f16", lem: "softfloat_f64_to_f16"} : (bits_rm, bits_D) -> unit val riscv_f64ToF16 : (bits_rm, bits_D) -> (bits_fflags, bits_H) function riscv_f64ToF16 (rm, v) = { extern_f64ToF16(rm, v); (float_fflags[4 .. 0], float_result[15 .. 0]) } -val extern_f64ToF32 = {c: "softfloat_f64tof32", ocaml: "Softfloat.f64_to_f32", lem: "softfloat_f64_to_f32"} : (bits_rm, bits_D) -> unit +val extern_f64ToF32 = pure {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) function riscv_f64ToF32 (rm, v) = { extern_f64ToF32(rm, v); @@ -396,126 +396,126 @@ function riscv_f64ToF32 (rm, v) = { /* **************************************************************** */ /* COMPARISONS */ -val extern_f16Lt = {c: "softfloat_f16lt", ocaml: "Softfloat.f16_lt", lem: "softfloat_f16_lt"} : (bits_H, bits_H) -> unit +val extern_f16Lt = pure {c: "softfloat_f16lt", ocaml: "Softfloat.f16_lt", lem: "softfloat_f16_lt"} : (bits_H, bits_H) -> unit val riscv_f16Lt : (bits_H, bits_H) -> (bits_fflags, bool) function riscv_f16Lt (v1, v2) = { extern_f16Lt(v1, v2); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } -val extern_f16Lt_quiet = {c: "softfloat_f16lt_quiet", ocaml: "Softfloat.f16_lt_quiet", lem: "softfloat_f16_lt_quiet"} : (bits_H, bits_H) -> unit +val extern_f16Lt_quiet = pure {c: "softfloat_f16lt_quiet", ocaml: "Softfloat.f16_lt_quiet", lem: "softfloat_f16_lt_quiet"} : (bits_H, bits_H) -> unit val riscv_f16Lt_quiet : (bits_H, bits_H) -> (bits_fflags, bool) function riscv_f16Lt_quiet (v1, v2) = { extern_f16Lt_quiet(v1, v2); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } -val extern_f16Le = {c: "softfloat_f16le", ocaml: "Softfloat.f16_le", lem: "softfloat_f16_le"} : (bits_H, bits_H) -> unit +val extern_f16Le = pure {c: "softfloat_f16le", ocaml: "Softfloat.f16_le", lem: "softfloat_f16_le"} : (bits_H, bits_H) -> unit val riscv_f16Le : (bits_H, bits_H) -> (bits_fflags, bool) function riscv_f16Le (v1, v2) = { extern_f16Le(v1, v2); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } -val extern_f16Le_quiet = {c: "softfloat_f16le_quiet", ocaml: "Softfloat.f16_le_quiet", lem: "softfloat_f16_le_quiet"} : (bits_H, bits_H) -> unit +val extern_f16Le_quiet = pure {c: "softfloat_f16le_quiet", ocaml: "Softfloat.f16_le_quiet", lem: "softfloat_f16_le_quiet"} : (bits_H, bits_H) -> unit val riscv_f16Le_quiet : (bits_H, bits_H) -> (bits_fflags, bool) function riscv_f16Le_quiet (v1, v2) = { extern_f16Le_quiet(v1, v2); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } -val extern_f16Eq = {c: "softfloat_f16eq", ocaml: "Softfloat.f16_eq", lem: "softfloat_f16_eq"} : (bits_H, bits_H) -> unit +val extern_f16Eq = pure {c: "softfloat_f16eq", ocaml: "Softfloat.f16_eq", lem: "softfloat_f16_eq"} : (bits_H, bits_H) -> unit val riscv_f16Eq : (bits_H, bits_H) -> (bits_fflags, bool) function riscv_f16Eq (v1, v2) = { extern_f16Eq(v1, v2); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } -val extern_f32Lt = {c: "softfloat_f32lt", ocaml: "Softfloat.f32_lt", lem: "softfloat_f32_lt"} : (bits_S, bits_S) -> unit +val extern_f32Lt = pure {c: "softfloat_f32lt", ocaml: "Softfloat.f32_lt", lem: "softfloat_f32_lt"} : (bits_S, bits_S) -> unit val riscv_f32Lt : (bits_S, bits_S) -> (bits_fflags, bool) function riscv_f32Lt (v1, v2) = { extern_f32Lt(v1, v2); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } -val extern_f32Lt_quiet = {c: "softfloat_f32lt_quiet", ocaml: "Softfloat.f32_lt_quiet", lem: "softfloat_f32_lt_quiet"} : (bits_S, bits_S) -> unit +val extern_f32Lt_quiet = pure {c: "softfloat_f32lt_quiet", ocaml: "Softfloat.f32_lt_quiet", lem: "softfloat_f32_lt_quiet"} : (bits_S, bits_S) -> unit val riscv_f32Lt_quiet : (bits_S, bits_S) -> (bits_fflags, bool) function riscv_f32Lt_quiet (v1, v2) = { extern_f32Lt_quiet(v1, v2); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } -val extern_f32Le = {c: "softfloat_f32le", ocaml: "Softfloat.f32_le", lem: "softfloat_f32_le"} : (bits_S, bits_S) -> unit +val extern_f32Le = pure {c: "softfloat_f32le", ocaml: "Softfloat.f32_le", lem: "softfloat_f32_le"} : (bits_S, bits_S) -> unit val riscv_f32Le : (bits_S, bits_S) -> (bits_fflags, bool) function riscv_f32Le (v1, v2) = { extern_f32Le(v1, v2); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } -val extern_f32Le_quiet = {c: "softfloat_f32le_quiet", ocaml: "Softfloat.f32_le_quiet", lem: "softfloat_f32_le_quiet"} : (bits_S, bits_S) -> unit +val extern_f32Le_quiet = pure {c: "softfloat_f32le_quiet", ocaml: "Softfloat.f32_le_quiet", lem: "softfloat_f32_le_quiet"} : (bits_S, bits_S) -> unit val riscv_f32Le_quiet : (bits_S, bits_S) -> (bits_fflags, bool) function riscv_f32Le_quiet (v1, v2) = { extern_f32Le_quiet(v1, v2); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } -val extern_f32Eq = {c: "softfloat_f32eq", ocaml: "Softfloat.f32_eq", lem: "softfloat_f32_eq"} : (bits_S, bits_S) -> unit +val extern_f32Eq = pure {c: "softfloat_f32eq", ocaml: "Softfloat.f32_eq", lem: "softfloat_f32_eq"} : (bits_S, bits_S) -> unit val riscv_f32Eq : (bits_S, bits_S) -> (bits_fflags, bool) function riscv_f32Eq (v1, v2) = { extern_f32Eq(v1, v2); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } -val extern_f64Lt = {c: "softfloat_f64lt", ocaml: "Softfloat.f64_lt", lem: "softfloat_f64_lt"} : (bits_D, bits_D) -> unit +val extern_f64Lt = pure {c: "softfloat_f64lt", ocaml: "Softfloat.f64_lt", lem: "softfloat_f64_lt"} : (bits_D, bits_D) -> unit val riscv_f64Lt : (bits_D, bits_D) -> (bits_fflags, bool) function riscv_f64Lt (v1, v2) = { extern_f64Lt(v1, v2); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } -val extern_f64Lt_quiet = {c: "softfloat_f64lt_quiet", ocaml: "Softfloat.f64_lt_quiet", lem: "softfloat_f64_lt_quiet"} : (bits_D, bits_D) -> unit +val extern_f64Lt_quiet = pure {c: "softfloat_f64lt_quiet", ocaml: "Softfloat.f64_lt_quiet", lem: "softfloat_f64_lt_quiet"} : (bits_D, bits_D) -> unit val riscv_f64Lt_quiet : (bits_D, bits_D) -> (bits_fflags, bool) function riscv_f64Lt_quiet (v1, v2) = { extern_f64Lt_quiet(v1, v2); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } -val extern_f64Le = {c: "softfloat_f64le", ocaml: "Softfloat.f64_le", lem: "softfloat_f64_le"} : (bits_D, bits_D) -> unit +val extern_f64Le = pure {c: "softfloat_f64le", ocaml: "Softfloat.f64_le", lem: "softfloat_f64_le"} : (bits_D, bits_D) -> unit val riscv_f64Le : (bits_D, bits_D) -> (bits_fflags, bool) function riscv_f64Le (v1, v2) = { extern_f64Le(v1, v2); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } -val extern_f64Le_quiet = {c: "softfloat_f64le_quiet", ocaml: "Softfloat.f64_le_quiet", lem: "softfloat_f64_le_quiet"} : (bits_D, bits_D) -> unit +val extern_f64Le_quiet = pure {c: "softfloat_f64le_quiet", ocaml: "Softfloat.f64_le_quiet", lem: "softfloat_f64_le_quiet"} : (bits_D, bits_D) -> unit val riscv_f64Le_quiet : (bits_D, bits_D) -> (bits_fflags, bool) function riscv_f64Le_quiet (v1, v2) = { extern_f64Le_quiet(v1, v2); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } -val extern_f64Eq = {c: "softfloat_f64eq", ocaml: "Softfloat.f64_eq", lem: "softfloat_f64_eq"} : (bits_D, bits_D) -> unit +val extern_f64Eq = pure {c: "softfloat_f64eq", ocaml: "Softfloat.f64_eq", lem: "softfloat_f64_eq"} : (bits_D, bits_D) -> unit val riscv_f64Eq : (bits_D, bits_D) -> (bits_fflags, bool) function riscv_f64Eq (v1, v2) = { extern_f64Eq(v1, v2); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } -val extern_f16roundToInt = {c: "softfloat_f16roundToInt", ocaml: "Softfloat.f16_round_to_int", lem: "softfloat_f16_round_to_int"} : (bits_rm, bits_H, bool) -> unit +val extern_f16roundToInt = pure {c: "softfloat_f16roundToInt", ocaml: "Softfloat.f16_round_to_int", lem: "softfloat_f16_round_to_int"} : (bits_rm, bits_H, bool) -> unit val riscv_f16roundToInt : (bits_rm, bits_H, bool) -> (bits_fflags, bits_H) function riscv_f16roundToInt (rm, v, exact) = { extern_f16roundToInt(rm, v, exact); (float_fflags[4 .. 0], float_result[15 .. 0]) } -val extern_f32roundToInt = {c: "softfloat_f32roundToInt", ocaml: "Softfloat.f32_round_to_int", lem: "softfloat_f32_round_to_int"} : (bits_rm, bits_S, bool) -> unit +val extern_f32roundToInt = pure {c: "softfloat_f32roundToInt", ocaml: "Softfloat.f32_round_to_int", lem: "softfloat_f32_round_to_int"} : (bits_rm, bits_S, bool) -> unit val riscv_f32roundToInt : (bits_rm, bits_S, bool) -> (bits_fflags, bits_S) function riscv_f32roundToInt (rm, v, exact) = { extern_f32roundToInt(rm, v, exact); (float_fflags[4 .. 0], float_result[31 .. 0]) } -val extern_f64roundToInt = {c: "softfloat_f64roundToInt", ocaml: "Softfloat.f64_round_to_int", lem: "softfloat_f64_round_to_int"} : (bits_rm, bits_D, bool) -> unit +val extern_f64roundToInt = pure {c: "softfloat_f64roundToInt", ocaml: "Softfloat.f64_round_to_int", lem: "softfloat_f64_round_to_int"} : (bits_rm, bits_D, bool) -> unit val riscv_f64roundToInt : (bits_rm, bits_D, bool) -> (bits_fflags, bits_D) function riscv_f64roundToInt (rm, v, exact) = { extern_f64roundToInt(rm, v, exact); diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index 2cd5df2be..f8ec00ac8 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -165,11 +165,11 @@ function check_CSR(csr : csreg, p : Privilege, isWrite : bool) -> bool = * where cancellation can be performed. */ -val speculate_conditional = monadic {ocaml: "Platform.speculate_conditional", interpreter: "excl_res", c: "speculate_conditional", lem: "speculate_conditional_success"} : unit -> bool +val speculate_conditional = impure {ocaml: "Platform.speculate_conditional", interpreter: "excl_res", c: "speculate_conditional", lem: "speculate_conditional_success"} : unit -> bool -val load_reservation = {ocaml: "Platform.load_reservation", interpreter: "Platform.load_reservation", c: "load_reservation", lem: "load_reservation"} : xlenbits -> unit -val match_reservation = {ocaml: "Platform.match_reservation", interpreter: "Platform.match_reservation", lem: "match_reservation", c: "match_reservation"} : xlenbits -> bool -val cancel_reservation = {ocaml: "Platform.cancel_reservation", interpreter: "Platform.cancel_reservation", c: "cancel_reservation", lem: "cancel_reservation"} : unit -> unit +val load_reservation = impure {ocaml: "Platform.load_reservation", interpreter: "Platform.load_reservation", c: "load_reservation", lem: "load_reservation"} : xlenbits -> unit +val match_reservation = pure {ocaml: "Platform.match_reservation", interpreter: "Platform.match_reservation", lem: "match_reservation", c: "match_reservation"} : xlenbits -> bool +val cancel_reservation = impure {ocaml: "Platform.cancel_reservation", interpreter: "Platform.cancel_reservation", c: "cancel_reservation", lem: "cancel_reservation"} : unit -> unit /* Exception delegation: given an exception and the privilege at which * it occured, returns the privilege at which it should be handled. diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 6d1afd0ee..295a4da19 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -79,39 +79,39 @@ bitfield Misa : xlenbits = { register misa : Misa /* whether misa is R/W */ -val sys_enable_writable_misa = {c: "sys_enable_writable_misa", ocaml: "Platform.enable_writable_misa", _: "sys_enable_writable_misa"} : unit -> bool +val sys_enable_writable_misa = pure {c: "sys_enable_writable_misa", ocaml: "Platform.enable_writable_misa", _: "sys_enable_writable_misa"} : unit -> bool /* whether misa.c was enabled at boot */ -val sys_enable_rvc = {c: "sys_enable_rvc", ocaml: "Platform.enable_rvc", _: "sys_enable_rvc"} : unit -> bool +val sys_enable_rvc = pure {c: "sys_enable_rvc", ocaml: "Platform.enable_rvc", _: "sys_enable_rvc"} : unit -> bool /* whether misa.{f,d} were enabled at boot */ -val sys_enable_fdext = {c: "sys_enable_fdext", ocaml: "Platform.enable_fdext", _: "sys_enable_fdext"} : unit -> bool +val sys_enable_fdext = pure {c: "sys_enable_fdext", ocaml: "Platform.enable_fdext", _: "sys_enable_fdext"} : unit -> bool /* whether Svinval was enabled at boot */ -val sys_enable_svinval = {c: "sys_enable_svinval", ocaml: "Platform.enable_svinval", _: "sys_enable_svinval"} : unit -> bool +val sys_enable_svinval = pure {c: "sys_enable_svinval", ocaml: "Platform.enable_svinval", _: "sys_enable_svinval"} : unit -> bool /* whether Zcb was enabled at boot */ -val sys_enable_zcb = {c: "sys_enable_zcb", ocaml: "Platform.enable_zcb", _: "sys_enable_zcb"} : unit -> bool +val sys_enable_zcb = pure {c: "sys_enable_zcb", ocaml: "Platform.enable_zcb", _: "sys_enable_zcb"} : unit -> bool /* whether zfinx was enabled at boot */ -val sys_enable_zfinx = {c: "sys_enable_zfinx", ocaml: "Platform.enable_zfinx", _: "sys_enable_zfinx"} : unit -> bool +val sys_enable_zfinx = pure {c: "sys_enable_zfinx", ocaml: "Platform.enable_zfinx", _: "sys_enable_zfinx"} : unit -> bool /* whether the N extension was enabled at boot */ -val sys_enable_next = {c: "sys_enable_next", ocaml: "Platform.enable_next", _: "sys_enable_next"} : unit -> bool +val sys_enable_next = pure {c: "sys_enable_next", ocaml: "Platform.enable_next", _: "sys_enable_next"} : unit -> bool /* Whether FIOM bit of menvcfg/senvcfg is enabled. It must be enabled if supervisor mode is implemented and non-bare addressing modes are supported. */ -val sys_enable_writable_fiom = {c: "sys_enable_writable_fiom", ocaml: "Platform.enable_writable_fiom", _: "sys_enable_writable_fiom"} : unit -> bool +val sys_enable_writable_fiom = pure {c: "sys_enable_writable_fiom", ocaml: "Platform.enable_writable_fiom", _: "sys_enable_writable_fiom"} : unit -> bool /* How many PMP entries are implemented. This must be 0, 16 or 64 (this is checked at runtime). */ -val sys_pmp_count = {c: "sys_pmp_count", ocaml: "Platform.pmp_count", _: "sys_pmp_count"} : unit -> range(0, 64) +val sys_pmp_count = pure {c: "sys_pmp_count", ocaml: "Platform.pmp_count", _: "sys_pmp_count"} : unit -> range(0, 64) /* G parameter that specifies the PMP grain size. The grain size is 2^(G+2), e.g. G=0 -> 4 bytes, G=10 -> 4096 bytes. */ -val sys_pmp_grain = {c: "sys_pmp_grain", ocaml: "Platform.pmp_grain", _: "sys_pmp_grain"} : unit -> range(0, 63) +val sys_pmp_grain = pure {c: "sys_pmp_grain", ocaml: "Platform.pmp_grain", _: "sys_pmp_grain"} : unit -> range(0, 63) /* whether misa.v was enabled at boot */ -val sys_enable_vext = {c: "sys_enable_vext", ocaml: "Platform.enable_vext", _: "sys_enable_vext"} : unit -> bool +val sys_enable_vext = pure {c: "sys_enable_vext", ocaml: "Platform.enable_vext", _: "sys_enable_vext"} : unit -> bool /* whether misa.b was enabled at boot */ -val sys_enable_bext = {c: "sys_enable_bext", ocaml: "Platform.enable_bext", _: "sys_enable_bext"} : unit -> bool +val sys_enable_bext = pure {c: "sys_enable_bext", ocaml: "Platform.enable_bext", _: "sys_enable_bext"} : unit -> bool // CBO extensions. Zicbop cannot be enabled/disabled because it has no effect // at all on this model. -val sys_enable_zicbom = {c: "sys_enable_zicbom", ocaml: "Platform.enable_zicbom", _: "sys_enable_zicbom"} : unit -> bool -val sys_enable_zicboz = {c: "sys_enable_zicboz", ocaml: "Platform.enable_zicboz", _: "sys_enable_zicboz"} : unit -> bool +val sys_enable_zicbom = pure {c: "sys_enable_zicbom", ocaml: "Platform.enable_zicbom", _: "sys_enable_zicbom"} : unit -> bool +val sys_enable_zicboz = pure {c: "sys_enable_zicboz", ocaml: "Platform.enable_zicboz", _: "sys_enable_zicboz"} : unit -> bool /* This function allows an extension to veto a write to Misa if it would violate an alignment restriction on @@ -733,7 +733,7 @@ mapping opst_code : seed_opst <-> bits(2) = { * for this function is unavailable when it's first encountered in * read_seed_csr. Hence it appears here. */ -val get_16_random_bits = { +val get_16_random_bits = impure { ocaml: "Platform.get_16_random_bits", interpreter: "Platform.get_16_random_bits", c: "plat_get_16_random_bits", From ae1e75e82bfd0bdffffc00a3db705053b7860bd5 Mon Sep 17 00:00:00 2001 From: Tim Hutt Date: Mon, 9 Sep 2024 16:03:16 +0100 Subject: [PATCH 2/2] Change prints from impure to pure From the Sail model's perspective the output is not observable so these are pure. Also the pure/impure is used for formal backends which don't actually print anything anyway. --- model/prelude.sail | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/model/prelude.sail b/model/prelude.sail index ea83700b7..4788a60e7 100644 --- a/model/prelude.sail +++ b/model/prelude.sail @@ -56,14 +56,14 @@ overload operator % = {emod_int} overload min = {min_int} overload max = {max_int} -val print_string = impure "print_string" : (string, string) -> unit +val print_string = pure "print_string" : (string, string) -> unit -val print_instr = impure {ocaml: "Platform.print_instr", interpreter: "print_endline", c: "print_instr", lem: "print_dbg", _: "print_endline"} : string -> unit -val print_reg = impure {ocaml: "Platform.print_reg", interpreter: "print_endline", c: "print_reg", lem: "print_dbg", _: "print_endline"} : string -> unit -val print_mem = impure {ocaml: "Platform.print_mem_access", interpreter: "print_endline", c: "print_mem_access", lem: "print_dbg", _: "print_endline"} : string -> unit -val print_platform = impure {ocaml: "Platform.print_platform", interpreter: "print_endline", c: "print_platform", lem: "print_dbg", _: "print_endline"} : string -> unit +val print_instr = pure {ocaml: "Platform.print_instr", interpreter: "print_endline", c: "print_instr", lem: "print_dbg", _: "print_endline"} : string -> unit +val print_reg = pure {ocaml: "Platform.print_reg", interpreter: "print_endline", c: "print_reg", lem: "print_dbg", _: "print_endline"} : string -> unit +val print_mem = pure {ocaml: "Platform.print_mem_access", interpreter: "print_endline", c: "print_mem_access", lem: "print_dbg", _: "print_endline"} : string -> unit +val print_platform = pure {ocaml: "Platform.print_platform", interpreter: "print_endline", c: "print_platform", lem: "print_dbg", _: "print_endline"} : string -> unit -val print_step = impure {ocaml: "Platform.print_step", c: "print_step"} : unit -> unit +val print_step = pure {ocaml: "Platform.print_step", c: "print_step"} : unit -> unit function print_step() = ()