diff options
| -rw-r--r-- | mips/mips_prelude.sail | 30 |
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) = |