diff options
Diffstat (limited to 'cheri')
| -rw-r--r-- | cheri/cheri_insts.sail | 30 | ||||
| -rw-r--r-- | cheri/cheri_prelude.sail | 9 |
2 files changed, 38 insertions, 1 deletions
diff --git a/cheri/cheri_insts.sail b/cheri/cheri_insts.sail index 20df3a62..892ed1f6 100644 --- a/cheri/cheri_insts.sail +++ b/cheri/cheri_insts.sail @@ -12,6 +12,7 @@ function clause decode (0b010010 : 0b01101 : (regno) rd : (regno) cb : 0b0000000 function clause execute (CGetX(op, rd, cb)) = { + checkCP2usable(); if (register_inaccessible(cb)) then exit (raise_c2_exception_v(cb)) else @@ -34,6 +35,7 @@ union ast member regno CGetPCC function clause decode (0b010010 : 0b00000 : (regno) cd : 0b00000 : 0b11111 : 0b111111) = Some(CGetPCC(cd)) function clause execute (CGetPCC(cd)) = { + checkCP2usable(); if (register_inaccessible(cd)) then exit (raise_c2_exception_v(cd)) else @@ -45,6 +47,7 @@ union ast member (regno, regno) CGetPCCSetOffset function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) rs : 0b00111 : 0b111111) = Some(CGetPCCSetOffset(cd, rs)) function clause execute (CGetPCCSetOffset(cd, rs)) = { + checkCP2usable(); if (register_inaccessible(cd)) then exit (raise_c2_exception_v(cd)) else @@ -59,6 +62,7 @@ union ast member regno CGetCause function clause decode (0b010010 : 0b00000 : (regno) rd : 0b00000 : 0b00000000 : 0b100) = Some(CGetCause(rd)) function clause execute (CGetCause(rd)) = { + checkCP2usable(); if (~(PCC.access_EPCC)) then exit (raise_c2_exception_noreg(CapEx_AccessEPCCViolation)) else @@ -69,6 +73,7 @@ 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)) = { + checkCP2usable(); if (~(PCC.access_EPCC)) then exit (raise_c2_exception_noreg(CapEx_AccessEPCCViolation)) else @@ -83,6 +88,7 @@ union ast member regregreg 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)) = { + checkCP2usable(); cb_val := readCapReg(cb); rt_val := rGPR(rt); if (register_inaccessible(cd)) then @@ -120,6 +126,7 @@ union ast member regregreg CToPtr function clause decode (0b010010 : 0b01100 : (regno) rd : (regno) cb : (regno) ct : 0b000 : 0b000) = Some(CToPtr(rd, cb, ct)) function clause execute(CToPtr(rd, cb, ct)) = { + checkCP2usable(); ct_val := readCapReg(ct); cb_val := readCapReg(cb); if (register_inaccessible(cb)) then @@ -148,6 +155,7 @@ function clause decode (0b010010 : 0b01110 : (regno) rd : (regno) cb : (regno) c function clause execute(CPtrCmp(rd, cb, ct, op)) = { + checkCP2usable(); if (register_inaccessible(cb)) then exit (raise_c2_exception_v(cb)) else if (register_inaccessible(ct)) then @@ -191,6 +199,7 @@ union ast member regregreg CIncOffset function clause decode (0b010010 : 0b01101 : (regno) cd : (regno) cb : (regno) rt : 0b000 : 0b000) = Some(CIncOffset(cd, cb, rt)) function clause execute (CIncOffset(cd, cb, rt)) = { + checkCP2usable(); cb_val := readCapReg(cb); rt_val := rGPR(rt); if (register_inaccessible(cd)) then @@ -207,6 +216,7 @@ union ast member regregreg CSetOffset function clause decode (0b010010 : 0b01101 : (regno) cd : (regno) cb : (regno) rt : 0b000 : 0b001) = Some(CSetOffset(cd, cb, rt)) function clause execute (CSetOffset(cd, cb, rt)) = { + checkCP2usable(); cb_val := readCapReg(cb); rt_val := rGPR(rt); if (register_inaccessible(cd)) then @@ -223,6 +233,7 @@ union ast member regregreg CSetBounds function clause decode (0b010010 : 0b00001 : (regno) cd : (regno) cb : (regno) rt : 0b000000) = Some(CSetBounds(cd, cb, rt)) function clause execute (CSetBounds(cd, cb, rt)) = { + checkCP2usable(); cb_val := readCapReg(cb); (nat) rt_val := rGPR(rt); (nat) cursor := getCapCursor(cb_val); @@ -246,6 +257,7 @@ union ast member (regno, regno) CClearTag function clause decode (0b010010 : 0b00100 : (regno) cd : (regno) cb : 0b00000 : 0b000: 0b101) = Some(CClearTag(cd, cb)) function clause execute (CClearTag(cd, cb)) = { + checkCP2usable(); if (register_inaccessible(cd)) then exit (raise_c2_exception_v(cd)) else if (register_inaccessible(cb)) then @@ -264,6 +276,7 @@ function clause decode (0b010010 : 0b01111 : 0b00010 : (bit[16]) imm) = Some(Cle function clause decode (0b010010 : 0b01111 : 0b00011 : (bit[16]) imm) = Some(ClearRegs(CHi, imm)) (* CClearHi *) function clause execute (ClearRegs(regset, mask)) = { + checkCP2usable(); if (regset == CHi) then ()(* XXX check exception *); foreach (i from 0 to 15) @@ -280,6 +293,7 @@ union ast member regregreg CFromPtr function clause decode (0b010010 : 0b00100 : (regno) cd : (regno) cb : (regno) rt : 0b000: 0b111) = Some(CFromPtr(cd, cb, rt)) function clause execute (CFromPtr(cd, cb, rt)) = { + checkCP2usable(); cb_val := readCapReg(cb); rt_val := rGPR(rt); if (register_inaccessible(cd)) then @@ -300,6 +314,7 @@ union ast member (regno, regno) CCheckPerm function clause decode (0b010010 : 0b01011 : (regno) cs : 0b00000 : (regno) rt : 0b000: 0b000) = Some(CCheckPerm(cs, rt)) function clause execute (CCheckPerm(cs, rt)) = { + checkCP2usable(); cs_val := readCapReg(cs); cs_perms := capPermsToVec(cs_val); rt_perms := (rGPR(rt))[30..0]; @@ -315,6 +330,7 @@ union ast member (regno, regno) CCheckType function clause decode (0b010010 : 0b01011 : (regno) cs : (regno) cb : 0b00000 : 0b000: 0b001) = Some(CCheckType(cs, cb)) function clause execute (CCheckType(cs, cb)) = { + checkCP2usable(); cs_val := readCapReg(cs); cb_val := readCapReg(cb); if (register_inaccessible(cs)) then @@ -337,6 +353,7 @@ union ast member regregreg CSeal function clause decode (0b010010 : 0b00010 : (regno) cd : (regno) cs : (regno) ct : 0b000: 0b000) = Some(CSeal(cd, cs, ct)) function clause execute (CSeal(cd, cs, ct)) = { + checkCP2usable(); cs_val := readCapReg(cs); ct_val := readCapReg(ct); (nat) ct_cursor := ((nat)(ct_val.base) + (nat)(ct_val.offset)); @@ -368,6 +385,7 @@ union ast member regregreg CUnseal function clause decode (0b010010 : 0b00011 : (regno) cd : (regno) cs : (regno) ct : 0b000: 0b000) = Some(CUnseal(cd, cs, ct)) function clause execute (CUnseal(cd, cs, ct)) = { + checkCP2usable(); cs_val := readCapReg(cs); ct_val := readCapReg(ct); (nat) ct_cursor := ((nat)(ct_val.base) + (nat)(ct_val.offset)); @@ -403,6 +421,7 @@ union ast member (regno, regno) CCall function clause decode (0b010010 : 0b00101 : (regno) cs : (regno) cb : (bit[11]) selector) = Some(CCall(cs, cb)) function clause execute (CCall(cs, cb)) = { + checkCP2usable(); (* Partial implementation of CCall with checks in hardware, but raising a trap to perform trusted stack manipulation *) cs_val := readCapReg(cs); cb_val := readCapReg(cb); @@ -433,7 +452,10 @@ function clause execute (CCall(cs, cb)) = union ast member unit CReturn function clause decode (0b010010 : 0b00110 : 0b000000000000000000000) = Some(CReturn) function clause execute (CReturn) = - exit (raise_c2_exception_noreg(CapEx_ReturnTrap)) + { + checkCP2usable(); + exit (raise_c2_exception_noreg(CapEx_ReturnTrap)) + } union ast member (regno, bit[16], bool) CBX function clause decode (0b010010 : 0b01001 : (regno) cb : (bit[16]) imm) = Some(CBX(cb, imm, true)) (* CBTU *) @@ -441,6 +463,7 @@ function clause decode (0b010010 : 0b01010 : (regno) cb : (bit[16]) imm) = Some( function clause execute (CBX(cb, imm, invert)) = { + checkCP2usable(); if (register_inaccessible(cb)) then exit (raise_c2_exception_v(cb)) else if (((CapRegs[cb]).tag) ^ invert) then @@ -456,6 +479,7 @@ function clause decode (0b010010 : 0b00111 : (regno) cd : (regno) cb : 0b00000 : function clause decode (0b010010 : 0b01000 : 0b00000 : (regno) cb : 0b00000 : 0b000000) = Some(CJALR(0b00000, cb, false)) (* CJR *) function clause execute(CJALR(cd, cb, link)) = { + checkCP2usable(); cb_val := readCapReg(cb); if (link & register_inaccessible(cd)) then exit (raise_c2_exception_v(cd)) @@ -502,6 +526,7 @@ function clause decode (0b010010 : 0b10000 : (regno) rd : (regno) cb : 0b0000000 function clause execute (CLoad(rd, cb, rt, offset, signext, width, linked)) = { + checkCP2usable(); cb_val := readCapReg(cb); if (register_inaccessible(cb)) then exit (raise_c2_exception_v(cb)) @@ -556,6 +581,7 @@ function clause decode (0b010010 : 0b10000 : (regno) rs : (regno) cb : (regno) r function clause execute (CStore(rs, cb, rt, rd, offset, width, conditional)) = { + checkCP2usable(); cb_val := readCapReg(cb); if (register_inaccessible(cb)) then exit (raise_c2_exception_v(cb)) @@ -612,6 +638,7 @@ function clause decode (0b111110 : (regno) cs : (regno) cb: (regno) rt : (bit[11 function clause decode (0b010010 : 0b10000 : (regno) cs : (regno) cb: (regno) rd : 0b00 : 0b0111) = Some(CSC(cs, cb, 0b00000, rd, 0b00000000000, true)) function clause execute (CSC(cs, cb, rt, rd, offset, conditional)) = { + checkCP2usable(); cs_val := readCapReg(cs); cb_val := readCapReg(cb); if (register_inaccessible(cs)) then @@ -659,6 +686,7 @@ function clause decode (0b110110 : (regno) cd : (regno) cb: (regno) rt : (bit[11 function clause decode (0b010010 : 0b10000 : (regno) cd : (regno) cb: 0b0000000 : 0b1111) = Some(CLC(cd, cb, 0b00000, 0b00000000000, true)) function clause execute (CLC(cd, cb, rt, offset, linked)) = { + checkCP2usable(); cb_val := readCapReg(cb); if (register_inaccessible(cd)) then exit (raise_c2_exception_v(cd)) diff --git a/cheri/cheri_prelude.sail b/cheri/cheri_prelude.sail index 7c5e34a9..8fa3b180 100644 --- a/cheri/cheri_prelude.sail +++ b/cheri/cheri_prelude.sail @@ -416,3 +416,12 @@ function (bit[64]) TranslateAddress ((bit[64]) vAddr, (MemAccessType) accessType exit (raise_c2_exception_noreg(CapEx_LengthViolation)) (* XXX take exception properly *) else TLBTranslate(absPC, accessType) + +function unit checkCP2usable () = + { + if (~((CP0Status.CU)[2])) then + { + (CP0Cause.CE) := 0b10; + exit (SignalException(CpU)); + } + } |