diff options
Diffstat (limited to 'mips')
| -rw-r--r-- | mips/mips_prelude.sail | 12 | ||||
| -rw-r--r-- | mips/mips_tlb.sail | 10 |
2 files changed, 13 insertions, 9 deletions
diff --git a/mips/mips_prelude.sail b/mips/mips_prelude.sail index 3c3c45f4..9e81a5d0 100644 --- a/mips/mips_prelude.sail +++ b/mips/mips_prelude.sail @@ -461,6 +461,18 @@ function SignalExceptionTLB(ex, badAddr) = { enum MemAccessType = {Instruction, LoadData, StoreData} enum AccessLevel = {User, Supervisor, Kernel} +val int_of_AccessLevel : AccessLevel -> int effect pure +function int_of_AccessLevel level = + match level { + User => 0, + Supervisor => 1, + Kernel => 2 + } + +val grantsAccess : (AccessLevel, AccessLevel) -> bool +function grantsAccess (currentLevel, requiredLevel) = + int_of_AccessLevel(currentLevel) >= int_of_AccessLevel(requiredLevel) + function getAccessLevel() : unit -> AccessLevel= if ((CP0Status.EXL()) | (CP0Status.ERL())) then Kernel diff --git a/mips/mips_tlb.sail b/mips/mips_tlb.sail index 6313c001..a8bb819e 100644 --- a/mips/mips_tlb.sail +++ b/mips/mips_tlb.sail @@ -100,14 +100,6 @@ function TLBTranslate2 (vAddr, accessType) = { } } -val cast_AccessLevel : AccessLevel -> int effect pure -function cast_AccessLevel level = - match level { - User => 0, - Supervisor => 1, - Kernel => 2 - } - /* perform TLB translation. bool is CHERI specific TLB bits noStoreCap/suppressTag */ val TLBTranslateC : (bits(64), MemAccessType) -> (bits(64), bool) effect {escape, rreg, undef, wreg} function TLBTranslateC (vAddr, accessType) = @@ -126,7 +118,7 @@ function TLBTranslateC (vAddr, accessType) = 0b01 => (Supervisor, None() : option(bits(64))), /* xsseg - supervisor mapped */ 0b00 => (User, None() : option(bits(64))) /* xuseg - user mapped */ } in - if (cast_AccessLevel(currentAccessLevel) < cast_AccessLevel(requiredLevel)) then + if not(grantsAccess(currentAccessLevel, requiredLevel)) then SignalExceptionBadAddr(if (accessType == StoreData) then AdES else AdEL, vAddr) else let (pa, c) : (bits(64), bool) = match addr { |