Source-shaped rustc_target::callconv argument records and ABI equality. Equality deliberately ignores attributes that are not calling-convention bits, as the pinned source does. This does not classify a target's calling convention.

inductive Miri.ABI.ArgExtension : Type

• None : ArgExtension
• Zext : ArgExtension
• Sext : ArgExtension

@[instance_reducible]

instance Miri.ABI.instDecidableEqArgExtension : DecidableEq ArgExtension

Equations

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

def Miri.ABI.instReprArgExtension.repr : ArgExtension → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.ABI.instReprArgExtension : Repr ArgExtension

Equations

• Miri.ABI.instReprArgExtension = { reprPrec := Miri.ABI.instReprArgExtension.repr }

structure Miri.ABI.ArgAttributes : Type

• regular : UInt16
• argExt : ArgExtension
• pointeeSize : Size
• pointeeAlign : Option Align

def Miri.ABI.instDecidableEqArgAttributes.decEq (x✝ x✝¹ : ArgAttributes) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.ABI.instDecidableEqArgAttributes : DecidableEq ArgAttributes

Equations

• Miri.ABI.instDecidableEqArgAttributes = Miri.ABI.instDecidableEqArgAttributes.decEq

def Miri.ABI.instReprArgAttributes.repr : ArgAttributes → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.ABI.instReprArgAttributes : Repr ArgAttributes

Equations

• Miri.ABI.instReprArgAttributes = { reprPrec := Miri.ABI.instReprArgAttributes.repr }

def Miri.ABI.ArgAttributes.new : ArgAttributes

Equations

• Miri.ABI.ArgAttributes.new = { regular := 0, argExt := Miri.ABI.ArgExtension.None, pointeeSize := Miri.ABI.Size.ZERO, pointeeAlign := none }

def Miri.ABI.ArgAttributes.contains (attrs : ArgAttributes) (mask : UInt16) : Bool

Equations

• attrs.contains mask = (attrs.regular &&& mask == mask)

def Miri.ABI.ArgAttributes.eqAbi (left right : ArgAttributes) : Bool

Equations

• left.eqAbi right = (left.contains 64 == right.contains 64 && left.argExt == right.argExt)

structure Miri.ABI.Uniform : Type

• unit : Reg
• total : Size
• isConsecutive : Bool

@[instance_reducible]

instance Miri.ABI.instDecidableEqUniform : DecidableEq Uniform

Equations

• Miri.ABI.instDecidableEqUniform = Miri.ABI.instDecidableEqUniform.decEq

def Miri.ABI.instDecidableEqUniform.decEq (x✝ x✝¹ : Uniform) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.ABI.instReprUniform : Repr Uniform

Equations

• Miri.ABI.instReprUniform = { reprPrec := Miri.ABI.instReprUniform.repr }

def Miri.ABI.instReprUniform.repr : Uniform → Nat → Std.Format

Equations

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

structure Miri.ABI.CastTarget : Type

• prefix : Array Reg
• restOffset : Option Size
• rest : Uniform
• attrs : ArgAttributes

def Miri.ABI.instDecidableEqCastTarget.decEq (x✝ x✝¹ : CastTarget) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.ABI.instDecidableEqCastTarget : DecidableEq CastTarget

Equations

• Miri.ABI.instDecidableEqCastTarget = Miri.ABI.instDecidableEqCastTarget.decEq

def Miri.ABI.instReprCastTarget.repr : CastTarget → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.ABI.instReprCastTarget : Repr CastTarget

Equations

• Miri.ABI.instReprCastTarget = { reprPrec := Miri.ABI.instReprCastTarget.repr }

def Miri.ABI.CastTarget.eqAbi (left right : CastTarget) : Bool

Equations

• left.eqAbi right = (left.prefix == right.prefix && left.restOffset == right.restOffset && left.rest == right.rest && left.attrs.eqAbi right.attrs)

inductive Miri.ABI.IndirectMode : Type

• Pointer : IndirectMode
• OnStack : IndirectMode
• AmdgpuKernelArg : IndirectMode

