unix/foreign_items.rs::is_dyn_sym, dlsym and _Unwind_RaiseException. Dynamic symbols remain FnVal::Other; data symbols remain their actual pointers.

@[reducible, inline]

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

Equations

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

structure Miri.Interpreter.UnixDynamic.Symbol : Type

• name : String

@[instance_reducible]

instance Miri.Interpreter.UnixDynamic.instDecidableEqSymbol : DecidableEq Symbol

Equations

• Miri.Interpreter.UnixDynamic.instDecidableEqSymbol = Miri.Interpreter.UnixDynamic.instDecidableEqSymbol.decEq

def Miri.Interpreter.UnixDynamic.instDecidableEqSymbol.decEq (x✝ x✝¹ : Symbol) : Decidable (x✝ = x✝¹)

Equations

• Miri.Interpreter.UnixDynamic.instDecidableEqSymbol.decEq { name := a } { name := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Miri.Interpreter.UnixDynamic.instReprSymbol.repr : Symbol → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.UnixDynamic.instReprSymbol : Repr Symbol

Equations

• Miri.Interpreter.UnixDynamic.instReprSymbol = { reprPrec := Miri.Interpreter.UnixDynamic.instReprSymbol.repr }

def Miri.Interpreter.UnixDynamic.isDynamic (os env name : String) : Bool

Equations

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

structure Miri.Interpreter.UnixDynamic.Hooks (S Place B I : Type) : Type

• signatures : ShimSignatures.PrimitiveHooks Memory.Provenance S
• signature : String → M S (ABI.FnAbi MIR.TyId)
• targetEnv : String
• readUsize : OpTy Memory.Provenance → M S UInt64
• readPointer : OpTy Memory.Provenance → M S (Memory.Pointer (Option Memory.Provenance))
• readCString : Memory.Pointer (Option Memory.Provenance) → M S ByteArray
• functionPointer : Symbol → M S (Memory.Pointer (Option Memory.Provenance))
• externStatic : String → M S (Option (Memory.Pointer (Option Memory.Provenance)))
• writePointer : Memory.Pointer (Option Memory.Provenance) → MPlaceTy Memory.Provenance → M S Unit
• writeNull : MPlaceTy Memory.Provenance → M S Unit
• startUnwind : OpTy Memory.Provenance → M S Unit

def Miri.Interpreter.UnixDynamic.emulate {Place S B I : Type} (h : Hooks S Place B I) (name : String) (abi : ABI.FnAbi MIR.TyId) (args : Array (OpTy Memory.Provenance)) (dest : MPlaceTy Memory.Provenance) : M S (Option ForeignItems.EmulateItemResult)

Equations

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

def Miri.Interpreter.UnixDynamic.bindStrings {Place S B I : Type} (strings : MemoryShims.Hooks Memory.Provenance S Place (MPlaceTy Memory.Provenance) B I) (scanBudget : Nat) (base : Hooks S Place B I) : Hooks S Place B I

Equations

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

def Miri.Interpreter.UnixDynamic.bindFunctions {Place K U Other B I : Type} (functions : FunctionPointers.Hooks K U Other) (inject : Symbol → Other) (base : Hooks (MachineHooks.State K U) Place B I) : Hooks (MachineHooks.State K U) Place B I

Equations

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

def Miri.Interpreter.UnixDynamic.bindStatics {Place U K B I : Type} (statics : U → ExternStatic.State) (base : Hooks (MachineHooks.State K U) Place B I) : Hooks (MachineHooks.State K U) Place B I

Actual exported data symbols share the machine's ExternStatic map; the source checks them only after the dynamic-function whitelist.

Equations

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

def Miri.Interpreter.UnixDynamic.bindUnwind {Place K U C Other B I : Type} (unwind : Unwind.Hooks K U C Other) (choice : C) (base : Hooks (MachineHooks.State K U) Place B I) : Hooks (MachineHooks.State K U) Place B I

Equations

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