add StartCycle to free monad, so that we can set nextPc

at beginning of cycle and don't need to thread it through an invariant from the previous cycle
mit-plv · Mar 4, 2022 · eb444af · eb444af
1 parent 8d9b63f
commit eb444af
Show file tree

Hide file tree

Showing 5 changed files with 14 additions and 0 deletions.
diff --git a/src/riscv/Platform/MaterializeRiscvProgram.v b/src/riscv/Platform/MaterializeRiscvProgram.v
@@ -29,6 +29,7 @@ Section Riscv.
   | Fence (_ : MachineInt) (_ : MachineInt)
   | GetPC
   | SetPC (_ : word)
+  | StartCycle
   | EndCycleNormal
   | EndCycleEarly (_ : Type)
   .
@@ -53,6 +54,7 @@ Section Riscv.
     | Fence _ _ => unit
     | GetPC => word
     | SetPC _ => unit
+    | StartCycle => unit
     | EndCycleNormal => unit
     | EndCycleEarly T => T
     end.
@@ -82,4 +84,9 @@ Section Riscv.
     endCycleEarly A := act (EndCycleEarly A) ret;
   |}.
 
+  (* Not (yet) in Riscv monad, but added here because it's useful to initialize
+     nextPc to pc+4 at the beginning of each cycle instead of having to maintain
+     a nextPc=pc+4 invariant everywhere *)
+  Definition startCycle: FreeMonad.free riscv_primitive primitive_result unit :=
+    FreeMonad.free.act StartCycle FreeMonad.free.ret.
 End Riscv.
diff --git a/src/riscv/Platform/MetricMinimalNoMul.v b/src/riscv/Platform/MetricMinimalNoMul.v
@@ -53,6 +53,7 @@ Section Riscv.
     | Fence a b => id
     | GetPC => id
     | SetPC a => addMetricJumps 1
+    | StartCycle => id
     | EndCycleNormal => addMetricInstructions 1
     | EndCycleEarly A => addMetricInstructions 1
     end.

diff --git a/src/riscv/Platform/MinimalCSRs.v b/src/riscv/Platform/MinimalCSRs.v
@@ -78,6 +78,8 @@ Section Riscv.
     | StoreHalf ctxid a v => fun postF postA => store 2 ctxid a v mach (postF tt)
     | StoreWord ctxid a v => fun postF postA => store 4 ctxid a v mach (postF tt)
     | StoreDouble ctxid a v => fun postF postA => store 8 ctxid a v mach (postF tt)
+    | StartCycle => fun postF postA =>
+        postF tt { mach with nextPc := word.add mach.(pc) (word.of_Z 4) }
     | EndCycleNormal => fun postF postA => postF tt (updatePc mach)
     | EndCycleEarly _ => fun postF postA => postA (updatePc mach) (* ignores postF containing the continuation *)
     | GetCSRField f => fun postF postA =>

diff --git a/src/riscv/Platform/MinimalMMIO.v b/src/riscv/Platform/MinimalMMIO.v
@@ -110,6 +110,8 @@ Section Riscv.
     | StoreHalf ctxid a v => fun postF postA => store 2 ctxid a v mach (postF tt)
     | StoreWord ctxid a v => fun postF postA => store 4 ctxid a v mach (postF tt)
     | StoreDouble ctxid a v => fun postF postA => store 8 ctxid a v mach (postF tt)
+    | StartCycle => fun postF postA =>
+        postF tt (withNextPc (word.add mach.(getPc) (word.of_Z 4)) mach)
     | EndCycleNormal => fun postF postA => postF tt (updatePc mach)
     | EndCycleEarly _ => fun postF postA => postA (updatePc mach) (* ignores postF containing the continuation *)
     | MakeReservation _

diff --git a/src/riscv/Platform/MinimalNoMul.v b/src/riscv/Platform/MinimalNoMul.v
@@ -76,6 +76,8 @@ Section Riscv.
     | StoreHalf ctxid a v => fun postF postA => store 2 ctxid a v mach (postF tt)
     | StoreWord ctxid a v => fun postF postA => store 4 ctxid a v mach (postF tt)
     | StoreDouble ctxid a v => fun postF postA => store 8 ctxid a v mach (postF tt)
+    | StartCycle => fun postF postA =>
+        postF tt (withNextPc (word.add mach.(getPc) (word.of_Z 4)) mach)
     | EndCycleNormal => fun postF postA => postF tt (updatePc mach)
     | EndCycleEarly _ => fun postF postA => postA (updatePc mach) (* ignores postF containing the continuation *)
     | MakeReservation _