Skip to content

Commit

Permalink
Replace atom with int
Browse files Browse the repository at this point in the history 
This is the newer, less confusing (and documented!) syntax. Fixes #425.
  • Loading branch information
@Timmmm @billmcspadden-riscv
Timmmm authored and billmcspadden-riscv committed Mar 25, 2024
1 parent fd21acc commit df6eac3
Show file tree
Hide file tree
Showing 9 changed files with 53 additions and 53 deletions.
12 changes: 6 additions & 6 deletions model/prelude.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -66,7 +66,7 @@ overload min = {min_int}

overload max = {max_int}

val pow2 = "pow2" : forall 'n. atom('n) -> atom(2 ^ 'n)
val pow2 = "pow2" : forall 'n. int('n) -> int(2 ^ 'n)

val print = "print_endline" : string -> unit
val print_string = "print_string" : (string, string) -> unit
Expand Down Expand Up @@ -112,7 +112,7 @@ function bit_to_bool b = match b {
bitzero => false
}

val to_bits : forall 'l, 'l >= 0.(atom('l), int) -> bits('l)
val to_bits : forall 'l, 'l >= 0.(int('l), int) -> bits('l)
function to_bits (l, n) = get_slice_int(l, n, 0)

infix 4 <_s
Expand Down Expand Up @@ -148,8 +148,8 @@ infix 7 <<
val "shift_bits_right" : forall 'n 'm. (bits('n), bits('m)) -> bits('n)
val "shift_bits_left" : forall 'n 'm. (bits('n), bits('m)) -> bits('n)

val "shiftl" : forall 'm 'n, 'n >= 0. (bits('m), atom('n)) -> bits('m)
val "shiftr" : forall 'm 'n, 'n >= 0. (bits('m), atom('n)) -> bits('m)
val "shiftl" : forall 'm 'n, 'n >= 0. (bits('m), int('n)) -> bits('m)
val "shiftr" : forall 'm 'n, 'n >= 0. (bits('m), int('n)) -> bits('m)

overload operator >> = {shift_bits_right, shiftr}
overload operator << = {shift_bits_left, shiftl}
Expand All @@ -175,11 +175,11 @@ val rotate_bits_left : forall 'n 'm, 'm >= 0. (bits('n), bits('m)) -> bits('n)
function rotate_bits_left (v, n) =
(v << n) | (v >> (to_bits(length(n), length(v)) - n))

