Source port of Miri shims/{mod,foreign_items,alloc,env}.rs. OS-specific, compiler signature construction, allocation and host effects remain mandatory queries; dispatch, ABI checks, allocation policy and control ordering are here.

@[reducible, inline]

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

Equations

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

inductive Miri.Interpreter.ForeignItems.EmulateItemResult : Type

• NeedsReturn : EmulateItemResult
• NeedsUnwind : EmulateItemResult
• AlreadyJumped : EmulateItemResult
• NotSupported : EmulateItemResult

@[instance_reducible]

instance Miri.Interpreter.ForeignItems.instDecidableEqEmulateItemResult : DecidableEq EmulateItemResult

Equations

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

def Miri.Interpreter.ForeignItems.instReprEmulateItemResult.repr : EmulateItemResult → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.ForeignItems.instReprEmulateItemResult : Repr EmulateItemResult

Equations

• Miri.Interpreter.ForeignItems.instReprEmulateItemResult = { reprPrec := Miri.Interpreter.ForeignItems.instReprEmulateItemResult.repr }

inductive Miri.Interpreter.ForeignItems.Family : Type

• unix : Family
• windows : Family
• other : Family

@[instance_reducible]

instance Miri.Interpreter.ForeignItems.instDecidableEqFamily : DecidableEq Family

Equations

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

@[instance_reducible]

instance Miri.Interpreter.ForeignItems.instReprFamily : Repr Family

Equations

• Miri.Interpreter.ForeignItems.instReprFamily = { reprPrec := Miri.Interpreter.ForeignItems.instReprFamily.repr }

def Miri.Interpreter.ForeignItems.instReprFamily.repr : Family → Nat → Std.Format

Equations

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

inductive Miri.Interpreter.ForeignItems.Init : Type

• uninit : Init
• zero : Init

@[instance_reducible]

instance Miri.Interpreter.ForeignItems.instDecidableEqInit : DecidableEq Init

Equations

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

@[instance_reducible]

instance Miri.Interpreter.ForeignItems.instReprInit : Repr Init

Equations

• Miri.Interpreter.ForeignItems.instReprInit = { reprPrec := Miri.Interpreter.ForeignItems.instReprInit.repr }

def Miri.Interpreter.ForeignItems.instReprInit.repr : Init → Nat → Std.Format

Equations

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

inductive Miri.Interpreter.ForeignItems.AllocationKind : Type

• rust : AllocationKind
• c : AllocationKind
• miri : AllocationKind
• mmap : AllocationKind

@[instance_reducible]

instance Miri.Interpreter.ForeignItems.instDecidableEqAllocationKind : DecidableEq AllocationKind

Equations

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

@[instance_reducible]

instance Miri.Interpreter.ForeignItems.instReprAllocationKind : Repr AllocationKind

Equations

• Miri.Interpreter.ForeignItems.instReprAllocationKind = { reprPrec := Miri.Interpreter.ForeignItems.instReprAllocationKind.repr }

def Miri.Interpreter.ForeignItems.instReprAllocationKind.repr : AllocationKind → Nat → Std.Format

Equations

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

inductive Miri.Interpreter.ForeignItems.SignatureType : Type

• unit : SignatureType
• usize : SignatureType
• isize : SignatureType
• i32 : SignatureType
• u32 : SignatureType
• pointer : SignatureType
• unitPointer : SignatureType
• alignment : SignatureType
• never : SignatureType
• u64 : SignatureType
• u8 : SignatureType
• bool : SignatureType
• byteSlice : SignatureType
• functionPointer : SignatureType

@[instance_reducible]

instance Miri.Interpreter.ForeignItems.instDecidableEqSignatureType : DecidableEq SignatureType

Equations

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

def Miri.Interpreter.ForeignItems.instReprSignatureType.repr : SignatureType → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.ForeignItems.instReprSignatureType : Repr SignatureType

Equations

• Miri.Interpreter.ForeignItems.instReprSignatureType = { reprPrec := Miri.Interpreter.ForeignItems.instReprSignatureType.repr }

structure Miri.Interpreter.ForeignItems.Signature : Type

