Pinned env.rs and Unix/Windows env storage. Os is a lossless target OS string, never a host String approximation. All memory operations are effectful leaves and must preserve provenance, allocation kinds, and race checks.

@[reducible, inline]

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

Equations

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

structure Miri.Interpreter.EnvVars.Unix (P : Type) : Type

• variables : Array (ByteArray × Memory.Pointer P)
• environ : Memory.Pointer P

inductive Miri.Interpreter.EnvVars.State (P Os : Type) : Type

• uninit {P Os : Type} : State P Os
• unix {P Os : Type} (vars : Unix P) : State P Os
• windows {P Os : Type} (variables : Array (Os × Os)) : State P Os

inductive Miri.Interpreter.EnvVars.Kind : Type

• machine : Kind
• externStatic : Kind
• runtime : Kind
• winLocal : Kind

@[instance_reducible]

instance Miri.Interpreter.EnvVars.instDecidableEqKind : DecidableEq Kind

Equations

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

@[instance_reducible]

instance Miri.Interpreter.EnvVars.instReprKind : Repr Kind

Equations

• Miri.Interpreter.EnvVars.instReprKind = { reprPrec := Miri.Interpreter.EnvVars.instReprKind.repr }

def Miri.Interpreter.EnvVars.instReprKind.repr : Kind → Nat → Std.Format

Equations

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

structure Miri.Interpreter.EnvVars.Hooks (P Os S : Type) : Type

• family : ForeignItems.Family
• get : M S (State P Os)
• put : State P Os → M S Unit
• encodeUnix : Os → M S ByteArray
• decodeUnix : ByteArray → M S Os
• emptyOs : Os
• concatOs : Os → Os → Os
• asciiOs : String → Os
• isEmpty : Os → Bool
• containsEquals : Os → Bool
• nullPointer : Memory.Pointer P
• isNull : Memory.Pointer P → M S Bool
• readCString : Memory.Pointer P → M S ByteArray
• allocCString : ByteArray → Kind → M S (Memory.Pointer P)
• allocPointerCell : Kind → M S (Memory.Pointer P)
• allocPointerArray : Nat → Kind → M S (Memory.Pointer P)
• projectPointerElement : Memory.Pointer P → Nat → Nat → M S (Memory.Pointer P)
• readPointer : Memory.Pointer P → M S (Memory.Pointer P)
• writePointer : Memory.Pointer P → Memory.Pointer P → M S Unit
• offset : Memory.Pointer P → UInt64 → M S (Memory.Pointer P)
• deallocate : Memory.Pointer P → Kind → M S Unit
• invalidArgument : M S Int32
• readWideString : Memory.Pointer P → M S Os
• writeWideString : Os → Memory.Pointer P → UInt32 → M S (Bool × UInt64)
• allocWideString : Os → Kind → M S (Memory.Pointer P)
• envVarNotFound : M S Unit

def Miri.Interpreter.EnvVars.allocEnvironmentBlock {P Os S : Type} (h : Hooks P Os S) (values : Array (Memory.Pointer P)) : M S (Memory.Pointer P)

Equations

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

def Miri.Interpreter.EnvVars.allocVariable {P Os S : Type} (h : Hooks P Os S) (name value : ByteArray) : M S (Memory.Pointer P)

Equations

