Merge remote-tracking branch 'origin/sail2' into c_fixes

5 files changed, 181 insertions, 94 deletions

diff --git a/cheri/Makefile b/cheri/Makefile
index 1cd9ecc7..0d207391 100644
--- a/cheri/Makefile
+++ b/cheri/Makefile
@@ -36,10 +36,20 @@ coverage_report: bisect*.out
 	bisect-ppx-report -I _sbuild/_build -html $@ $^
 
 cheri.c: $(CHERI_SAILS) $(CHERI_MAIN)
-	$(SAIL) -memo_z3 -c $^ 1> $@
+	$(SAIL) -memo_z3 -O -c $^ 1> $@
 
+C_OPT=-O2
+GCOV_FLAGS=
 cheri_c: cheri.c ../lib/sail.h Makefile
-	gcc -O2 $< ../lib/*.c -lgmp -lz -I ../lib/ -o $@
+	gcc $(C_OPT) $(GCOV_FLAGS) $< ../lib/*.c -lgmp -lz -I ../lib/ -o $@
+
+# Note that for coverage purposes O1 appears optimal. O0 means lots of obviously dead code but O2 risks reducing granularity too much.
+cheri_c_gcov: C_OPT=-O1
+cheri_c_gcov: GCOV_FLAGS=-fprofile-arcs -ftest-coverage
+cheri_c_gcov: cheri_c
+
+gcovr:
+	gcovr -r . --html --html-detail -o index.html
 
 latex_128: $(MIPS_SAIL_DIR)/prelude.sail $(CHERI_SAIL_DIR)/cheri_types.sail $(CHERI_SAIL_DIR)/cheri_prelude_128.sail
 	rm -rf sail_latexcc
@@ -57,6 +67,17 @@ cheri128: $(CHERI128_SAILS) $(CHERI_MAIN)
 cheri128_trace: $(CHERI128_SAILS) $(CHERI_MAIN)
 	$(SAIL) -ocaml_trace -o $@ $^
 
+cheri128.c: $(CHERI128_SAILS) $(CHERI_MAIN)
+	$(SAIL) -memo_z3 -O -c $^ 1> $@
+
+cheri128_c: cheri128.c ../lib/sail.h Makefile
+	gcc $(C_OPT) $(GCOV_FLAGS) $< ../lib/*.c -lgmp -lz -I ../lib/ -o $@
+
+# Note that for coverage purposes O1 appears optimal. O0 means lots of obviously dead code but O2 risks reducing granularity too much.
+cheri128_c_gcov: C_OPT=-O1
+cheri128_c_gcov: GCOV_FLAGS=-fprofile-arcs -ftest-coverage
+cheri128_c_gcov: cheri128_c
+
 LOC_FILES:=$(CHERI_SAILS) $(CHERI_MAIN)
 include ../etc/loc.mk
 
@@ -86,7 +107,7 @@ C%.thy: c%.lem c%_types.lem $(MIPS_SAIL_DIR)/mips_extras.lem
 	sed -i 's/datatype ast/datatype (plugins only: size) ast/' C$*_types.thy
 
 %Script.sml: %.lem %_types.lem $(MIPS_SAIL_DIR)/mips_extras.lem
-	lem -hol -outdir . -lib $(SAIL_DIR)/lib/hol -lib $(SAIL_DIR)/src/gen_lib -lib $(SAIL_DIR)/src/lem_interp $^
+	lem -hol -outdir . -lib $(SAIL_DIR)/lib/hol -i $(SAIL_DIR)/lib/hol/sail2_prompt_monad.lem -i $(SAIL_DIR)/lib/hol/sail2_prompt.lem -lib $(SAIL_DIR)/src/gen_lib -lib $(SAIL_DIR)/src/lem_interp $^
 
 %Theory.uo: %Script.sml
 	Holmake $@
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_128.sail b/cheri/cheri_prelude_128.sail
index 263dae43..da761c91 100644
--- a/cheri/cheri_prelude_128.sail
+++ b/cheri/cheri_prelude_128.sail
@@ -291,11 +291,11 @@ function incCapOffset(c, delta) : (CapStruct, bits(64)) -> (bool, CapStruct) =
 
 /** FUNCTION:integer HighestSetBit(bits(N) x) */
 