• conv : ABI.CanonAbi
• args : Array SignatureType
• ret : SignatureType

def Miri.Interpreter.ForeignItems.instDecidableEqSignature.decEq (x✝ x✝¹ : Signature) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.Interpreter.ForeignItems.instDecidableEqSignature : DecidableEq Signature

Equations

• Miri.Interpreter.ForeignItems.instDecidableEqSignature = Miri.Interpreter.ForeignItems.instDecidableEqSignature.decEq

def Miri.Interpreter.ForeignItems.instReprSignature.repr : Signature → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.ForeignItems.instReprSignature : Repr Signature

Equations

• Miri.Interpreter.ForeignItems.instReprSignature = { reprPrec := Miri.Interpreter.ForeignItems.instReprSignature.repr }

inductive Miri.Interpreter.ForeignItems.SpecialAllocatorMethod : Type

• Alloc : SpecialAllocatorMethod
• AllocZeroed : SpecialAllocatorMethod
• Dealloc : SpecialAllocatorMethod
• Realloc : SpecialAllocatorMethod

@[instance_reducible]

instance Miri.Interpreter.ForeignItems.instDecidableEqSpecialAllocatorMethod : DecidableEq SpecialAllocatorMethod

Equations

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

def Miri.Interpreter.ForeignItems.instReprSpecialAllocatorMethod.repr : SpecialAllocatorMethod → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.ForeignItems.instReprSpecialAllocatorMethod : Repr SpecialAllocatorMethod

Equations

• Miri.Interpreter.ForeignItems.instReprSpecialAllocatorMethod = { reprPrec := Miri.Interpreter.ForeignItems.instReprSpecialAllocatorMethod.repr }

inductive Miri.Interpreter.ForeignItems.AllocatorSymbol (Instance : Type) : Type

• redirect {Instance : Type} (symbol : String) : AllocatorSymbol Instance
• special {Instance : Type} (method : SpecialAllocatorMethod) : AllocatorSymbol Instance

def Miri.Interpreter.ForeignItems.mallocAlign (arch os : String) (size : UInt64) : Except StepError ABI.Align

Target architecture spellings are compiler target names, not host names.

Equations

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

def Miri.Interpreter.ForeignItems.checkRustAllocRequest (maximum size align : UInt64) : Except StepError ABI.Align

Equations

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

structure Miri.Interpreter.ForeignItems.SymbolCandidate (Instance : Type) : Type

• fnInstance : Instance
• crateId : Nat
• weak : Bool
• explicitSymbol : Bool
• symbol : String
• spanOrder : Nat × Nat

def Miri.Interpreter.ForeignItems.lookupSymbol {I : Type} (name : String) (symbols : Array (SymbolCandidate I)) : Except StepError (Option I)

Weak definitions lose to strong definitions; two equally weak definitions are an error, including two weak definitions. Compiler iteration order is kept.

Equations

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

inductive Miri.Interpreter.ForeignItems.ExportKind : Type

• function : ExportKind
• associatedFunction : ExportKind
• staticItem : ExportKind
• other : ExportKind

@[instance_reducible]

instance Miri.Interpreter.ForeignItems.instDecidableEqExportKind : DecidableEq ExportKind

Equations

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

@[instance_reducible]

instance Miri.Interpreter.ForeignItems.instReprExportKind : Repr ExportKind

Equations

• Miri.Interpreter.ForeignItems.instReprExportKind = { reprPrec := Miri.Interpreter.ForeignItems.instReprExportKind.repr }

def Miri.Interpreter.ForeignItems.instReprExportKind.repr : ExportKind → Nat → Std.Format

Equations

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

def Miri.Interpreter.ForeignItems.lookupFunctionFromSymbols {I S B : Type} (name : String) (symbols : Array (SymbolCandidate I)) (definitionKind : I → M S ExportKind) (loadMir : I → M S B) : M S (Option (B × I))

Compiler definition-kind checks precede MIR loading. A data export with a matching name must never become a callable fallback.

Equations

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

def Miri.Interpreter.ForeignItems.lookupStaticFromSymbols {I S : Type} (name : String) (symbols : Array (SymbolCandidate I)) (definitionKind : I → M S ExportKind) : M S (Option I)

