Skip to content

Refactor try_step() some more #883

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Apr 27, 2025
Merged

Refactor try_step() some more #883

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions model/riscv_platform.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -446,9 +446,9 @@ function tick_platform() -> unit = {

/* Platform-specific handling of instruction faults */

function handle_illegal(instbits: xlenbits) -> unit = {
let info = if plat_mtval_has_illegal_inst_bits ()
then Some(instbits)
function handle_illegal(instbits : instbits) -> unit = {
let info = if plat_mtval_has_illegal_inst_bits()
then Some(zero_extend(xlen, instbits))
else None();
let t : sync_exception = struct { trap = E_Illegal_Instr(),
excinfo = info,
Expand Down
165 changes: 68 additions & 97 deletions model/riscv_step.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,28 +10,6 @@

register hart_state : HartState = HART_ACTIVE()

// Returns whether the retire result returned by the execution of an
// instruction counts as a step, where a step is said to occur when an
// instruction retires successfully or it raises an exception.
// Crucially, if an instruction returns a Wait retire result, it does
// not step.
function retires_or_traps(r : ExecutionResult(Retire_Failure)) -> bool =
match r {
RETIRE_OK() => true,
RETIRE_FAIL(Illegal_Instruction()) => true,
RETIRE_FAIL(Memory_Exception(_)) => true,
RETIRE_FAIL(Trap(_)) => true,

// do not step if a wait instruction executed.
RETIRE_FAIL(Wait_For_Interrupt()) => false,

// errors from extensions
RETIRE_FAIL(Ext_ControlAddr_Check_Failure(_)) => true,
RETIRE_FAIL(Ext_DataAddr_Check_Failure(_)) => true,
RETIRE_FAIL(Ext_CSR_Check_Failure()) => true,
RETIRE_FAIL(Ext_XRET_Priv_Failure(_)) => true,
}

union Step = {
Step_Pending_Interrupt : (InterruptType, Privilege),
Step_Ext_Fetch_Failure : ext_fetch_addr_error,
Expand All @@ -40,15 +18,15 @@ union Step = {
Step_Waiting : unit,
}

function run_hart_waiting(step_no : int, exit_wait : bool, instbits : instbits) -> (Step, bool) = {
function run_hart_waiting(step_no : nat, exit_wait : bool, instbits : instbits) -> Step = {
if shouldWakeForInterrupt() then {
if get_config_print_instr()
then print_instr("interrupt exit from WAIT state at PC " ^ BitStr(PC));

hart_state = HART_ACTIVE();
// The waiting instruction retires successfully. The
// pending interrupts will be handled in the next step.
(Step_Execute(RETIRE_OK(), instbits), true)
Step_Execute(RETIRE_OK(), instbits)
} else if exit_wait then {
// There are no pending interrupts; transition out of the Wait
// as instructed.
Expand All @@ -61,27 +39,27 @@ function run_hart_waiting(step_no : int, exit_wait : bool, instbits : instbits)
// implementation-specific, bounded time limit, the WFI
// instruction causes an illegal-instruction exception."
if (cur_privilege == Machine | mstatus[TW] == 0b0)
then (Step_Execute(RETIRE_OK(), instbits), true)
else (Step_Execute(RETIRE_FAIL(Illegal_Instruction()), instbits), true)
then Step_Execute(RETIRE_OK(), instbits)
else Step_Execute(RETIRE_FAIL(Illegal_Instruction()), instbits)
} else {
if get_config_print_instr()
then print_instr("remaining in WAIT state at PC " ^ BitStr(PC));
(Step_Waiting(), false)
Step_Waiting()
}
}

function run_hart_active(step_no: int, exit_wait : bool) -> (Step, bool) = {
function run_hart_active(step_no: nat) -> Step = {
match dispatchInterrupt(cur_privilege) {
Some(intr, priv) => (Step_Pending_Interrupt(intr, priv), false),
Some(intr, priv) => Step_Pending_Interrupt(intr, priv),
None() => match ext_fetch_hook(fetch()) {
/* extension error */
F_Ext_Error(e) => (Step_Ext_Fetch_Failure(e), false),
F_Ext_Error(e) => Step_Ext_Fetch_Failure(e),
/* standard error */
F_Error(e, addr) => (Step_Fetch_Failure(Virtaddr(addr), e), false),
F_Error(e, addr) => Step_Fetch_Failure(Virtaddr(addr), e),
/* non-error cases: */
F_RVC(h) => {
sail_instr_announce(h);
let instbits : xlenbits = zero_extend(h);
let instbits : instbits = zero_extend(h);
let ast = ext_decode_compressed(h);
if get_config_print_instr()
then {
Expand All @@ -91,9 +69,9 @@ function run_hart_active(step_no: int, exit_wait : bool) -> (Step, bool) = {
if currentlyEnabled(Ext_Zca) then {
nextPC = PC + 2;
let r = execute(ast);
(Step_Execute(r, instbits), retires_or_traps(r))
Step_Execute(r, instbits)
} else {
(Step_Execute(RETIRE_FAIL(Illegal_Instruction()), instbits), true)
Step_Execute(RETIRE_FAIL(Illegal_Instruction()), instbits)
}
},
F_Base(w) => {
Expand All @@ -106,7 +84,7 @@ function run_hart_active(step_no: int, exit_wait : bool) -> (Step, bool) = {
};
nextPC = PC + 4;
let r = execute(ast);
(Step_Execute(r, instbits), retires_or_traps(r))
Step_Execute(r, instbits)
}
}
}
Expand All @@ -117,12 +95,28 @@ function wfi_is_nop() -> bool = config platform.wfi_is_nop
// The `try_step` function is the main internal driver of the Sail
// model. It performs the fetch-decode-execute for an instruction. It
// is also the primary interface to the non-Sail execution harness.
// The harness calls this function with the current step number (which
// numbers the active or wait step), and whether it should exit a wait
// state. The `try_step` function returns whether the Sail emulator
// executed a step, and the stepper state at the end of the step.

function try_step(step_no : int, exit_wait : bool) -> bool = {
//
// A "step" is a full execution of an instruction, resulting either
// in its retirement or a trap. WFI and WRS instructions can cause
// the model to wait (hart_state is HART_WAITING), in which case
// a step has not happened and `try_step()` returns false. Otherwise
// it returns true. Equivalently, it returns whether the model is now
// in an active state (HART_ACTIVE).
//
// * step_no: the current step number; this is maintained by by the
// non-Sail harness and is incremented when `try_step()`
// returns true.
// * exit_wait: if true, and the model is waiting (HART_WAITING)
// then it will wake up (switch to HART_ACTIVE) and
// complete the WFI/WRS instruction, either successfully
// retiring it or causing an illegal instruction
// exception depending on mstatus[TW]. `exit_wait`
// only affects the behaviour if the model is already
// waiting from a previous WFI/WRS. It doesn't affect
// WFI/WRS instructions executed in the same call of
// `try_step()` (but see `wfi_is_nop()`).
//
function try_step(step_no : nat, exit_wait : bool) -> bool = {
/* for step extensions */
ext_pre_step_hook();

Expand All @@ -136,95 +130,72 @@ function try_step(step_no : int, exit_wait : bool) -> bool = {
*/
minstret_increment = should_inc_minstret(cur_privilege);

let (step_val, did_step) : (Step, bool) = match hart_state {
let step_val : Step = match hart_state {
HART_WAITING(instbits) => run_hart_waiting(step_no, exit_wait, instbits),
HART_ACTIVE() => run_hart_active(step_no, exit_wait),
HART_ACTIVE() => run_hart_active(step_no),
};

var stepped : bool = did_step;

match step_val {
Step_Pending_Interrupt(intr, priv) => {
if get_config_print_instr()
then print_bits("Handling interrupt: ", interruptType_to_bits(intr));
minstret_increment = false;
handle_interrupt(intr, priv)
},
Step_Ext_Fetch_Failure(e) => {
minstret_increment = false;
ext_handle_fetch_check_error(e)
},
Step_Fetch_Failure(vaddr, e) => {
minstret_increment = false;
handle_mem_exception(vaddr, e)
},
Step_Waiting() => {
assert(hart_is_waiting(hart_state), "cannot be Waiting in a non-Wait state")
},
Step_Execute(RETIRE_OK(), _) => {
assert(hart_is_active(hart_state))
},
Step_Ext_Fetch_Failure(e) => ext_handle_fetch_check_error(e),
Step_Fetch_Failure(vaddr, e) => handle_mem_exception(vaddr, e),
Step_Waiting() => assert(hart_is_waiting(hart_state), "cannot be Waiting in a non-Wait state"),
Step_Execute(RETIRE_OK(), _) => assert(hart_is_active(hart_state)),
// standard errors
Step_Execute(RETIRE_FAIL(Trap(priv, ctl, pc)), _) => {
minstret_increment = false;
set_next_pc(exception_handler(priv, ctl, pc))
},
Step_Execute(RETIRE_FAIL(Memory_Exception(vaddr, e)), _) => {
minstret_increment = false;
handle_mem_exception(vaddr, e)
},
Step_Execute(RETIRE_FAIL(Illegal_Instruction()), instbits) => {
minstret_increment = false;
handle_illegal(instbits)
},
Step_Execute(RETIRE_FAIL(Trap(priv, ctl, pc)), _) => set_next_pc(exception_handler(priv, ctl, pc)),
Step_Execute(RETIRE_FAIL(Memory_Exception(vaddr, e)), _) => handle_mem_exception(vaddr, e),
Step_Execute(RETIRE_FAIL(Illegal_Instruction()), instbits) => handle_illegal(instbits),
Step_Execute(RETIRE_FAIL(Wait_For_Interrupt()), instbits) =>
if wfi_is_nop() then {
// This is the same as the RETIRE_OK case.
assert(hart_is_active(hart_state));
// Override the default step for WFI.
stepped = true;
} else {
// Transition into the wait state.
if get_config_print_instr()
then print_instr("entering WAIT state at PC " ^ BitStr(PC));
hart_state = HART_WAITING(instbits);
},
// errors from extensions
Step_Execute(RETIRE_FAIL(Ext_CSR_Check_Failure()), _) => {
minstret_increment = false;
ext_check_CSR_fail()
},
Step_Execute(RETIRE_FAIL(Ext_ControlAddr_Check_Failure(e)), _) => {
minstret_increment = false;
ext_handle_control_check_error(e)
},
Step_Execute(RETIRE_FAIL(Ext_DataAddr_Check_Failure(e)), _) => {
minstret_increment = false;
ext_handle_data_check_error(e)
},
Step_Execute(RETIRE_FAIL(Ext_XRET_Priv_Failure()), _) => {
minstret_increment = false;
ext_fail_xret_priv ()
},
Step_Execute(RETIRE_FAIL(Ext_CSR_Check_Failure()), _) => ext_check_CSR_fail(),
Step_Execute(RETIRE_FAIL(Ext_ControlAddr_Check_Failure(e)), _) => ext_handle_control_check_error(e),
Step_Execute(RETIRE_FAIL(Ext_DataAddr_Check_Failure(e)), _) => ext_handle_data_check_error(e),
Step_Execute(RETIRE_FAIL(Ext_XRET_Priv_Failure()), _) => ext_fail_xret_priv(),
};

match hart_state {
HART_WAITING(_) => (),
HART_WAITING(_) => false,
HART_ACTIVE() => {
tick_pc();
update_minstret();

let retired : bool = match step_val {
Step_Execute(RETIRE_OK(), _) => true,
// WFI retires immediately if the model is configured to treat it as a nop.
// Otherwise it always waits for at least one call of `try_step()`.
Step_Execute(RETIRE_FAIL(Wait_For_Interrupt()), _) if wfi_is_nop() => true,
_ => false,
};

// Increment minstret if we retired an instruction and the
// update wasn't suppressed by writing to it explicitly or
// mcountinhibit[IR] or minstretcfg.
if retired & minstret_increment then minstret = minstret + 1;

/* for step extensions */
ext_post_step_hook();
// Return that we have stepped and are active.
true
}
};

stepped
}
}

function loop () : unit -> unit = {
let insns_per_tick = plat_insns_per_tick();
var i : int = 0;
var step_no : int = 0;
var i : nat = 0;
var step_no : nat = 0;
while not(htif_done) do {
// This standalone loop always exits immediately out of waiting
// states.
Expand Down
31 changes: 16 additions & 15 deletions model/riscv_step_common.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,23 +18,13 @@
// instruction should finish execution. Note that in the latter
// case, the platform can decide to end the stall for any reason,
// even if there are no interrupts or invalidated reservation set.

type instbits = xlenbits

union HartState = {
HART_ACTIVE : unit,
HART_WAITING : instbits, // the instruction that caused the wait
}

/* The result of a fetch, which includes any possible error
* from an extension that interposes on the fetch operation.
*/

union FetchResult = {
F_Ext_Error : ext_fetch_addr_error, /* For extensions */
F_Base : word, /* Base ISA */
F_RVC : half, /* Compressed ISA */
F_Error : (ExceptionType, xlenbits) /* standard exception and PC */
// The instruction that caused the wait. This is needed
// because WFI and WRS can time out and cause an illegal
// instruction exception so we need to know what to write
// to mtval.
HART_WAITING : instbits,
}

// utility predicates
Expand All @@ -50,3 +40,14 @@ function hart_is_waiting(s : HartState) -> bool =
HART_ACTIVE() => false,
HART_WAITING(_) => true,
}

/* The result of a fetch, which includes any possible error
* from an extension that interposes on the fetch operation.
*/

union FetchResult = {
F_Ext_Error : ext_fetch_addr_error, /* For extensions */
F_Base : word, /* Base ISA */
F_RVC : half, /* Compressed ISA */
F_Error : (ExceptionType, xlenbits) /* standard exception and PC */
}
4 changes: 0 additions & 4 deletions model/riscv_sys_regs.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -638,10 +638,6 @@ register minstret : bits(64)
/* Should minstret be incremented when the instruction is retired. */
register minstret_increment : bool

function update_minstret() -> unit = {
if minstret_increment then minstret = minstret + 1;
}

/* machine information registers */
register mvendorid : bits(32) = zeros()
register mimpid : xlenbits = zeros()
Expand Down
3 changes: 3 additions & 0 deletions model/riscv_types.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,9 @@ let xlen_min_signed = 0 - 2 ^ (xlen - 1)
type half = bits(16)
type word = bits(32)

// Bit-vector of an uncompressed instruction.
type instbits = bits(32)

type pagesize_bits : Int = 12
let pagesize_bits = sizeof(pagesize_bits)

Expand Down
Loading