Add and use execute_branch and execute_branch_pcc functions to align code with existing MIPS and CHERI specs.

4 files changed, 25 insertions, 24 deletions

diff --git a/cheri/cheri_insts.sail b/cheri/cheri_insts.sail
index 6e2b2282..c832d70c 100644
--- a/cheri/cheri_insts.sail
+++ b/cheri/cheri_insts.sail
@@ -1053,13 +1053,11 @@ function clause execute (CCall(cs, cb, 0b00000000001)) = /* selector=1 */
   else if (cs_cursor >= getCapTop(cs_val)) then
     raise_c2_exception(CapEx_LengthViolation, cs)
   else
-    let csUnsealed = capStructToCapReg({cs_val with
+    {
+      execute_branch_pcc({cs_val with
         sealed=false,
         otype=zeros()
-    }) in {
-      delayedPC = to_bits(64, getCapOffset(cs_val));
-      delayedPCC = csUnsealed;
-      branchPending = 0b1;
+      });
       inCCallDelay  = 0b1;
       C26 = capStructToCapReg({cb_val with
         sealed=false,
@@ -1088,8 +1086,7 @@ function clause execute (CBX(cb, imm, notset)) =
   else if (((readCapReg(cb)).tag) ^ notset) then
     {
       let offset : bits(64) = (sign_extend(imm @ 0b00) + 4) in
-      delayedPC     = PC + offset;
-      branchPending = 0b1;
+      execute_branch(PC + offset);
     }
   /* END_CBtag */
 }
@@ -1104,8 +1101,7 @@ function clause execute (CBZ(cb, imm, notzero)) =
   else if (((readCapReg(cb)) == null_cap) ^ notzero) then
     {
       let offset : bits(64) = (sign_extend(imm @ 0b00) + 4) in
-      delayedPC     = PC + offset;
-      branchPending = 0b1;
+      execute_branch(PC + offset);
     }
   /* END_CBz */
 }
@@ -1144,9 +1140,7 @@ function clause execute(CJALR(cd, cb, link)) =
             writeCapReg(cd, linkCap)
         else
             assert(false, "");
-      delayedPC =  to_bits(64, getCapOffset(cb_val));
-      delayedPCC = capStructToCapReg(cb_val);
-      branchPending = 0b1;
+      execute_branch_pcc(cb_val);
     }
   /* END_CJALR */
 }
diff --git a/cheri/cheri_prelude_common.sail b/cheri/cheri_prelude_common.sail
index 0072ded7..09e07f70 100644
--- a/cheri/cheri_prelude_common.sail
+++ b/cheri/cheri_prelude_common.sail
@@ -185,6 +185,13 @@ bitfield CapCauseReg : bits(16) = {
 
 register CapCause : CapCauseReg
 
+val execute_branch_pcc : CapStruct -> unit effect {wreg}
+function execute_branch_pcc(newPCC) = {
+  delayedPC = to_bits(64, getCapOffset(newPCC));
+  delayedPCC = capStructToCapReg(newPCC);
+  branchPending = 0b1;
+}
+
 function SignalException (ex) = 
   {
     if (not (CP0Status.EXL())) then {
diff --git a/mips/mips_insts.sail b/mips/mips_insts.sail
index 028665c9..885608d1 100644
--- a/mips/mips_insts.sail
+++ b/mips/mips_insts.sail
@@ -884,8 +884,7 @@ function clause decode (0b000010 @ offset : bits(26)) =
   Some(J(offset))
 function clause execute (J(offset)) =
   {
-    delayedPC     = (PC + 4)[63..28] @ offset @ 0b00;
-    branchPending = 0b1
+    execute_branch((PC + 4)[63..28] @ offset @ 0b00);
   }
 
 /* JAL    - jump and link */
@@ -894,8 +893,7 @@ function clause decode (0b000011 @ offset : bits(26)) =
   Some(JAL(offset))
 function clause execute (JAL(offset)) =
   {
-    delayedPC     = (PC + 4)[63..28] @ offset @ 0b00;
-    branchPending = 0b1;
+    execute_branch((PC + 4)[63..28] @ offset @ 0b00);
     wGPR(0b11111) = PC + 8;
   }
 
@@ -905,8 +903,7 @@ function clause decode (0b000000 @ rs : regno @ 0b00000 @ 0b00000 @ hint : regno
   Some(JR(rs)) /* hint is ignored */
 function clause execute (JR(rs)) =
   {
-    delayedPC     = rGPR(rs);
-    branchPending = 0b1;
+    execute_branch(rGPR(rs));
   }
 
 /* JALR -- jump via register with link */
@@ -915,8 +912,7 @@ function clause decode (0b000000 @ rs : regno @ 0b00000 @ rd : regno @ hint : re
   Some(JALR(rs, rd)) /* hint is ignored */
 function clause execute (JALR(rs, rd)) =
   {
-    delayedPC     = rGPR(rs);
-    branchPending = 0b1;
+    execute_branch(rGPR(rs));
     wGPR(rd)      = PC + 8;
   }
 
@@ -939,8 +935,7 @@ function clause execute (BEQ(rs, rd, imm, ne, likely)) =
     if ((rGPR(rs) == rGPR(rd)) ^ ne) then
       {
         let offset : bits(64) = (sign_extend(imm @ 0b00) + 4) in
-        delayedPC     = PC + offset;
-        branchPending = 0b1;
+        execute_branch(PC + offset);
       }
     else
       {
@@ -996,8 +991,7 @@ function clause execute (BCMPZ(rs, imm, cmp, link, likely)) =
     if (condition) then
       {
         let offset : bits(64) = (sign_extend(imm @ 0b00) + 4) in
-        delayedPC     =  PC + offset;
-        branchPending = 0b1;
+        execute_branch(PC + offset);
       }
     else if (likely) then
       {
diff --git a/mips/mips_prelude.sail b/mips/mips_prelude.sail
index b672d993..3c3c45f4 100644
--- a/mips/mips_prelude.sail
+++ b/mips/mips_prelude.sail
@@ -289,6 +289,12 @@ register branchPending : bits(1)      /* Set by branch instructions to implement
 register inBranchDelay : bits(1)      /* Needs to be set by outside world when in branch delay slot */
 register delayedPC : bits(64)          /* Set by branch instructions to implement branch delay */
 
+val execute_branch : bits(64) -> unit effect {wreg}
+function execute_branch(pc) = {
+  delayedPC = pc;
+  branchPending = 0b1;
+}
+
 /* General purpose registers */