Use a branchPC function for branch instrs rather than two separate rules

runtimeverification · Jul 31, 2024 · 7be66bf · 7be66bf
1 parent 8d20701
commit 7be66bf
Showing 1 changed file with 10 additions and 36 deletions.
diff --git a/src/kriscv/kdist/riscv-semantics/riscv.md b/src/kriscv/kdist/riscv-semantics/riscv.md
@@ -274,61 +274,35 @@ The following instructions behave analogously to their `I`-suffixed counterparts
 ```
 `BEQ` increments `PC` by `OFFSET` so long as the values in registers `RS1` and `RS2` are equal. Otherwise, `PC` is incremented by `4`.
 ```k
+  syntax Word ::= branchPC(oldPC: Word, offset: Int, branchCond: Bool) [function, total]
+  rule branchPC(PC,  OFFSET, COND) => PC +Word chop(OFFSET) requires COND
+  rule branchPC(PC, _OFFSET, COND) => PC +Word W(4)         requires notBool COND
+
   rule <instrs> BEQ RS1 , RS2 , OFFSET => .K ...</instrs>
        <regs> REGS </regs>
-       <pc> PC => PC +Word chop(OFFSET) </pc>
-       requires readReg(REGS, RS1) ==Word readReg(REGS, RS2)
-
-  rule <instrs> BEQ _RS1 , _RS2 , _OFFSET => .K ...</instrs>
-       <pc> PC => PC +Word W(4) </pc>
-       [owise]
+       <pc> PC => branchPC(PC, OFFSET, readReg(REGS, RS1) ==Word readReg(REGS, RS2)) </pc>
 ```
 The remaining branch instructions proceed analogously, but performing different comparisons between `RS1` and `RS2`.
 ```k
   rule <instrs> BNE RS1 , RS2 , OFFSET => .K ...</instrs>
        <regs> REGS </regs>
-       <pc> PC => PC +Word chop(OFFSET) </pc>
-       requires readReg(REGS, RS1) =/=Word readReg(REGS, RS2)
-
-  rule <instrs> BNE _RS1 , _RS2 , _OFFSET => .K ...</instrs>
-       <pc> PC => PC +Word W(4) </pc>
-       [owise]
+       <pc> PC => branchPC(PC, OFFSET, readReg(REGS, RS1) =/=Word readReg(REGS, RS2)) </pc>
 
   rule <instrs> BLT RS1 , RS2 , OFFSET => .K ...</instrs>
        <regs> REGS </regs>
-       <pc> PC => PC +Word chop(OFFSET) </pc>
-       requires readReg(REGS, RS1) <sWord readReg(REGS, RS2)
-
-  rule <instrs> BLT _RS1 , _RS2 , _OFFSET => .K ...</instrs>
-       <pc> PC => PC +Word W(4) </pc>
-       [owise]
+       <pc> PC => branchPC(PC, OFFSET, readReg(REGS, RS1) <sWord readReg(REGS, RS2)) </pc>
 
   rule <instrs> BGE RS1 , RS2 , OFFSET => .K ...</instrs>
        <regs> REGS </regs>
-       <pc> PC => PC +Word chop(OFFSET) </pc>
-       requires readReg(REGS, RS1) >=sWord readReg(REGS, RS2)
-
-  rule <instrs> BGE _RS1 , _RS2 , _OFFSET => .K ...</instrs>
-       <pc> PC => PC +Word W(4) </pc>
-       [owise]
+       <pc> PC => branchPC(PC, OFFSET, readReg(REGS, RS1) >=sWord readReg(REGS, RS2)) </pc>
 
   rule <instrs> BLTU RS1 , RS2 , OFFSET => .K ...</instrs>
        <regs> REGS </regs>
-       <pc> PC => PC +Word chop(OFFSET) </pc>
-       requires readReg(REGS, RS1) <uWord readReg(REGS, RS2)
-
-  rule <instrs> BLTU _RS1 , _RS2 , _OFFSET => .K ...</instrs>
-       <pc> PC => PC +Word W(4) </pc>
-       [owise]
+       <pc> PC => branchPC(PC, OFFSET, readReg(REGS, RS1) <uWord readReg(REGS, RS2)) </pc>
 
   rule <instrs> BGEU RS1 , RS2 , OFFSET => .K ...</instrs>
        <regs> REGS </regs>
-       <pc> PC => PC +Word chop(OFFSET) </pc>
-       requires readReg(REGS, RS1) >=uWord readReg(REGS, RS2)
-
-  rule <instrs> BGEU _RS1 , _RS2 , _OFFSET => .K ...</instrs>
-       <pc> PC => PC +Word W(4) </pc>
-       [owise]
+       <pc> PC => branchPC(PC, OFFSET, readReg(REGS, RS1) >=uWord readReg(REGS, RS2)) </pc>
 ```
 `LB`, `LH`, and `LW` load `1`, `2`, and `4` bytes respectively from the memory address which is `OFFSET` greater than the value in register `RS1`, then sign extends the loaded bytes and places them in register `RD`.
 ```k