RISCV load-acquire in Lem (-> rmem)

5 files changed, 68 insertions, 15 deletions

diff --git a/riscv/prelude.sail b/riscv/prelude.sail
index 9ec1d86d..d99581a7 100644
--- a/riscv/prelude.sail
+++ b/riscv/prelude.sail
@@ -366,11 +366,36 @@ function __RISCV_write (addr, width, data) = {
 val __TraceMemoryWrite : forall 'n 'm.
   (atom('n), bits('m), bits(8 * 'n)) -> unit
 
-val __ReadRAM = "read_ram" : forall 'n 'm.
+val __ReadRAM = { lem: "MEMr", _ : "read_ram" } : forall 'n 'm.
   (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
 
-val __RISCV_read : forall 'n. (bits(64), atom('n)) -> option(bits(8 * 'n)) effect {rmem}
-function __RISCV_read (addr, width) = Some(__ReadRAM(64, width, 0x0000_0000_0000_0000, addr))
+val __ReadRAM_acquire = { lem: "MEMr_acquire", _ : "read_ram" } : forall 'n 'm.
+  (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.
+  (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
+
+val __ReadRAM_reserved = { lem: "MEMr_reserved", _ : "read_ram" } : forall 'n 'm.
+  (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.
+  (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.
+  (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
+
+val __RISCV_read : forall 'n. (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
 
diff --git a/riscv/riscv_extras.lem b/riscv/riscv_extras.lem
index 60b635da..60468a4e 100644
--- a/riscv/riscv_extras.lem
+++ b/riscv/riscv_extras.lem
@@ -34,6 +34,20 @@ let MEMea_conditional_release addr size  = write_mem_ea Write_RISCV_conditional_
 let MEMea_conditional_strong_release addr size
                                           = write_mem_ea Write_RISCV_conditional_strong_release addr size
 
+val MEMr                         : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e
+val MEMr_acquire                 : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e
+val MEMr_strong_acquire          : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e
+val MEMr_reserved                : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e
+val MEMr_reserved_acquire        : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e
+val MEMr_reserved_strong_acquire : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e
+
+let MEMr addrsize size hexRAM addr                         = read_mem Read_plain addr size
+let MEMr_acquire addrsize size hexRAM addr                 = read_mem Read_RISCV_acquire addr size
+let MEMr_strong_acquire addrsize size hexRAM addr          = read_mem Read_RISCV_strong_acquire addr size
+let MEMr_reserved addrsize size hexRAM addr                = read_mem Read_RISCV_reserved addr size
+let MEMr_reserved_acquire addrsize size hexRAM addr        = read_mem Read_RISCV_reserved_acquire addr size
+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
 let write_ram addrsize size hexRAM address value =
diff --git a/riscv/riscv_extras_sequential.lem b/riscv/riscv_extras_sequential.lem
index 88ac3e6f..60468a4e 100644
--- a/riscv/riscv_extras_sequential.lem
+++ b/riscv/riscv_extras_sequential.lem
@@ -34,6 +34,20 @@ let MEMea_conditional_release addr size  = write_mem_ea Write_RISCV_conditional_
 let MEMea_conditional_strong_release addr size
                                           = write_mem_ea Write_RISCV_conditional_strong_release addr size
 
+val MEMr                         : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e
+val MEMr_acquire                 : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e
+val MEMr_strong_acquire          : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e
+val MEMr_reserved                : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e
+val MEMr_reserved_acquire        : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e
+val MEMr_reserved_strong_acquire : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e
+
+let MEMr addrsize size hexRAM addr                         = read_mem Read_plain addr size
+let MEMr_acquire addrsize size hexRAM addr                 = read_mem Read_RISCV_acquire addr size
+let MEMr_strong_acquire addrsize size hexRAM addr          = read_mem Read_RISCV_strong_acquire addr size
+let MEMr_reserved addrsize size hexRAM addr                = read_mem Read_RISCV_reserved addr size
+let MEMr_reserved_acquire addrsize size hexRAM addr        = read_mem Read_RISCV_reserved_acquire addr size
+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
 let write_ram addrsize size hexRAM address value =
@@ -106,7 +120,7 @@ val shift_bits_left : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> bitvecto
 let shift_bits_left v m = shiftl v (uint m)
 
 val print_string : string -> string -> unit
-let print_string msg s = print_endline (msg ^ s)
+let print_string msg s = () (* print_endline (msg ^ s) *)
 
 val prerr_string : string -> string -> unit
 let prerr_string msg s = prerr_endline (msg ^ s)
@@ -115,4 +129,4 @@ val prerr_bits : forall 'a. Size 'a => string -> bitvector 'a -> unit
 let prerr_bits msg bs = prerr_endline (msg ^ (show_bitlist (bits_of bs)))
 
 val print_bits : forall 'a. Size 'a => string -> bitvector 'a -> unit
-let print_bits msg bs = print_endline (msg ^ (show_bitlist (bits_of bs)))
+let print_bits msg bs = () (* print_endline (msg ^ (show_bitlist (bits_of bs))) *)
diff --git a/riscv/riscv_mem.sail b/riscv/riscv_mem.sail
index 008c1642..cb60851a 100644
--- a/riscv/riscv_mem.sail
+++ b/riscv/riscv_mem.sail
@@ -4,8 +4,8 @@ function is_aligned_addr (addr : xlenbits, width : atom('n)) -> forall 'n. bool
   unsigned(addr) % width == 0
 
 // only used for actual memory regions, to avoid MMIO effects
-function phys_mem_read(t : ReadType, addr : xlenbits, width : atom('n)) -> forall 'n. MemoryOpResult(bits(8 * 'n)) =
-  match (t, __RISCV_read(addr, width)) {
+function phys_mem_read(t : ReadType, addr : xlenbits, width : atom('n), aq : bool, rl: bool, res : bool) -> forall 'n. MemoryOpResult(bits(8 * 'n)) =
+  match (t, __RISCV_read(addr, width, aq, rl, res)) {
     (Instruction, None()) => MemException(E_Fetch_Access_Fault),
     (Data, None())        => MemException(E_Load_Access_Fault),
     (_, Some(v))          => { print("mem[" ^ t ^ "," ^ BitStr(addr) ^ "] -> " ^ BitStr(v));
@@ -17,7 +17,7 @@ function checked_mem_read(t : ReadType, addr : xlenbits, width : atom('n)) -> fo
   if   t == Data & within_mmio_readable(addr, width)
   then mmio_read(addr, width)
   else if within_phys_mem(addr, width)
-  then phys_mem_read(t, addr, width)
+  then phys_mem_read(t, addr, width, false, false, false)
   else MemException(E_Load_Access_Fault)
 
 /* FIXME: We assume atomic accesses are only done to memory-backed regions.  MMIO is not modeled. */
@@ -29,12 +29,12 @@ val MEMr_reserved                : forall 'n. (xlenbits, atom('n)) -> MemoryOpRe
 val MEMr_reserved_acquire        : forall 'n. (xlenbits, atom('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rmem}
 val MEMr_reserved_strong_acquire : forall 'n. (xlenbits, atom('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rmem}
 
-function MEMr                         (addr, width) = phys_mem_read(Data, addr, width)
-function MEMr_acquire                 (addr, width) = phys_mem_read(Data, addr, width)
-function MEMr_strong_acquire          (addr, width) = phys_mem_read(Data, addr, width)
-function MEMr_reserved                (addr, width) = phys_mem_read(Data, addr, width)
-function MEMr_reserved_acquire        (addr, width) = phys_mem_read(Data, addr, width)
-function MEMr_reserved_strong_acquire (addr, width) = phys_mem_read(Data, addr, width)
+function MEMr                         (addr, width) = phys_mem_read(Data, addr, width, false, false, false)
+function MEMr_acquire                 (addr, width) = phys_mem_read(Data, addr, width, true,  false, false)
+function MEMr_strong_acquire          (addr, width) = phys_mem_read(Data, addr, width, true,  true,  false)
+function MEMr_reserved                (addr, width) = phys_mem_read(Data, addr, width, false, false, true)
+function MEMr_reserved_acquire        (addr, width) = phys_mem_read(Data, addr, width, true,  false, true)
+function MEMr_reserved_strong_acquire (addr, width) = phys_mem_read(Data, addr, width, true,  true,  true)
 
 /* NOTE: The rreg effect is due to MMIO. */
 val mem_read : forall 'n, 'n > 0. (xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, rreg, escape}
diff --git a/riscv/riscv_vmem.sail b/riscv/riscv_vmem.sail
index 36650705..fc9e7eb5 100644
--- a/riscv/riscv_vmem.sail
+++ b/riscv/riscv_vmem.sail
@@ -144,7 +144,7 @@ function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global) -> PTW_Result
                                 PTE39_LOG_SIZE);
   let pte_addr = ptb + pt_ofs;
   /* FIXME: we assume here that walks only access memory-backed addresses. */
-  match (phys_mem_read(Data, EXTZ(pte_addr), 8)) {
+  match (phys_mem_read(Data, EXTZ(pte_addr), 8, false, false, false)) {
     MemException(_) => {
       print("walk39(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level)
             ^ " pt_base=" ^ BitStr(ptb)