From 4d3e8058659d32e0b2668950fb1bb9d2a80cd7a1 Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Mon, 2 Oct 2017 15:49:35 +0100
Subject: cheri: fix swapped cmovz and cmovn.

---
 cheri/cheri_insts.sail | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'cheri')

diff --git a/cheri/cheri_insts.sail b/cheri/cheri_insts.sail
index 8b5d9dd0..caa87e55 100644
--- a/cheri/cheri_insts.sail
+++ b/cheri/cheri_insts.sail
@@ -468,9 +468,9 @@ 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 decode (0b010010 : 0b00000 : (regno) cd : (regno) cb : (regno) rt : 0b011100) = Some(CMOVX(cd, cb, rt, true)) (* CMOVN *)
+function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cb : (regno) rt : 0b011011) = Some(CMOVX(cd, cb, rt, false)) (* CMOVZ *)
+function clause execute (CMOVX(cd, cb, rt, ismovn)) =
 {
   (* START_CMOVX *)
   checkCP2usable();
@@ -478,7 +478,7 @@ 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 *)
 }
-- 
cgit v1.2.3


From 6e2cd26a769b7cce9b9e4dcd15515c3f42ed63cf Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Fri, 13 Oct 2017 15:45:46 +0100
Subject: Add support for new cheri instruction encodings. The order of pattern
 matching is now significant because register no. fields are re-used as
 additional function codes in operations with fewer operands so I pulled out
 all decode clauses to the beginning of file for easier rearranging. Old
 encodings can co-exist with new encodings as the only overlap is for recently
 added instructions which already use the new scheme. Eventually the old
 encodings will go away, however, and the opcode space may be reclaimed."

---
 cheri/cheri_insts.sail | 232 ++++++++++++++++++++++++++++++++-----------------
 1 file changed, 151 insertions(+), 81 deletions(-)

(limited to 'cheri')

diff --git a/cheri/cheri_insts.sail b/cheri/cheri_insts.sail
index caa87e55..e126ef64 100644
--- a/cheri/cheri_insts.sail
+++ b/cheri/cheri_insts.sail
@@ -32,6 +32,157 @@
 (*  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))
+
+(* 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))
+
+(* 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))
+(* XXX function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cs :    0b01010 : 0b111111) = Some(CMove(cd, 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(CBEZ(cd, imm)) XXX *)
+(* function clause decode (0b010010 : 0b10010 : (regno) cd : (bit[16]) imm) = Some(CBNZ(cd, imm)) XXX *)
+
+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))
+
+(* XXX CSetBoundsImmediate *)
+(* XXX CIncOffsetImmediate *)
+
+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 +193,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 *)
@@ -140,7 +282,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 *)
@@ -157,7 +298,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 *)
@@ -177,7 +317,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 *)
@@ -190,7 +329,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 *)
@@ -207,7 +345,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 *)
@@ -232,7 +369,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 *)
@@ -266,7 +402,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 *)
@@ -285,15 +420,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 *)
@@ -340,7 +466,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,7 +488,6 @@ function clause execute (CIncOffset(cd, cb, rt)) =
 }
 
 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 *)
@@ -386,7 +510,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 *)
@@ -417,7 +540,6 @@ function clause execute (CSetBounds(cd, cb, rt)) =
 
 
 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 *)
@@ -450,7 +572,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 *)
@@ -468,8 +589,6 @@ 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, true)) (* CMOVN *)
-function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cb : (regno) rt : 0b011011) = Some(CMOVX(cd, cb, rt, false)) (* CMOVZ *)
 function clause execute (CMOVX(cd, cb, rt, ismovn)) =
 {
   (* START_CMOVX *)
@@ -484,10 +603,6 @@ function clause execute (CMOVX(cd, cb, rt, ismovn)) =
 }
 
 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 *)
@@ -510,7 +625,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 *)
@@ -537,7 +651,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 *)
@@ -582,7 +695,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 *)
@@ -618,7 +730,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 *)
@@ -638,7 +749,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,7 +775,6 @@ function clause execute (CCheckType(cs, cb)) =
 }
 
 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 *)
@@ -707,7 +816,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 *)
@@ -749,7 +857,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 *)
@@ -789,7 +896,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 *)
@@ -876,7 +982,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 *)
@@ -886,9 +991,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,8 +1007,6 @@ function clause execute (CBX(cb, imm, invert)) =
 }
 
 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 *)
@@ -948,22 +1048,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 *)
@@ -1011,15 +1095,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)) =
 {
@@ -1078,8 +1153,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 *)
@@ -1130,8 +1203,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 *)
@@ -1176,6 +1247,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 *)
-- 
cgit v1.2.3


