Tree Borrows adapters for the three Miri Machine memory hooks.

The caller order in pinned machine.rs is represented here: optional allocation diagnostics, data-race handling, Tree Borrows, synchronization objects, and (for deallocation) span/address-map release. The data-race, sync-object, diagnostic, span, and allocation-ID operations remain callbacks; this module does not pretend to implement those machine subsystems. Read and write adapters update the live allocation's BorrowTree extra before returning a Tree Borrows failure, as the source mutates AllocExtra in place.

inductive Miri.TreeBorrows.MachineMemoryHooks.SyncAccessKind : Type

• Read : SyncAccessKind
• Write : SyncAccessKind
• Dealloc : SyncAccessKind

@[instance_reducible]

instance Miri.TreeBorrows.MachineMemoryHooks.instDecidableEqSyncAccessKind : DecidableEq SyncAccessKind

Equations

• Miri.TreeBorrows.MachineMemoryHooks.instDecidableEqSyncAccessKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Miri.TreeBorrows.MachineMemoryHooks.instReprSyncAccessKind.repr : SyncAccessKind → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.MachineMemoryHooks.instReprSyncAccessKind : Repr SyncAccessKind

Equations

• Miri.TreeBorrows.MachineMemoryHooks.instReprSyncAccessKind = { reprPrec := Miri.TreeBorrows.MachineMemoryHooks.instReprSyncAccessKind.repr }

@[instance_reducible]

instance Miri.TreeBorrows.MachineMemoryHooks.instInhabitedSyncAccessKind : Inhabited SyncAccessKind

Equations

• Miri.TreeBorrows.MachineMemoryHooks.instInhabitedSyncAccessKind = { default := Miri.TreeBorrows.MachineMemoryHooks.instInhabitedSyncAccessKind.default }

inductive Miri.TreeBorrows.MachineMemoryHooks.AccessDiagnostic : Type

• Read (range : Memory.AllocRange) : AccessDiagnostic
• Write (range : Memory.AllocRange) : AccessDiagnostic
• Freed : AccessDiagnostic

def Miri.TreeBorrows.MachineMemoryHooks.instDecidableEqAccessDiagnostic.decEq (x✝ x✝¹ : AccessDiagnostic) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.MachineMemoryHooks.instDecidableEqAccessDiagnostic : DecidableEq AccessDiagnostic

Equations

• Miri.TreeBorrows.MachineMemoryHooks.instDecidableEqAccessDiagnostic = Miri.TreeBorrows.MachineMemoryHooks.instDecidableEqAccessDiagnostic.decEq

def Miri.TreeBorrows.MachineMemoryHooks.instReprAccessDiagnostic.repr : AccessDiagnostic → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.TreeBorrows.MachineMemoryHooks.instReprAccessDiagnostic : Repr AccessDiagnostic

Equations

• Miri.TreeBorrows.MachineMemoryHooks.instReprAccessDiagnostic = { reprPrec := Miri.TreeBorrows.MachineMemoryHooks.instReprAccessDiagnostic.repr }

structure Miri.TreeBorrows.MachineMemoryHooks.SyncObjectMap (Obj : Type) : Type

A finite ordered representation of Miri's per-allocation BTreeMap<Size, Box<dyn SyncObj>>. Insertion keeps keys unique and ascending, so the access walks below have the source map's iteration order.

• entries : Array (ABI.Size × Obj)

def Miri.TreeBorrows.MachineMemoryHooks.SyncObjectMap.empty {Obj : Type} : SyncObjectMap Obj

Equations

• Miri.TreeBorrows.MachineMemoryHooks.SyncObjectMap.empty = { }

def Miri.TreeBorrows.MachineMemoryHooks.SyncObjectMap.insert {Obj : Type} (map : SyncObjectMap Obj) (offset : ABI.Size) (object : Obj) : SyncObjectMap Obj

Equations

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

def Miri.TreeBorrows.MachineMemoryHooks.SyncObjectMap.remove {Obj : Type} (map : SyncObjectMap Obj) (offset : ABI.Size) : SyncObjectMap Obj

Equations

• map.remove offset = { entries := Array.filter (fun (entry : Miri.ABI.Size × Obj) => entry.fst.bytes != offset.bytes) map.entries }

