diff options
Diffstat (limited to 'mips/mips_prelude.sail')
| -rw-r--r-- | mips/mips_prelude.sail | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/mips/mips_prelude.sail b/mips/mips_prelude.sail index 9e81a5d0..f9049b5d 100644 --- a/mips/mips_prelude.sail +++ b/mips/mips_prelude.sail @@ -469,11 +469,18 @@ function int_of_AccessLevel level = Kernel => 2 } +/*! +Returns whether the first AccessLevel is sufficient to grant access at the second, required, access level. + */ val grantsAccess : (AccessLevel, AccessLevel) -> bool function grantsAccess (currentLevel, requiredLevel) = int_of_AccessLevel(currentLevel) >= int_of_AccessLevel(requiredLevel) -function getAccessLevel() : unit -> AccessLevel= +/*! +Returns the current effective access level determined by accessing the relevant parts of the MIPS status register. + */ +val getAccessLevel : unit -> AccessLevel effect {rreg} +function getAccessLevel() = if ((CP0Status.EXL()) | (CP0Status.ERL())) then Kernel else match CP0Status.KSU() |