From 91c90cba4b0580802b5c4610e1b3dc5d10e3b4ae Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Mon, 16 Oct 2017 11:09:13 +0100
Subject: add support for capability branch null instructions.

---
 cheri/cheri_insts.sail | 22 +++++++++++++++++++---
 1 file changed, 19 insertions(+), 3 deletions(-)

(limited to 'cheri')

diff --git a/cheri/cheri_insts.sail b/cheri/cheri_insts.sail
index e126ef64..d5ba8d06 100644
--- a/cheri/cheri_insts.sail
+++ b/cheri/cheri_insts.sail
@@ -133,10 +133,10 @@ function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : (regno) c
 
 (* 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 : 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(CBEZ(cd, imm)) XXX *)
-(* function clause decode (0b010010 : 0b10010 : (regno) cd : (bit[16]) imm) = Some(CBNZ(cd, imm)) XXX *)
+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))
@@ -1006,6 +1006,22 @@ 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 execute(CJALR(cd, cb, link)) = 
 {
-- 
cgit v1.2.3


From 3c678570789fbbe37d25e2b6201b0eefb10fbae2 Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Mon, 16 Oct 2017 12:17:07 +0100
Subject: add support for CIncOffsetImmediate and CSetBoundsImmediate.

---
 cheri/cheri_insts.sail | 54 ++++++++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 52 insertions(+), 2 deletions(-)

(limited to 'cheri')

diff --git a/cheri/cheri_insts.sail b/cheri/cheri_insts.sail
index d5ba8d06..7542e377 100644
--- a/cheri/cheri_insts.sail
+++ b/cheri/cheri_insts.sail
@@ -146,8 +146,8 @@ function clause decode (0b010010 : 0b01111 : 0b00001 : (bit[16]) imm) = Some(Cle
 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))
 
-(* XXX CSetBoundsImmediate *)
-(* XXX CIncOffsetImmediate *)
+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 *)
@@ -487,6 +487,28 @@ 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 execute (CSetOffset(cd, cb, rt)) =
 {
@@ -538,6 +560,34 @@ 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 execute (CSetBoundsExact(cd, cb, rt)) =
-- 
cgit v1.2.3


From 27816b955866bd5021cb8534f92480d83d76cc32 Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Mon, 16 Oct 2017 14:46:50 +0100
Subject: implement CMove as an alias for cmovz with zero register.

---
 cheri/cheri_insts.sail | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'cheri')

diff --git a/cheri/cheri_insts.sail b/cheri/cheri_insts.sail
index 7542e377..3b602d03 100644
--- a/cheri/cheri_insts.sail
+++ b/cheri/cheri_insts.sail
@@ -86,6 +86,7 @@ function clause decode (0b010010 : 0b00000 : (regno) cd :    0b00000 :    0b1111
 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 *)
 
 (* Capability Inspection *)
 function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb :    0b00000 : 0b111111) = Some(CGetPerm(rd, cb))
@@ -117,7 +118,6 @@ function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cs : (regno) c
 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))
-(* XXX function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cs :    0b01010 : 0b111111) = Some(CMove(cd, 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 *)
 
-- 
cgit v1.2.3


From 1522c658263cb1f646e44489ba8a19764fe8f4c4 Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Mon, 16 Oct 2017 16:21:07 +0100
Subject: add missing new encodings for CJR and CJALR.

---
 cheri/cheri_insts.sail | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'cheri')

diff --git a/cheri/cheri_insts.sail b/cheri/cheri_insts.sail
index 3b602d03..1d6c4a13 100644
--- a/cheri/cheri_insts.sail
+++ b/cheri/cheri_insts.sail
@@ -81,12 +81,14 @@ fields are re-used as additional function codes.
 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))
-- 
cgit v1.2.3


From 7bd52dedf93ccaf4811307e12b8402fad6ab2312 Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Mon, 16 Oct 2017 16:24:59 +0100
Subject: add CTestSubset instruction.

---
 cheri/cheri_insts.sail | 37 ++++++++++++++++++++++++++++++++++++-
 1 file changed, 36 insertions(+), 1 deletion(-)

(limited to 'cheri')

diff --git a/cheri/cheri_insts.sail b/cheri/cheri_insts.sail
index 1d6c4a13..c27f6dc7 100644
--- a/cheri/cheri_insts.sail
+++ b/cheri/cheri_insts.sail
@@ -133,7 +133,7 @@ function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : (regno) c
 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 : 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 *)
