Remove bounds checks on jumps / branch. Simplify and clarify MEPCC an…

…d MTCC behaviour.

As per #23 we want to delay the bounds check on jumps / branches until instruction
fetch in order to simplify hardware. Due to this potentially leading to
unrepresentable MEPCC values we also clear the tag of MEPCC on instruction fetch
bounds violations. Due to this this got a bit mixed up with #30 which clarifies
and simplifies validation and legalization of MEPCC / MTCC.

archdoc/app-isaquick-riscv.tex

@@ -96,7 +96,6 @@ \chapter{Instruction encoding summary}
 	\optype{Control-Flow}
 
 	No special new control flow instructions are added, although RISC-V \texttt{JAL} / \texttt{JALR} become capability instructions \rvcheriasminsnref{CJAL}  / \rvcheriasminsnref{CJALR}.
-	The branch instructions also check that \PCC{} permits at least one 2-byte instruction to be loaded from the target address, otherwise they raise a capability bounds exception.
 
 	\optype{Memory-Access}
 	\label{quickref:mem}

archdoc/chap-changes.tex

@@ -12,6 +12,15 @@ \chapter{Version history}
     Tag clearing is preferable for software because it removes the possibility of a trap when copying untrusted inputs.
     It is also likely easier to implement in hardware.
     The capability exception code that was previously used for this (0x16) is now reserved.
-    \item[] The relocations for \insnref{auicgp} and \insnref{auipcc} are unified and the CHERIoT-specific relocations are now named with CHERIOT, rather than CHERI, as the prefix.
+    \item[\ghpr{33}] The relocations for \insnref{auicgp} and \insnref{auipcc} are unified and the CHERIoT-specific relocations are now named with CHERIOT, rather than CHERI, as the prefix.
+    \item[\ghissue{23}, \ghissue{18}, \ghpr{37}] Jumps and branches no longer include bounds checks.
+    Instead, any \PCC{} bounds error will be detected on the subsequent instruction fetch at the target.
+    To avoid problems with unrepresentable capabilities the tag of the value stored in \EPCC{} is cleared for instruction fetch bounds exceptions.
+    \item[\ghissue{30}, \ghpr{37}] Validate \MEPCC{} and \MTCC{} on write.
+    If either of these is written with a sealed or non-executable capability then the tag is cleared.
+    If the least significant bit of \MEPCC{}.\caddress{} is set on write then it is cleared and the tag is cleared.
+    If either of the two least significant bits of \MTCC{}.\caddress{} is set on write then they are cleared and the tag is cleared.
+    This simplifies both ISA and hardware and avoids potential violations of capability monotonicity due to \asm{mtvec} and \asm{mepc} legalization.
+    vectored interrupt mode is explicitly unsupported.
     \end{description}
 \end{description}

archdoc/chap-cheri-riscv.tex

@@ -54,16 +54,22 @@ \section{Instruction encodings}
 \section{Changes to instruction fetch / control flow}
 
 The program counter is extended to a capability, \PCC{}, with \PCC{}.\caddress{} assuming the role of the \PC{}.
-If \PCC{} is untagged, sealed, lacks \cappermX, or the instruction is not entirely within the bounds of \PCC{}, then an exception is raised.
+If \PCC{} becomes untagged or the instruction is not entirely within the bounds of \PCC{}, then an exception is raised.
 Note that the bounds check must take account of whether the fetched instruction is 2 or 4 bytes.
-Checks on jumps and branches mean the only way for \PCC{} to be untagged, sealed or non-executable is after an \asm{MRET} with an invalid \asm{MEPCC} or a trap with an invalid \asm{MTCC}.
-
-\insnriscvref{CJAL} and taken branch instructions check the destination address against the bounds of \PCC{}: if the bounds do not permit at least one 2-byte instruction to be loaded from the destination then a capability length violation exception is raised on the jump / branch instruction.
+If the program counter is outside the bounds of \PCC{} it might be unrepresentable in the compressed capability format (\cref{sec:bounds,sec:repcheck}).
+Therefore, to avoid violating capability monotonicity the value written to \MEPCC{} when there is an instruction fetch bounds violation has its tag cleared.
+Due to unrepresentability the bounds of \MEPCC{} might not correspond to the bounds of \PCC{} at the time of the exception in this case.
 
 \insnriscvref{CJALR} replaces the \asm{JALR} instruction and uses capabilities for the target and link register.