val rotater : forall 'm 'n, 'm >= 'n >= 0. (bits('m), atom('n)) -> bits('m)
val rotater : forall 'm 'n, 'm >= 'n >= 0. (bits('m), int('n)) -> bits('m)
function rotater (v, n) =
(v >> n) | (v << (length(v) - n))

val rotatel : forall 'm 'n, 'm >= 'n >= 0. (bits('m), atom('n)) -> bits('m)
val rotatel : forall 'm 'n, 'm >= 'n >= 0. (bits('m), int('n)) -> bits('m)
function rotatel (v, n) =
(v << n) | (v >> (length(v) - n))

Expand Down
10 changes: 5 additions & 5 deletions model/prelude_mem.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,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
val write_ram = {lem: "write_ram", coq: "write_ram"} : forall 'n, 0 < 'n <= max_mem_access . (write_kind, xlenbits, int('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 @@ -41,14 +41,14 @@ 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
val write_ram_ea : forall 'n, 0 < 'n <= max_mem_access . (write_kind, xlenbits, int('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)
val read_ram = {lem: "read_ram", coq: "read_ram"} : forall 'n, 0 < 'n <= max_mem_access . (read_kind, xlenbits, int('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)

val __TraceMemoryWrite : forall 'n 'm. (atom('n), bits('m), bits(8 * 'n)) -> unit
val __TraceMemoryRead : forall 'n 'm. (atom('n), bits('m), bits(8 * 'n)) -> unit
val __TraceMemoryWrite : forall 'n 'm. (int('n), bits('m), bits(8 * 'n)) -> unit
val __TraceMemoryRead : forall 'n 'm. (int('n), bits('m), bits(8 * 'n)) -> unit
4 changes: 2 additions & 2 deletions model/prelude_mem_metadata.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,8 +14,8 @@ type mem_meta = unit

let default_meta : mem_meta = ()

val __WriteRAM_Meta : forall 'n. (xlenbits, atom('n), mem_meta) -> unit
val __WriteRAM_Meta : forall 'n. (xlenbits, int('n), mem_meta) -> unit
function __WriteRAM_Meta(addr, width, meta) = ()

val __ReadRAM_Meta : forall 'n. (xlenbits, atom('n)) -> mem_meta
val __ReadRAM_Meta : forall 'n. (xlenbits, int('n)) -> mem_meta
function __ReadRAM_Meta(addr, width) = ()
4 changes: 2 additions & 2 deletions model/riscv_addr_checks_common.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -40,12 +40,12 @@ union Ext_PhysAddr_Check = {
* return Some(exception) to abort the read or None to allow it to proceed. The
* check is performed after PMP checks and does not apply to MMIO memory.
*/
val ext_check_phys_mem_read : forall 'n, 0 < 'n <= max_mem_access . (AccessType (ext_access_type), xlenbits, atom('n), bool, bool, bool, bool) -> Ext_PhysAddr_Check
val ext_check_phys_mem_read : forall 'n, 0 < 'n <= max_mem_access . (AccessType (ext_access_type), xlenbits, int('n), bool, bool, bool, bool) -> Ext_PhysAddr_Check

/*!
* Validate a write to physical memory.
* THIS(write_kind, paddr, size, data, metadata) should return Some(exception)
* to abort the write or None to allow it to proceed. The check is performed
* after PMP checks and does not apply to MMIO memory.
*/
val ext_check_phys_mem_write : forall 'n, 0 < 'n <= max_mem_access . (write_kind, xlenbits, atom('n), bits(8 * 'n), mem_meta) -> Ext_PhysAddr_Check
val ext_check_phys_mem_write : forall 'n, 0 < 'n <= max_mem_access . (write_kind, xlenbits, int('n), bits(8 * 'n), mem_meta) -> Ext_PhysAddr_Check
48 changes: 24 additions & 24 deletions model/riscv_mem.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -35,7 +35,7 @@
* per the platform memory map.
*/

function is_aligned_addr forall 'n. (addr : xlenbits, width : atom('n)) -> bool =
function is_aligned_addr forall 'n. (addr : xlenbits, width : int('n)) -> bool =
unsigned(addr) % width == 0

function read_kind_of_flags (aq : bool, rl : bool, res : bool) -> option(read_kind) =
Expand All @@ -51,7 +51,7 @@ function read_kind_of_flags (aq : bool, rl : bool, res : bool) -> option(read_ki
}

// only used for actual memory regions, to avoid MMIO effects
function phys_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), paddr : xlenbits, width : atom('n), aq : bool, rl: bool, res : bool, meta : bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) = {
function phys_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), paddr : xlenbits, width : int('n), aq : bool, rl: bool, res : bool, meta : bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) = {
let result = (match read_kind_of_flags(aq, rl, res) {
Some(rk) => Some(read_ram(rk, paddr, width, meta)),
None() => None()
Expand All @@ -67,7 +67,7 @@ function phys_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext
}

/* dispatches to MMIO regions or physical memory regions depending on physical memory map */
function checked_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), paddr : xlenbits, width : atom('n), aq : bool, rl : bool, res: bool, meta : bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) =
function checked_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), paddr : xlenbits, width : int('n), aq : bool, rl : bool, res: bool, meta : bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) =
if within_mmio_readable(paddr, width)
then MemoryOpResult_add_meta(mmio_read(t, paddr, width), default_meta)
else if within_phys_mem(paddr, width)
Expand All @@ -81,7 +81,7 @@ function checked_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(
}

/* PMP checks if enabled */
function pmp_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), p : Privilege, paddr : xlenbits, width : atom('n), aq : bool, rl : bool, res: bool, meta : bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) =
function pmp_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), p : Privilege, paddr : xlenbits, width : int('n), aq : bool, rl : bool, res: bool, meta : bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) =
if sys_pmp_count() == 0
then checked_mem_read(t, paddr, width, aq, rl, res, meta)
else {
Expand All @@ -94,7 +94,7 @@ function pmp_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_
/* Atomic accesses can be done to MMIO regions, e.g. in kernel access to device registers. */

$ifdef RVFI_DII
val rvfi_read : forall 'n, 'n > 0. (xlenbits, atom('n), MemoryOpResult((bits(8 * 'n), mem_meta))) -> unit
val rvfi_read : forall 'n, 'n > 0. (xlenbits, int('n), MemoryOpResult((bits(8 * 'n), mem_meta))) -> unit
function rvfi_read (addr, width, result) = {
rvfi_mem_data[rvfi_mem_addr] = zero_extend(addr);
rvfi_mem_data_present = true;
Expand All @@ -108,21 +108,21 @@ function rvfi_read (addr, width, result) = {
};
}
$else
val rvfi_read : forall 'n, 'n > 0. (xlenbits, atom('n), MemoryOpResult((bits(8 * 'n), mem_meta))) -> unit
val rvfi_read : forall 'n, 'n > 0. (xlenbits, int('n), MemoryOpResult((bits(8 * 'n), mem_meta))) -> unit
function rvfi_read (addr, width, result) = ()
$endif

/* NOTE: The rreg effect is due to MMIO. */
$ifdef RVFI_DII
val mem_read : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n))
val mem_read_priv : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), Privilege, xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n))
val mem_read_meta : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool, bool) -> MemoryOpResult((bits(8 * 'n), mem_meta))
val mem_read_priv_meta : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), Privilege, xlenbits, atom('n), bool, bool, bool, bool) -> MemoryOpResult((bits(8 * 'n), mem_meta))
val mem_read : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, int('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n))
val mem_read_priv : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), Privilege, xlenbits, int('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n))
val mem_read_meta : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, int('n), bool, bool, bool, bool) -> MemoryOpResult((bits(8 * 'n), mem_meta))
val mem_read_priv_meta : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), Privilege, xlenbits, int('n), bool, bool, bool, bool) -> MemoryOpResult((bits(8 * 'n), mem_meta))
$else
val mem_read : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n))
val mem_read_priv : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), Privilege, xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n))
val mem_read_meta : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool, bool) -> MemoryOpResult((bits(8 * 'n), mem_meta))
val mem_read_priv_meta : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), Privilege, xlenbits, atom('n), bool, bool, bool, bool) -> MemoryOpResult((bits(8 * 'n), mem_meta))
val mem_read : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, int('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n))
val mem_read_priv : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), Privilege, xlenbits, int('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n))
val mem_read_meta : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, int('n), bool, bool, bool, bool) -> MemoryOpResult((bits(8 * 'n), mem_meta))
val mem_read_priv_meta : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), Privilege, xlenbits, int('n), bool, bool, bool, bool) -> MemoryOpResult((bits(8 * 'n), mem_meta))
$endif

