Normalise whitespace in cheri_insts.sail for cleaner extraction of instructions into manual. Whitespace only.

2 files changed, 370 insertions, 372 deletions

diff --git a/cheri/Makefile b/cheri/Makefile
index 1c7c2304..200ddd5a 100644
--- a/cheri/Makefile
+++ b/cheri/Makefile
@@ -14,7 +14,7 @@ extract: cheri_insts.sail
 	$(call EXTRACT_INST,CSetOffset)
 	$(call EXTRACT_INST,CSetBounds)
 	$(call EXTRACT_INST,CClearTag)
-	$(call EXTRACT_INST,CClearRegs)
+	$(call EXTRACT_INST,ClearRegs)
 	$(call EXTRACT_INST,CFromPtr)
 	$(call EXTRACT_INST,CCheckPerm)
 	$(call EXTRACT_INST,CCheckType)
diff --git a/cheri/cheri_insts.sail b/cheri/cheri_insts.sail
index 215f0f19..15725b44 100644
--- a/cheri/cheri_insts.sail
+++ b/cheri/cheri_insts.sail
@@ -45,87 +45,87 @@ function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : 0b0000000
 function clause decode (0b010010 : 0b01101 : (regno) rd : (regno) cb : 0b00000000 : 0b010) = Some(CGetX(CGetOffset, rd, cb)) (* NB encoding does not follow pattern *)
 
 function clause execute (CGetX(op, rd, cb)) =
-  {
-    (* START_CGetX *)
-    checkCP2usable();
-    if (register_inaccessible(cb)) then
-      exit (raise_c2_exception_v(cb))
-    else
-      {
-        cbval    := CapRegs[cb];
-        wGPR(rd) := switch(op) {
-          case CGetPerm     -> EXTZ(cbval[223..193])  (* XXX only correct for 256-bit *)
-          case CGetType     -> EXTZ(cbval.otype)
-          case CGetBase     -> cbval.base
-          case CGetOffset   -> cbval.offset
-          case CGetLen      -> cbval.length
-          case CGetTag      -> EXTZ([cbval.tag])
-          case CGetUnsealed -> EXTZ([cbval.sealed])
-        }
+{
+  (* START_CGetX *)
+  checkCP2usable();
+  if (register_inaccessible(cb)) then
+    exit (raise_c2_exception_v(cb))
+  else
+    {
+      cbval    := CapRegs[cb];
+      wGPR(rd) := switch(op) {
+        case CGetPerm     -> EXTZ(cbval[223..193])  (* XXX only correct for 256-bit *)
+        case CGetType     -> EXTZ(cbval.otype)
+        case CGetBase     -> cbval.base
+        case CGetOffset   -> cbval.offset
+        case CGetLen      -> cbval.length
+        case CGetTag      -> EXTZ([cbval.tag])
+        case CGetUnsealed -> EXTZ([cbval.sealed])
       }
-    (* END_CGetX *)
-  }
+    }
+  (* END_CGetX *)
+}
 
 union ast member regno CGetPCC
 function clause decode (0b010010 : 0b00000 : (regno) cd : 0b00000 : 0b11111 : 0b111111) = Some(CGetPCC(cd))
 function clause execute (CGetPCC(cd)) =
-    {
-      (* START_CGetPCC *)
-      checkCP2usable();
-      if (register_inaccessible(cd)) then
-        exit (raise_c2_exception_v(cd))
-      else
-        let pcc = (capRegToCapStruct(PCC)) in
-        writeCapReg(cd, {pcc with offset = PC})
-      (* END_CGetPCC *)
-    }
+{
+  (* START_CGetPCC *)
+  checkCP2usable();
+  if (register_inaccessible(cd)) then
+    exit (raise_c2_exception_v(cd))
+  else
+    let pcc = (capRegToCapStruct(PCC)) in
+    writeCapReg(cd, {pcc with offset = PC})
+  (* END_CGetPCC *)
+}
 
 union ast member (regno, regno) CGetPCCSetOffset
 function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) rs : 0b00111 : 0b111111) = Some(CGetPCCSetOffset(cd, rs))
 function clause execute (CGetPCCSetOffset(cd, rs)) =
-    {
-      (* START_CGetPCCSetOffset *)
-      checkCP2usable();
-      if (register_inaccessible(cd)) then
-        exit (raise_c2_exception_v(cd))
-      else
-        let pcc = (capRegToCapStruct(PCC)) in
-        let rs_val = rGPR(rs) in
-        writeCapReg(cd, {pcc with offset = rs_val})
-      (* END_CGetPCCSetOffset *)
-    }
+{
+  (* START_CGetPCCSetOffset *)
+  checkCP2usable();
+  if (register_inaccessible(cd)) then
+    exit (raise_c2_exception_v(cd))
+  else
+    let pcc = (capRegToCapStruct(PCC)) in
+    let rs_val = rGPR(rs) in
+    writeCapReg(cd, {pcc with offset = rs_val})
+  (* END_CGetPCCSetOffset *)
+}
 
 (* Get and Set CP2 cause register *)
 
 union ast member regno CGetCause
 function clause decode (0b010010 : 0b00000 : (regno) rd : 0b00000 : 0b00000000 : 0b100) = Some(CGetCause(rd))
 function clause execute (CGetCause(rd)) = 