-It checks that the target capability is tagged, unsealed, executable and the address is in bounds before it is installed in \PCC{}.
-If the target is sealed with the reserved `sentry' type then it is unsealed before jumping to it.
-The link register, including the current \PCC{}, is sealed as a sentry.
+It checks that the target capability is tagged and executable before it is installed in \PCC{}.
+If the target is sealed with one of the reserved `sentry' types then it is unsealed before jumping to it, while possibly writing \asm{mstatus.MIE} (see \cref{sec:sealing}).
+If it is sealed with a non-sentry type an exception is raised.
+
+The link register written by \insnriscvref{CJAL} and \insnref{CJALR} is sealed as a sentry of the type corresponding to the current value of \asm{mstatus.MIE}.
+
+The checks on \insnriscvref{CJALR} and special capability writes (\cref{sec:scrs}) prevent execution with a \PCC{} that is sealed or lacks \cappermX{}.
+The only ways for \PCC{} to become untagged is by \asm{MRET} with an untagged \MEPCC{} or exception with untagged \MTCC{}.
+The latter will result in an unrecoverable exception loop.
 
 \section{Changes to memory accesses}
 
@@ -144,20 +150,12 @@ \section{Controlling access to system registers}
 \section{Special capability registers}
 
 \label{subsection:cheri-riscv-scrs}
+\label{sec:scrs}
 
-Special Capability Registers (SCRs) are similar to CSRs in that they affect special functions such as exception delivery, except that they contain capabilities rather than integers.
-SCRs are accessed via a new instruction, \insnriscvref{CSpecialRW}, which behaves similarly to the RISC-V \asm{CSRRW} instruction.
+Special Capability Registers (SCRs) are similar to RISC-V's Control and Status Registers (CSRs) except that they contain capabilities rather than integers.
+They are accessed via a new instruction, \insnriscvref{CSpecialRW}, which behaves similarly to the RISC-V \asm{CSRRW} instruction.
 \asm{CSpecialRW} requires that \PCC{} has \cappermASR{}, otherwise it will raise an exception.
 
-Some SCRs replace existing RISC-V CSRs.
-Attempting to access the legacy RISC-V CSR via the \asm{CSR*} instructions results in a Reserved Instruction exception.
-Any special meaning or behavior associated with the CSR applies to the SCR's address field.
-For example, the lower two bits of \MTCC{}.\caddress{} select the trap mode, and the remaining bits (including the capability metadata) form the trap base address in the same way as \mtvec{}.
-Some RISC-V CSRs have write-any read-legal (WARL) bits that implicitly modify the written value to restrict the CSR to legal values.
-This legalization must be applied to the SCR's address when reading or writing an SCR.
-If this results in the capability becoming unrepresentable then the tag is cleared, as per \insnriscvref{CSetAddr}.
-If a sealed capability is written to an SCR with WARL bits then the tag is cleared, even if the bits would be unchanged by legalization.
-
 \cref{tab:risc-v-special-capability-registers} lists the SCRs and their properties:
 \textbf{Reset} indicates the reset value as one of the capability roots defined in \cref{sec:capenc}.
 
@@ -177,12 +175,33 @@ \section{Special capability registers}
   }
 \end{table}
 
+The \MTCC{} and \MEPCC{} SCRs replace existing RISC-V CSRs \asm{mtvec} and \asm{mepcc} respectively.
+Attempting to access the legacy RISC-V CSR via the \asm{CSR*} instructions results in a Reserved Instruction exception.
+The special meaning associated with the CSR applies to the SCR's \caddress{} field and the value written is validated and legalized as follows:
+
+\begin{description}
+  \item[\MTCC{}] Only direct mode is suppported (not vectored). 
+  If either of the two least significant bits of the \caddress{} is set then they are cleared and the tag of the value written is cleared.
+  If the capability being written is sealed or does not have \cappermX{} then its tag is cleared.
+  \item[\MEPCC{}]
+  If the least significant bit of \caddress{} is set then it is cleared and the tag is cleared.
+  If the capability being written is sealed or does not have \cappermX{} then its tag is cleared.
+\end{description}
+
+These rules avoid potential problems due to legalisation where capabilities might become unrepresentable or sealed capabilties modified.
+
 \section{Changes to exception handling}
 
 Exception handling is the same as RISC-V except that \mtvec{} and \mepc{} are replaced by their equivalent SCRs.
