diff options
| author | Robert Norton | 2017-10-31 16:09:46 +0000 |
|---|---|---|
| committer | Robert Norton | 2017-10-31 16:09:46 +0000 |
| commit | a35692d69681683c2bffe7c824ad230b88679ed9 (patch) | |
| tree | 2b0962eb00a62c581a5eced904fa6451687cc382 /cheri | |
| parent | b41ee79485e155f67099b007650d73f449db1961 (diff) | |
cheri: throw an exception if there is an attempt to access C26/IDC in the delay slot of a ccall selector 1 call.
Diffstat (limited to 'cheri')
| -rw-r--r-- | cheri/cheri_insts.sail | 1 | ||||
| -rw-r--r-- | cheri/cheri_prelude_common.sail | 12 |
2 files changed, 11 insertions, 2 deletions
diff --git a/cheri/cheri_insts.sail b/cheri/cheri_insts.sail index 50399785..5687a275 100644 --- a/cheri/cheri_insts.sail +++ b/cheri/cheri_insts.sail @@ -1060,6 +1060,7 @@ function clause execute (CCall(cs, cb, 0b00000000001)) = (* selector=1 *) delayedPC := (bit[64]) (getCapOffset(cs_val)); delayedPCC := csUnsealed; branchPending := true; + inCCallDelay := true; C26 := capStructToCapReg({cb_val with sealed=false; otype=0; diff --git a/cheri/cheri_prelude_common.sail b/cheri/cheri_prelude_common.sail index dcb56d01..fa36decb 100644 --- a/cheri/cheri_prelude_common.sail +++ b/cheri/cheri_prelude_common.sail @@ -35,6 +35,7 @@ register CapReg PCC register CapReg nextPCC register CapReg delayedPCC +register (bit[1]) inCCallDelay register CapReg C00 (* aka default data capability, DDC *) register CapReg C01 register CapReg C02 @@ -105,6 +106,7 @@ typedef CapEx = enumerate { CapEx_PermitSealViolation; CapEx_AccessSystemRegsViolation; CapEx_PermitCCallViolation; + CapEx_AccessCCallIDCViolation; } typedef CPtrCmpOp = enumerate { @@ -148,6 +150,7 @@ function (bit[8]) CapExCode((CapEx) ex) = case CapEx_PermitSealViolation -> 0x17 case CapEx_AccessSystemRegsViolation -> 0x18 case CapEx_PermitCCallViolation -> 0x19 + case CapEx_AccessCCallIDCViolation -> 0x1a } typedef CapCauseReg = register bits [15:0] { @@ -194,7 +197,11 @@ function forall Type 'o . 'o raise_c2_exception8((CapEx) capEx, (bit[8]) regnum) } function forall Type 'o . 'o raise_c2_exception((CapEx) capEx, (regno) regnum) = - raise_c2_exception8(capEx, 0b000 : regnum) + let reg8 = 0b000 : regnum in + if ((capEx == CapEx_AccessSystemRegsViolation) & (regnum == 26 (* IDC *))) then + raise_c2_exception8(CapEx_AccessCCallIDCViolation, reg8) + else + raise_c2_exception8(capEx, reg8) function forall Type 'o . 'o raise_c2_exception_noreg((CapEx) capEx) = raise_c2_exception8(capEx, 0xff) @@ -203,7 +210,8 @@ function bool pcc_access_system_regs () = let pcc = capRegToCapStruct(PCC) in (pcc.access_system_regs) -function bool register_inaccessible((regno) r) = +function bool register_inaccessible((regno) r) = + if ((r == 26 (* IDC *)) & inCCallDelay) then true else let is_sys_reg = switch(r) { case 0b11011 -> true case 0b11100 -> true |