Skip to content

Commit

Permalink
Refactor interrupt code & small style changes
Browse files Browse the repository at this point in the history
  • Loading branch information
@Timmmm
Timmmm committed Oct 9, 2024
1 parent d79e0ba commit c1cfd62
Show file tree
Hide file tree
Showing 3 changed files with 27 additions and 54 deletions.
67 changes: 21 additions & 46 deletions model/riscv_sys_control.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,8 +27,8 @@ function is_CSR_defined (csr : csreg) -> bool =
/* machine mode: trap setup */
0x300 => true, // mstatus
0x301 => true, // misa
0x302 => extensionEnabled(Ext_S) , // medeleg
0x303 => extensionEnabled(Ext_S) , // mideleg
0x302 => extensionEnabled(Ext_S), // medeleg
0x303 => extensionEnabled(Ext_S), // mideleg
0x304 => true, // mie
0x305 => true, // mtvec
0x306 => extensionEnabled(Ext_U), // mcounteren
Expand Down Expand Up @@ -175,8 +175,7 @@ val cancel_reservation = impure {ocaml: "Platform.cancel_reservation", interpret
function exception_delegatee(e : ExceptionType, p : Privilege) -> Privilege = {
let idx = num_of_ExceptionType(e);
let super = bit_to_bool(medeleg.bits[idx]);
let deleg = if extensionEnabled(Ext_S) & super then Supervisor
else Machine;
let deleg = if extensionEnabled(Ext_S) & super then Supervisor else Machine;
/* We cannot transition to a less-privileged mode. */
if privLevel_to_bits(deleg) <_u privLevel_to_bits(p)
then p else deleg
Expand All @@ -193,7 +192,7 @@ function findPendingInterrupt(ip : xlenbits) -> option(InterruptType) = {
else if ip[SEI] == 0b1 then Some(I_S_External)
else if ip[SSI] == 0b1 then Some(I_S_Software)
else if ip[STI] == 0b1 then Some(I_S_Timer)
else None()
else None()
}

/* Process the pending interrupts xip at a privilege according to
Expand All @@ -209,28 +208,26 @@ union interrupt_set = {
function processPending(xip : Minterrupts, xie : Minterrupts, xideleg : xlenbits,
priv_enabled : bool) -> interrupt_set = {
/* interrupts that are enabled but not delegated are pending */
let effective_pend = xip.bits & xie.bits & (~ (xideleg));
let effective_pend = xip.bits & xie.bits & ~(xideleg);
/* the others are delegated */
let effective_delg = xip.bits & xideleg;
/* we have pending interrupts if this privilege is enabled */
if priv_enabled & (effective_pend != zero_extend(0b0))
if priv_enabled & (effective_pend != zeros())
then Ints_Pending(effective_pend)
else if effective_delg != zero_extend(0b0)
else if effective_delg != zeros()
then Ints_Delegated(effective_delg)
else Ints_Empty()
}

/* Given the current privilege level, iterate over privileges to get a
* pending set for an enabled privilege. This is only called for M/U or
* M/S/U systems.
* pending set for an enabled privilege.
*
* We don't use the lowered views of {xie,xip} here, since the spec
* allows for example the M_Timer to be delegated to the U-mode.
* allows for example the M_Timer to be delegated to the S-mode.
*/
function getPendingSet(priv : Privilege) -> option((xlenbits, Privilege)) = {
assert(extensionEnabled(Ext_U), "no user mode: M/U or M/S/U system required");
let effective_pending = mip.bits & mie.bits;
if effective_pending == zero_extend(0b0) then None() /* fast path */
if effective_pending == zeros() then None() /* fast path */
else {
/* Higher privileges than the current one are implicitly enabled,
* while lower privileges are blocked. An unsupported privilege is
Expand All @@ -240,10 +237,8 @@ function getPendingSet(priv : Privilege) -> option((xlenbits, Privilege)) = {
let sIE = extensionEnabled(Ext_S) & (priv == User | (priv == Supervisor & mstatus[SIE] == 0b1));
match processPending(mip, mie, mideleg.bits, mIE) {
Ints_Empty() => None(),
Ints_Pending(p) => let r = (p, Machine) in Some(r),
Ints_Delegated(d) =>
if not(extensionEnabled(Ext_S)) | not(sIE) then None()
else let r = (d, Supervisor) in Some(r)
Ints_Pending(p) => Some((p, Machine)),
Ints_Delegated(d) => if sIE then Some((d, Supervisor)) else None(),
}
}
}
Expand All @@ -252,32 +247,12 @@ function getPendingSet(priv : Privilege) -> option((xlenbits, Privilege)) = {
* handled (if any), and the privilege it should be handled at.
*/
function dispatchInterrupt(priv : Privilege) -> option((InterruptType, Privilege)) = {
/* If we don't have different privilege levels, we don't need to check delegation.
* Absence of U-mode implies absence of S-mode.
*/
let multipleModesSupported = extensionEnabled(Ext_U);
if not(multipleModesSupported) then {
assert(priv == Machine, "invalid current privilege")
};
/* Even with U-mode, we don't need to check delegation when M-mode is the only
one that can take interrupts, i.e. when we don't have S-mode and don't have
the N extension
*/
let delegationPossible = extensionEnabled(Ext_S);
if multipleModesSupported & delegationPossible then {
match getPendingSet(priv) {
None() => None(),
Some(ip, p) => match findPendingInterrupt(ip) {
None() => None(),
Some(i) => let r = (i, p) in Some(r)
}
}
} else {
let enabled_pending = mip.bits & mie.bits;
match findPendingInterrupt(enabled_pending) {
Some(i) => let r = (i, Machine) in Some(r),
None() => None()
}
match getPendingSet(priv) {
None() => None(),
Some(ip, p) => match findPendingInterrupt(ip) {
None() => None(),
Some(i) => Some((i, p)),
}
}
}

Expand All @@ -286,7 +261,7 @@ function dispatchInterrupt(priv : Privilege) -> option((InterruptType, Privilege
union ctl_result = {
CTL_TRAP : sync_exception,
CTL_SRET : unit,
CTL_MRET : unit
CTL_MRET : unit,
}

/* trap value */
Expand Down Expand Up @@ -363,7 +338,7 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen

prepare_trap_vector(del_priv, scause)
},
User => internal_error(__FILE__, __LINE__, "Invalid privilege level")
User => internal_error(__FILE__, __LINE__, "Invalid privilege level"),
};
}

Expand Down Expand Up @@ -409,7 +384,7 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result,
^ " to " ^ to_str(cur_privilege));

prepare_xret_target(Supervisor) & pc_alignment_mask()
}
},
}
}

