diff options
| author | Robert Norton | 2016-04-28 14:54:57 +0100 |
|---|---|---|
| committer | Robert Norton | 2016-04-28 14:55:04 +0100 |
| commit | ef3deb63b3eead7e3b3ec826fd3d4f5695d642df (patch) | |
| tree | 1898b9877ef98523925dfcf155b718626f1622e2 | |
| parent | ebea637489446114fb95863db861accf14a6b393 (diff) | |
implement (hopefully) correct exception behaviour wrt PCC/EPCC. Required shuffling function names and adding a hook in ERET.
| -rw-r--r-- | cheri/cheri_prelude.sail | 17 | ||||
| -rw-r--r-- | mips/mips_insts.sail | 1 | ||||
| -rw-r--r-- | mips/mips_prelude.sail | 4 | ||||
| -rw-r--r-- | mips/mips_wrappers.sail | 4 |
4 files changed, 25 insertions, 1 deletions
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() = () |