diff options
-rw-r--r-- | model/riscv_pte.sail | 4 | ||||
-rw-r--r-- | model/riscv_ptw.sail | 2 | ||||
-rw-r--r-- | model/riscv_types_ext.sail | 43 | ||||
-rw-r--r-- | model/riscv_vmem_sv32.sail | 6 | ||||
-rw-r--r-- | model/riscv_vmem_sv39.sail | 6 | ||||
-rw-r--r-- | model/riscv_vmem_sv48.sail | 4 |
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 */ |