/* Machine-mode and supervisor-mode state definitions and operations. */

/* privilege level */

register cur_privilege : Privilege

/* current instruction bits, used for illegal instruction exceptions */

register cur_inst : xlenbits

/* State projections
 *
 * Some machine state is processed via projections from machine-mode views to
 * views from lower privilege levels.  So, for e.g. when mstatus is read from
 * lower privilege levels, we use 'lowering_' projections:
 *
 *   mstatus  ->  sstatus  ->  ustatus
 *
 * Similarly, when machine state is written from lower privileges, that state is
 * lifted into the appropriate value for the machine-mode state.
 *
 *   ustatus  ->  sstatus  ->  mstatus
 *
 * In addition, several fields in machine state registers are WARL or WLRL,
 * requiring that values written to the registers be legalized.  For each such
 * register, there will be an associated 'legalize_' function.  These functions
 * will need to be supplied externally, and will depend on the legal values
 * supported by a platform/implementation (or misa).  The legalize_ functions
 * generate a legal value from the current value and the written value.  In more
 * complex cases, they will also implicitly read the current values of misa,
 * mstatus, etc.
 *
 * Each register definition below is followed by custom projections
 * and choice of legalizations if needed.  For now, we typically
 * implement the simplest legalize_ alternatives.
 */


/* M-mode registers */

bitfield Misa : bits(64) = {
  MXL  : 63 .. 62,

  Z    : 25,
  Y    : 24,
  X    : 23,
  W    : 22,
  V    : 21,
  U    : 20,
  T    : 19,
  S    : 18,
  R    : 17,
  Q    : 16,
  P    : 15,
  O    : 14,
  N    : 13,
  M    : 12,
  L    : 11,
  K    : 10,
  J    : 9,
  I    : 8,
  H    : 7,
  G    : 6,
  F    : 5,
  E    : 4,
  D    : 3,
  C    : 2,
  B    : 1,
  A    : 0
}
register misa : Misa

function legalize_misa(m : Misa, v : xlenbits) -> Misa = {
  /* Allow modifications to C. */
  let v = Mk_Misa(v);
  // Suppress changing C if nextPC would become misaligned.
  if   v.C() == false & nextPC[1] == true
  then m
  else update_C(m, v.C())
}

bitfield Mstatus : bits(64) = {
  SD   : 63,

  SXL  : 35 .. 34,
  UXL  : 33 .. 32,

  TSR  : 22,
  TW   : 21,
  TVM  : 20,
  MXR  : 19,
  SUM  : 18,
  MPRV : 17,

  XS   : 16 .. 15,
  FS   : 14 .. 13,

  MPP  : 12 .. 11,
  SPP  : 8,

  MPIE : 7,
  SPIE : 5,
  UPIE : 4,

  MIE  : 3,
  SIE  : 1,
  UIE  : 0
}
register mstatus : Mstatus

function legalize_mstatus(o : Mstatus, v : xlenbits) -> Mstatus = {
  let m : Mstatus = Mk_Mstatus(v);
  /* We don't have any extension context yet. */
  let m = update_XS(m, extStatus_to_bits(Off));
  let m = update_SD(m, extStatus_of_bits(m.FS()) == Dirty
                     | extStatus_of_bits(m.XS()) == Dirty);
  /* For now, we don't allow SXL and UXL to be changed, for Spike compatibility. */
  let m = update_SXL(m, o.SXL());
  let m = update_UXL(m, o.UXL());
  /* Hardwired to zero in the absence of 'N'. */
  let m = update_UPIE(m, false);
  let m = update_UIE(m, false);
  m
}

/* architecture and extension checks */

function cur_Architecture() -> Architecture = {
  let a : arch_xlen =
    match (cur_privilege) {
      Machine    => misa.MXL(),
      Supervisor => mstatus.SXL(),
      User       => mstatus.UXL()
    };
  match architecture(a) {
    Some(a) => a,
    None()  => internal_error("Invalid current architecture")
  }
}

function in32BitMode() -> bool = {
  cur_Architecture() == RV32
}

function haveAtomics() -> bool = { misa.A() == true }
function haveRVC()     -> bool = { misa.C() == true }
function haveMulDiv()  -> bool = { misa.M() == true }
function haveFP()      -> bool = { misa.F() == true | misa.D() == true }

/* interrupt processing state */

bitfield Minterrupts : bits(64) = {
  MEI : 11, /* external interrupts */
  SEI : 9,
  UEI : 8,

  MTI : 7,  /* timers interrupts */
  STI : 5,
  UTI : 4,

  MSI : 3,  /* software interrupts */
  SSI : 1,
  USI : 0,
}
register mip     : Minterrupts /* Pending */
register mie     : Minterrupts /* Enabled */
register mideleg : Minterrupts /* Delegation to S-mode */

