diff options
Diffstat (limited to 'cheri')
| -rw-r--r-- | cheri/cheri_insts.sail | 15 | ||||
| -rw-r--r-- | cheri/cheri_prelude.sail | 67 |
2 files changed, 28 insertions, 54 deletions
diff --git a/cheri/cheri_insts.sail b/cheri/cheri_insts.sail index 39453fd5..a3c0dc2f 100644 --- a/cheri/cheri_insts.sail +++ b/cheri/cheri_insts.sail @@ -103,8 +103,8 @@ function clause execute (CGetCause(rd)) = { (* START_CGetCause *) checkCP2usable(); - if not (PCC.access_EPCC) then - raise_c2_exception_noreg(CapEx_AccessEPCCViolation) + if not (PCC.access_system_regs) then + raise_c2_exception_noreg(CapEx_AccessSystemRegsViolation) else wGPR(rd) := EXTZ(CapCause) (* END_CGetCause *) @@ -116,8 +116,8 @@ function clause execute (CSetCause((regno) rt)) = { (* START_CSetCause *) checkCP2usable(); - if not (PCC.access_EPCC) then - raise_c2_exception_noreg(CapEx_AccessEPCCViolation) + if not (PCC.access_system_regs) then + raise_c2_exception_noreg(CapEx_AccessSystemRegsViolation) else { (bit[64]) rt_val := rGPR(rt); @@ -146,11 +146,8 @@ function clause execute(CAndPerm(cd, cb, rt)) = else writeCapReg(cd, {cb_val with sw_perms = (cb_val.sw_perms & (rt_val[30..15])); - access_KR2C = (cb_val.access_KR2C & (rt_val[14])); - access_KR1C = (cb_val.access_KR1C & (rt_val[13])); - access_KCC = (cb_val.access_KCC & (rt_val[12])); - access_KDC = (cb_val.access_KDC & (rt_val[11])); - access_EPCC = (cb_val.access_EPCC & (rt_val[10])); + perm_reserved11_14 = (cb_val.perm_reserved11_14 & (rt_val[14..11])); + access_system_regs = (cb_val.access_system_regs & (rt_val[10])); perm_reserved9 = (cb_val.perm_reserved9 & (rt_val[9])); perm_reserved8 = (cb_val.perm_reserved8 & (rt_val[8])); permit_seal = (cb_val.permit_seal & (rt_val[7])); diff --git a/cheri/cheri_prelude.sail b/cheri/cheri_prelude.sail index 66115d1a..6a5aa340 100644 --- a/cheri/cheri_prelude.sail +++ b/cheri/cheri_prelude.sail @@ -38,11 +38,8 @@ typedef CapReg = register bits [256:0] { (* 255..248: reserved1; padding *) 247..224: otype; 223..208: sw_perms; - 207: access_KR2C; - 206: access_KR1C; - 205: access_KCC; - 204: access_KDC; - 203: access_EPCC; + 207..204: perm_reserved11_14; + 203: access_system_regs; 202: perm_reserved9; (* perm bit 9 *) 201: perm_reserved8; (* perm bit 8 *) 200: permit_seal; @@ -106,11 +103,8 @@ typedef CapStruct = const struct { bit[8] padding; bit[24] otype; bit[16] sw_perms; - bool access_KR2C; - bool access_KR1C; - bool access_KCC; - bool access_KDC; - bool access_EPCC; + bit[4] perm_reserved11_14; + bool access_system_regs; bool perm_reserved9; bool perm_reserved8; bool permit_seal; @@ -132,11 +126,8 @@ let (CapStruct) null_cap = { padding = 0; otype = 0; sw_perms = 0; - access_KR2C = false; - access_KR1C = false; - access_KCC = false; - access_KDC = false; - access_EPCC = false; + perm_reserved11_14 = 0; + access_system_regs = false; perm_reserved9 = false; perm_reserved8 = false; permit_seal = false; @@ -163,11 +154,8 @@ function CapStruct capRegToCapStruct((CapReg) capReg) = padding = capReg[255..248]; otype = capReg.otype; sw_perms = capReg.sw_perms; - access_KR2C = capReg.access_KR2C; - access_KR1C = capReg.access_KR1C; - access_KCC = capReg.access_KCC; - access_KDC = capReg.access_KDC; - access_EPCC = capReg.access_EPCC; + perm_reserved11_14 = capReg.perm_reserved11_14; + access_system_regs = capReg.access_system_regs; perm_reserved9 = capReg.perm_reserved9; perm_reserved8 = capReg.perm_reserved8; permit_seal = capReg.permit_seal; @@ -191,11 +179,8 @@ function (CapStruct) readCapReg((regno) n) = function (bit[31]) capPermsToVec((CapStruct) cap) = ( cap.sw_perms - : [cap.access_KR2C] - : [cap.access_KR1C] - : [cap.access_KCC] - : [cap.access_KDC] - : [cap.access_EPCC] + : cap.perm_reserved11_14 + : [cap.access_system_regs] : [cap.perm_reserved9] : [cap.perm_reserved8] : [cap.permit_seal] @@ -273,11 +258,7 @@ typedef CapEx = enumerate { CapEx_PermitStoreCapViolation; CapEx_PermitStoreLocalCapViolation; CapEx_PermitSealViolation; - CapEx_AccessEPCCViolation; - CapEx_AccessKDCViolation; - CapEx_AccessKCCViolation; - CapEx_AccessKR1CViolation; - CapEx_AccessKR2CViolation; + CapEx_AccessSystemRegsViolation; } typedef CGetXOp = enumerate { @@ -328,11 +309,7 @@ function (bit[8]) CapExCode((CapEx) ex) = case CapEx_PermitStoreCapViolation -> 0x15 case CapEx_PermitStoreLocalCapViolation -> 0x16 case CapEx_PermitSealViolation -> 0x17 - case CapEx_AccessEPCCViolation -> 0x18 - case CapEx_AccessKDCViolation -> 0x18 - case CapEx_AccessKCCViolation -> 0x18 - case CapEx_AccessKR1CViolation -> 0x18 - case CapEx_AccessKR2CViolation -> 0x18 + case CapEx_AccessSystemRegsViolation -> 0x18 } typedef CapCauseReg = register bits [15:0] { @@ -374,11 +351,11 @@ function forall Type 'o . 'o raise_c2_exception((CapEx) capEx, (regno) regnum) = function forall Type 'o . 'o raise_c2_exception_v((regno) regnum) = switch(regnum) { - case 0b11011 -> raise_c2_exception(CapEx_AccessKR1CViolation, regnum) - case 0b11100 -> raise_c2_exception(CapEx_AccessKR2CViolation, regnum) - case 0b11101 -> raise_c2_exception(CapEx_AccessKCCViolation, regnum) - case 0b11110 -> raise_c2_exception(CapEx_AccessKDCViolation, regnum) - case 0b11111 -> raise_c2_exception(CapEx_AccessEPCCViolation, regnum) + case 0b11011 -> raise_c2_exception(CapEx_AccessSystemRegsViolation, regnum) + case 0b11100 -> raise_c2_exception(CapEx_AccessSystemRegsViolation, regnum) + case 0b11101 -> raise_c2_exception(CapEx_AccessSystemRegsViolation, regnum) + case 0b11110 -> raise_c2_exception(CapEx_AccessSystemRegsViolation, regnum) + case 0b11111 -> raise_c2_exception(CapEx_AccessSystemRegsViolation, regnum) case _ -> assert(false, Some("should only call for cap reg violation")) } @@ -387,11 +364,11 @@ function forall Type 'o . 'o raise_c2_exception_noreg((CapEx) capEx) = function bool register_inaccessible((regno) r) = ~(switch(r) { - case 0b11011 -> (PCC.access_KR1C) - case 0b11100 -> (PCC.access_KR2C) - case 0b11101 -> (PCC.access_KCC) - case 0b11110 -> (PCC.access_KDC) - case 0b11111 -> (PCC.access_EPCC) + case 0b11011 -> (PCC.access_system_regs) + case 0b11100 -> (PCC.access_system_regs) + case 0b11101 -> (PCC.access_system_regs) + case 0b11110 -> (PCC.access_system_regs) + case 0b11111 -> (PCC.access_system_regs) case _ -> bitone }) |