Documentation

Miri.Input.EvalCoreMachine

Physical core construction for the actual EvalWorld payload. Supplied compiler/host policies survive; memory operations, scalar arithmetic, validity, atomic storage and SIMD lanes are replaced by canonical source drivers.

source
@[reducible, inline]
abbrev Miri.Input.EvalCoreMachine.World (Os R Payload H D O Aff B Host : Type) :
Type
Equations
Instances For
    source
    @[reducible, inline]
    abbrev Miri.Input.EvalCoreMachine.Stored (Os R P H D O Aff B Host : Type) :
    Type
    Equations
    Instances For
      source
      @[reducible, inline]
      abbrev Miri.Input.EvalCoreMachine.User (Os R P H D O Aff B Host : Type) :
      Type
      Equations
      Instances For
        source
        @[reducible, inline]
        abbrev Miri.Input.EvalCoreMachine.State (Os R P H D O Aff B Host : Type) :
        Type
        Equations
        Instances For
          source
          def Miri.Input.EvalCoreMachine.tape {Os R P H D O Aff B Host : Type} :
          Interpreter.ExecutionChoices.Access (State Os R P H D O Aff B Host)

          One tape in the actual World; registry and Control survive every draw.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Miri.Input.EvalCoreMachine.extras {P Os R H D O Aff B Host : Type} (onAccess : P → Concurrency.SyncObject.AccessKind → Interpreter.PlaceMachine.MachineM Memory.MiriMemoryKind (User Os R P H D O Aff B Host) Unit) (weakError : Concurrency.StoreBufferAllocError → Interpreter.StepError) :
            Interpreter.MemoryExtras.Hooks Memory.MiriMemoryKind (User Os R P H D O Aff B Host) P

            Sync payload execution is an actual required machine operation; its registry is always the single shared runtime.extras, never caller-selected.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Miri.Input.EvalCoreMachine.config {C Os R P H D O Aff B Host X ClockHost : Type} (prepared : CompilerFactAdapters.Prepared) (runtime : CompilerRuntimeQueries.Prepared) (limits : Interpreter.ExecutionMachine.Limits) (choice : C) (failureRate : UInt64) (spans : Interpreter.AllocationDriver.SpanHooks) (pointers : Interpreter.PointerMachine.Hooks Memory.MiriMemoryKind (Interpreter.ValidityMachine.Control (Stored Os R P H D O Aff B Host))) (sync : P → Concurrency.SyncObject.AccessKind → Interpreter.PlaceMachine.MachineM Memory.MiriMemoryKind (User Os R P H D O Aff B Host) Unit) (weakError : Concurrency.StoreBufferAllocError → Interpreter.StepError) (deallocation : Interpreter.AllocationMachine.DeallocationHooks Memory.MiriMemoryKind (User Os R P H D O Aff B Host) P) (base : Interpreter.ExecutionMachine.Config Memory.MiriMemoryKind (User Os R P H D O Aff B Host) C O X ClockHost) :
              Interpreter.ExecutionMachine.Config Memory.MiriMemoryKind (User Os R P H D O Aff B Host) C O X ClockHost

              Close the caller-visible core configuration on EvalWorld. Backend dispatch, compiler allocation/global/vtable queries, diagnostic policy, platform calls, and allocation storage remain explicit source dependencies. The physical callbacks overwritten here cannot be chosen independently by the caller.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def Miri.Input.EvalCoreMachine.step {C Os R P H D O Aff B Host X ClockHost : Type} (prepared : CompilerFactAdapters.Prepared) (runtime : CompilerRuntimeQueries.Prepared) (limits : Interpreter.ExecutionMachine.Limits) (choice : C) (failureRate : UInt64) (spans : Interpreter.AllocationDriver.SpanHooks) (pointers : Interpreter.PointerMachine.Hooks Memory.MiriMemoryKind (Interpreter.ValidityMachine.Control (Stored Os R P H D O Aff B Host))) (sync : P → Concurrency.SyncObject.AccessKind → Interpreter.PlaceMachine.MachineM Memory.MiriMemoryKind (User Os R P H D O Aff B Host) Unit) (weakError : Concurrency.StoreBufferAllocError → Interpreter.StepError) (deallocation : Interpreter.AllocationMachine.DeallocationHooks Memory.MiriMemoryKind (User Os R P H D O Aff B Host) P) (base : Interpreter.ExecutionMachine.Config Memory.MiriMemoryKind (User Os R P H D O Aff B Host) C O X ClockHost) (state : Interpreter.MachineHooks.State Memory.MiriMemoryKind (Interpreter.ExecutionStateTransport.Outer (World Os R P H D O Aff B Host))) :
                Interpreter.StepResult (Interpreter.MachineHooks.State Memory.MiriMemoryKind (Interpreter.ExecutionStateTransport.Outer (World Os R P H D O Aff B Host))) Bool

                Actual outer-state MIR entry: the physical closure above is mandatory.

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