function legalize_mip(o : Minterrupts, v : xlenbits) -> Minterrupts = {
  /* The only writable bits are the S-mode bits, and with the 'N'
   * extension, the U-mode bits. */
  let v = Mk_Minterrupts(v);
  let m = update_SEI(o, v.SEI());
  let m = update_STI(m, v.STI());
  let m = update_SSI(m, v.SSI());
  m
}

function legalize_mie(o : Minterrupts, v : xlenbits) -> Minterrupts = {
  let v = Mk_Minterrupts(v);
  let m = update_MEI(o, v.MEI());
  let m = update_MTI(m, v.MTI());
  let m = update_MSI(m, v.MSI());
  let m = update_SEI(m, v.SEI());
  let m = update_STI(m, v.STI());
  let m = update_SSI(m, v.SSI());
  /* The U-mode bits will be modified if we have the 'N' extension. */
  m
}

function legalize_mideleg(o : Minterrupts, v : xlenbits) -> Minterrupts = {
  /* M-mode interrupt delegation bits "should" be hardwired to 0. */
  /* FIXME: needs verification against eventual spec language. */
  let m = Mk_Minterrupts(v);
  let m = update_MEI(m, false);
  let m = update_MTI(m, false);
  let m = update_MSI(m, false);
  m
}

/* exception processing state */

bitfield Medeleg : bits(64) = {
  SAMO_Page_Fault   : 15,
  Load_Page_Fault   : 13,
  Fetch_Page_Fault  : 12,
  MEnvCall          : 10,
  SEnvCall          : 9,
  UEnvCall          : 8,
  SAMO_Access_Fault : 7,
  SAMO_Addr_Align   : 6,
  Load_Access_Fault : 5,
  Load_Addr_Align   : 4,
  Breakpoint        : 3,
  Illegal_Instr     : 2,
  Fetch_Access_Fault: 1,
  Fetch_Addr_Align  : 0
}
register medeleg : Medeleg  /* Delegation to S-mode */

function legalize_medeleg(o : Medeleg, v : xlenbits) -> Medeleg = {
  let m = Mk_Medeleg(v);
  /* M-EnvCalls delegation is not supported */
  let m = update_MEnvCall(m, false);
  m
}

/* registers for trap handling */

bitfield Mtvec : bits(64) = {
  Base : 63 .. 2,
  Mode :  1 .. 0
}
register mtvec : Mtvec  /* Trap Vector */

function legalize_tvec(o : Mtvec, v : xlenbits) -> Mtvec = {
 let v = Mk_Mtvec(v);
 match (trapVectorMode_of_bits(v.Mode())) {
   TV_Direct => v,
   TV_Vector => v,
   _         => update_Mode(v, o.Mode())
 }
}

bitfield Mcause : bits(64) = {
  IsInterrupt : 63,
  Cause       : 62 .. 0
}
register mcause : Mcause

/* Interpreting the trap-vector address */
function tvec_addr(m : Mtvec, c : Mcause) -> option(xlenbits) = {
  let base : xlenbits = m.Base() @ 0b00;
  match (trapVectorMode_of_bits(m.Mode())) {
    TV_Direct => Some(base),
    TV_Vector => if   c.IsInterrupt() == true
                 then Some(base + (EXTZ(c.Cause()) << 0b10))
                 else Some(base),
    TV_Reserved => None()
  }
}

/* Exception PC */

register mepc : xlenbits

// legalizing writes to xepc
function legalize_xepc(v : xlenbits) -> xlenbits = {
  v & EXTS(if haveRVC() then 0b110 else 0b100)
}

// masking for reads to xepc
function pc_alignment_mask() -> xlenbits =
  ~(EXTZ(if misa.C() == true then 0b00 else 0b10))

/* auxiliary exception registers */

register mtval    : xlenbits
register mscratch : xlenbits

/* counters */

bitfield Counteren : bits(32) = {
  HPM  : 31 .. 3,
  IR   : 2,
  TM   : 1,
  CY   : 0
}

register mcounteren : Counteren
register scounteren : Counteren

function legalize_mcounteren(c : Counteren, v : xlenbits) -> Counteren = {
  /* no HPM counters yet */
  let c = update_IR(c, v[2]);
  let c = update_TM(c, v[1]);
  let c = update_CY(c, v[0]);
  c
}

function legalize_scounteren(c : Counteren, v : xlenbits) -> Counteren = {
  /* no HPM counters yet */
  let c = update_IR(c, v[2]);
  let c = update_TM(c, v[1]);
  let c = update_CY(c, v[0]);
  c
}

register mcycle : xlenbits
register mtime : xlenbits

