summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--cheri/Makefile2
-rw-r--r--cheri/cheri_insts.sail81
-rw-r--r--cheri/cheri_prelude_common.sail11
-rw-r--r--mips/mips_prelude.sail12
-rw-r--r--mips/mips_tlb.sail10
5 files changed, 106 insertions, 10 deletions
diff --git a/cheri/Makefile b/cheri/Makefile
index 663c8763..fd8a22a9 100644
--- a/cheri/Makefile
+++ b/cheri/Makefile
@@ -107,4 +107,6 @@ extract: cheri_insts.sail
$(call EXTRACT_INST,CStore)
$(call EXTRACT_INST,CSC)
$(call EXTRACT_INST,CLC)
+ $(call EXTRACT_INST,CReadHwr)
+ $(call EXTRACT_INST,CWriteHwr)
diff --git a/cheri/cheri_insts.sail b/cheri/cheri_insts.sail
index a1ddc8aa..fb3b370d 100644
--- a/cheri/cheri_insts.sail
+++ b/cheri/cheri_insts.sail
@@ -100,6 +100,9 @@ function clause decode (0b010010 @ 0b00000 @ rd : regno @ cb : regno @ 0b0010
function clause decode (0b010010 @ 0b00000 @ rd : regno @ cb : regno @ 0b00110 @ 0b111111) = Some(CGetOffset(rd, cb))
function clause decode (0b010010 @ 0b00000 @ cd : regno @ rs : regno @ 0b00111 @ 0b111111) = Some(CGetPCCSetOffset(cd, rs))
+function clause decode (0b010010 @ 0b00000 @ cd : regno @ sel : regno @ 0b01101 @ 0b111111) = Some(CReadHwr(cd, sel))
+function clause decode (0b010010 @ 0b00000 @ cb : regno @ sel : regno @ 0b01110 @ 0b111111) = Some(CWriteHwr(cb, sel))
+
/* Three operand */
/* Capability Modification */
@@ -345,6 +348,84 @@ function clause execute (CSetCause(rt)) =
/* END_CSetCause */
}
+union clause ast = CReadHwr : (regno, regno)
+function clause execute (CReadHwr(cd, sel)) =
+{
+ /* START_CReadHwr */
+ checkCP2usable();
+ let (needSup, needAccessSys) : (bool, bool) = match unsigned(sel) {
+ 0 => (false, false), /* DDC -- no access control */
+ 1 => (false, false), /* CTLSU -- no access control */
+ 8 => (false, true), /* CTLSP -- privileged TLS */
+ 22 => (true, false), /* KR1C */
+ 23 => (true, false), /* KR2C */
+ 29 => (true, true), /* KCC */
+ 30 => (true, true), /* KDC */
+ 31 => (true, true), /* EPCC */
+ _ => SignalException(ResI)
+ };
+ if register_inaccessible(cd) then
+ raise_c2_exception(CapEx_AccessSystemRegsViolation, cd)
+ else if needAccessSys & not(pcc_access_system_regs()) then
+ raise_c2_exception(CapEx_AccessSystemRegsViolation, sel)
+ else if needSup & not(grantsAccess(getAccessLevel(), Supervisor)) then
+ raise_c2_exception(CapEx_AccessSystemRegsViolation, sel)
+ else {
+ capVal : CapStruct = match unsigned(sel) {
+ 0 => readCapReg(DDC),
+ 1 => capRegToCapStruct(CTLSU),
+ 8 => capRegToCapStruct(CTLSP),
+ 22 => readCapReg(KR1C),
+ 23 => readCapReg(KR2C),
+ 29 => readCapReg(KCC),
+ 30 => readCapReg(KDC),
+ 31 => readCapReg(EPCC),
+ _ => {assert(false, "should be unreachable code"); undefined}
+ };
+ writeCapReg(cd, capVal);
+ };
+ /* END_CReadHwr */
+}
+
+union clause ast = CWriteHwr : (regno, regno)
+function clause execute (CWriteHwr(cb, sel)) =
+{
+ /* START_CWriteHwr */
+ checkCP2usable();
+ let (needSup, needAccessSys) : (bool, bool) = match unsigned(sel) {
+ 0 => (false, false), /* DDC -- no access control */
+ 1 => (false, false), /* CTLSU -- no access control */
+ 8 => (false, true), /* CTLSP -- privileged TLS */
+ 22 => (true, false), /* KR1C */
+ 23 => (true, false), /* KR2C */
+ 29 => (true, true), /* KCC */
+ 30 => (true, true), /* KDC */
+ 31 => (true, true), /* EPCC */
+ _ => SignalException(ResI)
+ };
+ if register_inaccessible(cb) then
+ raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
+ else if needAccessSys & not(pcc_access_system_regs()) then
+ raise_c2_exception(CapEx_AccessSystemRegsViolation, sel)
+ else if needSup & not(grantsAccess(getAccessLevel(), Supervisor)) then
+ raise_c2_exception(CapEx_AccessSystemRegsViolation, sel)
+ else {
+ capVal = readCapReg(cb);
+ match unsigned(sel) {
+ 0 => writeCapReg(DDC, capVal),
+ 1 => CTLSU = capStructToCapReg(capVal),
+ 8 => CTLSP = capStructToCapReg(capVal),
+ 22 => writeCapReg(KR1C, capVal),
+ 23 => writeCapReg(KR2C, capVal),
+ 29 => writeCapReg(KCC, capVal),
+ 30 => writeCapReg(KDC, capVal),
+ 31 => writeCapReg(EPCC, capVal),
+ _ => assert(false, "should be unreachable code")
+ };
+ };
+ /* END_CWriteHwr */
+}
+
union clause ast = CAndPerm : (regno, regno, regno)
function clause execute(CAndPerm(cd, cb, rt)) =
{
diff --git a/cheri/cheri_prelude_common.sail b/cheri/cheri_prelude_common.sail
index 9c51966b..c2fb9c24 100644
--- a/cheri/cheri_prelude_common.sail
+++ b/cheri/cheri_prelude_common.sail
@@ -78,7 +78,16 @@ register C29 : CapReg /* aka kernel code capability, KCC */
register C30 : CapReg /* aka kernel data capability, KDC */
register C31 : CapReg /* aka exception program counter capability, EPCC */
-let IDC : regno = 0b11010 /* 26 */
+register CTLSU : CapReg /* User thread local storage capabiltiy */
+register CTLSP : CapReg /* Privileged thread local storage capabiltiy */
+
+let DDC : regno = 0b00000 /* C0 */
+let IDC : regno = 0b11010 /* C26 */
+let KR1C : regno = 0b11011 /* C27 */
+let KR2C : regno = 0b11100 /* C28 */
+let KCC : regno = 0b11101 /* C29 */
+let KDC : regno = 0b11110 /* C30 */
+let EPCC : regno = 0b11111 /* C31 */
let CapRegs : vector(32, dec, register(CapReg)) =
[
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 {
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 21:40:54 +0000