Interpreter, RISC-V: move memory actions to parts of the interpreter response and refactor RISC-V model accordingly

6 files changed, 108 insertions, 105 deletions

diff --git a/riscv/platform.ml b/riscv/platform.ml
index 092df80f..f5324794 100644
--- a/riscv/platform.ml
+++ b/riscv/platform.ml
@@ -113,6 +113,29 @@ let cancel_reservation () =
   Printf.eprintf "reservation <- none\n";
   reservation := "none"
 
+(* memory *)
+
+let read_mem (rk, addr, len) =
+  Sail_lib.read_ram (List.length addr, len, [], addr)
+
+let last_write_ea = ref (None : (Sail_lib.bit list * Big_int.num) option)
+
+let write_ea (wk, addr, len) =
+  last_write_ea := Some (addr, len)
+
+let write_memv data =
+  match !last_write_ea with
+  | Some (addr, len) ->
+     if Big_int.mul len (Big_int.of_int 8) = Big_int.of_int (List.length data) then
+       Sail_lib.write_ram (List.length addr, len, [], addr, data)
+     else
+       failwith "write_memv with length mismatch to preceding write_ea"
+  | None ->
+     failwith "write_memv without preceding write_ea"
+
+let barrier bk =
+  ()
+
 (* terminal I/O *)
 
 let term_write char_bits =
diff --git a/riscv/riscv.sail b/riscv/riscv.sail
index 2cad614e..1dc9ba8f 100644
--- a/riscv/riscv.sail
+++ b/riscv/riscv.sail
@@ -627,15 +627,15 @@ mapping clause encdec = FENCE(pred, succ) <-> 0b0000 @ pred @ succ @ 0b00000 @ 0
 
 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) => mem_barrier(Barrier_RISCV_rw_rw),
+    (_ : bits(2) @ 0b10, _ : bits(2) @ 0b11) => mem_barrier(Barrier_RISCV_r_rw),
+    (_ : bits(2) @ 0b10, _ : bits(2) @ 0b10) => mem_barrier(Barrier_RISCV_r_r),
+    (_ : bits(2) @ 0b11, _ : bits(2) @ 0b01) => mem_barrier(Barrier_RISCV_rw_w),
+    (_ : bits(2) @ 0b01, _ : bits(2) @ 0b01) => mem_barrier(Barrier_RISCV_w_w),
+    (_ : bits(2) @ 0b01, _ : bits(2) @ 0b11) => mem_barrier(Barrier_RISCV_w_rw),
+    (_ : bits(2) @ 0b11, _ : bits(2) @ 0b10) => mem_barrier(Barrier_RISCV_rw_r),
+    (_ : bits(2) @ 0b10, _ : bits(2) @ 0b01) => mem_barrier(Barrier_RISCV_r_w),
+    (_ : bits(2) @ 0b01, _ : bits(2) @ 0b10) => mem_barrier(Barrier_RISCV_w_r),
 
     (_ : bits(2) @ 0b00, _ : bits(2) @ 0b00) => (),
 
