1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
|
/* These functions define the primitives for physical memory access.
* They depend on the XLEN of the architecture.
*
* They also depend on the type of metadata that is read and written
* to physical memory. For models that do not require this metadata,
* a unit type can be used.
*
* The underlying __read_mem and __write_mem functions are from the
* Sail library. The metadata primitives __{Read,Write}RAM_Meta are
* in prelude_mem_metadata.
*/
/* 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 = {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}
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;
* there is currently no return value.
* FIXME: We should convert the external API for all backends
* (not just for Lem) to consume the value along with the
* metadata to ensure atomicity.
*/
let ret : bool = __write_mem(wk, sizeof(xlen), addr, width, data);
if ret then __WriteRAM_Meta(addr, width, meta);
ret
}
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)
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}
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
|
