Documentation

Miri.ABI.Layout

Source-shaped rustc_abi layout records and checked observation methods. No type layout computation or type-system metadata is inferred here.

inductive Miri.ABI.LayoutError :

fieldOutOfBounds (index count : Nat) : LayoutError
invalidUnionCount : LayoutError
invalidMemoryOrder : LayoutError
size (error : SizeError) : LayoutError
expectedArbitraryVariant : LayoutError
missingField (index : Nat) : LayoutError
missingVariant (index : Nat) : LayoutError
missingPointee : LayoutError

Instances For

@[instance_reducible]

instance Miri.ABI.instDecidableEqLayoutError :

DecidableEq LayoutError

Equations

Miri.ABI.instDecidableEqLayoutError = Miri.ABI.instDecidableEqLayoutError.decEq

def Miri.ABI.instDecidableEqLayoutError.decEq (x✝ x✝¹ : LayoutError) :

Decidable (x✝ = x✝¹)

Equations

Instances For

def Miri.ABI.instReprLayoutError.repr :

LayoutError → Nat → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Miri.ABI.instReprLayoutError :

Repr LayoutError

Equations

Miri.ABI.instReprLayoutError = { reprPrec := Miri.ABI.instReprLayoutError.repr }

inductive Miri.ABI.FieldsShape :

Primitive : FieldsShape
Union (count : Nat) : FieldsShape
Array (stride : Size) (count : UInt64) : FieldsShape
Arbitrary (offsets : _root_.Array Size) (inMemoryOrder : _root_.Array Nat) : FieldsShape

Instances For

@[instance_reducible]

instance Miri.ABI.instDecidableEqFieldsShape :

DecidableEq FieldsShape

Equations

Miri.ABI.instDecidableEqFieldsShape = Miri.ABI.instDecidableEqFieldsShape.decEq

def Miri.ABI.instDecidableEqFieldsShape.decEq (x✝ x✝¹ : FieldsShape) :

Decidable (x✝ = x✝¹)

Equations

