def Miri.Interpreter.FrameRelevance.computeTop {P : Type} (stack : Stack P LocalLayout MachineHooks.FrameExtra) (skip : Nat) : Option Nat

Reverse source search: topmost wins ties; 255 short-circuits.

Equations

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

def Miri.Interpreter.FrameRelevance.top {P : Type} (stack : Stack P LocalLayout MachineHooks.FrameExtra) (cached : Option Nat) : Option Nat

Equations

• Miri.Interpreter.FrameRelevance.top stack cached = cached.orElse fun (x : Unit) => if stack.frames.isEmpty = true then none else some (stack.frames.size - 1)

def Miri.Interpreter.FrameRelevance.afterStackPush {K User : Type} (debugAssertions : Bool) : MachineHooks.M K User Unit

Equations

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

def Miri.Interpreter.FrameRelevance.beforeStackPop {K User : Type} : MachineHooks.M K User Unit

Invoke after successful TB on_stack_pop, before removing the frame.

Equations

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

def Miri.Interpreter.FrameRelevance.currentUserRelevantSpan {K User : Type} (debugAssertions : Bool) (dummy : MIR.SpanRef) : MachineHooks.M K User MIR.SpanRef

Equations

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

def Miri.Interpreter.FrameRelevance.callerSpan {K User : Type} : MachineHooks.M K User MIR.SpanRef

Equations

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

def Miri.Interpreter.FrameRelevance.bindLifecycle {K User : Type} (debugAssertions : Bool) (base : StackLifecycleHooks Memory.Provenance LocalLayout MachineHooks.FrameExtra (MachineHooks.MachineState K User)) : StackLifecycleHooks Memory.Provenance LocalLayout MachineHooks.FrameExtra (MachineHooks.MachineState K User)

Install source after_stack_push and the cache suffix of before_stack_pop. The supplied beforePop is the borrow-tracker prefix; its failure retains its state and never executes the cache update. Other lifecycle operations are retained.

Equations

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

@[reducible, inline]

abbrev Miri.Interpreter.FrameRelevance.FreshFrame : Type

Equations

• Miri.Interpreter.FrameRelevance.FreshFrame = Miri.Interpreter.Frame Miri.Memory.Provenance Miri.Interpreter.LocalLayout Miri.Interpreter.MachineHooks.FrameExtra

def Miri.Interpreter.FrameRelevance.pushedMachine {K U : Type} (frames : Array FreshFrame) (frame old : FreshFrame) (machine : MachineHooks.MachineState K U) : MachineHooks.MachineState K U

Equations

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

theorem Miri.Interpreter.FrameRelevance.afterPush_known {K U : Type} (frames : Array FreshFrame) (frame old : FreshFrame) (machine : MachineHooks.MachineState K U) (thread : Concurrency.ThreadRecord) (index : Nat) (current : machine.threads.activeThread? = some thread) (cached : top { frames := frames.push frame } thread.topUserRelevantFrame = some index) (selected : (frames.push frame)[index]? = some old) : afterStackPush false { stack := { frames := frames.push frame }, machine := machine } = EStateM.Result.ok () { stack := { frames := frames.push frame }, machine := pushedMachine frames frame old machine }