Enforce kernel only access to kernel address space. Doesn't really make any difference as without TLB we cannot run any non-kernel mode code anyway.

1 files changed, 24 insertions, 6 deletions

diff --git a/mips/mips_prelude.sail b/mips/mips_prelude.sail
index 5e741104..e27a49d7 100644
--- a/mips/mips_prelude.sail
+++ b/mips/mips_prelude.sail
@@ -193,22 +193,40 @@ function unit SignalExceptionBadAddr((Exception) ex, (bit[64]) badAddr) =
   }
 
 typedef MemAccessType = enumerate {Instruction; LoadData; StoreData}
-typedef AccessLevel   = enumerate {Kernel; Supervisor; User}
+typedef AccessLevel   = enumerate {User; Supervisor; Kernel} 
+
+function AccessLevel getAccessLevel() =
+  if ((CP0Status.EXL) | (CP0Status.ERL)) then
+    Kernel
+  else switch (CP0Status.KSU)
+    {
+      case 0b00 -> Kernel
+      case 0b01 -> Supervisor
+      case 0b10 -> User
+      case _    -> User (* behaviour undefined, assume user *)
+    }
+
+
 function (bit[64]) TLBTranslate ((bit[64]) vAddr, (MemAccessType) accessType) = 
   {
     err := (if (accessType == StoreData) then AdES else AdEL);
-    switch(vAddr[63..62]) {
+    let currentAccessLevel = getAccessLevel() in
+    let (requiredLevel, addr) = switch(vAddr[63..62]) {
       case 0b11 -> switch(vAddr[61..31], vAddr[30..29]) { (* xkseg *)
         case (0b1111111111111111111111111111111, 0b11) -> exit (SignalException(err))  (* kseg3 mapped 32-bit compat TODO *)
         case (0b1111111111111111111111111111111, 0b10) -> exit (SignalException(err))  (* sseg  mapped 32-bit compat TODO *)
-        case (0b1111111111111111111111111111111, 0b01) -> EXTZ(vAddr[28..0])         (* kseg1 unmapped uncached 32-bit compat *)
-        case (0b1111111111111111111111111111111, 0b00) -> EXTZ(vAddr[28..0])         (* kseg0 unmapped cached 32-bit compat *)
+        case (0b1111111111111111111111111111111, 0b01) -> (Kernel, EXTZ(vAddr[28..0])) (* kseg1 unmapped uncached 32-bit compat *)
+        case (0b1111111111111111111111111111111, 0b00) -> (Kernel, EXTZ(vAddr[28..0])) (* kseg0 unmapped cached 32-bit compat *)
         case (_, _) -> exit (SignalException(err))  (* xkseg mapped TODO *)
       }
-      case 0b10 -> EXTZ(vAddr[58..0]) (* xkphys bits 61-59 are cache mode which we ignore *)
+      case 0b10 -> (Kernel, EXTZ(vAddr[58..0])) (* xkphys bits 61-59 are cache mode which we ignore *)
       case 0b01 -> exit (SignalException(err)) (* xsseg - supervisor mapped TODO *)
       case 0b00 -> exit (SignalException(err)) (* xuseg - user mapped TODO *)
-    }
+    } in
+    if (((nat)currentAccessLevel) < ((nat)requiredLevel)) then
+      exit (SignalException(err))
+    else
+      addr
   }
 
 function bit[64] TranslateOrExit((bit[64]) vAddr, (MemAccessType) accessType) =