Documentation

Miri.Memory.AllocationAccess

Bounds-checked allocation access from pinned interpreter memory.rs. Actual global materialization precedes bounds checking. Machine access hooks remain explicit, and retain updated allocation extras even when they fail. These helpers do not check alignment or perform byte loads/stores.

source
structure Miri.Memory.AllocationExtraHookResult (HookState Extra : Type) :
Type
Instances For
    source
    structure Miri.Memory.AllocationAccessHooks (Prov Extra MachineKind HookState ProvExtra : Type) :
    Type
    Instances For
      source
      structure Miri.Memory.AllocationAccessRef (Prov Extra : Type) :
      Type
      Instances For
        source
        inductive Miri.Memory.PtrAllocationError :
        Type
        Instances For
          source
          @[instance_reducible]
          instance Miri.Memory.instDecidableEqPtrAllocationError :
          DecidableEq PtrAllocationError
          Equations
          source
          def Miri.Memory.instDecidableEqPtrAllocationError.decEq (x✝ x✝¹ : PtrAllocationError) :
          Decidable (x✝ = x✝¹)
          Equations
          Instances For
            source
            def Miri.Memory.instReprPtrAllocationError.repr :
            PtrAllocationError → Nat → Std.Format
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[instance_reducible]
              instance Miri.Memory.instReprPtrAllocationError :
              Repr PtrAllocationError
              Equations
              source
              structure Miri.Memory.PtrAllocationResult (Prov Extra MachineKind HookState α : Type) :
              Type
              Instances For
                source
                def Miri.Memory.AllocationAccess.getPtrAlloc {Prov Extra MachineKind HookState ProvExtra : Type} [DecidableEq MachineKind] (memory : MemoryState Prov Extra MachineKind) (hooksState : HookState) (target : PointerArithmetic) (ptr : Pointer (Option Prov)) (size : ABI.Size) (ghostMode : Bool) (globalKind : Option MachineKind) (globalHooks : GlobalAllocationHooks Prov Extra MachineKind HookState) (accessHooks : AllocationAccessHooks Prov Extra MachineKind HookState ProvExtra) :
                PtrAllocationResult Prov Extra MachineKind HookState (Option (AllocationAccessRef Prov Extra))
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  def Miri.Memory.AllocationAccess.getPtrAllocMut {Prov Extra MachineKind HookState ProvExtra : Type} [DecidableEq MachineKind] (memory : MemoryState Prov Extra MachineKind) (hooksState : HookState) (target : PointerArithmetic) (ptr : Pointer (Option Prov)) (size : ABI.Size) (ghostMode : Bool) (globalKind : Option MachineKind) (globalHooks : GlobalAllocationHooks Prov Extra MachineKind HookState) (accessHooks : AllocationAccessHooks Prov Extra MachineKind HookState ProvExtra) :
                  PtrAllocationResult Prov Extra MachineKind HookState (Option (AllocationAccessRef Prov Extra))
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    theorem Miri.Memory.AllocationAccess.live_mut_of_edges {P E K H X : Type} [DecidableEq K] (memory : MemoryState P E K) (hooks : H) (target : PointerArithmetic) (ptr : Pointer (Option P)) (size : ABI.Size) (kind : Option K) (global : GlobalAllocationHooks P E K H) (access : AllocationAccessHooks P E K H X) (id : AllocId) (entry : LocalAllocation P E K) (provenance : X) (amount : Int) (signed : sizeAsI64 size = Except.ok amount) (nonzero : amount ≠ 0) (resolve : access.resolvePointer memory hooks ptr amount = { state := hooks, outcome := Except.ok (Except.ok { allocId := id, offset := ABI.Size.ZERO, extra := provenance }) }) (live : Array.find? (fun (row : AllocId × LocalAllocation P E K) => row.fst == id) memory.live = some (id, entry)) (mutable : entry.allocation.mutability = Mutability.Mut) (synchronize : global.synchronizeMemory memory hooks = hooks) (bounds : checkedBounds target id entry.allocation.byteSize ABI.Size.ZERO amount CheckInAllocMsg.memoryAccess = Except.ok ()) (before : access.beforeAllocationAccess hooks id = { state := hooks, outcome := Except.ok () }) (write : access.beforeMemoryWrite hooks entry.allocation.extra ptr id provenance (allocRange ABI.Size.ZERO size) = { state := hooks, extra := entry.allocation.extra, outcome := Except.ok () }) (last : (Array.filter (fun (row : AllocId × LocalAllocation P E K) => row.fst != id) memory.live).push (id, entry) = memory.live) :
                    getPtrAllocMut memory hooks target ptr size false kind global access = { memory := memory, hooks := hooks, touched := some { allocId := id, range := allocRange ABI.Size.ZERO size, allocation := entry.allocation }, outcome := Except.ok (some { allocId := id, range := allocRange ABI.Size.ZERO size, allocation := entry.allocation }) }

                    Internal edges compose the production positive mutable-access path.