Source-extracted ordered error tables and policy from pinned shims/io_error.rs. Host/target errno numbers remain compiler/host queries, never platform guesses.

@[reducible, inline]

abbrev Miri.Interpreter.IoError.M (σ α : Type) : Type

Equations

• Miri.Interpreter.IoError.M = EStateM Miri.Interpreter.StepError

inductive Miri.Interpreter.IoError.ErrorKind : Type

• ArgumentListTooLong : ErrorKind
• AddrInUse : ErrorKind
• AddrNotAvailable : ErrorKind
• ResourceBusy : ErrorKind
• ConnectionAborted : ErrorKind
• ConnectionRefused : ErrorKind
• ConnectionReset : ErrorKind
• Deadlock : ErrorKind
• QuotaExceeded : ErrorKind
• AlreadyExists : ErrorKind
• FileTooLarge : ErrorKind
• HostUnreachable : ErrorKind
• Interrupted : ErrorKind
• InvalidInput : ErrorKind
• IsADirectory : ErrorKind
• FilesystemLoop : ErrorKind
• NotFound : ErrorKind
• OutOfMemory : ErrorKind
• StorageFull : ErrorKind
• TooManyLinks : ErrorKind
• InvalidFilename : ErrorKind
• NetworkDown : ErrorKind
• NetworkUnreachable : ErrorKind
• NotConnected : ErrorKind
• NotADirectory : ErrorKind
• DirectoryNotEmpty : ErrorKind
• BrokenPipe : ErrorKind
• ReadOnlyFilesystem : ErrorKind
• NotSeekable : ErrorKind
• StaleNetworkFileHandle : ErrorKind
• TimedOut : ErrorKind
• ExecutableFileBusy : ErrorKind
• CrossesDevices : ErrorKind
• InProgress : ErrorKind
• InputOutputError : ErrorKind
• PermissionDenied : ErrorKind
• WouldBlock : ErrorKind
• Unsupported : ErrorKind
• TooManyOpenFiles : ErrorKind
• Other : ErrorKind

@[instance_reducible]

instance Miri.Interpreter.IoError.instDecidableEqErrorKind : DecidableEq ErrorKind

Equations

• Miri.Interpreter.IoError.instDecidableEqErrorKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Miri.Interpreter.IoError.instReprErrorKind.repr : ErrorKind → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.IoError.instReprErrorKind : Repr ErrorKind

Equations

• Miri.Interpreter.IoError.instReprErrorKind = { reprPrec := Miri.Interpreter.IoError.instReprErrorKind.repr }

structure Miri.Interpreter.IoError.HostError (Host : Type) : Type

• kind : ErrorKind
• raw : Option Int32
• payload : Host

inductive Miri.Interpreter.IoError.Error (Host : Type) : Type

• libc {Host : Type} (name : String) : Error Host
• windows {Host : Type} (name : String) : Error Host
• host {Host : Type} (error : HostError Host) : Error Host
• raw {Host : Type} (value : Memory.Scalar Memory.Provenance) : Error Host

def Miri.Interpreter.IoError.unixTable : Array (String × ErrorKind)

Equations

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

def Miri.Interpreter.IoError.windowsTable : Array (String × ErrorKind)

Equations

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

def Miri.Interpreter.IoError.unixErrnoNames : Array String

Equations

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

structure Miri.Interpreter.IoError.Hooks (S Host : Type) : Type

• family : ForeignItems.Family
• os : String
• hostUnix : Bool
• hostErrno : String → M S Int32
• libc : String → M S (Memory.Scalar Memory.Provenance)
• windows : String → M S (Memory.Scalar Memory.Provenance)
• scalarI32 : Memory.Scalar Memory.Provenance → M S Int32
• scalarU32 : Memory.Scalar Memory.Provenance → M S UInt32
• hostFromRaw : Int32 → M S (HostError Host)
• hostFromKind : ErrorKind → M S (HostError Host)
• getLastErrorPlace : M S (Option (MPlaceTy Memory.Provenance))
• setLastErrorPlace : MPlaceTy Memory.Provenance → M S Unit
• allocateU32Machine : M S (MPlaceTy Memory.Provenance)
• writeScalar : Memory.Scalar Memory.Provenance → MPlaceTy Memory.Provenance → M S Unit
• readScalar : MPlaceTy Memory.Provenance → M S (Memory.Scalar Memory.Provenance)
• writeInt : Int → MPlaceTy Memory.Provenance → M S Unit