/* minstret
 *
 * minstret is an architectural register, and can be written to.  The
 * spec says that minstret increments on instruction retires need to
 * occur before any explicit writes to instret.  However, in our
 * simulation loop, we need to execute an instruction to find out
 * whether it retired, and hence can only increment instret after
 * execution.  To avoid doing this in the case minstret was explicitly
 * written to, we track writes to it in a separate model-internal
 * register.
 */
register minstret : xlenbits
register minstret_written : bool

function retire_instruction() -> unit = {
  if   minstret_written == true
  then minstret_written = false
  else minstret = minstret + 1
}

/* informational registers */
register mvendorid : xlenbits
register mimpid : xlenbits
register marchid : xlenbits
/* TODO: this should be readonly, and always 0 for now */
register mhartid : xlenbits

/* physical memory protection configuration */
register pmpaddr0 : xlenbits
register pmpcfg0 : xlenbits


/* S-mode registers */

/* sstatus reveals a subset of mstatus */
bitfield Sstatus : bits(64) = {
  SD   : 63,
  UXL  : 33 .. 32,
  MXR  : 19,
  SUM  : 18,
  XS   : 16 .. 15,
  FS   : 14 .. 13,
  SPP  : 8,
  SPIE : 5,
  UPIE : 4,
  SIE  : 1,
  UIE  : 0
}
/* This is a view, so there is no register defined. */
function lower_mstatus(m : Mstatus) -> Sstatus = {
  let s = Mk_Sstatus(EXTZ(0b0));
  let s = update_SD(s, m.SD());
  let s = update_UXL(s, m.UXL());
  let s = update_MXR(s, m.MXR());
  let s = update_SUM(s, m.SUM());
  let s = update_XS(s, m.XS());
  let s = update_FS(s, m.FS());
  let s = update_SPP(s, m.SPP());
  let s = update_SPIE(s, m.SPIE());
  let s = update_UPIE(s, m.UPIE());
  let s = update_SIE(s, m.SIE());
  let s = update_UIE(s, m.UIE());
  s
}

function lift_sstatus(m : Mstatus, s : Sstatus) -> Mstatus = {
  let m = update_SD(m, s.SD());
  // FIXME: This should be parameterized by a platform setting.  For now, match spike.
  // let m = update_UXL(m, s.UXL());
  let m = update_MXR(m, s.MXR());
  let m = update_SUM(m, s.SUM());
  let m = update_XS(m, s.XS());
  let m = update_FS(m, s.FS());
  let m = update_SPP(m, s.SPP());
  let m = update_SPIE(m, s.SPIE());
  let m = update_UPIE(m, s.UPIE());
  let m = update_SIE(m, s.SIE());
  let m = update_UIE(m, s.UIE());
  m
}

function legalize_sstatus(m : Mstatus, v : xlenbits) -> Mstatus = {
  lift_sstatus(m, Mk_Sstatus(v))
}

bitfield Sedeleg : bits(64) = {
  UEnvCall          : 8,
  SAMO_Access_Fault : 7,
  SAMO_Addr_Align   : 6,
  Load_Access_Fault : 5,
  Load_Addr_Align   : 4,
  Breakpoint        : 3,
  Illegal_Instr     : 2,
  Fetch_Access_Fault: 1,
  Fetch_Addr_Align  : 0
}
register sedeleg : Sedeleg

function legalize_sedeleg(s : Sedeleg, v : xlenbits) -> Sedeleg = {
  Mk_Sedeleg(EXTZ(v[8..0]))
}

bitfield Sinterrupts : bits(64) = {
  SEI : 9,  /* external interrupts */
  UEI : 8,

  STI : 5,  /* timers interrupts */
  UTI : 4,

  SSI : 1,  /* software interrupts */
  USI : 0
}

