Pinned shims/extern_static.rs and machine.rs::extern_static_pointer. Every pointer is canonical strict Miri provenance; extra import indirection is allocated and written rather than represented by a fabricated pointer.

@[reducible, inline]

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

Equations

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

structure Miri.Interpreter.ExternStatic.State : Type

• symbols : Array (String × Memory.StrictPointer)
• imports : Array (String × Memory.StrictPointer)
• missingWeak : Option Memory.StrictPointer

@[instance_reducible]

instance Miri.Interpreter.ExternStatic.instReprState : Repr State

Equations

• Miri.Interpreter.ExternStatic.instReprState = { reprPrec := Miri.Interpreter.ExternStatic.instReprState.repr }

def Miri.Interpreter.ExternStatic.instReprState.repr : State → Nat → Std.Format

Equations

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

inductive Miri.Interpreter.ExternStatic.InitialValue : Type

• zeroByte : InitialValue
• nullPointer : InitialValue

@[instance_reducible]

instance Miri.Interpreter.ExternStatic.instDecidableEqInitialValue : DecidableEq InitialValue

Equations

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

@[instance_reducible]

instance Miri.Interpreter.ExternStatic.instReprInitialValue : Repr InitialValue

Equations

• Miri.Interpreter.ExternStatic.instReprInitialValue = { reprPrec := Miri.Interpreter.ExternStatic.instReprInitialValue.repr }

def Miri.Interpreter.ExternStatic.instReprInitialValue.repr : InitialValue → Nat → Std.Format

Equations

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

structure Miri.Interpreter.ExternStatic.InitHooks (S : Type) : Type

• get : M S State
• put : State → M S Unit
• unix : Bool
• os : String
• gnu : Bool
• environ : M S Memory.StrictPointer
• allocateValue : InitialValue → M S Memory.StrictPointer
• allocatePointerCell : Memory.StrictPointer → M S Memory.StrictPointer
• isDynSym : String → M S Bool
• functionPointer : String → M S Memory.StrictPointer

def Miri.Interpreter.ExternStatic.add {S : Type} (h : InitHooks S) (name : String) (pointer : Memory.StrictPointer) : M S Unit

Equations

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

def Miri.Interpreter.ExternStatic.addWeak {S : Type} (h : InitHooks S) (name : String) (pointer : Memory.StrictPointer) : M S Unit

Equations

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

def Miri.Interpreter.ExternStatic.weakFunctions {S : Type} (h : InitHooks S) (names : Array String) : M S Unit

Equations

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

def Miri.Interpreter.ExternStatic.initExternStatics {S : Type} (h : InitHooks S) : M S Unit

Equations

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

inductive Miri.Interpreter.ExternStatic.ImportLinkage : Type

• none : ImportLinkage
• externalWeak : ImportLinkage
• other : ImportLinkage

@[instance_reducible]

instance Miri.Interpreter.ExternStatic.instDecidableEqImportLinkage : DecidableEq ImportLinkage

Equations

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

def Miri.Interpreter.ExternStatic.instReprImportLinkage.repr : ImportLinkage → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.ExternStatic.instReprImportLinkage : Repr ImportLinkage

Equations

• Miri.Interpreter.ExternStatic.instReprImportLinkage = { reprPrec := Miri.Interpreter.ExternStatic.instReprImportLinkage.repr }

structure Miri.Interpreter.ExternStatic.Declaration : Type

• symbol : String
• size : ABI.Size
• align : ABI.Align
• linkage : ImportLinkage

structure Miri.Interpreter.ExternStatic.AllocationInfo : Type

• size : ABI.Size
• align : ABI.Align

structure Miri.Interpreter.ExternStatic.ResolveHooks (S I : Type) : Type

• get : M S State
• declaration : MIR.DefId → M S Declaration
• pointerSize : ABI.Size
• checkSymbolClash : String → M S Unit
• allocationInfo : Memory.AllocId → M S AllocationInfo
• lookupStatic : String → M S (Option I)
• evalGlobal : I → M S Memory.StrictPointer
• declarationMutable : MIR.DefId → M S Bool
• allocationMutable : Memory.AllocId → M S Bool

def Miri.Interpreter.ExternStatic.resolve {S I : Type} (h : ResolveHooks S I) (definition : MIR.DefId) : M S Memory.StrictPointer

Equations

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

def Miri.Interpreter.ExternStatic.provenanceRoots (state : State) : Array Memory.StrictPointer

Equations

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