-val HighestSetBit : forall 'N , 'N >= 2. bits('N) -> {'n, 0 <= 'n < 'N . option(atom('n))}
+val HighestSetBit : forall 'N , 'N >= 2. bits('N) -> {'n, 0 <= 'n < 'N . (bool, atom('n))}
 function HighestSetBit x = {
   foreach (i from ('N - 1) to 0 by 1 in dec)
-    if [x[i]] == 0b1 then return Some(i);
-  return None() : option(atom(0))
+    if [x[i]] == 0b1 then return (true, i);
+  return (false, 0)
 }
 
 /* hw rounds up E to multiple of 4 */
@@ -306,12 +306,12 @@ function roundUp(e) : range(0, 45) -> range(0, 48) =
     else (e - r + 4)
 
 function computeE (rlength) : bits(65) -> range(0, 48) =
-    let 'msb = HighestSetBit((rlength + (rlength >> 6)) >> 19) in
-    match msb {
-      None()   => 0,
+    let (nonzero, 'msb) = HighestSetBit((rlength + (rlength >> 6)) >> 19) in
+    if nonzero then 
       /* above will always return <= 45 because 19 bits of zero are shifted in from right */
-      Some('b) => {assert(0 <= b & b <= 45); roundUp (min(b,45)) }
-      }
+      {assert(0 <= msb & msb <= 45); roundUp (min(msb,45)) }
+    else 
+      0
 
 function setCapBounds(cap, base, top) : (CapStruct, bits(64), bits(65)) -> (bool, CapStruct) =
     /* {cap with base=base; length=(bits(64)) length; offset=0} */
diff --git a/cheri/cheri_prelude_256.sail b/cheri/cheri_prelude_256.sail
index babfc117..08e285e7 100644
--- a/cheri/cheri_prelude_256.sail
+++ b/cheri/cheri_prelude_256.sail
@@ -86,7 +86,7 @@ let default_cap : CapStruct = struct {
   padding = zeros(),
   otype = zeros(),
   uperms = ones(),
-  perm_reserved11_14 = ones(),
+  perm_reserved11_14 = zeros(),
   access_system_regs = true,
   permit_unseal = true,
   permit_ccall = true,
@@ -178,7 +178,7 @@ function capStructToCapReg(cap) : CapStruct -> CapReg = cap.tag @ capStructToMem
 function setCapPerms(cap, perms) : (CapStruct, bits(31)) -> CapStruct =
     { cap with
       uperms                 = perms[30..15],
-      perm_reserved11_14     = perms[14..11],
+      /* perm_reserved11_14     = perms[14..11], XXX should allow to set? only affects cbuildcap. */
       access_system_regs     = perms[10],
       permit_unseal          = perms[9],
       permit_ccall           = perms[8],
diff --git a/cheri/cheri_prelude_common.sail b/cheri/cheri_prelude_common.sail
index cc4c657a..764a4ff1 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 }
@@ -351,29 +374,60 @@ function MEMw_conditional_wrapper(addr, size, data) =
     success;
   }
 
-val addrWrapper : (bits(64), MemAccessType, WordType) -> bits(64) effect {rreg, wreg, escape}
-function addrWrapper(addr, accessType, width) =
+val checkDDCPerms : (CapStruct, MemAccessType) -> unit effect {escape, rreg, wreg}
+function checkDDCPerms(ddc : CapStruct, accessType: MemAccessType) = 
   {
-    capno = 0b00000;
-    cap = readCapReg(capno);
-    if (not (cap.tag)) then
-      (raise_c2_exception(CapEx_TagViolation, capno))
-    else if (cap.sealed) then
-        (raise_c2_exception(CapEx_SealViolation, capno));
+    if (not (ddc.tag)) then
+      raise_c2_exception(CapEx_TagViolation, 0b00000)
+    else if (ddc.sealed) then
+      raise_c2_exception(CapEx_SealViolation, 0b00000);
     match accessType {
-      Instruction  => if (~(cap.permit_execute)) then (raise_c2_exception(CapEx_PermitExecuteViolation, capno)),
-      LoadData     => if (~(cap.permit_load)) then (raise_c2_exception(CapEx_PermitLoadViolation, capno)),
-      StoreData    => if (~(cap.permit_store)) then (raise_c2_exception(CapEx_PermitStoreViolation, capno))
+      Instruction  => assert(false), /* Only data accesses use DDC */
+      LoadData     => if (~(ddc.permit_load)) then (raise_c2_exception(CapEx_PermitLoadViolation, 0b00000)),
+      StoreData    => if (~(ddc.permit_store)) then (raise_c2_exception(CapEx_PermitStoreViolation, 0b00000))
     };
-    cursor = getCapCursor(cap);
+  }
+
+val addrWrapper : (bits(64), MemAccessType, WordType) -> bits(64) effect {rreg, wreg, escape}
+function addrWrapper(addr, accessType, width) =
+  {
+    ddc    = capRegToCapStruct(DDC);
+    checkDDCPerms(ddc, accessType);
+    cursor = getCapCursor(ddc);
     vAddr  = (cursor + unsigned(addr)) % pow2(64);
     size   = wordWidthBytes(width);
-    base   = getCapBase(cap);
-    top    = getCapTop(cap);
+    base   = getCapBase(ddc);
+    top    = getCapTop(ddc);
     if ((vAddr + size) > top) then
-      (raise_c2_exception(CapEx_LengthViolation, capno))
+      (raise_c2_exception(CapEx_LengthViolation, 0b00000))
     else if (vAddr < base) then
-      (raise_c2_exception(CapEx_LengthViolation, capno))
+      (raise_c2_exception(CapEx_LengthViolation, 0b00000))
+    else
+      to_bits(64, vAddr);
+  }
+
+val addrWrapperUnaligned : (bits(64), MemAccessType, WordTypeUnaligned) -> bits(64) effect {rreg, wreg, escape}
+function addrWrapperUnaligned(addr, accessType, width) =
+  {
+    ddc    = capRegToCapStruct(DDC);
+    checkDDCPerms(ddc, accessType);
+    cursor = getCapCursor(ddc);
+    vAddr  = (cursor + unsigned(addr)) % pow2(64);
+    woffset = vAddr % 4;
+    doffset = vAddr % 8;
+    /* Compute the address and size of the bytes touched -- this depends on alignment. */
+    let (waddr, size) : (int, int) = match width {
+      WL => (vAddr, 4 - woffset),
+      WR => (vAddr - woffset, woffset + 1),
+      DL => (vAddr, 8 - doffset),
+      DR => (vAddr - doffset, doffset + 1)
+    };
+    base   = getCapBase(ddc);
+    top    = getCapTop(ddc);
+    if ((waddr + size) > top) then
+      (raise_c2_exception(CapEx_LengthViolation, 0b00000))
+    else if (waddr < base) then
+      (raise_c2_exception(CapEx_LengthViolation, 0b00000))
     else
       to_bits(64, vAddr);
   }
@@ -416,12 +470,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 +520,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))));
 
 }