Canonical source-shaped function instance identity from pinned rustc_middle/src/ty/instance.rs. Saved frames retain every shim kind and payload; a definition ID alone is not function-instance identity.

inductive Miri.Interpreter.CallReifyReason : Type

• FnPtr : CallReifyReason
• Vtable : CallReifyReason

@[instance_reducible]

instance Miri.Interpreter.instReprCallReifyReason : Repr CallReifyReason

Equations

• Miri.Interpreter.instReprCallReifyReason = { reprPrec := Miri.Interpreter.instReprCallReifyReason.repr }

def Miri.Interpreter.instReprCallReifyReason.repr : CallReifyReason → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqCallReifyReason : DecidableEq CallReifyReason

Equations

• Miri.Interpreter.instDecidableEqCallReifyReason x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Miri.Interpreter.CallShimKind : Type

All variants and payloads of pinned ty::ShimKind.

• VTable (definition : MIR.DefId) : CallShimKind
• Reify (definition : MIR.DefId) (reason : Option CallReifyReason) : CallShimKind
• FnPtr (definition : MIR.DefId) (ty : MIR.TyId) : CallShimKind
• ClosureOnce (callOnce closure : MIR.DefId) (trackCaller : Bool) : CallShimKind
• ConstructCoroutineInClosure (definition : MIR.DefId) (receiverByRef : Bool) : CallShimKind
• ThreadLocal (definition : MIR.DefId) : CallShimKind
• FutureDropPoll (definition : MIR.DefId) (proxy impl : MIR.TyId) : CallShimKind
• DropGlue (definition : MIR.DefId) (ty : Option MIR.TyId) : CallShimKind
• Clone (definition : MIR.DefId) (ty : MIR.TyId) : CallShimKind
• FnPtrAsPtr (definition : MIR.DefId) (ty : MIR.TyId) : CallShimKind
• FnPtrFromPtr (definition : MIR.DefId) (ty : MIR.TyId) : CallShimKind
• AsyncDropGlueCtor (definition : MIR.DefId) (ty : MIR.TyId) : CallShimKind
• AsyncDropGlue (definition : MIR.DefId) (ty : MIR.TyId) : CallShimKind

def Miri.Interpreter.instReprCallShimKind.repr : CallShimKind → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.instReprCallShimKind : Repr CallShimKind

Equations

• Miri.Interpreter.instReprCallShimKind = { reprPrec := Miri.Interpreter.instReprCallShimKind.repr }

def Miri.Interpreter.instDecidableEqCallShimKind.decEq (x✝ x✝¹ : CallShimKind) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqCallShimKind : DecidableEq CallShimKind

Equations

• Miri.Interpreter.instDecidableEqCallShimKind = Miri.Interpreter.instDecidableEqCallShimKind.decEq

inductive Miri.Interpreter.CallInstanceKind : Type

• Item (definition : MIR.DefId) : CallInstanceKind
• Intrinsic (definition : MIR.DefId) : CallInstanceKind
• LlvmIntrinsic (definition : MIR.DefId) : CallInstanceKind
• Virtual (definition : MIR.DefId) (index : Nat) : CallInstanceKind
• Shim (shim : CallShimKind) : CallInstanceKind

@[instance_reducible]

instance Miri.Interpreter.instReprCallInstanceKind : Repr CallInstanceKind

Equations

• Miri.Interpreter.instReprCallInstanceKind = { reprPrec := Miri.Interpreter.instReprCallInstanceKind.repr }

def Miri.Interpreter.instReprCallInstanceKind.repr : CallInstanceKind → Nat → Std.Format

Equations

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

