Add support for CHERI exceptions. Validate PCC / PC on fetch.

8 files changed, 147 insertions, 96 deletions

diff --git a/model/cheri_insts.sail b/model/cheri_insts.sail
index 4e9fbc9..c4a6d60 100644
--- a/model/cheri_insts.sail
+++ b/model/cheri_insts.sail
@@ -32,37 +32,35 @@
 /*  SUCH DAMAGE.                                                          */
 /*========================================================================*/
 
-val raise_c2_exception8 : (CapEx, bits(8)) -> bool /*effect {escape, rreg, wreg}*/
-function raise_c2_exception8(capEx, regnum) =
+val raise_c2_exception6 : (CapEx, bits(6)) -> bool effect {escape, rreg, wreg}
+function raise_c2_exception6(capEx, regnum) =
   {
-    /*if trace then {
-      prerr(" C2Ex ");
-      prerr(string_of_capex(capEx));
-      prerr(" reg: ");
-      prerr_endline(BitStr(regnum));
-    };*/
-    /*CapCause->ExcCode() = CapExCode(capEx);
-    CapCause->RegNum()  = regnum;
-    let mipsEx = 
-      if ((capEx == CapEx_CallTrap) | (capEx == CapEx_ReturnTrap)) 
-      then C2Trap else C2E in
-    SignalException(mipsEx);*/
+    let cause : cheri_cause = struct {
+        cap_idx = regnum,
+        capEx   = capEx
+    };
+    let t : sync_exception = struct {
+      trap = E_CHERI,
+      excinfo = (None() : option(xlenbits)),
+      ccause = Some(cause)
+    };
+    nextPC = handle_exception(cur_privilege, CTL_TRAP(t), PC);
     false
   }
 
 /*!
-causes the processor to raise a capability exception by writing the given capability exception cause and register number to the CapCause register then signalling an exception using [SignalException] (on CHERI-MIPS this is a C2E exception in most cases, or a special C2Trap for CCall and CReturn). */
-val raise_c2_exception : (CapEx, bits(5)) -> bool /*effect {escape, rreg, wreg}*/
+causes the processor to raise a capability exception by writing the given capability exception cause and register number to the xccsr register then signalling an exception. */
+val raise_c2_exception : (CapEx, bits(5)) -> bool effect {escape, rreg, wreg}
 function raise_c2_exception(capEx, regnum) =
-  let reg8 = 0b000 @ regnum in
-  raise_c2_exception8(capEx, reg8)
+  let reg6 = 0b0 @ regnum in
+  raise_c2_exception6(capEx, reg6)
+
 /*!
-is as [raise_c2_exception] except that CapCause.RegNum  is written with the special value 0xff indicating PCC or no register.
+is as [raise_c2_exception] except that CapCause.RegNum  is written with the special value 0x10 indicating PCC register.
  */
-val raise_c2_exception_noreg : (CapEx) -> bool /* effect {escape, rreg, wreg}*/
-function raise_c2_exception_noreg(capEx) =
-  raise_c2_exception8(capEx, 0xff)
-
+val raise_c2_exception_pcc : (CapEx) -> bool effect {escape, rreg, wreg}
+function raise_c2_exception_pcc(capEx) =
+  raise_c2_exception6(capEx, 0b100000)
 
 val pcc_access_system_regs : unit -> bool effect {rreg}
 function pcc_access_system_regs () = PCC.access_system_regs