diff --git a/riscv/riscv_mem.sail b/riscv/riscv_mem.sail
index 2bcc9797..39d9713c 100644
--- a/riscv/riscv_mem.sail
+++ b/riscv/riscv_mem.sail
@@ -8,17 +8,28 @@ 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), aq : bool, rl: bool, res : bool) -> forall 'n, 'n >= 0. MemoryOpResult(bits(8 * 'n)) =
-  match (t, __RISCV_read(addr, width, aq, rl, res)) {
+function phys_mem_read(t : ReadType, addr : xlenbits, width : atom('n), aq : bool, rl: bool, res : bool) -> forall 'n, 'n > 0. MemoryOpResult(bits(8 * 'n)) =
+  let result : option(bits(8 * 'n)) = 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(),
+    (false, true,  true)  => None()
+  } in
+  match (t, result) {
     (Instruction, None()) => MemException(E_Fetch_Access_Fault),
     (Data, None())        => MemException(E_Load_Access_Fault),
     (_, Some(v))          => { print("mem[" ^ t ^ "," ^ BitStr(addr) ^ "] -> " ^ BitStr(v));
                                MemValue(v) }
   }
 
-function checked_mem_read(t : ReadType, addr : xlenbits, width : atom('n), aq : bool, rl : bool, res: bool) -> forall 'n, 'n > 0. MemoryOpResult(bits(8 * 'n)) =
+function checked_mem_read(t : ReadType, addr : xlenbits, width : atom('n), aq : bool, rl : bool, res : bool) -> forall 'n, 'n > 0. MemoryOpResult(bits(8 * 'n)) =
   /* treat MMIO regions as not executable for now. TODO: this should actually come from PMP/PMA. */
-  if   t == Data & within_mmio_readable(addr, width)
+  /* TODO: aq/rl/res to MMIO */
+  if   t == Data & within_mmio_readable(addr, width) & aq == false & rl == false & res == false
   then mmio_read(addr, width)
   else if within_phys_mem(addr, width)
   then phys_mem_read(t, addr, width, aq, rl, res)
@@ -26,20 +37,6 @@ function checked_mem_read(t : ReadType, addr : xlenbits, width : atom('n), aq :
 
 /* 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)
-
 /* 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}
 
@@ -47,77 +44,46 @@ function mem_read (addr, width, aq, rl, res) = {
   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)
+    _ => checked_mem_read(Data, addr, width, aq, rl, res)
   }
 }
 
-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) => { __write_ea(Write_plain, addr, width); MemValue(()) },
+    (false, true,  false) => { __write_ea(Write_RISCV_release, addr, width); MemValue(()) },
+    (false, false, true)  => { __write_ea(Write_RISCV_conditional, addr, width); MemValue(()) },
+    (false, true , true)  => { __write_ea(Write_RISCV_conditional_release, addr, width); MemValue(()) },
     (true,  false, false) => throw(Error_not_implemented("store.aq")),
-    (true,  true,  false) => MemValue(MEMea_strong_release(addr, width)),
+    (true,  true,  false) => { __write_ea(Write_RISCV_strong_release, addr, width); MemValue(()) },
     (true,  false, true)  => throw(Error_not_implemented("sc.aq")),
-    (true,  true , true)  => MemValue(MEMea_conditional_strong_release(addr, width))
+    (true,  true , true)  => { __write_ea(Write_RISCV_conditional_strong_release, addr, width); MemValue(()) }
   }
 }
 
 // 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(bool) = {
+function phys_mem_write(addr : xlenbits, width : atom('n), data: bits(8 * 'n), aq : bool, rl : bool, con : bool) -> forall 'n, 'n > 0. MemoryOpResult(bool) = {
   print("mem[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data));
-  MemValue(__RISCV_write(addr, width, data))
+  MemValue(__write_memv(data))
 }
 
 // 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(bool) =
-  if   within_mmio_writable(addr, width)
+function checked_mem_write(addr : xlenbits, width : atom('n), data: bits(8 * 'n), aq : bool, rl : bool, con : bool) -> forall 'n, 'n > 0. MemoryOpResult(bool) =
+  /* TODO: aq/rl/con to MMIO */
+  if   within_mmio_writable(addr, width) & aq == false & rl == false & con == false
   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)
-
 /* 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(bool) effect {wmv, rreg, wreg, escape}
 
@@ -125,24 +91,11 @@ function mem_write_value (addr, width, value, 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) => 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)
+    _ => 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_i     = {lem: "MEM_fence_i", coq: "MEM_fence_i", _: "skip"}     : unit -> unit effect {barr}
+val mem_barrier : barrier_kind -> unit effect {barr}
+function mem_barrier bk = __barrier(bk)
diff --git a/riscv/riscv_step.sail b/riscv/riscv_step.sail
index f9675115..7d883f24 100644
--- a/riscv/riscv_step.sail
+++ b/riscv/riscv_step.sail
@@ -9,7 +9,7 @@ union FetchResult = {
 function isRVC(h : half) -> bool =
  ~ (h[1 .. 0] == 0b11)
 
-val fetch : unit -> FetchResult effect {escape, rmem, rreg, wmv, wreg}
+val fetch : unit -> FetchResult effect {escape, rmem, rreg, eamem, wmv, wreg}
 function fetch() -> FetchResult =
   /* check for legal PC */
   if (PC[0] != 0b0 | (PC[1] != 0b0 & (~ (haveRVC()))))
diff --git a/riscv/riscv_sys.sail b/riscv/riscv_sys.sail
index 59bff606..2669ee3f 100644
--- a/riscv/riscv_sys.sail
+++ b/riscv/riscv_sys.sail
@@ -763,11 +763,29 @@ function check_CSR(csr : csreg, p : Privilege, isWrite : bool) -> bool =
  * where cancellation can be performed.
  */
 
-val load_reservation = {ocaml: "Platform.load_reservation", c: "load_reservation", lem: "load_reservation"} : xlenbits -> unit
+register reservation : option(xlenbits)
 
-val match_reservation = {ocaml: "Platform.match_reservation", lem: "speculate_conditional_success", c: "match_reservation"} : xlenbits -> bool effect {exmem}
+val load_reservation = {ocaml: "Platform.load_reservation", c: "load_reservation", lem: "load_reservation"} : xlenbits -> unit effect {wreg}
+function load_reservation bv = {
+  print("reservation <- " ^ BitStr(bv));
+  reservation = Some(bv)
+}
 
-val cancel_reservation = {ocaml: "Platform.cancel_reservation", c: "cancel_reservation", lem: "cancel_reservation"} : unit -> unit
+val match_reservation = {ocaml: "Platform.match_reservation", lem: "speculate_conditional_success", c: "match_reservation"} : xlenbits -> bool effect {rreg}
+function match_reservation bv = {
+  let current : string = match reservation {
+    Some(r) => BitStr(r),
+    None() => "none"
+  };
+  print("reservation: " ^ current ^ ", key=" ^ BitStr(bv)); 
+  (reservation == Some(bv))
+}
+
+val cancel_reservation = {ocaml: "Platform.cancel_reservation", c: "cancel_reservation", lem: "cancel_reservation"} : unit -> unit effect {wreg}
+function cancel_reservation () = {
+  print("reservation <- none");
+  reservation = None()
+}
 
 /* Exception delegation: given an exception and the privilege at which
  * it occured, returns the privilege at which it should be handled.
diff --git a/riscv/riscv_vmem.sail b/riscv/riscv_vmem.sail
index caafb131..337f576e 100644
--- a/riscv/riscv_vmem.sail
+++ b/riscv/riscv_vmem.sail
@@ -291,7 +291,7 @@ union TR39_Result = {
   TR39_Failure : PTW_Error
 }
 
-val translate39 : (vaddr39, AccessType, Privilege, bool, bool, nat) -> TR39_Result effect {rreg, wreg, wmv, escape, rmem}
+val translate39 : (vaddr39, AccessType, Privilege, bool, bool, nat) -> TR39_Result effect {rreg, wreg, eamem, wmv, escape, rmem}
 function translate39(vAddr, ac, priv, mxr, do_sum, level) = {
   let asid = curAsid64();
   match lookupTLB39(asid, vAddr) {
@@ -313,9 +313,13 @@ function translate39(vAddr, ac, priv, mxr, do_sum, level) = {
               n_ent.pte = update_BITS(ent.pte, pbits.bits());
               writeTLB39(idx, n_ent);
               /* update page table */
-              match checked_mem_write(EXTZ(ent.pteAddr), 8, ent.pte.bits()) {
-                MemValue(_) => (),
-                MemException(e) => internal_error("invalid physical address in TLB")
+              match mem_write_ea(EXTZ(ent.pteAddr), 8, false, false, false) {
+                MemValue(_) =>
+                  match checked_mem_write(EXTZ(ent.pteAddr), 8, ent.pte.bits(), false, false, false) {
+                    MemValue(_) => (),
+                    MemException(e) => internal_error("invalid physical address in TLB")
+                  },
+                _ => internal_error("invalid physical address in TLB")
               };
               TR39_Address(ent.pAddr | EXTZ(vAddr & ent.vAddrMask))
             }
@@ -339,15 +343,20 @@ function translate39(vAddr, ac, priv, mxr, do_sum, level) = {
                 TR39_Failure(PTW_PTE_Update)
               } else {
                 w_pte : SV39_PTE = update_BITS(pte, pbits.bits());
-                match checked_mem_write(EXTZ(pteAddr), 8, w_pte.bits()) {
-                  MemValue(_) => {
-                    addToTLB39(asid, vAddr, pAddr, w_pte, pteAddr, level, global);
-                    TR39_Address(pAddr)
-                  },
-                  MemException(e) => {
-                    /* pte is not in valid memory */
+                match mem_write_ea(EXTZ(pteAddr), 8, false, false, false) {
+                  MemValue(_) =>
+                    match checked_mem_write(EXTZ(pteAddr), 8, w_pte.bits(), false, false, false) {
+                      MemValue(true) => {
+                        addToTLB39(asid, vAddr, pAddr, w_pte, pteAddr, level, global);
+                        TR39_Address(pAddr)
+                      },
+                      _ => {
+                        /* pte is not in valid memory */
+                        TR39_Failure(PTW_Access)
+                      }
+                    },
+                  _ =>
                     TR39_Failure(PTW_Access)
-                  }
                 }
               }
           }
@@ -384,7 +393,7 @@ union TR_Result = {
 
 /* Top-level address translation dispatcher */
 
-val translateAddr : (xlenbits, AccessType, ReadType) -> TR_Result effect {escape, rmem, rreg, wmv, wreg}
+val translateAddr : (xlenbits, AccessType, ReadType) -> TR_Result effect {escape, rmem, rreg, eamem, wmv, wreg}
 function translateAddr(vAddr, ac, rt) = {
   let effPriv : Privilege = match rt {
     Instruction => cur_privilege,