Direct stateful Tree Borrows construction. Only source configuration, attribute queries and diagnostic emission enter as leaves; projection, pointer resolution, protection and memory writes are the canonical machine operations. Sources: tree_borrows/mod.rs; helpers.rs UnsafeCellVisitor; machine.rs retag.

structure Miri.Input.EvalRetagMachine.Leaves (K U : Type) : Type

• implicitWrites : Interpreter.MachineHooks.M K (Interpreter.ValidityMachine.UserState U) Bool
• rustcNoWritable : MIR.DefId → Interpreter.MachineHooks.M K (Interpreter.ValidityMachine.UserState U) Bool
• preciseInteriorMut : Interpreter.MachineHooks.M K (Interpreter.ValidityMachine.UserState U) Bool
• logCreation : Interpreter.MPlaceTy Memory.Provenance → ABI.Size → TreeBorrows.RetagPolicy.NewPermission → Memory.BorTag → Option TreeBorrows.RetagPipeline.ResolvedLocation → Interpreter.MachineHooks.M K (Interpreter.ValidityMachine.UserState U) Unit

def Miri.Input.EvalRetagMachine.hooks {K U C F A : Type} [DecidableEq K] (prepared : CompilerFactAdapters.Prepared) (runtime : CompilerRuntimeQueries.Prepared) (leaves : Leaves K U) (access : Interpreter.ValidityMachine.Access K U) (projection : Interpreter.PlaceProjectionHooks Memory.Provenance (Interpreter.ValidityMachine.State K U) C Interpreter.MachineHooks.FrameExtra) (vtable : Interpreter.VTableHooks Memory.Provenance (Interpreter.ValidityMachine.State K U) C F A) (pointers : Interpreter.PointerMachine.Hooks K (Interpreter.ValidityMachine.Control U)) (choice : C) : Interpreter.TypedRetag.Hooks K (Interpreter.ValidityMachine.UserState U)

Equations

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