Move CHERI PTE traps to their own vectors

Rather than riding through the generic 0x1C vector.  This removes
CapEx_CapLoadGen and CapEx_MMUNoStoreCap

Author: nwf

src/cheri_insts.sail

@@ -944,7 +944,7 @@ function clause execute (CLoadCap(rd, cs, is_unsigned, width)) =
 
 union load_cap_ptw_ext_result = {
   LCPE_OK : Capability,
-  LCPE_Exn : CapEx
+  LCPE_Exn : ExceptionType
 }
 
 val handle_load_cap_ptw_ext : (Capability, bool, ext_ptw_lcm) -> load_cap_ptw_ext_result
@@ -954,7 +954,7 @@ function handle_load_cap_ptw_ext (v, vialc, ptw_info) =
   else match ptw_info {
          PTW_LCM_OK => LCPE_OK({v with tag = v.tag & vialc}),
          PTW_LCM_CLR => LCPE_OK({v with tag = false}),
-         PTW_LCM_TRAP => LCPE_Exn(CapEx_CapLoadGen)
+         PTW_LCM_TRAP => LCPE_Exn(E_Extension(EXC_CHERI_MMU_LOAD_CAP))
        }
 
 val handle_load_cap_via_cap : (regidx, capreg_idx, Capability, xlenbits) -> Retired effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg}