@@ -74,7 +72,7 @@ function execute_branch (pc : xlenbits) = {
   base so branches below base will be negative / very large and
   greater than top. */
   if unsigned(pc) + 4 > len then
-    raise_c2_exception_noreg(CapEx_LengthViolation)
+    raise_c2_exception_pcc(CapEx_LengthViolation)
   else {
     nextPC = pc;
     false
@@ -185,7 +183,7 @@ function clause execute (CGetCause(rd)) =
 {
   checkCP2usable();
   if not (pcc_access_system_regs ()) then
-    raise_c2_exception_noreg(CapEx_AccessSystemRegsViolation)
+    raise_c2_exception_pcc(CapEx_AccessSystemRegsViolation)
   else {
     wGPR(rd) = zero_extend(CapCause.bits());
     true
@@ -197,7 +195,7 @@ function clause execute (CSetCause(rt)) =
 {
   checkCP2usable();
   if not (pcc_access_system_regs ()) then
-    raise_c2_exception_noreg(CapEx_AccessSystemRegsViolation)
+    raise_c2_exception_pcc(CapEx_AccessSystemRegsViolation)
   else
   {
     let rt_val = rGPR(rt);
@@ -839,7 +837,7 @@ function clause execute (CCall(cs, cb, 0b00001)) = /* selector=1 */
 function clause execute (CCall(_, _, 0b11111)) = /* CReturn */
 {
   checkCP2usable();
-  raise_c2_exception_noreg(CapEx_ReturnTrap)
+  raise_c2_exception(CapEx_ReturnTrap, 0b11111)
 }
 
 union clause ast = CJALR : (regbits, regbits)
diff --git a/model/cheri_types.sail b/model/cheri_types.sail
index 85bce30..66d1942 100644
--- a/model/cheri_types.sail
+++ b/model/cheri_types.sail
@@ -80,32 +80,32 @@ enum CapEx = {
   CapEx_PermitSetCIDViolation
 }
 
-function CapExCode(ex) : CapEx -> bits(8)=
+function CapExCode(ex) : CapEx -> bits(5)=
   match ex {
-    CapEx_None                          => 0x00,
-    CapEx_LengthViolation               => 0x01,
-    CapEx_TagViolation                  => 0x02,
-    CapEx_SealViolation                 => 0x03,
-    CapEx_TypeViolation                 => 0x04,
-    CapEx_CallTrap                      => 0x05,
-    CapEx_ReturnTrap                    => 0x06,
-    CapEx_TSSUnderFlow                  => 0x07,
-    CapEx_UserDefViolation              => 0x08,
-    CapEx_TLBNoStoreCap                 => 0x09,
-    CapEx_InexactBounds                 => 0x0a,
-    CapEx_GlobalViolation               => 0x10,
-    CapEx_PermitExecuteViolation        => 0x11,
-    CapEx_PermitLoadViolation           => 0x12,
-    CapEx_PermitStoreViolation          => 0x13,
-    CapEx_PermitLoadCapViolation        => 0x14,
-    CapEx_PermitStoreCapViolation       => 0x15,
-    CapEx_PermitStoreLocalCapViolation  => 0x16,
-    CapEx_PermitSealViolation           => 0x17,
-    CapEx_AccessSystemRegsViolation     => 0x18,
-    CapEx_PermitCCallViolation          => 0x19,
-    CapEx_AccessCCallIDCViolation       => 0x1a,
-    CapEx_PermitUnsealViolation         => 0x1b,
-    CapEx_PermitSetCIDViolation         => 0x1c
+    CapEx_None                          => 0b00000,
+    CapEx_LengthViolation               => 0b00001,
+    CapEx_TagViolation                  => 0b00010,
+    CapEx_SealViolation                 => 0b00011,
+    CapEx_TypeViolation                 => 0b00100,
+    CapEx_CallTrap                      => 0b00101,
+    CapEx_ReturnTrap                    => 0b00110,
+    CapEx_TSSUnderFlow                  => 0b00111,
+    CapEx_UserDefViolation              => 0b01000,
+    CapEx_TLBNoStoreCap                 => 0b01001,
+    CapEx_InexactBounds                 => 0b01010,
+    CapEx_GlobalViolation               => 0b10000,
+    CapEx_PermitExecuteViolation        => 0b10001,
+    CapEx_PermitLoadViolation           => 0b10010,
+    CapEx_PermitStoreViolation          => 0b10011,
+    CapEx_PermitLoadCapViolation        => 0b10100,
+    CapEx_PermitStoreCapViolation       => 0b10101,
+    CapEx_PermitStoreLocalCapViolation  => 0b10110,
+    CapEx_PermitSealViolation           => 0b10111,
+    CapEx_AccessSystemRegsViolation     => 0b11000,
+    CapEx_PermitCCallViolation          => 0b11001,
+    CapEx_AccessCCallIDCViolation       => 0b11010,
+    CapEx_PermitUnsealViolation         => 0b11011,
+    CapEx_PermitSetCIDViolation         => 0b11100
   }
 
 function string_of_capex (ex) : CapEx -> string = 
diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail
index 8a9af81..0ebd9a2 100644
--- a/model/riscv_insts_base.sail
+++ b/model/riscv_insts_base.sail
@@ -569,7 +569,8 @@ function clause execute ECALL() = {
                       Supervisor => E_S_EnvCall,
                       Machine    => E_M_EnvCall
                     },
-             excinfo = (None() : option(xlenbits)) };
+             excinfo = (None() : option(xlenbits)),
+             ccause = None()};
   nextPC = handle_exception(cur_privilege, CTL_TRAP(t), PC);
   false
 }
diff --git a/model/riscv_platform.sail b/model/riscv_platform.sail
index c0e8208..63c10b0 100644
--- a/model/riscv_platform.sail
+++ b/model/riscv_platform.sail
@@ -277,7 +277,8 @@ function handle_illegal() -> unit = {
              then Some(instbits)
              else None();
   let t : sync_exception = struct { trap    = E_Illegal_Instr,
-                                    excinfo = info };
+                                    excinfo = info,
+                                    ccause = None()};
   nextPC = handle_exception(cur_privilege, CTL_TRAP(t), PC)
 }
 
diff --git a/model/riscv_step.sail b/model/riscv_step.sail
index 78369a8..c0fc704 100644
--- a/model/riscv_step.sail
+++ b/model/riscv_step.sail
@@ -3,18 +3,30 @@
 union FetchResult = {
   F_Base  : word,                      /* Base ISA */
   F_RVC   : half,                      /* Compressed ISA */
-  F_Error : (ExceptionType, xlenbits)  /* exception and PC */
+  F_Error : (ExceptionType, xlenbits), /* exception and PC */
+  F_CHERI_Err : (CapEx, xlenbits)      /* CHERI exception code and PC */
 }
 
 function isRVC(h : half) -> bool =
  ~ (h[1 .. 0] == 0b11)
 
 val fetch : unit -> FetchResult effect {escape, rmem, rreg, wmv, wreg}
-function fetch() -> FetchResult =
+function fetch() -> FetchResult = {
   /* check for legal PC */
-  if (PC[0] != 0b0 | (PC[1] != 0b0 & (~ (haveRVC()))))
-  then F_Error(E_Fetch_Addr_Align, PC)
-  else match translateAddr(PC, Execute, Instruction) {
+  let abs_pc = getCapBase(PCC) + unsigned(PC);
+  let abs_pc_bits = to_bits(xlen, abs_pc);
+  let (pcc_base, pcc_top) = getCapBounds(PCC);
+  if not(PCC.tag) then
+     F_CHERI_Err(CapEx_TagViolation, PC)
+  else if PCC.sealed then
+     F_CHERI_Err(CapEx_SealViolation, PC)
+  else if not(PCC.permit_execute) then
+     F_CHERI_Err(CapEx_PermitExecuteViolation, PC)
+  else if abs_pc < pcc_base | abs_pc + 2 >= pcc_top then
+     F_CHERI_Err(CapEx_LengthViolation, PC)
+  else if (abs_pc_bits[0] != 0b0 | (abs_pc_bits[1] != 0b0 & (~ (haveRVC()))))
+    then F_Error(E_Fetch_Addr_Align, PC)
+  else match translateAddr(abs_pc_bits, Execute, Instruction) {
     TR_Failure(e)  => F_Error(e, PC),
     TR_Address(ppclo) => {
       /* split instruction fetch into 16-bit granules to handle RVC, as
@@ -25,8 +37,10 @@ function fetch() -> FetchResult =
         MemException(e) => F_Error(E_Fetch_Access_Fault, PC),
         MemValue(ilo) => {
           if isRVC(ilo) then F_RVC(ilo)
+          else if abs_pc + 4 > pcc_top then
+            F_CHERI_Err (CapEx_LengthViolation, PC)
           else {
-            PChi : xlenbits = PC + 2;
+            PChi : xlenbits = abs_pc_bits + 2;
             match translateAddr(PChi, Execute, Instruction) {
               TR_Failure(e) => F_Error(e, PChi),
               TR_Address(ppchi) => {
@@ -41,6 +55,7 @@ function fetch() -> FetchResult =
       }
     }
   }
+}
 
 /* returns whether to increment the step count in the trace */
 val step : int -> bool effect {barr, eamem, escape, exmem, rmem, rreg, wmv, wreg}
@@ -59,6 +74,10 @@ function step(step_no) = {
             handle_mem_exception(addr, e);
             (false, false)
           },
+          F_CHERI_Err(e, addr) => {
+            let _ = raise_c2_exception_pcc(e);
+            (false, false)
+          },
           F_RVC(h) => {
             match decodeCompressed(h) {
               None() => {
diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
index 0a2d9f9..abd9687 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -233,9 +233,15 @@ function dispatchInterrupt(priv : Privilege) -> option((InterruptType, Privilege
 
 /* privilege transitions due to exceptions and interrupts */
 
+struct cheri_cause = {
+  cap_idx : bits(6),
+  capEx   : CapEx
+}
+
 struct sync_exception = {
   trap    : ExceptionType,
-  excinfo : option(xlenbits)
+  excinfo : option(xlenbits),
+  ccause  : option(cheri_cause)
 }
 
 function tval(excinfo : option(xlenbits)) -> xlenbits = {
@@ -263,7 +269,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), ccause : option(cheri_cause))
                     -> xlenbits = {
   rvfi_trap();
   print_platform("handling " ^ (if intr then "int#" else "exc#")
@@ -280,6 +286,13 @@ function handle_trap(del_priv : Privilege, intr : bool, c : exc_code, pc : xlenb
        mstatus->MIE()  = false;
        mstatus->MPP()  = privLevel_to_bits(cur_privilege);
        mtval           = tval(info);
+       match (ccause) {
+          Some(c) => {
+            mccsr->cap_idx() = c.cap_idx;
+            mccsr->cause()   = CapExCode(c.capEx);
+          },
+          _ => ()
+       };
 
        /* XXX should legalize pc here? */
        let (representable, mepcc) = setCapOffset(PCC, pc);
@@ -310,7 +323,14 @@ function handle_trap(del_priv : Privilege, intr : bool, c : exc_code, pc : xlenb
                            Machine => internal_error("invalid privilege for s-mode trap")
                          };
        stval           = tval(info);
-
+       match (ccause) {
+          Some(c) => {
+            sccsr->cap_idx() = c.cap_idx;
+            sccsr->cause()   = CapExCode(c.capEx);
+          },
+          _ => ()
+       };
+       
        let (representable, sepcc) = setCapOffset(PCC, pc);
        assert(representable, "sepcc should always be representable");
        SEPCC           = sepcc;
@@ -334,7 +354,14 @@ function handle_trap(del_priv : Privilege, intr : bool, c : exc_code, pc : xlenb
        mstatus->UPIE() = mstatus.UIE();
        mstatus->UIE()  = false;
        utval           = tval(info);
-
+       match (ccause) {
+          Some(c) => {
+            uccsr->cap_idx() = c.cap_idx;
+            uccsr->cause()   = CapExCode(c.capEx);
+          },
+          _ => ()
+       };
+       
        let (representable, uepcc) = setCapOffset(PCC, pc);
        assert(representable, "UEPCC should always be representable");
        UEPCC           = uepcc;
@@ -354,12 +381,12 @@ function handle_trap(del_priv : Privilege, intr : bool, c : exc_code, pc : xlenb
 
 function handle_exception(cur_priv : Privilege, ctl : ctl_result,
                           pc: xlenbits) -> xlenbits = {
-  match (cur_priv, ctl) {
+  match (cur_priv, ctl) { /* XXX cur_priv seems to be redundant here */
     (_, CTL_TRAP(e)) => {
       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.ccause)
     },
     (_, CTL_MRET())  => {
       let prev_priv   = cur_privilege;
@@ -405,12 +432,13 @@ function handle_exception(cur_priv : Privilege, ctl : ctl_result,
 
 function handle_mem_exception(addr : xlenbits, e : ExceptionType) -> unit = {
   let t : sync_exception = struct { trap    = e,
-                                    excinfo = Some(addr) } in
+                                    excinfo = Some(addr),
+                                    ccause = 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 */
 
diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail
index 3c6ccd9..3348d69 100644
--- a/model/riscv_sys_regs.sail
+++ b/model/riscv_sys_regs.sail
@@ -224,6 +224,7 @@ function legalize_mideleg(o : Minterrupts, v : xlenbits) -> Minterrupts = {
 /* exception processing state */
 
 bitfield Medeleg : bits(64) = {
+  CHERI             : 32,
   SAMO_Page_Fault   : 15,
   Load_Page_Fault   : 13,
   Fetch_Page_Fault  : 12,
diff --git a/model/riscv_types.sail b/model/riscv_types.sail
index c282547..5e01770 100644
--- a/model/riscv_types.sail
+++ b/model/riscv_types.sail
@@ -327,7 +327,7 @@ enum word_width = {BYTE, HALF, WORD, DOUBLE}
 
 /* architectural interrupt definitions */
 
-type exc_code = bits(4)
+type exc_code = bits(8)
 
 enum InterruptType = {
   I_U_Software,
@@ -344,15 +344,15 @@ enum InterruptType = {
 val cast interruptType_to_bits : InterruptType -> exc_code
 function interruptType_to_bits (i) =
   match (i) {
-    I_U_Software => 0x0,
-    I_S_Software => 0x1,
-    I_M_Software => 0x3,
-    I_U_Timer    => 0x4,
-    I_S_Timer    => 0x5,
-    I_M_Timer    => 0x7,
-    I_U_External => 0x8,
-    I_S_External => 0x9,
-    I_M_External => 0xb
+    I_U_Software => 0x00,
+    I_S_Software => 0x01,
+    I_M_Software => 0x03,
+    I_U_Timer    => 0x04,
+    I_S_Timer    => 0x05,
+    I_M_Timer    => 0x07,
+    I_U_External => 0x08,
+    I_S_External => 0x09,
+    I_M_External => 0x0b
   }
 
 /* architectural exception definitions */
@@ -373,28 +373,30 @@ enum ExceptionType = {
  E_Fetch_Page_Fault,
  E_Load_Page_Fault,
  E_Reserved_14,
- E_SAMO_Page_Fault
+ E_SAMO_Page_Fault,
+ E_CHERI
 }
 
 val cast exceptionType_to_bits : ExceptionType -> exc_code
 function exceptionType_to_bits(e) =
   match (e) {
-    E_Fetch_Addr_Align   => 0x0,
-    E_Fetch_Access_Fault => 0x1,
-    E_Illegal_Instr      => 0x2,
-    E_Breakpoint         => 0x3,
-    E_Load_Addr_Align    => 0x4,
-    E_Load_Access_Fault  => 0x5,
-    E_SAMO_Addr_Align    => 0x6,
-    E_SAMO_Access_Fault  => 0x7,
-    E_U_EnvCall          => 0x8,
-    E_S_EnvCall          => 0x9,
-    E_Reserved_10        => 0xa,
-    E_M_EnvCall          => 0xb,
-    E_Fetch_Page_Fault   => 0xc,
-    E_Load_Page_Fault    => 0xd,
-    E_Reserved_14        => 0xe,
-    E_SAMO_Page_Fault    => 0xf
+    E_Fetch_Addr_Align   => 0x00,
+    E_Fetch_Access_Fault => 0x01,
+    E_Illegal_Instr      => 0x02,
+    E_Breakpoint         => 0x03,
+    E_Load_Addr_Align    => 0x04,
+    E_Load_Access_Fault  => 0x05,
+    E_SAMO_Addr_Align    => 0x06,
+    E_SAMO_Access_Fault  => 0x07,
+    E_U_EnvCall          => 0x08,
+    E_S_EnvCall          => 0x09,
+    E_Reserved_10        => 0x0a,
+    E_M_EnvCall          => 0x0b,
+    E_Fetch_Page_Fault   => 0x0c,
+    E_Load_Page_Fault    => 0x0d,
+    E_Reserved_14        => 0x0e,
+    E_SAMO_Page_Fault    => 0x0f,
+    E_CHERI              => 0x20
   }
 
 val cast exceptionType_to_str : ExceptionType -> string
@@ -415,7 +417,8 @@ function exceptionType_to_str(e) =
     E_Fetch_Page_Fault   => "fetch-page-fault",
     E_Load_Page_Fault    => "load-page-fault",
     E_Reserved_14        => "reserved-1",
-    E_SAMO_Page_Fault    => "store/amo-page-fault"
+    E_SAMO_Page_Fault    => "store/amo-page-fault",
+    E_CHERI              => "CHERI"
   }
 
 /* model-internal exceptions */