Split ext_ptw into pieces and add documentation

It was somewhat annoying that CHERI would have had to track both
successful and erroneous occurrences within the same type.  Break the
failures out to their own form and, while here, attempt to write down my
understanding of the extension's information flow through vmem.

6 files changed, 43 insertions, 19 deletions

diff --git a/model/riscv_pte.sail b/model/riscv_pte.sail
index 08cedc5..360e5bc 100644
--- a/model/riscv_pte.sail
+++ b/model/riscv_pte.sail
@@ -30,11 +30,11 @@ function isInvalidPTE(p : pteAttribs, ext : extPte) -> bool = {
 
 union PTE_Check = {
   PTE_Check_Success : ext_ptw,
-  PTE_Check_Failure : ext_ptw
+  PTE_Check_Failure : (ext_ptw, ext_ptw_fail)
 }
 
 function to_pte_check(b : bool) -> PTE_Check =
-  if b then PTE_Check_Success(()) else PTE_Check_Failure(())
+  if b then PTE_Check_Success(()) else PTE_Check_Failure((), ())
 
 /* For extensions: this function gets the extension-available bits of the PTE in extPte,
  * and the accumulated information of the page-table-walk in ext_ptw.  It should return
diff --git a/model/riscv_ptw.sail b/model/riscv_ptw.sail
index a46a755..77364f5 100644
--- a/model/riscv_ptw.sail
+++ b/model/riscv_ptw.sail
@@ -28,7 +28,7 @@ overload to_str = {ptw_error_to_str}
  * walks during address translation; it typically works in conjunction
  * with any customization to checkPTEPermission().
  */
-function ext_get_ptw_error(ext_ptw : ext_ptw) -> PTW_Error =
+function ext_get_ptw_error(eptwf : ext_ptw_fail) -> PTW_Error =
   PTW_No_Permission()
 
 /* conversion of these translation/PTW failures into architectural exceptions */
diff --git a/model/riscv_types_ext.sail b/model/riscv_types_ext.sail
index 6562981..e935049 100644
--- a/model/riscv_types_ext.sail
+++ b/model/riscv_types_ext.sail
@@ -1,12 +1,36 @@
-/* accumulator for information collected during PTW */
-
-/* This type is an accumulator; it is carried through the page-table
- * walk, and folds in information along the walk, currently from the
- * PTE checks from each PTE that is processed along the way.
+/*
+ * Types used in supporting extensions for page-table walks
+ *
+ * There are three types involved:
+ *
+ *   An accumulator, passed down from the root to the leaves (ext_ptw)
+ *   Metadata returned with failed permissions checks (_fail)
+ *   Errors embedded within the PTW_Error union
+ *
+ * Information flow begins with init_ext_ptw (: ext_ptw) being routed, via the
+ * translateNN functions and/or walkNN functions, to the checkPTEPermission
+ * function, which is the intended point of interaction with extensions.
+ *
+ * checkPTEPermission may be called repeatedly, each call seeing the
+ * accumulator state generated by a successful result of the previous
+ * iteration.  On failure, this function is expected to generate, instead, a
+ * ext_ptw_fail value as well as a new accumulator value, both of which will
+ * be returned to the code calling into translation.
+ *
+ * If translation ultimately succeeds, the final accumulator state is captured
+ * and will be returned to the code calling into translation.
+ *
+ * If translation ultimately fails, the accumulator at the time of failure is
+ * also captured and returned to the caller.  The ext_ptw_fail value is used
+ * to generate the PTW_Error value, using ext_get_ptw_error; this allows the
+ * extension to generate both novel (PTW_Ext_Error) and existing (e.g.,
+ * (PTW_Invalid_PTE) PTW_Error values.
  */
-type ext_ptw = unit  /* No extensions for page-table-walks */
 
-let init_ext_ptw : ext_ptw = () /* initial value of the accumulator */
+type ext_ptw = unit
+let init_ext_ptw : ext_ptw = ()
+
+type ext_ptw_fail = unit
 
 /* This type can be used for custom errors for page-table-walks,
  * and values in this type are typically generated from the final
@@ -19,7 +43,7 @@ type ext_exc_type = unit /* No exception extensions */
 
 /* Default translation of PTW errors into exception annotations */
 function ext_translate_exception(e : ext_ptw_error) -> ext_exc_type =
-  e
+  e /* type pun because both are unit; extensions may need to override this */
 
 /* Default conversion of extension exceptions to bits */
 val ext_exc_type_to_bits : ext_exc_type -> exc_code
diff --git a/model/riscv_vmem_sv32.sail b/model/riscv_vmem_sv32.sail
index c025630..4923be5 100644
--- a/model/riscv_vmem_sv32.sail
+++ b/model/riscv_vmem_sv32.sail
@@ -47,9 +47,9 @@ function walk32(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = {
           }
         } else { /* leaf PTE */
           match checkPTEPermission(ac, priv, mxr, do_sum, pattr, ext_pte, ext_ptw) {
-            PTE_Check_Failure(ext_ptw) => {
+            PTE_Check_Failure(ext_ptw, ext_ptw_fail) => {
 /*            print("walk32: pte permission check failure"); */
-              PTW_Failure(ext_get_ptw_error(ext_ptw), ext_ptw)
+              PTW_Failure(ext_get_ptw_error(ext_ptw_fail), ext_ptw)
             },
             PTE_Check_Success(ext_ptw) => {
               if level > 0 then { /* superpage */
@@ -124,7 +124,7 @@ function translate32(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) =
       let  ext_pte : extPte = zeros(); // no reserved bits for extensions
       let  pteBits = Mk_PTE_Bits(pte.BITS());
       match checkPTEPermission(ac, priv, mxr, do_sum, pteBits, ext_pte, ext_ptw) {
-        PTE_Check_Failure(ext_ptw) => { TR_Failure(ext_get_ptw_error(ext_ptw), ext_ptw) },
+        PTE_Check_Failure(ext_ptw, ext_ptw_fail) => { TR_Failure(ext_get_ptw_error(ext_ptw_fail), ext_ptw) },
         PTE_Check_Success(ext_ptw) => {
           match update_PTE_Bits(pteBits, ac, ext_pte) {
             None()           => TR_Address(ent.pAddr | EXTZ(vAddr & ent.vAddrMask), ext_ptw),
diff --git a/model/riscv_vmem_sv39.sail b/model/riscv_vmem_sv39.sail
index a6f9908..81ef79f 100644
--- a/model/riscv_vmem_sv39.sail
+++ b/model/riscv_vmem_sv39.sail
@@ -41,9 +41,9 @@ function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = {
           }
         } else { /* leaf PTE */
           match checkPTEPermission(ac, priv, mxr, do_sum, pattr, ext_pte, ext_ptw) {
-	    PTE_Check_Failure(ext_ptw) => {
+	    PTE_Check_Failure(ext_ptw, ext_ptw_fail) => {
 /*            print("walk39: pte permission check failure"); */
-              PTW_Failure(ext_get_ptw_error(ext_ptw), ext_ptw)
+              PTW_Failure(ext_get_ptw_error(ext_ptw_fail), ext_ptw)
             },
             PTE_Check_Success(ext_ptw)  => {
               if level > 0 then { /* superpage */
@@ -118,7 +118,7 @@ function translate39(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) =
       let  ext_pte = pte.Ext();
       let  pteBits = Mk_PTE_Bits(pte.BITS());
       match checkPTEPermission(ac, priv, mxr, do_sum, pteBits, ext_pte, ext_ptw) {
-        PTE_Check_Failure(ext_ptw) => { TR_Failure(ext_get_ptw_error(ext_ptw), ext_ptw) },
+        PTE_Check_Failure(ext_ptw, ext_ptw_fail) => { TR_Failure(ext_get_ptw_error(ext_ptw_fail), ext_ptw) },
         PTE_Check_Success(ext_ptw) => {
           match update_PTE_Bits(pteBits, ac, ext_pte) {
             None()           => TR_Address(ent.pAddr | EXTZ(vAddr & ent.vAddrMask), ext_ptw),
diff --git a/model/riscv_vmem_sv48.sail b/model/riscv_vmem_sv48.sail
index 2fc149f..4f2dac5 100644
--- a/model/riscv_vmem_sv48.sail
+++ b/model/riscv_vmem_sv48.sail
@@ -41,9 +41,9 @@ function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = {
           }
         } else { /* leaf PTE */
           match checkPTEPermission(ac, priv, mxr, do_sum, pattr, ext_pte, ext_ptw) {
-            PTE_Check_Failure(ext_ptw) => {
+            PTE_Check_Failure(ext_ptw, ext_ptw_fail) => {
 /*            print("walk48: pte permission check failure"); */
-              PTW_Failure(ext_get_ptw_error(ext_ptw), ext_ptw)
+              PTW_Failure(ext_get_ptw_error(ext_ptw_fail), ext_ptw)
             },
 	    PTE_Check_Success(ext_ptw) => {
               if level > 0 then { /* superpage */