Add extended model from cheri-merge.

1 files changed, 30 insertions, 31 deletions

diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
index 4155d66..5c72058 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -244,18 +244,12 @@ function dispatchInterrupt(priv : Privilege) -> option((InterruptType, Privilege
   }
 }
 
-/* privilege transitions due to exceptions and interrupts */
+/* model context for synchronous exceptions, parameterized for extensions */
 
 struct sync_exception = {
   trap    : ExceptionType,
-  excinfo : option(xlenbits)
-}
-
-function tval(excinfo : option(xlenbits)) -> xlenbits = {
-  match (excinfo) {
-    Some(e) => e,
-    None()  => EXTZ(0b0)
-  }
+  excinfo : option(xlenbits),
+  ext     : option(ext_exception)   /* for extensions */
 }
 
 union ctl_result = {
@@ -265,6 +259,15 @@ union ctl_result = {
   CTL_URET : unit
 }
 
+/* trap value */
+
+function tval(excinfo : option(xlenbits)) -> xlenbits = {
+  match (excinfo) {
+    Some(e) => e,
+    None()  => EXTZ(0b0)
+  }
+}
+
 $ifdef RVFI_DII
 val rvfi_trap : unit -> unit effect {wreg}
 function rvfi_trap () =
@@ -276,7 +279,7 @@ $endif
 
 /* handle exceptional ctl flow by updating nextPC and operating privilege */
 
-function handle_trap(del_priv : Privilege, intr : bool, c : exc_code, pc : xlenbits, info : option(xlenbits))
+function handle_trap(del_priv : Privilege, intr : bool, c : exc_code, pc : xlenbits, info : option(xlenbits), ext : option(ext_exception))
                     -> xlenbits = {
   rvfi_trap();
   print_platform("handling " ^ (if intr then "int#" else "exc#")
@@ -297,12 +300,11 @@ function handle_trap(del_priv : Privilege, intr : bool, c : exc_code, pc : xlenb
 
        cur_privilege   = del_priv;
 
+       handle_trap_extension(del_priv, pc, ext);
+
        print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits()));
 
-       match tvec_addr(mtvec, mcause) {
-         Some(epc) => epc,
-         None()    => internal_error("Invalid mtvec mode")
-       }
+       prepare_trap_vector(del_priv, mcause)
     },
     Supervisor => {
        //assert (haveSupMode());
@@ -322,13 +324,11 @@ function handle_trap(del_priv : Privilege, intr : bool, c : exc_code, pc : xlenb
 
        cur_privilege   = del_priv;
 
-       print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits()));
+       handle_trap_extension(del_priv, pc, ext);
 
-       match tvec_addr(stvec, scause) {
-         Some(epc) => epc,
-         None()    => internal_error("Invalid stvec mode")
-       }
+       print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits()));
 
+       prepare_trap_vector(del_priv, scause)
     },
     User => {
        //assert(haveUsrMode());
@@ -343,12 +343,11 @@ function handle_trap(del_priv : Privilege, intr : bool, c : exc_code, pc : xlenb
 
        cur_privilege   = del_priv;
 
+       handle_trap_extension(del_priv, pc, ext);
+
        print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits()));
 
-       match tvec_addr(utvec, ucause) {
-         Some(epc) => epc,
-         None()    => internal_error("Invalid utvec mode")
-       }
+       prepare_trap_vector(del_priv, ucause)
     }
   };
 }
@@ -360,7 +359,7 @@ function handle_exception(cur_priv : Privilege, ctl : ctl_result,
       let del_priv = exception_delegatee(e.trap, cur_priv);
       print_platform("trapping from " ^ cur_priv ^ " to " ^ del_priv
                      ^ " to handle " ^ e.trap);
-      handle_trap(del_priv, false, e.trap, pc, e.excinfo)
+      handle_trap(del_priv, false, e.trap, pc, e.excinfo, e.ext)
     },
     (_, CTL_MRET())  => {
       let prev_priv   = cur_privilege;
@@ -373,21 +372,21 @@ function handle_exception(cur_priv : Privilege, ctl : ctl_result,
       print_platform("ret-ing from " ^ prev_priv ^ " to " ^ cur_privilege);
 
       cancel_reservation();
-      mepc & pc_alignment_mask()
+      get_xret_target(Machine) & pc_alignment_mask()
     },
     (_, CTL_SRET())  => {
       let prev_priv   = cur_privilege;
       mstatus->SIE()  = mstatus.SPIE();
       mstatus->SPIE() = true;
       cur_privilege   = if mstatus.SPP() == true then Supervisor else User;
-      /* S-mode implies that U-mode is supported (issue #331 on riscv-isa-manual). */
+      /* S-mode implies that U-mode is supported (issue 331 on riscv-isa-manual). */
       mstatus->SPP()  = false;
 
       print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits()));
       print_platform("ret-ing from " ^ prev_priv ^ " to " ^ cur_privilege);
 
       cancel_reservation();
-      sepc & pc_alignment_mask()
+      get_xret_target(Supervisor) & pc_alignment_mask()
     },
     (_, CTL_URET())  => {
       let prev_priv   = cur_privilege;
@@ -399,23 +398,23 @@ function handle_exception(cur_priv : Privilege, ctl : ctl_result,
       print_platform("ret-ing from " ^ prev_priv ^ " to " ^ cur_privilege);
 
       cancel_reservation();
-      uepc & pc_alignment_mask()
+      get_xret_target(User) & pc_alignment_mask()
     }
   }
 }
 
 function handle_mem_exception(addr : xlenbits, e : ExceptionType) -> unit = {
   let t : sync_exception = struct { trap    = e,
-                                    excinfo = Some(addr) } in
+                                    excinfo = Some(addr),
+                                    ext     = None() } in
   nextPC = handle_exception(cur_privilege, CTL_TRAP(t), PC)
 }
 
 function handle_interrupt(i : InterruptType, del_priv : Privilege) -> unit =
-  nextPC = handle_trap(del_priv, true, i, PC, None())
+  nextPC = handle_trap(del_priv, true, i, PC, None(), None())
 
 /* state state initialization */
 
-val sys_enable_rvc = {c: "sys_enable_rvc", ocaml: "Platform.enable_rvc", _: "sys_enable_rvc"} : unit -> bool
 function init_sys() -> unit = {
   cur_privilege = Machine;