/* The most generic memory read operation */
Expand Down Expand Up @@ -150,7 +150,7 @@ function mem_read_priv (typ, priv, paddr, width, aq, rl, res) =
function mem_read (typ, paddr, width, aq, rel, res) =
mem_read_priv(typ, effectivePrivilege(typ, mstatus, cur_privilege), paddr, width, aq, rel, res)

val mem_write_ea : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(unit)
val mem_write_ea : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, int('n), bool, bool, bool) -> MemoryOpResult(unit)

function mem_write_ea (addr, width, aq, rl, con) = {
if (rl | con) & not(is_aligned_addr(addr, width))
Expand All @@ -168,7 +168,7 @@ function mem_write_ea (addr, width, aq, rl, con) = {
}

$ifdef RVFI_DII
val rvfi_write : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bits(8 * 'n), mem_meta, MemoryOpResult(bool)) -> unit
val rvfi_write : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, int('n), bits(8 * 'n), mem_meta, MemoryOpResult(bool)) -> unit
function rvfi_write (addr, width, value, meta, result) = {
rvfi_mem_data[rvfi_mem_addr] = zero_extend(addr);
rvfi_mem_data_present = true;
Expand All @@ -185,20 +185,20 @@ function rvfi_write (addr, width, value, meta, result) = {
}
}
$else
val rvfi_write : forall 'n, 'n > 0. (xlenbits, atom('n), bits(8 * 'n), mem_meta, MemoryOpResult(bool)) -> unit
val rvfi_write : forall 'n, 'n > 0. (xlenbits, int('n), bits(8 * 'n), mem_meta, MemoryOpResult(bool)) -> unit
function rvfi_write (addr, width, value, meta, result) = ()
$endif

// only used for actual memory regions, to avoid MMIO effects
function phys_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk : write_kind, paddr : xlenbits, width : atom('n), data : bits(8 * 'n), meta : mem_meta) -> MemoryOpResult(bool) = {
function phys_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk : write_kind, paddr : xlenbits, width : int('n), data : bits(8 * 'n), meta : mem_meta) -> MemoryOpResult(bool) = {
let result = MemValue(write_ram(wk, paddr, width, data, meta));
if get_config_print_mem()
then print_mem("mem[" ^ BitStr(paddr) ^ "] <- " ^ BitStr(data));
result
}

/* dispatches to MMIO regions or physical memory regions depending on physical memory map */
function checked_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk : write_kind, paddr : xlenbits, width : atom('n), data: bits(8 * 'n), meta: mem_meta) -> MemoryOpResult(bool) =
function checked_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk : write_kind, paddr : xlenbits, width : int('n), data: bits(8 * 'n), meta: mem_meta) -> MemoryOpResult(bool) =
if within_mmio_writable(paddr, width)
then mmio_write(paddr, width, data)
else if within_phys_mem(paddr, width)
Expand All @@ -209,7 +209,7 @@ function checked_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk : write_kin
else MemException(E_SAMO_Access_Fault())