def Miri.TreeBorrows.MachineMemoryHooks.SyncObjectMap.inRange {Obj : Type} (map : SyncObjectMap Obj) (range : Memory.AllocRange) : Except Memory.MemoryError (Array (ABI.Size × Obj))

Equations

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

structure Miri.TreeBorrows.MachineMemoryHooks.SyncObjectStore (Obj : Type) : Type

Allocation-indexed sync metadata. Miri stores one offset map inside each AllocExtra; this outer index lets a single mem_copy_repeatedly context carry the source and destination allocation maps independently.

• allocations : Array (Memory.AllocId × SyncObjectMap Obj)

def Miri.TreeBorrows.MachineMemoryHooks.SyncObjectStore.empty {Obj : Type} : SyncObjectStore Obj

Equations

• Miri.TreeBorrows.MachineMemoryHooks.SyncObjectStore.empty = { }

def Miri.TreeBorrows.MachineMemoryHooks.SyncObjectStore.get {Obj : Type} (store : SyncObjectStore Obj) (allocId : Memory.AllocId) : SyncObjectMap Obj

Equations

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

def Miri.TreeBorrows.MachineMemoryHooks.SyncObjectStore.set {Obj : Type} (store : SyncObjectStore Obj) (allocId : Memory.AllocId) (objects : SyncObjectMap Obj) : SyncObjectStore Obj

Equations

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

def Miri.TreeBorrows.MachineMemoryHooks.SyncObjectStore.remove {Obj : Type} (store : SyncObjectStore Obj) (allocId : Memory.AllocId) : SyncObjectStore Obj

Equations

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

structure Miri.TreeBorrows.MachineMemoryHooks.Context (State Obj : Type) : Type

The AllocExtra-local sync map plus the global state threaded through Miri's machine callbacks. The caller supplies the sync map for the allocation currently being accessed and stores the returned map with that allocation.

• state : State
• syncObjects : SyncObjectStore Obj
• trackAllocAccesses : Bool
• trackedAllocIds : Array Memory.AllocId

structure Miri.TreeBorrows.MachineMemoryHooks.Hooks (State Obj MachineKind : Type) : Type

Hooks corresponding to the portions of machine.rs and concurrency::sync::SyncObj outside the Tree Borrows subtree. Data-race hooks must dispatch the configured Miri handler (None or vector clocks), including its per-allocation-handler invariant and weak-memory write effect.

• protectedTags : ProtectedTags
• emitDiagnostic : State → Memory.AllocId → AccessDiagnostic → State
• dataRaceRead : State → Memory.Pointer (Option Memory.Provenance) → Memory.AllocId → Memory.AllocRange → Memory.MachineHookResult State Unit
• dataRaceWrite : State → Memory.Pointer (Option Memory.Provenance) → Memory.AllocId → Memory.AllocRange → Memory.MachineHookResult State Unit
• dataRaceDeallocate : State → Memory.Pointer (Option Memory.Provenance) → Memory.AllocId → ABI.Size → Memory.MemoryKind MachineKind → Memory.MachineHookResult State Unit
• syncOnAccess : State → Obj → SyncAccessKind → Memory.MachineHookResult State Unit
• deleteOnWrite : Obj → Bool
• recordDeallocatedSpan : State → Memory.AllocId → State
• freeAllocId : State → Memory.AllocId → ABI.Size → ABI.Align → Memory.MemoryKind MachineKind → State

structure Miri.TreeBorrows.MachineMemoryHooks.AccessResult (State Obj MachineKind : Type) : Type

• memory : Memory.MemoryState Memory.Provenance BorrowTree MachineKind
• context : Context State Obj
• outcome : Except String Unit

def Miri.TreeBorrows.MachineMemoryHooks.beforeMemoryRead {MachineKind State Obj : Type} [DecidableEq MachineKind] (memory : Memory.MemoryState Memory.Provenance BorrowTree MachineKind) (context : Context State Obj) (hooks : Hooks State Obj MachineKind) (allocation : Memory.Allocation Memory.Provenance BorrowTree) (pointer : Memory.Pointer (Option Memory.Provenance)) (allocId : Memory.AllocId) (provenance : Memory.ProvenanceExtra) (range : Memory.AllocRange) : AccessResult State Obj MachineKind