/* Provides the sip read view of mip as delegated by mideleg. */
function lower_mip(m : Minterrupts, d : Minterrupts) -> Sinterrupts = {
  let s : Sinterrupts = Mk_Sinterrupts(EXTZ(0b0));
  let s = update_SEI(s, m.SEI() & d.SEI());
  let s = update_STI(s, m.STI() & d.STI());
  let s = update_SSI(s, m.SSI() & d.SSI());

  let s = update_UEI(s, m.UEI() & d.UEI());
  let s = update_UTI(s, m.UTI() & d.UTI());
  let s = update_USI(s, m.USI() & d.USI());
  s
}
/* Provides the sie read view of mie as delegated by mideleg. */
function lower_mie(m : Minterrupts, d : Minterrupts) -> Sinterrupts = {
  let s : Sinterrupts = Mk_Sinterrupts(EXTZ(0b0));
  let s = update_SEI(s, m.SEI() & d.SEI());
  let s = update_STI(s, m.STI() & d.STI());
  let s = update_SSI(s, m.SSI() & d.SSI());
  let s = update_UEI(s, m.UEI() & d.UEI());
  let s = update_UTI(s, m.UTI() & d.UTI());
  let s = update_USI(s, m.USI() & d.USI());
  s
}
/* Provides the sip write view of mip as delegated by mideleg. */
function lift_sip(o : Minterrupts, d : Minterrupts, s : Sinterrupts) -> Minterrupts = {
  let m : Minterrupts = o;
  let m = update_SSI(m, s.SSI() & d.SSI());
  let m = update_UEI(m, m.UEI() & d.UEI());
  let m = update_USI(m, m.USI() & d.USI());
  m
}
function legalize_sip(m : Minterrupts, d : Minterrupts, v : xlenbits) -> Minterrupts = {
  lift_sip(m, d, Mk_Sinterrupts(v))
}
/* Provides the sie write view of mie as delegated by mideleg. */
function lift_sie(o : Minterrupts, d : Minterrupts, s : Sinterrupts) -> Minterrupts = {
  let m : Minterrupts = o;
  let m = if d.SEI() == true then update_SEI(m, s.SEI()) else m;
  let m = if d.STI() == true then update_STI(m, s.STI()) else m;
  let m = if d.SSI() == true then update_SSI(m, s.SSI()) else m;
  let m = if d.UEI() == true then update_UEI(m, s.UEI()) else m;
  let m = if d.UTI() == true then update_UTI(m, s.UTI()) else m;
  let m = if d.USI() == true then update_USI(m, s.USI()) else m;
  m
}
function legalize_sie(m : Minterrupts, d : Minterrupts, v : xlenbits) -> Minterrupts = {
  lift_sie(m, d, Mk_Sinterrupts(v))
}

register sideleg : Sinterrupts

/* s-mode address translation and protection (satp) */
bitfield Satp64 : bits(64) = {
  Mode : 63 .. 60,
  Asid : 59 .. 44,
  PPN  : 43 .. 0
}
register satp : xlenbits

function legalize_satp(a : Architecture, o : xlenbits, v : xlenbits) -> xlenbits = {
  let s = Mk_Satp64(v);
  match satpMode_of_bits(a, s.Mode()) {
    None()     => o,
    Some(Sv32) => o,  /* Sv32 is unsupported for now */
    Some(_)    => s.bits()
  }
}

/* other supervisor state */
register stvec    : Mtvec
register sscratch : xlenbits
register sepc     : xlenbits
register scause   : Mcause
register stval    : xlenbits

/* disabled trigger/debug module */
register tselect : xlenbits

/* CSR names */

val cast csr_name : csreg -> string
function csr_name(csr) = {
  match (csr) {
    /* user trap setup */
    0x000  => "ustatus",
    0x004  => "uie",
    0x005  => "utvec",
    /* user floating-point context */
    0x001  => "fflags",
    0x002  => "frm",
    0x003  => "fcsr",
    /* counter/timers */
    0xC00  => "cycle",
    0xC01  => "time",
    0xC02  => "instret",
    0xC80  => "cycleh",
    0xC81  => "timeh",
    0xC82  => "instreth",
    /* TODO: other hpm counters */
    /* supervisor trap setup */
    0x100  => "sstatus",
    0x102  => "sedeleg",
    0x103  => "sideleg",
    0x104  => "sie",
    0x105  => "stvec",
    0x106  => "scounteren",
    /* supervisor trap handling */
    0x140  => "sscratch",
    0x141  => "sepc",
    0x142  => "scause",
    0x143  => "stval",
    0x144  => "sip",
    /* supervisor protection and translation */
    0x180  => "satp",
    /* machine information registers */
    0xF11  => "mvendorid",
    0xF12  => "marchid",
    0xF13  => "mimpid",
    0xF14  => "mhartid",
    /* machine trap setup */
    0x300  => "mstatus",
    0x301  => "misa",
    0x302  => "medeleg",
    0x303  => "mideleg",
    0x304  => "mie",
    0x305  => "mtvec",
    0x306  => "mcounteren",
    /* machine trap handling */
    0x340  => "mscratch",
    0x341  => "mepc",
    0x342  => "mcause",
    0x343  => "mtval",
    0x344  => "mip",

    0x3A0  => "pmpcfg0",
    0x3B0  => "pmpaddr0",
    /* TODO: machine protection and translation */
    /* machine counters/timers */
    0xB00  => "mcycle",
    0xB02  => "minstret",
    0xB80  => "mcycleh",
    0xB82  => "minstreth",
    /* TODO: other hpm counters and events */
    /* trigger/debug */
    0x7a0  => "tselect",
    _      => "UNKNOWN"
  }
}

