diff options
Diffstat (limited to 'cheri')
| -rw-r--r-- | cheri/cheri_insts.sail | 236 | ||||
| -rw-r--r-- | cheri/cheri_prelude.sail | 30 |
2 files changed, 133 insertions, 133 deletions
diff --git a/cheri/cheri_insts.sail b/cheri/cheri_insts.sail index b084faa0..39453fd5 100644 --- a/cheri/cheri_insts.sail +++ b/cheri/cheri_insts.sail @@ -49,7 +49,7 @@ function clause execute (CGetX(op, rd, cb)) = (* START_CGetX *) checkCP2usable(); if (register_inaccessible(cb)) then - exit (raise_c2_exception_v(cb)) + raise_c2_exception_v(cb) else { cbval := CapRegs[cb]; @@ -73,7 +73,7 @@ function clause execute (CGetPCC(cd)) = (* START_CGetPCC *) checkCP2usable(); if (register_inaccessible(cd)) then - exit (raise_c2_exception_v(cd)) + raise_c2_exception_v(cd) else let pcc = (capRegToCapStruct(PCC)) in writeCapReg(cd, {pcc with offset = PC}) @@ -87,7 +87,7 @@ function clause execute (CGetPCCSetOffset(cd, rs)) = (* START_CGetPCCSetOffset *) checkCP2usable(); if (register_inaccessible(cd)) then - exit (raise_c2_exception_v(cd)) + raise_c2_exception_v(cd) else let pcc = (capRegToCapStruct(PCC)) in let rs_val = rGPR(rs) in @@ -104,7 +104,7 @@ function clause execute (CGetCause(rd)) = (* START_CGetCause *) checkCP2usable(); if not (PCC.access_EPCC) then - exit (raise_c2_exception_noreg(CapEx_AccessEPCCViolation)) + raise_c2_exception_noreg(CapEx_AccessEPCCViolation) else wGPR(rd) := EXTZ(CapCause) (* END_CGetCause *) @@ -117,7 +117,7 @@ function clause execute (CSetCause((regno) rt)) = (* START_CSetCause *) checkCP2usable(); if not (PCC.access_EPCC) then - exit (raise_c2_exception_noreg(CapEx_AccessEPCCViolation)) + raise_c2_exception_noreg(CapEx_AccessEPCCViolation) else { (bit[64]) rt_val := rGPR(rt); @@ -136,13 +136,13 @@ function clause execute(CAndPerm(cd, cb, rt)) = cb_val := readCapReg(cb); rt_val := rGPR(rt); if (register_inaccessible(cd)) then - exit (raise_c2_exception_v(cd)) + raise_c2_exception_v(cd) else if (register_inaccessible(cb)) then - exit (raise_c2_exception_v(cb)) + raise_c2_exception_v(cb) else if not (cb_val.tag) then - exit (raise_c2_exception(CapEx_TagViolation, cb)) + raise_c2_exception(CapEx_TagViolation, cb) else if (cb_val.sealed) then - exit (raise_c2_exception(CapEx_SealViolation, cb)) + raise_c2_exception(CapEx_SealViolation, cb) else writeCapReg(cd, {cb_val with sw_perms = (cb_val.sw_perms & (rt_val[30..15])); @@ -174,11 +174,11 @@ function clause execute(CToPtr(rd, cb, ct)) = ct_val := readCapReg(ct); cb_val := readCapReg(cb); if (register_inaccessible(cb)) then - exit (raise_c2_exception_v(cb)) + raise_c2_exception_v(cb) else if (register_inaccessible(ct)) then - exit (raise_c2_exception_v(ct)) + raise_c2_exception_v(ct) else if not (ct_val.tag) then - exit (raise_c2_exception(CapEx_TagViolation, ct)) + raise_c2_exception(CapEx_TagViolation, ct) else { wGPR(rd) := if not (cb_val.tag) then @@ -198,9 +198,9 @@ function clause execute(CSub(rd, cb, ct)) = ct_val := readCapReg(ct); cb_val := readCapReg(cb); if (register_inaccessible(cb)) then - exit (raise_c2_exception_v(cb)) + raise_c2_exception_v(cb) else if (register_inaccessible(ct)) then - exit (raise_c2_exception_v(ct)) + raise_c2_exception_v(ct) else { wGPR(rd) := (bit[64])(getCapCursor(cb_val) - getCapCursor(ct_val)) @@ -222,9 +222,9 @@ function clause execute(CPtrCmp(rd, cb, ct, op)) = (* START_CPtrCmp *) checkCP2usable(); if (register_inaccessible(cb)) then - exit (raise_c2_exception_v(cb)) + raise_c2_exception_v(cb) else if (register_inaccessible(ct)) then - exit (raise_c2_exception_v(ct)) + raise_c2_exception_v(ct) else { cb_val := readCapReg(cb); @@ -270,11 +270,11 @@ function clause execute (CIncOffset(cd, cb, rt)) = cb_val := readCapReg(cb); rt_val := rGPR(rt); if (register_inaccessible(cd)) then - exit (raise_c2_exception_v(cd)) + raise_c2_exception_v(cd) else if (register_inaccessible(cb)) then - exit (raise_c2_exception_v(cb)) + raise_c2_exception_v(cb) else if ((cb_val.tag) & (cb_val.sealed) & (rt_val != 0x0000000000000000)) then - exit (raise_c2_exception(CapEx_SealViolation, cb)) + raise_c2_exception(CapEx_SealViolation, cb) else writeCapReg(cd, {cb_val with offset=cb_val.offset+rt_val}) (* END_CIncOffset *) @@ -289,11 +289,11 @@ function clause execute (CSetOffset(cd, cb, rt)) = cb_val := readCapReg(cb); rt_val := rGPR(rt); if (register_inaccessible(cd)) then - exit (raise_c2_exception_v(cd)) + raise_c2_exception_v(cd) else if (register_inaccessible(cb)) then - exit (raise_c2_exception_v(cb)) + raise_c2_exception_v(cb) else if ((cb_val.tag) & (cb_val.sealed)) then - exit (raise_c2_exception(CapEx_SealViolation, cb)) + raise_c2_exception(CapEx_SealViolation, cb) else writeCapReg(cd, {cb_val with offset=rt_val}) (* END_CSetOffset *) @@ -309,17 +309,17 @@ function clause execute (CSetBounds(cd, cb, rt)) = (nat) rt_val := rGPR(rt); (nat) cursor := getCapCursor(cb_val); if (register_inaccessible(cd)) then - exit (raise_c2_exception_v(cd)) + raise_c2_exception_v(cd) else if (register_inaccessible(cb)) then - exit (raise_c2_exception_v(cb)) + raise_c2_exception_v(cb) else if not (cb_val.tag) then - exit (raise_c2_exception(CapEx_TagViolation, cb)) + raise_c2_exception(CapEx_TagViolation, cb) else if (cb_val.sealed) then - exit (raise_c2_exception(CapEx_SealViolation, cb)) + raise_c2_exception(CapEx_SealViolation, cb) else if (cursor < ((nat)(cb_val.base))) then - exit (raise_c2_exception(CapEx_LengthViolation, cb)) + raise_c2_exception(CapEx_LengthViolation, cb) else if ((cursor + rt_val) > ((nat)(cb_val.base) + (nat)(cb_val.length))) then - exit (raise_c2_exception(CapEx_LengthViolation, cb)) + raise_c2_exception(CapEx_LengthViolation, cb) else writeCapReg(cd, {cb_val with base=(bit[64])cursor; length=(bit[64])rt_val; offset=0}) (* END_CSetBounds *) @@ -332,9 +332,9 @@ function clause execute (CClearTag(cd, cb)) = (* START_CClearTag *) checkCP2usable(); if (register_inaccessible(cd)) then - exit (raise_c2_exception_v(cd)) + raise_c2_exception_v(cd) else if (register_inaccessible(cb)) then - exit (raise_c2_exception_v(cb)) + raise_c2_exception_v(cb) else { cb_val := readCapReg(cb); @@ -357,7 +357,7 @@ function clause execute (ClearRegs(regset, mask)) = foreach (i from 0 to 15) let r = ((bit[5]) (i+16)) in if (mask[i] & register_inaccessible(r)) then - exit (raise_c2_exception_v(r)); + raise_c2_exception_v(r); foreach (i from 0 to 15) if (mask[i]) then switch (regset) { @@ -378,15 +378,15 @@ function clause execute (CFromPtr(cd, cb, rt)) = cb_val := readCapReg(cb); rt_val := rGPR(rt); if (register_inaccessible(cd)) then - exit (raise_c2_exception_v(cd)) + raise_c2_exception_v(cd) else if (register_inaccessible(cb)) then - exit (raise_c2_exception_v(cb)) + raise_c2_exception_v(cb) else if (rt == 0) then writeCapReg(cd, null_cap) else if not (cb_val.tag) then - exit (raise_c2_exception(CapEx_TagViolation, cb)) + raise_c2_exception(CapEx_TagViolation, cb) else if (cb_val.sealed) then - exit (raise_c2_exception(CapEx_SealViolation, cb)) + raise_c2_exception(CapEx_SealViolation, cb) else writeCapReg(cd, {cb_val with offset = rt_val}); (* END_CFromPtr *) @@ -402,11 +402,11 @@ function clause execute (CCheckPerm(cs, rt)) = cs_perms := capPermsToVec(cs_val); rt_perms := (rGPR(rt))[30..0]; if (register_inaccessible(cs)) then - exit (raise_c2_exception_v(cs)) + raise_c2_exception_v(cs) else if not (cs_val.tag) then - exit (raise_c2_exception(CapEx_TagViolation, cs)) + raise_c2_exception(CapEx_TagViolation, cs) else if ((cs_perms & rt_perms) != rt_perms) then - exit (raise_c2_exception(CapEx_UserDefViolation, cs)) + raise_c2_exception(CapEx_UserDefViolation, cs) else () (* END_CCheckPerm *) @@ -421,19 +421,19 @@ function clause execute (CCheckType(cs, cb)) = cs_val := readCapReg(cs); cb_val := readCapReg(cb); if (register_inaccessible(cs)) then - exit (raise_c2_exception_v(cs)) + raise_c2_exception_v(cs) else if (register_inaccessible(cb)) then - exit (raise_c2_exception_v(cb)) + raise_c2_exception_v(cb) else if not (cs_val.tag) then - exit (raise_c2_exception(CapEx_TagViolation, cs)) + raise_c2_exception(CapEx_TagViolation, cs) else if not (cb_val.tag) then - exit (raise_c2_exception(CapEx_TagViolation, cb)) + raise_c2_exception(CapEx_TagViolation, cb) else if not (cs_val.sealed) then - exit (raise_c2_exception(CapEx_SealViolation, cs)) + raise_c2_exception(CapEx_SealViolation, cs) else if not (cb_val.sealed) then - exit (raise_c2_exception(CapEx_SealViolation, cb)) + raise_c2_exception(CapEx_SealViolation, cb) else if ((cs_val.otype) != (cb_val.otype)) then - exit (raise_c2_exception(CapEx_TypeViolation, cs)) + raise_c2_exception(CapEx_TypeViolation, cs) else () (* END_CCheckType *) @@ -449,25 +449,25 @@ function clause execute (CSeal(cd, cs, ct)) = ct_val := readCapReg(ct); (nat) ct_cursor := ((nat)(ct_val.base) + (nat)(ct_val.offset)); if (register_inaccessible(cd)) then - exit (raise_c2_exception_v(cd)) + raise_c2_exception_v(cd) else if (register_inaccessible(cs)) then - exit (raise_c2_exception_v(cs)) + raise_c2_exception_v(cs) else if (register_inaccessible(ct)) then - exit (raise_c2_exception_v(ct)) + raise_c2_exception_v(ct) else if not (cs_val.tag) then - exit (raise_c2_exception(CapEx_TagViolation, cs)) + raise_c2_exception(CapEx_TagViolation, cs) else if not (ct_val.tag) then - exit (raise_c2_exception(CapEx_TagViolation, ct)) + raise_c2_exception(CapEx_TagViolation, ct) else if (cs_val.sealed) then - exit (raise_c2_exception(CapEx_SealViolation, cs)) + raise_c2_exception(CapEx_SealViolation, cs) else if (ct_val.sealed) then - exit (raise_c2_exception(CapEx_SealViolation, ct)) + raise_c2_exception(CapEx_SealViolation, ct) else if not (ct_val.permit_seal) then - exit (raise_c2_exception(CapEx_PermitSealViolation, ct)) + raise_c2_exception(CapEx_PermitSealViolation, ct) else if ((nat)(ct_val.offset) >= (nat)(ct_val.length)) then - exit (raise_c2_exception(CapEx_LengthViolation, ct)) + raise_c2_exception(CapEx_LengthViolation, ct) else if (ct_cursor > max_otype) then - exit (raise_c2_exception(CapEx_LengthViolation, ct)) + raise_c2_exception(CapEx_LengthViolation, ct) else writeCapReg(cd, {cs_val with sealed=true; otype=((bit[24])ct_cursor)}) (* END_CSeal *) @@ -483,25 +483,25 @@ function clause execute (CUnseal(cd, cs, ct)) = ct_val := readCapReg(ct); (nat) ct_cursor := ((nat)(ct_val.base) + (nat)(ct_val.offset)); if (register_inaccessible(cd)) then - exit (raise_c2_exception_v(cd)) + raise_c2_exception_v(cd) else if (register_inaccessible(cs)) then - exit (raise_c2_exception_v(cs)) + raise_c2_exception_v(cs) else if (register_inaccessible(ct)) then - exit (raise_c2_exception_v(ct)) + raise_c2_exception_v(ct) else if not (cs_val.tag) then - exit (raise_c2_exception(CapEx_TagViolation, cs)) + raise_c2_exception(CapEx_TagViolation, cs) else if not (ct_val.tag) then - exit (raise_c2_exception(CapEx_TagViolation, ct)) + raise_c2_exception(CapEx_TagViolation, ct) else if not (cs_val.sealed) then - exit (raise_c2_exception(CapEx_SealViolation, cs)) + raise_c2_exception(CapEx_SealViolation, cs) else if (ct_val.sealed) then - exit (raise_c2_exception(CapEx_SealViolation, ct)) + raise_c2_exception(CapEx_SealViolation, ct) else if (ct_cursor != ((nat)(cs_val.otype))) then - exit (raise_c2_exception(CapEx_TypeViolation, ct)) + raise_c2_exception(CapEx_TypeViolation, ct) else if not (ct_val.permit_seal) then - exit (raise_c2_exception(CapEx_PermitSealViolation, ct)) + raise_c2_exception(CapEx_PermitSealViolation, ct) else if (unsigned(ct_val.offset) >= unsigned(ct_val.length)) then - exit (raise_c2_exception(CapEx_LengthViolation, ct)) + raise_c2_exception(CapEx_LengthViolation, ct) else writeCapReg(cd, {cs_val with sealed=false; @@ -521,27 +521,27 @@ function clause execute (CCall(cs, cb)) = cs_val := readCapReg(cs); cb_val := readCapReg(cb); if (register_inaccessible(cs)) then - exit (raise_c2_exception_v(cs)) + raise_c2_exception_v(cs) else if (register_inaccessible(cb)) then - exit (raise_c2_exception_v(cb)) + raise_c2_exception_v(cb) else if not (cs_val.tag) then - exit (raise_c2_exception(CapEx_TagViolation, cs)) + raise_c2_exception(CapEx_TagViolation, cs) else if not (cb_val.tag) then - exit (raise_c2_exception(CapEx_TagViolation, cb)) + raise_c2_exception(CapEx_TagViolation, cb) else if not (cs_val.sealed) then - exit (raise_c2_exception(CapEx_SealViolation, cs)) + raise_c2_exception(CapEx_SealViolation, cs) else if not (cb_val.sealed) then - exit (raise_c2_exception(CapEx_SealViolation, cb)) + raise_c2_exception(CapEx_SealViolation, cb) else if ((cs_val.otype) != (cb_val.otype)) then - exit (raise_c2_exception(CapEx_TypeViolation, cs)) + raise_c2_exception(CapEx_TypeViolation, cs) else if not (cs_val.permit_execute) then - exit (raise_c2_exception(CapEx_PermitExecuteViolation, cs)) + raise_c2_exception(CapEx_PermitExecuteViolation, cs) else if (cb_val.permit_execute) then - exit (raise_c2_exception(CapEx_PermitExecuteViolation, cb)) + raise_c2_exception(CapEx_PermitExecuteViolation, cb) else if (cs_val.offset >= cs_val.length) then - exit (raise_c2_exception(CapEx_LengthViolation, cs)) + raise_c2_exception(CapEx_LengthViolation, cs) else - exit (raise_c2_exception(CapEx_CallTrap, cs)); + raise_c2_exception(CapEx_CallTrap, cs); (* END_CCall *) } @@ -551,7 +551,7 @@ function clause execute (CReturn) = { (* START_CReturn *) checkCP2usable(); - exit (raise_c2_exception_noreg(CapEx_ReturnTrap)) + raise_c2_exception_noreg(CapEx_ReturnTrap) (* END_CReturn *) } @@ -564,7 +564,7 @@ function clause execute (CBX(cb, imm, invert)) = (* START_CBx *) checkCP2usable(); if (register_inaccessible(cb)) then - exit (raise_c2_exception_v(cb)) + raise_c2_exception_v(cb) else if (((CapRegs[cb]).tag) ^ invert) then { let (bit[64]) offset = (EXTS(imm : 0b00) + 4) in @@ -583,21 +583,21 @@ function clause execute(CJALR(cd, cb, link)) = checkCP2usable(); cb_val := readCapReg(cb); if (link & register_inaccessible(cd)) then - exit (raise_c2_exception_v(cd)) + raise_c2_exception_v(cd) else if (register_inaccessible(cb)) then - exit (raise_c2_exception_v(cb)) + raise_c2_exception_v(cb) else if not (cb_val.tag) then - exit (raise_c2_exception(CapEx_TagViolation, cb)) + raise_c2_exception(CapEx_TagViolation, cb) else if (cb_val.sealed) then - exit (raise_c2_exception(CapEx_SealViolation, cb)) + raise_c2_exception(CapEx_SealViolation, cb) else if not (cb_val.permit_execute) then - exit (raise_c2_exception(CapEx_PermitExecuteViolation, cb)) + raise_c2_exception(CapEx_PermitExecuteViolation, cb) else if not (cb_val.global) then - exit (raise_c2_exception(CapEx_GlobalViolation, cb)) + raise_c2_exception(CapEx_GlobalViolation, cb) else if (((nat)(cb_val.offset)) + 4 > ((nat) (cb_val.length))) then - exit (raise_c2_exception(CapEx_LengthViolation, cb)) + raise_c2_exception(CapEx_LengthViolation, cb) else if (((cb_val.base+cb_val.offset)[1..0]) != 0b00) then - exit (SignalException(AdEL)) + SignalException(AdEL) else { if (link) then @@ -632,13 +632,13 @@ 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)) + raise_c2_exception_v(cb) else if not (cb_val.tag) then - exit (raise_c2_exception(CapEx_TagViolation, cb)) + raise_c2_exception(CapEx_TagViolation, cb) else if (cb_val.sealed) then - exit (raise_c2_exception(CapEx_SealViolation, cb)) + raise_c2_exception(CapEx_SealViolation, cb) else if not (cb_val.permit_load) then - exit (raise_c2_exception(CapEx_PermitLoadViolation, cb)) + raise_c2_exception(CapEx_PermitLoadViolation, cb) else { size := wordWidthBytes(width); @@ -646,11 +646,11 @@ function clause execute (CLoad(rd, cb, rt, offset, signext, width, linked)) = vAddr := cursor + unsigned(rGPR(rt)) + (size*signed(offset)); vAddr64:= (bit[64]) vAddr; if ((vAddr + size) > ((nat) (cb_val.base) + ((nat) (cb_val.length)))) then - exit (raise_c2_exception(CapEx_LengthViolation, cb)) + raise_c2_exception(CapEx_LengthViolation, cb) else if (vAddr < ((nat) (cb_val.base))) then - exit (raise_c2_exception(CapEx_LengthViolation, cb)) + raise_c2_exception(CapEx_LengthViolation, cb) else if not (isAddressAligned(vAddr64, width)) then - exit (SignalExceptionBadAddr(AdEL, vAddr64)) + SignalExceptionBadAddr(AdEL, vAddr64) else { pAddr := (TLBTranslate(vAddr64, LoadData)); @@ -689,13 +689,13 @@ 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)) + raise_c2_exception_v(cb) else if not (cb_val.tag) then - exit (raise_c2_exception(CapEx_TagViolation, cb)) + raise_c2_exception(CapEx_TagViolation, cb) else if (cb_val.sealed) then - exit (raise_c2_exception(CapEx_SealViolation, cb)) + raise_c2_exception(CapEx_SealViolation, cb) else if not (cb_val.permit_store) then - exit (raise_c2_exception(CapEx_PermitStoreViolation, cb)) + raise_c2_exception(CapEx_PermitStoreViolation, cb) else { size := wordWidthBytes(width); @@ -703,11 +703,11 @@ function clause execute (CStore(rs, cb, rt, rd, offset, width, conditional)) = vAddr := cursor + unsigned(rGPR(rt)) + (size * signed(offset)); vAddr64:= (bit[64]) vAddr; if ((vAddr + size) > ((nat) (cb_val.base) + ((nat) (cb_val.length)))) then - exit (raise_c2_exception(CapEx_LengthViolation, cb)) + raise_c2_exception(CapEx_LengthViolation, cb) else if (vAddr < ((nat) (cb_val.base))) then - exit (raise_c2_exception(CapEx_LengthViolation, cb)) + raise_c2_exception(CapEx_LengthViolation, cb) else if not (isAddressAligned(vAddr64, width)) then - exit (SignalExceptionBadAddr(AdES, vAddr64)) + SignalExceptionBadAddr(AdES, vAddr64) else { pAddr := (TLBTranslate(vAddr64, StoreData)); @@ -749,33 +749,33 @@ function clause execute (CSC(cs, cb, rt, rd, offset, conditional)) = cs_val := readCapReg(cs); cb_val := readCapReg(cb); if (register_inaccessible(cs)) then - exit (raise_c2_exception_v(cs)) + raise_c2_exception_v(cs) else if (register_inaccessible(cb)) then - exit (raise_c2_exception_v(cb)) + raise_c2_exception_v(cb) else if not (cb_val.tag) then - exit (raise_c2_exception(CapEx_TagViolation, cb)) + raise_c2_exception(CapEx_TagViolation, cb) else if (cb_val.sealed) then - exit (raise_c2_exception(CapEx_SealViolation, cb)) + raise_c2_exception(CapEx_SealViolation, cb) else if not (cb_val.permit_store_cap) then - exit (raise_c2_exception(CapEx_PermitStoreCapViolation, cb)) + raise_c2_exception(CapEx_PermitStoreCapViolation, cb) else if not (cb_val.permit_store_local_cap) & (cs_val.tag) & not (cs_val.global) then - exit (raise_c2_exception(CapEx_PermitStoreLocalCapViolation, cb)) + raise_c2_exception(CapEx_PermitStoreLocalCapViolation, cb) else { cursor := getCapCursor(cb_val); vAddr := cursor + unsigned(rGPR(rt)) + (16 * signed(offset)); vAddr64:= (bit[64]) vAddr; if ((vAddr + cap_size) > ((nat) (cb_val.base) + ((nat) (cb_val.length)))) then - exit (raise_c2_exception(CapEx_LengthViolation, cb)) + raise_c2_exception(CapEx_LengthViolation, cb) else if (vAddr < ((nat) (cb_val.base))) then - exit (raise_c2_exception(CapEx_LengthViolation, cb)) + raise_c2_exception(CapEx_LengthViolation, cb) else if (vAddr64[4..0] != 0b00000) then - exit (SignalExceptionBadAddr(AdES, vAddr64)) + SignalExceptionBadAddr(AdES, vAddr64) else { let (pAddr, noStoreCap) = (TLBTranslateC(vAddr64, StoreData)) in if (cs_val.tag & noStoreCap) then - exit (raise_c2_exception(CapEx_TLBNoStoreCap, cs)) + raise_c2_exception(CapEx_TLBNoStoreCap, cs) else if (conditional) then { success := if (CP0LLBit[0]) then @@ -800,26 +800,26 @@ 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)) + raise_c2_exception_v(cd) else if (register_inaccessible(cb)) then - exit (raise_c2_exception_v(cb)) + raise_c2_exception_v(cb) else if not (cb_val.tag) then - exit (raise_c2_exception(CapEx_TagViolation, cb)) + raise_c2_exception(CapEx_TagViolation, cb) else if (cb_val.sealed) then - exit (raise_c2_exception(CapEx_SealViolation, cb)) + raise_c2_exception(CapEx_SealViolation, cb) else if not (cb_val.permit_load_cap) then - exit (raise_c2_exception(CapEx_PermitLoadCapViolation, cb)) + raise_c2_exception(CapEx_PermitLoadCapViolation, cb) else { cursor := getCapCursor(cb_val); vAddr := cursor + unsigned(rGPR(rt)) + (16*signed(offset)); vAddr64:= (bit[64]) vAddr; if ((vAddr + cap_size) > ((nat) (cb_val.base) + ((nat) (cb_val.length)))) then - exit (raise_c2_exception(CapEx_LengthViolation, cb)) + raise_c2_exception(CapEx_LengthViolation, cb) else if (vAddr < ((nat) (cb_val.base))) then - exit (raise_c2_exception(CapEx_LengthViolation, cb)) + raise_c2_exception(CapEx_LengthViolation, cb) else if (vAddr64[4..0] != 0b00000) then - exit (SignalExceptionBadAddr(AdEL, vAddr64)) + SignalExceptionBadAddr(AdEL, vAddr64) else { let (pAddr, suppressTag) = (TLBTranslateC(vAddr64, LoadData)) in diff --git a/cheri/cheri_prelude.sail b/cheri/cheri_prelude.sail index 23973782..66115d1a 100644 --- a/cheri/cheri_prelude.sail +++ b/cheri/cheri_prelude.sail @@ -342,7 +342,7 @@ typedef CapCauseReg = register bits [15:0] { register CapCauseReg CapCause -function unit SignalException ((Exception) ex) = +function forall Type 'o . 'o SignalException ((Exception) ex) = { C31 := PCC; C31.offset := PC; @@ -359,7 +359,7 @@ function unit ERETHook() = that non-capability branches don't override PCC *) } -function unit raise_c2_exception8((CapEx) capEx, (bit[8]) regnum) = +function forall Type 'o . 'o raise_c2_exception8((CapEx) capEx, (bit[8]) regnum) = { (CapCause.ExcCode) := CapExCode(capEx); (CapCause.RegNum) := regnum; @@ -369,10 +369,10 @@ function unit raise_c2_exception8((CapEx) capEx, (bit[8]) regnum) = SignalException(mipsEx); } -function unit raise_c2_exception((CapEx) capEx, (regno) regnum) = +function forall Type 'o . 'o raise_c2_exception((CapEx) capEx, (regno) regnum) = raise_c2_exception8(capEx, 0b000 : regnum) -function unit raise_c2_exception_v((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) @@ -382,7 +382,7 @@ function unit raise_c2_exception_v((regno) regnum) = case _ -> assert(false, Some("should only call for cap reg violation")) } -function unit raise_c2_exception_noreg((CapEx) capEx) = +function forall Type 'o . 'o raise_c2_exception_noreg((CapEx) capEx) = raise_c2_exception8(capEx, 0xff) function bool register_inaccessible((regno) r) = @@ -457,22 +457,22 @@ function bit[64] addrWrapper((bit[64]) addr, (MemAccessType) accessType, (WordTy capno := 0b00000; cap := readCapReg(capno); if (~(cap.tag)) then - exit (raise_c2_exception(CapEx_TagViolation, capno)) + (raise_c2_exception(CapEx_TagViolation, capno)) else if (cap.sealed) then - exit (raise_c2_exception(CapEx_SealViolation, capno)); + (raise_c2_exception(CapEx_SealViolation, capno)); switch (accessType) { - case Instruction -> if (~(cap.permit_execute)) then exit (raise_c2_exception(CapEx_PermitExecuteViolation, capno)) - case LoadData -> if (~(cap.permit_load)) then exit (raise_c2_exception(CapEx_PermitLoadViolation, capno)) - case StoreData -> if (~(cap.permit_store)) then exit (raise_c2_exception(CapEx_PermitStoreViolation, capno)) + case Instruction -> if (~(cap.permit_execute)) then (raise_c2_exception(CapEx_PermitExecuteViolation, capno)) + case LoadData -> if (~(cap.permit_load)) then (raise_c2_exception(CapEx_PermitLoadViolation, capno)) + case StoreData -> if (~(cap.permit_store)) then (raise_c2_exception(CapEx_PermitStoreViolation, capno)) }; cursor := getCapCursor(cap); vAddr := cursor + unsigned(addr); vAddr64:= (bit[64]) vAddr; size := wordWidthBytes(width); if ((vAddr + size) > ((nat) (cap.base) + ((nat) (cap.length)))) then - exit (raise_c2_exception(CapEx_LengthViolation, capno)) + (raise_c2_exception(CapEx_LengthViolation, capno)) else if (vAddr < ((nat) (cap.base))) then - exit (raise_c2_exception(CapEx_LengthViolation, capno)); + (raise_c2_exception(CapEx_LengthViolation, capno)); vAddr64; } @@ -482,9 +482,9 @@ function (bit[64]) TranslateAddress ((bit[64]) vAddr, (MemAccessType) accessType let (bit[64]) length = PCC.length in let (bit[64]) absPC = (base + vAddr) in if (absPC[1..0] != 0b00) then (* bad PC alignment *) - exit (SignalExceptionBadAddr(AdEL, absPC)) + (SignalExceptionBadAddr(AdEL, absPC)) else if ((unsigned(vAddr) + 4) > unsigned(length)) then - exit (raise_c2_exception_noreg(CapEx_LengthViolation)) + (raise_c2_exception_noreg(CapEx_LengthViolation)) else TLBTranslate(absPC, accessType) } @@ -494,7 +494,7 @@ function unit checkCP2usable () = if (~((CP0Status.CU)[2])) then { (CP0Cause.CE) := 0b10; - exit (SignalException(CpU)); + (SignalException(CpU)); } } |