-When taking an exception the current \PCC{}, with the address set to that of the trapping instruction, is placed in \MEPCC{}. \MTCC{} is then installed in \PCC{} and execution proceeds from the configured trap address according to the usual rules for \mtvec{}.
+
+When taking an exception the current \PCC{}, with the address set to that of the trapping instruction, is placed in \MEPCC{}.
+If the exception is a bounds violation on instruction fetch then the tag on \MEPCC{} is cleared.
+\MTCC{} is then installed in \PCC{} and execution proceeds from \MTCC.\caddress{}.
 When executing an \asm{MRET} instruction \MEPCC{} is moved to \PCC{} and execution proceeds from \MEPCC{}.\caddress{}.
 
+In either case if the new \PCC{} is untagged (due to an untagged \MEPCC{} or \MTCC{}) an CHERI tag violation exception is raised for the new \PC{}.
+In the case of an untagged \MTCC{} this will result in an unrecoverable exception loop.
+
 A new RISC-V exception code, 0x1C, is used for all CHERI specific exceptions, with a more detailed CHERI cause placed in \mtval{} as shown in \cref{fig-cheri-tval}.
 
 \label{subsubsec-cheri-tval}
@@ -605,14 +624,13 @@ \subsection{Representability checks}
 Note that although \insnriscvref{CJAL} and \insnriscvref{CJALR} also set the address on the link register, it is guaranteed to be representable because its \caddress{} can be at most equal to \PCC{}.\ctop{} given that the jump itself is in bounds.
 Therefore no representability check is required for these instructions.
 
-Similarly, the value placed in \MEPCC{} on exception should always be representable given that \PC{} is always in bounds (or equal to \PCC{}.\ctop{} in the case of stepping off the end of \PCC{}).
-One exception to this is if \MTCC{} is configured in vectored mode and a subsequent exception goes to a \PC{} that is out of the bounds of \MTCC{}.
-This would cause a \PCC{} bounds exception and in this case \MEPCC{} might not be representable, in which case its tag should be cleared.
-It may be preferable not to support vectored mode, although note that care should also be taken when legalizing \asm{mtvec} (\MTCC.\caddress{}) to ensure that this does not violate sealing or representability.
-legalization of \asm{mepc} (clearing the least significant bit) may also cause values read from \MEPCC{} to be unrepresentable if it has been written with an unaligned address.
-This includes the implicit read by \asm{MRET}.
-In these cases the unrepresentable \MEPCC{} that results from the \PCC{} bounds exception should have its tag cleared.
-\TODO{These cases are probably pretty annoying for hardware. Although less in keeping with RISC-V behavior it would probably be easier to clear tag if \MEPCC{} is written with an unaligned address.}
+Bounds exceptions on instruction fetch might result in an unrepresentable \MEPCC{}.
+To simplify hardware while preserving capability monotonicity the tag of \MEPCC{} is always cleared on instruction fetch bounds violations.
+This unrepresentability might mean that the decoded bounds of \MEPCC{} do not match the bounds of \PCC{} at the time of the exception,
+but \MEPCC{}.\caddress{} will contain the address of the faulting instruction or instruction fetch.
+
+Validation of \MTCC{} and \MEPCC{} in \insnriscvref{CSpecialRW} prevents potential unrepresentability due to the legalisation of \asm{mtvec} and \asm{mepc}.
+To simplify hardware these special registers are validated on write, with violations clearing the tag of the value stored (\cref{sec:scrs}).
 
 \subsection{The NULL capability}
 \label{sec:null}

src/cheri_addr_checks.sail