def Miri.Interpreter.instDecidableEqCallInstanceKind.decEq (x✝ x✝¹ : CallInstanceKind) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.instDecidableEqCallInstanceKind.decEq (Miri.Interpreter.CallInstanceKind.Item a) (Miri.Interpreter.CallInstanceKind.Item b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.Interpreter.instDecidableEqCallInstanceKind.decEq (Miri.Interpreter.CallInstanceKind.Item definition) (Miri.Interpreter.CallInstanceKind.Intrinsic definition_1) = isFalse ⋯
• Miri.Interpreter.instDecidableEqCallInstanceKind.decEq (Miri.Interpreter.CallInstanceKind.Item definition) (Miri.Interpreter.CallInstanceKind.LlvmIntrinsic definition_1) = isFalse ⋯
• Miri.Interpreter.instDecidableEqCallInstanceKind.decEq (Miri.Interpreter.CallInstanceKind.Item definition) (Miri.Interpreter.CallInstanceKind.Virtual definition_1 index) = isFalse ⋯
• Miri.Interpreter.instDecidableEqCallInstanceKind.decEq (Miri.Interpreter.CallInstanceKind.Item definition) (Miri.Interpreter.CallInstanceKind.Shim shim) = isFalse ⋯
• Miri.Interpreter.instDecidableEqCallInstanceKind.decEq (Miri.Interpreter.CallInstanceKind.Intrinsic definition) (Miri.Interpreter.CallInstanceKind.Item definition_1) = isFalse ⋯
• Miri.Interpreter.instDecidableEqCallInstanceKind.decEq (Miri.Interpreter.CallInstanceKind.Intrinsic definition) (Miri.Interpreter.CallInstanceKind.LlvmIntrinsic definition_1) = isFalse ⋯
• Miri.Interpreter.instDecidableEqCallInstanceKind.decEq (Miri.Interpreter.CallInstanceKind.Intrinsic definition) (Miri.Interpreter.CallInstanceKind.Virtual definition_1 index) = isFalse ⋯
• Miri.Interpreter.instDecidableEqCallInstanceKind.decEq (Miri.Interpreter.CallInstanceKind.Intrinsic definition) (Miri.Interpreter.CallInstanceKind.Shim shim) = isFalse ⋯
• Miri.Interpreter.instDecidableEqCallInstanceKind.decEq (Miri.Interpreter.CallInstanceKind.LlvmIntrinsic definition) (Miri.Interpreter.CallInstanceKind.Item definition_1) = isFalse ⋯
• Miri.Interpreter.instDecidableEqCallInstanceKind.decEq (Miri.Interpreter.CallInstanceKind.LlvmIntrinsic definition) (Miri.Interpreter.CallInstanceKind.Intrinsic definition_1) = isFalse ⋯
• Miri.Interpreter.instDecidableEqCallInstanceKind.decEq (Miri.Interpreter.CallInstanceKind.LlvmIntrinsic definition) (Miri.Interpreter.CallInstanceKind.Virtual definition_1 index) = isFalse ⋯
• Miri.Interpreter.instDecidableEqCallInstanceKind.decEq (Miri.Interpreter.CallInstanceKind.LlvmIntrinsic definition) (Miri.Interpreter.CallInstanceKind.Shim shim) = isFalse ⋯
• Miri.Interpreter.instDecidableEqCallInstanceKind.decEq (Miri.Interpreter.CallInstanceKind.Virtual definition index) (Miri.Interpreter.CallInstanceKind.Item definition_1) = isFalse ⋯
• Miri.Interpreter.instDecidableEqCallInstanceKind.decEq (Miri.Interpreter.CallInstanceKind.Virtual definition index) (Miri.Interpreter.CallInstanceKind.Intrinsic definition_1) = isFalse ⋯
• Miri.Interpreter.instDecidableEqCallInstanceKind.decEq (Miri.Interpreter.CallInstanceKind.Virtual definition index) (Miri.Interpreter.CallInstanceKind.LlvmIntrinsic definition_1) = isFalse ⋯
• Miri.Interpreter.instDecidableEqCallInstanceKind.decEq (Miri.Interpreter.CallInstanceKind.Virtual definition index) (Miri.Interpreter.CallInstanceKind.Shim shim) = isFalse ⋯
• Miri.Interpreter.instDecidableEqCallInstanceKind.decEq (Miri.Interpreter.CallInstanceKind.Shim shim) (Miri.Interpreter.CallInstanceKind.Item definition) = isFalse ⋯
• Miri.Interpreter.instDecidableEqCallInstanceKind.decEq (Miri.Interpreter.CallInstanceKind.Shim shim) (Miri.Interpreter.CallInstanceKind.Intrinsic definition) = isFalse ⋯
• Miri.Interpreter.instDecidableEqCallInstanceKind.decEq (Miri.Interpreter.CallInstanceKind.Shim shim) (Miri.Interpreter.CallInstanceKind.LlvmIntrinsic definition) = isFalse ⋯
• Miri.Interpreter.instDecidableEqCallInstanceKind.decEq (Miri.Interpreter.CallInstanceKind.Shim shim) (Miri.Interpreter.CallInstanceKind.Virtual definition index) = isFalse ⋯
• Miri.Interpreter.instDecidableEqCallInstanceKind.decEq (Miri.Interpreter.CallInstanceKind.Shim a) (Miri.Interpreter.CallInstanceKind.Shim b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqCallInstanceKind : DecidableEq CallInstanceKind

Equations

• Miri.Interpreter.instDecidableEqCallInstanceKind = Miri.Interpreter.instDecidableEqCallInstanceKind.decEq

structure Miri.Interpreter.CallInstance : Type

• kind : CallInstanceKind
• args : Array MIR.GenericArg

def Miri.Interpreter.instReprCallInstance.repr : CallInstance → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.instReprCallInstance : Repr CallInstance

Equations

• Miri.Interpreter.instReprCallInstance = { reprPrec := Miri.Interpreter.instReprCallInstance.repr }

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqCallInstance : DecidableEq CallInstance

Equations

• Miri.Interpreter.instDecidableEqCallInstance = Miri.Interpreter.instDecidableEqCallInstance.decEq

def Miri.Interpreter.instDecidableEqCallInstance.decEq (x✝ x✝¹ : CallInstance) : Decidable (x✝ = x✝¹)

Equations

• Miri.Interpreter.instDecidableEqCallInstance.decEq { kind := a, args := a_1 } { kind := b, args := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def Miri.Interpreter.CallShimKind.defId : CallShimKind → MIR.DefId

Pinned ShimKind::def_id: ClosureOnce selects call_once, not closure.

Equations

• (Miri.Interpreter.CallShimKind.VTable a).defId = a
• (Miri.Interpreter.CallShimKind.Reify a a_1).defId = a
• (Miri.Interpreter.CallShimKind.FnPtr a a_1).defId = a
• (Miri.Interpreter.CallShimKind.ClosureOnce a a_1 a_2).defId = a
• (Miri.Interpreter.CallShimKind.ConstructCoroutineInClosure a a_1).defId = a
• (Miri.Interpreter.CallShimKind.ThreadLocal a).defId = a
• (Miri.Interpreter.CallShimKind.FutureDropPoll a a_1 a_2).defId = a
• (Miri.Interpreter.CallShimKind.DropGlue a a_1).defId = a
• (Miri.Interpreter.CallShimKind.Clone a a_1).defId = a
• (Miri.Interpreter.CallShimKind.FnPtrAsPtr a a_1).defId = a
• (Miri.Interpreter.CallShimKind.FnPtrFromPtr a a_1).defId = a
• (Miri.Interpreter.CallShimKind.AsyncDropGlueCtor a a_1).defId = a
• (Miri.Interpreter.CallShimKind.AsyncDropGlue a a_1).defId = a

def Miri.Interpreter.CallInstanceKind.defId : CallInstanceKind → MIR.DefId

Equations

• (Miri.Interpreter.CallInstanceKind.Item a).defId = a
• (Miri.Interpreter.CallInstanceKind.Intrinsic a).defId = a
• (Miri.Interpreter.CallInstanceKind.LlvmIntrinsic a).defId = a
• (Miri.Interpreter.CallInstanceKind.Virtual a a_1).defId = a
• (Miri.Interpreter.CallInstanceKind.Shim a).defId = a.defId

def Miri.Interpreter.CallInstance.defId (self : CallInstance) : MIR.DefId

Equations

• self.defId = self.kind.defId