• Miri.Interpreter.EnvVars.allocVariable h name value = h.allocCString (name ++ { data := #[61] } ++ value) Miri.Interpreter.EnvVars.Kind.machine

def Miri.Interpreter.EnvVars.initUnix {P Os S : Type} (h : Hooks P Os S) (variables : Array (ByteArray × ByteArray)) : M S Unit

Equations

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

def Miri.Interpreter.EnvVars.getPointer {P Os S : Type} (h : Hooks P Os S) (name : ByteArray) : M S (Option (Memory.Pointer P))

The environ cell read is required even when the lookup misses: it participates in data-race detection. The returned pointer aliases the actual name=value allocation.

Equations

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

def Miri.Interpreter.EnvVars.getEnv {Os P S : Type} [DecidableEq Os] (h : Hooks P Os S) (name : Os) : M S (Option Os)

Equations

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

def Miri.Interpreter.EnvVars.getenv {P Os S : Type} (h : Hooks P Os S) (name : Memory.Pointer P) : M S (Memory.Pointer P)

Equations

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

def Miri.Interpreter.EnvVars.updateEnviron {P Os S : Type} (h : Hooks P Os S) : M S Unit

Equations

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

def Miri.Interpreter.EnvVars.setenv {P Os S : Type} (h : Hooks P Os S) (namePointer valuePointer : Memory.Pointer P) : M S Int32

Equations

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

def Miri.Interpreter.EnvVars.unsetenv {P Os S : Type} (h : Hooks P Os S) (namePointer : Memory.Pointer P) : M S Int32

Equations

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

def Miri.Interpreter.EnvVars.init {Os P S : Type} [DecidableEq Os] (h : Hooks P Os S) (communicate : Bool) (forwarded : Array Os) (environment overrides : Array (Os × Os)) : M S Unit

Config environment is supplied evidence. No process environment is read implicitly, and explicit overrides win after forwarding.

Equations

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

def Miri.Interpreter.EnvVars.windowsBufferSize (result : Bool × UInt64) : Except StepError UInt32

Equations

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

def Miri.Interpreter.EnvVars.getEnvironmentVariableW {Os P S : Type} [DecidableEq Os] (h : Hooks P Os S) (name buffer : Memory.Pointer P) (size : UInt32) : M S UInt32

Equations

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

def Miri.Interpreter.EnvVars.getEnvironmentStringsW {P Os S : Type} (h : Hooks P Os S) : M S (Memory.Pointer P)

Equations

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

def Miri.Interpreter.EnvVars.freeEnvironmentStringsW {P Os S : Type} (h : Hooks P Os S) (pointer : Memory.Pointer P) : M S Int32

Equations

• Miri.Interpreter.EnvVars.freeEnvironmentStringsW h pointer = do Miri.Interpreter.EnvVars.checkWindows✝ h h.deallocate pointer Miri.Interpreter.EnvVars.Kind.runtime pure 1

def Miri.Interpreter.EnvVars.setEnvironmentVariableW {Os P S : Type} [DecidableEq Os] (h : Hooks P Os S) (namePointer valuePointer : Memory.Pointer P) : M S Bool

Equations

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

structure Miri.Interpreter.EnvVars.ProcessHooks (S : Type) : Type

• communicate : Bool
• family : ForeignItems.Family
• os : String
• hostPid : M S UInt32
• activeThread : M S UInt32
• threadIdTryFrom : UInt32 → M S (Option UInt32)

  Authoritative thread manager check includes termination and ID validity.

def Miri.Interpreter.EnvVars.getPid {S : Type} (h : ProcessHooks S) : M S UInt32

Equations

• Miri.Interpreter.EnvVars.getPid h = if h.communicate = true then h.hostPid else pure 1000

def Miri.Interpreter.EnvVars.getTid {S : Type} (h : ProcessHooks S) (thread : UInt32) : M S UInt32

Equations

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

def Miri.Interpreter.EnvVars.currentTid {S : Type} (h : ProcessHooks S) : M S UInt32

Equations

• Miri.Interpreter.EnvVars.currentTid h = do let __do_lift ← h.activeThread Miri.Interpreter.EnvVars.getTid h __do_lift

def Miri.Interpreter.EnvVars.threadIdFromLinuxTid {S : Type} (h : ProcessHooks S) (tid : UInt32) : M S (Option UInt32)

Equations

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

def Miri.Interpreter.EnvVars.provenanceRoots {P Os : Type} : State P Os → Array (Memory.Pointer P)

All environment-owned pointer roots, including the stable environ cell. Windows/Uninit store no provenance. GC must visit these without dereferencing.

Equations

• Miri.Interpreter.EnvVars.provenanceRoots Miri.Interpreter.EnvVars.State.uninit = #[]
• Miri.Interpreter.EnvVars.provenanceRoots (Miri.Interpreter.EnvVars.State.windows variables) = #[]
• Miri.Interpreter.EnvVars.provenanceRoots (Miri.Interpreter.EnvVars.State.unix vars) = #[vars.environ] ++ Array.map (fun (x : ByteArray × Miri.Memory.Pointer P) => x.snd) vars.variables