mapping csr_name_map : csreg <-> string = {
    /* user trap setup */
    0x000  <-> "ustatus",
    0x004  <-> "uie",
    0x005  <-> "utvec",
    /* user trap handling */
    0x040  <-> "uscratch",
    0x041  <-> "uepc",
    0x042  <-> "ucause",
    0x043  <-> "utval",
    0x044  <-> "uip",
    /* user floating-point context */
    0x001  <-> "fflags",
    0x002  <-> "frm",
    0x003  <-> "fcsr",
    /* counter/timers */
    0xC00  <-> "cycle",
    0xC01  <-> "time",
    0xC02  <-> "instret",
    0xC80  <-> "cycleh",
    0xC81  <-> "timeh",
    0xC82  <-> "instreth",
    /* TODO: other hpm counters */
    /* supervisor trap setup */
    0x100  <-> "sstatus",
    0x102  <-> "sedeleg",
    0x103  <-> "sideleg",
    0x104  <-> "sie",
    0x105  <-> "stvec",
    0x106  <-> "scounteren",
    /* supervisor trap handling */
    0x140  <-> "sscratch",
    0x141  <-> "sepc",
    0x142  <-> "scause",
    0x143  <-> "stval",
    0x144  <-> "sip",
    /* supervisor protection and translation */
    0x180  <-> "satp",
    /* machine information registers */
    0xF11  <-> "mvendorid",
    0xF12  <-> "marchid",
    0xF13  <-> "mimpid",
    0xF14  <-> "mhartid",
    /* machine trap setup */
    0x300  <-> "mstatus",
    0x301  <-> "misa",
    0x302  <-> "medeleg",
    0x303  <-> "mideleg",
    0x304  <-> "mie",
    0x305  <-> "mtvec",
    0x306  <-> "mcounteren",
    /* machine trap handling */
    0x340  <-> "mscratch",
    0x341  <-> "mepc",
    0x342  <-> "mcause",
    0x343  <-> "mtval",
    0x344  <-> "mip",
    /* machine protection and translation */
    0x3A0  <-> "pmpcfg0",
    0x3A1  <-> "pmpcfg1",
    0x3A2  <-> "pmpcfg2",
    0x3A3  <-> "pmpcfg3",
    0x3B0  <-> "pmpaddr0",
    0x3B1  <-> "pmpaddr1",
    0x3B2  <-> "pmpaddr2",
    0x3B3  <-> "pmpaddr3",
    0x3B4  <-> "pmpaddr4",
    0x3B5  <-> "pmpaddr5",
    0x3B6  <-> "pmpaddr6",
    0x3B7  <-> "pmpaddr7",
    0x3B8  <-> "pmpaddr8",
    0x3B9  <-> "pmpaddr9",
    0x3BA  <-> "pmpaddr10",
    0x3BB  <-> "pmpaddr11",
    0x3BC  <-> "pmpaddr12",
    0x3BD  <-> "pmpaddr13",
    0x3BE  <-> "pmpaddr14",
    0x3BF  <-> "pmpaddr15",
    /* machine counters/timers */
    0xB00  <-> "mcycle",
    0xB02  <-> "minstret",
    0xB80  <-> "mcycleh",
    0xB82  <-> "minstreth",
    /* TODO: other hpm counters and events */
    /* trigger/debug */
    0x7a0  <-> "tselect",
    0x7a1  <-> "tdata1",
    0x7a2  <-> "tdata2",
    0x7a3  <-> "tdata3"

    /* numeric fallback */
    /* reg    <-> hex_bits_12(reg) */
 }


/* CSR access control */

function csrAccess(csr : csreg) -> csrRW = csr[11..10]
function csrPriv(csr : csreg) -> priv_level = csr[9..8]

function is_CSR_defined (csr : bits(12), p : Privilege) -> bool =
  match (csr) {
    /* machine mode: informational */
    0xf11 => p == Machine, // mvendorid
    0xf12 => p == Machine, // marchdid
    0xf13 => p == Machine, // mimpid
    0xf14 => p == Machine, // mhartid
    /* machine mode: trap setup */
    0x300 => p == Machine, // mstatus
    0x301 => p == Machine, // misa
    0x302 => p == Machine, // medeleg
    0x303 => p == Machine, // mideleg
    0x304 => p == Machine, // mie
    0x305 => p == Machine, // mtvec
    0x306 => p == Machine, // mcounteren
    /* machine mode: trap handling */
    0x340 => p == Machine, // mscratch
    0x341 => p == Machine, // mepc
    0x342 => p == Machine, // mcause
    0x343 => p == Machine, // mtval
    0x344 => p == Machine, // mip

    0x3A0 => p == Machine, // pmpcfg0
    0x3B0 => false, // (Disabled for Spike compatibility)
//  0x3B0 => p == Machine, // pmpaddr0

    /* supervisor mode: trap setup */
    0x100 => p == Machine | p == Supervisor, // sstatus
    0x102 => p == Machine | p == Supervisor, // sedeleg
    0x103 => p == Machine | p == Supervisor, // sideleg
    0x104 => p == Machine | p == Supervisor, // sie
    0x105 => p == Machine | p == Supervisor, // stvec
    0x106 => p == Machine | p == Supervisor, // scounteren

    /* supervisor mode: trap handling */
    0x140 => p == Machine | p == Supervisor, // sscratch
    0x141 => p == Machine | p == Supervisor, // sepc
    0x142 => p == Machine | p == Supervisor, // scause
    0x143 => p == Machine | p == Supervisor, // stval
    0x144 => p == Machine | p == Supervisor, // sip

    /* supervisor mode: address translation */
    0x180 => p == Machine | p == Supervisor, // satp

    /* disabled trigger/debug module */
    0x7a0 => p == Machine,

    _     => false
  }

