Concrete ghost visitors for source state embeddings. No dereference, callback invocation or dropped missing typed tokens. Remaining OS-owned state requires its own actual visitor before a complete interpreter is available.

def Miri.Interpreter.ProvenanceGC.Roots.inactiveStacks (roots : Roots) (manager : Concurrency.ThreadManager) (registry : ThreadStacks.Registry) : Except StepError Roots

The active stack is visited by the GC driver, not duplicated here.

Equations

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

def Miri.Interpreter.ProvenanceGC.Roots.threadTls (roots : Roots) (data : ThreadTlsData Memory.Provenance) : Except StepError Roots

Equations

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

def Miri.Interpreter.ProvenanceGC.Roots.threadLocalAllocations (roots : Roots) (manager : Concurrency.ThreadManager) (entries : Array (ThreadLocalEntry Memory.Provenance)) : Except StepError Roots

Match the authoritative manager entries against actual typed pointers.

Equations

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

def Miri.Interpreter.ProvenanceGC.Roots.envVars {Os : Type} (roots : Roots) (env : EnvVars.State (Option Memory.Provenance) Os) : Roots

Equations

• roots.envVars env = Array.foldl Miri.Interpreter.ProvenanceGC.Roots.pointer roots (Miri.Interpreter.EnvVars.provenanceRoots env)

def Miri.Interpreter.ProvenanceGC.Roots.externStatics (roots : Roots) (state : ExternStatic.State) : Roots

Equations

• roots.externStatics state = Array.foldl Miri.Interpreter.ProvenanceGC.Roots.strictPointer roots (Miri.Interpreter.ExternStatic.provenanceRoots state)

def Miri.Interpreter.ProvenanceGC.Roots.mainReturnPlace {E H : Type} (roots : Roots) (state : MainThreadState Memory.Provenance E H) : Except StepError Roots

Main's saved return place remains a root even when its stack is empty.

Equations

• roots.mainReturnPlace state = match state.mainReturnPlace with | none => Except.ok roots | some place => roots.memPlace place.mplace

def Miri.Interpreter.ProvenanceGC.Roots.weakMemory {Payload : Type} (roots : Roots) (registry : MemoryExtras.Registry Payload) : Except StepError Roots

Source allocation race-handler visitor traces every retained weak-buffer value. Sync objects are intentionally omitted by source AllocExtra::visit. Their captured representation metadata must not create extra strong roots.

Equations

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