Documentation

Miri.Input.EvalCompilerMachine

Production compiler/physical composition for the single EvalWorld. Compiler identities are prepared once, symbolic registries use World.functions/vtables, and address/salt decisions consume the same source-event tape as physical core. Sources: step.rs/call.rs query sites; memory.rs global function/vtable allocation; traits.rs symbolic vtables; machine.rs root-pointer adjustment.

source
@[reducible, inline]
abbrev Miri.Input.EvalCompilerMachine.User (Os R P H D O Aff B Host : Type) :
Type
Equations
Instances For
    source
    @[reducible, inline]
    abbrev Miri.Input.EvalCompilerMachine.State (Os R P H D O Aff B Host : Type) :
    Type
    Equations
    Instances For
      source
      @[reducible, inline]
      abbrev Miri.Input.EvalCompilerMachine.Stored (Os R P H D O Aff B Host : Type) :
      Type
      Equations
      Instances For
        source
        def Miri.Input.EvalCompilerMachine.functions {Os R P H D O Aff B Host : Type} (pointers : Interpreter.PointerMachine.Hooks Memory.MiriMemoryKind (Interpreter.ValidityMachine.Control (Stored Os R P H D O Aff B Host))) (base : Interpreter.FunctionPointers.Hooks Memory.MiriMemoryKind (User Os R P H D O Aff B Host) O) :
        Interpreter.FunctionPointers.Hooks Memory.MiriMemoryKind (User Os R P H D O Aff B Host) O

        The one actual function registry; no compiler shadow allocation map.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Miri.Input.EvalCompilerMachine.vtables {Os R P H D O Aff B Host : Type} (prepared : CompilerProviders.Prepared) (image : AllocationImage.Imported) (functionEngine : Interpreter.FunctionPointers.Hooks Memory.MiriMemoryKind (User Os R P H D O Aff B Host) O) :
          Interpreter.VTableMachine.Hooks Memory.MiriMemoryKind (User Os R P H D O Aff B Host) O

          The one actual symbolic vtable registry. Imported identities are installed by CompilerProviders from the same image/source allocation mapping.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Miri.Input.EvalCompilerMachine.config {C Os R P H D O Aff B Host ClockHost : Type} (prepared : CompilerProviders.Prepared) (image : AllocationImage.Imported) (userRelevantCrates : Array Nat) (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 ABI.ExternAbi ClockHost) :
            Interpreter.ExecutionMachine.Config Memory.MiriMemoryKind (User Os R P H D O Aff B Host) C O ABI.ExternAbi ClockHost

            Compiler binding must precede physical closure: retag/projection/scalar closures capture the same actual vtable/compiler dictionary at construction.

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