val check_CSR_access : (csrRW, priv_level, Privilege, bool) -> bool
function check_CSR_access(csrrw, csrpr, p, isWrite) =
    (~ (isWrite == true & csrrw == 0b11))  /* read/write */
  & (privLevel_to_bits(p) >=_u csrpr)      /* privilege */

function check_TVM_SATP(csr : csreg, p : Privilege) -> bool =
  ~ (csr == 0x180 & p == Supervisor & mstatus.TVM() == true)

function check_Counteren(csr : csreg, p : Privilege) -> bool =
  match(csr, p) {
    (0xC00, Supervisor) => mcounteren.CY() == true,
    (0xC01, Supervisor) => mcounteren.TM() == true,
    (0xC02, Supervisor) => mcounteren.IR() == true,

    (0xC00, User) => scounteren.CY() == true,
    (0xC01, User) => scounteren.TM() == true,
    (0xC02, User) => scounteren.IR() == true,

    (_, _) => /* no HPM counters for now */
              if   0xC03 <=_u csr & csr <=_u 0xC1F
              then false
              else true
  }

function check_CSR(csr : csreg, p : Privilege, isWrite : bool) -> bool =
    is_CSR_defined(csr, p)
  & check_CSR_access(csrAccess(csr), csrPriv(csr), p, isWrite)
  & check_TVM_SATP(csr, p)
  & check_Counteren(csr, p)

/* Reservation handling for LR/SC.
 *
 * The reservation state is maintained external to the model since the
 * reservation behavior is platform-specific anyway and maintaining
 * this state outside the model simplifies the concurrency analysis.
 *
 * These are externs are defined here in the system module since
 * we currently perform reservation cancellation on privilege level
 * transition.  Ideally, the platform should get more visibility into
 * where cancellation can be performed.
 */

val load_reservation = {ocaml: "Platform.load_reservation", c: "load_reservation", lem: "load_reservation"} : xlenbits -> unit

val match_reservation = {ocaml: "Platform.match_reservation", lem: "speculate_conditional_success", c: "match_reservation"} : xlenbits -> bool effect {exmem}

val cancel_reservation = {ocaml: "Platform.cancel_reservation", c: "cancel_reservation", lem: "cancel_reservation"} : unit -> unit

/* Exception delegation: given an exception and the privilege at which
 * it occured, returns the privilege at which it should be handled.
 */
function exception_delegatee(e : ExceptionType, p : Privilege) -> Privilege = {
  let idx   = num_of_ExceptionType(e);
  let super = medeleg.bits()[idx];
  let user  = sedeleg.bits()[idx];
  let deleg = /* if      misa.N() == true & user  then User
                 else */
              if misa.S() == true & super then Supervisor
              else Machine;
  /* Ensure there is no transition to a less-privileged mode. */
  if   privLevel_to_bits(deleg) <_u privLevel_to_bits(p)
  then p else deleg
}

/* Interrupts are prioritized in privilege order, and for each
 * privilege, in the order: external, software, timers.
 */
function findPendingInterrupt(ip : xlenbits) -> option(InterruptType) = {
  let ip = Mk_Minterrupts(ip);
  if      ip.MEI() == true then Some(I_M_External)
  else if ip.MSI() == true then Some(I_M_Software)
  else if ip.MTI() == true then Some(I_M_Timer)
  else if ip.SEI() == true then Some(I_S_External)
  else if ip.SSI() == true then Some(I_S_Software)
  else if ip.STI() == true then Some(I_S_Timer)
  else if ip.UEI() == true then Some(I_U_External)
  else if ip.USI() == true then Some(I_U_Software)
  else if ip.UTI() == true then Some(I_U_Timer)
  else None()
}