/* PMP checks if enabled */
function pmp_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk: write_kind, paddr : xlenbits, width : atom('n), data: bits(8 * 'n), typ: AccessType(ext_access_type), priv: Privilege, meta: mem_meta) -> MemoryOpResult(bool) =
function pmp_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk: write_kind, paddr : xlenbits, width : int('n), data: bits(8 * 'n), typ: AccessType(ext_access_type), priv: Privilege, meta: mem_meta) -> MemoryOpResult(bool) =
if sys_pmp_count() == 0
then checked_mem_write(wk, paddr, width, data, meta)
else {
Expand All @@ -226,7 +226,7 @@ function pmp_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk: write_kind, pa
* data.
* NOTE: The wreg effect is due to MMIO, the rreg is due to checking mtime.
*/
val mem_write_value_priv_meta : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bits(8 * 'n), AccessType(ext_access_type), Privilege, mem_meta, bool, bool, bool) -> MemoryOpResult(bool)
val mem_write_value_priv_meta : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, int('n), bits(8 * 'n), AccessType(ext_access_type), Privilege, mem_meta, bool, bool, bool) -> MemoryOpResult(bool)
function mem_write_value_priv_meta (paddr, width, value, typ, priv, meta, aq, rl, con) = {
if (rl | con) & not(is_aligned_addr(paddr, width))
then MemException(E_SAMO_Addr_Align())
Expand All @@ -249,20 +249,20 @@ function mem_write_value_priv_meta (paddr, width, value, typ, priv, meta, aq, rl
}

/* Memory write with explicit Privilege, implicit AccessType and metadata */
val mem_write_value_priv : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bits(8 * 'n), Privilege, bool, bool, bool) -> MemoryOpResult(bool)
val mem_write_value_priv : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, int('n), bits(8 * 'n), Privilege, bool, bool, bool) -> MemoryOpResult(bool)
function mem_write_value_priv (paddr, width, value, priv, aq, rl, con) =
mem_write_value_priv_meta(paddr, width, value, Write(default_write_acc), priv, default_meta, aq, rl, con)

/* Memory write with explicit metadata and AccessType, implicit and Privilege */
val mem_write_value_meta : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bits(8 * 'n), ext_access_type, mem_meta, bool, bool, bool) -> MemoryOpResult(bool)
val mem_write_value_meta : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, int('n), bits(8 * 'n), ext_access_type, mem_meta, bool, bool, bool) -> MemoryOpResult(bool)
function mem_write_value_meta (paddr, width, value, ext_acc, meta, aq, rl, con) = {
let typ = Write(ext_acc);
let ep = effectivePrivilege(typ, mstatus, cur_privilege);
mem_write_value_priv_meta(paddr, width, value, typ, ep, meta, aq, rl, con)
}

/* Memory write with default AccessType, Privilege, and metadata */
val mem_write_value : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bits(8 * 'n), bool, bool, bool) -> MemoryOpResult(bool)
val mem_write_value : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, int('n), bits(8 * 'n), bool, bool, bool) -> MemoryOpResult(bool)
function mem_write_value (paddr, width, value, aq, rl, con) = {
mem_write_value_meta(paddr, width, value, default_write_acc, default_meta, aq, rl, con)
}
Loading

0 comments on commit df6eac3

Please sign in to comment.