@@ -826,6 +826,41 @@ 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 execute (CSeal(cd, cs, ct)) =
 {
-- 
cgit v1.2.3


From 99a7462a88a186faf817e21c065e25f04d30aea7 Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Mon, 23 Oct 2017 17:47:16 +0100
Subject: cheri: Null capability should have maximum length, because in
 cheri128 we want all offsets to be representable. To maintain all-zeros as
 the in-memory representation of the null capability we xor memory bits with
 null capability when loading and storing.

---
 cheri/cheri_prelude_128.sail | 26 +++++++++++++++++++-------
 cheri/cheri_prelude_256.sail | 18 +++++++++++++++---
 2 files changed, 34 insertions(+), 10 deletions(-)

(limited to 'cheri')

diff --git a/cheri/cheri_prelude_128.sail b/cheri/cheri_prelude_128.sail
index 98b0a40c..9bc0e2d2 100644
--- a/cheri/cheri_prelude_128.sail
+++ b/cheri/cheri_prelude_128.sail
@@ -73,10 +73,10 @@ let (CapStruct) null_cap = {
   permit_execute         = false;
   global                 = false;
   reserved               = 0;
-  E                      = 48; (* encoded as 0 in memory due to xor *)
+  E                      = 48;
   sealed                 = false;
   B                      = 0;
-  T                      = 0;
+  T                      = 0x10000;
   otype                  = 0;
   address                = 0;
 }
@@ -104,7 +104,7 @@ function CapStruct capRegToCapStruct((CapReg) c) =
     permit_execute         = c[114];
     global                 = c[113];
     reserved               = c[112..111];
-    E                      = c[110..105] ^ 0b110000;
+    E                      = c[110..105];
     sealed                 = s;
     B                      = B;
     T                      = T;
@@ -125,13 +125,13 @@ 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
     : getCapHardPerms(cap)
     : cap.reserved
-    : (cap.E ^ 0b110000) (* XXX brackets required otherwise sail interpreter error *)
+    : (cap.E)
     : [cap.sealed]
     : b
     : t
@@ -139,12 +139,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 *)
diff --git a/cheri/cheri_prelude_256.sail b/cheri/cheri_prelude_256.sail
index f41d9c14..1b13e408 100644
--- a/cheri/cheri_prelude_256.sail
+++ b/cheri/cheri_prelude_256.sail
@@ -78,7 +78,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 *)
@@ -130,7 +130,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
@@ -144,13 +144,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 *)
+
+let (bit[256]) null_cap_bits = capStructToMemBits256(null_cap)
+
+function (bit[256]) capStructToMemBits((CapStruct) cap) =
+  capStructToMemBits256(cap) ^ null_cap_bits
+
+function (bit[257]) memBitsToCapBits((bool) tag, (bit[256]) b) =
+  memBitsToCapBits256(tag, b ^ null_cap_bits)
+
 function (CapReg) capStructToCapReg((CapStruct) cap) =
     (
       [cap.tag]
-- 
cgit v1.2.3


From 29182cd14e228529b3e26ef901e927bde8d27345 Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Tue, 24 Oct 2017 15:44:10 +0100
Subject: fix default cap value on cheri128 following previous changes -- E
 stored in registers is no longer xored with 48 so need to initialise it. Also
 use E and T values used by CHERI hw and adjust decoding functions
 appropriately. Fix shift functions for ocaml shallow embedding which failed
 to handle shifts greater than vector length.

---
 cheri/cheri_prelude_128.sail | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'cheri')

diff --git a/cheri/cheri_prelude_128.sail b/cheri/cheri_prelude_128.sail
index 9bc0e2d2..fbb4c21c 100644
--- a/cheri/cheri_prelude_128.sail
+++ b/cheri/cheri_prelude_128.sail
@@ -195,23 +195,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]) B = c.B in
     let (bit[65]) a = EXTZ(c.address) in
     let (bit[20]) R = B - 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, B) in
     let a_top = a >> (E+20) in
     let (bit[64]) base = EXTZ((a_top + correction) : B) << E in
     unsigned(base)
 
 function CapLen getCapTop ((CapStruct) c)  = 
-    let ([|45|])  E = min(unsigned(c.E), 45) in
+    let ([|48|])  E = min(unsigned(c.E), 48) in
     let (bit[20]) B = c.B in
     let (bit[20]) T = c.T in
     let (bit[65]) a = EXTZ(c.address)  in
     let (bit[20]) R = B - 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
-- 
cgit v1.2.3


