1 files changed, 2 insertions, 96 deletions
diff --git a/riscv/riscv_sys.sail b/riscv/riscv_sys.sail
index f81a7ebd..d9fe53bb 100644
--- a/riscv/riscv_sys.sail
+++ b/riscv/riscv_sys.sail
@@ -542,103 +542,9 @@ function handle_trap(curp : Privilege, e : sync_exception,
 
 function handle_exception_ctl(cur_priv : Privilege, ctl : ctl_result,
                               pc: xlenbits) -> xlenbits =
-  /* TODO: check delegation */
   match (cur_priv, ctl) {
-    (_, CTL_TRAP(e)) => {
-      mepc            = pc;
-
-      mcause->IsInterrupt() = false;
-      mcause->Cause()       = EXTZ(exceptionType_to_bits(e.trap));
-
-      mstatus->MPIE() = mstatus.MIE();
-      mstatus->MIE()  = false;
-      mstatus->MPP()  = privLevel_to_bits(cur_priv);
-      cur_privilege   = Machine;
-
-      match (e.trap) {
-        E_Fetch_Addr_Align => {
-          match (e.excinfo) {
-            Some(a) => mtval = a,
-            None()  => throw Error_internal_error()
-          }
-        },
-        E_Fetch_Access_Fault => {
-          match (e.excinfo) {
-            Some(a) => mtval = a,
-            None()  => throw Error_internal_error()
-          }
-        },
-        E_Illegal_Instr => {
-          match (e.excinfo) {
-            Some(a) => mtval = a,
-            None()  => throw Error_internal_error()
-          }
-        },
-
-        E_Breakpoint => not_implemented("breakpoint"),
-
-        E_Load_Addr_Align => {
-          match (e.excinfo) {
-            Some(a) => mtval = a,
-            None()  => throw Error_internal_error()
-          }
-        },
-        E_Load_Access_Fault => {
-          match (e.excinfo) {
-            Some(a) => mtval = a,
-            None()  => throw Error_internal_error()
-          }
-        },
-        E_SAMO_Addr_Align => {
-          match (e.excinfo) {
-            Some(a) => mtval = a,
-            None()  => throw Error_internal_error()
-          }
-        },
-        E_SAMO_Access_Fault => {
-          match (e.excinfo) {
-            Some(a) => mtval = a,
-            None()  => throw Error_internal_error()
-          }
-        },
-
-        E_U_EnvCall => {
-          mtval  = EXTZ(0b0)
-        },
-        E_S_EnvCall => {
-          mtval  = EXTZ(0b0)
-        },
-        E_M_EnvCall => {
-          mtval  = EXTZ(0b0)
-        },
-
-        E_Fetch_Page_Fault => {
-          match (e.excinfo) {
-            Some(a) => mtval = a,
-            None()  => throw Error_internal_error()
-          }
-        },
-        E_Load_Page_Fault => {
-          match (e.excinfo) {
-            Some(a) => mtval = a,
-            None()  => throw Error_internal_error()
-          }
-        },
-        E_SAMO_Page_Fault => {
-          match (e.excinfo) {
-            Some(a) => mtval = a,
-            None()  => throw Error_internal_error()
-          }
-        },
-        _ => throw Error_internal_error() /* Don't expect ReservedExc0 etc. here */
-      };
-      /* TODO: make register read explicit */
-      match (tvec_addr(mtvec, mcause)) {
-        Some(addr) => addr,
-        None()     => throw Error_internal_error()
-      }
-    },
-    (_, CTL_MRET()) => {
+    (_, CTL_TRAP(e)) => handle_trap(cur_priv, e, pc),
+    (_, CTL_MRET())  => {
       mstatus->MIE()  = mstatus.MPIE();
       mstatus->MPIE() = true;
       cur_privilege   = privLevel_of_bits(mstatus.MPP());