diff options
Diffstat (limited to 'model/prelude_mem.sail')
| -rw-r--r-- | model/prelude_mem.sail | 17 |
1 files changed, 9 insertions, 8 deletions
diff --git a/model/prelude_mem.sail b/model/prelude_mem.sail index b8d47d0..85d141b 100644 --- a/model/prelude_mem.sail +++ b/model/prelude_mem.sail @@ -17,15 +17,16 @@ 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 +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} +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 to consume - * the value along with the metadata to ensure atomicity. + * 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); @@ -36,10 +37,10 @@ val write_ram_ea : forall 'n, 0 < 'n <= max_mem_access . (write_kind, xlenbits, 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, 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) +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 |