diff options
Diffstat (limited to 'cheri')
| -rw-r--r-- | cheri/cheri_insts.sail | 91 | ||||
| -rw-r--r-- | cheri/cheri_prelude.sail | 170 |
2 files changed, 261 insertions, 0 deletions
diff --git a/cheri/cheri_insts.sail b/cheri/cheri_insts.sail new file mode 100644 index 00000000..7b9e555f --- /dev/null +++ b/cheri/cheri_insts.sail @@ -0,0 +1,91 @@ +(* Operations that extract parts of a capability into GPR *) + +union ast member (CGetXOp, regno, regno) CGetX +function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : 0b00000000 : 0b000) = Some(CGetX(CGetPerm, rd, cb)) +function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : 0b00000000 : 0b001) = Some(CGetX(CGetType, rd, cb)) +function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : 0b00000000 : 0b010) = Some(CGetX(CGetBase, rd, cb)) +function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : 0b00000000 : 0b011) = Some(CGetX(CGetLen, rd, cb)) +(* NB CGetCause Handled separately *) +function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : 0b00000000 : 0b101) = Some(CGetX(CGetTag, rd, cb)) +function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : 0b00000000 : 0b110) = Some(CGetX(CGetUnsealed, rd, cb)) +function clause decode (0b010010 : 0b01101 : (regno) rd : (regno) cb : 0b00000000 : 0b010) = Some(CGetX(CGetOffset, rd, cb)) (* NB encoding does not follow pattern *) + +function clause execute (CGetX(op, rd, cb)) = + { + if (register_inaccessible(cb)) then + exit (raise_c2_exception_v(cb)) + else + { + cbval := CapRegs[cb]; + wGPR(rd) := switch(op) { + case CGetPerm -> EXTZ(cbval[223..193]) + case CGetType -> EXTZ(cbval.otype) + case CGetBase -> cbval.base + case CGetOffset -> cbval.cursor + case CGetLen -> cbval.length (* XXX only correct for 256-bit *) + case CGetTag -> EXTZ([cbval.tag]) + case CGetUnsealed -> EXTZ([cbval.sealed]) + } + } + } + + +union ast member regno CGetPCC +function clause decode (0b010010 : 0b00000 : 0b00000 : (regno) cd : 0b00000 : 0b000 : 0b111) = Some(CGetPCC(cd)) +function clause execute (CGetPCC(cd)) = + { + if (register_inaccessible(cd)) then + exit (raise_c2_exception_v(cd)) + else + { + (CapRegs[cd]).cursor := 0; + (*destReg := PCC;*) + (*destReg.cursor):= PC; XXX help *) + } + } +(* Get and Set CP2 cause register *) + +union ast member regno CGetCause +function clause decode (0b010010 : 0b00000 : (regno) rd : 0b00000 : 0b00000000 : 0b100) = Some(CGetCause(rd)) +function clause execute (CGetCause(rd)) = + { + if (~(PCC.access_EPCC)) then + exit (raise_c2_exception_noreg(CapEx_AccessEPCCViolation)) + else + wGPR(rd) := EXTZ(CapCause) + } + +union ast member (regno) CSetCause +function clause decode (0b010010 : 0b00100 : 0b00000 : 0b00000 : (regno) rt : 0b000 : 0b100) = Some(CSetCause(rt)) +function clause execute (CSetCause((regno) rt)) = + { + if (~(PCC.access_EPCC)) then + exit (raise_c2_exception_noreg(CapEx_AccessEPCCViolation)) + else + { + (bit[64]) rt_val := rGPR(rt); + CapCause.ExcCode := rt_val[15..8]; + CapCause.RegNum := rt_val[7..0]; + } + } + +union ast member (regno, regno, regno) CAndPerm +function clause decode (0b010010 : 0b00100 : (regno) cd : (regno) cb : (regno) rt : 0b000 : 0b000) = Some(CAndPerm(cd, cb, rt)) +function clause execute(CAndPerm(cd, cb, rt)) = +{ + cb_reg := CapRegs[cb]; + if (register_inaccessible(cd)) then + exit (raise_c2_exception_v(cd)) + else if (register_inaccessible(cb)) then + exit (raise_c2_exception_v(cb)) + else if (~(cb_reg.tag)) then + exit (raise_c2_exception(CapEx_TagViolation, cb)) + else if (~(cb_reg.sealed)) then + exit (raise_c2_exception(CapEx_SealViolation, cb)) + else + { + (CapRegs[cd]) := cb_reg; + (*cd_reg :=*) + } +} + diff --git a/cheri/cheri_prelude.sail b/cheri/cheri_prelude.sail new file mode 100644 index 00000000..ec64ea45 --- /dev/null +++ b/cheri/cheri_prelude.sail @@ -0,0 +1,170 @@ +(* 265-bit capability is really 257 bits including tag *) +typedef Capability = register bits [256:0] { + 256: tag; + 255..248: reserved; (* padding *) + 247..224: otype; + 223..208: sw_perms; + 207: access_KR2C; + 206: access_KR1C; + 205: access_KCC; + 204: access_KDC; + 203: access_EPCC; + 202: reserved; + 201: permit_set_type; + 200: permit_seal; + 199: permit_store_ephemeral_cap; + 198: permit_store_cap; + 197: permit_load_cap; + 196: permit_store; + 195: permit_load; + 194: permit_execute; + 193: non_ephemeral; + 192: sealed; + 191..128: cursor; + 127..64: base; + 63 .. 0: length; +} + +register Capability PCC +register Capability C00 (* aka default data capability, DDC *) +register Capability C01 +register Capability C02 +register Capability C03 +register Capability C04 +register Capability C05 +register Capability C06 +register Capability C07 +register Capability C08 +register Capability C09 +register Capability C10 +register Capability C11 +register Capability C12 +register Capability C13 +register Capability C14 +register Capability C15 +register Capability C16 +register Capability C17 +register Capability C18 +register Capability C19 +register Capability C20 +register Capability C21 +register Capability C22 +register Capability C23 +register Capability C24 (* aka return code capability, RCC *) +register Capability C25 +register Capability C26 (* aka invoked data capability, IDC *) +register Capability C27 (* aka kernel reserved capability 1, KR1C *) +register Capability C28 (* aka kernel reserved capability 2, KR2C *) +register Capability C29 (* aka kernel code capability, KCC *) +register Capability C30 (* aka kernel data capability, KDC *) +register Capability C31 (* aka exception program counter capability, EPCC *) + +let (vector <0, 32, inc, (Capability)>) CapRegs = + [ C00, C01, C02, C03, C04, C05, C06, C07, C08, C09, C10, + C11, C12, C13, C14, C15, C16, C17, C18, C19, C20, + C21, C22, C23, C24, C25, C26, C27, C28, C29, C30, C31 + ] + +typedef CapEx = enumerate { + CapEx_None; + CapEx_LengthVioloation; + CapEx_TagViolation; + CapEx_SealViolation; + CapEx_TypeViolation; + CapEx_CallTrap; + CapEx_ReturnTrap; + CapEx_TSSUnderFlow; + CapEx_UserDefViolation; + CapEx_TLBNoStoreCap; + CapEx_InexactBounds; + CapEx_GlobalViolation; + CapEx_PermitExecuteViolation; + CapEx_PermitLoadViolation; + CapEx_PermitStoreViolation; + CapEx_PermitLoadCapViolation; + CapEx_PermitStoreCapViolation; + CapEx_PermitStoreLocalCapViolation; + CapEx_PermitSealViolation; + CapEx_AccessEPCCViolation; + CapEx_AccessKDCViolation; + CapEx_AccessKCCViolation; + CapEx_AccessKR1CViolation; + CapEx_AccessKR2CViolation; +} + +typedef CGetXOp = enumerate { + CGetPerm; + CGetType; + CGetBase; + CGetOffset; + CGetLen; + CGetTag; + CGetUnsealed; +} + + + +function (bit[8]) CapExCode((CapEx) ex) = + switch(ex) { + case CapEx_None -> 0x00 + case CapEx_LengthVioloation -> 0x01 + case CapEx_TagViolation -> 0x02 + case CapEx_SealViolation -> 0x03 + case CapEx_TypeViolation -> 0x04 + case CapEx_CallTrap -> 0x05 + case CapEx_ReturnTrap -> 0x06 + case CapEx_TSSUnderFlow -> 0x07 + case CapEx_UserDefViolation -> 0x08 + case CapEx_TLBNoStoreCap -> 0x09 + case CapEx_InexactBounds -> 0x0a + case CapEx_GlobalViolation -> 0x10 + case CapEx_PermitExecuteViolation -> 0x11 + case CapEx_PermitLoadViolation -> 0x12 + case CapEx_PermitStoreViolation -> 0x13 + case CapEx_PermitLoadCapViolation -> 0x14 + case CapEx_PermitStoreCapViolation -> 0x15 + case CapEx_PermitStoreLocalCapViolation -> 0x16 + case CapEx_PermitSealViolation -> 0x17 + case CapEx_AccessEPCCViolation -> 0x1a + case CapEx_AccessKDCViolation -> 0x1b + case CapEx_AccessKCCViolation -> 0x1c + case CapEx_AccessKR1CViolation -> 0x1d + case CapEx_AccessKR2CViolation -> 0x1e + } + +typedef CapCauseReg = register bits [15:0] { + 15..8: ExcCode; + 7..0: RegNum; +} + +register CapCauseReg CapCause + +function unit raise_c2_exception((CapEx) capEx, (bit[8]) regnum) = + { + (CapCause.ExcCode) := CapExCode(capEx); + (CapCause.RegNum) := regnum; + SignalException(C2E); + } + +function unit raise_c2_exception_v((bit[8]) regnum) = + switch(regnum[4..0]) { + 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 _ -> assert(false, Some("should only call for cap reg violation")) + } + +function unit raise_c2_exception_noreg((CapEx) capEx) = + raise_c2_exception(capEx, 0xff) + +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 _ -> bitone + }) |