Equations

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

structure Miri.Interpreter.ForeignItems.Core (P S D MD Ptr Body Instance : Type) : Type

• family : Family
• os : String
• arch : String
• maximumSize : UInt64
• noAllocShimSymbol : String
• allocatorSymbol : String → M S (Option (AllocatorSymbol Instance))
• lookupFunction : String → M S (Option (Body × Instance))
• forceAllocation : D → M S MD
• returnToBlock : Option MIR.BasicBlockId → M S Unit
• unwindToBlock : MIR.UnwindAction → M S Unit
• nativeEnabled : Bool
• callNative : String → MD → Array (OpTy P) → M S Bool
• expectedAbi : Signature → M S (ABI.FnAbi MIR.TyId)
• argumentCompat : ABI.ArgAbi MIR.TyId → ABI.ArgAbi MIR.TyId → M S Bool
• checkSymbolClash : String → M S Unit
• transmute : OpTy P → ABI.TyAndLayout MIR.TyId → M S (OpTy P)
• readUsize : OpTy P → M S UInt64
• readPointer : OpTy P → M S Ptr
• readI32 : OpTy P → M S Int32
• isNull : Ptr → M S Bool
• allocate : UInt64 → ABI.Align → Init → AllocationKind → M S Ptr
• deallocate : Ptr → Option (UInt64 × ABI.Align) → AllocationKind → M S Unit
• reallocate : Ptr → Option (UInt64 × ABI.Align) → UInt64 → ABI.Align → AllocationKind → M S Ptr
• writePointer : Ptr → MD → M S Unit
• writeNull : MD → M S Unit
• setEnomem : M S Unit
• startExit : Int32 → M S Unit
• specialDestination : D → M S MD

structure Miri.Interpreter.ForeignItems.Hooks (P S D MD Ptr Body Instance : Type) extends Miri.Interpreter.ForeignItems.Core P S D MD Ptr Body Instance : Type

Dispatch is separate from the nonrecursive source primitive dictionary. Portable/platform factories need only Core while constructing their bodies.

• family : Family
• os : String
• arch : String
• maximumSize : UInt64
• noAllocShimSymbol : String
• allocatorSymbol : String → M S (Option (AllocatorSymbol Instance))
• lookupFunction : String → M S (Option (Body × Instance))
• forceAllocation : D → M S MD
• returnToBlock : Option MIR.BasicBlockId → M S Unit
• unwindToBlock : MIR.UnwindAction → M S Unit
• nativeEnabled : Bool
• callNative : String → MD → Array (OpTy P) → M S Bool
• expectedAbi : Signature → M S (ABI.FnAbi MIR.TyId)
• argumentCompat : ABI.ArgAbi MIR.TyId → ABI.ArgAbi MIR.TyId → M S Bool
• checkSymbolClash : String → M S Unit
• transmute : OpTy P → ABI.TyAndLayout MIR.TyId → M S (OpTy P)
• readUsize : OpTy P → M S UInt64
• readPointer : OpTy P → M S Ptr
• readI32 : OpTy P → M S Int32
• isNull : Ptr → M S Bool
• allocate : UInt64 → ABI.Align → Init → AllocationKind → M S Ptr
• deallocate : Ptr → Option (UInt64 × ABI.Align) → AllocationKind → M S Unit
• reallocate : Ptr → Option (UInt64 × ABI.Align) → UInt64 → ABI.Align → AllocationKind → M S Ptr
• writePointer : Ptr → MD → M S Unit
• writeNull : MD → M S Unit
• setEnomem : M S Unit
• startExit : Int32 → M S Unit
• specialDestination : D → M S MD
• math : String → ABI.FnAbi MIR.TyId → Array (OpTy P) → MD → M S EmulateItemResult
• unix : String → ABI.FnAbi MIR.TyId → Array (OpTy P) → MD → M S EmulateItemResult
• windows : String → ABI.FnAbi MIR.TyId → Array (OpTy P) → MD → M S EmulateItemResult
• otherPortable : String → ABI.FnAbi MIR.TyId → Array (OpTy P) → MD → M S (Option EmulateItemResult)

  Other top-level arms (memory/string/Miri diagnostics) are required typed operations; NotSupported is reserved for names absent from the source table.