@@ -985,14 +985,15 @@ function handle_load_cap_via_cap(rd, cs, cap_val, vaddrBits) = {
 
       if ~(load_cap_data_dep_trap) & vialc & lcav == PTW_LCM_TRAP then {
         /* If we're not permitted to do tag-dependent traps, trap now */
-        handle_cheri_cap_exception(CapEx_CapLoadGen, cs); RETIRE_FAIL
+        handle_mem_exception(vaddrBits, E_Extension(EXC_CHERI_MMU_LOAD_CAP));
+        RETIRE_FAIL
       } else {
         let c = mem_read_cap(addr, aq, rl, false);
         match c {
           MemValue(v) => {
             match handle_load_cap_ptw_ext(v, vialc, lcav) {
               LCPE_OK(v') => { writeCapReg(rd, v'); RETIRE_SUCCESS },
-              LCPE_Exn(e) => { handle_cheri_cap_exception(e, cs); RETIRE_FAIL }
+              LCPE_Exn(e) => { handle_mem_exception(vaddrBits, e); RETIRE_FAIL }
             }
           },
           MemException(e) => {handle_mem_exception(vaddrBits, e); RETIRE_FAIL }
@@ -1090,14 +1091,15 @@ if not(cap_val.tag) then {
 
       if ~(load_cap_data_dep_trap) & vialc & lcav == PTW_LCM_TRAP then {
         /* If we're not permitted to do tag-dependent traps, trap now */
-        handle_cheri_cap_exception(CapEx_CapLoadGen, cs); RETIRE_FAIL
+        handle_mem_exception(vaddrBits, E_Extension(EXC_CHERI_MMU_LOAD_CAP));
+        RETIRE_FAIL
       } else {
         let c = mem_read_cap(addr, aq, rl, false);
         match c {
           MemValue(v) => {
             match handle_load_cap_ptw_ext(v, vialc, lcav) {
               LCPE_OK(v') => { load_reservation(addr); writeCapReg(cd, v'); RETIRE_SUCCESS },
-              LCPE_Exn(e) => { handle_cheri_cap_exception(e, cs); RETIRE_FAIL }
+              LCPE_Exn(e) => { handle_mem_exception(vaddrBits, e); RETIRE_FAIL }
             }
           },
           MemException(e) => {handle_mem_exception(vaddrBits, e); RETIRE_FAIL }
@@ -1248,16 +1250,16 @@ function handle_store_cap_via_cap(rs, cs, cap_val, vaddrBits) = {
     handle_mem_exception(vaddrBits, E_SAMO_Addr_Align());
     RETIRE_FAIL
   } else match translateAddr(vaddrBits, Write(if rs_val.tag then Cap else Data)) {
-    TR_Failure(E_Extension(EXC_CHERI_VMEM_STORE_CAP), _) => {
-      handle_cheri_cap_exception(CapEx_MMUNoStoreCap, cs);
+    TR_Failure(E_Extension(EXC_CHERI_MMU_STORE_CAP), _) => {
+      handle_mem_exception(vaddrBits, E_Extension(EXC_CHERI_MMU_STORE_CAP));
       RETIRE_FAIL
     },
     TR_Failure(E_Extension(_), _) => { internal_error("unexpected cheri exception for cap store") },
     TR_Failure(e, _) => { handle_mem_exception(vaddrBits, e); RETIRE_FAIL },
     TR_Address(addr, caveats) => {
       match (caveats.ptw_sc_mod, rs_val.tag) {
         (PTW_SCM_TRAP, true) => {
-          handle_cheri_cap_exception(CapEx_MMUNoStoreCap, cs);
+          handle_mem_exception(vaddrBits, E_Extension(EXC_CHERI_MMU_STORE_CAP));
           RETIRE_FAIL
         },
         _ => {
@@ -1405,15 +1407,15 @@ function handle_store_cond_cap_via_cap(cs2, cs, cap_val, vaddrBits) = {
   } else {
     match translateAddr(vaddrBits, Write(if cs2_val.tag then Cap else Data)) {
       TR_Failure(E_Extension(EXC_CHERI_VMEM_STORE_CAP), _) => {
-        handle_cheri_cap_exception(CapEx_MMUNoStoreCap, cs);
+        handle_mem_exception(vaddrBits, E_Extension(EXC_CHERI_MMU_STORE_CAP));
         RETIRE_FAIL
       },
       TR_Failure(E_Extension(_), _) => { internal_error("unexpected cheri exception for cap store") },
       TR_Failure(e, _) => { handle_mem_exception(vaddrBits, e); RETIRE_FAIL },
       TR_Address(addr, caveats) => {
         match (caveats.ptw_sc_mod, cs2_val.tag) {
           (PTW_SCM_TRAP, true) => {
-            handle_cheri_cap_exception(CapEx_MMUNoStoreCap, cs);
+            handle_mem_exception(vaddrBits, E_Extension(EXC_CHERI_MMU_STORE_CAP));
             RETIRE_FAIL
           },
           _ => {

src/cheri_riscv_types.sail

@@ -61,28 +61,57 @@ let init_ext_ptw : ext_ptw = struct {
   ptw_sc_mod = PTW_SCM_OK
 }
 
-/* Address translation errors */
-enum ext_ptw_error = {AT_LOAD_CAP_ERR, AT_STORE_CAP_ERR}
+/*
+ * Address translation errors
+ *
+ * For CHERI, these are defined but not used at present: our PTE extensions
+ * are defined here in a data-dependent way.  In some eventuality, perhaps
+ * we'll have this kind of data-independence as well, so it doesn't hurt to
+ * keep the symbols around.
+ */
+enum ext_ptw_error = {
+  AT_LOAD_CAP_ERR,
+  AT_STORE_CAP_ERR
+}
 
 /* CHERI exception extensions */
 
-enum ext_exc_type = {EXC_CHERI, EXC_CHERI_VMEM_LOAD_CAP, EXC_CHERI_VMEM_STORE_CAP}
+enum ext_exc_type = {
+  EXC_CHERI,
+  EXC_CHERI_MMU_LOAD_CAP,
+  EXC_CHERI_MMU_STORE_CAP
+}
 
 /* CHERI translation of PTW errors into exception annotations */
 function ext_translate_exception(e : ext_ptw_error) -> ext_exc_type =
   match e {
-    AT_LOAD_CAP_ERR  => EXC_CHERI_VMEM_LOAD_CAP,
-    AT_STORE_CAP_ERR => EXC_CHERI_VMEM_STORE_CAP
+    AT_LOAD_CAP_ERR  => EXC_CHERI_MMU_LOAD_CAP,
+    AT_STORE_CAP_ERR => EXC_CHERI_MMU_STORE_CAP
 }
 
 /* CHERI conversion of extension exceptions to bits */
 val ext_exc_type_to_bits : ext_exc_type -> exc_code
-function ext_exc_type_to_bits(e) = 0x1C
+function ext_exc_type_to_bits(e) =
+  match e {
+    EXC_CHERI_MMU_LOAD_CAP  => 0x1A,
+    EXC_CHERI_MMU_STORE_CAP => 0x1B,
+    _                       => 0x1C
+  }
 
 /* CHERI conversion of extension exceptions to integers */
 val num_of_ext_exc_type : ext_exc_type -> {'n, (0 <= 'n < xlen). int('n)}
-function num_of_ext_exc_type(e) = 28
+function num_of_ext_exc_type(e) =
+  match e {
+    EXC_CHERI_MMU_LOAD_CAP  => 26,
+    EXC_CHERI_MMU_STORE_CAP => 27,
+    _                       => 28
+  }
 
 /* CHERI conversion of extension exceptions to strings */
 val ext_exc_type_to_str : ext_exc_type -> string
-function ext_exc_type_to_str(e) = "cheri-exception"
+function ext_exc_type_to_str(e) =
+  match e {
+    EXC_CHERI_MMU_LOAD_CAP  => "cheri-mmu-cap-load",
+    EXC_CHERI_MMU_STORE_CAP => "cheri-mmu-cap-store",
+    _                       => "cheri-exception"
+  }

src/cheri_types.sail

@@ -65,7 +65,6 @@ enum CapEx = {
   CapEx_ReturnTrap,
   CapEx_TSSUnderFlow,
   CapEx_UserDefViolation,
-  CapEx_MMUNoStoreCap,
   CapEx_InexactBounds,
   CapEx_UnalignedBase,
   CapEx_GlobalViolation,
@@ -80,8 +79,7 @@ enum CapEx = {
   CapEx_PermitCCallViolation,
   CapEx_AccessCCallIDCViolation,
   CapEx_PermitUnsealViolation,
-  CapEx_PermitSetCIDViolation,
-  CapEx_CapLoadGen
+  CapEx_PermitSetCIDViolation
 }
 
 function CapExCode(ex) : CapEx -> bits(5) =
@@ -95,7 +93,7 @@ function CapExCode(ex) : CapEx -> bits(5) =
     CapEx_ReturnTrap                    => 0b00110,
     CapEx_TSSUnderFlow                  => 0b00111,
     CapEx_UserDefViolation              => 0b01000,
-    CapEx_MMUNoStoreCap                 => 0b01001,
+    /* 0b01001 unused; was CapEx_MMUNoStoreCap */
     CapEx_InexactBounds                 => 0b01010,
     CapEx_UnalignedBase                 => 0b01011,
     CapEx_GlobalViolation               => 0b10000,
@@ -110,8 +108,7 @@ function CapExCode(ex) : CapEx -> bits(5) =
     CapEx_PermitCCallViolation          => 0b11001,
     CapEx_AccessCCallIDCViolation       => 0b11010,
     CapEx_PermitUnsealViolation         => 0b11011,
-    CapEx_PermitSetCIDViolation         => 0b11100,
-    CapEx_CapLoadGen                    => 0b11101
+    CapEx_PermitSetCIDViolation         => 0b11100
   }
 
 function string_of_capex (ex) : CapEx -> string =
@@ -125,7 +122,6 @@ function string_of_capex (ex) : CapEx -> string =
     CapEx_ReturnTrap                    => "ReturnTrap"                  ,
     CapEx_TSSUnderFlow                  => "TSSUnderFlow"                ,
     CapEx_UserDefViolation              => "UserDefViolation"            ,
-    CapEx_MMUNoStoreCap                 => "MMUNoStoreCap"               ,
     CapEx_InexactBounds                 => "InexactBounds"               ,
     CapEx_UnalignedBase                 => "UnalignedBounds"             ,
     CapEx_GlobalViolation               => "GlobalViolation"             ,
@@ -140,8 +136,7 @@ function string_of_capex (ex) : CapEx -> string =
     CapEx_PermitCCallViolation          => "PermitCCallViolation"        ,
     CapEx_AccessCCallIDCViolation       => "AccessCCallIDCViolation"     ,
     CapEx_PermitUnsealViolation         => "PermitUnsealViolation"       ,
-    CapEx_PermitSetCIDViolation         => "PermitSetCIDViolation"       ,
-    CapEx_CapLoadGen                    => "CapLoadGen"
+    CapEx_PermitSetCIDViolation         => "PermitSetCIDViolation"
   }
 
 type capreg_idx = bits(6)