@@ -116,9 +116,9 @@ function ext_fetch_check_pc(start_pc, pc) = {
     if      not(PCC.tag)
     then    Ext_FetchAddr_Error(CapEx_TagViolation)
     else if isCapSealed(PCC)
-    then    Ext_FetchAddr_Error(CapEx_SealViolation)
+    then    internal_error(__FILE__, __LINE__, "PCC should never be sealed")
     else if not(PCC.permit_execute)
-    then    Ext_FetchAddr_Error(CapEx_PermitExecuteViolation)
+    then    internal_error(__FILE__, __LINE__, "PCC should always be executable")
     else if not(inCapBounds(PCC, pc, 2))
     then    Ext_FetchAddr_Error(CapEx_BoundsViolation)
     else    Ext_FetchAddr_OK(pc)
@@ -130,35 +130,34 @@ function ext_fetch_check_pc(start_pc, pc) = {
   }
 }
 
-function ext_handle_fetch_check_error(e : ext_fetch_addr_error) -> unit =
+function ext_handle_fetch_check_error(e : ext_fetch_addr_error) -> unit = {
+  if e == CapEx_BoundsViolation then {
+    // Always clear the tag on PCC when taking a bounds violation on fetch.
+    // This avoids having to do a representability check on MEPCC
+    // when the PC goes out of bounds.
+    PCC = clearTag(PCC);
+  };
   handle_cheri_pcc_exception(e)
+}
 
 /* CHERI control address checks */
 
 type ext_control_addr_error = (CapEx, capreg_idx)
 
 /* the control address is derived from a non-PC register, e.g. in JALR */
 function ext_control_check_addr(pc : xlenbits) -> Ext_ControlAddr_Check(ext_control_addr_error) = {
-  /* We are given the addr without any bit[0] clearing, so the addition
-   * below may include a set addr[0], and so the bounds checks should
-   * be accurate.
-   */
-  let target : xlenbits = [pc with 0=bitzero];
-  if   not(inCapBounds(PCC, target, min_instruction_bytes ()))
-  then Ext_ControlAddr_Error(CapEx_BoundsViolation, PCC_IDX)
-  else Ext_ControlAddr_OK(target)
+  // We used to do bounds check here but this is now performed only on
+  // instruction fetch
+  Ext_ControlAddr_OK(pc)
 }
 
 /* the control address is derived from the PC register, e.g. in JAL */
 function ext_control_check_pc(pc : xlenbits) -> Ext_ControlAddr_Check(ext_control_addr_error) = {
-  if   not(inCapBounds(PCC, pc, min_instruction_bytes ()))
-  then Ext_ControlAddr_Error(CapEx_BoundsViolation, PCC_IDX)
-  else Ext_ControlAddr_OK(pc)
+  Ext_ControlAddr_OK(pc)
 }
 
 function ext_handle_control_check_error(err : ext_control_addr_error) -> unit = {
-  let (capEx, regnum) = err;
-  handle_cheri_cap_exception(capEx, regnum)
+  internal_error(__FILE__, __LINE__, "ext_handle_control_check_error should be unreachable")
 }
 
 /* CHERI data address checks */

src/cheri_insts.sail

@@ -95,17 +95,20 @@ union clause ast = CJAL : (bits(21), regidx)
  * ## Exceptions
  *
  * An exception is raised if:
- *   - **PCC**.**address** $+$ *imm* $\lt$ **PCC**.**base**.
- *   - **PCC**.**address** $+$ *imm* $+$ min_instruction_bytes $\gt$ **PCC**.**top**.
  *   - **PCC**.**address** $+$ *imm* is unaligned, ignoring bit 0.