/* Examines current M-mode interrupt state and returns an interrupt to be
 * handled, and the privilege it should be handled at.  Interrupts are
 * dispatched in order of decreasing privilege, while ensuring that the
 * resulting privilege level is not reduced; i.e. delegated interrupts to
 * lower privileges are effectively masked until control returns to them.
 *
 * For now, it assumes 'S' and no 'N' extension, which is the common case.
 */
function curInterrupt(priv : Privilege, pend : Minterrupts, enbl : Minterrupts, delg : Minterrupts)
                     -> option((InterruptType, Privilege)) = {
  let en_mip : xlenbits = pend.bits() & enbl.bits();
  if en_mip == EXTZ(0b0) then None() /* fast path */
  else {
    /* check implicit enabling when in lower privileges */
    let eff_mie = priv != Machine | (priv == Machine & mstatus.MIE() == true);
    let eff_sie = priv == User | (priv == Supervisor & mstatus.SIE() == true);
    /* handle delegation */
    let eff_mip = en_mip & (~ (delg.bits())); /* retained at M-mode */
    let eff_sip = en_mip & delg.bits();       /* delegated to S-mode */

    if eff_mie & eff_mip != EXTZ(0b0)
    then match findPendingInterrupt(eff_mip) {
           Some(i) => let r = (i, Machine) in Some(r),
           None()  => { internal_error("non-zero eff_mip=" ^ BitStr(eff_mip) ^ ", but nothing pending") }
         }
    else if eff_sie & eff_sip != EXTZ(0b0)
    then match findPendingInterrupt(eff_sip) {
           Some(i) => let r = (i, Supervisor) in Some(r),
           None()  => { internal_error("non-zero eff_sip=" ^ BitStr(eff_sip) ^ ", but nothing pending") }
         }
    else {
      let p = if pend.MTI() == true then "1" else "0";
      let e = if enbl.MTI() == true then "1" else "0";
      let d = if delg.MTI() == true then "1" else "0";
      print(" MTI: pend=" ^ p ^ " enbl=" ^ e ^ " delg=" ^ d);
      let eff_mip = en_mip & (~ (delg.bits())); /* retained at M-mode */
      let eff_sip = en_mip & delg.bits();       /* delegated to S-mode */
      print("mstatus=" ^ BitStr(mstatus.bits())
            ^ " mie,sie=" ^ BitStr(mstatus.MIE()) ^ "," ^ BitStr(mstatus.SIE())
            ^ " en_mip=" ^ BitStr(en_mip)
            ^ " eff_mip=" ^ BitStr(eff_mip)
            ^ " eff_sip=" ^ BitStr(eff_sip));
      None()
    }
  }
}

/* privilege transitions due to exceptions and interrupts */

struct sync_exception = {
  trap    : ExceptionType,
  excinfo : option(xlenbits)
}

function tval(excinfo : option(xlenbits)) -> xlenbits = {
  match (excinfo) {
    Some(e) => e,
    None()  => EXTZ(0b0)
  }
}

union ctl_result = {
  CTL_TRAP : sync_exception,
  CTL_SRET : unit,
  CTL_MRET : unit
/* TODO: CTL_URET */
}

/* handle exceptional ctl flow by updating nextPC and operating privilege */

function handle_trap(del_priv : Privilege, intr : bool, c : exc_code, pc : xlenbits, info : option(xlenbits))
                    -> xlenbits = {
  print("handling " ^ (if intr then "int#" else "exc#") ^ BitStr(c) ^ " at priv " ^ del_priv ^ " with tval " ^ BitStr(tval(info)));

  match (del_priv) {
    Machine => {
       mcause->IsInterrupt() = intr;
       mcause->Cause()       = EXTZ(c);

       mstatus->MPIE() = mstatus.MIE();
       mstatus->MIE()  = false;
       mstatus->MPP()  = privLevel_to_bits(cur_privilege);
       mtval           = tval(info);
       mepc            = pc;

       cur_privilege   = del_priv;

       print("CSR mstatus <- " ^ BitStr(mstatus.bits()) ^ " (input: " ^ BitStr(mstatus.bits()) ^ ")"); // Spike compatible log

       cancel_reservation();

       match tvec_addr(mtvec, mcause) {
         Some(epc) => epc,
         None()    => internal_error("Invalid mtvec mode")
       }
    },
    Supervisor => {
       scause->IsInterrupt() = intr;
       scause->Cause()       = EXTZ(c);

       mstatus->SPIE() = mstatus.SIE();
       mstatus->SIE()  = false;
       mstatus->SPP()  = match (cur_privilege) {
                           User => false,
                           Supervisor => true,
                           Machine => internal_error("invalid privilege for s-mode trap")
                         };
       stval           = tval(info);
       sepc            = pc;

       cur_privilege   = del_priv;

       print("CSR mstatus <- " ^ BitStr(mstatus.bits()) ^ " (input: " ^ BitStr(mstatus.bits()) ^ ")"); // Spike compatible log

       cancel_reservation();

       match tvec_addr(stvec, scause) {
         Some(epc) => epc,
         None()    => internal_error("Invalid stvec mode")
       }

    },
    User => internal_error("the N extension is currently unsupported")
  };
}