@[instance_reducible]

instance Miri.ABI.instDecidableEqIndirectMode : DecidableEq IndirectMode

Equations

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

def Miri.ABI.instReprIndirectMode.repr : IndirectMode → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.ABI.instReprIndirectMode : Repr IndirectMode

Equations

• Miri.ABI.instReprIndirectMode = { reprPrec := Miri.ABI.instReprIndirectMode.repr }

inductive Miri.ABI.PassMode : Type

• Ignore : PassMode
• Direct (attrs : ArgAttributes) : PassMode
• Pair (first second : ArgAttributes) : PassMode
• Cast (padI32Count : UInt8) (cast : CastTarget) : PassMode
• Indirect (attrs : ArgAttributes) (addressSpace : Option AddressSpace) (mode : IndirectMode) : PassMode
• IndirectUnsized (attrs metaAttrs : ArgAttributes) : PassMode

def Miri.ABI.instDecidableEqPassMode.decEq (x✝ x✝¹ : PassMode) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.ABI.instDecidableEqPassMode.decEq Miri.ABI.PassMode.Ignore Miri.ABI.PassMode.Ignore = isTrue ⋯
• Miri.ABI.instDecidableEqPassMode.decEq Miri.ABI.PassMode.Ignore (Miri.ABI.PassMode.Direct attrs) = isFalse ⋯
• Miri.ABI.instDecidableEqPassMode.decEq Miri.ABI.PassMode.Ignore (Miri.ABI.PassMode.Pair first second) = isFalse ⋯
• Miri.ABI.instDecidableEqPassMode.decEq Miri.ABI.PassMode.Ignore (Miri.ABI.PassMode.Cast padI32Count cast) = isFalse ⋯
• Miri.ABI.instDecidableEqPassMode.decEq Miri.ABI.PassMode.Ignore (Miri.ABI.PassMode.Indirect attrs addressSpace mode) = isFalse ⋯
• Miri.ABI.instDecidableEqPassMode.decEq Miri.ABI.PassMode.Ignore (Miri.ABI.PassMode.IndirectUnsized attrs metaAttrs) = isFalse ⋯
• Miri.ABI.instDecidableEqPassMode.decEq (Miri.ABI.PassMode.Direct attrs) Miri.ABI.PassMode.Ignore = isFalse ⋯
• Miri.ABI.instDecidableEqPassMode.decEq (Miri.ABI.PassMode.Direct a) (Miri.ABI.PassMode.Direct b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.ABI.instDecidableEqPassMode.decEq (Miri.ABI.PassMode.Direct attrs) (Miri.ABI.PassMode.Pair first second) = isFalse ⋯
• Miri.ABI.instDecidableEqPassMode.decEq (Miri.ABI.PassMode.Direct attrs) (Miri.ABI.PassMode.Cast padI32Count cast) = isFalse ⋯
• Miri.ABI.instDecidableEqPassMode.decEq (Miri.ABI.PassMode.Direct attrs) (Miri.ABI.PassMode.Indirect attrs_1 addressSpace mode) = isFalse ⋯
• Miri.ABI.instDecidableEqPassMode.decEq (Miri.ABI.PassMode.Direct attrs) (Miri.ABI.PassMode.IndirectUnsized attrs_1 metaAttrs) = isFalse ⋯
• Miri.ABI.instDecidableEqPassMode.decEq (Miri.ABI.PassMode.Pair first second) Miri.ABI.PassMode.Ignore = isFalse ⋯
• Miri.ABI.instDecidableEqPassMode.decEq (Miri.ABI.PassMode.Pair first second) (Miri.ABI.PassMode.Direct attrs) = isFalse ⋯
• Miri.ABI.instDecidableEqPassMode.decEq (Miri.ABI.PassMode.Pair a a_1) (Miri.ABI.PassMode.Pair b b_1) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯
• Miri.ABI.instDecidableEqPassMode.decEq (Miri.ABI.PassMode.Pair first second) (Miri.ABI.PassMode.Cast padI32Count cast) = isFalse ⋯
• Miri.ABI.instDecidableEqPassMode.decEq (Miri.ABI.PassMode.Pair first second) (Miri.ABI.PassMode.Indirect attrs addressSpace mode) = isFalse ⋯
• Miri.ABI.instDecidableEqPassMode.decEq (Miri.ABI.PassMode.Pair first second) (Miri.ABI.PassMode.IndirectUnsized attrs metaAttrs) = isFalse ⋯
• Miri.ABI.instDecidableEqPassMode.decEq (Miri.ABI.PassMode.Cast padI32Count cast) Miri.ABI.PassMode.Ignore = isFalse ⋯
• Miri.ABI.instDecidableEqPassMode.decEq (Miri.ABI.PassMode.Cast padI32Count cast) (Miri.ABI.PassMode.Direct attrs) = isFalse ⋯
• Miri.ABI.instDecidableEqPassMode.decEq (Miri.ABI.PassMode.Cast padI32Count cast) (Miri.ABI.PassMode.Pair first second) = isFalse ⋯
• Miri.ABI.instDecidableEqPassMode.decEq (Miri.ABI.PassMode.Cast a a_1) (Miri.ABI.PassMode.Cast b b_1) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯
• Miri.ABI.instDecidableEqPassMode.decEq (Miri.ABI.PassMode.Cast padI32Count cast) (Miri.ABI.PassMode.Indirect attrs addressSpace mode) = isFalse ⋯
• Miri.ABI.instDecidableEqPassMode.decEq (Miri.ABI.PassMode.Cast padI32Count cast) (Miri.ABI.PassMode.IndirectUnsized attrs metaAttrs) = isFalse ⋯
• Miri.ABI.instDecidableEqPassMode.decEq (Miri.ABI.PassMode.Indirect attrs addressSpace mode) Miri.ABI.PassMode.Ignore = isFalse ⋯
• Miri.ABI.instDecidableEqPassMode.decEq (Miri.ABI.PassMode.Indirect attrs addressSpace mode) (Miri.ABI.PassMode.Direct attrs_1) = isFalse ⋯
• Miri.ABI.instDecidableEqPassMode.decEq (Miri.ABI.PassMode.Indirect attrs addressSpace mode) (Miri.ABI.PassMode.Pair first second) = isFalse ⋯
• Miri.ABI.instDecidableEqPassMode.decEq (Miri.ABI.PassMode.Indirect attrs addressSpace mode) (Miri.ABI.PassMode.Cast padI32Count cast) = isFalse ⋯
• Miri.ABI.instDecidableEqPassMode.decEq (Miri.ABI.PassMode.Indirect attrs addressSpace mode) (Miri.ABI.PassMode.IndirectUnsized attrs_1 metaAttrs) = isFalse ⋯
• Miri.ABI.instDecidableEqPassMode.decEq (Miri.ABI.PassMode.IndirectUnsized attrs metaAttrs) Miri.ABI.PassMode.Ignore = isFalse ⋯
• Miri.ABI.instDecidableEqPassMode.decEq (Miri.ABI.PassMode.IndirectUnsized attrs metaAttrs) (Miri.ABI.PassMode.Direct attrs_1) = isFalse ⋯
• Miri.ABI.instDecidableEqPassMode.decEq (Miri.ABI.PassMode.IndirectUnsized attrs metaAttrs) (Miri.ABI.PassMode.Pair first second) = isFalse ⋯
• Miri.ABI.instDecidableEqPassMode.decEq (Miri.ABI.PassMode.IndirectUnsized attrs metaAttrs) (Miri.ABI.PassMode.Cast padI32Count cast) = isFalse ⋯
• Miri.ABI.instDecidableEqPassMode.decEq (Miri.ABI.PassMode.IndirectUnsized attrs metaAttrs) (Miri.ABI.PassMode.Indirect attrs_1 addressSpace mode) = isFalse ⋯

@[instance_reducible]

instance Miri.ABI.instDecidableEqPassMode : DecidableEq PassMode

Equations

• Miri.ABI.instDecidableEqPassMode = Miri.ABI.instDecidableEqPassMode.decEq

def Miri.ABI.instReprPassMode.repr : PassMode → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.ABI.instReprPassMode : Repr PassMode

Equations

• Miri.ABI.instReprPassMode = { reprPrec := Miri.ABI.instReprPassMode.repr }

def Miri.ABI.PassMode.eqAbi : PassMode → PassMode → Bool

Equations

• Miri.ABI.PassMode.Ignore.eqAbi Miri.ABI.PassMode.Ignore = true
• (Miri.ABI.PassMode.Direct a).eqAbi (Miri.ABI.PassMode.Direct b) = a.eqAbi b
• (Miri.ABI.PassMode.Pair a b).eqAbi (Miri.ABI.PassMode.Pair c d) = (a.eqAbi c && b.eqAbi d)
• (Miri.ABI.PassMode.Cast pad a).eqAbi (Miri.ABI.PassMode.Cast pad' b) = (a.eqAbi b && pad == pad')
• (Miri.ABI.PassMode.Indirect a space mode).eqAbi (Miri.ABI.PassMode.Indirect b space' mode') = (a.eqAbi b && space == space' && mode == mode')
• (Miri.ABI.PassMode.IndirectUnsized a metadata).eqAbi (Miri.ABI.PassMode.IndirectUnsized b metadata') = (a.eqAbi b && metadata.eqAbi metadata')
• x✝¹.eqAbi x✝ = false

def Miri.ABI.PassMode.isIgnore : PassMode → Bool

Equations

• Miri.ABI.PassMode.Ignore.isIgnore = true
• x✝.isIgnore = false

def Miri.ABI.PassMode.isDirect : PassMode → Bool

Equations

• (Miri.ABI.PassMode.Direct attrs).isDirect = true
• x✝.isDirect = false

def Miri.ABI.PassMode.isUnsizedIndirect : PassMode → Bool

Equations

• (Miri.ABI.PassMode.IndirectUnsized attrs metaAttrs).isUnsizedIndirect = true
• x✝.isUnsizedIndirect = false

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

• layout : TyAndLayout Ty
• mode : PassMode

@[instance_reducible]

instance Miri.ABI.instDecidableEqArgAbi {Ty✝ : Type} [DecidableEq Ty✝] : DecidableEq (ArgAbi Ty✝)

Equations

• Miri.ABI.instDecidableEqArgAbi = Miri.ABI.instDecidableEqArgAbi.decEq

def Miri.ABI.instDecidableEqArgAbi.decEq {Ty✝ : Type} [DecidableEq Ty✝] (x✝ x✝¹ : ArgAbi Ty✝) : Decidable (x✝ = x✝¹)

Equations

• Miri.ABI.instDecidableEqArgAbi.decEq { layout := a, mode := a_1 } { layout := b, mode := 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.ABI.instReprArgAbi {Ty✝ : Type} [Repr Ty✝] : Repr (ArgAbi Ty✝)

Equations

• Miri.ABI.instReprArgAbi = { reprPrec := Miri.ABI.instReprArgAbi.repr }

def Miri.ABI.instReprArgAbi.repr {Ty✝ : Type} [Repr Ty✝] : ArgAbi Ty✝ → Nat → Std.Format

Equations

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

def Miri.ABI.ArgAbi.eqAbi {Ty : Type} [DecidableEq Ty] (left right : ArgAbi Ty) : Bool

Equations

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

def Miri.ABI.ArgAbi.isIgnore {Ty : Type} (arg : ArgAbi Ty) : Bool

Equations

• arg.isIgnore = arg.mode.isIgnore

def Miri.ABI.ArgAbi.isUnsizedIndirect {Ty : Type} (arg : ArgAbi Ty) : Bool

Equations

• arg.isUnsizedIndirect = arg.mode.isUnsizedIndirect