Fix all Sail compilation warnings

Add `pure`/`impure` annotations and remove some duplicate function declarations.
Timmmm · Sep 4, 2024 · 0cab9e6 · 0cab9e6
1 parent a58c58c
commit 0cab9e6
Show file tree

Hide file tree

Showing 5 changed files with 124 additions and 134 deletions.
diff --git 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
@@ -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. */