diff options
| author | Robert Norton | 2018-05-10 17:38:36 +0100 |
|---|---|---|
| committer | Robert Norton | 2018-05-10 17:38:36 +0100 |
| commit | 938f06bc6c711ef3e777beaace7da8d4aee158b9 (patch) | |
| tree | 2a31af2c7df2e77d22e1529cae4c89668c7fb035 | |
| parent | 839f239f01ce3ecb4fe91a3f542d194591bc1650 (diff) | |
Document the register_inaccessible function.
| -rw-r--r-- | cheri/cheri_prelude_common.sail | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/cheri/cheri_prelude_common.sail b/cheri/cheri_prelude_common.sail index e6273281..47c8759c 100644 --- a/cheri/cheri_prelude_common.sail +++ b/cheri/cheri_prelude_common.sail @@ -261,6 +261,9 @@ function pcc_access_system_regs () = let pcc = capRegToCapStruct(PCC) in (pcc.access_system_regs) +/*! +The following function should be called before reading or writing any capability register to check whether it is one of the protected system capabilities. Although it is usually a general purpose capabilty the invoked data capabiltiy (IDC) is restricted in the branch delay slot of the CCall (selector one) instruction to protect the confidentiality and integrity of the invoked sandbox. + */ val register_inaccessible : regno -> bool effect {rreg} function register_inaccessible(r) = ((r == IDC) & inCCallDelay) | |