RISC-V model fixes for RMEM

7 files changed, 37 insertions, 36 deletions

diff --git a/riscv/prelude.sail b/riscv/prelude.sail
index d99581a7..6eeda601 100644
--- a/riscv/prelude.sail
+++ b/riscv/prelude.sail
@@ -355,12 +355,11 @@ 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)) -> unit effect {wmv}
+  (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);
-  true
+  __WriteRAM(64, width, 0x0000_0000_0000_0000, addr, data)
 }
 
 val __TraceMemoryWrite : forall 'n 'm.
diff --git a/riscv/riscv.sail b/riscv/riscv.sail
index 44ba8e0f..27ec8a2f 100644
--- a/riscv/riscv.sail
+++ b/riscv/riscv.sail
@@ -348,14 +348,15 @@ function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) =
           MemException(e) => { handle_mem_exception(addr, e); false },
           MemValue(_) => {
             let rs2_val = X(rs2) in
-            let res : MemoryOpResult(unit) = match width {
+            let res : MemoryOpResult(bool) = match width {
               BYTE   => mem_write_value(addr, 1, rs2_val[7..0],  aq, rl, false),
               HALF   => mem_write_value(addr, 2, rs2_val[15..0], aq, rl, false),
               WORD   => mem_write_value(addr, 4, rs2_val[31..0], aq, rl, false),
               DOUBLE => mem_write_value(addr, 8, rs2_val,        aq, rl, false)
             } in
             match (res) {
-              MemValue(_)     => true,
+              MemValue(true)     => true,
+              MemValue(false)    => internal_error("store got false from mem_write_value"),
               MemException(e) => { handle_mem_exception(addr, e); false }
             }
           }
@@ -630,7 +631,8 @@ union clause ast = FENCEI : unit
 
 mapping clause encdec = FENCEI() <-> 0b000000000000 @ 0b00000 @ 0b001 @ 0b00000 @ 0b0001111
 
-function clause execute FENCEI() = { MEM_fence_i(); true }
+/* fence.i is a nop for the memory model */
+function clause execute FENCEI() = { /* MEM_fence_i(); */ true }
 
 
 mapping clause assembly = FENCEI() <-> "fence.i"
@@ -846,13 +848,14 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
             MemException(e)  => { handle_mem_exception(addr, e); false },
             MemValue(_) => {
               rs2_val = X(rs2);
-              let res : MemoryOpResult(unit) = match width {
+              let res : MemoryOpResult(bool) = match width {
                 WORD   => mem_write_value(addr, 4, rs2_val[31..0], aq, rl, true),
                 DOUBLE => mem_write_value(addr, 8, rs2_val,        aq, rl, true),
                 _      => internal_error("STORECON expected word or double")
               };
               match (res) {
-                MemValue(_)     => { X(rd) = EXTZ(0b0); cancel_reservation(); true },
+                MemValue(true)     => { X(rd) = EXTZ(0b0); cancel_reservation(); true },
+                MemValue(false)    => { X(rd) = EXTZ(0b1); cancel_reservation(); true },
                 MemException(e) => { handle_mem_exception(addr, e); false }
               }
             }
@@ -921,13 +924,14 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
                   AMOMAXU => vector64(max(unsigned(rs2_val), unsigned(loaded)))
                 };
 
-              let wval : MemoryOpResult(unit) = match width {
+              let wval : MemoryOpResult(bool) = match width {
                 WORD   => mem_write_value(addr, 4, result[31..0], aq & rl, rl, true),
                 DOUBLE => mem_write_value(addr, 8, result,        aq & rl, rl, true),
                 _      => internal_error("AMO expected WORD or DOUBLE")
               };
               match (wval) {
-                MemValue(_) => { X(rd) = loaded; true },
+                MemValue(true) => { X(rd) = loaded; true },
+                MemValue(false) => { internal_error("AMO got false from mem_write_value") },
                 MemException(e) => { handle_mem_exception(addr, e); false }
               }
             }
diff --git a/riscv/riscv_analysis.sail b/riscv/riscv_analysis.sail
index 84934a25..e374933a 100644
--- a/riscv/riscv_analysis.sail
+++ b/riscv/riscv_analysis.sail
@@ -2,7 +2,7 @@ $include <regfp.sail>
 
 /* in reverse order because inc vectors don't seem to work (bug) */
 let GPRstr : vector(32, dec, string) = [ "x31", "x30", "x29", "x28", "x27", "x26", "x25", "x24", "x23", "x22", "x21",
-  "x20", "x19", "x18", "x17", "x16", "x15", "x14", "x13", "x12", "x21",
+  "x20", "x19", "x18", "x17", "x16", "x15", "x14", "x13", "x12", "x11",
   "x10", "x9", "x8", "x7", "x6", "x5", "x4", "x3", "x2", "x1", "x0"
   ]
 
@@ -133,7 +133,7 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst
                };
       },
      FENCEI() => {
-              ik = IK_barrier (Barrier_RISCV_i);
+              ik = IK_simple (); // for RMEM, should morally be Barrier_RISCV_i
      },
      LOADRES(aq, rl, rs1, width, rd) => {
             if (rs1 == 0) then () else iR = RFull(GPRstr[rs1]) :: iR;
diff --git a/riscv/riscv_extras.lem b/riscv/riscv_extras.lem
index 60468a4e..a6fa1298 100644
--- a/riscv/riscv_extras.lem
+++ b/riscv/riscv_extras.lem
@@ -49,10 +49,9 @@ let MEMr_reserved_acquire addrsize size hexRAM addr        = read_mem Read_RISCV
 let MEMr_reserved_strong_acquire addrsize size hexRAM addr = read_mem Read_RISCV_reserved_strong_acquire addr size
 
 val write_ram : forall 'rv 'a 'b 'e. Size 'a, Size 'b =>
-  integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv unit 'e
+  integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e
 let write_ram addrsize size hexRAM address value =
-  write_mem_val value >>= fun _ ->
-  return ()
+  write_mem_val value
 
 val read_ram : forall 'rv 'a 'b 'e. Size 'a, Size 'b =>
   integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e
diff --git a/riscv/riscv_extras_sequential.lem b/riscv/riscv_extras_sequential.lem
index 60468a4e..a6fa1298 100644
--- a/riscv/riscv_extras_sequential.lem
+++ b/riscv/riscv_extras_sequential.lem
@@ -49,10 +49,9 @@ let MEMr_reserved_acquire addrsize size hexRAM addr        = read_mem Read_RISCV
 let MEMr_reserved_strong_acquire addrsize size hexRAM addr = read_mem Read_RISCV_reserved_strong_acquire addr size
 
 val write_ram : forall 'rv 'a 'b 'e. Size 'a, Size 'b =>
-  integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv unit 'e
+  integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e
 let write_ram addrsize size hexRAM address value =
-  write_mem_val value >>= fun _ ->
-  return ()
+  write_mem_val value
 
 val read_ram : forall 'rv 'a 'b 'e. Size 'a, Size 'b =>
   integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e
diff --git a/riscv/riscv_mem.sail b/riscv/riscv_mem.sail
index 2322a0ad..21a40af4 100644
--- a/riscv/riscv_mem.sail
+++ b/riscv/riscv_mem.sail
@@ -85,15 +85,15 @@ function mem_write_ea (addr, width, aq, rl, con) = {
 }
 
 // only used for actual memory regions, to avoid MMIO effects
-function phys_mem_write(addr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> forall 'n. MemoryOpResult(unit) = {
+function phys_mem_write(addr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> forall 'n. MemoryOpResult(bool) = {
   print("mem[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data));
-  if   __RISCV_write(addr, width, data)
-  then MemValue(())
-  else MemException(E_SAMO_Access_Fault)
+//  if   
+  MemValue(__RISCV_write(addr, width, data))
+//  else MemException(E_SAMO_Access_Fault)
 }
 
 // dispatches to MMIO regions or physical memory regions depending on physical memory map
-function checked_mem_write(addr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> forall 'n, 'n > 0. MemoryOpResult(unit) =
+function checked_mem_write(addr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> forall 'n, 'n > 0. MemoryOpResult(bool) =
   if   within_mmio_writable(addr, width)
   then mmio_write(addr, width, data)
   else if within_phys_mem(addr, width)
@@ -102,12 +102,12 @@ function checked_mem_write(addr : xlenbits, width : atom('n), data: bits(8 * 'n)
 
 /* 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(unit) effect {wmv, rreg, wreg}
-val MEMval_release                    : forall 'n, 'n > 0. (xlenbits, atom('n), bits(8 * 'n)) -> MemoryOpResult(unit) effect {wmv, rreg, wreg}
-val MEMval_strong_release             : forall 'n, 'n > 0. (xlenbits, atom('n), bits(8 * 'n)) -> MemoryOpResult(unit) effect {wmv, rreg, wreg}
-val MEMval_conditional                : forall 'n, 'n > 0. (xlenbits, atom('n), bits(8 * 'n)) -> MemoryOpResult(unit) effect {wmv, rreg, wreg}
-val MEMval_conditional_release        : forall 'n, 'n > 0. (xlenbits, atom('n), bits(8 * 'n)) -> MemoryOpResult(unit) effect {wmv, rreg, wreg}
-val MEMval_conditional_strong_release : forall 'n, 'n > 0. (xlenbits, atom('n), bits(8 * 'n)) -> MemoryOpResult(unit) effect {wmv, rreg, wreg}
+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)
@@ -117,7 +117,7 @@ function MEMval_conditional_release        (addr, width, data) = checked_mem_wri
 function MEMval_conditional_strong_release (addr, width, data) = checked_mem_write(addr, width, data)
 
 /* NOTE: The wreg effect is due to MMIO, the rreg is due to checking mtime. */
-val mem_write_value : forall 'n, 'n > 0. (xlenbits, atom('n), bits(8 * 'n), bool, bool, bool) -> MemoryOpResult(unit) effect {wmv, rreg, wreg, escape}
+val mem_write_value : forall 'n, 'n > 0. (xlenbits, atom('n), bits(8 * 'n), bool, bool, bool) -> MemoryOpResult(bool) effect {wmv, rreg, wreg, escape}
 
 function mem_write_value (addr, width, value, aq, rl, con) = {
   if (rl | con) & (~ (is_aligned_addr(addr, width)))
diff --git a/riscv/riscv_platform.sail b/riscv/riscv_platform.sail
index 6b903e70..558ca2db 100644
--- a/riscv/riscv_platform.sail
+++ b/riscv/riscv_platform.sail
@@ -118,19 +118,19 @@ function clint_dispatch() -> unit = {
 }
 
 /* The rreg effect is due to checking mtime. */
-val clint_store: forall 'n, 'n > 0. (xlenbits, int('n), bits(8 * 'n)) -> MemoryOpResult(unit) effect {rreg,wreg}
+val clint_store: forall 'n, 'n > 0. (xlenbits, int('n), bits(8 * 'n)) -> MemoryOpResult(bool) effect {rreg,wreg}
 function clint_store(addr, width, data) = {
   let addr = addr - plat_clint_base ();
   if addr == MSIP_BASE & ('n == 8 | 'n == 4) then {
     print("clint[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data) ^ " (mip.MSI <- " ^ BitStr(data[0]) ^ ")");
     mip->MSI() = data[0] == 0b1;
     clint_dispatch();
-    MemValue(())
+    MemValue(true)
   } else if addr == MTIMECMP_BASE & 'n == 8 then {
     print("clint[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data) ^ " (mtimecmp)");
     mtimecmp = zero_extend(data, 64); /* FIXME: Redundant zero_extend currently required by Lem backend */
     clint_dispatch();
-    MemValue(())
+    MemValue(true)
   } else {
     print("clint[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data) ^ " (<unmapped>)");
     MemException(E_SAMO_Access_Fault)
@@ -177,7 +177,7 @@ function htif_load(addr, width) = {
 }
 
 /* The wreg effect is an artifact of using 'register' to implement device state. */
-val htif_store: forall 'n, 0 < 'n <= 8. (xlenbits, int('n), bits(8 * 'n)) -> MemoryOpResult(unit) effect {wreg}
+val htif_store: forall 'n, 0 < 'n <= 8. (xlenbits, int('n), bits(8 * 'n)) -> MemoryOpResult(bool) effect {wreg}
 function htif_store(addr, width, data) = {
   print("htif[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data));
   /* Store the written value so that we can ack it later. */
@@ -205,7 +205,7 @@ function htif_store(addr, width, data) = {
     },
     d => print("htif-???? cmd: " ^ BitStr(data))
   };
-  MemValue(())
+  MemValue(true)
 }
 
 val htif_tick : unit -> unit effect {rreg, wreg}
@@ -229,7 +229,7 @@ function mmio_read(addr : xlenbits, width : atom('n)) -> forall 'n. MemoryOpResu
   then htif_load(addr, width)
   else MemException(E_Load_Access_Fault)
 
-function mmio_write(addr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> forall 'n, 'n > 0. MemoryOpResult(unit) =
+function mmio_write(addr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> forall 'n, 'n > 0. MemoryOpResult(bool) =
   if   within_clint(addr, width)
   then clint_store(addr, width, data)
   else if within_htif_writable(addr, width) & 'n <= 8