Add some tracing to riscv address translation.

2 files changed, 40 insertions, 12 deletions

diff --git a/riscv/riscv_types.sail b/riscv/riscv_types.sail
index e2341a8a..ddce0615 100644
--- a/riscv/riscv_types.sail
+++ b/riscv/riscv_types.sail
@@ -309,7 +309,7 @@ function exceptionType_to_bits(e) =
 val cast exceptionType_to_str : ExceptionType -> string
 function exceptionType_to_str(e) =
   match (e) {
-    E_Fetch_Addr_Align => "fisaligned-fetch",
+    E_Fetch_Addr_Align => "misaligned-fetch",
     E_Fetch_Access_Fault => "fetch-access-fault",
     E_Illegal_Instr => "illegal-instruction",
     E_Breakpoint => "breakpoint",
diff --git a/riscv/riscv_vmem.sail b/riscv/riscv_vmem.sail
index 9d0f42d1..36650705 100644
--- a/riscv/riscv_vmem.sail
+++ b/riscv/riscv_vmem.sail
@@ -61,21 +61,33 @@ enum PTW_Error = {
   PTW_Misaligned,   /* misaligned superpage */
   PTW_PTE_Update    /* PTE update needed but not enabled */
 }
+val cast ptw_error_to_str : PTW_Error -> string
+function ptw_error_to_str(e) =
+  match (e) {
+    PTW_Access        => "mem-access-error",
+    PTW_Invalid_PTE   => "invalid-pte",
+    PTW_No_Permission => "no-permission",
+    PTW_Misaligned    => "misaligned-superpage",
+    PTW_PTE_Update    => "pte-update-needed"
+  }
 
 /* conversion of these translation/PTW failures into architectural exceptions */
-function translationException(a : AccessType, f : PTW_Error) -> ExceptionType =
+function translationException(a : AccessType, f : PTW_Error) -> ExceptionType = {
+  let e : ExceptionType =
   match (a, f) {
-    (Read, PTW_Access)  => E_Load_Access_Fault,
-    (Read, _)           => E_Load_Page_Fault,
-    (Write, PTW_Access) => E_SAMO_Access_Fault,
-    (Write, _)          => E_SAMO_Page_Fault,
-    (Fetch, PTW_Access) => E_Fetch_Access_Fault,
-    (Fetch, _)          => E_Fetch_Page_Fault,
-    /* atomics never raise Load exceptions */
     (ReadWrite, PTW_Access) => E_SAMO_Access_Fault,
-    (ReadWrite, _)          => E_SAMO_Page_Fault
+    (ReadWrite, _)          => E_SAMO_Page_Fault,
+    (Read, PTW_Access)      => E_Load_Access_Fault,
+    (Read, _)               => E_Load_Page_Fault,
+    (Write, PTW_Access)     => E_SAMO_Access_Fault,
+    (Write, _)              => E_SAMO_Page_Fault,
+    (Fetch, PTW_Access)     => E_Fetch_Access_Fault,
+    (Fetch, _)              => E_Fetch_Page_Fault
+  } in {
+    print("translationException(" ^ a ^ ", " ^ f ^ ") -> " ^ e);
+    e
   }
-
+}
 /* address translation: Sv39 */
 
 let SV39_LEVEL_BITS = 9
@@ -133,18 +145,32 @@ function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global) -> PTW_Result
   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)) {
-    MemException(_) => PTW_Failure(PTW_Access),
+    MemException(_) => {
+      print("walk39(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level)
+            ^ " pt_base=" ^ BitStr(ptb)
+            ^ " pt_ofs=" ^ BitStr(pt_ofs)
+            ^ " pte_addr=" ^ BitStr(pte_addr)
+            ^ ": invalid pte address");
+      PTW_Failure(PTW_Access)
+    },
     MemValue(v) => {
       let pte = Mk_SV39_PTE(v);
       let pbits = pte.BITS();
       let pattr = Mk_PTE_Bits(pbits);
       let is_global = global | (pattr.G() == true);
+/*    print("walk39(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level)
+            ^ " pt_base=" ^ BitStr(ptb)
+            ^ " pt_ofs=" ^ BitStr(pt_ofs)
+            ^ " pte_addr=" ^ BitStr(pte_addr)
+            ^ " pte=" ^ BitStr(v)); */
       if isInvalidPTE(pbits) then {
+/*      print("walk39: invalid pte"); */
         PTW_Failure(PTW_Invalid_PTE)
       } else {
         if isPTEPtr(pbits) then {
           if level == 0 then {
             /* last-level PTE contains a pointer instead of a leaf */
+/*          print("walk39: last-level pte contains a ptr"); */
             PTW_Failure(PTW_Invalid_PTE)
           } else {
             /* walk down the pointer to the next level */
@@ -152,6 +178,7 @@ function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global) -> PTW_Result
           }
         } else { /* leaf PTE */
           if ~ (checkPTEPermission(ac, priv, mxr, do_sum, pattr)) then {
+/*          print("walk39: pte permission check failure"); */
             PTW_Failure(PTW_No_Permission)
           } else {
             if level > 0 then { /* superpage */
@@ -159,6 +186,7 @@ function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global) -> PTW_Result
               let mask = shiftl(pte.PPNi() ^ pte.PPNi() ^ EXTZ(0b1), level * SV39_LEVEL_BITS) - 1;
               if (pte.PPNi() & mask) != EXTZ(0b0) then {
                 /* misaligned superpage mapping */
+/*              print("walk39: misaligned superpage mapping"); */
                 PTW_Failure(PTW_Misaligned)
               } else {
                 /* add the appropriate bits of the VPN to the superpage PPN */