Add Makefile and marker comments in cheri sail file for extracting individual instructions to go in CHERI documentation.

2 files changed, 84 insertions, 1 deletions

diff --git a/cheri/Makefile b/cheri/Makefile
new file mode 100644
index 00000000..1c7c2304
--- /dev/null
+++ b/cheri/Makefile
@@ -0,0 +1,30 @@
+EXTRACT_INST=sed -n "/START_${1}\b/,/END_${1}\b/p" cheri_insts.sail | sed 's/^  //;1d;$$d' > inst_$1.sail
+
+extract: cheri_insts.sail
+	$(call EXTRACT_INST,CGetX)
+	$(call EXTRACT_INST,CGetPCC)
+	$(call EXTRACT_INST,CGetPCCSetOffset)
+	$(call EXTRACT_INST,CGetCause)
+	$(call EXTRACT_INST,CSetCause)
+	$(call EXTRACT_INST,CAndPerm)
+	$(call EXTRACT_INST,CToPtr)
+	$(call EXTRACT_INST,CSub)
+	$(call EXTRACT_INST,CPtrCmp)
+	$(call EXTRACT_INST,CIncOffset)
+	$(call EXTRACT_INST,CSetOffset)
+	$(call EXTRACT_INST,CSetBounds)
+	$(call EXTRACT_INST,CClearTag)
+	$(call EXTRACT_INST,CClearRegs)
+	$(call EXTRACT_INST,CFromPtr)
+	$(call EXTRACT_INST,CCheckPerm)
+	$(call EXTRACT_INST,CCheckType)
+	$(call EXTRACT_INST,CSeal)
+	$(call EXTRACT_INST,CUnseal)
+	$(call EXTRACT_INST,CCall)
+	$(call EXTRACT_INST,CReturn)
+	$(call EXTRACT_INST,CBx)
+	$(call EXTRACT_INST,CJALR)
+	$(call EXTRACT_INST,CLoad)
+	$(call EXTRACT_INST,CStore)
+	$(call EXTRACT_INST,CSC)
+	$(call EXTRACT_INST,CLC)                 
diff --git a/cheri/cheri_insts.sail b/cheri/cheri_insts.sail
index 132d7da3..215f0f19 100644
--- a/cheri/cheri_insts.sail
+++ b/cheri/cheri_insts.sail
@@ -46,6 +46,7 @@ function clause decode (0b010010 : 0b01101 : (regno) rd : (regno) cb : 0b0000000
 
 function clause execute (CGetX(op, rd, cb)) =
   {
+    (* START_CGetX *)
     checkCP2usable();
     if (register_inaccessible(cb)) then
       exit (raise_c2_exception_v(cb))
@@ -62,25 +63,28 @@ function clause execute (CGetX(op, rd, cb)) =
           case CGetUnsealed -> EXTZ([cbval.sealed])
         }
       }
+    (* 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 *)
     }
 
 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))
@@ -88,6 +92,7 @@ function clause execute (CGetPCCSetOffset(cd, rs)) =
         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 *)
@@ -96,17 +101,20 @@ 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 *)
     }
 
 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))
@@ -116,12 +124,14 @@ function clause execute (CSetCause((regno) 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))
 function clause execute(CAndPerm(cd, cb, rt)) = 
 {
+  (* START_CAndPerm *)
   checkCP2usable();
   cb_val := readCapReg(cb);
   rt_val := rGPR(rt);
@@ -154,12 +164,14 @@ function clause execute(CAndPerm(cd, cb, rt)) =
         global                     = (cb_val.global                     & (rt_val[0]));
       })
     }
+  (* END_CAndPerm *)
 }
 
 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 *)
   checkCP2usable();
   ct_val := readCapReg(ct);
   cb_val := readCapReg(cb);
@@ -176,12 +188,14 @@ function clause execute(CToPtr(rd, cb, ct)) =
         else
           (bit[64])(((nat)(cb_val.base)) + ((nat) (cb_val.offset)) - ((nat)(ct_val.base)))
     }
+  (* END_CToPtr *)
 }
 
 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 *)
   checkCP2usable();
   ct_val := readCapReg(ct);
   cb_val := readCapReg(cb);
