The allocation-bounds and pointer-alignment helpers from the pinned rustc_const_eval/src/interpret/memory.rs. Pointer-to-allocation resolution, live-allocation lookup, and machine policy are explicit inputs: this module does not infer liveness or dereference validity from an allocation ID alone.

inductive Miri.Memory.CheckInAllocMsg : Type

• memoryAccess : CheckInAllocMsg
• inboundsPointerArithmetic : CheckInAllocMsg
• dereferenceable (description : String) : CheckInAllocMsg
• other (description : String) : CheckInAllocMsg

def Miri.Memory.instDecidableEqCheckInAllocMsg.decEq (x✝ x✝¹ : CheckInAllocMsg) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Memory.instDecidableEqCheckInAllocMsg.decEq Miri.Memory.CheckInAllocMsg.memoryAccess Miri.Memory.CheckInAllocMsg.memoryAccess = isTrue ⋯
• Miri.Memory.instDecidableEqCheckInAllocMsg.decEq Miri.Memory.CheckInAllocMsg.memoryAccess (Miri.Memory.CheckInAllocMsg.dereferenceable description) = isFalse ⋯
• Miri.Memory.instDecidableEqCheckInAllocMsg.decEq Miri.Memory.CheckInAllocMsg.memoryAccess (Miri.Memory.CheckInAllocMsg.other description) = isFalse ⋯
• Miri.Memory.instDecidableEqCheckInAllocMsg.decEq Miri.Memory.CheckInAllocMsg.inboundsPointerArithmetic Miri.Memory.CheckInAllocMsg.inboundsPointerArithmetic = isTrue ⋯
• Miri.Memory.instDecidableEqCheckInAllocMsg.decEq Miri.Memory.CheckInAllocMsg.inboundsPointerArithmetic (Miri.Memory.CheckInAllocMsg.dereferenceable description) = isFalse ⋯
• Miri.Memory.instDecidableEqCheckInAllocMsg.decEq Miri.Memory.CheckInAllocMsg.inboundsPointerArithmetic (Miri.Memory.CheckInAllocMsg.other description) = isFalse ⋯
• Miri.Memory.instDecidableEqCheckInAllocMsg.decEq (Miri.Memory.CheckInAllocMsg.dereferenceable description) Miri.Memory.CheckInAllocMsg.memoryAccess = isFalse ⋯
• Miri.Memory.instDecidableEqCheckInAllocMsg.decEq (Miri.Memory.CheckInAllocMsg.dereferenceable description) Miri.Memory.CheckInAllocMsg.inboundsPointerArithmetic = isFalse ⋯
• Miri.Memory.instDecidableEqCheckInAllocMsg.decEq (Miri.Memory.CheckInAllocMsg.dereferenceable a) (Miri.Memory.CheckInAllocMsg.dereferenceable b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.Memory.instDecidableEqCheckInAllocMsg.decEq (Miri.Memory.CheckInAllocMsg.dereferenceable description) (Miri.Memory.CheckInAllocMsg.other description_1) = isFalse ⋯
• Miri.Memory.instDecidableEqCheckInAllocMsg.decEq (Miri.Memory.CheckInAllocMsg.other description) Miri.Memory.CheckInAllocMsg.memoryAccess = isFalse ⋯
• Miri.Memory.instDecidableEqCheckInAllocMsg.decEq (Miri.Memory.CheckInAllocMsg.other description) Miri.Memory.CheckInAllocMsg.inboundsPointerArithmetic = isFalse ⋯
• Miri.Memory.instDecidableEqCheckInAllocMsg.decEq (Miri.Memory.CheckInAllocMsg.other description) (Miri.Memory.CheckInAllocMsg.dereferenceable description_1) = isFalse ⋯
• Miri.Memory.instDecidableEqCheckInAllocMsg.decEq (Miri.Memory.CheckInAllocMsg.other a) (Miri.Memory.CheckInAllocMsg.other b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Memory.instDecidableEqCheckInAllocMsg : DecidableEq CheckInAllocMsg

Equations

• Miri.Memory.instDecidableEqCheckInAllocMsg = Miri.Memory.instDecidableEqCheckInAllocMsg.decEq

def Miri.Memory.instReprCheckInAllocMsg.repr : CheckInAllocMsg → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Memory.instReprCheckInAllocMsg : Repr CheckInAllocMsg

Equations

• Miri.Memory.instReprCheckInAllocMsg = { reprPrec := Miri.Memory.instReprCheckInAllocMsg.repr }

def Miri.Memory.CheckInAllocMsg.asString : CheckInAllocMsg → String

Equations

• Miri.Memory.CheckInAllocMsg.memoryAccess.asString = "memory access"
• Miri.Memory.CheckInAllocMsg.inboundsPointerArithmetic.asString = "inbounds pointer arithmetic"
• (Miri.Memory.CheckInAllocMsg.dereferenceable a).asString = toString "dereferenceable " ++ toString a
• (Miri.Memory.CheckInAllocMsg.other a).asString = a

inductive Miri.Memory.AllocationKind : Type

• liveData : AllocationKind
• function : AllocationKind
• vaList : AllocationKind
• vtable : AllocationKind
• typeId : AllocationKind
• dead : AllocationKind

@[instance_reducible]

instance Miri.Memory.instDecidableEqAllocationKind : DecidableEq AllocationKind

Equations

• Miri.Memory.instDecidableEqAllocationKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Miri.Memory.instReprAllocationKind.repr : AllocationKind → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Memory.instReprAllocationKind : Repr AllocationKind

Equations

• Miri.Memory.instReprAllocationKind = { reprPrec := Miri.Memory.instReprAllocationKind.repr }

structure Miri.Memory.AllocationInfo : Type

• size : ABI.Size
• align : ABI.Align
• kind : AllocationKind
• mutability : Mutability

@[instance_reducible]

instance Miri.Memory.instDecidableEqAllocationInfo : DecidableEq AllocationInfo

Equations

• Miri.Memory.instDecidableEqAllocationInfo = Miri.Memory.instDecidableEqAllocationInfo.decEq

def Miri.Memory.instDecidableEqAllocationInfo.decEq (x✝ x✝¹ : AllocationInfo) : Decidable (x✝ = x✝¹)

Equations

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

def Miri.Memory.instReprAllocationInfo.repr : AllocationInfo → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Memory.instReprAllocationInfo : Repr AllocationInfo

Equations

• Miri.Memory.instReprAllocationInfo = { reprPrec := Miri.Memory.instReprAllocationInfo.repr }

structure Miri.Memory.Misalignment : Type

• has : ABI.Align
• required : ABI.Align

@[instance_reducible]

instance Miri.Memory.instDecidableEqMisalignment : DecidableEq Misalignment

Equations

• Miri.Memory.instDecidableEqMisalignment = Miri.Memory.instDecidableEqMisalignment.decEq

def Miri.Memory.instDecidableEqMisalignment.decEq (x✝ x✝¹ : Misalignment) : Decidable (x✝ = x✝¹)

Equations

• Miri.Memory.instDecidableEqMisalignment.decEq { has := a, required := a_1 } { has := b, required := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Memory.instReprMisalignment : Repr Misalignment

Equations

• Miri.Memory.instReprMisalignment = { reprPrec := Miri.Memory.instReprMisalignment.repr }

def Miri.Memory.instReprMisalignment.repr : Misalignment → Nat → Std.Format

Equations

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

inductive Miri.Memory.AllocationLookupError : Type

• deadAllocation (id : AllocId) : AllocationLookupError
• unavailable (id : AllocId) : AllocationLookupError

@[instance_reducible]

instance Miri.Memory.instDecidableEqAllocationLookupError : DecidableEq AllocationLookupError

Equations

• Miri.Memory.instDecidableEqAllocationLookupError = Miri.Memory.instDecidableEqAllocationLookupError.decEq

def Miri.Memory.instDecidableEqAllocationLookupError.decEq (x✝ x✝¹ : AllocationLookupError) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Memory.instDecidableEqAllocationLookupError.decEq (Miri.Memory.AllocationLookupError.deadAllocation id) (Miri.Memory.AllocationLookupError.unavailable id_1) = isFalse ⋯
• Miri.Memory.instDecidableEqAllocationLookupError.decEq (Miri.Memory.AllocationLookupError.unavailable id) (Miri.Memory.AllocationLookupError.deadAllocation id_1) = isFalse ⋯

@[instance_reducible]

instance Miri.Memory.instReprAllocationLookupError : Repr AllocationLookupError

Equations

• Miri.Memory.instReprAllocationLookupError = { reprPrec := Miri.Memory.instReprAllocationLookupError.repr }

def Miri.Memory.instReprAllocationLookupError.repr : AllocationLookupError → Nat → Std.Format

Equations

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

inductive Miri.Memory.AccessError : Type

• sizeDoesNotFitI64 (size : ABI.Size) : AccessError
• signedSizeOutsideI64 (size : Int) : AccessError
• danglingIntegerPointer (address : UInt64) (size : Int) (message : CheckInAllocMsg) : AccessError
• allocationLookup (reason : AllocationLookupError) : AccessError
• pointerArithmetic (reason : PointerError) : AccessError
• pointerOutOfBounds (id : AllocId) (allocationSize : ABI.Size) (offset inboundsSize : Int) (message : CheckInAllocMsg) : AccessError
• malformedAlignment (reason : ABI.AlignError) : AccessError
• alignmentCheckFailed (misalignment : Misalignment) : AccessError

def Miri.Memory.instDecidableEqAccessError.decEq (x✝ x✝¹ : AccessError) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Memory.instDecidableEqAccessError.decEq (Miri.Memory.AccessError.sizeDoesNotFitI64 a) (Miri.Memory.AccessError.sizeDoesNotFitI64 b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.Memory.instDecidableEqAccessError.decEq (Miri.Memory.AccessError.sizeDoesNotFitI64 size) (Miri.Memory.AccessError.signedSizeOutsideI64 size_1) = isFalse ⋯
• Miri.Memory.instDecidableEqAccessError.decEq (Miri.Memory.AccessError.sizeDoesNotFitI64 size) (Miri.Memory.AccessError.danglingIntegerPointer address size_1 message) = isFalse ⋯
• Miri.Memory.instDecidableEqAccessError.decEq (Miri.Memory.AccessError.sizeDoesNotFitI64 size) (Miri.Memory.AccessError.allocationLookup reason) = isFalse ⋯
• Miri.Memory.instDecidableEqAccessError.decEq (Miri.Memory.AccessError.sizeDoesNotFitI64 size) (Miri.Memory.AccessError.pointerArithmetic reason) = isFalse ⋯
• Miri.Memory.instDecidableEqAccessError.decEq (Miri.Memory.AccessError.sizeDoesNotFitI64 size) (Miri.Memory.AccessError.malformedAlignment reason) = isFalse ⋯
• Miri.Memory.instDecidableEqAccessError.decEq (Miri.Memory.AccessError.sizeDoesNotFitI64 size) (Miri.Memory.AccessError.alignmentCheckFailed misalignment) = isFalse ⋯
• Miri.Memory.instDecidableEqAccessError.decEq (Miri.Memory.AccessError.signedSizeOutsideI64 size) (Miri.Memory.AccessError.sizeDoesNotFitI64 size_1) = isFalse ⋯
• Miri.Memory.instDecidableEqAccessError.decEq (Miri.Memory.AccessError.signedSizeOutsideI64 a) (Miri.Memory.AccessError.signedSizeOutsideI64 b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.Memory.instDecidableEqAccessError.decEq (Miri.Memory.AccessError.signedSizeOutsideI64 size) (Miri.Memory.AccessError.danglingIntegerPointer address size_1 message) = isFalse ⋯
• Miri.Memory.instDecidableEqAccessError.decEq (Miri.Memory.AccessError.signedSizeOutsideI64 size) (Miri.Memory.AccessError.allocationLookup reason) = isFalse ⋯
• Miri.Memory.instDecidableEqAccessError.decEq (Miri.Memory.AccessError.signedSizeOutsideI64 size) (Miri.Memory.AccessError.pointerArithmetic reason) = isFalse ⋯
• Miri.Memory.instDecidableEqAccessError.decEq (Miri.Memory.AccessError.signedSizeOutsideI64 size) (Miri.Memory.AccessError.malformedAlignment reason) = isFalse ⋯
• Miri.Memory.instDecidableEqAccessError.decEq (Miri.Memory.AccessError.signedSizeOutsideI64 size) (Miri.Memory.AccessError.alignmentCheckFailed misalignment) = isFalse ⋯
• Miri.Memory.instDecidableEqAccessError.decEq (Miri.Memory.AccessError.danglingIntegerPointer address size message) (Miri.Memory.AccessError.sizeDoesNotFitI64 size_1) = isFalse ⋯
• Miri.Memory.instDecidableEqAccessError.decEq (Miri.Memory.AccessError.danglingIntegerPointer address size message) (Miri.Memory.AccessError.signedSizeOutsideI64 size_1) = isFalse ⋯
• Miri.Memory.instDecidableEqAccessError.decEq (Miri.Memory.AccessError.danglingIntegerPointer address size message) (Miri.Memory.AccessError.allocationLookup reason) = isFalse ⋯
• Miri.Memory.instDecidableEqAccessError.decEq (Miri.Memory.AccessError.danglingIntegerPointer address size message) (Miri.Memory.AccessError.pointerArithmetic reason) = isFalse ⋯
• Miri.Memory.instDecidableEqAccessError.decEq (Miri.Memory.AccessError.danglingIntegerPointer address size message) (Miri.Memory.AccessError.malformedAlignment reason) = isFalse ⋯
• Miri.Memory.instDecidableEqAccessError.decEq (Miri.Memory.AccessError.danglingIntegerPointer address size message) (Miri.Memory.AccessError.alignmentCheckFailed misalignment) = isFalse ⋯
• Miri.Memory.instDecidableEqAccessError.decEq (Miri.Memory.AccessError.allocationLookup reason) (Miri.Memory.AccessError.sizeDoesNotFitI64 size) = isFalse ⋯
• Miri.Memory.instDecidableEqAccessError.decEq (Miri.Memory.AccessError.allocationLookup reason) (Miri.Memory.AccessError.signedSizeOutsideI64 size) = isFalse ⋯
• Miri.Memory.instDecidableEqAccessError.decEq (Miri.Memory.AccessError.allocationLookup reason) (Miri.Memory.AccessError.danglingIntegerPointer address size message) = isFalse ⋯
• Miri.Memory.instDecidableEqAccessError.decEq (Miri.Memory.AccessError.allocationLookup a) (Miri.Memory.AccessError.allocationLookup b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.Memory.instDecidableEqAccessError.decEq (Miri.Memory.AccessError.allocationLookup reason) (Miri.Memory.AccessError.pointerArithmetic reason_1) = isFalse ⋯
• Miri.Memory.instDecidableEqAccessError.decEq (Miri.Memory.AccessError.allocationLookup reason) (Miri.Memory.AccessError.malformedAlignment reason_1) = isFalse ⋯
• Miri.Memory.instDecidableEqAccessError.decEq (Miri.Memory.AccessError.allocationLookup reason) (Miri.Memory.AccessError.alignmentCheckFailed misalignment) = isFalse ⋯
• Miri.Memory.instDecidableEqAccessError.decEq (Miri.Memory.AccessError.pointerArithmetic reason) (Miri.Memory.AccessError.sizeDoesNotFitI64 size) = isFalse ⋯
• Miri.Memory.instDecidableEqAccessError.decEq (Miri.Memory.AccessError.pointerArithmetic reason) (Miri.Memory.AccessError.signedSizeOutsideI64 size) = isFalse ⋯
• Miri.Memory.instDecidableEqAccessError.decEq (Miri.Memory.AccessError.pointerArithmetic reason) (Miri.Memory.AccessError.danglingIntegerPointer address size message) = isFalse ⋯
• Miri.Memory.instDecidableEqAccessError.decEq (Miri.Memory.AccessError.pointerArithmetic reason) (Miri.Memory.AccessError.allocationLookup reason_1) = isFalse ⋯
• Miri.Memory.instDecidableEqAccessError.decEq (Miri.Memory.AccessError.pointerArithmetic a) (Miri.Memory.AccessError.pointerArithmetic b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.Memory.instDecidableEqAccessError.decEq (Miri.Memory.AccessError.pointerArithmetic reason) (Miri.Memory.AccessError.malformedAlignment reason_1) = isFalse ⋯
• Miri.Memory.instDecidableEqAccessError.decEq (Miri.Memory.AccessError.pointerArithmetic reason) (Miri.Memory.AccessError.alignmentCheckFailed misalignment) = isFalse ⋯
• Miri.Memory.instDecidableEqAccessError.decEq (Miri.Memory.AccessError.malformedAlignment reason) (Miri.Memory.AccessError.sizeDoesNotFitI64 size) = isFalse ⋯
• Miri.Memory.instDecidableEqAccessError.decEq (Miri.Memory.AccessError.malformedAlignment reason) (Miri.Memory.AccessError.signedSizeOutsideI64 size) = isFalse ⋯
• Miri.Memory.instDecidableEqAccessError.decEq (Miri.Memory.AccessError.malformedAlignment reason) (Miri.Memory.AccessError.danglingIntegerPointer address size message) = isFalse ⋯
• Miri.Memory.instDecidableEqAccessError.decEq (Miri.Memory.AccessError.malformedAlignment reason) (Miri.Memory.AccessError.allocationLookup reason_1) = isFalse ⋯
• Miri.Memory.instDecidableEqAccessError.decEq (Miri.Memory.AccessError.malformedAlignment reason) (Miri.Memory.AccessError.pointerArithmetic reason_1) = isFalse ⋯
• Miri.Memory.instDecidableEqAccessError.decEq (Miri.Memory.AccessError.malformedAlignment a) (Miri.Memory.AccessError.malformedAlignment b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.Memory.instDecidableEqAccessError.decEq (Miri.Memory.AccessError.malformedAlignment reason) (Miri.Memory.AccessError.alignmentCheckFailed misalignment) = isFalse ⋯
• Miri.Memory.instDecidableEqAccessError.decEq (Miri.Memory.AccessError.alignmentCheckFailed misalignment) (Miri.Memory.AccessError.sizeDoesNotFitI64 size) = isFalse ⋯
• Miri.Memory.instDecidableEqAccessError.decEq (Miri.Memory.AccessError.alignmentCheckFailed misalignment) (Miri.Memory.AccessError.signedSizeOutsideI64 size) = isFalse ⋯
• Miri.Memory.instDecidableEqAccessError.decEq (Miri.Memory.AccessError.alignmentCheckFailed misalignment) (Miri.Memory.AccessError.danglingIntegerPointer address size message) = isFalse ⋯
• Miri.Memory.instDecidableEqAccessError.decEq (Miri.Memory.AccessError.alignmentCheckFailed misalignment) (Miri.Memory.AccessError.allocationLookup reason) = isFalse ⋯
• Miri.Memory.instDecidableEqAccessError.decEq (Miri.Memory.AccessError.alignmentCheckFailed misalignment) (Miri.Memory.AccessError.pointerArithmetic reason) = isFalse ⋯
• Miri.Memory.instDecidableEqAccessError.decEq (Miri.Memory.AccessError.alignmentCheckFailed misalignment) (Miri.Memory.AccessError.malformedAlignment reason) = isFalse ⋯
• Miri.Memory.instDecidableEqAccessError.decEq (Miri.Memory.AccessError.alignmentCheckFailed a) (Miri.Memory.AccessError.alignmentCheckFailed b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Memory.instDecidableEqAccessError : DecidableEq AccessError

Equations

• Miri.Memory.instDecidableEqAccessError = Miri.Memory.instDecidableEqAccessError.decEq

@[instance_reducible]

instance Miri.Memory.instReprAccessError : Repr AccessError

Equations

• Miri.Memory.instReprAccessError = { reprPrec := Miri.Memory.instReprAccessError.repr }

def Miri.Memory.instReprAccessError.repr : AccessError → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Memory.instToStringAccessError : ToString AccessError

Equations

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

structure Miri.Memory.ResolvedPointer (ProvExtra : Type) : Type

• allocId : AllocId
• offset : ABI.Size
• extra : ProvExtra

structure Miri.Memory.CheckedPointerAccess (ProvExtra : Type) : Type

• pointer : ResolvedPointer ProvExtra
• allocation : AllocationInfo

@[reducible, inline]

abbrev Miri.Memory.PointerResolver (Prov ProvExtra : Type) : Type

Equations

• Miri.Memory.PointerResolver Prov ProvExtra = (Miri.Memory.Pointer (Option Prov) → Int → Except UInt64 (Miri.Memory.ResolvedPointer ProvExtra))

@[reducible, inline]

abbrev Miri.Memory.LiveAllocationLookup : Type

Equations

• Miri.Memory.LiveAllocationLookup = (Miri.Memory.AllocId → Except Miri.Memory.AllocationLookupError Miri.Memory.AllocationInfo)

def Miri.Memory.sizeAsI64 (size : ABI.Size) : Except AccessError Int

Equations

• Miri.Memory.sizeAsI64 size = if size.bytes.toNat < 9223372036854775808 then Except.ok (Int.ofNat size.bytes.toNat) else Except.error (Miri.Memory.AccessError.sizeDoesNotFitI64 size)

def Miri.Memory.checkedBounds (target : PointerArithmetic) (id : AllocId) (allocationSize offset : ABI.Size) (signedSize : Int) (message : CheckInAllocMsg) : Except AccessError Unit

Equations

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

def Miri.Memory.checkAndDerefPtr {Prov ProvExtra : Type} (target : PointerArithmetic) (ptr : Pointer (Option Prov)) (signedSize : Int) (message : CheckInAllocMsg) (resolve : PointerResolver Prov ProvExtra) (lookup : LiveAllocationLookup) : Except AccessError (Option (CheckedPointerAccess ProvExtra))

The exact common check_and_deref_ptr order. Zero-sized accesses return none without pointer resolution or allocation lookup. Nonzero accesses first resolve provenance/address, then obtain live allocation metadata, then perform the checked signed interval test. The callbacks are the unported Machine and memory-map dependencies of the source method.

Equations

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

def Miri.Memory.getPtrAccess {Prov ProvExtra : Type} (target : PointerArithmetic) (ptr : Pointer (Option Prov)) (size : ABI.Size) (message : CheckInAllocMsg) (resolve : PointerResolver Prov ProvExtra) (lookup : LiveAllocationLookup) : Except AccessError (Option (ABI.Size × ABI.Align × AllocId × ABI.Size × ProvExtra))

Source get_ptr_access: converting Size to host i64 is checked, then the common dereference/bounds helper supplies the live allocation details.

Equations

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

def Miri.Memory.checkPtrAccess {Prov ProvExtra : Type} (target : PointerArithmetic) (ptr : Pointer (Option Prov)) (size : ABI.Size) (message : CheckInAllocMsg) (resolve : PointerResolver Prov ProvExtra) (lookup : LiveAllocationLookup) : Except AccessError Unit

Source check_ptr_access, retaining its configurable access diagnostic.

Equations

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

def Miri.Memory.checkPtrAccessSigned {Prov ProvExtra : Type} (target : PointerArithmetic) (ptr : Pointer (Option Prov)) (size : Int64) (message : CheckInAllocMsg) (resolve : PointerResolver Prov ProvExtra) (lookup : LiveAllocationLookup) : Except AccessError Unit

Source check_ptr_access_signed; a negative amount checks bytes to the left of the pointer, and zero retains the source's no-dereference behavior.

Equations

• Miri.Memory.checkPtrAccessSigned target ptr size message resolve lookup = do let _ ← Miri.Memory.checkAndDerefPtr target ptr size.toInt message resolve lookup pure ()

def Miri.Memory.isPtrMisaligned {Prov ProvExtra : Type} [PointerProvenance Prov] (ptr : Pointer (Option Prov)) (required : ABI.Align) (enforceAlignment : Bool) (resolve : PointerResolver Prov ProvExtra) (lookup : AllocId → Except AllocationLookupError AllocationInfo) (machineAlignmentCheck : AllocId → ABI.Align → AllocationKind → ABI.Size → ABI.Align → Option Misalignment) : Except AccessError (Option Misalignment)

Source is_ptr_misaligned, factored over explicit resolver, allocation metadata, enforcement policy, and machine-specific alignment hook. For address-based provenance, the pointer offset is its absolute address; for relative provenance, both allocation alignment and relative offset are checked. The hook must be supplied by the selected Machine, including its default None behavior when no machine-specific rule applies.

Equations

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

def Miri.Memory.checkPtrAlign {Prov ProvExtra : Type} [PointerProvenance Prov] (ptr : Pointer (Option Prov)) (required : ABI.Align) (enforceAlignment : Bool) (resolve : PointerResolver Prov ProvExtra) (lookup : AllocId → Except AllocationLookupError AllocationInfo) (machineAlignmentCheck : AllocId → ABI.Align → AllocationKind → ABI.Size → ABI.Align → Option Misalignment) : Except AccessError Unit

Source check_ptr_align error boundary. The source message is always CheckAlignMsg::AccessedPtr for this API.

Equations

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

theorem Miri.Memory.zero_sized_check_skips_resolution {Prov ProvExtra : Type} (ptr : Pointer (Option Prov)) (message : CheckInAllocMsg) (resolve : PointerResolver Prov ProvExtra) (lookup : LiveAllocationLookup) (target : PointerArithmetic) : checkAndDerefPtr target ptr 0 message resolve lookup = Except.ok none