/*=======================================================================================*/
/*  This Sail RISC-V architecture model, comprising all files and                        */
/*  directories except where otherwise noted is subject the BSD                          */
/*  two-clause license in the LICENSE file.                                              */
/*                                                                                       */
/*  SPDX-License-Identifier: BSD-2-Clause                                                */
/*=======================================================================================*/

/*
 * 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
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
 * result of the ext_ptw at the end of the walk.
 */
type ext_ptw_error = unit /* No extensions for page-table-walk errors */

/* This type supports extensions to the exceptions defined in the ISA. */
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 /* 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
function ext_exc_type_to_bits(e) = 0x18 /* First code for a custom extension */

/* Default conversion of extension exceptions to integers */
val num_of_ext_exc_type : ext_exc_type -> {'n, (0 <= 'n < xlen). int('n)}
function num_of_ext_exc_type(e) = 24 /* First code for a custom extension */

/* Default conversion of extension exceptions to strings */
val ext_exc_type_to_str : ext_exc_type -> string
function ext_exc_type_to_str(e) = "extension-exception"