Pinned portable C memory/string arms of shims/foreign_items.rs and the read_c_str helper. Pointer checks are preserved even for zero-byte C accesses. Concrete string scanning has an explicit resource budget, whose exhaustion is Unknown; it is never treated as an empty string or a successful execution.

@[reducible, inline]

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

Equations

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

structure Miri.Interpreter.MemoryShims.Operations (P S D MD B I : Type) : Type

• checkPointer : Memory.Pointer (Option P) → M S Unit

  ptr_get_alloc_id(...,0), with source dangling/provenance behavior.

• readByte : Memory.Pointer (Option P) → M S UInt8
• readBytes : Memory.Pointer (Option P) → UInt64 → M S ByteArray
• offset : Memory.Pointer (Option P) → UInt64 → M S (Memory.Pointer (Option P))
• copy : Memory.Pointer (Option P) → Memory.Pointer (Option P) → UInt64 → Bool → M S Unit
• writeRepeatedByte : Memory.Pointer (Option P) → UInt8 → UInt64 → M S Unit
• writeI32 : Int32 → MD → M S Unit
• writeUsize : UInt64 → MD → M S Unit
• wcharLayout : M S (ABI.Size × ABI.Align)

  Actual libc wchar_t (u16 on Windows), not the Lean host's wchar type.

• checkAlignment : Memory.Pointer (Option P) → ABI.Align → M S Unit
• readUnsigned : Memory.Pointer (Option P) → ABI.Size → M S ABI.U128

structure Miri.Interpreter.MemoryShims.CoreHooks (P S D MD B I : Type) extends Miri.Interpreter.MemoryShims.Operations P S D MD B I : Type

• checkPointer : Memory.Pointer (Option P) → M S Unit
• readByte : Memory.Pointer (Option P) → M S UInt8
• readBytes : Memory.Pointer (Option P) → UInt64 → M S ByteArray
• offset : Memory.Pointer (Option P) → UInt64 → M S (Memory.Pointer (Option P))
• copy : Memory.Pointer (Option P) → Memory.Pointer (Option P) → UInt64 → Bool → M S Unit
• writeRepeatedByte : Memory.Pointer (Option P) → UInt8 → UInt64 → M S Unit
• writeI32 : Int32 → MD → M S Unit
• writeUsize : UInt64 → MD → M S Unit
• wcharLayout : M S (ABI.Size × ABI.Align)
• checkAlignment : Memory.Pointer (Option P) → ABI.Align → M S Unit
• readUnsigned : Memory.Pointer (Option P) → ABI.Size → M S ABI.U128
• foreign : ForeignItems.Core P S D MD (Memory.Pointer (Option P)) B I

structure Miri.Interpreter.MemoryShims.Hooks (P S D MD B I : Type) extends Miri.Interpreter.MemoryShims.Operations P S D MD B I : Type

• checkPointer : Memory.Pointer (Option P) → M S Unit
• readByte : Memory.Pointer (Option P) → M S UInt8
• readBytes : Memory.Pointer (Option P) → UInt64 → M S ByteArray
• offset : Memory.Pointer (Option P) → UInt64 → M S (Memory.Pointer (Option P))
• copy : Memory.Pointer (Option P) → Memory.Pointer (Option P) → UInt64 → Bool → M S Unit
• writeRepeatedByte : Memory.Pointer (Option P) → UInt8 → UInt64 → M S Unit
• writeI32 : Int32 → MD → M S Unit
• writeUsize : UInt64 → MD → M S Unit
• wcharLayout : M S (ABI.Size × ABI.Align)
• checkAlignment : Memory.Pointer (Option P) → ABI.Align → M S Unit
• readUnsigned : Memory.Pointer (Option P) → ABI.Size → M S ABI.U128
• foreign : ForeignItems.Hooks P S D MD (Memory.Pointer (Option P)) B I

def Miri.Interpreter.MemoryShims.Hooks.core {P S D MD B I : Type} (h : Hooks P S D MD B I) : CoreHooks P S D MD B I

Equations

• h.core = { toOperations := h.toOperations, foreign := h.foreign.toCore }

@[instance_reducible]

instance Miri.Interpreter.MemoryShims.instCoeOutHooksCoreHooks {P S D MD B I : Type} : CoeOut (Hooks P S D MD B I) (CoreHooks P S D MD B I)

Equations

• Miri.Interpreter.MemoryShims.instCoeOutHooksCoreHooks = { coe := Miri.Interpreter.MemoryShims.Hooks.core }

def Miri.Interpreter.MemoryShims.Source.memchr {P S D MD B I : Type} (h : CoreHooks P S D MD B I) (pointer : Memory.Pointer (Option P)) (count : UInt64) (reverse : Bool) (needle : UInt8) : M S (Option (UInt64 × Memory.Pointer (Option P)))

Each character is read separately; a match prevents all later accesses.

Equations

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

def Miri.Interpreter.MemoryShims.Source.readCString {P S D MD B I : Type} (h : CoreHooks P S D MD B I) (budget : Nat) (pointer : Memory.Pointer (Option P)) : M S ByteArray

Source read_c_str deliberately reads all bytes a second time after the terminator scan, including a zero-length read for the empty string.

Equations

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

def Miri.Interpreter.MemoryShims.Source.wcharLength {P S D MD B I : Type} (h : CoreHooks P S D MD B I) (budget : Nat) (pointer : Memory.Pointer (Option P)) : M S UInt64

Equations

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

def Miri.Interpreter.MemoryShims.Source.emulate {P S D MD B I : Type} (h : CoreHooks P S D MD B I) (budget : Nat) (name : String) (abi : ABI.FnAbi MIR.TyId) (args : Array (OpTy P)) (dest : MD) : M S (Option ForeignItems.EmulateItemResult)

All argument reads and mandatory pointer checks precede actual memory operations in the source order. memset truncates C int to unsigned char.

Equations

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

def Miri.Interpreter.MemoryShims.memchr {P S D MD B I : Type} (h : Hooks P S D MD B I) (pointer : Memory.Pointer (Option P)) (count : UInt64) (reverse : Bool) (needle : UInt8) : M S (Option (UInt64 × Memory.Pointer (Option P)))

Equations

• Miri.Interpreter.MemoryShims.memchr h pointer count reverse needle = Miri.Interpreter.MemoryShims.Source.memchr h.core pointer count reverse needle

def Miri.Interpreter.MemoryShims.readCString {P S D MD B I : Type} (h : Hooks P S D MD B I) (budget : Nat) (pointer : Memory.Pointer (Option P)) : M S ByteArray

Equations

• Miri.Interpreter.MemoryShims.readCString h budget pointer = Miri.Interpreter.MemoryShims.Source.readCString h.core budget pointer

def Miri.Interpreter.MemoryShims.wcharLength {P S D MD B I : Type} (h : Hooks P S D MD B I) (budget : Nat) (pointer : Memory.Pointer (Option P)) : M S UInt64

Equations

• Miri.Interpreter.MemoryShims.wcharLength h budget pointer = Miri.Interpreter.MemoryShims.Source.wcharLength h.core budget pointer

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

Equations

• Miri.Interpreter.MemoryShims.emulate h budget name abi args dest = Miri.Interpreter.MemoryShims.Source.emulate h.core budget name abi args dest

def Miri.Interpreter.MemoryShims.bind {P S D MD B I : Type} (h : Hooks P S D MD B I) (budget : Nat) : ForeignItems.Hooks P S D MD (Memory.Pointer (Option P)) B I

Preserve remaining portable source handlers and their fallback ordering.

Equations

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