cheri: update to register file semantics. Most instructions now treat c0 as null capability while some still refer to DDC. Special registers moved out of general capability register file. All capabilties initialised to null except those required for MIPS compatibility.

2 files changed, 101 insertions, 66 deletions

diff --git a/cheri/cheri_insts.sail b/cheri/cheri_insts.sail
index 3df442d9..f1038ed6 100644
--- a/cheri/cheri_insts.sail
+++ b/cheri/cheri_insts.sail
@@ -363,14 +363,14 @@ function clause execute (CReadHwr(cd, sel)) =
      raise_c2_exception(CapEx_AccessSystemRegsViolation, sel)
   else {
     capVal : CapStruct = match unsigned(sel) {
-      0 => readCapReg(DDC),
-      1 => capRegToCapStruct(CTLSU),
-      8 => capRegToCapStruct(CTLSP),
-      22 => readCapReg(KR1C),
-      23 => readCapReg(KR2C),
-      29 => readCapReg(KCC),
-      30 => readCapReg(KDC),
-      31 => readCapReg(EPCC),
+      0  => capRegToCapStruct(DDC),
+      1  => capRegToCapStruct(CTLSU),
+      8  => capRegToCapStruct(CTLSP),
+      22 => capRegToCapStruct(KR1C),
+      23 => capRegToCapStruct(KR2C),
+      29 => capRegToCapStruct(KCC),
+      30 => capRegToCapStruct(KDC),
+      31 => capRegToCapStruct(EPCC),
       _  => {assert(false, "should be unreachable code"); undefined}
     };
     writeCapReg(cd, capVal);
@@ -401,14 +401,14 @@ function clause execute (CWriteHwr(cb, sel)) =
   else {
     capVal = readCapReg(cb);
     match unsigned(sel) {
-      0 => writeCapReg(DDC, capVal),
-      1 => CTLSU = capStructToCapReg(capVal),
-      8 => CTLSP = capStructToCapReg(capVal),
-      22 => writeCapReg(KR1C, capVal),
-      23 => writeCapReg(KR2C, capVal),
-      29 => writeCapReg(KCC, capVal),
-      30 => writeCapReg(KDC, capVal),
-      31 => writeCapReg(EPCC, capVal),
+      0  => DDC   = capStructToCapReg(capVal),
+      1  => CTLSU = capStructToCapReg(capVal),
+      8  => CTLSP = capStructToCapReg(capVal),
+      22 => KR1C  = capStructToCapReg(capVal),
+      23 => KR2C  = capStructToCapReg(capVal),
+      29 => KCC   = capStructToCapReg(capVal),
+      30 => KDC   = capStructToCapReg(capVal),
+      31 => EPCC  = capStructToCapReg(capVal),
       _  => assert(false, "should be unreachable code")
     };
   };
@@ -440,7 +440,7 @@ union clause ast = CToPtr : (regno, regno, regno)
 function clause execute(CToPtr(rd, cb, ct)) = 
 {
   checkCP2usable();
-  let ct_val = readCapReg(ct);
+  let ct_val = readCapRegDDC(ct);
   let cb_val = readCapReg(cb);
   if (register_inaccessible(cb)) then
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
@@ -714,7 +714,10 @@ function clause execute (ClearRegs(regset, m)) =
       match regset {
         GPLo  => wGPR(to_bits(5, i)) = zeros(),
         GPHi  => wGPR(to_bits(5, i+16)) = zeros(),
-        CLo   => writeCapReg(to_bits(5, i)) = null_cap,
+        CLo   => if i == 0 then
+                   DDC = capStructToCapReg(null_cap)
+                 else
+                   writeCapReg(to_bits(5, i)) = null_cap,
         CHi   => writeCapReg(to_bits(5, i+16)) = null_cap
       }
 }
@@ -723,7 +726,7 @@ union clause ast = CFromPtr : (regno, regno, regno)
 function clause execute (CFromPtr(cd, cb, rt)) =
 {
   checkCP2usable();
-  cb_val = readCapReg(cb);
+  cb_val = readCapRegDDC(cb);
   rt_val = rGPR(rt);
   if (register_inaccessible(cd)) then
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cd)
@@ -747,7 +750,7 @@ union clause ast = CBuildCap : (regno, regno, regno)
 function clause execute (CBuildCap(cd, cb, ct)) =
 {
   checkCP2usable();
-  cb_val = readCapReg(cb);
+  cb_val = readCapRegDDC(cb);
   ct_val = readCapReg(ct);
   cb_base = getCapBase(cb_val);
   ct_base = getCapBase(ct_val);
@@ -859,7 +862,7 @@ union clause ast = CTestSubset : (regno, regno, regno)
 function clause execute (CTestSubset(rd, cb, ct)) =
 {
   checkCP2usable();
-  cb_val = readCapReg(cb);
+  cb_val = readCapRegDDC(cb);
   ct_val = readCapReg(ct);
   ct_top    = getCapTop(ct_val);
   ct_base   = getCapBase(ct_val);
@@ -1156,7 +1159,7 @@ union clause ast = CLoad : (regno, regno, regno, bits(8), bool, WordType, bool)
 function clause execute (CLoad(rd, cb, rt, offset, signext, width, linked)) =
 {
   checkCP2usable();
-  cb_val = readCapReg(cb);
+  cb_val = readCapRegDDC(cb);
   if (register_inaccessible(cb)) then
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
   else if not (cb_val.tag) then
@@ -1198,7 +1201,7 @@ union clause ast = CStore : (regno, regno, regno, regno, bits(8), WordType, bool
 function clause execute (CStore(rs, cb, rt, rd, offset, width, conditional)) =
 {
   checkCP2usable();
-  cb_val = readCapReg(cb);
+  cb_val = readCapRegDDC(cb);
   if (register_inaccessible(cb)) then
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
   else if not (cb_val.tag) then
@@ -1254,7 +1257,7 @@ function clause execute (CSC(cs, cb, rt, rd, offset, conditional)) =
 {
   checkCP2usable();
   cs_val = readCapReg(cs);
-  cb_val = readCapReg(cb);
+  cb_val = readCapRegDDC(cb);
   if (register_inaccessible(cs)) then
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cs)
   else if (register_inaccessible(cb)) then
@@ -1303,7 +1306,7 @@ union clause ast = CLC : (regno, regno, regno, bits(16), bool)
 function clause execute (CLC(cd, cb, rt, offset, linked)) =  
 {
   checkCP2usable();
-  cb_val = readCapReg(cb);
+  cb_val = readCapRegDDC(cb);
   if (register_inaccessible(cd)) then
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cd)
   else if (register_inaccessible(cb)) then
diff --git a/cheri/cheri_prelude_common.sail b/cheri/cheri_prelude_common.sail
index cc4c657a..d2b69de8 100644
--- a/cheri/cheri_prelude_common.sail
+++ b/cheri/cheri_prelude_common.sail
@@ -45,7 +45,7 @@ register PCC        : CapReg
 register nextPCC    : CapReg
 register delayedPCC : CapReg
 register inCCallDelay : bits(1)
-register C00 : CapReg /* aka default data capability, DDC */
+register DDC : CapReg
 register C01 : CapReg
 register C02 : CapReg
 register C03 : CapReg
@@ -72,22 +72,28 @@ register C23 : CapReg
 register C24 : CapReg /* aka return code capability, RCC */
 register C25 : CapReg
 register C26 : CapReg /* aka invoked data capability, IDC */
-register C27 : CapReg /* aka kernel reserved capability 1, KR1C */
-register C28 : CapReg /* aka kernel reserved capability 2, KR2C */
-register C29 : CapReg /* aka kernel code capability, KCC */
-register C30 : CapReg /* aka kernel data capability, KDC */
-register C31 : CapReg /* aka exception program counter capability, EPCC */
+register C27 : CapReg
+register C28 : CapReg
+register C29 : CapReg
+register C30 : CapReg
+register C31 : CapReg
 
 register CTLSU : CapReg /* User thread local storage capabiltiy */
 register CTLSP : CapReg /* Privileged thread local storage capabiltiy */
+register KR1C  : CapReg /* kernel reserved capability 1 */
+register KR2C  : CapReg /* kernel reserved capability 2 */
+register KCC   : CapReg /* kernel code capability */
+register KDC   : CapReg /* kernel data capability */
+register EPCC  : CapReg /* exception program counter capability */
 
-let DDC  : regno = 0b00000 /* C0  */
-let IDC  : regno = 0b11010 /* C26 */
-let KR1C : regno = 0b11011 /* C27 */
-let KR2C : regno = 0b11100 /* C28 */
-let KCC  : regno = 0b11101 /* C29 */
-let KDC  : regno = 0b11110 /* C30 */
-let EPCC : regno = 0b11111 /* C31 */
+let IDCNO  : regno = 0b11010 /* C26, invoked data capability used be CCall */
+
+/* Special register used to have these numbers -- here for transition purposes */
+let KR1CNO : regno = 0b11011 /* C27 */
+let KR2CNO : regno = 0b11100 /* C28 */
+let KCCNO  : regno = 0b11101 /* C29 */
+let KDCNO  : regno = 0b11110 /* C30 */
+let EPCCNO : regno = 0b11111 /* C31 */
 
 let CapRegs : vector(32, dec, register(CapReg)) =
   [
@@ -122,7 +128,7 @@ let CapRegs : vector(32, dec, register(CapReg)) =
     ref C03,
     ref C02,
     ref C01,
-    ref C00
+    ref DDC
   ]
 
 let max_otype = MAX(24) /*0xffffff*/
@@ -130,15 +136,32 @@ let have_cp2 = true
 
 /*!
 This function reads a given capability register and returns its contents converted to a CapStruct.
+If the argument is zero then the null capability is returned.
 */
 val readCapReg : regno -> CapStruct effect {rreg}
 function readCapReg(n) =
-  let 'i = unsigned(n) in
-  capRegToCapStruct(reg_deref(CapRegs[i]))
+  if (n == 0b00000) then
+    null_cap
+  else
+    let i = unsigned(n) in
+    capRegToCapStruct(reg_deref(CapRegs[i]))
+
+/*!
+This is the same as readCapReg except that when the argument is zero the value of DDC is returned 
+instead of the null capability. This is used for instructions that expect an address, where using
+null would always generate an exception.
+*/
+val readCapRegDDC : regno -> CapStruct effect {rreg}
+function readCapRegDDC(n) =
+  let i = unsigned(n) in
+  capRegToCapStruct(reg_deref(CapRegs[i])) /* NB CapRegs[0] is points to DDC */
 
 function writeCapReg(n, cap) : (regno, CapStruct) -> unit =
-  let 'i = unsigned(n) in
-  (*CapRegs[i]) = capStructToCapReg(cap) 
+  if (n == 0b00000) then
+    ()
+  else
+    let i = unsigned(n) in
+    (*CapRegs[i]) = capStructToCapReg(cap) 
 
 enum CapEx = {
   CapEx_None, 
@@ -214,22 +237,22 @@ function SignalException (ex) =
       let pcc = capRegToCapStruct(PCC) in
       let (success, epcc) = setCapOffset(pcc, pc) in
       if (success) then
-        C31 = capStructToCapReg(epcc)
+        EPCC = capStructToCapReg(epcc)
       else
-        C31 = capStructToCapReg(int_to_cap(to_bits(64, getCapBase(pcc)) + unsigned(pc)));
+        EPCC = capStructToCapReg(int_to_cap(to_bits(64, getCapBase(pcc)) + unsigned(pc)));
     };
 
-    nextPCC    = C29; /* KCC */
-    delayedPCC = C29; /* always write delayedPCC together with nextPCC so 
+    nextPCC    = KCC;
+    delayedPCC = KCC; /* always write delayedPCC together with nextPCC so 
                           that non-capability branches don't override PCC */
-    let base = getCapBase(capRegToCapStruct(C29)) in
+    let base = getCapBase(capRegToCapStruct(KCC)) in
     SignalExceptionMIPS(ex, to_bits(64, base));
   }
 
 function ERETHook() : unit -> unit =
   {
-    nextPCC    = C31;
-    delayedPCC = C31; /* always write delayedPCC together with nextPCC so 
+    nextPCC    = EPCC;
+    delayedPCC = EPCC; /* always write delayedPCC together with nextPCC so 
                           that non-capability branches don't override PCC */
   }
 
@@ -247,7 +270,7 @@ function raise_c2_exception8(capEx, regnum) =
 val raise_c2_exception : forall ('o : Type) . (CapEx, regno) -> 'o effect {escape, rreg, wreg}
 function raise_c2_exception(capEx, regnum) =
   let reg8 = 0b000 @ regnum in
-  if ((capEx == CapEx_AccessSystemRegsViolation) & (regnum == IDC)) then
+  if ((capEx == CapEx_AccessSystemRegsViolation) & (regnum == IDCNO)) then
      raise_c2_exception8(CapEx_AccessCCallIDCViolation, reg8)
   else
      raise_c2_exception8(capEx, reg8)
@@ -266,12 +289,12 @@ The following function should be called before reading or writing any capability
  */
 val register_inaccessible : regno -> bool effect {rreg}
 function register_inaccessible(r) =
-  ((r == IDC) & inCCallDelay) |
-  ((r == KR1C |
-    r == KR2C |
-    r == KDC  |
-    r == KCC  |
-    r == EPCC) & not (pcc_access_system_regs ()))
+  ((r == IDCNO) & inCCallDelay) |
+  ((r == KR1CNO |
+    r == KR2CNO |
+    r == KDCNO  |
+    r == KCCNO  |
+    r == EPCCNO) & not (pcc_access_system_regs ()))
 
 val MEMr_tag = "read_tag_bool"  : bits(64) -> bool effect { rmemt }
 val MEMw_tag = "write_tag_bool" : (bits(64) , bool) -> unit effect { wmvt }
@@ -355,7 +378,7 @@ val addrWrapper : (bits(64), MemAccessType, WordType) -> bits(64) effect {rreg,
 function addrWrapper(addr, accessType, width) =
   {
     capno = 0b00000;
-    cap = readCapReg(capno);
+    cap = readCapRegDDC(capno);
     if (not (cap.tag)) then
       (raise_c2_exception(CapEx_TagViolation, capno))
     else if (cap.sealed) then
@@ -416,12 +439,21 @@ function checkCP2usable ()  =
 
 function init_cp2_state () = {
   let defaultBits = capStructToCapReg(default_cap);
+  let nullBits = capStructToCapReg(null_cap);
   PCC = defaultBits;
   nextPCC = defaultBits;
   delayedPCC = defaultBits;
-  foreach(i from 0 to 31) {
+  DDC  = defaultBits;
+  KCC  = defaultBits;
+  EPCC = defaultBits;
+  KDC  = nullBits;
+  KR1C = nullBits;
+  KR2C = nullBits;
+  CTLSP = nullBits;
+  CTLSU = nullBits;
+  foreach(i from 1 to 31) {
     let idx = to_bits(5, i) in
-    writeCapReg(idx, default_cap);
+    writeCapReg(idx, null_cap)
   }
 }
 
@@ -457,15 +489,15 @@ function dump_cp2_state () = {
   foreach(i from 0 to 31) {
     print(concat_str("DEBUG CAP REG ", concat_str(string_of_int(i), capToString(readCapReg(to_bits(5, i))))))
   };
-  print(concat_str("DEBUG CAP HWREG 00", capToString(capRegToCapStruct(C00))));
+  print(concat_str("DEBUG CAP HWREG 00", capToString(capRegToCapStruct(DDC))));
   print(concat_str("DEBUG CAP HWREG 01", capToString(capRegToCapStruct(CTLSU))));
   print(concat_str("DEBUG CAP HWREG 08", capToString(capRegToCapStruct(CTLSP))));
   /* TODO: these two should not be mirrored to match the FPGA */
-  print(concat_str("DEBUG CAP HWREG 22", capToString(capRegToCapStruct(C27))));
-  print(concat_str("DEBUG CAP HWREG 23", capToString(capRegToCapStruct(C28))));
+  print(concat_str("DEBUG CAP HWREG 22", capToString(capRegToCapStruct(KR1C))));
+  print(concat_str("DEBUG CAP HWREG 23", capToString(capRegToCapStruct(KR2C))));
   /* KCC, KDC, EPCC */
-  print(concat_str("DEBUG CAP HWREG 29", capToString(capRegToCapStruct(C29))));
-  print(concat_str("DEBUG CAP HWREG 30", capToString(capRegToCapStruct(C30))));
-  print(concat_str("DEBUG CAP HWREG 31", capToString(capRegToCapStruct(C31))));
+  print(concat_str("DEBUG CAP HWREG 29", capToString(capRegToCapStruct(KCC))));
+  print(concat_str("DEBUG CAP HWREG 30", capToString(capRegToCapStruct(KDC))));
+  print(concat_str("DEBUG CAP HWREG 31", capToString(capRegToCapStruct(EPCC))));
 
 }