riscv · billmcspadden-riscv · Sep 12, 2023 · Aug 11, 2023
diff --git a/model/prelude.sail b/model/prelude.sail
@@ -87,7 +87,7 @@ val eq_anything = {ocaml: "(fun (x, y) -> x = y)", interpreter: "eq_anything", l
 
 overload operator == = {eq_string, eq_anything}
 
-val "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg}
+val "reg_deref" : forall ('a : Type). register('a) -> 'a
 /* sneaky deref with no effect necessary for bitfield writes */
 val _reg_deref = "reg_deref" : forall ('a : Type). register('a) -> 'a
 

diff --git a/model/prelude_mem.sail b/model/prelude_mem.sail
@@ -89,7 +89,7 @@
    capabilities and SIMD / vector instructions will also need more. */
 type max_mem_access : Int = 16
 
-val write_ram = {lem: "write_ram", coq: "write_ram"} : forall 'n, 0 < 'n <= max_mem_access . (write_kind, xlenbits, atom('n), bits(8 * 'n), mem_meta) -> bool effect {wmv, wmvt}
+val write_ram = {lem: "write_ram", coq: "write_ram"} : forall 'n, 0 < 'n <= max_mem_access . (write_kind, xlenbits, atom('n), bits(8 * 'n), mem_meta) -> bool
 function write_ram(wk, addr, width, data, meta) = {
   /* Write out metadata only if the value write succeeds.
    * It is assumed for now that this write always succeeds;
@@ -103,11 +103,11 @@ function write_ram(wk, addr, width, data, meta) = {
   ret
 }
 
-val write_ram_ea : forall 'n, 0 < 'n <= max_mem_access . (write_kind, xlenbits, atom('n)) -> unit effect {eamem}
+val write_ram_ea : forall 'n, 0 < 'n <= max_mem_access . (write_kind, xlenbits, atom('n)) -> unit
 function write_ram_ea(wk, addr, width) =
   __write_mem_ea(wk, sizeof(xlen), addr, width)
 
-val read_ram = {lem: "read_ram", coq: "read_ram"} : forall 'n, 0 < 'n <= max_mem_access .  (read_kind, xlenbits, atom('n), bool) -> (bits(8 * 'n), mem_meta) effect {rmem, rmemt}
+val read_ram = {lem: "read_ram", coq: "read_ram"} : forall 'n, 0 < 'n <= max_mem_access .  (read_kind, xlenbits, atom('n), bool) -> (bits(8 * 'n), mem_meta)
 function read_ram(rk, addr, width, read_meta) =
   let meta = if read_meta then __ReadRAM_Meta(addr, width) else default_meta in
   (__read_mem(rk, sizeof(xlen), addr, width), meta)

diff --git a/model/prelude_mem_metadata.sail b/model/prelude_mem_metadata.sail
@@ -76,8 +76,8 @@ type mem_meta = unit
 
 let default_meta : mem_meta = ()
 
-val __WriteRAM_Meta : forall 'n. (xlenbits, atom('n), mem_meta) -> unit effect {wmvt}
+val __WriteRAM_Meta : forall 'n. (xlenbits, atom('n), mem_meta) -> unit
 function __WriteRAM_Meta(addr, width, meta) = ()
 
-val __ReadRAM_Meta  : forall 'n. (xlenbits, atom('n)) -> mem_meta effect {rmem}
+val __ReadRAM_Meta  : forall 'n. (xlenbits, atom('n)) -> mem_meta
 function __ReadRAM_Meta(addr, width) = ()
diff --git a/model/riscv_csr_map.sail b/model/riscv_csr_map.sail
@@ -180,13 +180,13 @@ overload to_str = {csr_name}
 /* returns whether a CSR is defined and accessible at a given address
  * and privilege
  */
-val ext_is_CSR_defined : (csreg, Privilege) -> bool effect {rreg}
+val ext_is_CSR_defined : (csreg, Privilege) -> bool
 scattered function ext_is_CSR_defined
 
 /* returns the value of the CSR if it is defined */
-val ext_read_CSR : csreg -> option(xlenbits) effect {rreg}
+val ext_read_CSR : csreg -> option(xlenbits)
 scattered function ext_read_CSR
 
 /* returns new value (after legalisation) if the CSR is defined */
-val ext_write_CSR : (csreg, xlenbits) -> option(xlenbits) effect {rreg, wreg, escape}
+val ext_write_CSR : (csreg, xlenbits) -> option(xlenbits)
 scattered function ext_write_CSR
diff --git a/model/riscv_decode_ext.sail b/model/riscv_decode_ext.sail
@@ -73,8 +73,8 @@
   hooks, the default implementation of which is provided below.
  */
 
-val ext_decode_compressed : bits(16) -> ast effect {rreg}
+val ext_decode_compressed : bits(16) -> ast
 function ext_decode_compressed(bv) = encdec_compressed(bv)
 
-val ext_decode : bits(32) -> ast effect {rreg}
+val ext_decode : bits(32) -> ast
 function ext_decode(bv) = encdec(bv)
diff --git a/model/riscv_ext_regs.sail b/model/riscv_ext_regs.sail
@@ -72,15 +72,15 @@
  * overridden by extensions.
  */
 
-val ext_init_regs : unit -> unit effect {wreg}
+val ext_init_regs : unit -> unit
 function ext_init_regs () = ()
 
 /*!
 This function is called after above when running rvfi and allows the model
 to be initialised differently (e.g. CHERI cap regs are initialised
 to omnipotent instead of null).
  */
-val ext_rvfi_init : unit -> unit effect {rreg, wreg}
+val ext_rvfi_init : unit -> unit
 function ext_rvfi_init () = {
   x1 = x1 // to avoid hook being optimized out
 }

diff --git a/model/riscv_fdext_control.sail b/model/riscv_fdext_control.sail
@@ -77,7 +77,7 @@
 
 /* **************************************************************** */
 
-/* val clause ext_is_CSR_defined : (csreg, Privilege) -> bool effect {rreg} */
+/* val clause ext_is_CSR_defined : (csreg, Privilege) -> bool */
 
 function clause ext_is_CSR_defined (0x001, _) = haveFExt() | haveZfinx()
 function clause ext_is_CSR_defined (0x002, _) = haveFExt() | haveZfinx()

diff --git a/model/riscv_fdext_regs.sail b/model/riscv_fdext_regs.sail
@@ -106,15 +106,15 @@ function nan_unbox_H   regval =
        then regval [15..0]
        else canonical_NaN_H()
 
-val nan_box_S : bits(32) -> flenbits effect {escape}
+val nan_box_S : bits(32) -> flenbits
 function nan_box_S val_32b = {
   assert(sys_enable_fdext());
   if (sizeof(flen) == 32)
   then val_32b
   else 0x_FFFF_FFFF @ val_32b
 }
 
-val nan_unbox_S : flenbits -> bits(32) effect {escape}
+val nan_unbox_S : flenbits -> bits(32)
 function nan_unbox_S regval = {
   assert(sys_enable_fdext());
   if (sizeof(flen) == 32)
@@ -174,7 +174,7 @@ function dirty_fd_context_if_present() -> unit = {
   if sys_enable_fdext() then dirty_fd_context()
 }
 
-val rF : forall 'n, 0 <= 'n < 32. regno('n) -> flenbits effect {rreg, escape}
+val rF : forall 'n, 0 <= 'n < 32. regno('n) -> flenbits
 function rF r = {
   assert(sys_enable_fdext());
   let v : fregtype =
@@ -216,7 +216,7 @@ function rF r = {
   fregval_from_freg(v)
 }
 
-val wF : forall 'n, 0 <= 'n < 32. (regno('n), flenbits) -> unit effect {wreg, escape}
+val wF : forall 'n, 0 <= 'n < 32. (regno('n), flenbits) -> unit
 function wF (r, in_v) = {
   assert(sys_enable_fdext());
   let v = fregval_into_freg(in_v);
@@ -272,42 +272,42 @@ function wF_bits(i: bits(5), data: flenbits) -> unit = {
 
 overload F = {rF_bits, wF_bits, rF, wF}
 
-val rF_H : bits(5) -> bits(16) effect {escape, rreg}
+val rF_H : bits(5) -> bits(16)
 function rF_H(i) = {
   assert(sizeof(flen) >= 16);
   assert(sys_enable_fdext() & not(sys_enable_zfinx()));
   nan_unbox(F(i))
 }
 
-val wF_H : (bits(5), bits(16)) -> unit effect {escape, wreg}
+val wF_H : (bits(5), bits(16)) -> unit
 function wF_H(i, data) = {
   assert(sizeof(flen) >= 16);
   assert(sys_enable_fdext() & not(sys_enable_zfinx()));
   F(i) = nan_box(data)
 }
 
-val rF_S : bits(5) -> bits(32) effect {escape, rreg}
+val rF_S : bits(5) -> bits(32)
 function rF_S(i) = {
   assert(sizeof(flen) >= 32);
   assert(sys_enable_fdext() & not(sys_enable_zfinx()));
   nan_unbox(F(i))
 }
 
-val wF_S : (bits(5), bits(32)) -> unit effect {escape, wreg}
+val wF_S : (bits(5), bits(32)) -> unit
 function wF_S(i, data) = {
   assert(sizeof(flen) >= 32);
   assert(sys_enable_fdext() & not(sys_enable_zfinx()));
   F(i) = nan_box(data)
 }
 
-val rF_D : bits(5) -> bits(64) effect {escape, rreg}
+val rF_D : bits(5) -> bits(64)
 function rF_D(i) = {
   assert(sizeof(flen) >= 64);
   assert(sys_enable_fdext() & not(sys_enable_zfinx()));
   F(i)
 }
 
-val wF_D : (bits(5), bits(64)) -> unit effect {escape, wreg}
+val wF_D : (bits(5), bits(64)) -> unit
 function wF_D(i, data) = {
   assert(sizeof(flen) >= 64);
   assert(sys_enable_fdext() & not(sys_enable_zfinx()));
@@ -318,7 +318,7 @@ overload F_H = { rF_H, wF_H }
 overload F_S = { rF_S, wF_S }
 overload F_D = { rF_D, wF_D }
 
-val rF_or_X_H : bits(5) -> bits(16) effect {escape, rreg}
+val rF_or_X_H : bits(5) -> bits(16)
 function rF_or_X_H(i) = {
   assert(sizeof(flen) >= 16);
   assert(sys_enable_fdext() != sys_enable_zfinx());
@@ -327,7 +327,7 @@ function rF_or_X_H(i) = {
   else X(i)[15..0]
 }
 
-val rF_or_X_S : bits(5) -> bits(32) effect {escape, rreg}
+val rF_or_X_S : bits(5) -> bits(32)
 function rF_or_X_S(i) = {
   assert(sizeof(flen) >= 32);
   assert(sys_enable_fdext() != sys_enable_zfinx());
@@ -336,7 +336,7 @@ function rF_or_X_S(i) = {
   else X(i)[31..0]
 }
 
-val rF_or_X_D : bits(5) -> bits(64) effect {escape, rreg}
+val rF_or_X_D : bits(5) -> bits(64)
 function rF_or_X_D(i) = {
   assert(sizeof(flen) >= 64);
   assert(sys_enable_fdext() != sys_enable_zfinx());
@@ -350,7 +350,7 @@ function rF_or_X_D(i) = {
   }
 }
 
-val wF_or_X_H : (bits(5), bits(16)) -> unit effect {escape, wreg}
+val wF_or_X_H : (bits(5), bits(16)) -> unit
 function wF_or_X_H(i, data) = {
   assert(sizeof(flen) >= 16);
   assert(sys_enable_fdext() != sys_enable_zfinx());
@@ -359,7 +359,7 @@ function wF_or_X_H(i, data) = {
   else X(i) = sign_extend(data)
 }
 
-val wF_or_X_S : (bits(5), bits(32)) -> unit effect {escape, wreg}
+val wF_or_X_S : (bits(5), bits(32)) -> unit
 function wF_or_X_S(i, data) = {
   assert(sizeof(flen) >= 32);
   assert(sys_enable_fdext() != sys_enable_zfinx());
@@ -368,7 +368,7 @@ function wF_or_X_S(i, data) = {
   else X(i) = sign_extend(data)
 }
 
-val wF_or_X_D : (bits(5), bits(64)) -> unit effect {escape, wreg}
+val wF_or_X_D : (bits(5), bits(64)) -> unit
 function wF_or_X_D(i, data) = {
   assert (sizeof(flen) >= 64);
   assert(sys_enable_fdext() != sys_enable_zfinx());
@@ -474,7 +474,7 @@ mapping freg_or_reg_name = {
   reg if sys_enable_zfinx() <-> reg_name(reg)  if sys_enable_zfinx()
 }
 
-val init_fdext_regs : unit -> unit effect {wreg}
+val init_fdext_regs : unit -> unit
 function init_fdext_regs () = {
   f0  = zero_freg;
   f1  = zero_freg;
@@ -524,7 +524,7 @@ bitfield Fcsr : bits(32) = {
 
 register fcsr : Fcsr
 
-val ext_write_fcsr : (bits(3), bits(5)) -> unit effect {rreg, wreg, escape}
+val ext_write_fcsr : (bits(3), bits(5)) -> unit
 function ext_write_fcsr (frm, fflags) = {
   fcsr->FRM()    = frm;      /* Note: frm can be an illegal value, 101, 110, 111 */
   fcsr->FFLAGS() = fflags;
@@ -533,15 +533,15 @@ function ext_write_fcsr (frm, fflags) = {
 }
 
 /* called for softfloat paths (softfloat flags are consistent) */
-val write_fflags : (bits(5)) -> unit effect {rreg, wreg, escape}
+val write_fflags : (bits(5)) -> unit
 function write_fflags(fflags) = {
   if   fcsr.FFLAGS() != fflags
   then dirty_fd_context_if_present();
   fcsr->FFLAGS() = fflags;
 }
 
 /* called for non-softfloat paths (softfloat flags need updating) */
-val accrue_fflags : (bits(5)) -> unit effect {rreg, wreg, escape}
+val accrue_fflags : (bits(5)) -> unit
 function accrue_fflags(flags) = {
   let f = fcsr.FFLAGS() | flags;
   if  fcsr.FFLAGS() != f

diff --git a/model/riscv_fetch.sail b/model/riscv_fetch.sail
@@ -74,7 +74,7 @@
 
 function isRVC(h : half) -> bool = not(h[1 .. 0] == 0b11)
 
-val fetch : unit -> FetchResult effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg}
+val fetch : unit -> FetchResult
 function fetch() -> FetchResult =
   /* fetch PC check for extensions: extensions return a transformed PC to fetch,
    * but any exceptions use the untransformed PC.

diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail
@@ -115,7 +115,7 @@ mapping clause encdec = LOADRES(aq, rl, rs1, size, rd) if amo_width_valid(size)
  * call to load_reservation in LR and cancel_reservation in SC.
  */
 
-val process_loadres : forall 'n, 0 < 'n <= xlen_bytes. (regidx, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) -> Retired effect {escape, rreg, wreg}
+val process_loadres : forall 'n, 0 < 'n <= xlen_bytes. (regidx, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) -> Retired
 function process_loadres(rd, addr, value, is_unsigned) =
   match extend_value(is_unsigned, value) {
     MemValue(result) => { load_reservation(addr); X(rd) = result; RETIRE_SUCCESS },

diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail
@@ -368,7 +368,7 @@ function extend_value(is_unsigned, value) = match (value) {
   MemException(e) => MemException(e)
 }
 
-val process_load : forall 'n, 0 < 'n <= xlen_bytes. (regidx, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) -> Retired effect {escape, rreg, wreg}
+val process_load : forall 'n, 0 < 'n <= xlen_bytes. (regidx, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) -> Retired
 function process_load(rd, vaddr, value, is_unsigned) =
   match extend_value(is_unsigned, value) {
     MemValue(result) => { X(rd) = result; RETIRE_SUCCESS },

diff --git a/model/riscv_insts_begin.sail b/model/riscv_insts_begin.sail
@@ -76,16 +76,16 @@
 scattered union ast
 
 /* returns whether an instruction was retired, used for computing minstret */
-val execute : ast -> Retired effect {escape, wreg, rreg, wmv, wmvt, eamem, rmem, rmemt, barr, exmem, undef}
+val execute : ast -> Retired
 scattered function execute
 
 val assembly : ast <-> string
 scattered mapping assembly
 
-val encdec : ast <-> bits(32) effect {rreg}
+val encdec : ast <-> bits(32)
 scattered mapping encdec
 
-val encdec_compressed : ast <-> bits(16) effect {rreg}
+val encdec_compressed : ast <-> bits(16)
 scattered mapping encdec_compressed
 
 /*

diff --git a/model/riscv_insts_fext.sail b/model/riscv_insts_fext.sail
@@ -108,7 +108,7 @@ mapping frm_mnemonic : rounding_mode <-> string = {
 val      valid_rounding_mode : bits(3) -> bool
 function valid_rounding_mode rm = (rm != 0b101 & rm != 0b110)
 
-val      select_instr_or_fcsr_rm : rounding_mode -> option(rounding_mode) effect {rreg}
+val      select_instr_or_fcsr_rm : rounding_mode -> option(rounding_mode)
 function select_instr_or_fcsr_rm instr_rm =
   if (instr_rm == RM_DYN)
   then {
@@ -345,7 +345,7 @@ mapping clause encdec = LOAD_FP(imm, rs1, rd, DOUBLE)        if haveDExt()
 /* Execution semantics ================================ */
 
 val process_fload64 : (regidx, xlenbits, MemoryOpResult(bits(64)))
-                      -> Retired effect {escape, rreg, wreg}
+                      -> Retired
 function process_fload64(rd, addr, value) =
   if   sizeof(flen) == 64
   then match value {
@@ -358,15 +358,15 @@ function process_fload64(rd, addr, value) =
   }
 
 val process_fload32 : (regidx, xlenbits, MemoryOpResult(bits(32)))
-                      -> Retired effect {escape, rreg, wreg}
+                      -> Retired
 function process_fload32(rd, addr, value) =
   match value {
     MemValue(result) => { F(rd) = nan_box(result); RETIRE_SUCCESS },
     MemException(e)  => { handle_mem_exception(addr, e); RETIRE_FAIL }
   }
 
 val process_fload16 : (regidx, xlenbits, MemoryOpResult(bits(16)))
-                      -> Retired effect {escape, rreg, wreg}
+                      -> Retired
 function process_fload16(rd, addr, value) =
   match value {
     MemValue(result) => { F(rd) = nan_box(result); RETIRE_SUCCESS },
@@ -430,7 +430,7 @@ mapping clause encdec = STORE_FP(imm7 @ imm5, rs2, rs1, DOUBLE)
 
 /* Execution semantics ================================ */
 
-val process_fstore : (xlenbits, MemoryOpResult(bool)) -> Retired effect {escape, rreg, wreg}
+val process_fstore : (xlenbits, MemoryOpResult(bool)) -> Retired
 function process_fstore(vaddr, value) =
   match value {
     MemValue(true)  => { RETIRE_SUCCESS },