diff options
| author | Alasdair Armstrong | 2017-11-30 20:26:49 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2017-11-30 20:26:49 +0000 |
| commit | d61eb1760eb48158ca2ebc7eadb75f0d4882c9da (patch) | |
| tree | bdf32238488b46cfc8e047c2fed882b60e11e148 /cheri/cheri_prelude_common.sail | |
| parent | dd00feacb373defbcfd8c50b9a8381c4a7db7cba (diff) | |
| parent | 16c269d6f26fd69d8788c448b87f4bb479a6ef66 (diff) | |
Merge branch 'master' into experiments
Diffstat (limited to 'cheri/cheri_prelude_common.sail')
| -rw-r--r-- | cheri/cheri_prelude_common.sail | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/cheri/cheri_prelude_common.sail b/cheri/cheri_prelude_common.sail index f5fcd095..a2d3b441 100644 --- a/cheri/cheri_prelude_common.sail +++ b/cheri/cheri_prelude_common.sail @@ -45,6 +45,7 @@ scattered function option<ast> decode 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 @@ -115,6 +116,7 @@ typedef CapEx = enumerate { CapEx_PermitSealViolation; CapEx_AccessSystemRegsViolation; CapEx_PermitCCallViolation; + CapEx_AccessCCallIDCViolation; } typedef CPtrCmpOp = enumerate { @@ -158,6 +160,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] { @@ -204,7 +207,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) @@ -213,7 +220,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 *)) & ((bool)inCCallDelay)) then true else (* XXX interpreter crash without cast *) let (bool) is_sys_reg = switch(r) { case 0b11011 -> true case 0b11100 -> true |