summaryrefslogtreecommitdiff
path: root/cheri
diff options
context:
space:
mode:
Diffstat (limited to 'cheri')
-rw-r--r--cheri/cheri_insts.sail344
-rw-r--r--cheri/cheri_prelude_128.sail28
-rw-r--r--cheri/cheri_prelude_256.sail18
-rw-r--r--cheri/cheri_prelude_common.sail12
4 files changed, 304 insertions, 98 deletions
diff --git a/cheri/cheri_insts.sail b/cheri/cheri_insts.sail
index 101414f8..3c1e34bb 100644
--- a/cheri/cheri_insts.sail
+++ b/cheri/cheri_insts.sail
@@ -32,6 +32,159 @@
(* SUCH DAMAGE. *)
(*========================================================================*)
+(* Old encodings *)
+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))
+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 : 0b00000 : (regno) rd : 0b00000 : 0b00000000 : 0b100) = Some(CGetCause(rd))
+
+function clause decode (0b010010 : 0b00110 : 0b000000000000000000000) = Some(CReturn)
+
+function clause decode (0b010010 : 0b01101 : (regno) rd : (regno) cb : 0b00000000 : 0b010) = Some(CGetOffset(rd, cb)) (* NB encoding does not follow pattern *)
+function clause decode (0b010010 : 0b00100 : 0b00000 : 0b00000 : (regno) rt : 0b000 : 0b100) = Some(CSetCause(rt))
+function clause decode (0b010010 : 0b00100 : (regno) cd : (regno) cb : (regno) rt : 0b000 : 0b000) = Some(CAndPerm(cd, cb, rt))
+function clause decode (0b010010 : 0b01100 : (regno) rd : (regno) cb : (regno) ct : 0b000 : 0b000) = Some(CToPtr(rd, cb, ct))
+
+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 decode (0b010010 : 0b01110 : (regno) rd : (regno) cb : (regno) ct : 0b000 : 0b111) = Some(CPtrCmp(rd, cb, ct, CNEXEQ))
+function clause decode (0b010010 : 0b01101 : (regno) cd : (regno) cb : (regno) rt : 0b000 : 0b000) = Some(CIncOffset(cd, cb, rt))
+function clause decode (0b010010 : 0b01101 : (regno) cd : (regno) cb : (regno) rt : 0b000 : 0b001) = Some(CSetOffset(cd, cb, rt))
+function clause decode (0b010010 : 0b00001 : (regno) cd : (regno) cb : (regno) rt : 0b000000) = Some(CSetBounds(cd, cb, rt))
+
+function clause decode (0b010010 : 0b00100 : (regno) cd : (regno) cb : 0b00000 : 0b000: 0b101) = Some(CClearTag(cd, cb))
+function clause decode (0b010010 : 0b00100 : (regno) cd : (regno) cb : (regno) rt : 0b000: 0b111) = Some(CFromPtr(cd, cb, rt))
+function clause decode (0b010010 : 0b01011 : (regno) cs : 0b00000 : (regno) rt : 0b000: 0b000) = Some(CCheckPerm(cs, rt))
+function clause decode (0b010010 : 0b01011 : (regno) cs : (regno) cb : 0b00000 : 0b000: 0b001) = Some(CCheckType(cs, cb))
+function clause decode (0b010010 : 0b00010 : (regno) cd : (regno) cs : (regno) ct : 0b000: 0b000) = Some(CSeal(cd, cs, ct))
+function clause decode (0b010010 : 0b00011 : (regno) cd : (regno) cs : (regno) ct : 0b000: 0b000) = Some(CUnseal(cd, cs, ct))
+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 *)
+
+
+(*
+New encodings as per CHERI ISA Appendix B.2.
+
+NB: Must be careful about order of matching because unused register
+fields are re-used as additional function codes.
+*)
+
+(* One arg *)
+function clause decode (0b010010 : 0b00000 : (regno) rd : 0b00001 : 0b11111 : 0b111111) = Some(CGetCause(rd))
+function clause decode (0b010010 : 0b00000 : (regno) rs : 0b00010 : 0b11111 : 0b111111) = Some(CSetCause(rs))
+function clause decode (0b010010 : 0b00000 : (regno) cd : 0b00000 : 0b11111 : 0b111111) = Some(CGetPCC(cd))
+function clause decode (0b010010 : 0b00000 : (regno) cb : 0b00011 : 0b11111 : 0b111111) = Some(CJALR(0b00000, cb, false)) (* CJR *)
+
+(* Two arg *)
+function clause decode (0b010010 : 0b00000 : (regno) cs : (regno) rt : 0b01000 : 0b111111) = Some(CCheckPerm(cs, rt))
+function clause decode (0b010010 : 0b00000 : (regno) cs : (regno) cb : 0b01001 : 0b111111) = Some(CCheckType(cs, cb))
+function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cb : 0b01011 : 0b111111) = Some(CClearTag(cd, cb))
+function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cs : 0b01010 : 0b111111) = Some(CMOVX(cd, cs, 0b00000, false)) (* CMOVE *)
+function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cb : 0b01100 : 0b111111) = Some(CJALR(cd, cb, true)) (* CJALR *)
+
+(* Capability Inspection *)
+function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : 0b00000 : 0b111111) = Some(CGetPerm(rd, cb))
+function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : 0b00001 : 0b111111) = Some(CGetType(rd, cb))
+function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : 0b00010 : 0b111111) = Some(CGetBase(rd, cb))
+function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : 0b00011 : 0b111111) = Some(CGetLen(rd, cb))
+function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : 0b00100 : 0b111111) = Some(CGetTag(rd, cb))
+function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : 0b00101 : 0b111111) = Some(CGetSealed(rd, cb))
+function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : 0b00110 : 0b111111) = Some(CGetOffset(rd, cb))
+function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) rs : 0b00111 : 0b111111) = Some(CGetPCCSetOffset(cd, rs))
+
+(* Three operand *)
+
+(* Capability Modification *)
+function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cs : (regno) ct : 0b001011) = Some(CSeal(cd, cs, ct))
+function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cs : (regno) ct : 0b001100) = Some(CUnseal(cd, cs, ct))
+function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cs : (regno) rt : 0b001101) = Some(CAndPerm(cd, cs, rt))
+function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cs : (regno) rt : 0b001111) = Some(CSetOffset(cd, cs, rt))
+function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cs : (regno) rt : 0b001000) = Some(CSetBounds(cd, cs, rt))
+function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cs : (regno) rt : 0b001001) = Some(CSetBoundsExact(cd, cs, rt))
+
+
+function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cb : (regno) rt : 0b010001) = Some(CIncOffset(cd, cb, rt))
+function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cb : (regno) ct : 0b011101) = Some(CBuildCap(cd, cb, ct))
+function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cb : (regno) ct : 0b011110) = Some(CCopyType(cd, cb, ct))
+function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cs : (regno) ct : 0b011111) = Some(CCSeal(cd, cs, ct))
+
+(* Pointer Arithmetic *)
+function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : (regno) ct : 0b010010) = Some(CToPtr(rd, cb, ct))
+function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cb : (regno) rs : 0b010011) = Some(CFromPtr(cd, cb, rs))
+function clause decode (0b010010 : 0b00000 : (regno) rt : (regno) cb : (regno) cs : 0b001010) = Some(CSub(rt, cb, cs))
+function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cs : (regno) rs : 0b011011) = Some(CMOVX(cd, cs, rs, false)) (* CMOVZ *)
+function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cs : (regno) rs : 0b011100) = Some(CMOVX(cd, cs, rs, true)) (* CMOVN *)
+
+(* Pointer Comparison *)
+function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : (regno) cs : 0b010100) = Some(CPtrCmp(rd, cb, cs, CEQ))
+function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : (regno) cs : 0b010101) = Some(CPtrCmp(rd, cb, cs, CNE))
+function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : (regno) cs : 0b010110) = Some(CPtrCmp(rd, cb, cs, CLT))
+function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : (regno) cs : 0b010111) = Some(CPtrCmp(rd, cb, cs, CLE))
+function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : (regno) cs : 0b011000) = Some(CPtrCmp(rd, cb, cs, CLTU))
+function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : (regno) cs : 0b011001) = Some(CPtrCmp(rd, cb, cs, CLEU))
+function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : (regno) cs : 0b011010) = Some(CPtrCmp(rd, cb, cs, CEXEQ))
+function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : (regno) cs : 0b100001) = Some(CPtrCmp(rd, cb, cs, CNEXEQ))
+
+function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : (regno) ct : 0b100000) = Some(CTestSubset(rd, cb, ct))
+
+function clause decode (0b010010 : 0b01001 : (regno) cd : (bit[16]) imm) = Some(CBX(cd, imm, true)) (* CBTU *)
+function clause decode (0b010010 : 0b01010 : (regno) cd : (bit[16]) imm) = Some(CBX(cd, imm, false)) (* CBTS *)
+function clause decode (0b010010 : 0b10001 : (regno) cd : (bit[16]) imm) = Some(CBZ(cd, imm, false)) (* CBEZ *)
+function clause decode (0b010010 : 0b10010 : (regno) cd : (bit[16]) imm) = Some(CBZ(cd, imm, true)) (* CBNZ *)
+
+function clause decode (0b010010 : 0b00101 : 0b00000 : 0b00000 : 0b11111111111) = Some(CReturn)
+function clause decode (0b010010 : 0b00101 : (regno) cs : (regno) cb : (bit[11]) selector) = Some(CCall(cs, cb, selector))
+
+function clause decode (0b010010 : 0b01111 : 0b00000 : (bit[16]) imm) = Some(ClearRegs(GPLo, imm))
+function clause decode (0b010010 : 0b01111 : 0b00001 : (bit[16]) imm) = Some(ClearRegs(GPHi, imm))
+function clause decode (0b010010 : 0b01111 : 0b00010 : (bit[16]) imm) = Some(ClearRegs(CLo, imm))
+function clause decode (0b010010 : 0b01111 : 0b00011 : (bit[16]) imm) = Some(ClearRegs(CHi, imm))
+
+function clause decode (0b010010 : 0b10011 : (regno) cd : (regno) cb : (bit[11]) imm) = Some(CIncOffsetImmediate(cd, cb, imm))
+function clause decode (0b010010 : 0b10100 : (regno) cd : (regno) cb : (bit[11]) imm) = Some(CSetBoundsImmediate(cd, cb, imm))
+
+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 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 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 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 decode (0b010010 : 0b00100 : (regno) rt : 0x0006) = Some(C2Dump(rt))
+
(* Operations that extract parts of a capability into GPR *)
union ast member (regno, regno) CGetPerm
@@ -42,15 +195,6 @@ 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 *)
@@ -141,7 +285,6 @@ function clause execute (CGetSealed(rd, cb)) =
}
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 *)
@@ -158,7 +301,6 @@ function clause execute (CGetPCC(cd)) =
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 *)
@@ -178,7 +320,6 @@ function clause execute (CGetPCCSetOffset(cd, rs)) =
(* 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 *)
@@ -191,7 +332,6 @@ function clause execute (CGetCause(rd)) =
}
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 *)
@@ -208,7 +348,6 @@ function clause execute (CSetCause((regno) rt)) =
}
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 *)
@@ -233,7 +372,6 @@ function clause execute(CAndPerm(cd, cb, rt)) =
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 *)
@@ -267,7 +405,6 @@ function clause execute(CToPtr(rd, cb, ct)) =
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 *)
@@ -286,15 +423,6 @@ function clause execute(CSub(rd, cb, ct)) =
}
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 decode (0b010010 : 0b01110 : (regno) rd : (regno) cb : (regno) ct : 0b000 : 0b111) = Some(CPtrCmp(rd, cb, ct, CNEXEQ))
-
function clause execute(CPtrCmp(rd, cb, ct, op)) =
{
(* START_CPtrCmp *)
@@ -341,7 +469,6 @@ function clause execute(CPtrCmp(rd, cb, ct, op)) =
}
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 *)
@@ -363,8 +490,29 @@ function clause execute (CIncOffset(cd, cb, rt)) =
(* END_CIncOffset *)
}
+union ast member (regno, regno, bit[11]) CIncOffsetImmediate
+function clause execute (CIncOffsetImmediate(cd, cb, imm)) =
+{
+ (* START_CIncOffsetImmediate *)
+ checkCP2usable();
+ cb_val := readCapReg(cb);
+ let (bit[64]) imm64 = EXTZ(imm) in
+ 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) = incCapOffset(cb_val, imm64) in
+ if (success) then
+ writeCapReg(cd, newCap)
+ else
+ writeCapReg(cd, int_to_cap(getCapBase(cb_val) + imm64))
+ (* END_CIncOffsetImmediate *)
+}
+
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 *)
@@ -387,7 +535,6 @@ function clause execute (CSetOffset(cd, cb, rt)) =
}
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 *)
@@ -416,9 +563,36 @@ function clause execute (CSetBounds(cd, cb, rt)) =
(* END_CSetBounds *)
}
+union ast member (regno, regno, bit[11]) CSetBoundsImmediate
+function clause execute (CSetBoundsImmediate(cd, cb, imm)) =
+{
+ (* START_CSetBoundsImmedate *)
+ checkCP2usable();
+ cb_val := readCapReg(cb);
+ immU := unsigned(imm);
+ cursor := getCapCursor(cb_val);
+ base := getCapBase(cb_val);
+ top := getCapTop(cb_val);
+ newTop := cursor + immU;
+ 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_CSetBoundsImmediate *)
+}
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 *)
@@ -451,7 +625,6 @@ function clause execute (CSetBoundsExact(cd, cb, rt)) =
}
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 *)
@@ -469,9 +642,7 @@ function clause execute (CClearTag(cd, cb)) =
}
union ast member (regno,regno,regno,bool) CMOVX
-function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cb : (regno) rt : 0b011100) = Some(CMOVX(cd, cb, rt, false)) (* CMOVN *)
-function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cb : (regno) rt : 0b011011) = Some(CMOVX(cd, cb, rt, true)) (* CMOVZ *)
-function clause execute (CMOVX(cd, cb, rt, ismovz)) =
+function clause execute (CMOVX(cd, cb, rt, ismovn)) =
{
(* START_CMOVX *)
checkCP2usable();
@@ -479,16 +650,12 @@ function clause execute (CMOVX(cd, cb, rt, ismovz)) =
raise_c2_exception(CapEx_AccessSystemRegsViolation, cd)
else if (register_inaccessible(cb)) then
raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
- else if ((rGPR(rt) == 0) ^ ismovz) then
+ else if ((rGPR(rt) == 0) ^ ismovn) then
writeCapReg(cd) := readCapReg(cb);
(* END_CMOVX *)
}
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 *)
@@ -511,7 +678,6 @@ function clause execute (ClearRegs(regset, mask)) =
}
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 *)
@@ -538,7 +704,6 @@ function clause execute (CFromPtr(cd, cb, rt)) =
}
union ast member regregreg CBuildCap
-function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cb : (regno) ct : 0b011101) = Some(CBuildCap(cd, cb, ct))
function clause execute (CBuildCap(cd, cb, ct)) =
{
(* START_CBuildCap *)
@@ -583,7 +748,6 @@ function clause execute (CBuildCap(cd, cb, ct)) =
}
union ast member regregreg CCopyType
-function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cb : (regno) ct : 0b011110) = Some(CCopyType(cd, cb, ct))
function clause execute (CCopyType(cd, cb, ct)) =
{
(* START_CCopyType *)
@@ -619,7 +783,6 @@ function clause execute (CCopyType(cd, cb, ct)) =
}
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 *)
@@ -639,7 +802,6 @@ function clause execute (CCheckPerm(cs, rt)) =
}
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 *)
@@ -665,8 +827,42 @@ function clause execute (CCheckType(cs, cb)) =
(* END_CCheckType *)
}
+union ast member regregreg CTestSubset
+function clause execute (CTestSubset(rd, cb, ct)) =
+{
+ (* START_CTestSubset *)
+ checkCP2usable();
+ cb_val := readCapReg(cb);
+ ct_val := readCapReg(ct);
+ ct_top := getCapTop(ct_val);
+ ct_base := getCapBase(ct_val);
+ ct_perms := getCapPerms(ct_val);
+ cb_top := getCapTop(cb_val);
+ cb_base := getCapBase(cb_val);
+ cb_perms := getCapPerms(cb_val);
+ if (register_inaccessible(cb)) then
+ raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
+ else if (register_inaccessible(ct)) then
+ raise_c2_exception(CapEx_AccessSystemRegsViolation, ct)
+ else {
+ (bit[64]) result := EXTZ(if (cb_val.tag != ct_val.tag) then
+ 0x0
+ else if (cb_val.sealed != ct_val.sealed) then
+ 0x0
+ else if (ct_base < cb_base) then
+ 0x0
+ else if (ct_top > cb_top) then
+ 0x0
+ else if ((ct_perms & cb_perms) != cb_perms) then
+ 0x0
+ else
+ 0x1);
+ wGPR(rd) := result;
+ }
+ (* END_CTestSubset *)
+}
+
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 *)
@@ -708,7 +904,6 @@ function clause execute (CSeal(cd, cs, ct)) =
}
union ast member regregreg CCSeal
-function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cs : (regno) ct : 0b011111) = Some(CCSeal(cd, cs, ct))
function clause execute (CCSeal(cd, cs, ct)) =
{
(* START_CCSeal *)
@@ -750,7 +945,6 @@ function clause execute (CCSeal(cd, cs, ct)) =
}
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 *)
@@ -790,7 +984,6 @@ function clause execute (CUnseal(cd, cs, ct)) =
}
union ast member (regno, regno, bit[11]) CCall
-function clause decode (0b010010 : 0b00101 : (regno) cs : (regno) cb : (bit[11]) selector) = Some(CCall(cs, cb, selector))
function clause execute (CCall(cs, cb, 0b00000000000)) = (* selector=0 *)
{
(* Partial implementation of CCall with checks in hardware, but raising a trap to perform trusted stack manipulation *)
@@ -865,9 +1058,10 @@ function clause execute (CCall(cs, cb, 0b00000000001)) = (* selector=1 *)
sealed=false;
otype=0;
}) in {
- nextPC := (bit[64]) (getCapOffset(cs_val));
- nextPCC := csUnsealed;
+ delayedPC := (bit[64]) (getCapOffset(cs_val));
delayedPCC := csUnsealed;
+ branchPending := true;
+ inCCallDelay := true;
C26 := capStructToCapReg({cb_val with
sealed=false;
otype=0;
@@ -877,7 +1071,6 @@ function clause execute (CCall(cs, cb, 0b00000000001)) = (* selector=1 *)
}
union ast member unit CReturn
-function clause decode (0b010010 : 0b00110 : 0b000000000000000000000) = Some(CReturn)
function clause execute (CReturn) =
{
(* START_CReturn *)
@@ -887,9 +1080,6 @@ function clause execute (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 *)
@@ -905,9 +1095,23 @@ function clause execute (CBX(cb, imm, invert)) =
(* END_CBx *)
}
+union ast member (regno, bit[16], bool) CBZ
+function clause execute (CBZ(cb, imm, invert)) =
+{
+ (* START_CBz *)
+ checkCP2usable();
+ if (register_inaccessible(cb)) then
+ raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
+ else if (((readCapReg(cb)) == null_cap) ^ invert) then
+ {
+ let (bit[64]) offset = (EXTS(imm : 0b00) + 4) in
+ delayedPC := PC + offset;
+ branchPending := 1;
+ }
+ (* END_CBz *)
+}
+
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 *)
@@ -949,22 +1153,6 @@ function clause execute(CJALR(cd, cb, link)) =
}
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 *)
@@ -1017,15 +1205,6 @@ function clause execute (CLoad(rd, cb, rt, offset, signext, width, linked)) =
}
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)) =
{
@@ -1084,8 +1263,6 @@ function clause execute (CStore(rs, cb, rt, rd, offset, width, conditional)) =
}
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 *)
@@ -1136,8 +1313,6 @@ function clause execute (CSC(cs, cb, rt, rd, offset, conditional)) =
}
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 *)
@@ -1183,6 +1358,5 @@ function clause execute (CLC(cd, cb, rt, offset, linked)) =
}
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 5e63221e..cc939f59 100644
--- a/cheri/cheri_prelude_128.sail
+++ b/cheri/cheri_prelude_128.sail
@@ -84,7 +84,7 @@ let (CapStruct) null_cap = {
E = 48; (* encoded as 0 in memory due to xor *)
sealed = false;
B = 0;
- T = 0;
+ T = 0x10000;
otype = 0;
address = 0;
}
@@ -133,7 +133,7 @@ function (bit[11]) getCapHardPerms((CapStruct) cap) =
: [cap.permit_execute]
: [cap.global])
-function (bit[128]) capStructToMemBits((CapStruct) cap) =
+function (bit[128]) capStructToMemBits128((CapStruct) cap) =
let (bit[20]) b = if cap.sealed then (cap.B)[19..12] : (cap.otype)[23..12] else cap.B in
let (bit[20]) t = if cap.sealed then (cap.T)[19..12] : (cap.otype)[11..0] else cap.T in
( cap.uperms
@@ -147,12 +147,24 @@ function (bit[128]) capStructToMemBits((CapStruct) cap) =
)
function (CapReg) capStructToCapReg((CapStruct) cap) =
- ([cap.tag] : capStructToMemBits(cap))
+ ([cap.tag] : capStructToMemBits128(cap))
(* Reverse of above used when reading from memory *)
-function (CapReg) memBitsToCapBits((bool) tag, (bit[128]) b) =
+function (CapReg) memBitsToCapBits128((bool) tag, (bit[128]) b) =
([tag] : b)
+(* When saving/restoring capabilities xor them with bits of null_cap --
+ this ensures that canonical null_cap is always all-zeros in memory
+ even though it may have bits set logically (e.g. length or exponent *)
+
+let (bit[128]) null_cap_bits = capStructToMemBits128(null_cap)
+
+function (bit[128]) capStructToMemBits((CapStruct) cap) =
+ capStructToMemBits128(cap) ^ null_cap_bits
+
+function (bit[129]) memBitsToCapBits((bool) tag, (bit[128]) b) =
+ memBitsToCapBits128(tag, b ^ null_cap_bits)
+
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 *)
@@ -191,23 +203,23 @@ function [|-1:1|] a_top_correction((bit[20]) a_mid, (bit[20]) R, (bit[20]) bound
}
function uint64 getCapBase((CapStruct) c) =
- let ([|45|]) E = min(unsigned(c.E), 45) in
+ let ([|48|]) E = min(unsigned(c.E), 48) in
let (bit[20]) Bc = c.B in
let (bit[65]) a = EXTZ(c.address) in
let (bit[20]) R = Bc - 0x01000 in (* wraps *)
- let (bit[20]) a_mid = a[(E + 19)..E] in
+ let (bit[20]) a_mid = mask(a >> E) in
let correction = a_top_correction(a_mid, R, Bc) in
let a_top = a >> (E+20) in
let (bit[64]) base = EXTZ((a_top + correction) : Bc) << E in
unsigned(base)
function CapLen getCapTop ((CapStruct) c) =
- let ([|45|]) E = min(unsigned(c.E), 45) in
+ let ([|45|]) E = min(unsigned(c.E), 48) in
let (bit[20]) Bc = c.B in
let (bit[20]) T = c.T in
let (bit[65]) a = EXTZ(c.address) in
let (bit[20]) R = Bc - 0x01000 in (* wraps *)
- let (bit[20]) a_mid = a[(E + 19)..E] in
+ let (bit[20]) a_mid = mask(a >> E) in
let correction = a_top_correction(a_mid, R, T) in
let a_top = a >> (E+20) in
let (bit[65]) top1 = EXTZ((a_top + correction) : T) in
diff --git a/cheri/cheri_prelude_256.sail b/cheri/cheri_prelude_256.sail
index 7b42020d..988cfe49 100644
--- a/cheri/cheri_prelude_256.sail
+++ b/cheri/cheri_prelude_256.sail
@@ -86,7 +86,7 @@ let (CapStruct) null_cap = {
sealed = false;
offset = 0;
base = 0;
- length = 0;
+ length = 0xffffffffffffffff;
}
def Nat cap_size_t = 32 (* cap size in bytes *)
@@ -138,7 +138,7 @@ function (bit[31]) getCapPerms((CapStruct) cap) =
- 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) =
+function (bit[256]) capStructToMemBits256((CapStruct) cap) =
(
cap.padding
: cap.otype
@@ -152,13 +152,25 @@ function (bit[256]) capStructToMemBits((CapStruct) cap) =
(* Reverse of above used when reading from memory *)
-function (bit[257]) memBitsToCapBits((bool) tag, (bit[256]) b) =
+function (bit[257]) memBitsToCapBits256((bool) tag, (bit[256]) b) =
([tag]
: b[255..192]
: ((bit[64])(b[191..128] - b[127..64]))
: b[127..0]
)
+(* When saving/restoring capabilities xor them with bits of null_cap --
+ this ensures that canonical null_cap is always all-zeros in memory
+ even though it may have bits set logically (e.g. length or exponent *)
+
+function (bit[256]) capStructToMemBits((CapStruct) cap) =
+ let (bit[256]) null_cap_bits = capStructToMemBits256(null_cap) in
+ capStructToMemBits256(cap) ^ null_cap_bits
+
+function (bit[257]) memBitsToCapBits((bool) tag, (bit[256]) b) =
+ let (bit[256]) null_cap_bits = capStructToMemBits256(null_cap) in
+ memBitsToCapBits256(tag, b ^ null_cap_bits)
+
function (CapReg) capStructToCapReg((CapStruct) cap) =
(
[cap.tag]
diff --git a/cheri/cheri_prelude_common.sail b/cheri/cheri_prelude_common.sail
index f5fcd095..a2d3b441 100644
--- a/cheri/cheri_prelude_common.sail
+++ b/cheri/cheri_prelude_common.sail
@@ -45,6 +45,7 @@ scattered function option<ast> decode
register CapReg PCC
register CapReg nextPCC
register CapReg delayedPCC
+register (bit[1]) inCCallDelay
register CapReg C00 (* aka default data capability, DDC *)
register CapReg C01
register CapReg C02
@@ -115,6 +116,7 @@ typedef CapEx = enumerate {
CapEx_PermitSealViolation;
CapEx_AccessSystemRegsViolation;
CapEx_PermitCCallViolation;
+ CapEx_AccessCCallIDCViolation;
}
typedef CPtrCmpOp = enumerate {
@@ -158,6 +160,7 @@ function (bit[8]) CapExCode((CapEx) ex) =
case CapEx_PermitSealViolation -> 0x17
case CapEx_AccessSystemRegsViolation -> 0x18
case CapEx_PermitCCallViolation -> 0x19
+ case CapEx_AccessCCallIDCViolation -> 0x1a
}
typedef CapCauseReg = register bits [15:0] {
@@ -204,7 +207,11 @@ function forall Type 'o . 'o raise_c2_exception8((CapEx) capEx, (bit[8]) regnum)
}
function forall Type 'o . 'o raise_c2_exception((CapEx) capEx, (regno) regnum) =
- raise_c2_exception8(capEx, 0b000 : regnum)
+ let reg8 = 0b000 : regnum in
+ if ((capEx == CapEx_AccessSystemRegsViolation) & (regnum == 26 (* IDC *))) then
+ raise_c2_exception8(CapEx_AccessCCallIDCViolation, reg8)
+ else
+ raise_c2_exception8(capEx, reg8)
function forall Type 'o . 'o raise_c2_exception_noreg((CapEx) capEx) =
raise_c2_exception8(capEx, 0xff)
@@ -213,7 +220,8 @@ function bool pcc_access_system_regs () =
let pcc = capRegToCapStruct(PCC) in
(pcc.access_system_regs)
-function bool register_inaccessible((regno) r) =
+function bool register_inaccessible((regno) r) =
+ if ((r == 26 (* IDC *)) & ((bool)inCCallDelay)) then true else (* XXX interpreter crash without cast *)
let (bool) is_sys_reg = switch(r) {
case 0b11011 -> true
case 0b11100 -> true
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 08:24:23 +0000