Complete canonical calling-convention and FnAbi records from pinned rustc_abi/canon_abi.rs and rustc_target/callconv/mod.rs:660–679. Target ABI classification is supplied by the compiler, not recomputed by this module.

inductive Miri.ABI.ArmCall : Type

• Aapcs : ArmCall
• CCmseNonSecureCall : ArmCall
• CCmseNonSecureEntry : ArmCall

@[instance_reducible]

instance Miri.ABI.instDecidableEqArmCall : DecidableEq ArmCall

Equations

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

def Miri.ABI.instReprArmCall.repr : ArmCall → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.ABI.instReprArmCall : Repr ArmCall

Equations

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

inductive Miri.ABI.InterruptKind : Type

• Avr : InterruptKind
• AvrNonBlocking : InterruptKind
• Msp430 : InterruptKind
• RiscvMachine : InterruptKind
• RiscvSupervisor : InterruptKind
• X86 : InterruptKind

@[instance_reducible]

instance Miri.ABI.instDecidableEqInterruptKind : DecidableEq InterruptKind

Equations

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

def Miri.ABI.instReprInterruptKind.repr : InterruptKind → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.ABI.instReprInterruptKind : Repr InterruptKind

Equations

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

inductive Miri.ABI.X86Call : Type

• Fastcall : X86Call
• Stdcall : X86Call
• SysV64 : X86Call
• Thiscall : X86Call
• Vectorcall : X86Call
• Win64 : X86Call

@[instance_reducible]

instance Miri.ABI.instDecidableEqX86Call : DecidableEq X86Call

Equations

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

def Miri.ABI.instReprX86Call.repr : X86Call → Nat → Std.Format

Equations

• Miri.ABI.instReprX86Call.repr Miri.ABI.X86Call.Fastcall prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.ABI.X86Call.Fastcall")).group prec✝
• Miri.ABI.instReprX86Call.repr Miri.ABI.X86Call.Stdcall prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.ABI.X86Call.Stdcall")).group prec✝
• Miri.ABI.instReprX86Call.repr Miri.ABI.X86Call.SysV64 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.ABI.X86Call.SysV64")).group prec✝
• Miri.ABI.instReprX86Call.repr Miri.ABI.X86Call.Thiscall prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.ABI.X86Call.Thiscall")).group prec✝
• Miri.ABI.instReprX86Call.repr Miri.ABI.X86Call.Vectorcall prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.ABI.X86Call.Vectorcall")).group prec✝
• Miri.ABI.instReprX86Call.repr Miri.ABI.X86Call.Win64 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.ABI.X86Call.Win64")).group prec✝

@[instance_reducible]

instance Miri.ABI.instReprX86Call : Repr X86Call

Equations

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

inductive Miri.ABI.CanonAbi : Type

• C : CanonAbi
• Rust : CanonAbi
• RustCold : CanonAbi
• RustPreserveNone : CanonAbi
• RustTail : CanonAbi
• Custom : CanonAbi
• Swift : CanonAbi
• Arm (call : ArmCall) : CanonAbi
• GpuKernel : CanonAbi
• Interrupt (kind : InterruptKind) : CanonAbi
• X86 (call : X86Call) : CanonAbi

def Miri.ABI.instDecidableEqCanonAbi.decEq (x✝ x✝¹ : CanonAbi) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.ABI.instDecidableEqCanonAbi : DecidableEq CanonAbi

Equations

• Miri.ABI.instDecidableEqCanonAbi = Miri.ABI.instDecidableEqCanonAbi.decEq

def Miri.ABI.instReprCanonAbi.repr : CanonAbi → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Miri.ABI.instReprCanonAbi.repr Miri.ABI.CanonAbi.C prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.ABI.CanonAbi.C")).group prec✝
• Miri.ABI.instReprCanonAbi.repr Miri.ABI.CanonAbi.Rust prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.ABI.CanonAbi.Rust")).group prec✝
• Miri.ABI.instReprCanonAbi.repr Miri.ABI.CanonAbi.RustCold prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.ABI.CanonAbi.RustCold")).group prec✝
• Miri.ABI.instReprCanonAbi.repr Miri.ABI.CanonAbi.RustTail prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.ABI.CanonAbi.RustTail")).group prec✝
• Miri.ABI.instReprCanonAbi.repr Miri.ABI.CanonAbi.Custom prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.ABI.CanonAbi.Custom")).group prec✝
• Miri.ABI.instReprCanonAbi.repr Miri.ABI.CanonAbi.Swift prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.ABI.CanonAbi.Swift")).group prec✝
• Miri.ABI.instReprCanonAbi.repr Miri.ABI.CanonAbi.GpuKernel prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.ABI.CanonAbi.GpuKernel")).group prec✝

@[instance_reducible]

instance Miri.ABI.instReprCanonAbi : Repr CanonAbi

Equations

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

def Miri.ABI.CanonAbi.isRusticAbi : CanonAbi → Bool

Equations

• Miri.ABI.CanonAbi.Rust.isRusticAbi = true
• Miri.ABI.CanonAbi.RustCold.isRusticAbi = true
• Miri.ABI.CanonAbi.RustPreserveNone.isRusticAbi = true
• Miri.ABI.CanonAbi.RustTail.isRusticAbi = true
• Miri.ABI.CanonAbi.C.isRusticAbi = false
• Miri.ABI.CanonAbi.Custom.isRusticAbi = false
• Miri.ABI.CanonAbi.Swift.isRusticAbi = false
• (Miri.ABI.CanonAbi.Arm call).isRusticAbi = false
• Miri.ABI.CanonAbi.GpuKernel.isRusticAbi = false
• (Miri.ABI.CanonAbi.Interrupt kind).isRusticAbi = false
• (Miri.ABI.CanonAbi.X86 call).isRusticAbi = false

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

• args : Array (ArgAbi Ty)
• ret : ArgAbi Ty
• cVariadic : Bool
• fixedCount : UInt32
• conv : CanonAbi
• canUnwind : Bool

@[instance_reducible]

instance Miri.ABI.instDecidableEqFnAbi {Ty✝ : Type} [DecidableEq Ty✝] : DecidableEq (FnAbi Ty✝)

Equations

• Miri.ABI.instDecidableEqFnAbi = Miri.ABI.instDecidableEqFnAbi.decEq

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

Equations

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

@[instance_reducible]

instance Miri.ABI.instReprFnAbi {Ty✝ : Type} [Repr Ty✝] : Repr (FnAbi Ty✝)

Equations

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

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

Equations

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