-    {
-      (* START_CGetCause *)
-      checkCP2usable();
-      if (~(PCC.access_EPCC)) then
-        exit (raise_c2_exception_noreg(CapEx_AccessEPCCViolation))
-      else
-        wGPR(rd) := EXTZ(CapCause)
-      (* END_CGetCause *)
-    }
+{
+  (* START_CGetCause *)
+  checkCP2usable();
+  if (~(PCC.access_EPCC)) then
+    exit (raise_c2_exception_noreg(CapEx_AccessEPCCViolation))
+  else
+    wGPR(rd) := EXTZ(CapCause)
+  (* END_CGetCause *)
+}
 
 union ast member (regno) CSetCause
 function clause decode (0b010010 : 0b00100 : 0b00000 : 0b00000 : (regno) rt : 0b000 : 0b100) = Some(CSetCause(rt))
 function clause execute (CSetCause((regno) rt)) = 
+{
+  (* START_CSetCause *)
+  checkCP2usable();
+  if (~(PCC.access_EPCC)) then
+    exit (raise_c2_exception_noreg(CapEx_AccessEPCCViolation))
+  else
     {
-      (* START_CSetCause *)
-      checkCP2usable();
-      if (~(PCC.access_EPCC)) then
-        exit (raise_c2_exception_noreg(CapEx_AccessEPCCViolation))
-      else
-        {
-          (bit[64]) rt_val := rGPR(rt);
-          CapCause.ExcCode := rt_val[15..8];
-          CapCause.RegNum  := rt_val[7..0];
-        }
-      (* END_CSetCause *)
+      (bit[64]) rt_val := rGPR(rt);
+      CapCause.ExcCode := rt_val[15..8];
+      CapCause.RegNum  := rt_val[7..0];
     }
+  (* END_CSetCause *)
+}
 
 union ast member regregreg CAndPerm
 function clause decode (0b010010 : 0b00100 : (regno) cd : (regno) cb : (regno) rt : 0b000 : 0b000) = Some(CAndPerm(cd, cb, rt))
@@ -144,26 +144,24 @@ function clause execute(CAndPerm(cd, cb, rt)) =
   else if (cb_val.sealed) then
     exit (raise_c2_exception(CapEx_SealViolation, cb))
   else
-    {
-      writeCapReg(cd, {cb_val with 
-        sw_perms                   = (cb_val.sw_perms                   & (rt_val[30..15]));
-        access_KR2C                = (cb_val.access_KR2C                & (rt_val[14]));
-        access_KR1C                = (cb_val.access_KR1C                & (rt_val[13]));
-        access_KCC                 = (cb_val.access_KCC                 & (rt_val[12]));
-        access_KDC                 = (cb_val.access_KDC                 & (rt_val[11]));
-        access_EPCC                = (cb_val.access_EPCC                & (rt_val[10]));
-        perm_reserved9             = (cb_val.perm_reserved9             & (rt_val[9]));
-        perm_reserved8             = (cb_val.perm_reserved8             & (rt_val[8]));
-        permit_seal                = (cb_val.permit_seal                & (rt_val[7]));
-        permit_store_local_cap     = (cb_val.permit_store_local_cap     & (rt_val[6]));
-        permit_store_cap           = (cb_val.permit_store_cap           & (rt_val[5]));
-        permit_load_cap            = (cb_val.permit_load_cap            & (rt_val[4]));
-        permit_store               = (cb_val.permit_store               & (rt_val[3]));
-        permit_load                = (cb_val.permit_load                & (rt_val[2]));
-        permit_execute             = (cb_val.permit_execute             & (rt_val[1]));
-        global                     = (cb_val.global                     & (rt_val[0]));
-      })
-    }
+    writeCapReg(cd, {cb_val with 
+      sw_perms               = (cb_val.sw_perms           & (rt_val[30..15]));
+      access_KR2C            = (cb_val.access_KR2C            & (rt_val[14]));
+      access_KR1C            = (cb_val.access_KR1C            & (rt_val[13]));
+      access_KCC             = (cb_val.access_KCC             & (rt_val[12]));
+      access_KDC             = (cb_val.access_KDC             & (rt_val[11]));
+      access_EPCC            = (cb_val.access_EPCC            & (rt_val[10]));
+      perm_reserved9         = (cb_val.perm_reserved9         & (rt_val[9]));
+      perm_reserved8         = (cb_val.perm_reserved8         & (rt_val[8]));
+      permit_seal            = (cb_val.permit_seal            & (rt_val[7]));
+      permit_store_local_cap = (cb_val.permit_store_local_cap & (rt_val[6]));
+      permit_store_cap       = (cb_val.permit_store_cap       & (rt_val[5]));
+      permit_load_cap        = (cb_val.permit_load_cap        & (rt_val[4]));
+      permit_store           = (cb_val.permit_store           & (rt_val[3]));
+      permit_load            = (cb_val.permit_load            & (rt_val[2]));
+      permit_execute         = (cb_val.permit_execute         & (rt_val[1]));
+      global                 = (cb_val.global                 & (rt_val[0]));
+    })
   (* END_CAndPerm *)
 }
 
