diff options
| author | Peter Sewell | 2017-01-26 09:31:39 +0000 |
|---|---|---|
| committer | Peter Sewell | 2017-01-26 09:31:39 +0000 |
| commit | 9c825884245e1cb5f6ad1fbc66a7d0c9fca24fe9 (patch) | |
| tree | a3a63dc27883648ff9343117860064790a8c4f50 | |
| parent | 4f2c4427c0f578ade8a7454220ad600bf190ae81 (diff) | |
| parent | db4d71f55e40747538c4df601fa5f4f6b0e6b0b6 (diff) | |
Merge branch 'master' of bitbucket.org:Peter_Sewell/sail
| -rw-r--r-- | cheri/cheri_insts.sail | 281 | ||||
| -rw-r--r-- | cheri/cheri_insts_128.sail | 973 | ||||
| -rw-r--r-- | cheri/cheri_prelude_128.sail | 337 | ||||
| -rw-r--r-- | cheri/cheri_prelude_256.sail | 207 | ||||
| -rw-r--r-- | cheri/cheri_prelude_common.sail (renamed from cheri/cheri_prelude.sail) | 254 | ||||
| -rw-r--r-- | src/Makefile | 6 | ||||
| -rw-r--r-- | src/lem_interp/interp.lem | 2 | ||||
| -rw-r--r-- | src/lem_interp/interp_lib.lem | 13 |
8 files changed, 512 insertions, 1561 deletions
diff --git a/cheri/cheri_insts.sail b/cheri/cheri_insts.sail index 06a27dcb..525ff324 100644 --- a/cheri/cheri_insts.sail +++ b/cheri/cheri_insts.sail @@ -34,36 +34,108 @@ (* 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)) +union ast member (regno, regno) CGetPerm +union ast member (regno, regno) CGetType +union ast member (regno, regno) CGetBase +union ast member (regno, regno) CGetLen +union ast member (regno, regno) CGetTag +union ast member (regno, regno) CGetSealed +union ast member (regno, regno) CGetOffset + +function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : 0b00000000 : 0b000) = Some(CGetPerm(rd, cb)) +function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : 0b00000000 : 0b001) = Some(CGetType(rd, cb)) +function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : 0b00000000 : 0b010) = Some(CGetBase(rd, cb)) +function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : 0b00000000 : 0b011) = Some(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 decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : 0b00000000 : 0b101) = Some(CGetTag(rd, cb)) +function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : 0b00000000 : 0b110) = Some(CGetSealed(rd, cb)) +function clause decode (0b010010 : 0b01101 : (regno) rd : (regno) cb : 0b00000000 : 0b010) = Some(CGetOffset(rd, cb)) (* NB encoding does not follow pattern *) -function clause execute (CGetX(op, rd, cb)) = +function clause execute (CGetPerm(rd, cb)) = { - (* START_CGetX *) + (* START_CGetPerms *) checkCP2usable(); if (register_inaccessible(cb)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) else - { - cbval := CapRegs[cb]; - wGPR(rd) := switch(op) { - case CGetPerm -> EXTZ(cbval[223..193]) (* XXX only correct for 256-bit *) - case CGetType -> EXTZ(cbval.otype) - case CGetBase -> cbval.base - case CGetOffset -> cbval.offset - case CGetLen -> cbval.length - case CGetTag -> EXTZ([cbval.tag]) - case CGetUnsealed -> EXTZ([cbval.sealed]) - } - } - (* END_CGetX *) + let capVal = readCapReg(cb) in + wGPR(rd) := EXTZ(getCapPerms(capVal)); + (* END_CGetPerms *) +} + +function clause execute (CGetType(rd, cb)) = +{ + (* START_CGetType *) + checkCP2usable(); + if (register_inaccessible(cb)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) + else + let capVal = readCapReg(cb) in + wGPR(rd) := EXTZ(capVal.otype); + (* END_CGetType *) +} + +function clause execute (CGetBase(rd, cb)) = +{ + (* START_CGetBase *) + checkCP2usable(); + if (register_inaccessible(cb)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) + else + let capVal = readCapReg(cb) in + wGPR(rd) := getCapBase(capVal); + (* END_CGetBase *) +} + +function clause execute (CGetOffset(rd, cb)) = +{ + (* START_CGetOffset *) + checkCP2usable(); + if (register_inaccessible(cb)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) + else + let capVal = readCapReg(cb) in + wGPR(rd) := getCapOffset(capVal); + (* END_CGetOffset *) +} + +function clause execute (CGetLen(rd, cb)) = +{ + (* START_CGetLen *) + checkCP2usable(); + if (register_inaccessible(cb)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) + else + let capVal = readCapReg(cb) in + let len65 = getCapLength(capVal) in + let len64 = if unsigned(len65) > MAX_U64 then + (bit[64]) MAX_U64 else len65[63..0] in + wGPR(rd) := len64; + (* END_CGetLen *) +} + +function clause execute (CGetTag(rd, cb)) = +{ + (* START_CGetTag *) + checkCP2usable(); + if (register_inaccessible(cb)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) + else + let capVal = readCapReg(cb) in + wGPR(rd) := EXTZ(capVal.tag); + (* END_CGetTag *) +} + +function clause execute (CGetSealed(rd, cb)) = +{ + (* START_CGetSealed *) + checkCP2usable(); + if (register_inaccessible(cb)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) + else + let capVal = readCapReg(cb) in + wGPR(rd) := EXTZ(capVal.sealed); + (* END_CGetSealed *) } union ast member regno CGetPCC @@ -76,10 +148,13 @@ function clause execute (CGetPCC(cd)) = raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) else let pcc = (capRegToCapStruct(PCC)) in - writeCapReg(cd, {pcc with offset = PC}) + let (success, pcc2) = setCapOffset(pcc, PC) in + {assert (success, None); (* guaranteed to be in-bounds *) + writeCapReg(cd, pcc2)}; (* END_CGetPCC *) } + 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)) = @@ -91,10 +166,13 @@ function clause execute (CGetPCCSetOffset(cd, rs)) = else let pcc = (capRegToCapStruct(PCC)) in let rs_val = rGPR(rs) in - writeCapReg(cd, {pcc with offset = rs_val}) + let (success, newPCC) = setCapOffset(pcc, rs_val) in + if (success) then + writeCapReg(cd, newPCC) + else + writeCapReg(cd, int_to_cap(rs_val)); (* END_CGetPCCSetOffset *) } - (* Get and Set CP2 cause register *) union ast member regno CGetCause @@ -103,7 +181,7 @@ function clause execute (CGetCause(rd)) = { (* START_CGetCause *) checkCP2usable(); - if not (PCC.access_system_regs) then + if not (pcc_access_system_regs ()) then raise_c2_exception_noreg(CapEx_AccessSystemRegsViolation) else wGPR(rd) := EXTZ(CapCause) @@ -116,7 +194,7 @@ function clause execute (CSetCause((regno) rt)) = { (* START_CSetCause *) checkCP2usable(); - if not (PCC.access_system_regs) then + if not (pcc_access_system_regs ()) then raise_c2_exception_noreg(CapEx_AccessSystemRegsViolation) else { @@ -144,24 +222,14 @@ function clause execute(CAndPerm(cd, cb, rt)) = else if (cb_val.sealed) then raise_c2_exception(CapEx_SealViolation, cb) else - writeCapReg(cd, {cb_val with - sw_perms = (cb_val.sw_perms & (rt_val[30..15])); - perm_reserved11_14 = (cb_val.perm_reserved11_14 & (rt_val[14..11])); - access_system_regs = (cb_val.access_system_regs & (rt_val[10])); - perm_reserved9 = (cb_val.perm_reserved9 & (rt_val[9])); - perm_reserved8 = (cb_val.perm_reserved8 & (rt_val[8])); - permit_seal = (cb_val.permit_seal & (rt_val[7])); - permit_store_local_cap = (cb_val.permit_store_local_cap & (rt_val[6])); - permit_store_cap = (cb_val.permit_store_cap & (rt_val[5])); - permit_load_cap = (cb_val.permit_load_cap & (rt_val[4])); - permit_store = (cb_val.permit_store & (rt_val[3])); - permit_load = (cb_val.permit_load & (rt_val[2])); - permit_execute = (cb_val.permit_execute & (rt_val[1])); - global = (cb_val.global & (rt_val[0])); - }) + let perms = getCapPerms(cb_val) in + let newCap = setCapPerms(cb_val, (perms & rt_val[30..0])) in + writeCapReg(cd, newCap); (* END_CAndPerm *) } + + 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)) = @@ -181,11 +249,13 @@ function clause execute(CToPtr(rd, cb, ct)) = wGPR(rd) := if not (cb_val.tag) then ((bit[64]) 0) else - (bit[64])(((nat)(cb_val.base)) + ((nat) (cb_val.offset)) - ((nat)(ct_val.base))) + (bit[64])(getCapCursor(cb_val) - unsigned(getCapBase(ct_val))) } (* END_CToPtr *) } + + union ast member regregreg CSub function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : (regno) ct : 0b001010) = Some(CSub(rd, cb, ct)) function clause execute(CSub(rd, cb, ct)) = @@ -273,7 +343,11 @@ function clause execute (CIncOffset(cd, cb, rt)) = else if ((cb_val.tag) & (cb_val.sealed) & (rt_val != 0x0000000000000000)) then raise_c2_exception(CapEx_SealViolation, cb) else - writeCapReg(cd, {cb_val with offset=cb_val.offset+rt_val}) + let (success, newCap) = incCapOffset(cb_val, rt_val) in + if (success) then + writeCapReg(cd, newCap) + else + writeCapReg(cd, int_to_cap(getCapBase(cb_val) + rt_val)) (* END_CIncOffset *) } @@ -292,7 +366,11 @@ function clause execute (CSetOffset(cd, cb, rt)) = else if ((cb_val.tag) & (cb_val.sealed)) then raise_c2_exception(CapEx_SealViolation, cb) else - writeCapReg(cd, {cb_val with offset=rt_val}) + let (success, newCap) = setCapOffset(cb_val, rt_val) in + if (success) then + writeCapReg(cd, newCap) + else + writeCapReg(cd, int_to_cap(getCapBase(cb_val) + rt_val)) (* END_CSetOffset *) } @@ -303,8 +381,11 @@ function clause execute (CSetBounds(cd, cb, rt)) = (* START_CSetBounds *) checkCP2usable(); cb_val := readCapReg(cb); - (nat) rt_val := rGPR(rt); - (nat) cursor := getCapCursor(cb_val); + rt_val := unsigned(rGPR(rt)); + cursor := getCapCursor(cb_val); + base := unsigned(getCapBase(cb_val)); + top := unsigned(getCapTop(cb_val)); + newTop := cursor + rt_val; if (register_inaccessible(cd)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) else if (register_inaccessible(cb)) then @@ -313,15 +394,49 @@ function clause execute (CSetBounds(cd, cb, rt)) = raise_c2_exception(CapEx_TagViolation, cb) else if (cb_val.sealed) then raise_c2_exception(CapEx_SealViolation, cb) - else if (cursor < ((nat)(cb_val.base))) then + else if (cursor < base) then raise_c2_exception(CapEx_LengthViolation, cb) - else if ((cursor + rt_val) > ((nat)(cb_val.base) + (nat)(cb_val.length))) then + else if (newTop > top) then raise_c2_exception(CapEx_LengthViolation, cb) else - writeCapReg(cd, {cb_val with base=(bit[64])cursor; length=(bit[64])rt_val; offset=0}) + let (_, newCap) = setCapBounds(cb_val, (bit[64]) cursor, (bit[65]) newTop) in + writeCapReg(cd, newCap) (* ignore exact *) (* END_CSetBounds *) } + +union ast member regregreg CSetBoundsExact +function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cb : (regno) rt : 0b001001) = Some(CSetBoundsExact(cd, cb, rt)) +function clause execute (CSetBoundsExact(cd, cb, rt)) = +{ + (* START_CSetBoundsExact *) + checkCP2usable(); + cb_val := readCapReg(cb); + rt_val := unsigned(rGPR(rt)); + cursor := getCapCursor(cb_val); + base := unsigned(getCapBase(cb_val)); + top := unsigned(getCapTop(cb_val)); + if (register_inaccessible(cd)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) + else if (register_inaccessible(cb)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) + else if not (cb_val.tag) then + raise_c2_exception(CapEx_TagViolation, cb) + else if (cb_val.sealed) then + raise_c2_exception(CapEx_SealViolation, cb) + else if (cursor < base) then + raise_c2_exception(CapEx_LengthViolation, cb) + else if ((cursor + rt_val) > top) then + raise_c2_exception(CapEx_LengthViolation, cb) + else + let (exact, newCap) = setCapBounds(cb_val, (bit[64]) base, (bit[65]) top) in + if not (exact) then + raise_c2_exception(CapEx_InexactBounds, cb) + else + writeCapReg(cd, newCap) + (* END_CSetBoundsExact *) +} + 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)) = @@ -385,7 +500,11 @@ function clause execute (CFromPtr(cd, cb, rt)) = else if (cb_val.sealed) then raise_c2_exception(CapEx_SealViolation, cb) else - writeCapReg(cd, {cb_val with offset = rt_val}); + let (success, newCap) = setCapOffset(cb_val, rt_val) in + if (success) then + writeCapReg(cd, newCap) + else + writeCapReg(cd, int_to_cap(getCapBase(cb_val) + rt_val)) (* END_CFromPtr *) } @@ -396,8 +515,8 @@ function clause execute (CCheckPerm(cs, rt)) = (* START_CCheckPerm *) checkCP2usable(); cs_val := readCapReg(cs); - cs_perms := capPermsToVec(cs_val); - rt_perms := (rGPR(rt))[30..0]; + cs_perms := EXTZ(getCapPerms(cs_val)); + rt_perms := rGPR(rt); if (register_inaccessible(cs)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cs) else if not (cs_val.tag) then @@ -444,7 +563,8 @@ 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)); + ct_cursor := getCapCursor(ct_val); + ct_top := unsigned(getCapTop(ct_val)); if (register_inaccessible(cd)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) else if (register_inaccessible(cs)) then @@ -461,12 +581,16 @@ function clause execute (CSeal(cd, cs, ct)) = raise_c2_exception(CapEx_SealViolation, ct) else if not (ct_val.permit_seal) then raise_c2_exception(CapEx_PermitSealViolation, ct) - else if ((nat)(ct_val.offset) >= (nat)(ct_val.length)) then + else if (ct_cursor >= ct_top) then raise_c2_exception(CapEx_LengthViolation, ct) else if (ct_cursor > max_otype) then raise_c2_exception(CapEx_LengthViolation, ct) else - writeCapReg(cd, {cs_val with sealed=true; otype=((bit[24])ct_cursor)}) + let (success, newCap) = sealCap(cs_val, (bit[24]) ct_cursor) in + if not (success) then + raise_c2_exception(CapEx_InexactBounds, cs) + else + writeCapReg(cd, newCap) (* END_CSeal *) } @@ -478,7 +602,7 @@ 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)); + ct_cursor := getCapCursor(ct_val); if (register_inaccessible(cd)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) else if (register_inaccessible(cs)) then @@ -493,11 +617,11 @@ function clause execute (CUnseal(cd, cs, ct)) = raise_c2_exception(CapEx_SealViolation, cs) else if (ct_val.sealed) then raise_c2_exception(CapEx_SealViolation, ct) - else if (ct_cursor != ((nat)(cs_val.otype))) then + else if (ct_cursor != unsigned(cs_val.otype)) then raise_c2_exception(CapEx_TypeViolation, ct) else if not (ct_val.permit_seal) then raise_c2_exception(CapEx_PermitSealViolation, ct) - else if (unsigned(ct_val.offset) >= unsigned(ct_val.length)) then + else if (ct_cursor >= unsigned(getCapTop(ct_val))) then raise_c2_exception(CapEx_LengthViolation, ct) else writeCapReg(cd, {cs_val with @@ -535,7 +659,7 @@ function clause execute (CCall(cs, cb)) = raise_c2_exception(CapEx_PermitExecuteViolation, cs) else if (cb_val.permit_execute) then raise_c2_exception(CapEx_PermitExecuteViolation, cb) - else if (cs_val.offset >= cs_val.length) then + else if (getCapCursor(cs_val) >= unsigned(getCapTop(cs_val))) then raise_c2_exception(CapEx_LengthViolation, cs) else raise_c2_exception(CapEx_CallTrap, cs); @@ -562,7 +686,7 @@ function clause execute (CBX(cb, imm, invert)) = checkCP2usable(); if (register_inaccessible(cb)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) - else if (((CapRegs[cb]).tag) ^ invert) then + else if (((readCapReg(cb)).tag) ^ invert) then { let (bit[64]) offset = (EXTS(imm : 0b00) + 4) in delayedPC := PC + offset; @@ -579,6 +703,8 @@ function clause execute(CJALR(cd, cb, link)) = (* START_CJALR *) checkCP2usable(); cb_val := readCapReg(cb); + cb_ptr := getCapCursor(cb_val); + cb_top := unsigned(getCapTop(cb_val)); if (link & register_inaccessible(cd)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) else if (register_inaccessible(cb)) then @@ -591,16 +717,21 @@ function clause execute(CJALR(cd, cb, link)) = raise_c2_exception(CapEx_PermitExecuteViolation, cb) else if not (cb_val.global) then raise_c2_exception(CapEx_GlobalViolation, cb) - else if (((nat)(cb_val.offset)) + 4 > ((nat) (cb_val.length))) then + else if (cb_ptr + 4 > cb_top) then raise_c2_exception(CapEx_LengthViolation, cb) - else if (((cb_val.base+cb_val.offset)[1..0]) != 0b00) then + else if ((cb_ptr mod 4) != 0) then SignalException(AdEL) else { if (link) then - writeCapReg(cd, {capRegToCapStruct(PCC) with offset=(PC+8)}); - delayedPC := cb_val.offset; - delayedPCC := capStructToBit257(cb_val); + let pcc = capRegToCapStruct(PCC) in + let (success, linkCap) = setCapOffset(pcc, PC+8) in + if (success) then + writeCapReg(cd, linkCap) + else + assert(false, None); + delayedPC := getCapOffset(cb_val); + delayedPCC := capStructToCapReg(cb_val); branchPending := 1; } (* END_CJALR *) @@ -642,9 +773,9 @@ function clause execute (CLoad(rd, cb, rt, offset, signext, width, linked)) = cursor := getCapCursor(cb_val); vAddr := cursor + unsigned(rGPR(rt)) + (size*signed(offset)); vAddr64:= (bit[64]) vAddr; - if ((vAddr + size) > ((nat) (cb_val.base) + ((nat) (cb_val.length)))) then + if ((vAddr + size) > unsigned(getCapTop(cb_val))) then raise_c2_exception(CapEx_LengthViolation, cb) - else if (vAddr < ((nat) (cb_val.base))) then + else if (vAddr < unsigned(getCapBase(cb_val))) then raise_c2_exception(CapEx_LengthViolation, cb) else if not (isAddressAligned(vAddr64, width)) then SignalExceptionBadAddr(AdEL, vAddr64) @@ -699,9 +830,9 @@ function clause execute (CStore(rs, cb, rt, rd, offset, width, conditional)) = cursor := getCapCursor(cb_val); vAddr := cursor + unsigned(rGPR(rt)) + (size * signed(offset)); vAddr64:= (bit[64]) vAddr; - if ((vAddr + size) > ((nat) (cb_val.base) + ((nat) (cb_val.length)))) then + if ((vAddr + size) > unsigned(getCapTop(cb_val))) then raise_c2_exception(CapEx_LengthViolation, cb) - else if (vAddr < ((nat) (cb_val.base))) then + else if (vAddr < unsigned(getCapBase(cb_val))) then raise_c2_exception(CapEx_LengthViolation, cb) else if not (isAddressAligned(vAddr64, width)) then SignalExceptionBadAddr(AdES, vAddr64) @@ -762,9 +893,9 @@ function clause execute (CSC(cs, cb, rt, rd, offset, conditional)) = 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 + if ((vAddr + cap_size) > unsigned(getCapTop(cb_val))) then raise_c2_exception(CapEx_LengthViolation, cb) - else if (vAddr < ((nat) (cb_val.base))) then + else if (vAddr < unsigned(getCapBase(cb_val))) then raise_c2_exception(CapEx_LengthViolation, cb) else if ((vAddr mod cap_size) != 0) then SignalExceptionBadAddr(AdES, vAddr64) @@ -811,9 +942,9 @@ function clause execute (CLC(cd, cb, rt, offset, linked)) = 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 + if ((vAddr + cap_size) > unsigned(getCapTop(cb_val))) then raise_c2_exception(CapEx_LengthViolation, cb) - else if (vAddr < ((nat) (cb_val.base))) then + else if (vAddr < unsigned(getCapBase(cb_val))) then raise_c2_exception(CapEx_LengthViolation, cb) else if ((vAddr mod cap_size) != 0) then SignalExceptionBadAddr(AdEL, vAddr64) diff --git a/cheri/cheri_insts_128.sail b/cheri/cheri_insts_128.sail deleted file mode 100644 index 1d2b37fb..00000000 --- a/cheri/cheri_insts_128.sail +++ /dev/null @@ -1,973 +0,0 @@ -(*========================================================================*) -(* *) -(* Copyright (c) 2015-2016 Robert M. Norton *) -(* Copyright (c) 2015-2016 Kathyrn Gray *) -(* All rights reserved. *) -(* *) -(* This software was developed by the University of Cambridge Computer *) -(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) -(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) -(* *) -(* Redistribution and use in source and binary forms, with or without *) -(* modification, are permitted provided that the following conditions *) -(* are met: *) -(* 1. Redistributions of source code must retain the above copyright *) -(* notice, this list of conditions and the following disclaimer. *) -(* 2. Redistributions in binary form must reproduce the above copyright *) -(* notice, this list of conditions and the following disclaimer in *) -(* the documentation and/or other materials provided with the *) -(* distribution. *) -(* *) -(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) -(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) -(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) -(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) -(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) -(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) -(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) -(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) -(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) -(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) -(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) -(* SUCH DAMAGE. *) -(*========================================================================*) - -(* Operations that extract parts of a capability into GPR *) - -union ast member (regno, regno) CGetPerm -union ast member (regno, regno) CGetType -union ast member (regno, regno) CGetBase -union ast member (regno, regno) CGetLen -union ast member (regno, regno) CGetTag -union ast member (regno, regno) CGetSealed -union ast member (regno, regno) CGetOffset - -function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : 0b00000000 : 0b000) = Some(CGetPerm(rd, cb)) -function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : 0b00000000 : 0b001) = Some(CGetType(rd, cb)) -function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : 0b00000000 : 0b010) = Some(CGetBase(rd, cb)) -function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : 0b00000000 : 0b011) = Some(CGetLen(rd, cb)) -(* NB CGetCause Handled separately *) -function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : 0b00000000 : 0b101) = Some(CGetTag(rd, cb)) -function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : 0b00000000 : 0b110) = Some(CGetSealed(rd, cb)) -function clause decode (0b010010 : 0b01101 : (regno) rd : (regno) cb : 0b00000000 : 0b010) = Some(CGetOffset(rd, cb)) (* NB encoding does not follow pattern *) - -function clause execute (CGetPerm(rd, cb)) = -{ - (* START_CGetPerms *) - checkCP2usable(); - if (register_inaccessible(cb)) then - raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) - else - let capVal = readCapReg(cb) in - wGPR(rd) := EXTZ(getCapPerms(capVal)); - (* END_CGetPerms *) -} - -function clause execute (CGetType(rd, cb)) = -{ - (* START_CGetType *) - checkCP2usable(); - if (register_inaccessible(cb)) then - raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) - else - let capVal = readCapReg(cb) in - wGPR(rd) := EXTZ(capVal.otype); - (* END_CGetType *) -} - -function clause execute (CGetBase(rd, cb)) = -{ - (* START_CGetBase *) - checkCP2usable(); - if (register_inaccessible(cb)) then - raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) - else - let capVal = readCapReg(cb) in - wGPR(rd) := getCapBase(capVal); - (* END_CGetBase *) -} - -function clause execute (CGetOffset(rd, cb)) = -{ - (* START_CGetOffset *) - checkCP2usable(); - if (register_inaccessible(cb)) then - raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) - else - let capVal = readCapReg(cb) in - wGPR(rd) := getCapOffset(capVal); - (* END_CGetOffset *) -} - -function clause execute (CGetLen(rd, cb)) = -{ - (* START_CGetLen *) - checkCP2usable(); - if (register_inaccessible(cb)) then - raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) - else - let capVal = readCapReg(cb) in - let len65 = getCapLength(capVal) in - let len64 = if unsigned(len65) > MAX_U64 then - (bit[64]) MAX_U64 else len65[63..0] in - wGPR(rd) := len64; - (* END_CGetLen *) -} - -function clause execute (CGetTag(rd, cb)) = -{ - (* START_CGetTag *) - checkCP2usable(); - if (register_inaccessible(cb)) then - raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) - else - let capVal = readCapReg(cb) in - wGPR(rd) := EXTZ(capVal.tag); - (* END_CGetTag *) -} - -function clause execute (CGetSealed(rd, cb)) = -{ - (* START_CGetSealed *) - checkCP2usable(); - if (register_inaccessible(cb)) then - raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) - else - let capVal = readCapReg(cb) in - wGPR(rd) := EXTZ(capVal.sealed); - (* END_CGetSealed *) -} - -union ast member regno CGetPCC -function clause decode (0b010010 : 0b00000 : (regno) cd : 0b00000 : 0b11111 : 0b111111) = Some(CGetPCC(cd)) -function clause execute (CGetPCC(cd)) = -{ - (* START_CGetPCC *) - checkCP2usable(); - if (register_inaccessible(cd)) then - raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) - else - let pcc = (capRegToCapStruct(PCC)) in - let (success, pcc2) = setCapOffset(pcc, PC) in - {assert (success, None); (* guaranteed to be in-bounds *) - writeCapReg(cd, pcc2)}; - (* END_CGetPCC *) -} - - -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)) = -{ - (* START_CGetPCCSetOffset *) - checkCP2usable(); - if (register_inaccessible(cd)) then - raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) - else - let pcc = (capRegToCapStruct(PCC)) in - let rs_val = rGPR(rs) in - let (success, newPCC) = setCapOffset(pcc, rs_val) in - if (success) then - writeCapReg(cd, newPCC) - else - writeCapReg(cd, int_to_cap(rs_val)); - (* END_CGetPCCSetOffset *) -} -(* 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)) = -{ - (* START_CGetCause *) - checkCP2usable(); - if not (pcc_access_system_regs ()) then - raise_c2_exception_noreg(CapEx_AccessSystemRegsViolation) - else - wGPR(rd) := EXTZ(CapCause) - (* END_CGetCause *) -} - -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)) = -{ - (* START_CSetCause *) - checkCP2usable(); - if not (pcc_access_system_regs ()) then - raise_c2_exception_noreg(CapEx_AccessSystemRegsViolation) - else - { - (bit[64]) rt_val := rGPR(rt); - CapCause.ExcCode := rt_val[15..8]; - CapCause.RegNum := rt_val[7..0]; - } - (* END_CSetCause *) -} - -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)) = -{ - (* START_CAndPerm *) - checkCP2usable(); - cb_val := readCapReg(cb); - rt_val := rGPR(rt); - if (register_inaccessible(cd)) then - raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) - else if (register_inaccessible(cb)) then - raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) - else if not (cb_val.tag) then - raise_c2_exception(CapEx_TagViolation, cb) - else if (cb_val.sealed) then - raise_c2_exception(CapEx_SealViolation, cb) - else - let perms = getCapPerms(cb_val) in - let newCap = setCapPerms(cb_val, (perms & rt_val[30..0])) in - writeCapReg(cd, newCap); - (* END_CAndPerm *) -} - - - -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)) = -{ - (* START_CToPtr *) - checkCP2usable(); - ct_val := readCapReg(ct); - cb_val := readCapReg(cb); - if (register_inaccessible(cb)) then - raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) - else if (register_inaccessible(ct)) then - raise_c2_exception(CapEx_AccessSystemRegsViolation, ct) - else if not (ct_val.tag) then - raise_c2_exception(CapEx_TagViolation, ct) - else - { - wGPR(rd) := if not (cb_val.tag) then - ((bit[64]) 0) - else - (bit[64])(getCapCursor(cb_val) - unsigned(getCapBase(ct_val))) - } - (* END_CToPtr *) -} - - - -union ast member regregreg CSub -function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : (regno) ct : 0b001010) = Some(CSub(rd, cb, ct)) -function clause execute(CSub(rd, cb, ct)) = -{ - (* START_CSub *) - checkCP2usable(); - ct_val := readCapReg(ct); - cb_val := readCapReg(cb); - if (register_inaccessible(cb)) then - raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) - else if (register_inaccessible(ct)) then - raise_c2_exception(CapEx_AccessSystemRegsViolation, ct) - else - { - wGPR(rd) := (bit[64])(getCapCursor(cb_val) - getCapCursor(ct_val)) - } - (* END_CSub *) -} - -union ast member (regno, regno, regno, CPtrCmpOp) CPtrCmp -function clause decode (0b010010 : 0b01110 : (regno) rd : (regno) cb : (regno) ct : 0b000 : 0b000) = Some(CPtrCmp(rd, cb, ct, CEQ)) -function clause decode (0b010010 : 0b01110 : (regno) rd : (regno) cb : (regno) ct : 0b000 : 0b001) = Some(CPtrCmp(rd, cb, ct, CNE)) -function clause decode (0b010010 : 0b01110 : (regno) rd : (regno) cb : (regno) ct : 0b000 : 0b010) = Some(CPtrCmp(rd, cb, ct, CLT)) -function clause decode (0b010010 : 0b01110 : (regno) rd : (regno) cb : (regno) ct : 0b000 : 0b011) = Some(CPtrCmp(rd, cb, ct, CLE)) -function clause decode (0b010010 : 0b01110 : (regno) rd : (regno) cb : (regno) ct : 0b000 : 0b100) = Some(CPtrCmp(rd, cb, ct, CLTU)) -function clause decode (0b010010 : 0b01110 : (regno) rd : (regno) cb : (regno) ct : 0b000 : 0b101) = Some(CPtrCmp(rd, cb, ct, CLEU)) -function clause decode (0b010010 : 0b01110 : (regno) rd : (regno) cb : (regno) ct : 0b000 : 0b110) = Some(CPtrCmp(rd, cb, ct, CEXEQ)) - -function clause execute(CPtrCmp(rd, cb, ct, op)) = -{ - (* START_CPtrCmp *) - checkCP2usable(); - if (register_inaccessible(cb)) then - raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) - else if (register_inaccessible(ct)) then - raise_c2_exception(CapEx_AccessSystemRegsViolation, ct) - else - { - cb_val := readCapReg(cb); - ct_val := readCapReg(ct); - equal := false; - ltu := false; - lts := false; - if (cb_val.tag != ct_val.tag) then - { - if not (cb_val.tag) then - { - ltu := true; - lts := true; - } - } - else - { - cursor1 := getCapCursor(cb_val); - cursor2 := getCapCursor(ct_val); - equal := (cursor1 == cursor2); - ltu := (cursor1 < cursor2); - lts := (((bit[64])cursor1) <_s ((bit[64])cursor2)); - }; - wGPR(rd) := EXTZ(switch (op) { - case CEQ -> [equal] - case CNE -> [not (equal)] - case CLT -> [lts] - case CLE -> [lts | equal] - case CLTU -> [ltu] - case CLEU -> [lts | equal] - case CEXEQ -> [cb_val == ct_val] - }) - } - (* END_CPtrCmp *) -} - -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)) = -{ - (* START_CIncOffset *) - checkCP2usable(); - cb_val := readCapReg(cb); - rt_val := rGPR(rt); - if (register_inaccessible(cd)) then - raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) - else if (register_inaccessible(cb)) then - raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) - else if ((cb_val.tag) & (cb_val.sealed) & (rt_val != 0x0000000000000000)) then - raise_c2_exception(CapEx_SealViolation, cb) - else - let (success, newCap) = incCapOffset(cb_val, rt_val) in - if (success) then - writeCapReg(cd, newCap) - else - writeCapReg(cd, int_to_cap(getCapBase(cb_val) + rt_val)) - (* END_CIncOffset *) -} - -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)) = -{ - (* START_CSetOffset *) - checkCP2usable(); - cb_val := readCapReg(cb); - rt_val := rGPR(rt); - if (register_inaccessible(cd)) then - raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) - else if (register_inaccessible(cb)) then - raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) - else if ((cb_val.tag) & (cb_val.sealed)) then - raise_c2_exception(CapEx_SealViolation, cb) - else - let (success, newCap) = setCapOffset(cb_val, rt_val) in - if (success) then - writeCapReg(cd, newCap) - else - writeCapReg(cd, int_to_cap(cb_val.address + rt_val)) - (* END_CSetOffset *) -} - -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)) = -{ - (* START_CSetBounds *) - checkCP2usable(); - cb_val := readCapReg(cb); - rt_val := unsigned(rGPR(rt)); - cursor := getCapCursor(cb_val); - base := unsigned(getCapBase(cb_val)); - top := unsigned(getCapTop(cb_val)); - newTop := cursor + rt_val; - if (register_inaccessible(cd)) then - raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) - else if (register_inaccessible(cb)) then - raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) - else if not (cb_val.tag) then - raise_c2_exception(CapEx_TagViolation, cb) - else if (cb_val.sealed) then - raise_c2_exception(CapEx_SealViolation, cb) - else if (cursor < base) then - raise_c2_exception(CapEx_LengthViolation, cb) - else if (newTop > top) then - raise_c2_exception(CapEx_LengthViolation, cb) - else - let (_, newCap) = setCapBounds(cb_val, (bit[64]) cursor, (bit[65]) newTop) in - writeCapReg(cd, newCap) (* ignore exact *) - (* END_CSetBounds *) -} - - -union ast member regregreg CSetBoundsExact -function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cb : (regno) rt : 0b001001) = Some(CSetBoundsExact(cd, cb, rt)) -function clause execute (CSetBoundsExact(cd, cb, rt)) = -{ - (* START_CSetBoundsExact *) - checkCP2usable(); - cb_val := readCapReg(cb); - rt_val := unsigned(rGPR(rt)); - cursor := getCapCursor(cb_val); - base := unsigned(getCapBase(cb_val)); - top := unsigned(getCapTop(cb_val)); - if (register_inaccessible(cd)) then - raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) - else if (register_inaccessible(cb)) then - raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) - else if not (cb_val.tag) then - raise_c2_exception(CapEx_TagViolation, cb) - else if (cb_val.sealed) then - raise_c2_exception(CapEx_SealViolation, cb) - else if (cursor < base) then - raise_c2_exception(CapEx_LengthViolation, cb) - else if ((cursor + rt_val) > top) then - raise_c2_exception(CapEx_LengthViolation, cb) - else - let (exact, newCap) = setCapBounds(cb_val, (bit[64]) base, (bit[65]) top) in - if not (exact) then - raise_c2_exception(CapEx_InexactBounds, cb) - else - writeCapReg(cd, newCap) - (* END_CSetBoundsExact *) -} - -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)) = -{ - (* START_CClearTag *) - checkCP2usable(); - if (register_inaccessible(cd)) then - raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) - else if (register_inaccessible(cb)) then - raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) - else - { - cb_val := readCapReg(cb); - writeCapReg(cd, {cb_val with tag = false}); - } - (* END_CClearTag *) -} - -union ast member (ClearRegSet, bit[16]) ClearRegs -function clause decode (0b010010 : 0b01111 : 0b00000 : (bit[16]) imm) = Some(ClearRegs(GPLo, imm)) (* ClearLo *) -function clause decode (0b010010 : 0b01111 : 0b00001 : (bit[16]) imm) = Some(ClearRegs(GPHi, imm)) (* ClearHi *) -function clause decode (0b010010 : 0b01111 : 0b00010 : (bit[16]) imm) = Some(ClearRegs(CLo, imm)) (* CClearLo *) -function clause decode (0b010010 : 0b01111 : 0b00011 : (bit[16]) imm) = Some(ClearRegs(CHi, imm)) (* CClearHi *) -function clause execute (ClearRegs(regset, mask)) = -{ - (* START_ClearRegs *) - if ((regset == CLo) | (regset == CHi)) then - checkCP2usable(); - if (regset == CHi) then - foreach (i from 0 to 15) - let r = ((bit[5]) (i+16)) in - if (mask[i] & register_inaccessible(r)) then - raise_c2_exception(CapEx_AccessSystemRegsViolation, r); - foreach (i from 0 to 15) - if (mask[i]) then - switch (regset) { - case GPLo -> wGPR((bit[5])i) := 0 - case GPHi -> wGPR((bit[5])(i+16)) := 0 - case CLo -> writeCapReg((bit[5]) i) := null_cap - case CHi -> writeCapReg((bit[5]) (i+16)) := null_cap - } - (* END_ClearRegs *) -} - -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)) = -{ - (* START_CFromPtr *) - checkCP2usable(); - cb_val := readCapReg(cb); - rt_val := rGPR(rt); - if (register_inaccessible(cd)) then - raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) - else if (register_inaccessible(cb)) then - raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) - else if (rt == 0) then - writeCapReg(cd, null_cap) - else if not (cb_val.tag) then - raise_c2_exception(CapEx_TagViolation, cb) - else if (cb_val.sealed) then - raise_c2_exception(CapEx_SealViolation, cb) - else - let (success, newCap) = setCapOffset(cb_val, rt_val) in - if (success) then - writeCapReg(cd, newCap) - else - writeCapReg(cd, int_to_cap(getCapBase(cb_val) + rt_val)) - (* END_CFromPtr *) -} - -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)) = -{ - (* START_CCheckPerm *) - checkCP2usable(); - cs_val := readCapReg(cs); - cs_perms := EXTZ(getCapPerms(cs_val)); - rt_perms := rGPR(rt); - if (register_inaccessible(cs)) then - raise_c2_exception(CapEx_AccessSystemRegsViolation, cs) - else if not (cs_val.tag) then - raise_c2_exception(CapEx_TagViolation, cs) - else if ((cs_perms & rt_perms) != rt_perms) then - raise_c2_exception(CapEx_UserDefViolation, cs) - else - () - (* END_CCheckPerm *) -} - -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)) = -{ - (* START_CCheckType *) - checkCP2usable(); - cs_val := readCapReg(cs); - cb_val := readCapReg(cb); - if (register_inaccessible(cs)) then - raise_c2_exception(CapEx_AccessSystemRegsViolation, cs) - else if (register_inaccessible(cb)) then - raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) - else if not (cs_val.tag) then - raise_c2_exception(CapEx_TagViolation, cs) - else if not (cb_val.tag) then - raise_c2_exception(CapEx_TagViolation, cb) - else if not (cs_val.sealed) then - raise_c2_exception(CapEx_SealViolation, cs) - else if not (cb_val.sealed) then - raise_c2_exception(CapEx_SealViolation, cb) - else if ((cs_val.otype) != (cb_val.otype)) then - raise_c2_exception(CapEx_TypeViolation, cs) - else - () - (* END_CCheckType *) -} - -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)) = -{ - (* START_CSeal *) - checkCP2usable(); - cs_val := readCapReg(cs); - ct_val := readCapReg(ct); - ct_cursor := getCapCursor(ct_val); - ct_top := unsigned(getCapTop(ct_val)); - if (register_inaccessible(cd)) then - raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) - else if (register_inaccessible(cs)) then - raise_c2_exception(CapEx_AccessSystemRegsViolation, cs) - else if (register_inaccessible(ct)) then - raise_c2_exception(CapEx_AccessSystemRegsViolation, ct) - else if not (cs_val.tag) then - raise_c2_exception(CapEx_TagViolation, cs) - else if not (ct_val.tag) then - raise_c2_exception(CapEx_TagViolation, ct) - else if (cs_val.sealed) then - raise_c2_exception(CapEx_SealViolation, cs) - else if (ct_val.sealed) then - raise_c2_exception(CapEx_SealViolation, ct) - else if not (ct_val.permit_seal) then - raise_c2_exception(CapEx_PermitSealViolation, ct) - else if (ct_cursor >= ct_top) then - raise_c2_exception(CapEx_LengthViolation, ct) - else if (ct_cursor > max_otype) then - raise_c2_exception(CapEx_LengthViolation, ct) - else - let (success, newCap) = sealCap(cs_val, (bit[24]) ct_cursor) in - if not (success) then - raise_c2_exception(CapEx_InexactBounds, cs) - else - writeCapReg(cd, newCap) - (* END_CSeal *) -} - -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)) = -{ - (* START_CUnseal *) - checkCP2usable(); - cs_val := readCapReg(cs); - ct_val := readCapReg(ct); - ct_cursor := getCapCursor(ct_val); - if (register_inaccessible(cd)) then - raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) - else if (register_inaccessible(cs)) then - raise_c2_exception(CapEx_AccessSystemRegsViolation, cs) - else if (register_inaccessible(ct)) then - raise_c2_exception(CapEx_AccessSystemRegsViolation, ct) - else if not (cs_val.tag) then - raise_c2_exception(CapEx_TagViolation, cs) - else if not (ct_val.tag) then - raise_c2_exception(CapEx_TagViolation, ct) - else if not (cs_val.sealed) then - raise_c2_exception(CapEx_SealViolation, cs) - else if (ct_val.sealed) then - raise_c2_exception(CapEx_SealViolation, ct) - else if (ct_cursor != unsigned(cs_val.otype)) then - raise_c2_exception(CapEx_TypeViolation, ct) - else if not (ct_val.permit_seal) then - raise_c2_exception(CapEx_PermitSealViolation, ct) - else if (ct_cursor >= unsigned(getCapTop(ct_val))) then - raise_c2_exception(CapEx_LengthViolation, ct) - else - writeCapReg(cd, {cs_val with - sealed=false; - otype=0; - global=(cs_val.global & ct_val.global) - }) - (* END_CUnseal *) -} - -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)) = -{ - (* Partial implementation of CCall with checks in hardware, but raising a trap to perform trusted stack manipulation *) - (* START_CCall *) - checkCP2usable(); - cs_val := readCapReg(cs); - cb_val := readCapReg(cb); - if (register_inaccessible(cs)) then - raise_c2_exception(CapEx_AccessSystemRegsViolation, cs) - else if (register_inaccessible(cb)) then - raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) - else if not (cs_val.tag) then - raise_c2_exception(CapEx_TagViolation, cs) - else if not (cb_val.tag) then - raise_c2_exception(CapEx_TagViolation, cb) - else if not (cs_val.sealed) then - raise_c2_exception(CapEx_SealViolation, cs) - else if not (cb_val.sealed) then - raise_c2_exception(CapEx_SealViolation, cb) - else if ((cs_val.otype) != (cb_val.otype)) then - raise_c2_exception(CapEx_TypeViolation, cs) - else if not (cs_val.permit_execute) then - raise_c2_exception(CapEx_PermitExecuteViolation, cs) - else if (cb_val.permit_execute) then - raise_c2_exception(CapEx_PermitExecuteViolation, cb) - else if (getCapCursor(cs_val) >= unsigned(getCapTop(cs_val))) then - raise_c2_exception(CapEx_LengthViolation, cs) - else - raise_c2_exception(CapEx_CallTrap, cs); - (* END_CCall *) -} - -union ast member unit CReturn -function clause decode (0b010010 : 0b00110 : 0b000000000000000000000) = Some(CReturn) -function clause execute (CReturn) = -{ - (* START_CReturn *) - checkCP2usable(); - raise_c2_exception_noreg(CapEx_ReturnTrap) - (* END_CReturn *) -} - -union ast member (regno, bit[16], bool) CBX -function clause decode (0b010010 : 0b01001 : (regno) cb : (bit[16]) imm) = Some(CBX(cb, imm, true)) (* CBTU *) -function clause decode (0b010010 : 0b01010 : (regno) cb : (bit[16]) imm) = Some(CBX(cb, imm, false)) (* CBTS *) - -function clause execute (CBX(cb, imm, invert)) = -{ - (* START_CBx *) - checkCP2usable(); - if (register_inaccessible(cb)) then - raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) - else if (((readCapReg(cb)).tag) ^ invert) then - { - let (bit[64]) offset = (EXTS(imm : 0b00) + 4) in - delayedPC := PC + offset; - branchPending := 1; - } - (* END_CBx *) -} - -union ast member (regno, regno, bool) CJALR -function clause decode (0b010010 : 0b00111 : (regno) cd : (regno) cb : 0b00000 : 0b000000) = Some(CJALR(cd, cb, true)) (* CJALR *) -function clause decode (0b010010 : 0b01000 : 0b00000 : (regno) cb : 0b00000 : 0b000000) = Some(CJALR(0b00000, cb, false)) (* CJR *) -function clause execute(CJALR(cd, cb, link)) = -{ - (* START_CJALR *) - checkCP2usable(); - cb_val := readCapReg(cb); - cb_ptr := getCapCursor(cb_val); - cb_top := unsigned(getCapTop(cb_val)); - if (link & register_inaccessible(cd)) then - raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) - else if (register_inaccessible(cb)) then - raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) - else if not (cb_val.tag) then - raise_c2_exception(CapEx_TagViolation, cb) - else if (cb_val.sealed) then - raise_c2_exception(CapEx_SealViolation, cb) - else if not (cb_val.permit_execute) then - raise_c2_exception(CapEx_PermitExecuteViolation, cb) - else if not (cb_val.global) then - raise_c2_exception(CapEx_GlobalViolation, cb) - else if (cb_ptr + 4 > cb_top) then - raise_c2_exception(CapEx_LengthViolation, cb) - else if ((cb_ptr mod 4) != 0) then - SignalException(AdEL) - else - { - if (link) then - let pcc = capRegToCapStruct(PCC) in - let (success, linkCap) = setCapOffset(pcc, PC+8) in - if (success) then - writeCapReg(cd, linkCap) - else - assert(false, None); - delayedPC := getCapOffset(cb_val); - delayedPCC := capStructToCapReg(cb_val); - branchPending := 1; - } - (* END_CJALR *) -} - -union ast member (regno, regno, regno, bit[8], bool, WordType, bool) CLoad -function clause decode (0b110010 : (regno) rd : (regno) cb: (regno) rt : (bit[8]) offset : 0b0 : 0b00) = Some(CLoad(rd, cb, rt, offset, false, B, false)) (* CLBU *) -function clause decode (0b110010 : (regno) rd : (regno) cb: (regno) rt : (bit[8]) offset : 0b1 : 0b00) = Some(CLoad(rd, cb, rt, offset, true, B, false)) (* CLB *) -function clause decode (0b110010 : (regno) rd : (regno) cb: (regno) rt : (bit[8]) offset : 0b0 : 0b01) = Some(CLoad(rd, cb, rt, offset, false, H, false)) (* CLHU *) -function clause decode (0b110010 : (regno) rd : (regno) cb: (regno) rt : (bit[8]) offset : 0b1 : 0b01) = Some(CLoad(rd, cb, rt, offset, true, H, false)) (* CLH *) -function clause decode (0b110010 : (regno) rd : (regno) cb: (regno) rt : (bit[8]) offset : 0b0 : 0b10) = Some(CLoad(rd, cb, rt, offset, false, W, false)) (* CLWU *) -function clause decode (0b110010 : (regno) rd : (regno) cb: (regno) rt : (bit[8]) offset : 0b1 : 0b10) = Some(CLoad(rd, cb, rt, offset, true, W, false)) (* CLW *) -function clause decode (0b110010 : (regno) rd : (regno) cb: (regno) rt : (bit[8]) offset : 0b0 : 0b11) = Some(CLoad(rd, cb, rt, offset, false, D, false)) (* CLD *) - -function clause decode (0b010010 : 0b10000 : (regno) rd : (regno) cb : 0b00000001 : 0b0 : 0b00) = Some(CLoad(rd, cb, 0b00000, 0b00000000, false, B, true)) (* CLLBU *) -function clause decode (0b010010 : 0b10000 : (regno) rd : (regno) cb : 0b00000001 : 0b1 : 0b00) = Some(CLoad(rd, cb, 0b00000, 0b00000000, true, B, true)) (* CLLB *) -function clause decode (0b010010 : 0b10000 : (regno) rd : (regno) cb : 0b00000001 : 0b0 : 0b01) = Some(CLoad(rd, cb, 0b00000, 0b00000000, false, H, true)) (* CLLHU *) -function clause decode (0b010010 : 0b10000 : (regno) rd : (regno) cb : 0b00000001 : 0b1 : 0b01) = Some(CLoad(rd, cb, 0b00000, 0b00000000, true, H, true)) (* CLLH *) -function clause decode (0b010010 : 0b10000 : (regno) rd : (regno) cb : 0b00000001 : 0b0 : 0b10) = Some(CLoad(rd, cb, 0b00000, 0b00000000, false, W, true)) (* CLLWU *) -function clause decode (0b010010 : 0b10000 : (regno) rd : (regno) cb : 0b00000001 : 0b1 : 0b10) = Some(CLoad(rd, cb, 0b00000, 0b00000000, true, W, true)) (* CLLW *) -function clause decode (0b010010 : 0b10000 : (regno) rd : (regno) cb : 0b00000001 : 0b0 : 0b11) = Some(CLoad(rd, cb, 0b00000, 0b00000000, false, D, true)) (* CLLD *) - -function clause execute (CLoad(rd, cb, rt, offset, signext, width, linked)) = -{ - (* START_CLoad *) - checkCP2usable(); - cb_val := readCapReg(cb); - if (register_inaccessible(cb)) then - raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) - else if not (cb_val.tag) then - raise_c2_exception(CapEx_TagViolation, cb) - else if (cb_val.sealed) then - raise_c2_exception(CapEx_SealViolation, cb) - else if not (cb_val.permit_load) then - raise_c2_exception(CapEx_PermitLoadViolation, cb) - else - { - size := wordWidthBytes(width); - cursor := getCapCursor(cb_val); - vAddr := cursor + unsigned(rGPR(rt)) + (size*signed(offset)); - vAddr64:= (bit[64]) vAddr; - if ((vAddr + size) > unsigned(getCapTop(cb_val))) then - raise_c2_exception(CapEx_LengthViolation, cb) - else if (vAddr < unsigned(getCapBase(cb_val))) then - raise_c2_exception(CapEx_LengthViolation, cb) - else if not (isAddressAligned(vAddr64, width)) then - SignalExceptionBadAddr(AdEL, vAddr64) - else - { - pAddr := (TLBTranslate(vAddr64, LoadData)); - widthBytes := wordWidthBytes(width); - memResult := if (linked) then - { - CP0LLBit := 0b1; - CP0LLAddr := pAddr; - MEMr_reserve(pAddr, widthBytes); - } - else - MEMr(pAddr, widthBytes); - if (signext) then - wGPR(rd) := EXTS(memResult) - else - wGPR(rd) := EXTZ(memResult) - } - } - (* END_CLoad *) -} - -union ast member (regno, regno, regno, regno, bit[8], WordType, bool) CStore -function clause decode (0b111010 : (regno) rs : (regno) cb: (regno) rt : (bit[8]) offset : 0b0 : 0b00) = Some(CStore(rs, cb, rt, 0b00000, offset, B, false)) (* CSB *) -function clause decode (0b111010 : (regno) rs : (regno) cb: (regno) rt : (bit[8]) offset : 0b0 : 0b01) = Some(CStore(rs, cb, rt, 0b00000, offset, H, false)) (* CSH *) -function clause decode (0b111010 : (regno) rs : (regno) cb: (regno) rt : (bit[8]) offset : 0b0 : 0b10) = Some(CStore(rs, cb, rt, 0b00000, offset, W, false)) (* CSW *) -function clause decode (0b111010 : (regno) rs : (regno) cb: (regno) rt : (bit[8]) offset : 0b0 : 0b11) = Some(CStore(rs, cb, rt, 0b00000, offset, D, false)) (* CSD *) - -function clause decode (0b010010 : 0b10000 : (regno) rs : (regno) cb : (regno) rd : 0b0000 : 0b00) = Some(CStore(rs, cb, 0b00000, rd, 0b00000000, B, true)) (* CSCB *) -function clause decode (0b010010 : 0b10000 : (regno) rs : (regno) cb : (regno) rd : 0b0000 : 0b01) = Some(CStore(rs, cb, 0b00000, rd, 0b00000000, H, true)) (* CSCH *) -function clause decode (0b010010 : 0b10000 : (regno) rs : (regno) cb : (regno) rd : 0b0000 : 0b10) = Some(CStore(rs, cb, 0b00000, rd, 0b00000000, W, true)) (* CSCW *) -function clause decode (0b010010 : 0b10000 : (regno) rs : (regno) cb : (regno) rd : 0b0000 : 0b11) = Some(CStore(rs, cb, 0b00000, rd, 0b00000000, D, true)) (* CSCD *) - -function clause execute (CStore(rs, cb, rt, rd, offset, width, conditional)) = -{ - (* START_CStore *) - checkCP2usable(); - cb_val := readCapReg(cb); - if (register_inaccessible(cb)) then - raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) - else if not (cb_val.tag) then - raise_c2_exception(CapEx_TagViolation, cb) - else if (cb_val.sealed) then - raise_c2_exception(CapEx_SealViolation, cb) - else if not (cb_val.permit_store) then - raise_c2_exception(CapEx_PermitStoreViolation, cb) - else - { - size := wordWidthBytes(width); - cursor := getCapCursor(cb_val); - vAddr := cursor + unsigned(rGPR(rt)) + (size * signed(offset)); - vAddr64:= (bit[64]) vAddr; - if ((vAddr + size) > unsigned(getCapTop(cb_val))) then - raise_c2_exception(CapEx_LengthViolation, cb) - else if (vAddr < unsigned(getCapBase(cb_val))) then - raise_c2_exception(CapEx_LengthViolation, cb) - else if not (isAddressAligned(vAddr64, width)) then - SignalExceptionBadAddr(AdES, vAddr64) - else - { - pAddr := (TLBTranslate(vAddr64, StoreData)); - rs_val := rGPR(rs); - if (conditional) then - { - success := if (CP0LLBit[0]) then - switch(width) - { - case B -> MEMw_conditional_wrapper(pAddr, 1, rs_val[7..0]) - case H -> MEMw_conditional_wrapper(pAddr, 2, rs_val[15..0]) - case W -> MEMw_conditional_wrapper(pAddr, 4, rs_val[31..0]) - case D -> MEMw_conditional_wrapper(pAddr, 8, rs_val) - } - else - false; - wGPR(rd) := EXTZ([success]); - } - else - switch(width) - { - case B -> MEMw_wrapper(pAddr, 1) := rs_val[7..0] - case H -> MEMw_wrapper(pAddr, 2) := rs_val[15..0] - case W -> MEMw_wrapper(pAddr, 4) := rs_val[31..0] - case D -> MEMw_wrapper(pAddr, 8) := rs_val - } - } - } - (* END_CStore *) -} - -union ast member (regno, regno, regno, regno, bit[11], bool) CSC -function clause decode (0b111110 : (regno) cs : (regno) cb: (regno) rt : (bit[11]) offset) = Some(CSC(cs, cb, rt, 0b00000, offset, false)) -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)) = -{ - (* START_CSC *) - checkCP2usable(); - cs_val := readCapReg(cs); - cb_val := readCapReg(cb); - if (register_inaccessible(cs)) then - raise_c2_exception(CapEx_AccessSystemRegsViolation, cs) - else if (register_inaccessible(cb)) then - raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) - else if not (cb_val.tag) then - raise_c2_exception(CapEx_TagViolation, cb) - else if (cb_val.sealed) then - raise_c2_exception(CapEx_SealViolation, cb) - else if not (cb_val.permit_store_cap) then - raise_c2_exception(CapEx_PermitStoreCapViolation, cb) - else if not (cb_val.permit_store_local_cap) & (cs_val.tag) & not (cs_val.global) then - 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) > unsigned(getCapTop(cb_val))) then - raise_c2_exception(CapEx_LengthViolation, cb) - else if (vAddr < unsigned(getCapBase(cb_val))) then - raise_c2_exception(CapEx_LengthViolation, cb) - else if ((vAddr mod cap_size) != 0) then - SignalExceptionBadAddr(AdES, vAddr64) - else - { - let (pAddr, noStoreCap) = (TLBTranslateC(vAddr64, StoreData)) in - if (cs_val.tag & noStoreCap) then - raise_c2_exception(CapEx_TLBNoStoreCap, cs) - else if (conditional) then - { - success := if (CP0LLBit[0]) then - MEMw_tagged_conditional(pAddr, cs_val.tag, capStructToMemBits(cs_val)) - else - false; - wGPR(rd) := EXTZ([success]); - } - else - MEMw_tagged(pAddr, cs_val.tag, capStructToMemBits(cs_val)); - } - } - (* END_CSC *) -} - -union ast member (regno, regno, regno, bit[11], bool) CLC -function clause decode (0b110110 : (regno) cd : (regno) cb: (regno) rt : (bit[11]) offset) = Some(CLC(cd, cb, rt, offset, false)) -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)) = -{ - (* START_CLC *) - checkCP2usable(); - cb_val := readCapReg(cb); - if (register_inaccessible(cd)) then - raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) - else if (register_inaccessible(cb)) then - raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) - else if not (cb_val.tag) then - raise_c2_exception(CapEx_TagViolation, cb) - else if (cb_val.sealed) then - raise_c2_exception(CapEx_SealViolation, cb) - else if not (cb_val.permit_load_cap) then - 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) > unsigned(getCapTop(cb_val))) then - raise_c2_exception(CapEx_LengthViolation, cb) - else if (vAddr < unsigned(getCapBase(cb_val))) then - raise_c2_exception(CapEx_LengthViolation, cb) - else if ((vAddr mod cap_size) != 0) then - SignalExceptionBadAddr(AdEL, vAddr64) - else - { - let (pAddr, suppressTag) = (TLBTranslateC(vAddr64, LoadData)) in - let (tag, mem) = (if (linked) - then - { - CP0LLBit := 0b1; - CP0LLAddr := pAddr; - MEMr_tagged_reserve(pAddr); - } - else - (MEMr_tagged(pAddr))) - in - (CapRegs[cd]) := memBitsToCapBits(tag & not (suppressTag), mem); - } - } - (* END_CLC *) -} - -union ast member (regno) C2Dump -function clause decode (0b010010 : 0b00100 : (regno) rt : 0x0006) = Some(C2Dump(rt)) -function clause execute (C2Dump (rt)) = - () (* Currently a NOP *) diff --git a/cheri/cheri_prelude_128.sail b/cheri/cheri_prelude_128.sail index 323682b7..a96949a5 100644 --- a/cheri/cheri_prelude_128.sail +++ b/cheri/cheri_prelude_128.sail @@ -32,54 +32,9 @@ (* SUCH DAMAGE. *) (*========================================================================*) -(* 265-bit capability is really 257 bits including tag *) +(* 128 bit cap + tag *) typedef CapReg = bit[129] -register CapReg PCC -register CapReg nextPCC -register CapReg delayedPCC -register CapReg C00 (* aka default data capability, DDC *) -register CapReg C01 -register CapReg C02 -register CapReg C03 -register CapReg C04 -register CapReg C05 -register CapReg C06 -register CapReg C07 -register CapReg C08 -register CapReg C09 -register CapReg C10 -register CapReg C11 -register CapReg C12 -register CapReg C13 -register CapReg C14 -register CapReg C15 -register CapReg C16 -register CapReg C17 -register CapReg C18 -register CapReg C19 -register CapReg C20 -register CapReg C21 -register CapReg C22 -register CapReg C23 -register CapReg C24 (* aka return code capability, RCC *) -register CapReg C25 -register CapReg C26 (* aka invoked data capability, IDC *) -register CapReg C27 (* aka kernel reserved capability 1, KR1C *) -register CapReg C28 (* aka kernel reserved capability 2, KR2C *) -register CapReg C29 (* aka kernel code capability, KCC *) -register CapReg C30 (* aka kernel data capability, KDC *) -register CapReg C31 (* aka exception program counter capability, EPCC *) - -let (vector <0, 32, inc, (register<CapReg>)>) 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 - ] - -let num_uperms = 4 - - typedef CapStruct = const struct { bool tag; bit[4] uperms; @@ -129,7 +84,6 @@ let (CapStruct) null_cap = { let (nat) max_otype = 0xffffff def Nat cap_size_t = 16 (* cap size in bytes *) let ([:cap_size_t:]) cap_size = 16 -let have_cp2 = true function CapStruct capRegToCapStruct((CapReg) c) = let (bool) s = c[104] in @@ -159,10 +113,6 @@ function CapStruct capRegToCapStruct((CapReg) c) = address = c[63..0]; } - -function (CapStruct) readCapReg((regno) n) = - capRegToCapStruct(CapRegs[n]) - function (bit[11]) getCapHardPerms((CapStruct) cap) = ([cap.access_system_regs] : [cap.perm_reserved9] @@ -176,6 +126,26 @@ function (bit[11]) getCapHardPerms((CapStruct) cap) = : [cap.permit_execute] : [cap.global]) +function (bit[128]) capStructToMemBits((CapStruct) cap) = + let (bit[20]) b = if cap.sealed then (cap.B)[23..12] : (cap.otype)[23..12] else cap.B in + let (bit[20]) t = if cap.sealed then (cap.T)[23..12] : (cap.otype)[11..0] else cap.T in + ( cap.uperms + : getCapHardPerms(cap) + : cap.reserved + : cap.E + : [cap.sealed] + : b + : t + : cap.address + ) + +function (CapReg) capStructToCapReg((CapStruct) cap) = + ([cap.tag] : capStructToMemBits(cap)) + +(* Reverse of above used when reading from memory *) +function (CapReg) memBitsToCapBits((bool) tag, (bit[128]) b) = + ([tag] : b) + function (bit[31]) getCapPerms((CapStruct) cap) = let (bit[15]) perms = EXTS(getCapHardPerms(cap)) in (* NB access_system copied into 14-11 *) (0x000 (* uperms 30-19 *) @@ -205,34 +175,6 @@ function (bool, CapStruct) sealCap((CapStruct) cap, (bit[24]) otype) = else (false, undefined) -function (bit[128]) capStructToMemBits((CapStruct) cap) = - let (bit[20]) b = if cap.sealed then (cap.B)[23..12] : (cap.otype)[23..12] else cap.B in - let (bit[20]) t = if cap.sealed then (cap.T)[23..12] : (cap.otype)[11..0] else cap.T in - ( cap.uperms - : getCapHardPerms(cap) - : cap.reserved - : cap.E - : [cap.sealed] - : b - : t - : cap.address - ) - -function (CapReg) capStructToCapReg((CapStruct) cap) = - ([cap.tag] : capStructToMemBits(cap)) - -(* Reverse of above used when reading from memory *) -function (CapReg) memBitsToCapBits((bool) tag, (bit[128]) b) = - ([tag] - : b - ) - -function unit writeCapReg((regno) n, (CapStruct) cap) = - { - CapRegs[n] := capStructToCapReg(cap) - } - - function int a_top_correction((bit[20]) a_mid, (bit[20]) R, (bit[20]) bound) = switch (a_mid < R, bound < R) { case (False, False) -> 0 @@ -330,240 +272,3 @@ function (bool, CapStruct) setCapBounds((CapStruct) cap, (bit[64]) base, (bit[65 function CapStruct int_to_cap ((bit[64]) offset) = {null_cap with address = offset} - -typedef CapEx = enumerate { - CapEx_None; - CapEx_LengthViolation; - 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_AccessSystemRegsViolation; -} - -typedef CPtrCmpOp = enumerate { - CEQ; - CNE; - CLT; - CLE; - CLTU; - CLEU; - CEXEQ; -} - -typedef ClearRegSet = enumerate { -GPLo; -GPHi; -CLo; -CHi; -} - -function (bit[8]) CapExCode((CapEx) ex) = - switch(ex) { - case CapEx_None -> 0x00 - case CapEx_LengthViolation -> 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_AccessSystemRegsViolation -> 0x18 - } - -typedef CapCauseReg = register bits [15:0] { - 15..8: ExcCode; - 7..0: RegNum; -} - -register CapCauseReg CapCause - -function forall Type 'o . 'o SignalException ((Exception) ex) = - { - C31 := PCC; - (*C31.offset := PC; XXX fix this *) - nextPCC := C29; (* KCC *) - delayedPCC := C29; (* always write delayedPCC together whether PCC so - that non-capability branches don't override PCC *) - SignalExceptionMIPS(ex, getCapBase(capRegToCapStruct(C29))); - } - -function unit ERETHook() = - { - nextPCC := C31; - delayedPCC := C31; (* always write delayedPCC together whether PCC so - that non-capability branches don't override PCC *) - } - -function forall Type 'o . 'o raise_c2_exception8((CapEx) capEx, (bit[8]) regnum) = - { - (CapCause.ExcCode) := CapExCode(capEx); - (CapCause.RegNum) := regnum; - let mipsEx = - if ((capEx == CapEx_CallTrap) | (capEx == CapEx_ReturnTrap)) - then C2Trap else C2E in - SignalException(mipsEx); - } - -function forall Type 'o . 'o raise_c2_exception((CapEx) capEx, (regno) regnum) = - raise_c2_exception8(capEx, 0b000 : regnum) - -function forall Type 'o . 'o raise_c2_exception_noreg((CapEx) capEx) = - raise_c2_exception8(capEx, 0xff) - -function bool pcc_access_system_regs () = - let pcc = capRegToCapStruct(PCC) in - (pcc.access_system_regs) - -function bool register_inaccessible((regno) r) = - let is_sys_reg = switch(r) { - case 0b11011 -> true - case 0b11100 -> true - case 0b11101 -> true - case 0b11110 -> true - case 0b11111 -> true - case _ -> false - } in - if is_sys_reg then - not (pcc_access_system_regs ()) - else - false - -val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * ('n + 1)]) effect { rmem } MEMr_tag -val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * ('n + 1)]) effect { rmem } MEMr_tag_reserve - -val extern (bit[64] , bit[8]) -> unit effect { wmem } TAGw -val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_tag -val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_tag_conditional -val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8 * ('n + 1)]) -> unit effect { wmv } MEMval_tag -val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8 * ('n + 1)]) -> bool effect { wmv } MEMval_tag_conditional - - -function (bool, bit[cap_size_t * 8]) MEMr_tagged ((bit[64]) addr) = -{ - (* assumes addr is cap. aligned *) - let ((bit[8]) tag : mem) = (MEMr_tag (addr, cap_size)) in - (tag[0], mem) -} - -function (bool, bit[cap_size_t * 8]) MEMr_tagged_reserve ((bit[64]) addr) = -{ - (* assumes addr is cap. aligned *) - let ((bit[8]) tag : mem) = (MEMr_tag_reserve (addr, cap_size)) in - (tag[0], mem) -} - -function unit MEMw_tagged((bit[64]) addr, (bool) tag, (bit[cap_size_t * 8]) data) = -{ - (* assumes addr is cap. aligned *) - MEMea_tag(addr, cap_size); - MEMval_tag(addr, cap_size, 0b0000000 : [tag] : data); -} - -function bool MEMw_tagged_conditional((bit[64]) addr, (bool) tag, (bit[cap_size_t * 8]) data) = -{ - (* assumes addr is cap. aligned *) - MEMea_tag_conditional(addr, cap_size); - MEMval_tag_conditional(addr, cap_size, 0b0000000 : [tag] : data); -} - -function unit effect {wmem} MEMw_wrapper(addr, size, data) = - if (addr == 0x000000007f000000) then - { - UART_WDATA := data[31..24]; - UART_WRITTEN := 1; - } - else - { - (* On cheri non-capability writes must clear the corresponding tag - XXX this is vestigal and only works on sequential modle -- tag clearing - should probably be done in memory model. *) - TAGw((addr[63..4] : 0b0000), 0x00); - MEMea(addr,size); - MEMval(addr, size, data); - } - -function bool effect {wmem} MEMw_conditional_wrapper(addr, size, data) = - { - (* On cheri non-capability writes must clear the corresponding tag*) - MEMea_conditional(addr, size); - success := MEMval_conditional(addr,size,data); - if (success) then - (* XXX as above TAGw is vestigal and must die *) - TAGw((addr[63..4] : 0b0000), 0x00); - success; - } - -function bit[64] addrWrapper((bit[64]) addr, (MemAccessType) accessType, (WordType) width) = - { - capno := 0b00000; - cap := readCapReg(capno); - if (~(cap.tag)) then - (raise_c2_exception(CapEx_TagViolation, capno)) - else if (cap.sealed) then - (raise_c2_exception(CapEx_SealViolation, capno)); - switch (accessType) { - 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); - size := wordWidthBytes(width); - base := unsigned(getCapBase(cap)); - top := unsigned(getCapTop(cap)); - if ((vAddr + size) > top) then - (raise_c2_exception(CapEx_LengthViolation, capno)) - else if (vAddr < (base)) then - (raise_c2_exception(CapEx_LengthViolation, capno)) - else - (bit[64]) vAddr; (* XXX vAddr not truncated because top <= 2^64 and size > 0 *) - } - -function (bit[64]) TranslateAddress ((bit[64]) vAddr, (MemAccessType) accessType) = { - incrementCP0Count(); - let pcc = capRegToCapStruct(PCC) in - let base = unsigned(getCapBase(pcc)) in - let top = unsigned(getCapTop(pcc)) in - let absPC = (unsigned(vAddr)) in - if ((absPC mod 4) != 0) then (* bad PC alignment *) - (SignalExceptionBadAddr(AdEL, (bit[64]) absPC)) (* XXX absPC may be truncated *) - else if ((absPC + 4) > top) then - (raise_c2_exception_noreg(CapEx_LengthViolation)) - else - TLBTranslate((bit[64]) absPC, accessType) (* XXX assert absPC never gets truncated due to above check and top <= 2^64 for valid caps *) -} - -function unit checkCP2usable () = - { - if (~((CP0Status.CU)[2])) then - { - (CP0Cause.CE) := 0b10; - (SignalException(CpU)); - } - } - diff --git a/cheri/cheri_prelude_256.sail b/cheri/cheri_prelude_256.sail new file mode 100644 index 00000000..8cb162f8 --- /dev/null +++ b/cheri/cheri_prelude_256.sail @@ -0,0 +1,207 @@ +(*========================================================================*) +(* *) +(* Copyright (c) 2015-2016 Robert M. Norton *) +(* Copyright (c) 2015-2016 Kathyrn Gray *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(*========================================================================*) + +(* 256 bit cap + tag *) +typedef CapReg = bit[257] + +typedef CapStruct = const struct { + bool tag; + bit[8] padding; + bit[24] otype; + bit[16] uperms; + bit[4] perm_reserved11_14; + bool access_system_regs; + bool perm_reserved9; + bool perm_reserved8; + bool permit_seal; + bool permit_store_local_cap; + bool permit_store_cap; + bool permit_load_cap; + bool permit_store; + bool permit_load; + bool permit_execute; + bool global; + bool sealed; + bit[64] offset; + bit[64] base; + bit[64] length; +} + +let (CapStruct) null_cap = { + tag = false; + padding = 0; + otype = 0; + uperms = 0; + perm_reserved11_14 = 0; + access_system_regs = false; + perm_reserved9 = false; + perm_reserved8 = false; + permit_seal = false; + permit_store_local_cap = false; + permit_store_cap = false; + permit_load_cap = false; + permit_store = false; + permit_load = false; + permit_execute = false; + global = false; + sealed = false; + offset = 0; + base = 0; + length = 0; +} + +def Nat cap_size_t = 32 (* cap size in bytes *) +let ([:cap_size_t:]) cap_size = 32 + +function CapStruct capRegToCapStruct((CapReg) capReg) = + { + tag = capReg[256]; + padding = capReg[255..248]; + otype = capReg[247..224]; + uperms = capReg[223..208]; + perm_reserved11_14 = capReg[207..204]; + access_system_regs = capReg[203]; + perm_reserved9 = capReg[202]; + perm_reserved8 = capReg[201]; + permit_seal = capReg[200]; + permit_store_local_cap = capReg[199]; + permit_store_cap = capReg[198]; + permit_load_cap = capReg[197]; + permit_store = capReg[196]; + permit_load = capReg[195]; + permit_execute = capReg[194]; + global = capReg[193]; + sealed = capReg[192]; + offset = capReg[191..128]; + base = capReg[127..64]; + length = capReg[63..0]; + } + +function (bit[31]) getCapPerms((CapStruct) cap) = + ( + cap.uperms + : cap.perm_reserved11_14 + : [cap.access_system_regs] + : [cap.perm_reserved9] + : [cap.perm_reserved8] + : [cap.permit_seal] + : [cap.permit_store_local_cap] + : [cap.permit_store_cap] + : [cap.permit_load_cap] + : [cap.permit_store] + : [cap.permit_load] + : [cap.permit_execute] + : [cap.global] + ) + + +(* Function used to convert capabilities to in-memory format + - this is the same as register format except for the offset, + field which is stored as an absolute cursor on CHERI + due to uarch optimisation *) +function (bit[256]) capStructToMemBits((CapStruct) cap) = + ( + cap.padding + : cap.otype + : getCapPerms(cap) + : [cap.sealed] + (* NB in memory format stores cursor, not offset *) + : (cap.base + cap.offset) + : cap.base + : cap.length + ) + + +(* Reverse of above used when reading from memory *) +function (bit[257]) memBitsToCapBits((bool) tag, (bit[256]) b) = + ([tag] + : b[255..192] + : ((bit[64])(b[191..128] - b[127..64])) + : b[127..0] + ) + +function (CapReg) capStructToCapReg((CapStruct) cap) = + ( + [cap.tag] + : cap.padding + : cap.otype + : getCapPerms(cap) + : [cap.sealed] + : cap.offset + : cap.base + : cap.length + ) + +function CapStruct setCapPerms((CapStruct) cap, (bit[31]) perms) = + { cap with + uperms = perms[30..15]; + perm_reserved11_14 = perms[14..11]; + access_system_regs = perms[10]; + perm_reserved9 = perms[9]; + perm_reserved8 = perms[8]; + permit_seal = perms[7]; + permit_store_local_cap = perms[6]; + permit_store_cap = perms[5]; + permit_load_cap = perms[4]; + permit_store = perms[3]; + permit_load = perms[2]; + permit_execute = perms[1]; + global = perms[0]; + } + +function (bool, CapStruct) sealCap((CapStruct) cap, (bit[24]) otype) = + (true, {cap with sealed=true; otype=otype}) + +function bit[64] getCapBase((CapStruct) c) = c.base +function bit[65] getCapTop((CapStruct) c) = (0b0 : c.base) + (0b0 : c.length) +function bit[64] getCapOffset((CapStruct) c) = c.offset +function bit[65] getCapLength((CapStruct) c) = EXTZ(c.length) + +function nat getCapCursor((CapStruct) cap) = + (unsigned(cap.base) + unsigned(cap.offset)) mod (2 ** 64) + +function (bool, CapStruct) setCapOffset((CapStruct) c, (bit[64]) offset) = + (true, {c with offset=offset}) + +function (bool, CapStruct) incCapOffset((CapStruct) c, (bit[64]) delta) = + let (bit[64]) newOffset = c.offset + delta in + (true, {c with offset = newOffset}) + +function (bool, CapStruct) setCapBounds((CapStruct) cap, (bit[64]) base, (bit[65]) top) = + let (bit[65]) length = top - (0b0 : base) in + (true, {cap with base = base; length = length[63..0]; offset = 0}) + +function CapStruct int_to_cap ((bit[64]) offset) = + {null_cap with offset = offset} + diff --git a/cheri/cheri_prelude.sail b/cheri/cheri_prelude_common.sail index 428b3d8c..7530c9cc 100644 --- a/cheri/cheri_prelude.sail +++ b/cheri/cheri_prelude_common.sail @@ -32,30 +32,6 @@ (* SUCH DAMAGE. *) (*========================================================================*) -(* 265-bit capability is really 257 bits including tag *) -typedef CapReg = register bits [256:0] { - 256: tag; - (* 255..248: reserved1; padding *) - 247..224: otype; - 223..208: sw_perms; - 207..204: perm_reserved11_14; - 203: access_system_regs; - 202: perm_reserved9; (* perm bit 9 *) - 201: perm_reserved8; (* perm bit 8 *) - 200: permit_seal; - 199: permit_store_local_cap; - 198: permit_store_cap; - 197: permit_load_cap; - 196: permit_store; - 195: permit_load; - 194: permit_execute; - 193: global; - 192: sealed; - 191..128: offset; - 127..64: base; - 63 .. 0: length; -} - register CapReg PCC register CapReg nextPCC register CapReg delayedPCC @@ -92,151 +68,35 @@ register CapReg C29 (* aka kernel code capability, KCC *) register CapReg C30 (* aka kernel data capability, KDC *) register CapReg C31 (* aka exception program counter capability, EPCC *) -let (vector <0, 32, inc, (CapReg)>) CapRegs = +let (vector <0, 32, inc, (register<CapReg>)>) 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 CapStruct = const struct { - bool tag; - bit[8] padding; - bit[24] otype; - bit[16] sw_perms; - bit[4] perm_reserved11_14; - bool access_system_regs; - bool perm_reserved9; - bool perm_reserved8; - bool permit_seal; - bool permit_store_local_cap; - bool permit_store_cap; - bool permit_load_cap; - bool permit_store; - bool permit_load; - bool permit_execute; - bool global; - bool sealed; - bit[64] offset; - bit[64] base; - bit[64] length; -} - -let (CapStruct) null_cap = { - tag = false; - padding = 0; - otype = 0; - sw_perms = 0; - perm_reserved11_14 = 0; - access_system_regs = false; - perm_reserved9 = false; - perm_reserved8 = false; - permit_seal = false; - permit_store_local_cap = false; - permit_store_cap = false; - permit_load_cap = false; - permit_store = false; - permit_load = false; - permit_execute = false; - global = false; - sealed = false; - offset = 0; - base = 0; - length = 0; -} let (nat) max_otype = 0xffffff -def Nat cap_size_t = 32 (* cap size in bytes *) -let ([:cap_size_t:]) cap_size = 32 let have_cp2 = true -function CapStruct capRegToCapStruct((CapReg) capReg) = - { - tag = capReg.tag; - padding = capReg[255..248]; - otype = capReg.otype; - sw_perms = capReg.sw_perms; - perm_reserved11_14 = capReg.perm_reserved11_14; - access_system_regs = capReg.access_system_regs; - perm_reserved9 = capReg.perm_reserved9; - perm_reserved8 = capReg.perm_reserved8; - permit_seal = capReg.permit_seal; - permit_store_local_cap = capReg.permit_store_local_cap; - permit_store_cap = capReg.permit_store_cap; - permit_load_cap = capReg.permit_load_cap; - permit_store = capReg.permit_store; - permit_load = capReg.permit_load; - permit_execute = capReg.permit_execute; - global = capReg.global; - sealed = capReg.sealed; - offset = capReg.offset; - base = capReg.base; - length = capReg.length; - } - - function (CapStruct) readCapReg((regno) n) = capRegToCapStruct(CapRegs[n]) -function (bit[31]) capPermsToVec((CapStruct) cap) = - ( - cap.sw_perms - : cap.perm_reserved11_14 - : [cap.access_system_regs] - : [cap.perm_reserved9] - : [cap.perm_reserved8] - : [cap.permit_seal] - : [cap.permit_store_local_cap] - : [cap.permit_store_cap] - : [cap.permit_load_cap] - : [cap.permit_store] - : [cap.permit_load] - : [cap.permit_execute] - : [cap.global] - ) - -(* Function used to convert capabilities to in-memory format - - this is the same as register format except for the offset, - field which is stored as an absolute cursor on CHERI - due to uarch optimisation *) -function (bit[256]) capStructToMemBits((CapStruct) cap) = - ( - cap.padding - : cap.otype - : capPermsToVec(cap) - : [cap.sealed] - (* NB in memory format stores cursor, not offset *) - : (cap.base + cap.offset) - : cap.base - : cap.length - ) - - -(* Reverse of above used when reading from memory *) -function (bit[257]) memBitsToCapBits((bool) tag, (bit[256]) b) = - ([tag] - : b[255..192] - : ((bit[64])(b[191..128] - b[127..64])) - : b[127..0] - ) - -function (bit[257]) capStructToBit257((CapStruct) cap) = - ( - [cap.tag] - : cap.padding - : cap.otype - : capPermsToVec(cap) - : [cap.sealed] - : cap.offset - : cap.base - : cap.length - ) - -function nat getCapCursor((CapStruct) cap) = - (((nat)(cap.base)) + ((nat)(cap.offset))) mod (2 ** 64) - function unit writeCapReg((regno) n, (CapStruct) cap) = - { - (CapRegs[n]) := capStructToBit257(cap) - } + CapRegs[n] := capStructToCapReg(cap) + +(* +function (CapStruct) readCapReg((regno) n) = +function (CapReg) capStructToCapReg((CapStruct) cap) = +function (CapReg) memBitsToCapBits((bool) tag, (bit[8*cap_size_t]) b)function unit writeCapReg((regno) n, (CapStruct) cap) = +function bit[64] getCapBase((CapStruct) c) +function bit[65] getCapTop((CapStruct) c) +function bit[64] getCapOffset((CapStruct) c) +function bit[65] getCapLength((CapStruct) c) = getCapTop(c) - (0b0 : getCapBase(c)) +function nat getCapCursor((CapStruct) cap) +function (bool, CapStruct) setCapOffset((CapStruct) c, (bit[64]) offset) +function (bool, CapStruct) incCapOffset((CapStruct) c, (bit[64]) delta) +function (bool, CapStruct) setCapBounds((CapStruct) cap, (bit[64]) base, (bit[65]) top) +function CapStruct int_to_cap ((bit[64]) offset) +*) typedef CapEx = enumerate { CapEx_None; @@ -261,16 +121,6 @@ typedef CapEx = enumerate { CapEx_AccessSystemRegsViolation; } -typedef CGetXOp = enumerate { - CGetPerm; - CGetType; - CGetBase; - CGetOffset; - CGetLen; - CGetTag; - CGetUnsealed; -} - typedef CPtrCmpOp = enumerate { CEQ; CNE; @@ -321,12 +171,14 @@ register CapCauseReg CapCause function forall Type 'o . 'o SignalException ((Exception) ex) = { - C31 := PCC; - C31.offset := PC; + let pcc = capRegToCapStruct(PCC) in + let (success, epcc) = setCapOffset(pcc, PC) in + C31 := capStructToCapReg(epcc); + (* XXX what if not success? *) nextPCC := C29; (* KCC *) delayedPCC := C29; (* always write delayedPCC together whether PCC so that non-capability branches don't override PCC *) - SignalExceptionMIPS(ex, C29.base); + SignalExceptionMIPS(ex, getCapBase(capRegToCapStruct(C29))); } function unit ERETHook() = @@ -352,15 +204,23 @@ function forall Type 'o . 'o raise_c2_exception((CapEx) capEx, (regno) regnum) = function forall Type 'o . 'o raise_c2_exception_noreg((CapEx) capEx) = raise_c2_exception8(capEx, 0xff) +function bool pcc_access_system_regs () = + let pcc = capRegToCapStruct(PCC) in + (pcc.access_system_regs) + function bool register_inaccessible((regno) r) = - ~(switch(r) { - case 0b11011 -> (PCC.access_system_regs) - case 0b11100 -> (PCC.access_system_regs) - case 0b11101 -> (PCC.access_system_regs) - case 0b11110 -> (PCC.access_system_regs) - case 0b11111 -> (PCC.access_system_regs) - case _ -> bitone - }) + let is_sys_reg = switch(r) { + case 0b11011 -> true + case 0b11100 -> true + case 0b11101 -> true + case 0b11110 -> true + case 0b11111 -> true + case _ -> false + } in + if is_sys_reg then + not (pcc_access_system_regs ()) + else + false val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * ('n + 1)]) effect { rmem } MEMr_tag val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * ('n + 1)]) effect { rmem } MEMr_tag_reserve @@ -400,6 +260,10 @@ function bool MEMw_tagged_conditional((bit[64]) addr, (bool) tag, (bit[cap_size_ MEMval_tag_conditional(addr, cap_size, 0b0000000 : [tag] : data); } +function (bit[64]) align((bit[64]) addr, (nat) alignment) = + let remainder = unsigned(addr) mod alignment in + addr - remainder + function unit effect {wmem} MEMw_wrapper(addr, size, data) = if (addr == 0x000000007f000000) then { @@ -411,7 +275,7 @@ function unit effect {wmem} MEMw_wrapper(addr, size, data) = (* On cheri non-capability writes must clear the corresponding tag XXX this is vestigal and only works on sequential modle -- tag clearing should probably be done in memory model. *) - TAGw((addr[63..5] : 0b00000), 0x00); + TAGw(align(addr, cap_size), 0x00); MEMea(addr,size); MEMval(addr, size, data); } @@ -423,7 +287,7 @@ function bool effect {wmem} MEMw_conditional_wrapper(addr, size, data) = success := MEMval_conditional(addr,size,data); if (success) then (* XXX as above TAGw is vestigal and must die *) - TAGw((addr[63..5] : 0b00000), 0x00); + TAGw(align(addr, cap_size), 0x00); success; } @@ -434,7 +298,7 @@ function bit[64] addrWrapper((bit[64]) addr, (MemAccessType) accessType, (WordTy if (~(cap.tag)) then (raise_c2_exception(CapEx_TagViolation, capno)) else if (cap.sealed) then - (raise_c2_exception(CapEx_SealViolation, capno)); + (raise_c2_exception(CapEx_SealViolation, capno)); switch (accessType) { 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)) @@ -442,26 +306,29 @@ function bit[64] addrWrapper((bit[64]) addr, (MemAccessType) accessType, (WordTy }; cursor := getCapCursor(cap); vAddr := cursor + unsigned(addr); - vAddr64:= (bit[64]) vAddr; size := wordWidthBytes(width); - if ((vAddr + size) > ((nat) (cap.base) + ((nat) (cap.length)))) then + base := unsigned(getCapBase(cap)); + top := unsigned(getCapTop(cap)); + if ((vAddr + size) > top) then (raise_c2_exception(CapEx_LengthViolation, capno)) - else if (vAddr < ((nat) (cap.base))) then - (raise_c2_exception(CapEx_LengthViolation, capno)); - vAddr64; + else if (vAddr < (base)) then + (raise_c2_exception(CapEx_LengthViolation, capno)) + else + (bit[64]) vAddr; (* XXX vAddr not truncated because top <= 2^64 and size > 0 *) } function (bit[64]) TranslateAddress ((bit[64]) vAddr, (MemAccessType) accessType) = { incrementCP0Count(); - let (bit[64]) base = PCC.base in - let (bit[64]) length = PCC.length in - let (bit[64]) absPC = (base + vAddr) in - if (absPC[1..0] != 0b00) then (* bad PC alignment *) - (SignalExceptionBadAddr(AdEL, absPC)) - else if ((unsigned(vAddr) + 4) > unsigned(length)) then + let pcc = capRegToCapStruct(PCC) in + let base = unsigned(getCapBase(pcc)) in + let top = unsigned(getCapTop(pcc)) in + let absPC = base + unsigned(vAddr) in + if ((absPC mod 4) != 0) then (* bad PC alignment *) + (SignalExceptionBadAddr(AdEL, (bit[64]) absPC)) (* XXX absPC may be truncated *) + else if ((absPC + 4) > top) then (raise_c2_exception_noreg(CapEx_LengthViolation)) else - TLBTranslate(absPC, accessType) + TLBTranslate((bit[64]) absPC, accessType) (* XXX assert absPC never gets truncated due to above check and top <= 2^64 for valid caps *) } function unit checkCP2usable () = @@ -472,4 +339,3 @@ function unit checkCP2usable () = (SignalException(CpU)); } } - diff --git a/src/Makefile b/src/Makefile index 594f5c15..7927f9bc 100644 --- a/src/Makefile +++ b/src/Makefile @@ -39,10 +39,10 @@ MIPS_NOTLB_SAILS:=$(MIPS_NOTLB_SAILS_PRE) $(BITBUCKET_ROOT)/sail/etc/regfp.sail CHERI_SAIL_DIR:=$(BITBUCKET_ROOT)/sail/cheri -CHERI_NOTLB_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb_stub.sail $(CHERI_SAIL_DIR)/cheri_prelude.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail -CHERI_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(CHERI_SAIL_DIR)/cheri_prelude.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail +CHERI_NOTLB_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb_stub.sail $(CHERI_SAIL_DIR)/cheri_prelude_256.sail $(CHERI_SAIL_DIR)/cheri_prelude_common.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail +CHERI_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(CHERI_SAIL_DIR)/cheri_prelude_256.sail $(CHERI_SAIL_DIR)/cheri_prelude_common.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail -CHERI128_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(CHERI_SAIL_DIR)/cheri_prelude_128.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts_128.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail +CHERI128_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(CHERI_SAIL_DIR)/cheri_prelude_128.sail $(CHERI_SAIL_DIR)/cheri_prelude_common.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail elf: make -C $(ELFDIR) diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem index 51e8fd8e..9072a3bd 100644 --- a/src/lem_interp/interp.lem +++ b/src/lem_interp/interp.lem @@ -210,6 +210,8 @@ let reg_start_pos reg = | Reg _ (Just(typ,_,_,_,_)) _ -> let start_from_vec targs = match targs with | T_args [T_arg_nexp (Ne_const s);_;_;_] -> natFromInteger s + | T_args [T_arg_nexp _; T_arg_nexp (Ne_const s); T_arg_order Odec; _] -> (natFromInteger s) - 1 + | T_args [_; _; T_arg_order Oinc; _] -> 0 | _ -> Assert_extra.failwith "vector type not well formed" end in let start_from_reg targs = match targs with diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem index 3d354774..625dfb6c 100644 --- a/src/lem_interp/interp_lib.lem +++ b/src/lem_interp/interp_lib.lem @@ -350,6 +350,9 @@ let eq_vec v = else V_lit (L_aux L_zero Unknown) | (V_unknown, _) -> V_unknown | (_, V_unknown) -> V_unknown + | (V_vector _ _ [c1], _) -> eq (V_tuple [c1; v2]) + | (_, V_vector _ _ [c2]) -> eq (V_tuple [v1; c2]) + | (V_lit _, V_lit _) -> eq (V_tuple [v1;v2]) (*Vectors of one bit return one bit; we need coercion to match*) | _ -> Assert_extra.failwith ("eq_vec not given two vectors, given instead " ^ (string_of_value v)) end in match v with | (V_tuple [v1; v2]) -> binary_taint eq_vec_help v1 v2 @@ -384,6 +387,15 @@ let neq = compose neg eq ;; let neq_vec = compose neg eq_vec +let rec v_abs v = retaint v (match detaint v with + | V_lit (L_aux arg la) -> + V_lit (L_aux (match arg with + | L_num n -> if n < 0 then L_num (n * (0 - 1)) else L_num n + | _ -> Assert_extra.failwith ("abs given unexpected " ^ (string_of_value v)) end) la) + | V_unknown -> V_unknown + | V_tuple [v] -> v_abs v + | _ -> Assert_extra.failwith ("abs given unexpected " ^ (string_of_value v)) end) + let arith_op op v = let fail () = Assert_extra.failwith ("arith_op given unexpected " ^ (string_of_value v)) in let arith_op_help vl vr = @@ -1023,6 +1035,7 @@ let library_functions direction = [ ("most_significant", most_significant); ("min", min); ("max", max); + ("abs", v_abs); ] ;; let eval_external name v = match List.lookup name (library_functions IInc) with |