Documentation

Miri.Input.EvalWindowsCallbackAssembly

Construct the Windows callback boundary from the initialized source Core, its live foreign context, and the same Main hooks. This owns physical typed synchronization objects and callback routing; it does not seed Unix sockets or descriptors. Optional host time representations stay existential.

source
@[reducible, inline]
abbrev Miri.Input.EvalWindowsCallbackAssembly.Other (Raw Listener TcpStream Error : Type) :
Type
Equations
Instances For
    source
    @[reducible, inline]
    abbrev Miri.Input.EvalWindowsCallbackAssembly.Host (Poll Instant System H D Raw Listener TcpStream Error Native Profiler : Type) :
    Type
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[reducible, inline]
      abbrev Miri.Input.EvalWindowsCallbackAssembly.State (Os R 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.EvalWindowsCallbackAssembly.CoreState (Os R 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
          structure Miri.Input.EvalWindowsCallbackAssembly.Product (Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error C X F A : Type) :
          Type 1
          Instances For
            source
            def Miri.Input.EvalWindowsCallbackAssembly.fromSource {Os R H D Raw Listener TcpStream Error Aff B Poll Instant System Native Profiler C Meta Path Zone Timestamp ErrorHost AddrIter : Type} [DecidableEq Memory.MiriMemoryKind] [DecidableEq Os] (p : CompilerProviders.Prepared) (image : AllocationImage.Imported) (context : EvalConfigurationCore.ForeignContext Os R EvalSyncObjectAccess.Payload H D (Other Raw Listener TcpStream Error) Aff B (Host Poll Instant System H D Raw Listener TcpStream Error Native Profiler) C Instant (EvalWindowsCallDispatchConstruction.Assembly Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error C Meta Path Zone Timestamp)) (assembly : EvalWindowsCallDispatchConstruction.Assembly Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error C Meta Path Zone Timestamp) (main : Interpreter.MainMachine.Hooks (EvalWindowsFileConstruction.Payload Os R EvalSyncObjectAccess.Payload H D (Other Raw Listener TcpStream Error) Aff B (Host Poll Instant System H D Raw Listener TcpStream Error Native Profiler)) C (Other Raw Listener TcpStream Error) ABI.ExternAbi (ABI.FnAbi MIR.TyId) (ABI.ArgAbi MIR.TyId) Aff Interpreter.ProgramExitPoll) (sourceLeaves : EvalConfigurationCore.SourceLeaves Os R EvalSyncObjectAccess.Payload H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error ErrorHost Meta Path MIR.Place C Instant Interpreter.CallInstance AddrIter) (world : State Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) :
            Except (Interpreter.StepError × State Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (Product Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error C ABI.ExternAbi (ABI.FnAbi MIR.TyId) (ABI.ArgAbi MIR.TyId) × State Os R H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error)

            Create physical synchronization objects, backend-selected callback effects, the Main callback router, and a Windows time shim from the same initialized machine. If chrono data is absent its calls fail on demand while clock and synchronization operations still use the source host clock.

            Equations
            Instances For