@@ -260,90 +258,90 @@ function clause execute(CPtrCmp(rd, cb, ct, op)) =
         case CEXEQ -> [cb_val == ct_val]
       })
     }
-    (* END_CPtrCMP *)
+  (* END_CPtrCMP *)
 }
 
 union ast member regregreg CIncOffset
 function clause decode (0b010010 : 0b01101 : (regno) cd : (regno) cb : (regno) rt : 0b000 : 0b000) = Some(CIncOffset(cd, cb, rt))
 function clause execute (CIncOffset(cd, cb, rt)) =
-    {
-      (* START_CIncOffset *)
-      checkCP2usable();
-      cb_val := readCapReg(cb);
-      rt_val := rGPR(rt);
-      if (register_inaccessible(cd)) then
-        exit (raise_c2_exception_v(cd))
-      else if (register_inaccessible(cb)) then
-        exit (raise_c2_exception_v(cb))
-      else if ((cb_val.tag) & (cb_val.sealed) & (rt_val != 0x0000000000000000)) then
-        exit (raise_c2_exception(CapEx_SealViolation, cb))
-      else
-        writeCapReg(cd, {cb_val with offset=cb_val.offset+rt_val})
-      (* END_CIncOffset *)
-    }
+{
+  (* START_CIncOffset *)
+  checkCP2usable();
+  cb_val := readCapReg(cb);
+  rt_val := rGPR(rt);
+  if (register_inaccessible(cd)) then
+    exit (raise_c2_exception_v(cd))
+  else if (register_inaccessible(cb)) then
+    exit (raise_c2_exception_v(cb))
+  else if ((cb_val.tag) & (cb_val.sealed) & (rt_val != 0x0000000000000000)) then
+    exit (raise_c2_exception(CapEx_SealViolation, cb))
+  else
+    writeCapReg(cd, {cb_val with offset=cb_val.offset+rt_val})
+  (* END_CIncOffset *)
+}
 
 union ast member regregreg CSetOffset
 function clause decode (0b010010 : 0b01101 : (regno) cd : (regno) cb : (regno) rt : 0b000 : 0b001) = Some(CSetOffset(cd, cb, rt))
 function clause execute (CSetOffset(cd, cb, rt)) =
-    {
-      (* START_CSetOffset *)
-      checkCP2usable();
-      cb_val := readCapReg(cb);
-      rt_val := rGPR(rt);
-      if (register_inaccessible(cd)) then
-        exit (raise_c2_exception_v(cd))
-      else if (register_inaccessible(cb)) then
-        exit (raise_c2_exception_v(cb))
-      else if ((cb_val.tag) & (cb_val.sealed)) then
-        exit (raise_c2_exception(CapEx_SealViolation, cb))
-      else
-        writeCapReg(cd, {cb_val with offset=rt_val})
-      (* END_CSetOffset *)
-    }
+{
+  (* START_CSetOffset *)
+  checkCP2usable();
+  cb_val := readCapReg(cb);
+  rt_val := rGPR(rt);
+  if (register_inaccessible(cd)) then
+    exit (raise_c2_exception_v(cd))
+  else if (register_inaccessible(cb)) then
+    exit (raise_c2_exception_v(cb))
+  else if ((cb_val.tag) & (cb_val.sealed)) then
+    exit (raise_c2_exception(CapEx_SealViolation, cb))
+  else
+    writeCapReg(cd, {cb_val with offset=rt_val})
+  (* END_CSetOffset *)
+}
 
 union ast member regregreg CSetBounds
 function clause decode (0b010010 : 0b00001 : (regno) cd : (regno) cb : (regno) rt : 0b000000) = Some(CSetBounds(cd, cb, rt))
 function clause execute (CSetBounds(cd, cb, rt)) =
-    {
-      (* START_CSetBounds *)
-      checkCP2usable();
-      cb_val := readCapReg(cb);
-      (nat) rt_val := rGPR(rt);
-      (nat) cursor := getCapCursor(cb_val);
-      if (register_inaccessible(cd)) then
-        exit (raise_c2_exception_v(cd))
-      else if (register_inaccessible(cb)) then
-        exit (raise_c2_exception_v(cb))
-      else if (~(cb_val.tag)) then
-        exit (raise_c2_exception(CapEx_TagViolation, cb))
-      else if (cb_val.sealed) then
-        exit (raise_c2_exception(CapEx_SealViolation, cb))
-      else if (cursor < ((nat)(cb_val.base))) then
-        exit (raise_c2_exception(CapEx_LengthViolation, cb))
-      else if ((cursor + rt_val) > ((nat)(cb_val.base) + (nat)(cb_val.length))) then
-        exit (raise_c2_exception(CapEx_LengthViolation, cb))
-      else
-        writeCapReg(cd, {cb_val with base=(bit[64])cursor; length=(bit[64])rt_val; offset=0})
-      (* END_CSetBounds *)
-    }
+{
+  (* START_CSetBounds *)
+  checkCP2usable();
+  cb_val := readCapReg(cb);
+  (nat) rt_val := rGPR(rt);
+  (nat) cursor := getCapCursor(cb_val);
+  if (register_inaccessible(cd)) then
+    exit (raise_c2_exception_v(cd))
+  else if (register_inaccessible(cb)) then
+    exit (raise_c2_exception_v(cb))
+  else if (~(cb_val.tag)) then
+    exit (raise_c2_exception(CapEx_TagViolation, cb))
+  else if (cb_val.sealed) then
+    exit (raise_c2_exception(CapEx_SealViolation, cb))
+  else if (cursor < ((nat)(cb_val.base))) then
+    exit (raise_c2_exception(CapEx_LengthViolation, cb))
+  else if ((cursor + rt_val) > ((nat)(cb_val.base) + (nat)(cb_val.length))) then
+    exit (raise_c2_exception(CapEx_LengthViolation, cb))
+  else
+    writeCapReg(cd, {cb_val with base=(bit[64])cursor; length=(bit[64])rt_val; offset=0})
+  (* END_CSetBounds *)
+}
 
 union ast member (regno, regno) CClearTag
 function clause decode (0b010010 : 0b00100 : (regno) cd : (regno) cb : 0b00000 : 0b000: 0b101) = Some(CClearTag(cd, cb))
 function clause execute (CClearTag(cd, cb)) =