function handle_exception(cur_priv : Privilege, ctl : ctl_result,
                          pc: xlenbits) -> xlenbits = {
  match (cur_priv, ctl) {
    (_, CTL_TRAP(e)) => {
      let del_priv = exception_delegatee(e.trap, cur_priv);
      print("trapping from " ^ cur_priv ^ " to " ^ del_priv
            ^ " to handle " ^ e.trap);
      handle_trap(del_priv, false, e.trap, pc, e.excinfo)
    },
    (_, CTL_MRET())  => {
      let prev_priv   = cur_privilege;
      mstatus->MIE()  = mstatus.MPIE();
      mstatus->MPIE() = true;
      cur_privilege   = privLevel_of_bits(mstatus.MPP());
      mstatus->MPP()  = privLevel_to_bits(User);

      print("CSR mstatus <- " ^ BitStr(mstatus.bits()) ^ " (input: " ^ BitStr(mstatus.bits()) ^ ")"); // Spike compatible log
      print("ret-ing from " ^ prev_priv ^ " to " ^ cur_privilege);

      cancel_reservation();
      mepc & pc_alignment_mask()
    },
    (_, CTL_SRET())  => {
      let prev_priv   = cur_privilege;
      mstatus->SIE()  = mstatus.SPIE();
      mstatus->SPIE() = true;
      cur_privilege   = if mstatus.SPP() == true then Supervisor else User;
      mstatus->SPP()  = false;

      print("CSR mstatus <- " ^ BitStr(mstatus.bits()) ^ " (input: " ^ BitStr(mstatus.bits()) ^ ")"); // Spike compatible log
      print("ret-ing from " ^ prev_priv ^ " to " ^ cur_privilege);

      cancel_reservation();
      sepc & pc_alignment_mask()
    }
  }
}

function handle_mem_exception(addr : xlenbits, e : ExceptionType) -> unit = {
  let t : sync_exception = struct { trap    = e,
                                    excinfo = Some(addr) } in
  nextPC = handle_exception(cur_privilege, CTL_TRAP(t), PC)
}

function handle_decode_exception(instbits : xlenbits) -> unit = {
  let t : sync_exception = struct { trap    = E_Illegal_Instr,
                                    excinfo = Some(instbits) };
  nextPC = handle_exception(cur_privilege, CTL_TRAP(t), PC)
}

function handle_interrupt(i : InterruptType, del_priv : Privilege) -> unit =
  nextPC = handle_trap(del_priv, true, i, PC, None())

function handle_illegal() -> unit = {
  let t : sync_exception = struct { trap    = E_Illegal_Instr,
                                    excinfo = None() };
  nextPC = handle_exception(cur_privilege, CTL_TRAP(t), PC)
}

/* state state initialization */

function init_sys() -> unit = {
  cur_privilege = Machine;

  mhartid     = EXTZ(0b0);

  misa->MXL() = arch_to_bits(RV64);
  misa->A()   = true; /* atomics */
  misa->C()   = true; /* RVC */
  misa->I()   = true; /* base integer ISA */
  misa->M()   = true; /* integer multiply/divide */
  misa->U()   = true; /* user-mode */
  misa->S()   = true; /* supervisor-mode */

  /* 64-bit only mode with no extensions */
  mstatus->SXL()  = misa.MXL();
  mstatus->UXL()  = misa.MXL();
  mstatus->SD()   = false;

  mip->bits()     = EXTZ(0b0);
  mie->bits()     = EXTZ(0b0);
  mideleg->bits() = EXTZ(0b0);
  medeleg->bits() = EXTZ(0b0);
  mtvec->bits()   = EXTZ(0b0);
  mcause->bits()  = EXTZ(0b0);
  mepc            = EXTZ(0b0);
  mtval           = EXTZ(0b0);
  mscratch        = EXTZ(0b0);

  mcycle          = EXTZ(0b0);
  mtime           = EXTZ(0b0);

  mcounteren->bits() = EXTZ(0b0);

  minstret           = EXTZ(0b0);
  minstret_written   = false;

  // log compatibility with spike
  print("CSR mstatus <- " ^ BitStr(mstatus.bits()) ^ " (input: " ^ BitStr(EXTZ(0b0) : xlenbits) ^ ")")
}

/* memory access exceptions, defined here for use by the platform model. */

union MemoryOpResult ('a : Type) = {
  MemValue     : 'a,
  MemException : ExceptionType
}