summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--cheri/cheri_insts.sail53
-rw-r--r--cheri/cheri_prelude_common.sail114
2 files changed, 101 insertions, 66 deletions
diff --git a/cheri/cheri_insts.sail b/cheri/cheri_insts.sail
index 3df442d9..f1038ed6 100644
--- a/cheri/cheri_insts.sail
+++ b/cheri/cheri_insts.sail
@@ -363,14 +363,14 @@ function clause execute (CReadHwr(cd, sel)) =
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),
+ 0 => capRegToCapStruct(DDC),
+ 1 => capRegToCapStruct(CTLSU),
+ 8 => capRegToCapStruct(CTLSP),
+ 22 => capRegToCapStruct(KR1C),
+ 23 => capRegToCapStruct(KR2C),
+ 29 => capRegToCapStruct(KCC),
+ 30 => capRegToCapStruct(KDC),
+ 31 => capRegToCapStruct(EPCC),
_ => {assert(false, "should be unreachable code"); undefined}
};
writeCapReg(cd, capVal);
@@ -401,14 +401,14 @@ function clause execute (CWriteHwr(cb, 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),
+ 0 => DDC = capStructToCapReg(capVal),
+ 1 => CTLSU = capStructToCapReg(capVal),
+ 8 => CTLSP = capStructToCapReg(capVal),
+ 22 => KR1C = capStructToCapReg(capVal),
+ 23 => KR2C = capStructToCapReg(capVal),
+ 29 => KCC = capStructToCapReg(capVal),
+ 30 => KDC = capStructToCapReg(capVal),
+ 31 => EPCC = capStructToCapReg(capVal),
_ => assert(false, "should be unreachable code")
};
};
@@ -440,7 +440,7 @@ union clause ast = CToPtr : (regno, regno, regno)
function clause execute(CToPtr(rd, cb, ct)) =
{
checkCP2usable();
- let ct_val = readCapReg(ct);
+ let ct_val = readCapRegDDC(ct);
let cb_val = readCapReg(cb);
if (register_inaccessible(cb)) then
raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
@@ -714,7 +714,10 @@ function clause execute (ClearRegs(regset, m)) =
match regset {
GPLo => wGPR(to_bits(5, i)) = zeros(),
GPHi => wGPR(to_bits(5, i+16)) = zeros(),
- CLo => writeCapReg(to_bits(5, i)) = null_cap,
+ CLo => if i == 0 then
+ DDC = capStructToCapReg(null_cap)
+ else
+ writeCapReg(to_bits(5, i)) = null_cap,
CHi => writeCapReg(to_bits(5, i+16)) = null_cap
}
}
@@ -723,7 +726,7 @@ union clause ast = CFromPtr : (regno, regno, regno)
function clause execute (CFromPtr(cd, cb, rt)) =
{
checkCP2usable();
- cb_val = readCapReg(cb);
+ cb_val = readCapRegDDC(cb);
rt_val = rGPR(rt);
if (register_inaccessible(cd)) then
raise_c2_exception(CapEx_AccessSystemRegsViolation, cd)
@@ -747,7 +750,7 @@ union clause ast = CBuildCap : (regno, regno, regno)
function clause execute (CBuildCap(cd, cb, ct)) =
{
checkCP2usable();
- cb_val = readCapReg(cb);
+ cb_val = readCapRegDDC(cb);
ct_val = readCapReg(ct);
cb_base = getCapBase(cb_val);
ct_base = getCapBase(ct_val);
@@ -859,7 +862,7 @@ union clause ast = CTestSubset : (regno, regno, regno)
function clause execute (CTestSubset(rd, cb, ct)) =
{
checkCP2usable();
- cb_val = readCapReg(cb);
+ cb_val = readCapRegDDC(cb);
ct_val = readCapReg(ct);
ct_top = getCapTop(ct_val);
ct_base = getCapBase(ct_val);
@@ -1156,7 +1159,7 @@ union clause ast = CLoad : (regno, regno, regno, bits(8), bool, WordType, bool)
function clause execute (CLoad(rd, cb, rt, offset, signext, width, linked)) =
{
checkCP2usable();
- cb_val = readCapReg(cb);
+ cb_val = readCapRegDDC(cb);
if (register_inaccessible(cb)) then
raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
else if not (cb_val.tag) then
@@ -1198,7 +1201,7 @@ union clause ast = CStore : (regno, regno, regno, regno, bits(8), WordType, bool
function clause execute (CStore(rs, cb, rt, rd, offset, width, conditional)) =
{
checkCP2usable();
- cb_val = readCapReg(cb);
+ cb_val = readCapRegDDC(cb);
if (register_inaccessible(cb)) then
raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
else if not (cb_val.tag) then
@@ -1254,7 +1257,7 @@ function clause execute (CSC(cs, cb, rt, rd, offset, conditional)) =
{
checkCP2usable();
cs_val = readCapReg(cs);
- cb_val = readCapReg(cb);
+ cb_val = readCapRegDDC(cb);
if (register_inaccessible(cs)) then
raise_c2_exception(CapEx_AccessSystemRegsViolation, cs)
else if (register_inaccessible(cb)) then
@@ -1303,7 +1306,7 @@ union clause ast = CLC : (regno, regno, regno, bits(16), bool)
function clause execute (CLC(cd, cb, rt, offset, linked)) =
{
checkCP2usable();
- cb_val = readCapReg(cb);
+ cb_val = readCapRegDDC(cb);
if (register_inaccessible(cd)) then
raise_c2_exception(CapEx_AccessSystemRegsViolation, cd)
else if (register_inaccessible(cb)) then
diff --git a/cheri/cheri_prelude_common.sail b/cheri/cheri_prelude_common.sail
index cc4c657a..d2b69de8 100644
--- a/cheri/cheri_prelude_common.sail
+++ b/cheri/cheri_prelude_common.sail
@@ -45,7 +45,7 @@ register PCC : CapReg
register nextPCC : CapReg
register delayedPCC : CapReg
register inCCallDelay : bits(1)
-register C00 : CapReg /* aka default data capability, DDC */
+register DDC : CapReg
register C01 : CapReg
register C02 : CapReg
register C03 : CapReg
@@ -72,22 +72,28 @@ register C23 : CapReg
register C24 : CapReg /* aka return code capability, RCC */
register C25 : CapReg
register C26 : CapReg /* aka invoked data capability, IDC */
-register C27 : CapReg /* aka kernel reserved capability 1, KR1C */
-register C28 : CapReg /* aka kernel reserved capability 2, KR2C */
-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 */
+register C27 : CapReg
+register C28 : CapReg
+register C29 : CapReg
+register C30 : CapReg
+register C31 : CapReg
register CTLSU : CapReg /* User thread local storage capabiltiy */
register CTLSP : CapReg /* Privileged thread local storage capabiltiy */
+register KR1C : CapReg /* kernel reserved capability 1 */
+register KR2C : CapReg /* kernel reserved capability 2 */
+register KCC : CapReg /* kernel code capability */
+register KDC : CapReg /* kernel data capability */
+register EPCC : CapReg /* exception program counter capability */
-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 IDCNO : regno = 0b11010 /* C26, invoked data capability used be CCall */
+
+/* Special register used to have these numbers -- here for transition purposes */
+let KR1CNO : regno = 0b11011 /* C27 */
+let KR2CNO : regno = 0b11100 /* C28 */
+let KCCNO : regno = 0b11101 /* C29 */
+let KDCNO : regno = 0b11110 /* C30 */
+let EPCCNO : regno = 0b11111 /* C31 */
let CapRegs : vector(32, dec, register(CapReg)) =
[
@@ -122,7 +128,7 @@ let CapRegs : vector(32, dec, register(CapReg)) =
ref C03,
ref C02,
ref C01,
- ref C00
+ ref DDC
]
let max_otype = MAX(24) /*0xffffff*/
@@ -130,15 +136,32 @@ let have_cp2 = true
/*!
This function reads a given capability register and returns its contents converted to a CapStruct.
+If the argument is zero then the null capability is returned.
*/
val readCapReg : regno -> CapStruct effect {rreg}
function readCapReg(n) =
- let 'i = unsigned(n) in
- capRegToCapStruct(reg_deref(CapRegs[i]))
+ if (n == 0b00000) then
+ null_cap
+ else
+ let i = unsigned(n) in
+ capRegToCapStruct(reg_deref(CapRegs[i]))
+
+/*!
+This is the same as readCapReg except that when the argument is zero the value of DDC is returned
+instead of the null capability. This is used for instructions that expect an address, where using
+null would always generate an exception.
+*/
+val readCapRegDDC : regno -> CapStruct effect {rreg}
+function readCapRegDDC(n) =
+ let i = unsigned(n) in
+ capRegToCapStruct(reg_deref(CapRegs[i])) /* NB CapRegs[0] is points to DDC */
function writeCapReg(n, cap) : (regno, CapStruct) -> unit =
- let 'i = unsigned(n) in
- (*CapRegs[i]) = capStructToCapReg(cap)
+ if (n == 0b00000) then
+ ()
+ else
+ let i = unsigned(n) in
+ (*CapRegs[i]) = capStructToCapReg(cap)
enum CapEx = {
CapEx_None,
@@ -214,22 +237,22 @@ function SignalException (ex) =
let pcc = capRegToCapStruct(PCC) in
let (success, epcc) = setCapOffset(pcc, pc) in
if (success) then
- C31 = capStructToCapReg(epcc)
+ EPCC = capStructToCapReg(epcc)
else
- C31 = capStructToCapReg(int_to_cap(to_bits(64, getCapBase(pcc)) + unsigned(pc)));
+ EPCC = capStructToCapReg(int_to_cap(to_bits(64, getCapBase(pcc)) + unsigned(pc)));
};
- nextPCC = C29; /* KCC */
- delayedPCC = C29; /* always write delayedPCC together with nextPCC so
+ nextPCC = KCC;
+ delayedPCC = KCC; /* always write delayedPCC together with nextPCC so
that non-capability branches don't override PCC */
- let base = getCapBase(capRegToCapStruct(C29)) in
+ let base = getCapBase(capRegToCapStruct(KCC)) in
SignalExceptionMIPS(ex, to_bits(64, base));
}
function ERETHook() : unit -> unit =
{
- nextPCC = C31;
- delayedPCC = C31; /* always write delayedPCC together with nextPCC so
+ nextPCC = EPCC;
+ delayedPCC = EPCC; /* always write delayedPCC together with nextPCC so
that non-capability branches don't override PCC */
}
@@ -247,7 +270,7 @@ function raise_c2_exception8(capEx, regnum) =
val raise_c2_exception : forall ('o : Type) . (CapEx, regno) -> 'o effect {escape, rreg, wreg}
function raise_c2_exception(capEx, regnum) =
let reg8 = 0b000 @ regnum in
- if ((capEx == CapEx_AccessSystemRegsViolation) & (regnum == IDC)) then
+ if ((capEx == CapEx_AccessSystemRegsViolation) & (regnum == IDCNO)) then
raise_c2_exception8(CapEx_AccessCCallIDCViolation, reg8)
else
raise_c2_exception8(capEx, reg8)
@@ -266,12 +289,12 @@ The following function should be called before reading or writing any capability
*/
val register_inaccessible : regno -> bool effect {rreg}
function register_inaccessible(r) =
- ((r == IDC) & inCCallDelay) |
- ((r == KR1C |
- r == KR2C |
- r == KDC |
- r == KCC |
- r == EPCC) & not (pcc_access_system_regs ()))
+ ((r == IDCNO) & inCCallDelay) |
+ ((r == KR1CNO |
+ r == KR2CNO |
+ r == KDCNO |
+ r == KCCNO |
+ r == EPCCNO) & not (pcc_access_system_regs ()))
val MEMr_tag = "read_tag_bool" : bits(64) -> bool effect { rmemt }
val MEMw_tag = "write_tag_bool" : (bits(64) , bool) -> unit effect { wmvt }
@@ -355,7 +378,7 @@ val addrWrapper : (bits(64), MemAccessType, WordType) -> bits(64) effect {rreg,
function addrWrapper(addr, accessType, width) =
{
capno = 0b00000;
- cap = readCapReg(capno);
+ cap = readCapRegDDC(capno);
if (not (cap.tag)) then
(raise_c2_exception(CapEx_TagViolation, capno))
else if (cap.sealed) then
@@ -416,12 +439,21 @@ function checkCP2usable () =
function init_cp2_state () = {
let defaultBits = capStructToCapReg(default_cap);
+ let nullBits = capStructToCapReg(null_cap);
PCC = defaultBits;
nextPCC = defaultBits;
delayedPCC = defaultBits;
- foreach(i from 0 to 31) {
+ DDC = defaultBits;
+ KCC = defaultBits;
+ EPCC = defaultBits;
+ KDC = nullBits;
+ KR1C = nullBits;
+ KR2C = nullBits;
+ CTLSP = nullBits;
+ CTLSU = nullBits;
+ foreach(i from 1 to 31) {
let idx = to_bits(5, i) in
- writeCapReg(idx, default_cap);
+ writeCapReg(idx, null_cap)
}
}
@@ -457,15 +489,15 @@ function dump_cp2_state () = {
foreach(i from 0 to 31) {
print(concat_str("DEBUG CAP REG ", concat_str(string_of_int(i), capToString(readCapReg(to_bits(5, i))))))
};
- print(concat_str("DEBUG CAP HWREG 00", capToString(capRegToCapStruct(C00))));
+ print(concat_str("DEBUG CAP HWREG 00", capToString(capRegToCapStruct(DDC))));
print(concat_str("DEBUG CAP HWREG 01", capToString(capRegToCapStruct(CTLSU))));
print(concat_str("DEBUG CAP HWREG 08", capToString(capRegToCapStruct(CTLSP))));
/* TODO: these two should not be mirrored to match the FPGA */
- print(concat_str("DEBUG CAP HWREG 22", capToString(capRegToCapStruct(C27))));
- print(concat_str("DEBUG CAP HWREG 23", capToString(capRegToCapStruct(C28))));
+ print(concat_str("DEBUG CAP HWREG 22", capToString(capRegToCapStruct(KR1C))));
+ print(concat_str("DEBUG CAP HWREG 23", capToString(capRegToCapStruct(KR2C))));
/* KCC, KDC, EPCC */
- print(concat_str("DEBUG CAP HWREG 29", capToString(capRegToCapStruct(C29))));
- print(concat_str("DEBUG CAP HWREG 30", capToString(capRegToCapStruct(C30))));
- print(concat_str("DEBUG CAP HWREG 31", capToString(capRegToCapStruct(C31))));
+ print(concat_str("DEBUG CAP HWREG 29", capToString(capRegToCapStruct(KCC))));
+ print(concat_str("DEBUG CAP HWREG 30", capToString(capRegToCapStruct(KDC))));
+ print(concat_str("DEBUG CAP HWREG 31", capToString(capRegToCapStruct(EPCC))));
}
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 03:42:07 +0000