@[instance_reducible]

instance Miri.Interpreter.ForeignItems.instCoeOutHooksCore {P S D MD Ptr B I : Type} : CoeOut (Hooks P S D MD Ptr B I) (Core P S D MD Ptr B I)

Equations

• Miri.Interpreter.ForeignItems.instCoeOutHooksCore = { coe := Miri.Interpreter.ForeignItems.Hooks.toCore }

def Miri.Interpreter.ForeignItems.Core.checkAbi {P S D MD Ptr B I : Type} (h : Core P S D MD Ptr B I) (caller callee : ABI.FnAbi MIR.TyId) : M S Unit

Equations

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

def Miri.Interpreter.ForeignItems.Core.checkSignature {P S D MD Ptr B I : Type} (h : Core P S D MD Ptr B I) (name : String) (signature : Signature) (caller : ABI.FnAbi MIR.TyId) (args : Array (OpTy P)) : M S (Array (OpTy P))

Equations

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

def Miri.Interpreter.ForeignItems.checkAbi {P S D MD Ptr B I : Type} (h : Hooks P S D MD Ptr B I) (caller callee : ABI.FnAbi MIR.TyId) : M S Unit

Compatibility entry points project the lawful nonrecursive dictionary.

Equations

• Miri.Interpreter.ForeignItems.checkAbi h caller callee = h.checkAbi caller callee

def Miri.Interpreter.ForeignItems.checkSignature {P S D MD Ptr B I : Type} (h : Hooks P S D MD Ptr B I) (name : String) (signature : Signature) (caller : ABI.FnAbi MIR.TyId) (args : Array (OpTy P)) : M S (Array (OpTy P))

Equations

• Miri.Interpreter.ForeignItems.checkSignature h name signature caller args = h.checkSignature name signature caller args

def Miri.Interpreter.ForeignItems.specialAllocator {P S D MD Ptr B I : Type} (h : Hooks P S D MD Ptr B I) (method : SpecialAllocatorMethod) (name : String) (abi : ABI.FnAbi MIR.TyId) (args : Array (OpTy P)) (dest : D) : M S Unit

Equations

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

def Miri.Interpreter.ForeignItems.inner {P S D MD Ptr B I : Type} (h : Hooks P S D MD Ptr B I) (name : String) (abi : ABI.FnAbi MIR.TyId) (args : Array (OpTy P)) (dest : MD) : M S EmulateItemResult

Equations

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

def Miri.Interpreter.ForeignItems.emulate {P S D MD Ptr B I : Type} (h : Hooks P S D MD Ptr B I) (name : String) (abi : ABI.FnAbi MIR.TyId) (args : Array (OpTy P)) (dest : D) (ret : Option MIR.BasicBlockId) (unwind : MIR.UnwindAction) : M S (Option (B × I))

Equations

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

def Miri.Interpreter.ForeignItems.emulateDynSym {P S D MD Ptr B I : Type} (h : Hooks P S D MD Ptr B I) (name : String) (abi : ABI.FnAbi MIR.TyId) (args : Array (OpTy P)) (dest : D) (ret : Option MIR.BasicBlockId) (unwind : MIR.UnwindAction) : M S Unit

Equations

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

def Miri.Interpreter.ForeignItems.initialEnvironment (communicate : Bool) (forwarded : Array String) (environment overrides : Array (String × String)) : Array (String × String)

OS strings are supplied as already-decoded target strings. Unix byte encoding and Windows case rules belong to their separate OS modules.

Equations

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

def Miri.Interpreter.ForeignItems.getPid {S : Type} (communicate : Bool) (hostPid : M S UInt32) : M S UInt32

Equations

• Miri.Interpreter.ForeignItems.getPid communicate hostPid = if communicate = true then hostPid else pure 1000

def Miri.Interpreter.ForeignItems.getTid (family : Family) (pid thread : UInt32) : Except StepError UInt32

Equations

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