CAndPerms: permit clearing GL on sealed caps

archdoc/chap-changes.tex

@@ -45,5 +45,9 @@ \chapter{Version history}
       Instead, it merely requires that the otype of the sealed input is within bounds to yield a tagged result.
       The address of a sealing-root capability is now meaningful only to \rvcheriasminsnref{CSeal}.
     \item[\ghissue{72},\ghpr{74}] Introduce \rvcheriasminsnref{CSetBoundsRoundDown} to facilitate constructing representable slices of buffers.
+    \item[\ghissue{70},\ghpr{83}] \rvcheriasminsnref{CAndPerm} can now clear \cappermG on sealed caps, so long as that is the only bit being cleared.
+      Previously, this was possible by round-tripping to memory, loading back through an authority lacking \cappermILG(recall \ghpr{44} and \ghissue{14} above), but not directly as a register-to-register operation.
+      Presently, we require that the mask provided to \rvcheriasminsnref{CAndPerm} be all-1s except possibly \cappermG;
+      that is, feeding the result of \rvcheriasminsnref{CGetPerm} on a sealed capability to \rvcheriasminsnref{CAndPerm} will still clear the tag of the result.
   \end{description}
 \end{description}

archdoc/chap-encoding-sail.tex

@@ -42,34 +42,30 @@ \section{SMT validation of properties of the capability encoding}
 
 Some helper functions are used in the Sail properties:
 
-\medskip
-\sailRISCVfn{encodeDecode}
-
-\medskip
-\sailRISCVfn{capEncodable}
-
-The following functions have been checked to return true for all inputs.
-
-\medskip
-\sailRISCVfn{prop\_decEnc}
-
-\medskip
-\sailRISCVfn{prop\_andperms}
+\begin{itemize}
+  \item \sailRISCVfn{encodeDecode}
+  \item \sailRISCVfn{capEncodable}
+\end{itemize}
 
-\medskip
-\sailRISCVfn{prop\_setbounds}
+The following nullary properties of the encoding hold.
 
-\medskip
-\sailRISCVfn{prop\_setbounds\_monotonic}
+\begin{itemize}
+  \item \sailRISCVfn{prop\_nullzero}
+  \item \sailRISCVfn{prop\_null\_noperms}
+  \item \sailRISCVfn{prop\_mem\_root}
+  \item \sailRISCVfn{prop\_exe\_root}
+  \item \sailRISCVfn{prop\_seal\_root}
+\end{itemize}
 
-\medskip
-\sailRISCVfn{prop\_setaddr}
-
-\medskip
-\sailRISCVfn{prop\_repbounds\_c}
-
-\medskip
-\sailRISCVfn{prop\_repbounds}
+The following functions have been checked to return true for all inputs.
 
-\medskip
-\sailRISCVfn{prop\_crrl\_cram}
+\begin{itemize}
+  \item \sailRISCVfn{prop\_decEnc}
+  \item \sailRISCVfn{prop\_andperms}
+  \item \sailRISCVfn{prop\_setbounds}
+  \item \sailRISCVfn{prop\_setbounds\_monotonic}
+  \item \sailRISCVfn{prop\_setaddr}
+  \item \sailRISCVfn{prop\_repbounds\_c}
+  \item \sailRISCVfn{prop\_repbounds}
+  \item \sailRISCVfn{prop\_crrl\_cram}
+\end{itemize}

properties/props.sail

@@ -19,23 +19,36 @@ $property
  * Check that null_cap as defined in the Sail encodes to all zeros.
  */
 function prop_nullzero() -> bool = {
-    capEncodable(null_cap) & (capToBits(null_cap) == zeros()) & (null_cap.tag == false)
+    capEncodable(null_cap)
+  & (capToBits(null_cap) == zeros())
+  & (null_cap.tag == false)
 }
 
 $property
-function prop_mem_root() -> bool = {
-    capEncodable(root_cap_mem)
+/*!
+ * Check that null_cap has no set permission bits.
+ */
+function prop_null_noperms() -> bool = {
+  getCapPerms(null_cap) == zeros()
 }
 
 $property
-function prop_exe_root() -> bool = {
-    capEncodable(root_cap_exe)
-}
+/*!
+ * Check that [root_cap_mem] is encodable
+ */
+function prop_mem_root() -> bool = { capEncodable(root_cap_mem) }
 
 $property
-function prop_seal_root() -> bool = {
-    capEncodable(root_cap_seal)
-}
+/*!
+ * Check that [root_cap_exe] is encodable
+ */
+function prop_exe_root() -> bool = { capEncodable(root_cap_exe) }
+
+$property
+/*!
+ * Check that [root_cap_seal] is encodable
+ */
+function prop_seal_root() -> bool = { capEncodable(root_cap_seal) }
 
 $property
 /*!

src/cheri_insts.sail

@@ -410,7 +410,8 @@ union clause ast = CAndPerm : (regidx, regidx, regidx)
  * previous value and bits 0 to [cap_perms_width]-1 of integer register *rs2*.
  * If the resulting set of permissions cannot be represented by the capability
  * encoding then the result will have a (possibly empty) subset of the ANDed
- * permissions. If *cs1* was sealed then *cd*.**tag** is cleared.
+ * permissions. If *cs1* was sealed and *rs2* codes for clearing anything other
+ * than Permit_Global, then *cd*.**tag** is cleared.
  */
 function clause execute(CAndPerm(cd, cs1, rs2)) = {
   let cs1_val = C(cs1);
@@ -419,8 +420,23 @@ function clause execute(CAndPerm(cd, cs1, rs2)) = {
   let perms = getCapPerms(cs1_val);
   let mask = truncate(rs2_val, cap_perms_width);
 
-  let inCap = clearTagIfSealed(cs1_val);
-  let newCap = setCapPerms(inCap, (perms & mask));
+  let newperms = perms & mask;
+
+  /*
+   * CAndPerm on a sealed cap clears the tag unless the mask is all ones or
+   * has *only* the global permission clear.
+   *
+   * Here, perm_global is a bit vector (in the architectural format used by
+   * [CAndPerm] and [CGetPerm]) of all zeros except for the global permission
+   * bit.  Its formulation here relies on null_cap having no asserted
+   * permissions (which we verify in our SMT properties; see
+   * [prop_null_noperms]).
+   */
+  let perm_global = getCapPerms({ null_cap with global = true });
+  let inCap = clearTagIf(cs1_val,
+                isCapSealed(cs1_val) & ((mask | perm_global) == ones()));
+
+  let newCap = setCapPerms(inCap, newperms);
 
   C(cd) = newCap;
   RETIRE_SUCCESS