refactor memory access to use new sail intrinsics

3 files changed, 49 insertions, 139 deletions

diff --git a/model/prelude.sail b/model/prelude.sail
index 335c20d..806562c 100644
--- a/model/prelude.sail
+++ b/model/prelude.sail
@@ -5,6 +5,8 @@ $include <flow.sail>
 type bits ('n : Int) = vector('n, dec, bit)
 union option ('a : Type) = {None : unit, Some : 'a}
 
+$include <regfp.sail>
+
 val spc : unit <-> string
 val opt_spc : unit <-> string
 val def_spc : unit <-> string
@@ -959,48 +961,9 @@ overload min = {min_nat, min_int}
 
 overload max = {max_nat, max_int}
 
-val __WriteRAM = "write_ram" : forall 'n 'm.
-  (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv}
-
-val __RISCV_write : forall 'n. (bits(64), atom('n), bits(8 * 'n)) -> bool effect {wmv}
-function __RISCV_write (addr, width, data) = {
-  __WriteRAM(64, width, 0x0000_0000_0000_0000, addr, data)
-}
-
 val __TraceMemoryWrite : forall 'n 'm.
   (atom('n), bits('m), bits(8 * 'n)) -> unit
 
-val __ReadRAM = { lem: "MEMr", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
-  (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
-
-val __ReadRAM_acquire = { lem: "MEMr_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
-  (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
-
-val __ReadRAM_strong_acquire = { lem: "MEMr_strong_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
-  (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
-
-val __ReadRAM_reserved = { lem: "MEMr_reserved", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
-  (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
-
-val __ReadRAM_reserved_acquire = { lem: "MEMr_reserved_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
-  (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
-
-val __ReadRAM_reserved_strong_acquire = { lem: "MEMr_reserved_strong_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
-  (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
-
-val __RISCV_read : forall 'n, 'n >= 0. (bits(64), atom('n), bool, bool, bool) -> option(bits(8 * 'n)) effect {rmem}
-function __RISCV_read (addr, width, aq, rl, res) =
-  match (aq, rl, res) {
-    (false, false, false) => Some(__ReadRAM(64, width, 0x0000_0000_0000_0000, addr)),
-    (true,  false, false) => Some(__ReadRAM_acquire(64, width, 0x0000_0000_0000_0000, addr)),
-    (true,  true,  false) => Some(__ReadRAM_strong_acquire(64, width, 0x0000_0000_0000_0000, addr)),
-    (false, false, true)  => Some(__ReadRAM_reserved(64, width, 0x0000_0000_0000_0000, addr)),
-    (true,  false, true)  => Some(__ReadRAM_reserved_acquire(64, width, 0x0000_0000_0000_0000, addr)),
-    (true,  true,  true)  => Some(__ReadRAM_reserved_strong_acquire(64, width, 0x0000_0000_0000_0000, addr)),
-    (false, true,  false) => None(),
-    (false, true,  true)  => None()
-  }
-
 val __TraceMemoryRead : forall 'n 'm. (atom('n), bits('m), bits(8 * 'n)) -> unit
 
 val replicate_bits = "replicate_bits" : forall 'n 'm, 'm >= 0. (bits('n), atom('m)) -> bits('n * 'm)
diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail
index d18f92f..3f8eac8 100644
--- a/model/riscv_insts_base.sail
+++ b/model/riscv_insts_base.sail
@@ -480,15 +480,15 @@ mapping clause encdec = FENCE(pred, succ)
 
 function clause execute (FENCE(pred, succ)) = {
   match (pred, succ) {
-    (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => MEM_fence_rw_rw(),
-    (_ : bits(2) @ 0b10, _ : bits(2) @ 0b11) => MEM_fence_r_rw(),
-    (_ : bits(2) @ 0b10, _ : bits(2) @ 0b10) => MEM_fence_r_r(),
-    (_ : bits(2) @ 0b11, _ : bits(2) @ 0b01) => MEM_fence_rw_w(),
-    (_ : bits(2) @ 0b01, _ : bits(2) @ 0b01) => MEM_fence_w_w(),
-    (_ : bits(2) @ 0b01, _ : bits(2) @ 0b11) => MEM_fence_w_rw(),
-    (_ : bits(2) @ 0b11, _ : bits(2) @ 0b10) => MEM_fence_rw_r(),
-    (_ : bits(2) @ 0b10, _ : bits(2) @ 0b01) => MEM_fence_r_w(),
-    (_ : bits(2) @ 0b01, _ : bits(2) @ 0b10) => MEM_fence_w_r(),
+    (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_rw_rw),
+    (_ : bits(2) @ 0b10, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_r_rw),
+    (_ : bits(2) @ 0b10, _ : bits(2) @ 0b10) => __barrier(Barrier_RISCV_r_r),
+    (_ : bits(2) @ 0b11, _ : bits(2) @ 0b01) => __barrier(Barrier_RISCV_rw_w),
+    (_ : bits(2) @ 0b01, _ : bits(2) @ 0b01) => __barrier(Barrier_RISCV_w_w),
+    (_ : bits(2) @ 0b01, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_w_rw),
+    (_ : bits(2) @ 0b11, _ : bits(2) @ 0b10) => __barrier(Barrier_RISCV_rw_r),
+    (_ : bits(2) @ 0b10, _ : bits(2) @ 0b01) => __barrier(Barrier_RISCV_r_w),
+    (_ : bits(2) @ 0b01, _ : bits(2) @ 0b10) => __barrier(Barrier_RISCV_w_r),
 
     (_ : bits(2) @ 0b00, _ : bits(2) @ 0b00) => (),
 
@@ -533,7 +533,7 @@ mapping clause encdec = FENCE_TSO(pred, succ)
 
 function clause execute (FENCE_TSO(pred, succ)) = {
   match (pred, succ) {
-    (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => MEM_fence_tso(),
+    (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_tso),
     (_ : bits(2) @ 0b00, _ : bits(2) @ 0b00) => (),
 
     _ => { print("FIXME: unsupported fence");
@@ -552,7 +552,7 @@ mapping clause encdec = FENCEI()
   <-> 0b000000000000 @ 0b00000 @ 0b001 @ 0b00000 @ 0b0001111
 
 /* fence.i is a nop for the memory model */
-function clause execute FENCEI() = { /* MEM_fence_i(); */ true }
+function clause execute FENCEI() = { /* __barrier(Barrier_RISCV_i); */ true }
 
 mapping clause assembly = FENCEI() <-> "fence.i"
 
diff --git a/model/riscv_mem.sail b/model/riscv_mem.sail
index 0b3e550..9ffb713 100644
--- a/model/riscv_mem.sail
+++ b/model/riscv_mem.sail
@@ -8,13 +8,24 @@ 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 : ReadType, addr : xlenbits, width : atom('n), aq : bool, rl: bool, res : bool) -> MemoryOpResult(bits(8 * 'n)) =
-  match (t, __RISCV_read(addr, width, aq, rl, res)) {
+function phys_mem_read forall 'n, 'n > 0. (t : ReadType, 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_mem(Read_plain, addr, width)),
+    (true, false, false)  => Some(__read_mem(Read_RISCV_acquire, addr, width)),
+    (true, true, false)   => Some(__read_mem(Read_RISCV_strong_acquire, addr, width)),
+    (false, false, true)  => Some(__read_mem(Read_RISCV_reserved, addr, width)),
+    (true, false, true)   => Some(__read_mem(Read_RISCV_reserved_acquire, addr, width)),
+    (true, true, true)    => Some(__read_mem(Read_RISCV_reserved_strong_acquire, addr, width)),
+    (false, true, false)  => None(), /* should these be instead throwing error_not_implemented as below? */
+    (false, true, true)   => None()
+  }) : option(bits(8 * 'n));
+  match (t, result) {
     (Instruction, None()) => MemException(E_Fetch_Access_Fault),
     (Data, None())        => MemException(E_Load_Access_Fault),
     (_, Some(v))          => { print_mem("mem[" ^ t ^ "," ^ BitStr(addr) ^ "] -> " ^ BitStr(v));
                                MemValue(v) }
   }
+}
 
 function checked_mem_read forall 'n, 'n > 0. (t : ReadType, addr : xlenbits, width : atom('n), aq : bool, rl : bool, res: bool) -> MemoryOpResult(bits(8 * 'n)) =
   /* treat MMIO regions as not executable for now. TODO: this should actually come from PMP/PMA. */
@@ -26,20 +37,6 @@ function checked_mem_read forall 'n, 'n > 0. (t : ReadType, addr : xlenbits, wid
 
 /* Atomic accesses can be done to MMIO regions, e.g. in kernel access to device registers. */
 
-val MEMr                         : forall 'n, 'n > 0. (xlenbits, atom('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, rreg}
-val MEMr_acquire                 : forall 'n, 'n > 0. (xlenbits, atom('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, rreg}
-val MEMr_strong_acquire          : forall 'n, 'n > 0. (xlenbits, atom('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, rreg}
-val MEMr_reserved                : forall 'n, 'n > 0. (xlenbits, atom('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, rreg}
-val MEMr_reserved_acquire        : forall 'n, 'n > 0. (xlenbits, atom('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, rreg}
-val MEMr_reserved_strong_acquire : forall 'n, 'n > 0. (xlenbits, atom('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, rreg}
-
-function MEMr                         (addr, width) = checked_mem_read(Data, addr, width, false, false, false)
-function MEMr_acquire                 (addr, width) = checked_mem_read(Data, addr, width, true, false, false)
-function MEMr_strong_acquire          (addr, width) = checked_mem_read(Data, addr, width, true, true, false)
-function MEMr_reserved                (addr, width) = checked_mem_read(Data, addr, width, false, false, true)
-function MEMr_reserved_acquire        (addr, width) = checked_mem_read(Data, addr, width, true, false, true)
-function MEMr_reserved_strong_acquire (addr, width) = checked_mem_read(Data, addr, width, true, true, true)
-
 $ifdef RVFI_DII
 val rvfi_read : forall 'n, 'n > 0. (xlenbits, atom('n), MemoryOpResult(bits(8 * 'n))) -> unit effect {wreg}
 function rvfi_read (addr, width, result) = {
@@ -70,81 +67,54 @@ function mem_read (addr, width, aq, rl, res) = {
  let result : MemoryOpResult(bits(8 * 'n)) =
   if (aq | res) & (~ (is_aligned_addr(addr, width)))
   then MemException(E_Load_Addr_Align)
-  else match (aq, rl, res) {
-    (false, false, false) => checked_mem_read(Data, addr, width, false, false, false),
-    (true,  false, false) => MEMr_acquire(addr, width),
-    (false, false, true)  => MEMr_reserved(addr, width),
-    (true,  false, true)  => MEMr_reserved_acquire(addr, width),
-    (false, true,  false) => throw(Error_not_implemented("load.rl")),
-    (true,  true,  false) => MEMr_strong_acquire(addr, width),
-    (false, true,  true)  => throw(Error_not_implemented("lr.rl")),
-    (true,  true,  true)  => MEMr_reserved_strong_acquire(addr, width)
-  };
+  else checked_mem_read(Data, addr, width, aq, rl, res);
  rvfi_read(addr, width, result);
  result
 }
 
-val MEMea = {lem: "MEMea", coq: "MEMea", _: "memea"} : forall 'n.
-  (xlenbits, atom('n)) -> unit effect {eamem}
-val MEMea_release = {lem: "MEMea_release", coq: "MEMea_release", _: "memea"} : forall 'n.
-  (xlenbits, atom('n)) -> unit effect {eamem}
-val MEMea_strong_release = {lem: "MEMea_strong_release", coq: "MEMea_strong_release", _: "memea"} : forall 'n.
-  (xlenbits, atom('n)) -> unit effect {eamem}
-val MEMea_conditional = {lem: "MEMea_conditional", coq: "MEMea_conditional", _: "memea"} : forall 'n.
-  (xlenbits, atom('n)) -> unit effect {eamem}
-val MEMea_conditional_release = {lem: "MEMea_conditional_release", coq: "MEMea_conditional_release", _: "memea"} : forall 'n.
-  (xlenbits, atom('n)) -> unit effect {eamem}
-val MEMea_conditional_strong_release = {lem: "MEMea_conditional_strong_release", coq: "MEMea_conditional_strong_release", _: "memea"} : forall 'n.
-  (xlenbits, atom('n)) -> unit effect {eamem}
-
-val mem_write_ea : forall 'n. (xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(unit) effect {eamem, escape}
+val mem_write_ea : forall 'n, 'n > 0. (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)))
   then MemException(E_SAMO_Addr_Align)
   else match (aq, rl, con) {
-    (false, false, false) => MemValue(MEMea(addr, width)),
-    (false, true,  false) => MemValue(MEMea_release(addr, width)),
-    (false, false, true)  => MemValue(MEMea_conditional(addr, width)),
-    (false, true , true)  => MemValue(MEMea_conditional_release(addr, width)),
+    (false, false, false) => MemValue(__write_mem_ea(Write_plain, addr, width)),
+    (false, true,  false) => MemValue(__write_mem_ea(Write_RISCV_release, addr, width)),
+    (false, false, true)  => MemValue(__write_mem_ea(Write_RISCV_conditional, addr, width)),
+    (false, true , true)  => MemValue(__write_mem_ea(Write_RISCV_conditional_release, addr, width)),
     (true,  false, false) => throw(Error_not_implemented("store.aq")),
-    (true,  true,  false) => MemValue(MEMea_strong_release(addr, width)),
+    (true,  true,  false) => MemValue(__write_mem_ea(Write_RISCV_strong_release, addr, width)),
     (true,  false, true)  => throw(Error_not_implemented("sc.aq")),
-    (true,  true , true)  => MemValue(MEMea_conditional_strong_release(addr, width))
+    (true,  true , true)  => MemValue(__write_mem_ea(Write_RISCV_conditional_strong_release, addr, width))
   }
 }
 
 // only used for actual memory regions, to avoid MMIO effects
-function phys_mem_write forall 'n. (addr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> MemoryOpResult(bool) = {
+function phys_mem_write forall 'n, 'n > 0. (addr : xlenbits, width : atom('n), data : bits(8 * 'n), aq : bool, rl : bool, con : bool) -> MemoryOpResult(bool) = {
+  let result = (match (aq, rl, con) {
+    (false, false, false) => MemValue(__write_mem(Write_plain, addr, width, data)),
+    (false, true,  false) => MemValue(__write_mem(Write_RISCV_release, addr, width, data)),
+    (false, false, true)  => MemValue(__write_mem(Write_RISCV_conditional, addr, width, data)),
+    (false, true , true)  => MemValue(__write_mem(Write_RISCV_conditional_release, addr, width, data)),
+    (true,  false, false) => throw(Error_not_implemented("store.aq")),
+    (true,  true,  false) => MemValue(__write_mem(Write_RISCV_strong_release, addr, width, data)),
+    (true,  false, true)  => throw(Error_not_implemented("sc.aq")),
+    (true,  true , true)  => MemValue(__write_mem(Write_RISCV_conditional_strong_release, addr, width, data))
+  }) : MemoryOpResult(bool);
   print_mem("mem[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data));
-  MemValue(__RISCV_write(addr, width, data))
+  result
 }
 
 // dispatches to MMIO regions or physical memory regions depending on physical memory map
-function checked_mem_write forall 'n, 'n > 0. (addr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> MemoryOpResult(bool) =
+function checked_mem_write forall 'n, 'n > 0. (addr : xlenbits, width : atom('n), data: bits(8 * 'n), aq : bool, rl : bool, con : bool) -> MemoryOpResult(bool) =
   if   within_mmio_writable(addr, width)
   then mmio_write(addr, width, data)
   else if within_phys_mem(addr, width)
-  then phys_mem_write(addr, width, data)
+  then phys_mem_write(addr, width, data, aq, rl, con)
   else MemException(E_SAMO_Access_Fault)
 
 /* Atomic accesses can be done to MMIO regions, e.g. in kernel access to device registers. */
 
-val MEMval                            : forall 'n, 'n > 0. (xlenbits, atom('n), bits(8 * 'n)) -> MemoryOpResult(bool) effect {wmv, rreg, wreg}
-val MEMval_release                    : forall 'n, 'n > 0. (xlenbits, atom('n), bits(8 * 'n)) -> MemoryOpResult(bool) effect {wmv, rreg, wreg}
-val MEMval_strong_release             : forall 'n, 'n > 0. (xlenbits, atom('n), bits(8 * 'n)) -> MemoryOpResult(bool) effect {wmv, rreg, wreg}
-val MEMval_conditional                : forall 'n, 'n > 0. (xlenbits, atom('n), bits(8 * 'n)) -> MemoryOpResult(bool) effect {wmv, rreg, wreg}
-val MEMval_conditional_release        : forall 'n, 'n > 0. (xlenbits, atom('n), bits(8 * 'n)) -> MemoryOpResult(bool) effect {wmv, rreg, wreg}
-val MEMval_conditional_strong_release : forall 'n, 'n > 0. (xlenbits, atom('n), bits(8 * 'n)) -> MemoryOpResult(bool) effect {wmv, rreg, wreg}
-
-function MEMval                            (addr, width, data) = checked_mem_write(addr, width, data)
-function MEMval_release                    (addr, width, data) = checked_mem_write(addr, width, data)
-function MEMval_strong_release             (addr, width, data) = checked_mem_write(addr, width, data)
-function MEMval_conditional                (addr, width, data) = checked_mem_write(addr, width, data)
-function MEMval_conditional_release        (addr, width, data) = checked_mem_write(addr, width, data)
-function MEMval_conditional_strong_release (addr, width, data) = checked_mem_write(addr, width, data)
-
-
 $ifdef RVFI_DII
 val rvfi_write : forall 'n, 'n > 0. (xlenbits, atom('n), bits(8 * 'n)) -> unit effect {wreg}
 function rvfi_write (addr, width, value) = {
@@ -166,28 +136,5 @@ function mem_write_value (addr, width, value, aq, rl, con) = {
   rvfi_write(addr, width, value);
   if (rl | con) & (~ (is_aligned_addr(addr, width)))
   then MemException(E_SAMO_Addr_Align)
-  else match (aq, rl, con) {
-    (false, false, false) => checked_mem_write(addr, width, value),
-    (false, true,  false) => MEMval_release(addr, width, value),
-    (false, false, true)  => MEMval_conditional(addr, width, value),
-    (false, true,  true)  => MEMval_conditional_release(addr, width, value),
-    (true,  false, false) => throw(Error_not_implemented("store.aq")),
-    (true,  true,  false) => MEMval_strong_release(addr, width, value),
-    (true,  false, true)  => throw(Error_not_implemented("sc.aq")),
-    (true,  true,  true)  => MEMval_conditional_strong_release(addr, width, value)
-  }
+  else checked_mem_write(addr, width, value, aq, rl, con)
 }
-
-val MEM_fence_rw_rw = {lem: "MEM_fence_rw_rw", coq: "MEM_fence_rw_rw", _: "skip"} : unit -> unit effect {barr}
-val MEM_fence_r_rw  = {lem: "MEM_fence_r_rw", coq: "MEM_fence_r_rw", _: "skip"}  : unit -> unit effect {barr}
-val MEM_fence_r_r   = {lem: "MEM_fence_r_r", coq: "MEM_fence_r_r", _: "skip"}   : unit -> unit effect {barr}
-val MEM_fence_rw_w  = {lem: "MEM_fence_rw_w", coq: "MEM_fence_rw_w", _: "skip"}  : unit -> unit effect {barr}
-val MEM_fence_w_w   = {lem: "MEM_fence_w_w", coq: "MEM_fence_w_w", _: "skip"}   : unit -> unit effect {barr}
-val MEM_fence_w_rw  = {lem: "MEM_fence_w_rw", coq: "MEM_fence_w_rw", _: "skip"}  : unit -> unit effect {barr}
-val MEM_fence_rw_r  = {lem: "MEM_fence_rw_r", coq: "MEM_fence_rw_r", _: "skip"}  : unit -> unit effect {barr}
-val MEM_fence_r_w   = {lem: "MEM_fence_r_w", coq: "MEM_fence_r_w", _: "skip"}   : unit -> unit effect {barr}
-val MEM_fence_w_r   = {lem: "MEM_fence_w_r", coq: "MEM_fence_w_r", _: "skip"}   : unit -> unit effect {barr}
-
-val MEM_fence_tso = {lem: "MEM_fence_tso", coq: "MEM_fence_tso", _: "skip"} : unit -> unit effect {barr}
-
-val MEM_fence_i     = {lem: "MEM_fence_i", coq: "MEM_fence_i", _: "skip"}     : unit -> unit effect {barr}