Expand Down
6 changes: 3 additions & 3 deletions model/riscv_sys_exceptions.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@ function prepare_trap_vector(p : Privilege, cause : Mcause) -> xlenbits = {
let tvec : Mtvec = match p {
Machine => mtvec,
Supervisor => stvec,
User => internal_error(__FILE__, __LINE__, "Invalid privilege level")
User => internal_error(__FILE__, __LINE__, "Invalid privilege level"),
};
match tvec_addr(tvec, cause) {
Some(epc) => epc,
Expand All @@ -42,7 +42,7 @@ function get_xret_target(p) =
match p {
Machine => mepc,
Supervisor => sepc,
User => internal_error(__FILE__, __LINE__, "Invalid privilege level")
User => internal_error(__FILE__, __LINE__, "Invalid privilege level"),
}

val set_xret_target : (Privilege, xlenbits) -> xlenbits
Expand All @@ -51,7 +51,7 @@ function set_xret_target(p, value) = {
match p {
Machine => mepc = target,
Supervisor => sepc = target,
User => internal_error(__FILE__, __LINE__, "Invalid privilege level")
User => internal_error(__FILE__, __LINE__, "Invalid privilege level"),
};
target
}
Expand Down
8 changes: 3 additions & 5 deletions model/riscv_sys_regs.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -310,21 +310,19 @@ 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 = [o with SEI = v[SEI], STI = v[STI], SSI = v[SSI]];
m
[o with SEI = v[SEI], STI = v[STI], SSI = v[SSI]]
}

function legalize_mie(o : Minterrupts, v : xlenbits) -> Minterrupts = {
let v = Mk_Minterrupts(v);
let m = [o with
[o with
MEI = v[MEI],
MTI = v[MTI],
MSI = v[MSI],
SEI = v[SEI],
STI = v[STI],
SSI = v[SSI]
];
m
]
}

function legalize_mideleg(o : Minterrupts, v : xlenbits) -> Minterrupts = {
Expand Down

0 comments on commit c1cfd62

Please sign in to comment.