From eb444afd9a6b9abb9d9ee732ca3dc3954eaf4a0e Mon Sep 17 00:00:00 2001
From: Samuel Gruetter <saemi472@gmail.com>
Date: Thu, 3 Mar 2022 23:00:39 -0500
Subject: [PATCH] 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
---
 src/riscv/Platform/MaterializeRiscvProgram.v | 7 +++++++
 src/riscv/Platform/MetricMinimalNoMul.v      | 1 +
 src/riscv/Platform/MinimalCSRs.v             | 2 ++
 src/riscv/Platform/MinimalMMIO.v             | 2 ++
 src/riscv/Platform/MinimalNoMul.v            | 2 ++
 5 files changed, 14 insertions(+)

diff --git a/src/riscv/Platform/MaterializeRiscvProgram.v b/src/riscv/Platform/MaterializeRiscvProgram.v
index b3b404c..b8a522f 100644
--- 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
index bd58242..d22edd8 100644
--- 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
index ad25851..7163209 100644
--- 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
index 3a76445..dad0916 100644
--- 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
index 468b167..87a9c02 100644
--- 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 _