From ef3deb63b3eead7e3b3ec826fd3d4f5695d642df Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Thu, 28 Apr 2016 14:54:57 +0100
Subject: implement (hopefully) correct exception behaviour wrt PCC/EPCC.
 Required shuffling function names and adding a hook in ERET.

---
 cheri/cheri_prelude.sail | 17 +++++++++++++++++
 mips/mips_insts.sail     |  1 +
 mips/mips_prelude.sail   |  4 +++-
 mips/mips_wrappers.sail  |  4 ++++
 4 files changed, 25 insertions(+), 1 deletion(-)

diff --git a/cheri/cheri_prelude.sail b/cheri/cheri_prelude.sail
index 1ae3fa77..9c7e4d20 100644
--- a/cheri/cheri_prelude.sail
+++ b/cheri/cheri_prelude.sail
@@ -279,6 +279,23 @@ typedef CapCauseReg = register bits [15:0] {
 
 register CapCauseReg CapCause
 
+function unit SignalException ((Exception) ex) = 
+  {
+    C31        := PCC;
+    C31.offset := PC;
+    nextPCC    := C29; (* KCC *)
+    delayedPCC := C29; (* always write delayedPCC together whether PCC so 
+                          that non-capability branches don't override PCC *)
+    SignalExceptionMIPS(ex);
+  }
+
+function unit ERETHook() =
+  {
+    nextPCC    := C31;
+    delayedPCC := C31; (* always write delayedPCC together whether PCC so 
+                          that non-capability branches don't override PCC *)
+  }
+
 function unit raise_c2_exception8((CapEx) capEx, (bit[8]) regnum) =
   {
     (CapCause.ExcCode) := CapExCode(capEx);
diff --git a/mips/mips_insts.sail b/mips/mips_insts.sail
index 26ef9fae..16af5c22 100644
--- a/mips/mips_insts.sail
+++ b/mips/mips_insts.sail
@@ -1393,6 +1393,7 @@ function clause decode (0b010000 : 0b1 : 0b0000000000000000000 : 0b011000) =
       Some(ERET)
 function clause execute (ERET) =
       {
+        ERETHook();
         if (CP0Status.ERL == bitone) then
           {
             nextPC := CP0ErrorEPC;
diff --git a/mips/mips_prelude.sail b/mips/mips_prelude.sail
index 801802de..9161b929 100644
--- a/mips/mips_prelude.sail
+++ b/mips/mips_prelude.sail
@@ -146,7 +146,9 @@ function (bit[5]) ExceptionCode ((Exception) ex) =
    }
 
 
-function unit SignalException ((Exception) ex) = 
+val Exception -> unit effect {rreg, wreg} SignalException
+
+function unit SignalExceptionMIPS ((Exception) ex) = 
   {
     (* Only update EPC and BD if not already in EXL mode *)
     if (~ (CP0Status.EXL)) then 
diff --git a/mips/mips_wrappers.sail b/mips/mips_wrappers.sail
index f9530b25..110b551d 100644
--- a/mips/mips_wrappers.sail
+++ b/mips/mips_wrappers.sail
@@ -7,3 +7,7 @@ function bit[64] addrWrapper((bit[64]) addr, (MemAccessType) accessType, (WordTy
 
 function (option<Exception>, option<bit[64]>) TranslateAddress ((bit[64]) vAddr, (MemAccessType) accessType) = 
     TLBTranslate(vAddr, accessType)
+
+function unit SignalException ((Exception) ex) = SignalExceptionMIPS(ex)
+
+function unit ERETHook() = ()
-- 
cgit v1.2.3