From bfb7331e0d1df763e51c59016f9d42e1ff7f90c5 Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Fri, 2 Mar 2018 13:42:22 +0000
Subject: add a cp2_next_pc function to update cheri state in fde loop and a
 stub version for mips.

---
 cheri/cheri_prelude_common.sail | 9 +++++++++
 mips_new_tc/main.sail           | 3 ++-
 mips_new_tc/mips_prelude.sail   | 1 +
 mips_new_tc/mips_wrappers.sail  | 1 +
 4 files changed, 13 insertions(+), 1 deletion(-)

diff --git a/cheri/cheri_prelude_common.sail b/cheri/cheri_prelude_common.sail
index c11bfc8d..02a6d408 100644
--- a/cheri/cheri_prelude_common.sail
+++ b/cheri/cheri_prelude_common.sail
@@ -391,6 +391,15 @@ function init_cp2_state () = {
   }
 }
 
+function cp2_next_pc () = {
+  PCC = nextPCC;
+  if inBranchDelay then {
+    nextPCC = delayedPCC;
+  } else {
+    inCCallDelay = 0b0;
+  };
+}
+
 val capToString : CapStruct -> string
 function capToString cap =
          concat_str(" t:",
diff --git a/mips_new_tc/main.sail b/mips_new_tc/main.sail
index 71beb582..ee77f4dc 100644
--- a/mips_new_tc/main.sail
+++ b/mips_new_tc/main.sail
@@ -8,7 +8,8 @@ function fetch_and_execute () = {
     inBranchDelay = branchPending;
     branchPending = 0b0;
     nextPC = if inBranchDelay then delayedPC else PC + 4;
-
+    cp2_next_pc();
+    
     print_bits("PC: ", PC);
     try {
       let pc_pa = TranslatePC(PC);
diff --git a/mips_new_tc/mips_prelude.sail b/mips_new_tc/mips_prelude.sail
index d1302c52..9927d20e 100644
--- a/mips_new_tc/mips_prelude.sail
+++ b/mips_new_tc/mips_prelude.sail
@@ -615,4 +615,5 @@ function init_cp0_state () : unit -> unit = {
 }
 
 val init_cp2_state : unit -> unit effect {wreg}
+val cp2_next_pc:     unit -> unit effect {rreg, wreg}
 val dump_cp2_state : unit -> unit effect {rreg}
\ No newline at end of file
diff --git a/mips_new_tc/mips_wrappers.sail b/mips_new_tc/mips_wrappers.sail
index bbb99e17..2e67a880 100644
--- a/mips_new_tc/mips_wrappers.sail
+++ b/mips_new_tc/mips_wrappers.sail
@@ -82,4 +82,5 @@ val ERETHook : unit -> unit
 function ERETHook() = ()
 
 function init_cp2_state () = skip_wreg()
+function cp2_next_pc()     = {skip_wreg(); skip_rreg()}
 function dump_cp2_state () = skip_rreg()
-- 
cgit v1.2.3