This avoids a deprecations warning from Sail

The warning reads:
Explicit effect annotations are deprecated. They are no longer used and can be removed.

Author: marnovandermaas

src/cheri_cap_common.sail

@@ -742,7 +742,7 @@ function incCapAddr(c, delta) =
     (representable, newCap)
 
 
-val capToString : (Capability) -> string effect {escape}
+val capToString : (Capability) -> string
 function capToString (cap) = {
   let len = getCapLength(cap);
   let len_str = BitStr(to_bits(cap_len_width + 3, len));

src/cheri_insts_begin.sail

@@ -64,8 +64,8 @@
  * We add a separate capability-mode encdec clause to handle encodings that overlap
  * with baseline RISC-V encodings.
  */
-val encdec_capmode : ast <-> bits(32) effect {rreg}
+val encdec_capmode : ast <-> bits(32)
 scattered mapping encdec_capmode
 
-val encdec_compressed_capmode : ast <-> bits(16) effect {rreg}
+val encdec_compressed_capmode : ast <-> bits(16)
 scattered mapping encdec_compressed_capmode

src/cheri_mem.sail

@@ -69,7 +69,7 @@
  * are flags controlling relaxed memory ordering and atomic memory access 
  * (not used on single-core MCU).
  */
-val mem_read_cap : (xlenbits, bool, bool, bool) -> MemoryOpResult(Capability) effect {rmem, rmemt, rreg, escape}
+val mem_read_cap : (xlenbits, bool, bool, bool) -> MemoryOpResult(Capability)
 function mem_read_cap (addr, aq, rl, res) = {
   let result : MemoryOpResult((CapBits, bool)) = mem_read_meta(Read(Data), addr, cap_size, aq, rl, res, true);
   match result {
@@ -116,7 +116,7 @@ function mem_read_cap_revoked (addr) = {
  * integrated with the RMEM concurrency tool, but the address annoucement
  * may be ignored in sequential execution.
  */
-val mem_write_ea_cap : (xlenbits, bool, bool, bool) -> MemoryOpResult(unit) effect {eamem}
+val mem_write_ea_cap : (xlenbits, bool, bool, bool) -> MemoryOpResult(unit)
 function mem_write_ea_cap(addr, aq, rl, con) = {
   if   ~(is_aligned_addr(addr, cap_size))
   then MemException(E_SAMO_Addr_Align())
@@ -130,7 +130,7 @@ function mem_write_ea_cap(addr, aq, rl, con) = {
  * in case of exception [e]. [aq], [rl] and [res] are flags controlling relaxed
  * memory ordering and atomic accesses (not used on single-core MCU).
  */
-val mem_write_cap : (xlenbits, Capability, bool, bool, bool) -> MemoryOpResult(bool) effect {wmv, rreg, wreg, escape, wmvt}
+val mem_write_cap : (xlenbits, Capability, bool, bool, bool) -> MemoryOpResult(bool)
 function mem_write_cap (addr, cap, aq, rl, con) = {
   let cap_bits = capToBits(cap);
   /* Assume that conversion to bits and back does not change the capability.

src/cheri_mem_metadata.sail

@@ -74,7 +74,7 @@ function tag_addr_to_addr(tag_addr : tagaddrbits) -> xlenbits = tag_addr @ zeros
 /* FIXME: we should have a maximum cap_size constraint for 'n.
  * This would check that the assumption below of a max span of two regions is valid.
  */
-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, tag) = {
   let tag_addr = addr_to_tag_addr(addr);
   if get_config_print_mem() then
@@ -93,7 +93,7 @@ function __WriteRAM_Meta(addr, width, tag) = {
 }
 
 /* FIXME: we should have a maximum cap_size constraint for 'n. */
-val __ReadRAM_Meta  : forall 'n. (xlenbits, atom('n)) -> mem_meta effect {rmemt}
+val __ReadRAM_Meta  : forall 'n. (xlenbits, atom('n)) -> mem_meta
 function __ReadRAM_Meta(addr, width) = {
   let tag_addr = addr_to_tag_addr(addr);
   let tag = MEMr_tag(zero_extend(tag_addr));

src/cheri_pc_access.sail

@@ -62,20 +62,20 @@
 
 /* accessors for default architectural addresses, for use from within instructions */
 
-val get_arch_pc : unit -> xlenbits effect {rreg}
+val get_arch_pc : unit -> xlenbits
 function get_arch_pc () =
   PC
 
-val get_next_pc : unit -> xlenbits effect {rreg}
+val get_next_pc : unit -> xlenbits
 function get_next_pc() =
   nextPC
 
-val set_next_pc : xlenbits -> unit effect {wreg}
+val set_next_pc : xlenbits -> unit
 function set_next_pc(pc) =
   /* could check for internal errors here on invalid pc */
   nextPC = pc
 
-val tick_pc : unit -> unit effect {rreg, wreg}
+val tick_pc : unit -> unit
 function tick_pc() = {
   PCC = nextPCC;
   PC = nextPC

src/cheri_prelude.sail

@@ -62,10 +62,10 @@
 
 /* CHERI specific helpers */
 
-val MEMr_tag = "read_tag_bool"  : bits(64) -> bool effect { rmemt }
-val MEMw_tag = "write_tag_bool" : (bits(64) , bool) -> unit effect { wmvt }
+val MEMr_tag = "read_tag_bool"  : bits(64) -> bool
+val MEMw_tag = "write_tag_bool" : (bits(64) , bool) -> unit
 
-val MAX : forall 'n, 'n >= 0 . atom('n) -> atom(2 ^ 'n - 1) effect pure
+val MAX : forall 'n, 'n >= 0 . atom('n) -> atom(2 ^ 'n - 1)
 function MAX(n) = pow2(n) - 1
 
 /*!

src/cheri_reg_type.sail

@@ -70,7 +70,7 @@ type regtype = Capability
 let zero_reg : regtype = null_cap
 
 /* register printer */
-val RegStr : Capability -> string effect {escape}
+val RegStr : Capability -> string
 function RegStr(r) = capToString(r)
 
 /* conversions */

src/cheri_regs.sail

@@ -63,7 +63,7 @@
 /* accessors for capability representation */
 
 /* reads a given capability register, or the null capability if the argument is zero. */
-val rC : forall 'n, 0 <= 'n < 32. regno('n) -> regtype effect {rreg, escape}
+val rC : forall 'n, 0 <= 'n < 32. regno('n) -> regtype
 function rC r = {
   match r {
     0  => zero_reg,
@@ -87,7 +87,7 @@ function rC r = {
 }
 
 /* writes a register with a capability value */
-val wC : forall 'n, 0 <= 'n < 32. (regno('n), regtype) -> unit effect {wreg, escape}
+val wC : forall 'n, 0 <= 'n < 32. (regno('n), regtype) -> unit
 function wC (r, v) = {
   /* Encode and decode capability to normalise it prior to writing to register */
   let v = encCapabilityToCapability(v.tag, capToEncCap(v));
@@ -123,7 +123,7 @@ function wC_bits(r: bits(5), v: regtype) -> unit = wC(unsigned(r), v)
 
 overload C = {rC_bits, wC_bits, rC, wC}
 
-val ext_init_regs : unit -> unit effect {wreg}
+val ext_init_regs : unit -> unit
 function ext_init_regs () = {
   PCC = root_cap_exe;
   nextPCC = root_cap_exe;
@@ -163,7 +163,7 @@ function ext_init_regs () = {
  * to be initialised differently. For RVFI we initialise cap regs to default
  * instead of null.
  */
-val ext_rvfi_init : unit -> unit effect {wreg}
+val ext_rvfi_init : unit -> unit
 function ext_rvfi_init () = {
   x1  = root_cap_mem;
   x2  = root_cap_mem;

src/cheri_step_ext.sail

@@ -62,7 +62,7 @@
 
 /* set misa.X to indicate the presence of a non-standard extension. */
 
-val ext_init : unit -> unit effect {wreg}
+val ext_init : unit -> unit
 function ext_init () = {
   misa->X() = 0b1;
   mccsr->d() = 0b1;

src/cheri_sys_exceptions.sail

@@ -101,7 +101,7 @@ function prepare_trap_vector(p : Privilege, c : Mcause) -> xlenbits = {
  * just for reads from (integer) CSRs. EPCC is validated on write
  * so no legalization is required here.
  */
-val get_xret_target : Privilege -> xlenbits effect {escape, rreg}
+val get_xret_target : Privilege -> xlenbits
 function get_xret_target(p) = {
   if p != Machine then internal_error(__FILE__, __LINE__,"unsupported");
   let cap : Capability = MEPCC;
@@ -112,7 +112,7 @@ function get_xret_target(p) = {
  * Setting mepc via CSRW is not supported. MEPCC should be
  * written using CSpecialRW instead.
  */
-val set_xret_target : (Privilege, xlenbits) -> xlenbits effect {escape}
+val set_xret_target : (Privilege, xlenbits) -> xlenbits
 function set_xret_target(p, value) = {
   internal_error(__FILE__, __LINE__,"unsupported");
 }
@@ -121,7 +121,7 @@ function set_xret_target(p, value) = {
  * MEPCC is validated and legalized on write, so this just sets
  * up the new PCC and returns new PC.
  */
-val prepare_xret_target : (Privilege) -> xlenbits effect {rreg, wreg, escape}
+val prepare_xret_target : (Privilege) -> xlenbits
 function prepare_xret_target(p) = {
   if p != Machine then internal_error(__FILE__, __LINE__,"unsupported");
   let epcc : Capability = MEPCC;