From b41ee79485e155f67099b007650d73f449db1961 Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Tue, 31 Oct 2017 11:01:10 +0000
Subject: cheri: ccall selector 1 should have a branch delay slot. TODO we need
 to throw exception for access to IDC/C26 in branch delay slot.

---
 cheri/cheri_insts.sail | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'cheri')

diff --git a/cheri/cheri_insts.sail b/cheri/cheri_insts.sail
index c27f6dc7..50399785 100644
--- a/cheri/cheri_insts.sail
+++ b/cheri/cheri_insts.sail
@@ -1057,9 +1057,9 @@ 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;
       C26 := capStructToCapReg({cb_val with
         sealed=false;
         otype=0;
-- 
cgit v1.2.3


From a35692d69681683c2bffe7c824ad230b88679ed9 Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Tue, 31 Oct 2017 16:09:46 +0000
Subject: cheri: throw an exception if there is an attempt to access C26/IDC in
 the delay slot of a ccall selector 1 call.

---
 cheri/cheri_insts.sail          |  1 +
 cheri/cheri_prelude_common.sail | 12 ++++++++++--
 2 files changed, 11 insertions(+), 2 deletions(-)

(limited to 'cheri')

diff --git a/cheri/cheri_insts.sail b/cheri/cheri_insts.sail
index 50399785..5687a275 100644
--- a/cheri/cheri_insts.sail
+++ b/cheri/cheri_insts.sail
@@ -1060,6 +1060,7 @@ function clause execute (CCall(cs, cb, 0b00000000001)) = (* selector=1 *)
       delayedPC := (bit[64]) (getCapOffset(cs_val));
       delayedPCC := csUnsealed;
       branchPending := true;
+      inCCallDelay  := true;
       C26 := capStructToCapReg({cb_val with
         sealed=false;
         otype=0;
diff --git a/cheri/cheri_prelude_common.sail b/cheri/cheri_prelude_common.sail
index dcb56d01..fa36decb 100644
--- a/cheri/cheri_prelude_common.sail
+++ b/cheri/cheri_prelude_common.sail
@@ -35,6 +35,7 @@
 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
@@ -105,6 +106,7 @@ typedef CapEx = enumerate {
   CapEx_PermitSealViolation;
   CapEx_AccessSystemRegsViolation;
   CapEx_PermitCCallViolation;
+  CapEx_AccessCCallIDCViolation;
 }
 
 typedef CPtrCmpOp = enumerate {
@@ -148,6 +150,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] {
@@ -194,7 +197,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)
@@ -203,7 +210,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 *)) & inCCallDelay) then true else
   let is_sys_reg = switch(r) {
     case 0b11011 -> true
     case 0b11100 -> true
-- 
cgit v1.2.3


From 701d572adda905e6b2098a73c9af56f98212b4a3 Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Tue, 31 Oct 2017 17:02:16 +0000
Subject: work around interpreter crash by adding cast. Likely this kind of
 thing will be resolved by merge of new_tc branch.

---
 cheri/cheri_prelude_common.sail | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'cheri')

diff --git a/cheri/cheri_prelude_common.sail b/cheri/cheri_prelude_common.sail
index fa36decb..a84c118f 100644
--- a/cheri/cheri_prelude_common.sail
+++ b/cheri/cheri_prelude_common.sail
@@ -211,7 +211,7 @@ function bool pcc_access_system_regs () =
       (pcc.access_system_regs)
 
 function bool register_inaccessible((regno) r) =
-  if ((r == 26 (* IDC *)) & inCCallDelay) then true else
+  if ((r == 26 (* IDC *)) & ((bool)inCCallDelay)) then true else (* XXX interpreter crash without cast *)
   let is_sys_reg = switch(r) {
     case 0b11011 -> true
     case 0b11100 -> true
-- 
cgit v1.2.3


From 40a85677707395199a005c2742304b80be87e117 Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Wed, 1 Nov 2017 18:42:17 +0000
Subject: workaound for another odd interpreter error where top level let
 variable got truncated to 64 bits...

---
 cheri/cheri_prelude_256.sail | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'cheri')

diff --git a/cheri/cheri_prelude_256.sail b/cheri/cheri_prelude_256.sail
index 1b13e408..b2bc8b1f 100644
--- a/cheri/cheri_prelude_256.sail
+++ b/cheri/cheri_prelude_256.sail
@@ -155,12 +155,12 @@ function (bit[257]) memBitsToCapBits256((bool) tag, (bit[256]) b) =
    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[256]) null_cap_bits = capStructToMemBits256(null_cap)
-
 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) =
-- 
cgit v1.2.3