Pinned shims/sig.rs signature/varargs policies, and rustc interpret/intrinsics.rs::validate_c_variadic_compatible_ty. Query budgets are concrete execution resources; their exhaustion is unresolved, never UB/success.

@[reducible, inline]

abbrev Miri.Interpreter.ShimSignatures.M (σ α : Type) : Type

Equations

• Miri.Interpreter.ShimSignatures.M = EStateM Miri.Interpreter.StepError

inductive Miri.Interpreter.ShimSignatures.Compatible : Type

• yes : Compatible
• no : Compatible
• castInteger (sourceSigned : Bool) : Compatible

@[instance_reducible]

instance Miri.Interpreter.ShimSignatures.instDecidableEqCompatible : DecidableEq Compatible

Equations

• Miri.Interpreter.ShimSignatures.instDecidableEqCompatible = Miri.Interpreter.ShimSignatures.instDecidableEqCompatible.decEq

def Miri.Interpreter.ShimSignatures.instDecidableEqCompatible.decEq (x✝ x✝¹ : Compatible) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.ShimSignatures.instDecidableEqCompatible.decEq Miri.Interpreter.ShimSignatures.Compatible.yes Miri.Interpreter.ShimSignatures.Compatible.yes = isTrue ⋯
• Miri.Interpreter.ShimSignatures.instDecidableEqCompatible.decEq Miri.Interpreter.ShimSignatures.Compatible.yes (Miri.Interpreter.ShimSignatures.Compatible.castInteger sourceSigned) = isFalse ⋯
• Miri.Interpreter.ShimSignatures.instDecidableEqCompatible.decEq Miri.Interpreter.ShimSignatures.Compatible.no Miri.Interpreter.ShimSignatures.Compatible.no = isTrue ⋯
• Miri.Interpreter.ShimSignatures.instDecidableEqCompatible.decEq Miri.Interpreter.ShimSignatures.Compatible.no (Miri.Interpreter.ShimSignatures.Compatible.castInteger sourceSigned) = isFalse ⋯

@[instance_reducible]

instance Miri.Interpreter.ShimSignatures.instReprCompatible : Repr Compatible

Equations

• Miri.Interpreter.ShimSignatures.instReprCompatible = { reprPrec := Miri.Interpreter.ShimSignatures.instReprCompatible.repr }

def Miri.Interpreter.ShimSignatures.instReprCompatible.repr : Compatible → Nat → Std.Format

Equations

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

structure Miri.Interpreter.ShimSignatures.Varargs (P : Type) : Type

• args : Array (OpTy P)
• alreadyGone : Nat

structure Miri.Interpreter.ShimSignatures.Hooks (P S D MD Ptr B I : Type) : Type

• foreign : ForeignItems.Hooks P S D MD Ptr B I
• types : LayoutCompat.Queries MIR.TyId S
• isCVoid : MIR.TyId → M S Bool
• readScalar : OpTy P → M S (Memory.Scalar P)
• hostUsizeBits : Nat

  Width of the host usize used by source strict_add diagnostics.

structure Miri.Interpreter.ShimSignatures.CoreHooks (P S D MD Ptr B I : Type) : Type

Nonrecursive exact-signature effects for fixed shims that do not need variadic type compatibility. This avoids requiring a complete platform ForeignItems dispatch merely to validate one source family.

• foreign : ForeignItems.Core P S D MD Ptr B I

structure Miri.Interpreter.ShimSignatures.PrimitiveHooks (P S : Type) : Type

Signature-only projection for source dispatchers that need no recursive foreign-item fallback. This keeps fixed shim validation tied to the actual ABI/symbol/transmute primitives while avoiding a dependency on a complete platform hook record.

• family : ForeignItems.Family
• os : String
• checkAbi : ABI.FnAbi MIR.TyId → ABI.FnAbi MIR.TyId → M S Unit
• checkSymbolClash : String → M S Unit
• transmute : OpTy P → ABI.TyAndLayout MIR.TyId → M S (OpTy P)

def Miri.Interpreter.ShimSignatures.primitiveView {P S D MD Ptr B I : Type} (h : Hooks P S D MD Ptr B I) : PrimitiveHooks P S

Equations

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

def Miri.Interpreter.ShimSignatures.compatible {P S D MD Ptr B I : Type} (h : Hooks P S D MD Ptr B I) : Nat → MIR.TyId → MIR.TyId → M S Compatible

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.ShimSignatures.compatible h 0 x✝¹ x✝ = throw (Miri.Interpreter.StepError.resourceExhaustion "C variadic type recursion budget")

def Miri.Interpreter.ShimSignatures.fixed {P S D MD Ptr B I : Type} (h : Hooks P S D MD Ptr B I) (name : String) (expected : M S (ABI.FnAbi MIR.TyId)) (count : Nat) (caller : ABI.FnAbi MIR.TyId) (args : Array (OpTy P)) : M S (Array (OpTy P))

The closure has already built the exact compiler signature (source ShimSig.as_abi); ABI checks precede symbol-clash checks and operand transmutes.

Equations

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

def Miri.Interpreter.ShimSignatures.fixedCore {P S D MD Ptr B I : Type} (h : CoreHooks P S D MD Ptr B I) (name : String) (expected : M S (ABI.FnAbi MIR.TyId)) (count : Nat) (caller : ABI.FnAbi MIR.TyId) (args : Array (OpTy P)) : M S (Array (OpTy P))

Fixed-signature source path over the nonrecursive foreign primitive core; the ABI check, symbol clash, then argument transmute order is unchanged.

Equations

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

def Miri.Interpreter.ShimSignatures.fixedPrimitive {P S : Type} (h : PrimitiveHooks P S) (name : String) (expected : M S (ABI.FnAbi MIR.TyId)) (count : Nat) (caller : ABI.FnAbi MIR.TyId) (args : Array (OpTy P)) : M S (Array (OpTy P))

Fixed shim validation over the minimal source signature primitives. The source order remains ABI check, symbol clash, then argument transmutation.

Equations

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

def Miri.Interpreter.ShimSignatures.variadic {P S D MD Ptr B I : Type} (h : Hooks P S D MD Ptr B I) (name : String) (expected : M S (ABI.FnAbi MIR.TyId)) (count : Nat) (caller : ABI.FnAbi MIR.TyId) (args : Array (OpTy P)) : M S (Array (OpTy P) × Varargs P)

Equations

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

def Miri.Interpreter.ShimSignatures.take {P S D MD Ptr B I : Type} [Memory.PointerProvenance P] (h : Hooks P S D MD Ptr B I) (budget : Nat) (types : M S (Array MIR.TyId)) (varargs : Varargs P) : M S (Array (OpTy P) × Varargs P)

Check the entire prefix for C type compatibility before transmuting any operand. Signed/unsigned pairs share source signed-at-width value checking.

Equations

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

def Miri.Interpreter.ShimSignatures.deprecated {P S D MD Ptr B I : Type} (h : Hooks P S D MD Ptr B I) (name : String) (conv : ABI.CanonAbi) (caller : ABI.FnAbi MIR.TyId) (args : Array (OpTy P)) (count : Nat) : M S (Array (OpTy P))

Equations

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

def Miri.Interpreter.ShimSignatures.llvmIntrinsic {P S D MD Ptr B I : Type} (h : Hooks P S D MD Ptr B I) (name : String) (args : Array (OpTy P)) (count : Nat) : M S (Array (OpTy P))

Equations

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