Skip to content

Commit

Permalink
Remove effects
Browse files Browse the repository at this point in the history
Since Sail 0.15 (released Nov 2022), effects have had no effect. They now generate a deprecation warning. This commit removes all the effect annotations from the model, thus fixing the compiler warnings.
  • Loading branch information
Timmmm authored and billmcspadden-riscv committed Sep 12, 2023
1 parent e2e942c commit 4c77f62
Show file tree
Hide file tree
Showing 32 changed files with 189 additions and 189 deletions.
2 changes: 1 addition & 1 deletion model/prelude.sail
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
6 changes: 3 additions & 3 deletions model/prelude_mem.sail
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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)
Expand Down
4 changes: 2 additions & 2 deletions model/prelude_mem_metadata.sail
Original file line number Diff line number Diff line change
Expand Up @@ -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) = ()
6 changes: 3 additions & 3 deletions model/riscv_csr_map.sail
Original file line number Diff line number Diff line change
Expand Up @@ -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
4 changes: 2 additions & 2 deletions model/riscv_decode_ext.sail
Original file line number Diff line number Diff line change
Expand Up @@ -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)
4 changes: 2 additions & 2 deletions model/riscv_ext_regs.sail
Original file line number Diff line number Diff line change
Expand Up @@ -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
}
Expand Down
2 changes: 1 addition & 1 deletion model/riscv_fdext_control.sail
Original file line number Diff line number Diff line change
Expand Up @@ -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()
Expand Down
40 changes: 20 additions & 20 deletions model/riscv_fdext_regs.sail
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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 =
Expand Down Expand Up @@ -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);
Expand Down Expand Up @@ -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()));
Expand All @@ -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());
Expand All @@ -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());
Expand All @@ -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());
Expand All @@ -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());
Expand All @@ -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());
Expand All @@ -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());
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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;
Expand All @@ -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
Expand Down
2 changes: 1 addition & 1 deletion model/riscv_fetch.sail
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
2 changes: 1 addition & 1 deletion model/riscv_insts_aext.sail
Original file line number Diff line number Diff line change
Expand Up @@ -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 },
Expand Down
2 changes: 1 addition & 1 deletion model/riscv_insts_base.sail
Original file line number Diff line number Diff line change
Expand Up @@ -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 },
Expand Down
6 changes: 3 additions & 3 deletions model/riscv_insts_begin.sail
Original file line number Diff line number Diff line change
Expand Up @@ -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

/*
Expand Down
10 changes: 5 additions & 5 deletions model/riscv_insts_fext.sail
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down Expand Up @@ -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 {
Expand All @@ -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 },
Expand Down Expand Up @@ -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 },
Expand Down
Loading

0 comments on commit 4c77f62

Please sign in to comment.