@@ -193,6 +207,7 @@ function clause execute(CSub(rd, cb, ct)) =
     {
       wGPR(rd) := (bit[64])(getCapCursor(cb_val) - getCapCursor(ct_val))
     }
+  (* END_CSub *)
 }
 
 union ast member (regno, regno, regno, CPtrCmpOp) CPtrCmp
@@ -206,6 +221,7 @@ function clause decode (0b010010 : 0b01110 : (regno) rd : (regno) cb : (regno) c
 
 function clause execute(CPtrCmp(rd, cb, ct, op)) = 
 {
+  (* START_CPtrCMP *)
   checkCP2usable();
   if (register_inaccessible(cb)) then
     exit (raise_c2_exception_v(cb))
@@ -244,12 +260,14 @@ function clause execute(CPtrCmp(rd, cb, ct, op)) =
         case CEXEQ -> [cb_val == ct_val]
       })
     }
+    (* 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);
@@ -261,12 +279,14 @@ function clause execute (CIncOffset(cd, cb, rt)) =
         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);
@@ -278,12 +298,14 @@ function clause execute (CSetOffset(cd, cb, rt)) =
         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);
@@ -302,12 +324,14 @@ function clause execute (CSetBounds(cd, cb, rt)) =
         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))
@@ -318,6 +342,7 @@ function clause execute (CClearTag(cd, cb)) =
           cb_val := readCapReg(cb);
           writeCapReg(cd, {cb_val with tag = false});
         }
+      (* END_CClearTag *)
     }
 
 union ast member (ClearRegSet, bit[16]) ClearRegs
@@ -327,6 +352,7 @@ function clause decode (0b010010 : 0b01111 : 0b00010 : (bit[16]) imm) = Some(Cle
 function clause decode (0b010010 : 0b01111 : 0b00011 : (bit[16]) imm) = Some(ClearRegs(CHi, imm))  (* CClearHi *)
 function clause execute (ClearRegs(regset, mask)) =
 {
+  (* START_ClearRegs *)
   if ((regset == CLo) | (regset == CHi)) then
     checkCP2usable();
   if (regset == CHi) then
@@ -342,12 +368,14 @@ function clause execute (ClearRegs(regset, mask)) =
         case CLo  -> writeCapReg((bit[5]) i) := null_cap
         case CHi  -> writeCapReg((bit[5]) (i+16)) := null_cap
       }
+  (* END_ClearRegs *)
 }
 
 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);
@@ -363,12 +391,14 @@ function clause execute (CFromPtr(cd, cb, rt)) =
         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);
@@ -379,12 +409,14 @@ function clause execute (CCheckPerm(cs, rt)) =
         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))
 function clause execute (CCheckType(cs, cb)) =
 {
+  (* START_CCheckType *)
   checkCP2usable();
   cs_val := readCapReg(cs);
   cb_val := readCapReg(cb);
@@ -402,12 +434,14 @@ function clause execute (CCheckType(cs, cb)) =
     exit (raise_c2_exception(CapEx_SealViolation, cb))
   else if ((cs_val.otype) != (cb_val.otype)) then
     exit (raise_c2_exception(CapEx_TypeViolation, cs))
+  (* END_CCheckType *)
 }
 
 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 *)
   checkCP2usable();
   cs_val := readCapReg(cs);
   ct_val := readCapReg(ct);
@@ -434,12 +468,14 @@ function clause execute (CSeal(cd, cs, ct)) =
     exit (raise_c2_exception(CapEx_LengthViolation, ct))
   else
     writeCapReg(cd, {cs_val with sealed=true; otype=((bit[24])ct_cursor)})
+  (* END_CSeal *)
 }
 
 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 *)
   checkCP2usable();
   cs_val := readCapReg(cs);
   ct_val := readCapReg(ct);
@@ -470,12 +506,14 @@ function clause execute (CUnseal(cd, cs, ct)) =
       otype=0;
       global=(cs_val.global & ct_val.global)
     })
