Run

This module provides the operational run semantics of MRiscX.

def MState.jif (ms : MState) (reg : UInt64) (lbl : String) (cond : UInt64 → Bool) : MState

Conditional jump on one register: jump to lbl if cond holds of register reg, otherwise advance the program counter.

Equations

• ms.jif reg lbl cond = if cond (ms.getRegisterAt reg) = true then ms.jump lbl else ms.incPc

def MState.jif' (ms : MState) (reg1 reg2 : UInt64) (lbl : String) (cond : UInt64 → UInt64 → Bool) : MState

Conditional jump on two registers: jump to lbl if cond holds of registers reg1 and reg2, otherwise advance the program counter.

Equations

• ms.jif' reg1 reg2 lbl cond = if cond (ms.getRegisterAt reg1) (ms.getRegisterAt reg2) = true then ms.jump lbl else ms.incPc

def MState.runOneStep (ms : MState) : MState

This function evaluates the given machine state to a new one. Tt represents the nxt function from the paper LUNDBERG, Didrik, et al. Hoare-style logic for unstructured programs. In: International Conference on Software Engineering and Formal Methods. Cham: Springer International Publishing, 2020. S. 193-213.

Generally, if the terminated of the State is false and the instruction is legal and evaluateable, a new State is returned holding the next instructions and the updated storage. When the instruction is not legal (e.g. jmp s, there is no label s), terminated is set to true.

Equations

• One or more equations did not get rendered due to their size.

def MState.runNSteps (ms : MState) (n : Nat) : MState

Runs runOneStep n times. It represents the function nxt^n from LUNDBERG, Didrik, et al. Hoare-style logic for unstructured programs. In: International Conference on Software Engineering and Formal Methods. Cham: Springer International Publishing, 2020. S. 193-213.

Equations

• ms.runNSteps Nat.zero = ms
• ms.runNSteps n'.succ = ms.runOneStep.runNSteps n'

def MState.runUntilTerminatedWithFuel (ms : MState) (fuel : Nat) : MState

Run the machine until it terminates or fuel steps have elapsed.

Equations

• ms.runUntilTerminatedWithFuel Nat.zero = ms
• ms.runUntilTerminatedWithFuel n'.succ = if ms.terminated = true then ms else ms.runOneStep.runUntilTerminatedWithFuel n'

def MState.runUntilTerminated (ms : MState) : MState

Run the machine until it terminates, bounded by UInt64.size steps.

Equations

• ms.runUntilTerminated = ms.runUntilTerminatedWithFuel UInt64.size

def MState.nextInstruction (ms : MState) : Instr

The instruction the machine would execute after one more step.

Equations

• ms.nextInstruction = ms.runOneStep.currInstruction