+{
+  (* START_CClearTag *)
+  checkCP2usable();
+  if (register_inaccessible(cd)) then
+    exit (raise_c2_exception_v(cd))
+  else if (register_inaccessible(cb)) then
+    exit (raise_c2_exception_v(cb))
+  else
     {
-      (* START_CClearTag *)
-      checkCP2usable();
-      if (register_inaccessible(cd)) then
-        exit (raise_c2_exception_v(cd))
-      else if (register_inaccessible(cb)) then
-        exit (raise_c2_exception_v(cb))
-      else
-        {
-          cb_val := readCapReg(cb);
-          writeCapReg(cd, {cb_val with tag = false});
-        }
-      (* END_CClearTag *)
+      cb_val := readCapReg(cb);
+      writeCapReg(cd, {cb_val with tag = false});
     }
+  (* END_CClearTag *)
+}
 
 union ast member (ClearRegSet, bit[16]) ClearRegs
 function clause decode (0b010010 : 0b01111 : 0b00000 : (bit[16]) imm) = Some(ClearRegs(GPLo, imm)) (* ClearLo *)
@@ -374,43 +372,43 @@ 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 *)
-      checkCP2usable();
-      cb_val := readCapReg(cb);
-      rt_val := rGPR(rt);
-      if (register_inaccessible(cd)) then
-        exit (raise_c2_exception_v(cd))
-      else if (register_inaccessible(cb)) then
-        exit (raise_c2_exception_v(cb))
-      else if (rt == 0) then
-        writeCapReg(cd, null_cap)
-      else if (~(cb_val.tag)) then
-        exit (raise_c2_exception(CapEx_TagViolation, cb))
-      else if (cb_val.sealed) then
-        exit (raise_c2_exception(CapEx_SealViolation, cb))
-      else
-        writeCapReg(cd, {cb_val with offset = rt_val});
-      (* END_CFromPtr *)
-    }
+{
+  (* START_CFromPtr *)
+  checkCP2usable();
+  cb_val := readCapReg(cb);
+  rt_val := rGPR(rt);
+  if (register_inaccessible(cd)) then
+    exit (raise_c2_exception_v(cd))
+  else if (register_inaccessible(cb)) then
+    exit (raise_c2_exception_v(cb))
+  else if (rt == 0) then
+    writeCapReg(cd, null_cap)
+  else if (~(cb_val.tag)) then
+    exit (raise_c2_exception(CapEx_TagViolation, cb))
+  else if (cb_val.sealed) then
+    exit (raise_c2_exception(CapEx_SealViolation, cb))
+  else
+    writeCapReg(cd, {cb_val with offset = rt_val});
+  (* END_CFromPtr *)
+}
 
 union ast member (regno, regno) CCheckPerm
 function clause decode (0b010010 : 0b01011 : (regno) cs : 0b00000 : (regno) rt : 0b000: 0b000) = Some(CCheckPerm(cs, rt))
 function clause execute (CCheckPerm(cs, rt)) =
-    {
-      (* START_CCheckPerm *)
-      checkCP2usable();
-      cs_val := readCapReg(cs);
-      cs_perms := capPermsToVec(cs_val);
-      rt_perms := (rGPR(rt))[30..0];
-      if (register_inaccessible(cs)) then
-        exit (raise_c2_exception_v(cs))
-      else if (~(cs_val.tag)) then
-        exit (raise_c2_exception(CapEx_TagViolation, cs))
-      else if ((cs_perms & rt_perms) != rt_perms) then
-        exit (raise_c2_exception(CapEx_UserDefViolation, cs))
-      (* END_CCheckPerm *)
-    }
+{
+  (* START_CCheckPerm *)
+  checkCP2usable();
+  cs_val := readCapReg(cs);
+  cs_perms := capPermsToVec(cs_val);
+  rt_perms := (rGPR(rt))[30..0];
+  if (register_inaccessible(cs)) then
+    exit (raise_c2_exception_v(cs))
+  else if (~(cs_val.tag)) then
+    exit (raise_c2_exception(CapEx_TagViolation, cs))
+  else if ((cs_perms & rt_perms) != rt_perms) then
+    exit (raise_c2_exception(CapEx_UserDefViolation, cs))
+  (* END_CCheckPerm *)
+}
 
 union ast member (regno, regno) CCheckType
 function clause decode (0b010010 : 0b01011 : (regno) cs : (regno) cb : 0b00000 : 0b000: 0b001) = Some(CCheckType(cs, cb))