+  (* END_CUnseal *)
 }
 
 union ast member (regno, regno) CCall
 function clause decode (0b010010 : 0b00101 : (regno) cs : (regno) cb : (bit[11]) selector) = Some(CCall(cs, cb))
 function clause execute (CCall(cs, cb)) =
 {
+  (* START_CCall *)
   checkCP2usable();
   (* Partial implementation of CCall with checks in hardware, but raising a trap to perform trusted stack manipulation *)
   cs_val := readCapReg(cs);
@@ -502,14 +540,17 @@ function clause execute (CCall(cs, cb)) =
     exit (raise_c2_exception(CapEx_LengthViolation, cs))
   else
     exit (raise_c2_exception(CapEx_CallTrap, cs));
+  (* END_CCall *)
 }
 
 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 *)
     }
 
 union ast member (regno, bit[16], bool) CBX
@@ -518,6 +559,7 @@ function clause decode (0b010010 : 0b01010 : (regno) cb : (bit[16]) imm) = Some(
 
 function clause execute (CBX(cb, imm, invert)) =
 {
+  (* START_CBx *)
   checkCP2usable();
   if (register_inaccessible(cb)) then
     exit (raise_c2_exception_v(cb))
@@ -527,6 +569,7 @@ function clause execute (CBX(cb, imm, invert)) =
       delayedPC     := PC + offset;
       branchPending := 1;
     }
+  (* END_CBx *)
 }
 
 union ast member (regno, regno, bool) CJALR
@@ -534,6 +577,7 @@ function clause decode (0b010010 : 0b00111 : (regno) cd : (regno) cb : 0b00000 :
 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 *)
   checkCP2usable();
   cb_val := readCapReg(cb);
   if (link & register_inaccessible(cd)) then
@@ -560,6 +604,7 @@ function clause execute(CJALR(cd, cb, link)) =
       delayedPCC := capStructToBit257(cb_val);
       branchPending := 1;
     }
+  (* END_CJALR *)
 }
 
 union ast member (regno, regno, regno, bit[8], bool, WordType, bool) CLoad
@@ -581,6 +626,7 @@ function clause decode (0b010010 : 0b10000 : (regno) rd : (regno) cb : 0b0000000
 
 function clause execute (CLoad(rd, cb, rt, offset, signext, width, linked)) =
   {
+    (* START_CLoad *)
     checkCP2usable();
     cb_val := readCapReg(cb);
     if (register_inaccessible(cb)) then
@@ -621,6 +667,7 @@ function clause execute (CLoad(rd, cb, rt, offset, signext, width, linked)) =
               wGPR(rd) := EXTZ(memResult)
           }
       }
+    (* END_CLoad *)
   }
 
 union ast member (regno, regno, regno, regno, bit[8], WordType, bool) CStore
@@ -636,6 +683,7 @@ function clause decode (0b010010 : 0b10000 : (regno) rs : (regno) cb : (regno) r
 
 function clause execute (CStore(rs, cb, rt, rd, offset, width, conditional)) =
   {
+    (* START_CStore *)
     checkCP2usable();
     cb_val := readCapReg(cb);
     if (register_inaccessible(cb)) then
@@ -686,6 +734,7 @@ function clause execute (CStore(rs, cb, rt, rd, offset, width, conditional)) =
               }
           }
       }
+    (* END_CStore *)
   }
 
 union ast member (regno, regno, regno, regno, bit[11], bool) CSC
@@ -693,6 +742,7 @@ function clause decode (0b111110 : (regno) cs : (regno) cb: (regno) rt : (bit[11
 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);
@@ -736,6 +786,7 @@ function clause execute (CSC(cs, cb, rt, rd, offset, conditional)) =
               MEMw_tagged(pAddr, cs_val.tag, capStructToMemBits(cs_val));
           }
       }
+    (* END_CSC *)
   }
 
 union ast member (regno, regno, regno, bit[11], bool) CLC
@@ -743,6 +794,7 @@ function clause decode (0b110110 : (regno) cd : (regno) cb: (regno) rt : (bit[11
 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
@@ -782,6 +834,7 @@ function clause execute (CLC(cd, cb, rt, offset, linked)) =
             (CapRegs[cd]) := memBitsToCapBits(tag & (~(suppressTag)), mem);
           }
       }
+    (* END_CLC *)
   }
 
 union ast member (regno) C2Dump