Attach the source-built physical Miri shim machine and source effects to an already assembled foreign resolver. Miri runs first in the portable family; unrecognized names continue through the pre-existing backtrace and C memory/string handlers.

@[reducible, inline]

abbrev Miri.Input.EvalMiriSourceRuntime.User (Os R P H D O Aff B Host : Type) : Type

Equations

• Miri.Input.EvalMiriSourceRuntime.User Os R P H D O Aff B Host = Miri.Input.EvalCoreMachine.User Os R P H D O Aff B Host

@[reducible, inline]

abbrev Miri.Input.EvalMiriSourceRuntime.State (Os R P H D O Aff B Host : Type) : Type

Equations

• Miri.Input.EvalMiriSourceRuntime.State Os R P H D O Aff B Host = Miri.Input.EvalCoreMachine.State Os R P H D O Aff B Host

@[reducible, inline]

abbrev Miri.Input.EvalMiriSourceRuntime.Stored (Os R P H D O Aff B Host : Type) : Type

Equations

• Miri.Input.EvalMiriSourceRuntime.Stored Os R P H D O Aff B Host = Miri.Input.EvalCoreMachine.Stored Os R P H D O Aff B Host

@[reducible, inline]

abbrev Miri.Input.EvalMiriSourceRuntime.World (Os R P H D O Aff B Host : Type) : Type

Equations

• Miri.Input.EvalMiriSourceRuntime.World Os R P H D O Aff B Host = Miri.Input.EvalWorld.World Os R P H D O Aff B Host

@[reducible, inline]

abbrev Miri.Input.EvalMiriSourceRuntime.Control (Os R P H D O Aff B Host : Type) : Type

Equations

• Miri.Input.EvalMiriSourceRuntime.Control Os R P H D O Aff B Host = Miri.Interpreter.ValidityMachine.Control (Miri.Input.EvalMiriSourceRuntime.Stored Os R P H D O Aff B Host)

@[reducible, inline]

abbrev Miri.Input.EvalMiriSourceRuntime.EntryUser (Os R P H D O Aff B Host : Type) : Type

Equations

• Miri.Input.EvalMiriSourceRuntime.EntryUser Os R P H D O Aff B Host = Miri.Interpreter.ValidityMachine.UserState (Miri.Input.EvalMiriSourceRuntime.World Os R P H D O Aff B Host)

@[reducible, inline]

abbrev Miri.Input.EvalMiriSourceRuntime.M (Os R P H D O Aff B Host A : Type) : Type

Equations

• Miri.Input.EvalMiriSourceRuntime.M Os R P H D O Aff B Host A = Miri.Interpreter.MachineHooks.M Miri.Memory.MiriMemoryKind (Miri.Input.EvalMiriSourceRuntime.User Os R P H D O Aff B Host) A

def Miri.Input.EvalMiriSourceRuntime.bindPhysical {C : Type} [DecidableEq Memory.MiriMemoryKind] {Os R P H D O Aff B Host Other HostPath : Type} (machine : Interpreter.MiriShimMachine.Hooks Memory.MiriMemoryKind (Control Os R P H D O Aff B Host) C Interpreter.MachineHooks.FrameExtra Other) (choice : C) (thread : Interpreter.ThreadMachine.Hooks Memory.MiriMemoryKind (EntryUser Os R P H D O Aff B Host) C O ABI.ExternAbi (ABI.FnAbi MIR.TyId) (ABI.ArgAbi MIR.TyId) Aff) (unitLayout : M Os R P H D O Aff B Host Interpreter.LocalLayout) (reuseClock : Option Concurrency.VectorIdx) (effects : EvalPortableForeignConstruction.MiriEffects Os R P H D O Aff B Host HostPath) (foreign : Interpreter.ForeignItems.Hooks Memory.Provenance (State Os R P H D O Aff B Host) (Interpreter.RuntimePlace Memory.Provenance) (Interpreter.RuntimePlace Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) Interpreter.LoadedBody Interpreter.CallInstance) : Interpreter.ForeignItems.Hooks Memory.Provenance (State Os R P H D O Aff B Host) (Interpreter.RuntimePlace Memory.Provenance) (Interpreter.RuntimePlace Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) Interpreter.LoadedBody Interpreter.CallInstance

Bind physical source Miri operations without replacing any other portable family. Allocation/provenance/GC/bookkeeping come from machine; thread creation and joining use the canonical source ThreadMachine; only true host, diagnostic, and selected-backend effects are supplied in effects.

Equations

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