C-varargs pipelines and compatibility recursion from pinned intrinsics.rs, with memory.rs's symbolic VaList allocation lifecycle and partial updates.

inductive Miri.Interpreter.VaTypeInfo : Type

• signedInteger (kind : MIR.IntegerKind) : VaTypeInfo
• unsignedInteger (kind : MIR.IntegerKind) : VaTypeInfo
• pointer (pointee : MIR.TyId) : VaTypeInfo
• other : VaTypeInfo

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqVaTypeInfo : DecidableEq VaTypeInfo

Equations

• Miri.Interpreter.instDecidableEqVaTypeInfo = Miri.Interpreter.instDecidableEqVaTypeInfo.decEq

def Miri.Interpreter.instDecidableEqVaTypeInfo.decEq (x✝ x✝¹ : VaTypeInfo) : Decidable (x✝ = x✝¹)

Equations

• Miri.Interpreter.instDecidableEqVaTypeInfo.decEq (Miri.Interpreter.VaTypeInfo.signedInteger a) (Miri.Interpreter.VaTypeInfo.signedInteger b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.Interpreter.instDecidableEqVaTypeInfo.decEq (Miri.Interpreter.VaTypeInfo.signedInteger kind) (Miri.Interpreter.VaTypeInfo.unsignedInteger kind_1) = isFalse ⋯
• Miri.Interpreter.instDecidableEqVaTypeInfo.decEq (Miri.Interpreter.VaTypeInfo.signedInteger kind) (Miri.Interpreter.VaTypeInfo.pointer pointee) = isFalse ⋯
• Miri.Interpreter.instDecidableEqVaTypeInfo.decEq (Miri.Interpreter.VaTypeInfo.signedInteger kind) Miri.Interpreter.VaTypeInfo.other = isFalse ⋯
• Miri.Interpreter.instDecidableEqVaTypeInfo.decEq (Miri.Interpreter.VaTypeInfo.unsignedInteger kind) (Miri.Interpreter.VaTypeInfo.signedInteger kind_1) = isFalse ⋯
• Miri.Interpreter.instDecidableEqVaTypeInfo.decEq (Miri.Interpreter.VaTypeInfo.unsignedInteger a) (Miri.Interpreter.VaTypeInfo.unsignedInteger b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.Interpreter.instDecidableEqVaTypeInfo.decEq (Miri.Interpreter.VaTypeInfo.unsignedInteger kind) (Miri.Interpreter.VaTypeInfo.pointer pointee) = isFalse ⋯
• Miri.Interpreter.instDecidableEqVaTypeInfo.decEq (Miri.Interpreter.VaTypeInfo.unsignedInteger kind) Miri.Interpreter.VaTypeInfo.other = isFalse ⋯
• Miri.Interpreter.instDecidableEqVaTypeInfo.decEq (Miri.Interpreter.VaTypeInfo.pointer pointee) (Miri.Interpreter.VaTypeInfo.signedInteger kind) = isFalse ⋯
• Miri.Interpreter.instDecidableEqVaTypeInfo.decEq (Miri.Interpreter.VaTypeInfo.pointer pointee) (Miri.Interpreter.VaTypeInfo.unsignedInteger kind) = isFalse ⋯
• Miri.Interpreter.instDecidableEqVaTypeInfo.decEq (Miri.Interpreter.VaTypeInfo.pointer a) (Miri.Interpreter.VaTypeInfo.pointer b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.Interpreter.instDecidableEqVaTypeInfo.decEq (Miri.Interpreter.VaTypeInfo.pointer pointee) Miri.Interpreter.VaTypeInfo.other = isFalse ⋯
• Miri.Interpreter.instDecidableEqVaTypeInfo.decEq Miri.Interpreter.VaTypeInfo.other (Miri.Interpreter.VaTypeInfo.signedInteger kind) = isFalse ⋯
• Miri.Interpreter.instDecidableEqVaTypeInfo.decEq Miri.Interpreter.VaTypeInfo.other (Miri.Interpreter.VaTypeInfo.unsignedInteger kind) = isFalse ⋯
• Miri.Interpreter.instDecidableEqVaTypeInfo.decEq Miri.Interpreter.VaTypeInfo.other (Miri.Interpreter.VaTypeInfo.pointer pointee) = isFalse ⋯
• Miri.Interpreter.instDecidableEqVaTypeInfo.decEq Miri.Interpreter.VaTypeInfo.other Miri.Interpreter.VaTypeInfo.other = isTrue ⋯

@[instance_reducible]

instance Miri.Interpreter.instReprVaTypeInfo : Repr VaTypeInfo

Equations

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

def Miri.Interpreter.instReprVaTypeInfo.repr : VaTypeInfo → Nat → Std.Format

Equations

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

inductive Miri.Interpreter.VarArgCompatible : Type

• compatible : VarArgCompatible
• incompatible : VarArgCompatible
• castInteger (sourceSigned : Bool) : VarArgCompatible

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqVarArgCompatible : DecidableEq VarArgCompatible

Equations

• Miri.Interpreter.instDecidableEqVarArgCompatible = Miri.Interpreter.instDecidableEqVarArgCompatible.decEq

def Miri.Interpreter.instDecidableEqVarArgCompatible.decEq (x✝ x✝¹ : VarArgCompatible) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.instDecidableEqVarArgCompatible.decEq Miri.Interpreter.VarArgCompatible.compatible Miri.Interpreter.VarArgCompatible.compatible = isTrue ⋯
• Miri.Interpreter.instDecidableEqVarArgCompatible.decEq Miri.Interpreter.VarArgCompatible.compatible (Miri.Interpreter.VarArgCompatible.castInteger sourceSigned) = isFalse ⋯
• Miri.Interpreter.instDecidableEqVarArgCompatible.decEq Miri.Interpreter.VarArgCompatible.incompatible Miri.Interpreter.VarArgCompatible.incompatible = isTrue ⋯
• Miri.Interpreter.instDecidableEqVarArgCompatible.decEq Miri.Interpreter.VarArgCompatible.incompatible (Miri.Interpreter.VarArgCompatible.castInteger sourceSigned) = isFalse ⋯
• Miri.Interpreter.instDecidableEqVarArgCompatible.decEq (Miri.Interpreter.VarArgCompatible.castInteger sourceSigned) Miri.Interpreter.VarArgCompatible.compatible = isFalse ⋯
• Miri.Interpreter.instDecidableEqVarArgCompatible.decEq (Miri.Interpreter.VarArgCompatible.castInteger sourceSigned) Miri.Interpreter.VarArgCompatible.incompatible = isFalse ⋯

@[instance_reducible]

instance Miri.Interpreter.instReprVarArgCompatible : Repr VarArgCompatible

Equations

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

def Miri.Interpreter.instReprVarArgCompatible.repr : VarArgCompatible → Nat → Std.Format

Equations

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

structure Miri.Interpreter.IntrinsicVarArgsHooks (P S C V : Type) : Type

• getLists : S → Array (Memory.AllocId × List V)
• setLists : S → Array (Memory.AllocId × List V) → S
• markDead : S → Memory.AllocId → ABI.Size → ABI.Align → S
• reserveAllocId : C → RvalueM S Memory.AllocId
• globalRootPointer : C → Memory.AllocId → RvalueM S (Memory.Pointer (Option P))
• resolvePointer : C → Memory.Pointer (Option P) → RvalueM S (Memory.AllocId × ABI.Size)
• destLayout : V → ABI.TyAndLayout MIR.TyId
• layoutOf : C → MIR.TyId → RvalueM S (ABI.TyAndLayout MIR.TyId)
• typeInfo : C → MIR.TyId → RvalueM S VaTypeInfo
• identicalCTypes : C → MIR.TyId → MIR.TyId → RvalueM S Bool
• isCVoid : C → MIR.TyId → RvalueM S Bool
• vaListFields : C → MIR.TyId → RvalueM S (Array MIR.TyId)
• isRawPointer : C → MIR.TyId → RvalueM S Bool
• projectField : C → V → Nat → RvalueM S V
• derefPointer : C → OpTy P → RvalueM S V
• placePointer : V → Except StepError (Memory.Pointer (Option P))
• readPointer : C → V → RvalueM S (Memory.Pointer (Option P))
• readScalar : C → V → RvalueM S (Memory.Scalar P)
• writePointer : C → Memory.Pointer (Option P) → V → RvalueM S Unit
• forceAllocation : C → V → RvalueM S V
• writeBytesPointer : C → Memory.Pointer (Option P) → UInt8 → ABI.Size → RvalueM S Unit
• copyAllowTransmute : C → V → V → RvalueM S Unit

def Miri.Interpreter.IntrinsicVarArgs.keyField {P S C V : Type} (h : IntrinsicVarArgsHooks P S C V) (choice : C) (place : V) : RvalueM S V

First raw-pointer field of the target-specific VaListImpl after unwrapping its outer field. Compiler field metadata is required and never guessed.

Equations

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

def Miri.Interpreter.IntrinsicVarArgs.getList {P S C V : Type} (h : IntrinsicVarArgsHooks P S C V) (choice : C) (pointer : Memory.Pointer (Option P)) : RvalueM S (List V)

Equations

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

def Miri.Interpreter.IntrinsicVarArgs.deallocateList {P S C V : Type} (h : IntrinsicVarArgsHooks P S C V) (choice : C) (pointer : Memory.Pointer (Option P)) : RvalueM S (List V)

Source swap_remove and dead_alloc_map update occur before caller validation or copying of a va_arg value. Errors retain this invalidation.

Equations

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

def Miri.Interpreter.IntrinsicVarArgs.createList {P S C V : Type} (h : IntrinsicVarArgsHooks P S C V) (choice : C) (values : List V) : RvalueM S (Memory.Pointer (Option P))

Map insertion precedes global-root pointer creation, preserving the source partial update even when the compiler/machine root-pointer query is unknown.

Equations

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

def Miri.Interpreter.IntrinsicVarArgs.compatibleTypes {P S C V : Type} (h : IntrinsicVarArgsHooks P S C V) (choice : C) (fuel : Nat) (caller callee : MIR.TyId) : RvalueM S VarArgCompatible

Exact source compatibility rules, with compiler C-type identity before layout queries. Pointer target signedness differences require no value read.

Equations

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

def Miri.Interpreter.IntrinsicVarArgs.validateArgument {P S C V : Type} [Memory.PointerProvenance P] (h : IntrinsicVarArgsHooks P S C V) (choice : C) (fuel : Nat) (source : V) (target : ABI.TyAndLayout MIR.TyId) : RvalueM S Unit

Equations

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

def Miri.Interpreter.IntrinsicVarArgs.copy {P S C V : Type} (h : IntrinsicVarArgsHooks P S C V) (choice : C) (source : OpTy P) (dest : V) : RvalueM S Unit

Equations

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

def Miri.Interpreter.IntrinsicVarArgs.finish {P S C V : Type} (h : IntrinsicVarArgsHooks P S C V) (choice : C) (source : OpTy P) : RvalueM S Unit

Equations

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

def Miri.Interpreter.IntrinsicVarArgs.next {P S C V : Type} [Memory.PointerProvenance P] (h : IntrinsicVarArgsHooks P S C V) (choice : C) (fuel : Nat) (source : OpTy P) (dest : V) : RvalueM S Unit

Equations

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