@@ -546,12 +544,12 @@ function clause execute (CCall(cs, cb)) =
 union ast member unit CReturn
 function clause decode (0b010010 : 0b00110 : 0b000000000000000000000) = Some(CReturn)
 function clause execute (CReturn) =
-    {
-      (* START_CReturn *)
-      checkCP2usable();
-      exit (raise_c2_exception_noreg(CapEx_ReturnTrap))
-      (* END_CReturn *)
-    }
+{
+  (* START_CReturn *)
+  checkCP2usable();
+  exit (raise_c2_exception_noreg(CapEx_ReturnTrap))
+  (* END_CReturn *)
+}
 
 union ast member (regno, bit[16], bool) CBX
 function clause decode (0b010010 : 0b01001 : (regno) cb : (bit[16]) imm) = Some(CBX(cb, imm, true)) (* CBTU *)
@@ -625,50 +623,50 @@ function clause decode (0b010010 : 0b10000 : (regno) rd : (regno) cb : 0b0000000
 function clause decode (0b010010 : 0b10000 : (regno) rd : (regno) cb : 0b00000001 : 0b0 : 0b11) = Some(CLoad(rd, cb, 0b00000, 0b00000000, false, D, true)) (* CLLD  *)
 
 function clause execute (CLoad(rd, cb, rt, offset, signext, width, linked)) =
-  {
-    (* START_CLoad *)
-    checkCP2usable();
-    cb_val := readCapReg(cb);
-    if (register_inaccessible(cb)) then
-      exit (raise_c2_exception_v(cb))
-    else if (~(cb_val.tag)) then
-      exit (raise_c2_exception(CapEx_TagViolation, cb))
-    else if (cb_val.sealed) then
-      exit (raise_c2_exception(CapEx_SealViolation, cb))
-    else if (~(cb_val.permit_load)) then
-      exit (raise_c2_exception(CapEx_PermitLoadViolation, cb))
-    else
-      {
-        size   := wordWidthBytes(width);
-        cursor := getCapCursor(cb_val);
-        vAddr  := cursor + unsigned(rGPR(rt)) + (size*signed(offset));
-        vAddr64:= (bit[64]) vAddr;
-        if ((vAddr + size) > ((nat) (cb_val.base) + ((nat) (cb_val.length)))) then
-          exit (raise_c2_exception(CapEx_LengthViolation, cb))
-        else if (vAddr < ((nat) (cb_val.base))) then
-          exit (raise_c2_exception(CapEx_LengthViolation, cb))
-        else if ~(isAddressAligned(vAddr64, width)) then
-          exit (SignalExceptionBadAddr(AdEL, vAddr64))
-        else
-          {
-            pAddr      := (TLBTranslate(vAddr64, LoadData));
-            widthBytes := wordWidthBytes(width);
-            memResult  := if (linked) then
-                {
-                  CP0LLBit  := 0b1;
-                  CP0LLAddr := pAddr;
-                  MEMr_reserve(pAddr, widthBytes);
-                }
-              else
-                MEMr(pAddr, widthBytes);
-            if (signext) then
-              wGPR(rd) := EXTS(memResult)
+{
+  (* START_CLoad *)
+  checkCP2usable();
+  cb_val := readCapReg(cb);
+  if (register_inaccessible(cb)) then
+    exit (raise_c2_exception_v(cb))
+  else if (~(cb_val.tag)) then
+    exit (raise_c2_exception(CapEx_TagViolation, cb))
+  else if (cb_val.sealed) then
+    exit (raise_c2_exception(CapEx_SealViolation, cb))
+  else if (~(cb_val.permit_load)) then
+    exit (raise_c2_exception(CapEx_PermitLoadViolation, cb))
+  else
+    {
+      size   := wordWidthBytes(width);
+      cursor := getCapCursor(cb_val);
+      vAddr  := cursor + unsigned(rGPR(rt)) + (size*signed(offset));
+      vAddr64:= (bit[64]) vAddr;
+      if ((vAddr + size) > ((nat) (cb_val.base) + ((nat) (cb_val.length)))) then
+        exit (raise_c2_exception(CapEx_LengthViolation, cb))
+      else if (vAddr < ((nat) (cb_val.base))) then
+        exit (raise_c2_exception(CapEx_LengthViolation, cb))
+      else if ~(isAddressAligned(vAddr64, width)) then
+        exit (SignalExceptionBadAddr(AdEL, vAddr64))
+      else
+        {
+          pAddr      := (TLBTranslate(vAddr64, LoadData));
+          widthBytes := wordWidthBytes(width);
+          memResult  := if (linked) then
+              {
+                CP0LLBit  := 0b1;
+                CP0LLAddr := pAddr;
+                MEMr_reserve(pAddr, widthBytes);
+              }
             else
-              wGPR(rd) := EXTZ(memResult)
-          }
-      }
-    (* END_CLoad *)
-  }
+              MEMr(pAddr, widthBytes);
+          if (signext) then
+            wGPR(rd) := EXTS(memResult)
+          else
+            wGPR(rd) := EXTZ(memResult)
+        }
+    }
+  (* END_CLoad *)
+}
 
 union ast member (regno, regno, regno, regno, bit[8], WordType, bool) CStore
 function clause decode (0b111010 : (regno) rs : (regno) cb: (regno) rt : (bit[8]) offset : 0b0 : 0b00) = Some(CStore(rs, cb, rt, 0b00000, offset, B, false)) (* CSB *)
@@ -682,160 +680,160 @@ function clause decode (0b010010 : 0b10000 : (regno) rs : (regno) cb : (regno) r
 function clause decode (0b010010 : 0b10000 : (regno) rs : (regno) cb : (regno) rd : 0b0000 : 0b11) = Some(CStore(rs, cb, 0b00000, rd, 0b00000000, D, true)) (* CSCD *)
 
 function clause execute (CStore(rs, cb, rt, rd, offset, width, conditional)) =
-  {
-    (* START_CStore *)
-    checkCP2usable();
-    cb_val := readCapReg(cb);
-    if (register_inaccessible(cb)) then
-      exit (raise_c2_exception_v(cb))
-    else if (~(cb_val.tag)) then
-      exit (raise_c2_exception(CapEx_TagViolation, cb))
-    else if (cb_val.sealed) then
-      exit (raise_c2_exception(CapEx_SealViolation, cb))
-    else if (~(cb_val.permit_store)) then
-      exit (raise_c2_exception(CapEx_PermitStoreViolation, cb))
-    else
-      {
-        size   := wordWidthBytes(width);
-        cursor := getCapCursor(cb_val);
-        vAddr  := cursor + unsigned(rGPR(rt)) + (size * signed(offset));
-        vAddr64:= (bit[64]) vAddr;
-        if ((vAddr + size) > ((nat) (cb_val.base) + ((nat) (cb_val.length)))) then
-          exit (raise_c2_exception(CapEx_LengthViolation, cb))
-        else if (vAddr < ((nat) (cb_val.base))) then
-          exit (raise_c2_exception(CapEx_LengthViolation, cb))
-        else if ~(isAddressAligned(vAddr64, width)) then
-          exit (SignalExceptionBadAddr(AdES, vAddr64))
-        else
-          {
-            pAddr  := (TLBTranslate(vAddr64, StoreData));
-            rs_val := rGPR(rs);
-            if (conditional) then
-              {
-                success := if (CP0LLBit[0]) then
-                    switch(width)
-                      {
-                        case B -> MEMw_conditional_wrapper(pAddr, 1, rs_val[7..0])
-                        case H -> MEMw_conditional_wrapper(pAddr, 2, rs_val[15..0])
-                        case W -> MEMw_conditional_wrapper(pAddr, 4, rs_val[31..0])
-                        case D -> MEMw_conditional_wrapper(pAddr, 8, rs_val)
-                      }
-                  else
-                    false;
-                wGPR(rd) := EXTZ([success]);
-              }
-              else
-            switch(width)
-              {
-                case B -> MEMw_wrapper(pAddr, 1) := rs_val[7..0]
-                case H -> MEMw_wrapper(pAddr, 2) := rs_val[15..0]
-                case W -> MEMw_wrapper(pAddr, 4) := rs_val[31..0]
-                case D -> MEMw_wrapper(pAddr, 8) := rs_val
-              }
-          }
-      }
-    (* END_CStore *)
-  }
+{
+  (* START_CStore *)
+  checkCP2usable();
+  cb_val := readCapReg(cb);
+  if (register_inaccessible(cb)) then
+    exit (raise_c2_exception_v(cb))
+  else if (~(cb_val.tag)) then
+    exit (raise_c2_exception(CapEx_TagViolation, cb))
+  else if (cb_val.sealed) then
+    exit (raise_c2_exception(CapEx_SealViolation, cb))
+  else if (~(cb_val.permit_store)) then
+    exit (raise_c2_exception(CapEx_PermitStoreViolation, cb))
+  else
+    {
+      size   := wordWidthBytes(width);
+      cursor := getCapCursor(cb_val);
+      vAddr  := cursor + unsigned(rGPR(rt)) + (size * signed(offset));
+      vAddr64:= (bit[64]) vAddr;
+      if ((vAddr + size) > ((nat) (cb_val.base) + ((nat) (cb_val.length)))) then
+        exit (raise_c2_exception(CapEx_LengthViolation, cb))
+      else if (vAddr < ((nat) (cb_val.base))) then
+        exit (raise_c2_exception(CapEx_LengthViolation, cb))
+      else if ~(isAddressAligned(vAddr64, width)) then
+        exit (SignalExceptionBadAddr(AdES, vAddr64))
+      else
+        {
+          pAddr  := (TLBTranslate(vAddr64, StoreData));
+          rs_val := rGPR(rs);
+          if (conditional) then
+            {
+              success := if (CP0LLBit[0]) then
+                  switch(width)
+                    {
+                      case B -> MEMw_conditional_wrapper(pAddr, 1, rs_val[7..0])
+                      case H -> MEMw_conditional_wrapper(pAddr, 2, rs_val[15..0])
+                      case W -> MEMw_conditional_wrapper(pAddr, 4, rs_val[31..0])
+                      case D -> MEMw_conditional_wrapper(pAddr, 8, rs_val)
+                    }
+                else
+                  false;
+              wGPR(rd) := EXTZ([success]);
+            }
+            else
+          switch(width)
+            {
+              case B -> MEMw_wrapper(pAddr, 1) := rs_val[7..0]
+              case H -> MEMw_wrapper(pAddr, 2) := rs_val[15..0]
+              case W -> MEMw_wrapper(pAddr, 4) := rs_val[31..0]
+              case D -> MEMw_wrapper(pAddr, 8) := rs_val
+            }
+        }
+    }
+  (* END_CStore *)
+}
 
 union ast member (regno, regno, regno, regno, bit[11], bool) CSC
 function clause decode (0b111110 : (regno) cs : (regno) cb: (regno) rt : (bit[11]) offset) = Some(CSC(cs, cb, rt, 0b00000, offset, false))
 function clause decode (0b010010 : 0b10000 : (regno) cs : (regno) cb: (regno) rd : 0b00 : 0b0111) = Some(CSC(cs, cb, 0b00000, rd, 0b00000000000, true))
 function clause execute (CSC(cs, cb, rt, rd, offset, conditional)) =
-  {
-    (* START_CSC *)
-    checkCP2usable();
-    cs_val := readCapReg(cs);
-    cb_val := readCapReg(cb);
-    if (register_inaccessible(cs)) then
-      exit (raise_c2_exception_v(cs))
-    else if (register_inaccessible(cb)) then
-      exit (raise_c2_exception_v(cb))
-    else if (~(cb_val.tag)) then
-      exit (raise_c2_exception(CapEx_TagViolation, cb))
-    else if (cb_val.sealed) then
-      exit (raise_c2_exception(CapEx_SealViolation, cb))
-    else if (~(cb_val.permit_store_cap)) then
-      exit (raise_c2_exception(CapEx_PermitStoreCapViolation, cb))
-    else if ((~(cb_val.permit_store_local_cap)) & (cs_val.tag) & ~(cs_val.global)) then
-      exit (raise_c2_exception(CapEx_PermitStoreLocalCapViolation, cb))
-    else
-      {
-        cursor := getCapCursor(cb_val);
-        vAddr  := cursor + unsigned(rGPR(rt)) + (16 * signed(offset));
-        vAddr64:= (bit[64]) vAddr;
-        if ((vAddr + cap_size) > ((nat) (cb_val.base) + ((nat) (cb_val.length)))) then
-          exit (raise_c2_exception(CapEx_LengthViolation, cb))
-        else if (vAddr < ((nat) (cb_val.base))) then
-          exit (raise_c2_exception(CapEx_LengthViolation, cb))
-        else if (vAddr64[4..0] != 0b00000) then
-          exit (SignalExceptionBadAddr(AdES, vAddr64))
-        else
-          {
-            let (pAddr, noStoreCap)  = (TLBTranslateC(vAddr64, StoreData)) in
-            if (cs_val.tag & noStoreCap) then
-              exit (raise_c2_exception(CapEx_TLBNoStoreCap, cs))
-            else if (conditional) then
-              {
-                success := if (CP0LLBit[0]) then
-                    MEMw_tagged_conditional(pAddr, cs_val.tag, capStructToMemBits(cs_val))
-                  else
-                    false;
-                wGPR(rd) := EXTZ([success]);
-              }
-            else
-              MEMw_tagged(pAddr, cs_val.tag, capStructToMemBits(cs_val));
-          }
-      }
-    (* END_CSC *)
-  }
+{
+  (* START_CSC *)
+  checkCP2usable();
+  cs_val := readCapReg(cs);
+  cb_val := readCapReg(cb);
+  if (register_inaccessible(cs)) then
+    exit (raise_c2_exception_v(cs))
+  else if (register_inaccessible(cb)) then
+    exit (raise_c2_exception_v(cb))
+  else if (~(cb_val.tag)) then
+    exit (raise_c2_exception(CapEx_TagViolation, cb))
+  else if (cb_val.sealed) then
+    exit (raise_c2_exception(CapEx_SealViolation, cb))
+  else if (~(cb_val.permit_store_cap)) then
+    exit (raise_c2_exception(CapEx_PermitStoreCapViolation, cb))
+  else if ((~(cb_val.permit_store_local_cap)) & (cs_val.tag) & ~(cs_val.global)) then
+    exit (raise_c2_exception(CapEx_PermitStoreLocalCapViolation, cb))
+  else
+    {
+      cursor := getCapCursor(cb_val);
+      vAddr  := cursor + unsigned(rGPR(rt)) + (16 * signed(offset));
+      vAddr64:= (bit[64]) vAddr;
+      if ((vAddr + cap_size) > ((nat) (cb_val.base) + ((nat) (cb_val.length)))) then
+        exit (raise_c2_exception(CapEx_LengthViolation, cb))
+      else if (vAddr < ((nat) (cb_val.base))) then
+        exit (raise_c2_exception(CapEx_LengthViolation, cb))
+      else if (vAddr64[4..0] != 0b00000) then
+        exit (SignalExceptionBadAddr(AdES, vAddr64))
+      else
+        {
+          let (pAddr, noStoreCap)  = (TLBTranslateC(vAddr64, StoreData)) in
+          if (cs_val.tag & noStoreCap) then
+            exit (raise_c2_exception(CapEx_TLBNoStoreCap, cs))
+          else if (conditional) then
+            {
+              success := if (CP0LLBit[0]) then
+                  MEMw_tagged_conditional(pAddr, cs_val.tag, capStructToMemBits(cs_val))
+                else
+                  false;
+              wGPR(rd) := EXTZ([success]);
+            }
+          else
+            MEMw_tagged(pAddr, cs_val.tag, capStructToMemBits(cs_val));
+        }
+    }
+  (* END_CSC *)
+}
 
 union ast member (regno, regno, regno, bit[11], bool) CLC
 function clause decode (0b110110 : (regno) cd : (regno) cb: (regno) rt : (bit[11]) offset) = Some(CLC(cd, cb, rt, offset, false))
 function clause decode (0b010010 : 0b10000 : (regno) cd : (regno) cb: 0b0000000 : 0b1111) = Some(CLC(cd, cb, 0b00000, 0b00000000000, true))
 function clause execute (CLC(cd, cb, rt, offset, linked)) =  
-  {
-    (* START_CLC *)
-    checkCP2usable();
-    cb_val := readCapReg(cb);
-    if (register_inaccessible(cd)) then
-      exit (raise_c2_exception_v(cd))
-    else if (register_inaccessible(cb)) then
-      exit (raise_c2_exception_v(cb))
-    else if (~(cb_val.tag)) then
-      exit (raise_c2_exception(CapEx_TagViolation, cb))
-    else if (cb_val.sealed) then
-      exit (raise_c2_exception(CapEx_SealViolation, cb))
-    else if (~(cb_val.permit_load_cap)) then
-      exit (raise_c2_exception(CapEx_PermitLoadCapViolation, cb))
-    else
-      {
-        cursor := getCapCursor(cb_val);
-        vAddr  := cursor + unsigned(rGPR(rt)) + (16*signed(offset));
-        vAddr64:= (bit[64]) vAddr;
-        if ((vAddr + cap_size) > ((nat) (cb_val.base) + ((nat) (cb_val.length)))) then
-          exit (raise_c2_exception(CapEx_LengthViolation, cb))
-        else if (vAddr < ((nat) (cb_val.base))) then
-          exit (raise_c2_exception(CapEx_LengthViolation, cb))
-        else if (vAddr64[4..0] != 0b00000) then
-          exit (SignalExceptionBadAddr(AdEL, vAddr64))
-        else
-          {
-            let (pAddr, suppressTag) = (TLBTranslateC(vAddr64, LoadData)) in
-            let (tag, mem) = (if (linked) 
-              then
-                {
-                  CP0LLBit  := 0b1;
-                  CP0LLAddr := pAddr;
-                  MEMr_tagged_reserve(pAddr);
-                }
-              else 
-                (MEMr_tagged(pAddr)))
-            in
-            (CapRegs[cd]) := memBitsToCapBits(tag & (~(suppressTag)), mem);
-          }
-      }
-    (* END_CLC *)
-  }
+{
+  (* START_CLC *)
+  checkCP2usable();
+  cb_val := readCapReg(cb);
+  if (register_inaccessible(cd)) then
+    exit (raise_c2_exception_v(cd))
+  else if (register_inaccessible(cb)) then
+    exit (raise_c2_exception_v(cb))
+  else if (~(cb_val.tag)) then
+    exit (raise_c2_exception(CapEx_TagViolation, cb))
+  else if (cb_val.sealed) then
+    exit (raise_c2_exception(CapEx_SealViolation, cb))
+  else if (~(cb_val.permit_load_cap)) then
+    exit (raise_c2_exception(CapEx_PermitLoadCapViolation, cb))
+  else
+    {
+      cursor := getCapCursor(cb_val);
+      vAddr  := cursor + unsigned(rGPR(rt)) + (16*signed(offset));
+      vAddr64:= (bit[64]) vAddr;
+      if ((vAddr + cap_size) > ((nat) (cb_val.base) + ((nat) (cb_val.length)))) then
+        exit (raise_c2_exception(CapEx_LengthViolation, cb))
+      else if (vAddr < ((nat) (cb_val.base))) then
+        exit (raise_c2_exception(CapEx_LengthViolation, cb))
+      else if (vAddr64[4..0] != 0b00000) then
+        exit (SignalExceptionBadAddr(AdEL, vAddr64))
+      else
+        {
+          let (pAddr, suppressTag) = (TLBTranslateC(vAddr64, LoadData)) in
+          let (tag, mem) = (if (linked) 
+            then
+              {
+                CP0LLBit  := 0b1;
+                CP0LLAddr := pAddr;
+                MEMr_tagged_reserve(pAddr);
+              }
+            else 
+              (MEMr_tagged(pAddr)))
+          in
+          (CapRegs[cd]) := memBitsToCapBits(tag & (~(suppressTag)), mem);
+        }
+    }
+  (* END_CLC *)
+}
 
 union ast member (regno) C2Dump
 function clause decode (0b010010 : 0b00100 : (regno) rt : 0x0006) = Some(C2Dump(rt))