Exact compiler crate identity/name, caller attributes and source scopes. The configured user-relevant crate set is supplied explicitly by the machine.

structure Miri.Input.CompilerFrameMetadata.Prepared : Type

• calls : CompilerCallPipeline.Prepared
• localCrate : Nat
• crates : Array (Nat × String)

def Miri.Input.CompilerFrameMetadata.prepare (calls : CompilerCallPipeline.Prepared) : Except String Prepared

Equations

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

def Miri.Input.CompilerFrameMetadata.hooks {K User : Type} (p : Prepared) (userRelevantCrates : Array Nat) : Interpreter.FrameMetadata.CompilerHooks K User

Equations

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

def Miri.Input.CompilerFrameMetadata.resolvedRank (localCrate definitionCrate : Nat) (relevant : Array Nat) : UInt8

Equations

• Miri.Input.CompilerFrameMetadata.resolvedRank localCrate definitionCrate relevant = if (definitionCrate == localCrate || relevant.contains definitionCrate) = true then 255 else 1

theorem Miri.Input.CompilerFrameMetadata.userRelevance_resolved {K U P : Type} (p : Prepared) (relevant : Array Nat) (frame : Interpreter.Frame P Interpreter.LocalLayout Unit) (definition : DefinitionId) (inline : CompilerVirtualFacts.inlineAttribute p.calls.scopes frame.functionInstance = Except.ok none ∨ CompilerVirtualFacts.inlineAttribute p.calls.scopes frame.functionInstance = Except.ok (some false)) (track : CompilerRuntimeQueries.requiresCallerLocation p.calls.runtime frame.functionInstance = Except.ok false) (found : p.calls.calls.program.compilerTables.definitions[Interpreter.CallInstance.defId frame.functionInstance]? = some definition) : Interpreter.FrameMetadata.userRelevance (hooks p relevant) frame = pure (resolvedRank p.localCrate definition.crateIndex relevant)

theorem Miri.Input.CompilerFrameMetadata.initFrame_resolved {K U : Type} (p : Prepared) (relevant : Array Nat) (frame : Interpreter.Frame Memory.Provenance Interpreter.LocalLayout Unit) (definition : DefinitionId) (inline : CompilerVirtualFacts.inlineAttribute p.calls.scopes frame.functionInstance = Except.ok none ∨ CompilerVirtualFacts.inlineAttribute p.calls.scopes frame.functionInstance = Except.ok (some false)) (track : CompilerRuntimeQueries.requiresCallerLocation p.calls.runtime frame.functionInstance = Except.ok false) (found : p.calls.calls.program.compilerTables.definitions[Interpreter.CallInstance.defId frame.functionInstance]? = some definition) (state : Interpreter.MachineHooks.State K U) : ∃ (fresh : Interpreter.Frame Memory.Provenance Interpreter.LocalLayout Interpreter.MachineHooks.FrameExtra), Interpreter.MachineHooks.initFrame (Interpreter.FrameMetadata.userRelevance (hooks p relevant)) frame state = EStateM.Result.ok fresh state ∧ fresh.extra.borrowTracker = Option.map (fun (x : Interpreter.MachineHooks.BorrowState) => { }) state.machine.borrowTracker ∧ fresh.extra.dataRace = Option.map (fun (x : Concurrency.GlobalState) => { }) state.machine.dataRace ∧ fresh.extra.userRelevance = resolvedRank p.localCrate definition.crateIndex relevant ∧ fresh.returnContinuation = frame.returnContinuation ∧ fresh.returnPlace = frame.returnPlace

def Miri.Input.CompilerFrameMetadata.resolvedFrame {K U : Type} (frame : Interpreter.Frame Memory.Provenance Interpreter.LocalLayout Unit) (machine : Interpreter.MachineHooks.MachineState K U) (rank : UInt8) : Interpreter.Frame Memory.Provenance Interpreter.LocalLayout Interpreter.MachineHooks.FrameExtra

Equations

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

theorem Miri.Input.CompilerFrameMetadata.initFrame_explicit {K U : Type} (p : Prepared) (relevant : Array Nat) (frame : Interpreter.Frame Memory.Provenance Interpreter.LocalLayout Unit) (definition : DefinitionId) (inline : CompilerVirtualFacts.inlineAttribute p.calls.scopes frame.functionInstance = Except.ok none ∨ CompilerVirtualFacts.inlineAttribute p.calls.scopes frame.functionInstance = Except.ok (some false)) (track : CompilerRuntimeQueries.requiresCallerLocation p.calls.runtime frame.functionInstance = Except.ok false) (found : p.calls.calls.program.compilerTables.definitions[Interpreter.CallInstance.defId frame.functionInstance]? = some definition) (state : Interpreter.MachineHooks.State K U) : Interpreter.MachineHooks.initFrame (Interpreter.FrameMetadata.userRelevance (hooks p relevant)) frame state = EStateM.Result.ok (resolvedFrame frame state.machine (resolvedRank p.localCrate definition.crateIndex relevant)) state