One or more equations did not get rendered due to their size.
Miri.ABI.instDecidableEqFieldsShape.decEq Miri.ABI.FieldsShape.Primitive Miri.ABI.FieldsShape.Primitive = isTrue ⋯
Miri.ABI.instDecidableEqFieldsShape.decEq Miri.ABI.FieldsShape.Primitive (Miri.ABI.FieldsShape.Union count) = isFalse ⋯
Miri.ABI.instDecidableEqFieldsShape.decEq Miri.ABI.FieldsShape.Primitive (Miri.ABI.FieldsShape.Array stride count) = isFalse ⋯
Miri.ABI.instDecidableEqFieldsShape.decEq Miri.ABI.FieldsShape.Primitive (Miri.ABI.FieldsShape.Arbitrary offsets inMemoryOrder) = isFalse ⋯
Miri.ABI.instDecidableEqFieldsShape.decEq (Miri.ABI.FieldsShape.Union count) Miri.ABI.FieldsShape.Primitive = isFalse ⋯
Miri.ABI.instDecidableEqFieldsShape.decEq (Miri.ABI.FieldsShape.Union a) (Miri.ABI.FieldsShape.Union b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
Miri.ABI.instDecidableEqFieldsShape.decEq (Miri.ABI.FieldsShape.Union count) (Miri.ABI.FieldsShape.Array stride count_1) = isFalse ⋯
Miri.ABI.instDecidableEqFieldsShape.decEq (Miri.ABI.FieldsShape.Union count) (Miri.ABI.FieldsShape.Arbitrary offsets inMemoryOrder) = isFalse ⋯
Miri.ABI.instDecidableEqFieldsShape.decEq (Miri.ABI.FieldsShape.Array stride count) Miri.ABI.FieldsShape.Primitive = isFalse ⋯
Miri.ABI.instDecidableEqFieldsShape.decEq (Miri.ABI.FieldsShape.Array stride count) (Miri.ABI.FieldsShape.Union count_1) = isFalse ⋯
Miri.ABI.instDecidableEqFieldsShape.decEq (Miri.ABI.FieldsShape.Array stride count) (Miri.ABI.FieldsShape.Arbitrary offsets inMemoryOrder) = isFalse ⋯
Miri.ABI.instDecidableEqFieldsShape.decEq (Miri.ABI.FieldsShape.Arbitrary offsets inMemoryOrder) Miri.ABI.FieldsShape.Primitive = isFalse ⋯
Miri.ABI.instDecidableEqFieldsShape.decEq (Miri.ABI.FieldsShape.Arbitrary offsets inMemoryOrder) (Miri.ABI.FieldsShape.Union count) = isFalse ⋯
Miri.ABI.instDecidableEqFieldsShape.decEq (Miri.ABI.FieldsShape.Arbitrary offsets inMemoryOrder) (Miri.ABI.FieldsShape.Array stride count) = isFalse ⋯

Instances For

@[instance_reducible]

instance Miri.ABI.instReprFieldsShape :

Repr FieldsShape

Equations

Miri.ABI.instReprFieldsShape = { reprPrec := Miri.ABI.instReprFieldsShape.repr }

def Miri.ABI.instReprFieldsShape.repr :

FieldsShape → Nat → Std.Format

Equations

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

Instances For

def Miri.ABI.FieldsShape.count :

FieldsShape → Nat

Equations

Miri.ABI.FieldsShape.Primitive.count = 0
(Miri.ABI.FieldsShape.Union a).count = a
(Miri.ABI.FieldsShape.Array a a_1).count = a_1.toNat
(Miri.ABI.FieldsShape.Arbitrary a a_1).count = a.size

Instances For

def Miri.ABI.FieldsShape.offset (fields : FieldsShape) (index : Nat) :

Except LayoutError Size

Equations

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

Instances For

def Miri.ABI.FieldsShape.validate :

FieldsShape → Except LayoutError Unit

Equations

One or more equations did not get rendered due to their size.
(Miri.ABI.FieldsShape.Union 0).validate = Except.error Miri.ABI.LayoutError.invalidUnionCount
x✝.validate = Except.ok ()

Instances For

def Miri.ABI.FieldsShape.indexByIncreasingOffset (fields : FieldsShape) :

Except LayoutError (_root_.Array Nat)

Primitive deliberately yields the source's single pseudo-field.

Equations

Miri.ABI.FieldsShape.Primitive.indexByIncreasingOffset = do Miri.ABI.FieldsShape.Primitive.validate pure #[0]
(Miri.ABI.FieldsShape.Arbitrary offsets order).indexByIncreasingOffset = do (Miri.ABI.FieldsShape.Arbitrary offsets order).validate pure order
fields.indexByIncreasingOffset = do fields.validate pure (List.range fields.count).toArray

Instances For

inductive Miri.ABI.TagEncoding :

Direct : TagEncoding
Niche (untaggedVariant nicheVariantsStart nicheVariantsEnd : Nat) (nicheStart : U128) : TagEncoding

Instances For

@[instance_reducible]

instance Miri.ABI.instDecidableEqTagEncoding :

DecidableEq TagEncoding

Equations

Miri.ABI.instDecidableEqTagEncoding = Miri.ABI.instDecidableEqTagEncoding.decEq

def Miri.ABI.instDecidableEqTagEncoding.decEq (x✝ x✝¹ : TagEncoding) :

Decidable (x✝ = x✝¹)

Equations

One or more equations did not get rendered due to their size.
Miri.ABI.instDecidableEqTagEncoding.decEq Miri.ABI.TagEncoding.Direct Miri.ABI.TagEncoding.Direct = isTrue ⋯
Miri.ABI.instDecidableEqTagEncoding.decEq Miri.ABI.TagEncoding.Direct (Miri.ABI.TagEncoding.Niche untaggedVariant nicheVariantsStart nicheVariantsEnd nicheStart) = isFalse ⋯
Miri.ABI.instDecidableEqTagEncoding.decEq (Miri.ABI.TagEncoding.Niche untaggedVariant nicheVariantsStart nicheVariantsEnd nicheStart) Miri.ABI.TagEncoding.Direct = isFalse ⋯

Instances For

def Miri.ABI.instReprTagEncoding.repr :

TagEncoding → Nat → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Miri.ABI.instReprTagEncoding :

Repr TagEncoding

Equations

Miri.ABI.instReprTagEncoding = { reprPrec := Miri.ABI.instReprTagEncoding.repr }

structure Miri.ABI.Niche :

offset : Size
value : Primitive
validRange : WrappingRange

Instances For

@[instance_reducible]

instance Miri.ABI.instDecidableEqNiche :

DecidableEq Niche

Equations

Miri.ABI.instDecidableEqNiche = Miri.ABI.instDecidableEqNiche.decEq

def Miri.ABI.instDecidableEqNiche.decEq (x✝ x✝¹ : Niche) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

def Miri.ABI.instReprNiche.repr :

Niche → Nat → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Miri.ABI.instReprNiche :

Equations

Miri.ABI.instReprNiche = { reprPrec := Miri.ABI.instReprNiche.repr }

structure Miri.ABI.VariantLayout :

size : Size
backendRepr : BackendRepr
fieldOffsets : Array Size
fieldsInMemoryOrder : Array Nat
largestNiche : Option Niche
uninhabited : Bool

Instances For

@[instance_reducible]

instance Miri.ABI.instDecidableEqVariantLayout :

DecidableEq VariantLayout

Equations

Miri.ABI.instDecidableEqVariantLayout = Miri.ABI.instDecidableEqVariantLayout.decEq

def Miri.ABI.instDecidableEqVariantLayout.decEq (x✝ x✝¹ : VariantLayout) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

@[instance_reducible]

instance Miri.ABI.instReprVariantLayout :

Repr VariantLayout

Equations

Miri.ABI.instReprVariantLayout = { reprPrec := Miri.ABI.instReprVariantLayout.repr }

def Miri.ABI.instReprVariantLayout.repr :

VariantLayout → Nat → Std.Format

Equations

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

Instances For

def Miri.ABI.VariantLayout.isUninhabited (variant : VariantLayout) :

Equations

variant.isUninhabited = variant.uninhabited

Instances For

def Miri.ABI.VariantLayout.hasFields (variant : VariantLayout) :

Equations

variant.hasFields = !variant.fieldOffsets.isEmpty

Instances For

inductive Miri.ABI.Variants :

Empty : Variants
Single (index : Nat) : Variants
Multiple (tag : Scalar) (tagEncoding : TagEncoding) (tagField : Nat) (variants : Array VariantLayout) : Variants

Instances For

def Miri.ABI.instDecidableEqVariants.decEq (x✝ x✝¹ : Variants) :

Decidable (x✝ = x✝¹)

Equations

One or more equations did not get rendered due to their size.
Miri.ABI.instDecidableEqVariants.decEq Miri.ABI.Variants.Empty Miri.ABI.Variants.Empty = isTrue ⋯
Miri.ABI.instDecidableEqVariants.decEq Miri.ABI.Variants.Empty (Miri.ABI.Variants.Single index) = isFalse ⋯
Miri.ABI.instDecidableEqVariants.decEq Miri.ABI.Variants.Empty (Miri.ABI.Variants.Multiple tag tagEncoding tagField variants) = isFalse ⋯
Miri.ABI.instDecidableEqVariants.decEq (Miri.ABI.Variants.Single index) Miri.ABI.Variants.Empty = isFalse ⋯
Miri.ABI.instDecidableEqVariants.decEq (Miri.ABI.Variants.Single a) (Miri.ABI.Variants.Single b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
Miri.ABI.instDecidableEqVariants.decEq (Miri.ABI.Variants.Single index) (Miri.ABI.Variants.Multiple tag tagEncoding tagField variants) = isFalse ⋯
Miri.ABI.instDecidableEqVariants.decEq (Miri.ABI.Variants.Multiple tag tagEncoding tagField variants) Miri.ABI.Variants.Empty = isFalse ⋯
Miri.ABI.instDecidableEqVariants.decEq (Miri.ABI.Variants.Multiple tag tagEncoding tagField variants) (Miri.ABI.Variants.Single index) = isFalse ⋯

Instances For

@[instance_reducible]

instance Miri.ABI.instDecidableEqVariants :

DecidableEq Variants

Equations

Miri.ABI.instDecidableEqVariants = Miri.ABI.instDecidableEqVariants.decEq

def Miri.ABI.instReprVariants.repr :

Variants → Nat → Std.Format

Equations

One or more equations did not get rendered due to their size.
Miri.ABI.instReprVariants.repr Miri.ABI.Variants.Empty prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.ABI.Variants.Empty")).group prec✝

Instances For

@[instance_reducible]

instance Miri.ABI.instReprVariants :

Equations

Miri.ABI.instReprVariants = { reprPrec := Miri.ABI.instReprVariants.repr }

structure Miri.ABI.LayoutData :

fields : FieldsShape
variants : Variants
backendRepr : BackendRepr
largestNiche : Option Niche
uninhabited : Bool
align : AbiAlign
size : Size
maxReprAlign : Option Align
unadjustedAbiAlign : Align
reprC : Bool
randomizationSeed : UInt64

Instances For

def Miri.ABI.instDecidableEqLayoutData.decEq (x✝ x✝¹ : LayoutData) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

@[instance_reducible]

instance Miri.ABI.instDecidableEqLayoutData :

DecidableEq LayoutData

Equations

Miri.ABI.instDecidableEqLayoutData = Miri.ABI.instDecidableEqLayoutData.decEq

def Miri.ABI.instReprLayoutData.repr :

LayoutData → Nat → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Miri.ABI.instReprLayoutData :

Repr LayoutData

Equations

Miri.ABI.instReprLayoutData = { reprPrec := Miri.ABI.instReprLayoutData.repr }

@[reducible, inline]

abbrev Miri.ABI.Layout :

Equations

Miri.ABI.Layout = Miri.ABI.LayoutData

Instances For

def Miri.ABI.LayoutData.isAggregate (layout : LayoutData) :

Equations

layout.isAggregate = !layout.backendRepr.isScalarOrSimd

Instances For

def Miri.ABI.LayoutData.isUninhabited (layout : LayoutData) :

Equations

layout.isUninhabited = layout.uninhabited

Instances For

def Miri.ABI.LayoutData.isVariantUninhabited (layout : LayoutData) (index : Nat) :

Equations

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

Instances For

def Miri.ABI.LayoutData.isReprC (layout : LayoutData) :

Equations

layout.isReprC = layout.reprC

Instances For

def Miri.ABI.LayoutData.isUnsized (layout : LayoutData) :

Equations

layout.isUnsized = layout.backendRepr.isUnsized

Instances For

def Miri.ABI.LayoutData.isSized (layout : LayoutData) :

Equations

layout.isSized = layout.backendRepr.isSized

Instances For

def Miri.ABI.LayoutData.is1zst (layout : LayoutData) :

Equations

layout.is1zst = (layout.isSized && layout.size.bytes == 0 && layout.align.abi.pow2 == 0)

Instances For

def Miri.ABI.LayoutData.isScalableVector (layout : LayoutData) :

Equations

layout.isScalableVector = match layout.backendRepr with | Miri.ABI.BackendRepr.SimdScalableVector => true | x => false

Instances For

def Miri.ABI.LayoutData.scalableVectorElementCount (layout : LayoutData) :

Option BackendLaneCount

Equations

layout.scalableVectorElementCount = match layout.backendRepr with | Miri.ABI.BackendRepr.SimdScalableVector => some count | x => none

Instances For

def Miri.ABI.LayoutData.isZst (layout : LayoutData) :

Equations

layout.isZst = match layout.backendRepr with | Miri.ABI.BackendRepr.Memory => sized && layout.size.bytes == 0 | x => false

Instances For

def Miri.ABI.LayoutData.isSsaStandalone (layout : LayoutData) :

Equations

layout.isSsaStandalone = match layout.backendRepr with | Miri.ABI.BackendRepr.Memory => layout.isZst | x => true

Instances For

def Miri.ABI.LayoutData.eqAbi (layout other : LayoutData) :

Equations

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

Instances For

def Miri.ABI.VariantLayout.fromLayout (layout : LayoutData) :

Except LayoutError VariantLayout

Equations

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

Instances For

structure Miri.ABI.TyAndLayout (Ty : Type) :

ty : Ty
layout : LayoutData

Instances For

@[instance_reducible]

instance Miri.ABI.instDecidableEqTyAndLayout {Ty✝ : Type} [DecidableEq Ty✝] :

DecidableEq (TyAndLayout Ty✝)

Equations

Miri.ABI.instDecidableEqTyAndLayout = Miri.ABI.instDecidableEqTyAndLayout.decEq

def Miri.ABI.instDecidableEqTyAndLayout.decEq {Ty✝ : Type} [DecidableEq Ty✝] (x✝ x✝¹ : TyAndLayout Ty✝) :

Decidable (x✝ = x✝¹)

Equations

Miri.ABI.instDecidableEqTyAndLayout.decEq { ty := a, layout := a_1 } { ty := b, layout := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

Instances For

@[instance_reducible]

instance Miri.ABI.instReprTyAndLayout {Ty✝ : Type} [Repr Ty✝] :

Repr (TyAndLayout Ty✝)

Equations

Miri.ABI.instReprTyAndLayout = { reprPrec := Miri.ABI.instReprTyAndLayout.repr }

def Miri.ABI.instReprTyAndLayout.repr {Ty✝ : Type} [Repr Ty✝] :

TyAndLayout Ty✝ → Nat → Std.Format

Equations

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

Instances For

structure Miri.ABI.LayoutQueries (Ty : Type) :

Required compiler/type-system queries: callers supply evidence; this module never fabricates the type of a field, variant, or pointee.

field : TyAndLayout Ty → Nat → Except LayoutError (TyAndLayout Ty)
variant : TyAndLayout Ty → Nat → Except LayoutError (TyAndLayout Ty)
pointee : TyAndLayout Ty → Except LayoutError (TyAndLayout Ty)

Instances For