diff options
| author | Robert Norton | 2018-05-09 16:36:54 +0100 |
|---|---|---|
| committer | Robert Norton | 2018-05-09 16:58:19 +0100 |
| commit | cd33f38664c620f1eec5d97bde5b837770e7abbc (patch) | |
| tree | ee69f685f93ef237a59b1587b46c76ced78aa956 /mips/mips_prelude.sail | |
| parent | 680acef72a84b1d3810ffd88c06639bafd1d4b3a (diff) | |
Use latex support for generating cheri documentation and remove sed based hack. Also some minor code cleanups and comments.
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() |