diff options
author | Robert Norton <rmn30@cam.ac.uk> | 2019-07-03 16:43:44 +0100 |
---|---|---|
committer | Robert Norton <rmn30@cam.ac.uk> | 2019-07-03 16:43:44 +0100 |
commit | cc53e6272416ac3ba680849d0b29b0571e2bbcbd (patch) | |
tree | 87ecd2a461d49a81eb38e6db15b4ecd2e6c1573f | |
parent | 39376dd662d67e2fe014a3c1c8d47a6e74615a4b (diff) | |
download | sail-riscv-cc53e6272416ac3ba680849d0b29b0571e2bbcbd.zip sail-riscv-cc53e6272416ac3ba680849d0b29b0571e2bbcbd.tar.gz sail-riscv-cc53e6272416ac3ba680849d0b29b0571e2bbcbd.tar.bz2 |
Add a maximum memory access size to slightly improve C code geneation.
-rw-r--r-- | model/prelude_mem.sail | 15 | ||||
-rw-r--r-- | model/riscv_mem.sail | 24 | ||||
-rw-r--r-- | model/riscv_platform.sail | 16 |
3 files changed, 32 insertions, 23 deletions
diff --git a/model/prelude_mem.sail b/model/prelude_mem.sail index d9c521b..b8d47d0 100644 --- a/model/prelude_mem.sail +++ b/model/prelude_mem.sail @@ -10,7 +10,16 @@ * in prelude_mem_metadata. */ -val write_ram : forall 'n, 'n > 0. (write_kind, xlenbits, atom('n), bits(8 * 'n), mem_meta) -> bool effect {wmv, wmvt} + +/* This is a slightly arbitrary limit on the maximum number of bytes + in a memory access. It helps to generate slightly better C code + because it means width argument can be fast native integer. It + would be even better if it could be <= 8 bytes so that data can + also be a 64-bit int but CHERI needs 128-bit accesses for + capabilities and SIMD / vector instructions will also need more. */ + type max_mem_access : Int = 16 + +val write_ram : forall 'n, 0 < 'n <= max_mem_access . (write_kind, xlenbits, atom('n), bits(8 * 'n), mem_meta) -> bool effect {wmv, wmvt} 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; @@ -23,12 +32,12 @@ function write_ram(wk, addr, width, data, meta) = { ret } -val write_ram_ea : forall 'n, 'n > 0 . (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 effect {eamem} function write_ram_ea(wk, addr, width) = __write_mem_ea(wk, sizeof(xlen), addr, width) /* FIXME: Make this also return the metadata, which will also require external API changes. */ -val read_ram : forall 'n, 'n > 0. (read_kind, xlenbits, atom('n)) -> bits(8 * 'n) effect {rmem} +val read_ram : forall 'n, 0 < 'n <= max_mem_access . (read_kind, xlenbits, atom('n)) -> bits(8 * 'n) effect {rmem} function read_ram(rk, addr, width) = __read_mem(rk, sizeof(xlen), addr, width) diff --git a/model/riscv_mem.sail b/model/riscv_mem.sail index 364c4d6..9f417c0 100644 --- a/model/riscv_mem.sail +++ b/model/riscv_mem.sail @@ -20,7 +20,7 @@ function is_aligned_addr forall 'n. (addr : xlenbits, width : atom('n)) -> bool unsigned(addr) % width == 0 // only used for actual memory regions, to avoid MMIO effects -function phys_mem_read forall 'n, 'n > 0. (t : AccessType, addr : xlenbits, width : atom('n), aq : bool, rl: bool, res : bool) -> MemoryOpResult(bits(8 * 'n)) = { +function phys_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType, addr : xlenbits, width : atom('n), aq : bool, rl: bool, res : bool) -> MemoryOpResult(bits(8 * 'n)) = { let result = (match (aq, rl, res) { (false, false, false) => Some(read_ram(Read_plain, addr, width)), (true, false, false) => Some(read_ram(Read_RISCV_acquire, addr, width)), @@ -42,7 +42,7 @@ function phys_mem_read forall 'n, 'n > 0. (t : AccessType, addr : xlenbits, widt } /* dispatches to MMIO regions or physical memory regions depending on physical memory map */ -function checked_mem_read forall 'n, 'n > 0. (t : AccessType, addr : xlenbits, width : atom('n), aq : bool, rl : bool, res: bool) -> MemoryOpResult(bits(8 * 'n)) = +function checked_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType, addr : xlenbits, width : atom('n), aq : bool, rl : bool, res: bool) -> MemoryOpResult(bits(8 * 'n)) = if within_mmio_readable(addr, width) then mmio_read(addr, width) else if within_phys_mem(addr, width) @@ -50,7 +50,7 @@ function checked_mem_read forall 'n, 'n > 0. (t : AccessType, addr : xlenbits, w else MemException(E_Load_Access_Fault) /* PMP checks if enabled */ -function pmp_mem_read forall 'n, 'n > 0. (t : AccessType, addr : xlenbits, width : atom('n), aq : bool, rl : bool, res: bool) -> MemoryOpResult(bits(8 * 'n)) = +function pmp_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType, addr : xlenbits, width : atom('n), aq : bool, rl : bool, res: bool) -> MemoryOpResult(bits(8 * 'n)) = if (~ (plat_enable_pmp ())) then checked_mem_read(t, addr, width, aq, rl, res) else { @@ -81,9 +81,9 @@ $endif /* NOTE: The rreg effect is due to MMIO. */ $ifdef RVFI_DII -val mem_read : forall 'n, 'n > 0. (AccessType, xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) effect {wreg, rmem, rreg, escape} +val mem_read : forall 'n, 0 < 'n <= max_mem_access . (AccessType, xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) effect {wreg, rmem, rreg, escape} $else -val mem_read : forall 'n, 'n > 0. (AccessType, xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, rreg, escape} +val mem_read : forall 'n, 0 < 'n <= max_mem_access . (AccessType, xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, rreg, escape} $endif function mem_read (typ, addr, width, aq, rl, res) = { @@ -99,7 +99,7 @@ function mem_read (typ, addr, width, aq, rl, res) = { result } -val mem_write_ea : forall 'n, 'n > 0. (xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(unit) effect {eamem, escape} +val mem_write_ea : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(unit) effect {eamem, escape} function mem_write_ea (addr, width, aq, rl, con) = { if (rl | con) & (~ (is_aligned_addr(addr, width))) @@ -117,7 +117,7 @@ function mem_write_ea (addr, width, aq, rl, con) = { } $ifdef RVFI_DII -val rvfi_write : forall 'n, 'n > 0. (xlenbits, atom('n), bits(8 * 'n)) -> unit effect {wreg} +val rvfi_write : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bits(8 * 'n)) -> unit effect {wreg} function rvfi_write (addr, width, value) = { rvfi_exec->rvfi_mem_addr() = EXTZ(addr); if width <= 8 then { @@ -131,7 +131,7 @@ function rvfi_write (addr, width, value) = () $endif // only used for actual memory regions, to avoid MMIO effects -function phys_mem_write forall 'n, 'n > 0. (wk : write_kind, addr : 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, addr : xlenbits, width : atom('n), data : bits(8 * 'n), meta : mem_meta) -> MemoryOpResult(bool) = { rvfi_write(addr, width, data); let result = MemValue(write_ram(wk, addr, width, data, meta)); if get_config_print_mem() @@ -140,7 +140,7 @@ function phys_mem_write forall 'n, 'n > 0. (wk : write_kind, addr : xlenbits, wi } /* dispatches to MMIO regions or physical memory regions depending on physical memory map */ -function checked_mem_write forall 'n, 'n > 0. (wk : write_kind, addr : 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, addr : xlenbits, width : atom('n), data: bits(8 * 'n), meta: mem_meta) -> MemoryOpResult(bool) = if within_mmio_writable(addr, width) then mmio_write(addr, width, data) else if within_phys_mem(addr, width) @@ -148,7 +148,7 @@ function checked_mem_write forall 'n, 'n > 0. (wk : write_kind, addr : xlenbits, else MemException(E_SAMO_Access_Fault) /* PMP checks if enabled */ -function pmp_mem_write forall 'n, 'n > 0. (wk: write_kind, addr : xlenbits, width : atom('n), data: bits(8 * 'n), meta: mem_meta) -> MemoryOpResult(bool) = +function pmp_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk: write_kind, addr : xlenbits, width : atom('n), data: bits(8 * 'n), meta: mem_meta) -> MemoryOpResult(bool) = if (~ (plat_enable_pmp ())) then checked_mem_write(wk, addr, width, data, meta) else match pmpCheck(addr, width, Write, effectivePrivilege(mstatus, cur_privilege)) { @@ -163,7 +163,7 @@ function pmp_mem_write forall 'n, 'n > 0. (wk: write_kind, addr : xlenbits, widt * data. * NOTE: The wreg effect is due to MMIO, the rreg is due to checking mtime. */ -val mem_write_value_meta : forall 'n, 'n > 0. (xlenbits, atom('n), bits(8 * 'n), mem_meta, bool, bool, bool) -> MemoryOpResult(bool) effect {wmv, wmvt, rreg, wreg, escape} +val mem_write_value_meta : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bits(8 * 'n), mem_meta, bool, bool, bool) -> MemoryOpResult(bool) effect {wmv, wmvt, rreg, wreg, escape} function mem_write_value_meta (addr, width, value, meta, aq, rl, con) = { rvfi_write(addr, width, value); if (rl | con) & (~ (is_aligned_addr(addr, width))) @@ -182,6 +182,6 @@ function mem_write_value_meta (addr, width, value, meta, aq, rl, con) = { } /* Memory write with a default metadata value. */ -val mem_write_value : forall 'n, 'n > 0. (xlenbits, atom('n), bits(8 * 'n), bool, bool, bool) -> MemoryOpResult(bool) effect {wmv, wmvt, rreg, wreg, escape} +val mem_write_value : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bits(8 * 'n), bool, bool, bool) -> MemoryOpResult(bool) effect {wmv, wmvt, rreg, wreg, escape} function mem_write_value (addr, width, value, aq, rl, con) = mem_write_value_meta(addr, width, value, default_meta, aq, rl, con) diff --git a/model/riscv_platform.sail b/model/riscv_platform.sail index 477731e..dd8b5bc 100644 --- a/model/riscv_platform.sail +++ b/model/riscv_platform.sail @@ -69,7 +69,7 @@ function phys_mem_segments() = /* Physical memory map predicates */ -function within_phys_mem forall 'n. (addr : xlenbits, width : atom('n)) -> bool = { +function within_phys_mem forall 'n, 'n <= max_mem_access. (addr : xlenbits, width : atom('n)) -> bool = { /* To avoid overflow issues when physical memory extends to the end * of the addressable range, we need to perform address bound checks * on unsigned unbounded integers. @@ -97,7 +97,7 @@ function within_phys_mem forall 'n. (addr : xlenbits, width : atom('n)) -> bool } } -function within_clint forall 'n. (addr : xlenbits, width : atom('n)) -> bool = { +function within_clint forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : atom('n)) -> bool = { /* To avoid overflow issues when physical memory extends to the end * of the addressable range, we need to perform address bound checks * on unsigned unbounded integers. @@ -109,10 +109,10 @@ function within_clint forall 'n. (addr : xlenbits, width : atom('n)) -> bool = { & (addr_int + sizeof('n)) <= (clint_base_int + clint_size_int) } -function within_htif_writable forall 'n. (addr : xlenbits, width : atom('n)) -> bool = +function within_htif_writable forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : atom('n)) -> bool = plat_htif_tohost() == addr | (plat_htif_tohost() + 4 == addr & width == 4) -function within_htif_readable forall 'n. (addr : xlenbits, width : atom('n)) -> bool = +function within_htif_readable forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : atom('n)) -> bool = plat_htif_tohost() == addr | (plat_htif_tohost() + 4 == addr & width == 4) /* CLINT (Core Local Interruptor), based on Spike. */ @@ -319,20 +319,20 @@ function htif_tick() = { /* Top-level MMIO dispatch */ -function within_mmio_readable forall 'n. (addr : xlenbits, width : atom('n)) -> bool = +function within_mmio_readable forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : atom('n)) -> bool = within_clint(addr, width) | (within_htif_readable(addr, width) & 1 <= 'n) -function within_mmio_writable forall 'n. (addr : xlenbits, width : atom('n)) -> bool = +function within_mmio_writable forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : atom('n)) -> bool = within_clint(addr, width) | (within_htif_writable(addr, width) & 'n <= 8) -function mmio_read forall 'n, 'n > 0. (addr : xlenbits, width : atom('n)) -> MemoryOpResult(bits(8 * 'n)) = +function mmio_read forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : atom('n)) -> MemoryOpResult(bits(8 * 'n)) = if within_clint(addr, width) then clint_load(addr, width) else if within_htif_readable(addr, width) & (1 <= 'n) then htif_load(addr, width) else MemException(E_Load_Access_Fault) -function mmio_write forall 'n, 'n > 0. (addr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> MemoryOpResult(bool) = +function mmio_write forall 'n, 0 <'n <= max_mem_access . (addr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> MemoryOpResult(bool) = if within_clint(addr, width) then clint_store(addr, width, data) else if within_htif_writable(addr, width) & 'n <= 8 |