Pinned MiriMachine::before_memory_read after optional diagnostic. The data-race hook runs first. The actual live allocation extra is then updated by the Tree Borrows access, and a Tree error prevents all sync-object callbacks.

Equations

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

def Miri.TreeBorrows.MachineMemoryHooks.beforeMemoryWrite {MachineKind State Obj : Type} [DecidableEq MachineKind] (memory : Memory.MemoryState Memory.Provenance BorrowTree MachineKind) (context : Context State Obj) (hooks : Hooks State Obj MachineKind) (allocation : Memory.Allocation Memory.Provenance BorrowTree) (pointer : Memory.Pointer (Option Memory.Provenance)) (allocId : Memory.AllocId) (provenance : Memory.ProvenanceExtra) (range : Memory.AllocRange) : AccessResult State Obj MachineKind

Pinned MiriMachine::before_memory_write after optional diagnostic. Sync objects are deleted only after every overlapping object's write check succeeds, matching the source's collect-then-remove loop.

Equations

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

structure Miri.TreeBorrows.MachineMemoryHooks.DeallocationResult (State Obj MachineKind : Type) : Type

• allocation : Memory.Allocation Memory.Provenance BorrowTree
• context : Context State Obj
• outcome : Except String Unit

def Miri.TreeBorrows.MachineMemoryHooks.beforeMemoryDeallocation {State Obj MachineKind : Type} (context : Context State Obj) (hooks : Hooks State Obj MachineKind) (allocation : Memory.Allocation Memory.Provenance BorrowTree) (pointer : Memory.Pointer (Option Memory.Provenance)) (allocId : Memory.AllocId) (provenance : Memory.ProvenanceExtra) (size : ABI.Size) (align : ABI.Align) (kind : Memory.MemoryKind MachineKind) : DeallocationResult State Obj MachineKind

Pinned MiriMachine::before_memory_deallocation. MemoryLifecycle.deallocatePtr has already removed the allocation from its live map when it invokes this callback. The tree result is retained in allocation for callers that need to inspect a failed hook; the lifecycle caller still preserves its source removal on failure.

Equations

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

def Miri.TreeBorrows.MachineMemoryHooks.asMemoryCopyHooks {MachineKind State Obj : Type} [DecidableEq MachineKind] (machineHooks : Hooks State Obj MachineKind) (pointerAccess : Memory.MemoryState Memory.Provenance BorrowTree MachineKind → Context State Obj → Memory.Pointer (Option Memory.Provenance) → ABI.Size → Memory.MemoryStateHookResult Memory.Provenance BorrowTree MachineKind (Context State Obj) (Option (Memory.AllocId × ABI.Size × Memory.ProvenanceExtra))) (tryGetAllocId : Memory.MemoryState Memory.Provenance BorrowTree MachineKind → Context State Obj → Memory.Pointer (Option Memory.Provenance) → UInt64 → Option Memory.AllocId) (beforeAllocationAccess : Memory.MemoryState Memory.Provenance BorrowTree MachineKind → Context State Obj → Memory.AllocId → Memory.MemoryStateHookResult Memory.Provenance BorrowTree MachineKind (Context State Obj) Unit) : Memory.MemoryCopyHooks Memory.Provenance BorrowTree MachineKind (Context State Obj) Memory.ProvenanceExtra

Adapt the source-ordered Tree Borrows hooks to the existing mem_copy read/write callback boundary. Pointer resolution, before_alloc_access, and the actual Miri data-race handler remain explicit caller inputs.

Equations

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

def Miri.TreeBorrows.MachineMemoryHooks.asDeallocationHook {State Obj MachineKind : Type} (machineHooks : Hooks State Obj MachineKind) : Memory.MemoryState Memory.Provenance BorrowTree MachineKind → Context State Obj → Memory.Allocation Memory.Provenance BorrowTree → Memory.Pointer (Option Memory.Provenance) → Memory.AllocId → Memory.ProvenanceExtra → ABI.Size → ABI.Align → Memory.MemoryKind MachineKind → Memory.MemoryStateHookResult Memory.Provenance BorrowTree MachineKind (Context State Obj) Unit

Adapt the ordered tree/race/sync/free sequence to MemoryLifecycleHooks.beforeDeallocation. The surrounding lifecycle owns pointer resolution, live-map removal, and dead-allocation caching; the adapter returns the explicit memory successor unchanged.

Equations

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