diff options
| -rw-r--r-- | cheri/cheri_insts.sail | 2 | ||||
| -rw-r--r-- | cheri/cheri_prelude.sail | 5 | ||||
| -rw-r--r-- | mips/mips_prelude.sail | 19 |
3 files changed, 18 insertions, 8 deletions
diff --git a/cheri/cheri_insts.sail b/cheri/cheri_insts.sail index 935f47ca..fe77df82 100644 --- a/cheri/cheri_insts.sail +++ b/cheri/cheri_insts.sail @@ -414,7 +414,7 @@ function clause execute (CCall(cs, cb)) = else if (cs_val.offset >= cs_val.length) then exit (raise_c2_exception(CapEx_LengthViolation, cs)) else - exit (raise_c2_exception_noreg(CapEx_CallTrap)); + exit (raise_c2_exception(CapEx_CallTrap, cs)); } union ast member unit CReturn diff --git a/cheri/cheri_prelude.sail b/cheri/cheri_prelude.sail index 9c7e4d20..6aaa9a0c 100644 --- a/cheri/cheri_prelude.sail +++ b/cheri/cheri_prelude.sail @@ -300,7 +300,10 @@ function unit raise_c2_exception8((CapEx) capEx, (bit[8]) regnum) = { (CapCause.ExcCode) := CapExCode(capEx); (CapCause.RegNum) := regnum; - SignalException(C2E); + let mipsEx = + if ((capEx == CapEx_CallTrap) | (capEx == CapEx_ReturnTrap)) + then C2Trap else C2E in + SignalException(mipsEx); } function unit raise_c2_exception((CapEx) capEx, (regno) regnum) = diff --git a/mips/mips_prelude.sail b/mips/mips_prelude.sail index 9161b929..b3fb9a32 100644 --- a/mips/mips_prelude.sail +++ b/mips/mips_prelude.sail @@ -120,7 +120,7 @@ val extern unit -> unit effect { barr } MEM_sync typedef Exception = enumerate { - Int; Mod; TLBL; TLBS; AdEL; AdES; Sys; Bp; ResI; CpU; Ov; Tr; C2E; + Int; Mod; TLBL; TLBS; AdEL; AdES; Sys; Bp; ResI; CpU; Ov; Tr; C2E; C2Trap; XTLBRefillL; XTLBRefillS } @@ -141,6 +141,7 @@ function (bit[5]) ExceptionCode ((Exception) ex) = case Ov -> mask(0x0c) (* Arithmetic overflow *) case Tr -> mask(0x0d) (* Trap *) case C2E -> mask(0x12) (* C2E coprocessor 2 exception *) + case C2Trap -> mask(0x12) (* C2Trap maps to same exception code, different vector *) case XTLBRefillL -> mask(0x02) case XTLBRefillS -> mask(0x03) } @@ -165,11 +166,17 @@ function unit SignalExceptionMIPS ((Exception) ex) = } }; - (* choose an exception vector to branch to *) - vectorOffset := if ((ex == XTLBRefillL) | (ex == XTLBRefillS)) & ~ (CP0Status.EXL) then - 0x080 - else - 0x180; + (* choose an exception vector to branch to. Some are not supported + e.g. Reset *) + vectorOffset := + if (CP0Status.EXL) then + 0x180 (* Always use common vector if in exception mode already *) + else if ((ex == XTLBRefillL) | (ex == XTLBRefillS)) then + 0x080 + else if (ex == C2Trap) then + 0x280 (* Special vector for CHERI traps *) + else + 0x180; (* Common vector *) (bit[64]) vectorBase := if CP0Status.BEV then 0xFFFFFFFFBFC00200 else |