def Miri.Interpreter.IoError.hostErrorToErrnum {S H : Type} (h : Hooks S H) (error : HostError H) : M S (Memory.Scalar Memory.Provenance)

Equations

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

def Miri.Interpreter.IoError.toErrnum {S H : Type} (h : Hooks S H) : Error H → M S (Memory.Scalar Memory.Provenance)

Equations

• Miri.Interpreter.IoError.toErrnum h (Miri.Interpreter.IoError.Error.host error) = Miri.Interpreter.IoError.hostErrorToErrnum h error
• Miri.Interpreter.IoError.toErrnum h (Miri.Interpreter.IoError.Error.libc name) = h.libc name
• Miri.Interpreter.IoError.toErrnum h (Miri.Interpreter.IoError.Error.windows name) = h.windows name
• Miri.Interpreter.IoError.toErrnum h (Miri.Interpreter.IoError.Error.raw value) = pure value

def Miri.Interpreter.IoError.lastErrorPlace {S H : Type} (h : Hooks S H) : M S (MPlaceTy Memory.Provenance)

Equations

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

def Miri.Interpreter.IoError.setLastError {S H : Type} (h : Hooks S H) (error : Error H) : M S Unit

Equations

• Miri.Interpreter.IoError.setLastError h error = do let value ← Miri.Interpreter.IoError.toErrnum h error let __do_lift ← Miri.Interpreter.IoError.lastErrorPlace h h.writeScalar value __do_lift

def Miri.Interpreter.IoError.setErrnoAndReturnNeg1 {S H : Type} (h : Hooks S H) (error : Error H) (dest : MPlaceTy Memory.Provenance) : M S Unit

Equations

• Miri.Interpreter.IoError.setErrnoAndReturnNeg1 h error dest = do Miri.Interpreter.IoError.setLastError h error h.writeInt (-1) dest

def Miri.Interpreter.IoError.setErrnoAndReturnNeg1I32 {S H : Type} (h : Hooks S H) (error : Error H) : M S Int32

Equations

• Miri.Interpreter.IoError.setErrnoAndReturnNeg1I32 h error = do Miri.Interpreter.IoError.setLastError h error pure (-1)

def Miri.Interpreter.IoError.setErrnoAndReturnNeg1I64 {S H : Type} (h : Hooks S H) (error : Error H) : M S Int64

Equations

• Miri.Interpreter.IoError.setErrnoAndReturnNeg1I64 h error = do Miri.Interpreter.IoError.setLastError h error pure (-1)

def Miri.Interpreter.IoError.getLastError {S H : Type} (h : Hooks S H) : M S (Memory.Scalar Memory.Provenance)

Equations

• Miri.Interpreter.IoError.getLastError h = do let __do_lift ← Miri.Interpreter.IoError.lastErrorPlace h h.readScalar __do_lift

def Miri.Interpreter.IoError.tryErrnumToHost {S H : Type} (h : Hooks S H) (value : Memory.Scalar Memory.Provenance) : M S (Option (HostError H))

Equations

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

def Miri.Interpreter.IoError.intoNtstatus {H : Type} : Error H → Int32

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.IoError.intoNtstatus x✝ = Int32.ofInt 3221225861

def Miri.Interpreter.IoError.tryUnwrap {S H A : Type} (h : Hooks S H) (result : Except (HostError H) A) (negativeOne : A) : M S A

Equations

• Miri.Interpreter.IoError.tryUnwrap h (Except.ok value) negativeOne = pure value
• Miri.Interpreter.IoError.tryUnwrap h (Except.error error) negativeOne = do Miri.Interpreter.IoError.setLastError h (Miri.Interpreter.IoError.Error.host error) pure negativeOne