Documentation

Miri.Input.EvalUnixMacOsConstruction

Source macOS foreign-item construction over the initialized Main state, canonical callback sync arena, source environment and the shared native FD registry. The sync projection below creates no new object tables.

source
@[reducible, inline]
abbrev Miri.Input.EvalUnixMacOsConstruction.Other (Raw Listener TcpStream Error : Type) :
Type
Equations
Instances For
    source
    @[reducible, inline]
    abbrev Miri.Input.EvalUnixMacOsConstruction.User (Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error : Type) :
    Type
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[reducible, inline]
      abbrev Miri.Input.EvalUnixMacOsConstruction.State (Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error : Type) :
      Type
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[reducible, inline]
        abbrev Miri.Input.EvalUnixMacOsConstruction.Control (Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error : Type) :
        Type
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Miri.Input.EvalUnixMacOsConstruction.syncFromSource {Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error C Zone Timestamp ErrorHost : Type} [DecidableEq Memory.MiriMemoryKind] (p : CompilerProviders.Prepared) (memory : EvalHostRuntimeConstruction.EnvironmentMemory (Control Os R EvalSyncObjectAccess.Payload H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) C EvalSyncObjectAccess.Payload) (objects : Interpreter.ForeignSyncMachine.Objects (Interpreter.LinuxFutexMachine.State Memory.MiriMemoryKind (EvalSyncMachine.World Os R EvalSyncObjectAccess.Payload H D (Other Raw Listener TcpStream Error) Aff B Poll Instant System Native Profiler))) (futex : Interpreter.LinuxFutexMachine.Hooks Memory.MiriMemoryKind (EvalSyncMachine.World Os R EvalSyncObjectAccess.Payload H D (Other Raw Listener TcpStream Error) Aff B Poll Instant System Native Profiler) C EvalSyncObjectAccess.Payload (Other Raw Listener TcpStream Error) B Instant System Zone Timestamp ErrorHost) (choice : C) (time : Option (Interpreter.TimeShims.Hooks (Interpreter.LinuxFutexMachine.State Memory.MiriMemoryKind (EvalSyncMachine.World Os R EvalSyncObjectAccess.Payload H D (Other Raw Listener TcpStream Error) Aff B Poll Instant System Native Profiler)) Instant System Zone Timestamp)) (hostUsizeBits semaphoreBudget : Nat) :
          Except Interpreter.StepError (Interpreter.MacOsSync.Hooks (Interpreter.LinuxFutexMachine.State Memory.MiriMemoryKind (EvalSyncMachine.World Os R EvalSyncObjectAccess.Payload H D (Other Raw Listener TcpStream Error) Aff B Poll Instant System Native Profiler)) Concurrency.TypedSyncRuntime.Ref)
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Miri.Input.EvalUnixMacOsConstruction.handlerFromSource {Os R H D Raw Listener TcpStream Error Aff B Poll Instant System Native Profiler C Zone Timestamp ErrorHost Duration Meta : Type} [DecidableEq Memory.MiriMemoryKind] (p : CompilerProviders.Prepared) (core : Interpreter.ForeignItems.Core Memory.Provenance (Interpreter.LinuxFutexMachine.State Memory.MiriMemoryKind (EvalSyncMachine.World Os R EvalSyncObjectAccess.Payload H D (Other Raw Listener TcpStream Error) Aff B Poll Instant System Native Profiler)) (Interpreter.RuntimePlace Memory.Provenance) (Interpreter.RuntimePlace Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) Interpreter.LoadedBody Interpreter.CallInstance) (environment : Interpreter.UnixEnvironment.Hooks (Interpreter.LinuxFutexMachine.State Memory.MiriMemoryKind (EvalSyncMachine.World Os R EvalSyncObjectAccess.Payload H D (Other Raw Listener TcpStream Error) Aff B Poll Instant System Native Profiler)) Os Error Interpreter.EnvVars.Kind) (main : Interpreter.MainMachine.Hooks (EvalCallbackMachine.ThreadUser Os R EvalSyncObjectAccess.Payload H D (Other Raw Listener TcpStream Error) Aff B Poll Instant System Native Profiler) C (Other Raw Listener TcpStream Error) ABI.ExternAbi (ABI.FnAbi MIR.TyId) (ABI.ArgAbi MIR.TyId) Aff EvalSyncObjectAccess.Payload) (memory : EvalHostRuntimeConstruction.EnvironmentMemory (Control Os R EvalSyncObjectAccess.Payload H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) C EvalSyncObjectAccess.Payload) (objects : Interpreter.ForeignSyncMachine.Objects (Interpreter.LinuxFutexMachine.State Memory.MiriMemoryKind (EvalSyncMachine.World Os R EvalSyncObjectAccess.Payload H D (Other Raw Listener TcpStream Error) Aff B Poll Instant System Native Profiler))) (futex : Interpreter.LinuxFutexMachine.Hooks Memory.MiriMemoryKind (EvalSyncMachine.World Os R EvalSyncObjectAccess.Payload H D (Other Raw Listener TcpStream Error) Aff B Poll Instant System Native Profiler) C EvalSyncObjectAccess.Payload (Other Raw Listener TcpStream Error) B Instant System Zone Timestamp ErrorHost) (time : Option (Interpreter.TimeShims.Hooks (Interpreter.LinuxFutexMachine.State Memory.MiriMemoryKind (EvalSyncMachine.World Os R EvalSyncObjectAccess.Payload H D (Other Raw Listener TcpStream Error) Aff B Poll Instant System Native Profiler)) Instant System Zone Timestamp)) (pthread : Interpreter.PthreadSync.Hooks (Interpreter.LinuxFutexMachine.State Memory.MiriMemoryKind (EvalSyncMachine.World Os R EvalSyncObjectAccess.Payload H D (Other Raw Listener TcpStream Error) Aff B Poll Instant System Native Profiler)) Concurrency.TypedSyncRuntime.Ref Duration) (fd : Interpreter.UnixFd.Hooks (Interpreter.LinuxFutexMachine.State Memory.MiriMemoryKind (EvalSyncMachine.World Os R EvalSyncObjectAccess.Payload H D (Other Raw Listener TcpStream Error) Aff B Poll Instant System Native Profiler)) H D (Other Raw Listener TcpStream Error) Error Meta) (choice : C) (communicate : Bool) (hostGetrandom : Nat → EStateM Interpreter.StepError (Interpreter.LinuxFutexMachine.State Memory.MiriMemoryKind (EvalSyncMachine.World Os R EvalSyncObjectAccess.Payload H D (Other Raw Listener TcpStream Error) Aff B Poll Instant System Native Profiler)) (Except String ByteArray)) (tape : Interpreter.ExecutionChoices.Access (Interpreter.LinuxFutexMachine.State Memory.MiriMemoryKind (EvalSyncMachine.World Os R EvalSyncObjectAccess.Payload H D (Other Raw Listener TcpStream Error) Aff B Poll Instant System Native Profiler))) (currentExe : EStateM Interpreter.StepError (Interpreter.LinuxFutexMachine.State Memory.MiriMemoryKind (EvalSyncMachine.World Os R EvalSyncObjectAccess.Payload H D (Other Raw Listener TcpStream Error) Aff B Poll Instant System Native Profiler)) (Option Os)) (hostUsizeBits semaphoreBudget : Nat) (stackAddress stackSize : UInt64) :
            Except Interpreter.StepError (Interpreter.UnixForeign.OptionalHandler (Interpreter.LinuxFutexMachine.State Memory.MiriMemoryKind (EvalSyncMachine.World Os R EvalSyncObjectAccess.Payload H D (Other Raw Listener TcpStream Error) Aff B Poll Instant System Native Profiler)))

            Assemble the remaining macOS foreign-item arm from the selected source Core, source environment/Main/TLS engines, native-FD registry, and the same callback-owned synchronization arena. Host executable-path conversion is a raw host result because its representation is outside the guest memory model; if that host leaf is absent, only _NSGetExecutablePath fails on demand.

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