+ * 
+ * ## Notes
+ *   - This instruction no longer attempts to check that the destination is
+ *     within the bounds of PCC.  In that case an exception will be raised 
+ *     raised by the subsequent instruction fetch.  EPCC will have the new
+ *     PC as address but will have the tag cleared due to the possibility of 
+ *     creating an unrepresentable PCC.  The bounds of EPCC will be 
+ *     undefined.
  */
 function clause execute(CJAL(imm, cd)) = {
   let off : xlenbits = sign_extend(imm);
   let newPC = PC + off;
-  if not(inCapBounds(PCC, newPC, min_instruction_bytes())) then {
-    handle_cheri_cap_exception(CapEx_BoundsViolation, PCC_IDX);
-    RETIRE_FAIL
-  } else if newPC[1] == bitone & ~(haveRVC()) then {
+  if newPC[1] == bitone & ~(haveRVC()) then {
     handle_mem_exception(newPC,  E_Fetch_Addr_Align());
     RETIRE_FAIL
   } else {
@@ -133,10 +136,15 @@ union clause ast = CJALR : (bits(12), regidx, regidx)
  *   - *cs1* is sealed and is not a sentry.
  *   - *cs1* is a sentry and *imm* $\ne$ 0.
  *   - *cs1*.**perms** does not grant **Permit_Execute**.
- *   - *cs1*.**address** $+$ *imm* $\lt$ *cs1*.**base**.
- *   - *cs1*.**address** $+$ *imm* $+$ min_instruction_bytes $\gt$ *cs1*.**top**.
- *   - *cs1*.**base** is unaligned.
  *   - *cs1*.**address** $+$ *imm* is unaligned, ignoring bit 0.
+ *
+  * ## Notes
+ *   - This instruction no longer attempts to check that the destination is
+ *     within the bounds of PCC.  In that case an exception will be raised 
+ *     raised by the subsequent instruction fetch.  EPCC will have the new
+ *     PC as address but will have the tag cleared due to the possibility of 
+ *     creating an unrepresentable PCC.  The bounds of EPCC will be 
+ *     undefined.
  */
 function clause execute(CJALR(imm, cs1, cd)) = {
   let cs1_val = C(cs1);
@@ -151,9 +159,6 @@ function clause execute(CJALR(imm, cs1, cd)) = {
   } else if not (cs1_val.permit_execute) then {
     handle_cheri_reg_exception(CapEx_PermitExecuteViolation, cs1);
     RETIRE_FAIL
-  } else if not(inCapBounds(cs1_val, newPC, min_instruction_bytes())) then {
-    handle_cheri_reg_exception(CapEx_BoundsViolation, cs1);
-    RETIRE_FAIL
   } else if newPC[1] == bitone & ~(haveRVC()) then {
     handle_mem_exception(newPC,  E_Fetch_Addr_Align());
     RETIRE_FAIL
@@ -330,6 +335,10 @@ union clause ast = CSpecialRW : (regidx, screg, regidx)
  *   a separate two-operand CSpecialR instruction and interpret *cs1* being
  *   **C0** as a write of **NULL** if the need to use a temporary capability
  *   register proves to be overly problematic for software.
+ * 
+ * - MEPCC and MTCC are validated and legalized on write. Any invalid write will
+ *   cause the tag to be cleared which might result in a tag violation
+ *   on instruction fetch following MRET or exception.
  */
 function clause execute (CSpecialRW(cd, scr, cs1)) = {
   let specialExists : bool = match unsigned(scr) {
@@ -346,20 +355,37 @@ function clause execute (CSpecialRW(cd, scr, cs1)) = {
     handle_cheri_cap_exception(CapEx_AccessSystemRegsViolation, 0b1 @ scr);
     RETIRE_FAIL
   } else {
-    let cs1_val = C(cs1);
+    var cs1_val = C(cs1);
     C(cd) = match unsigned(scr) {
       28 => MTCC,
       29 => MTDC,
       30 => MScratchC,
-      31 => legalize_epcc(MEPCC),
+      31 => MEPCC,
       _  => {assert(false, "unreachable"); undefined}
     };
     if (cs1 != zeros()) then {
       match unsigned(scr) {
-        28 => MTCC = legalize_tcc(MTCC, cs1_val),
+        28 => {
+          /* Validate that the new MTCC is unsealed, executable and 
+             indicates direct trap mode */
+          let invalid = cs1_val.address[1..0] != 0b00 |
+            isCapSealed(cs1_val) |
+            not(cs1_val.permit_execute);
+          /* Legalize MTCC.address / mtvec */
+          cs1_val.address[1..0] = 0b00;
+          MTCC = clearTagIf(cs1_val, invalid)
+        },
         29 => MTDC = cs1_val,
         30 => MScratchC = cs1_val,
-        31 => MEPCC = cs1_val,
+        31 => {
+          /* Validate that new MEPCC is aligned, unsealed and executable */
+          let invalid = cs1_val.address[0] != bitzero |
+            isCapSealed(cs1_val) |
+            not(cs1_val.permit_execute);
+          /* Legalize MEPCC.address / mepc */
+          cs1_val.address[0] = bitzero;
+          MEPCC = clearTagIf(cs1_val, invalid)
+        },
         _  => assert(false, "unreachable")
       }
     };