Read/write memory values and metadata together atomically

For Lem, bypass the Sail implementation of {read,write}_ram and map to
atomic primitives directly.

We might want to make these functions primitive for other backends as well.

1 files changed, 12 insertions, 0 deletions

diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
index 8162cb8..3db3bbf 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -489,3 +489,15 @@ union MemoryOpResult ('a : Type) = {
   MemValue     : 'a,
   MemException : ExceptionType
 }
+
+val MemoryOpResult_add_meta : forall ('t : Type). (MemoryOpResult('t), mem_meta) -> MemoryOpResult(('t, mem_meta))
+function MemoryOpResult_add_meta(r, m) = match r {
+  MemValue(v)     => MemValue(v, m),
+  MemException(e) => MemException(e)
+}
+
+val MemoryOpResult_drop_meta : forall ('t : Type). MemoryOpResult(('t, mem_meta)) -> MemoryOpResult('t)
+function MemoryOpResult_drop_meta(r) = match r {
+  MemValue(v, m)  => MemValue(v),
+  MemException(e) => MemException(e)
+}