Merge pull request #64 from nwf:pte-check-split with minor edits.

Split ext_ptw into pieces and add documentation

6 files changed, 46 insertions, 19 deletions

diff --git a/model/riscv_pte.sail b/model/riscv_pte.sail
index 6f170ae..501bc5c 100644
--- a/model/riscv_pte.sail
+++ b/model/riscv_pte.sail
@@ -41,11 +41,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..48b8c41 100644
--- a/model/riscv_types_ext.sail
+++ b/model/riscv_types_ext.sail
@@ -1,12 +1,39 @@
-/* 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 (ext_ptw_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 will be called repeatedly at each PTE, each call
+ * seeing the accumulator state generated by a successful result of
+ * the previous call.  On failure, this function is expected to
+ * generate, instead, an 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 and the ext_ptw_fail value are returned to the caller.  The
+ * ext_ptw_fail value is used to generate a PTW_Error value by calling
+ * ext_get_ptw_error; this allows the extension to generate both novel
+ * (e.g., 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 +46,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 cd1d51e..1b19679 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 */