kernel/src/sk-kernel.adb

   1 --
   2 --  Copyright (C) 2013, 2015  Reto Buerki <reet@codelabs.ch>
   3 --  Copyright (C) 2013, 2015  Adrian-Ken Rueegsegger <ken@codelabs.ch>
   4 --
   5 --  This program is free software: you can redistribute it and/or modify
   6 --  it under the terms of the GNU General Public License as published by
   7 --  the Free Software Foundation, either version 3 of the License, or
   8 --  (at your option) any later version.
   9 --
  10 --  This program is distributed in the hope that it will be useful,
  11 --  but WITHOUT ANY WARRANTY; without even the implied warranty of
  12 --  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  13 --  GNU General Public License for more details.
  14 --
  15 --  You should have received a copy of the GNU General Public License
  16 --  along with this program.  If not, see <http://www.gnu.org/licenses/>.
  17 --
  18
  19 with Skp.Events;
  20 with Skp.Interrupts;
  21 with Skp.Kernel;
  22 with Skp.Subjects;
  23
  24 with SK.Apic;
  25 with SK.Bitops;
  26 with SK.CPU;
  27 with SK.Constants;
  28 with SK.Dump;
  29 with SK.KC;
  30 with SK.Version;
  31 with SK.Power;
  32 with SK.Subjects.Debug;
  33 with SK.System_State;
  34 with SK.VTd.Debug;
  35 with SK.VTd.Interrupts;
  36 with SK.Interrupts;
  37 with SK.Crash_Audit_Types;
  38
  39 pragma $Release_Warnings
  40   (Off, "unit * is not referenced", Reason => "Only used for debug output");
  41 with SK.Strings;
  42 pragma $Release_Warnings (On, "unit * is not referenced");
  43
  44 package body SK.Kernel
  45 is
  46
  47    --  Initialize subject with given ID.
  48    procedure Init_Subject (ID : Skp.Global_Subject_ID_Type)
  49    with
  50       Global =>
  51         (Input  => (CPU_Info.APIC_ID, Interrupt_Tables.State,
  52                     VMX.Exit_Address),
  53          In_Out => (Crash_Audit.State, FPU.State, Subjects.State,
  54                     Subjects_Events.State, Subjects_Interrupts.State,
  55                     Subjects_MSR_Store.State, Timed_Events.State,
  56                     VMX.VMCS_State, X86_64.State));
  57
  58    -------------------------------------------------------------------------
  59
  60    use type Crash_Audit_Types.Reason_Type;
  61
  62    --  Allocate crash audit entry for given error and trigger system restart.
  63    procedure Error
  64      (Reason   : Crash_Audit_Types.Reason_Type;
  65       Subj_Ctx : Crash_Audit_Types.Subj_Context_Type
  66       := Crash_Audit_Types.Null_Subj_Context;
  67       MCE_Ctx  : Crash_Audit_Types.MCE_Context_Type
  68       := Crash_Audit_Types.Null_MCE_Context)
  69    with
  70       Pre => Reason /= Crash_Audit_Types.Reason_Undefined,
  71       No_Return
  72    is
  73       use type Crash_Audit_Types.Subj_Context_Type;
  74       use type Crash_Audit_Types.MCE_Context_Type;
  75
  76       A : Crash_Audit.Entry_Type;
  77    begin
  78       Crash_Audit.Allocate (Audit => A);
  79       Crash_Audit.Set_Reason
  80         (Audit  => A,
  81          Reason => Reason);
  82       if Subj_Ctx /= Crash_Audit_Types.Null_Subj_Context then
  83          Crash_Audit.Set_Subject_Context
  84            (Audit   => A,
  85             Context => Subj_Ctx);
  86       end if;
  87       if MCE_Ctx /= Crash_Audit_Types.Null_MCE_Context then
  88          Crash_Audit.Set_MCE_Context
  89            (Audit   => A,
  90             Context => MCE_Ctx);
  91       end if;
  92       Crash_Audit.Finalize (Audit => A);
  93    end Error;
  94
  95    -------------------------------------------------------------------------
  96
  97    --  Inject pending interrupt into subject identified by ID. Sets interrupt
  98    --  window if interrupt(s) remain pending.
  99    --D @Section Id => impl_inject_interrupt, Label => Interrupt Injection, Parent => impl_exit_handler, Priority => 70
 100    procedure Inject_Interrupt (Subject_ID : Skp.Global_Subject_ID_Type)
 101    with
 102       Global => (Input  => CPU_Info.APIC_ID,
 103                  In_Out => (Crash_Audit.State, Subjects_Interrupts.State,
 104                             Subjects.State, X86_64.State))
 105    is
 106       Vector            : Byte;
 107       Interrupt_Pending : Boolean;
 108    begin
 109       if Subjects.Accepts_Interrupts (ID => Subject_ID) then
 110          --D @Text Section => impl_inject_interrupt, Priority => 10
 111          --D If a subject is ready to accept interrupts, check if it has a
 112          --D pending interrupt.
 113          Subjects_Interrupts.Consume_Interrupt
 114            (Subject => Subject_ID,
 115             Found   => Interrupt_Pending,
 116             Vector  => Vector);
 117
 118          if Interrupt_Pending then
 119             --D @Text Section => impl_inject_interrupt, Priority => 10
 120             --D Consume the pending interrupt by writing the corresponding
 121             --D vector to the VM-entry interruption-information and setting the
 122             --D valid bit, see Intel SDM Vol. 3C, "26.6 Event Injection".
 123             VMX.VMCS_Write
 124               (Field => Constants.VM_ENTRY_INTERRUPT_INFO,
 125                Value => Constants.VM_INTERRUPT_INFO_VALID + Word64 (Vector));
 126
 127             if not Subjects.Is_Running (ID => Subject_ID) then
 128                --D @Text Section => impl_inject_interrupt, Priority => 10
 129                --D If the subject is currently sleeping, then set it to running.
 130                Subjects.Set_Running (ID    => Subject_ID,
 131                                      Value => True);
 132             end if;
 133          end if;
 134       end if;
 135
 136       --D @Text Section => impl_inject_interrupt, Priority => 10
 137       --D Then, check if the subject has more pending interrupts and activate
 138       --D interrupt window exiting if required, see Intel SDM Vol. 3C, "26.7.5
 139       --D Interrupt-Window Exiting and Virtual-Interrupt Delivery".
 140       Interrupt_Pending := Subjects_Interrupts.Has_Pending_Interrupt
 141         (Subject => Subject_ID);
 142       if Interrupt_Pending then
 143          VMX.VMCS_Set_Interrupt_Window (Value => True);
 144       end if;
 145    end Inject_Interrupt;
 146
 147    -------------------------------------------------------------------------
 148
 149    --D @Section Id => impl_handle_target_event, Label => Target Event Handling, Parent => impl_exit_handler, Priority => 60
 150    --D @Text Section => impl_handle_target_event
 151    --D Target events are actions performed prior to resuming execution of a
 152    --D given subject.
 153    procedure Handle_Pending_Target_Event
 154      (Subject_ID : Skp.Global_Subject_ID_Type)
 155    with
 156       Global =>
 157         (Input  => (CPU_Info.APIC_ID, Interrupt_Tables.State,
 158                     VMX.Exit_Address),
 159          In_Out => (Crash_Audit.State, FPU.State, Subjects.State,
 160                     Subjects_Events.State, Subjects_Interrupts.State,
 161                     Subjects_MSR_Store.State, Timed_Events.State,
 162                     VMX.VMCS_State, X86_64.State))
 163    is
 164       Found         : Boolean;
 165       Event_Handled : Boolean := False;
 166       Event_ID      : Skp.Events.Event_Range;
 167    begin
 168       for I in Skp.Events.Event_Range loop
 169          --D @Text Section => impl_handle_target_event
 170          --D First, check if the subject specified by ID has a target event
 171          --D pending by consulting the subject events data.
 172          Subjects_Events.Consume_Event
 173            (Subject => Subject_ID,
 174             Found   => Found,
 175             Event   => Event_ID);
 176
 177          exit when not Found;
 178
 179          Event_Handled := True;
 180
 181          --D @Text Section => impl_handle_target_event
 182          --D If an event is pending, it is consumed by looking up the target
 183          --D event and its action as specified by the policy.
 184          --D @UL Id => impl_handle_target_event_actions, Section => impl_handle_target_event
 185          declare
 186             Cur_Event : constant Skp.Events.Target_Event_Type
 187               := Skp.Events.Get_Target_Event (Subject_ID => Subject_ID,
 188                                               Event_Nr   => Event_ID);
 189          begin
 190             case Skp.Events.Get_Kind (Target_Event => Cur_Event)
 191             is
 192                when Skp.Events.No_Action        => null;
 193                   --D @Item List => impl_handle_target_event_actions
 194                   --D If the designated action is no action, then nothing is
 195                   --D done.
 196                when Skp.Events.Inject_Interrupt =>
 197                   --D @Item List => impl_handle_target_event_actions
 198                   --D If the designated action is interrupt injection, then the
 199                   --D interrupt with the vector specified in the policy is
 200                   --D marked as pending for the subject.
 201                   Subjects_Interrupts.Insert_Interrupt
 202                     (Subject => Subject_ID,
 203                      Vector  => Byte (Skp.Events.Get_Vector
 204                        (Target_Event => Cur_Event)));
 205                when Skp.Events.Reset            =>
 206                   --D @Item List => impl_handle_target_event_actions
 207                   --D If the designated action is subject reset, then the
 208                   --D subject state is initialized, see \ref{impl_subject_init}.
 209                   Init_Subject (ID => Subject_ID);
 210             end case;
 211          end;
 212          --D @Text Section => impl_handle_target_event, Priority => 10
 213          --D At most 64 target events are processed since that is the maximum
 214          --D number of events that can be pending.
 215       end loop;
 216
 217       if Event_Handled and not Subjects.Is_Running (ID => Subject_ID) then
 218          --D @Text Section => impl_handle_target_event, Priority => 10
 219          --D If an event was handled and the subject is currently sleeping, set
 220          --D it to running.
 221          Subjects.Set_Running (ID    => Subject_ID,
 222                                Value => True);
 223       end if;
 224    end Handle_Pending_Target_Event;
 225
 226    -------------------------------------------------------------------------
 227
 228    --D @Section Id => impl_handle_system_panic, Label => System Panic Action Handling, Parent => impl_handle_source_event, Priority => 10
 229    procedure Handle_System_Panic (Subject : Skp.Global_Subject_ID_Type)
 230    with
 231        Global => (Input  => (CPU_Info.APIC_ID, FPU.State, Subjects.State),
 232                   In_Out => (Crash_Audit.State, X86_64.State)),
 233        No_Return
 234    is
 235       S : Crash_Audit_Types.Subj_Context_Type;
 236    begin
 237       --D @Text Section => impl_handle_system_panic
 238       --D A system panic action triggered by a source event of a given subject
 239       --D is handled by creating a crash audit entry with the state of the
 240       --D triggering subject and invoking the crash audit facility.
 241       Subjects.Create_Context (ID  => Subject,
 242                                Ctx => S);
 243       FPU.Get_Registers (ID   => Subject,
 244                          Regs => S.FPU_Registers);
 245       pragma Debug (Dump.Print_Message (Msg => ">>> System Panic triggered"));
 246       pragma Debug (Subjects.Debug.Print_State (S => S));
 247       Error (Reason   => Crash_Audit_Types.Subj_System_Panic,
 248              Subj_Ctx => S);
 249    end Handle_System_Panic;
 250
 251    -------------------------------------------------------------------------
 252
 253    --D @Section Id => impl_handle_source_event, Label => Source Event Handling, Parent => impl_exit_handler, Priority => 50
 254    --D @Text Section => impl_handle_source_event
 255    --D Source events are actions performed when a given subject triggers a trap
 256    --D or a hypercall. Source events can also be triggered by the timed event
 257    --D mechanism. The increment RIP parameter specifies that the RIP of the
 258    --D subject should be incremented if necessary, as part of the event
 259    --D handling (e.g. sleep action).
 260    procedure Handle_Source_Event
 261      (Subject       :     Skp.Global_Subject_ID_Type;
 262       Event         :     Skp.Events.Source_Event_Type;
 263       Increment_RIP :     Boolean;
 264       Next_Subject  : out Skp.Global_Subject_ID_Type)
 265    with
 266       Global =>
 267         (Input  => (CPU_Info.APIC_ID, CPU_Info.CPU_ID, FPU.State,
 268                     Subjects_Interrupts.State,
 269                     Timed_Events.State),
 270          In_Out => (Crash_Audit.State, IO_Apic.State,
 271                     Scheduler.State, Scheduler.Group_Activity_Indicator,
 272                     Subjects.State, Subjects_Events.State, X86_64.State))
 273    is
 274       use type Skp.CPU_Range;
 275       use type Skp.Events.Target_Event_Range;
 276
 277       Dst_CPU : Skp.CPU_Range;
 278    begin
 279       --D @Text Section => impl_handle_source_event
 280       --D \paragraph*{}
 281       --D First, the next subject to be executed is initialized to the current
 282       --D one. A handover event may change this but otherwise the same subject
 283       --D is to be executed next.
 284       Next_Subject := Subject;
 285
 286       --D @Text Section => impl_handle_source_event
 287       --D Then the operation corresponding to the given source event action is
 288       --D performed.
 289       --D @UL Id => impl_handle_source_event_actions, Section => impl_handle_source_event, Priority => 10
 290       case Event.Source_Action
 291       is
 292          when Skp.Events.No_Action       => null;
 293             --D @Item List => impl_handle_source_event_actions
 294             --D If the designated action is no action, then nothing is
 295             --D done.
 296          when Skp.Events.Subject_Sleep   =>
 297             --D @Item List => impl_handle_source_event_actions
 298             --D If the designated action is subject sleep, then a rescheduling
 299             --D of the partition with parameter \verb!Sleep! set to \verb!True!
 300             --D is performed, see \ref{impl_scheduling_resched_sp}.
 301             Scheduler.Reschedule_Partition
 302               (Subject_ID    => Subject,
 303                Increment_RIP => Increment_RIP,
 304                Sleep         => True,
 305                Next_Subject  => Next_Subject);
 306          when Skp.Events.Subject_Yield   =>
 307             --D @Item List => impl_handle_source_event_actions
 308             --D If the designated action is subject yield, then a rescheduling
 309             --D of the partition with parameter \verb!Sleep! set to \verb!False!
 310             --D is performed, see \ref{impl_scheduling_resched_sp}.
 311             Scheduler.Reschedule_Partition
 312               (Subject_ID    => Subject,
 313                Increment_RIP => Increment_RIP,
 314                Sleep         => False,
 315                Next_Subject  => Next_Subject);
 316          when Skp.Events.System_Reboot   =>
 317             --D @Item List => impl_handle_source_event_actions
 318             --D If the designated action is system reboot, then a reboot with
 319             --D power-cycle is initiated.
 320             Power.Reboot (Power_Cycle => True);
 321          when Skp.Events.System_Poweroff =>
 322             --D @Item List => impl_handle_source_event_actions
 323             --D If the designated action is system poweroff, then a shutdown is
 324             --D initiated.
 325             Power.Shutdown;
 326          when Skp.Events.System_Panic =>
 327             --D @Item List => impl_handle_source_event_actions
 328             --D If the designated action is system panic, then the system panic
 329             --D handler is invoked.
 330             Handle_System_Panic (Subject => Subject);
 331          when Skp.Events.Unmask_Irq      =>
 332             --D @Item List => impl_handle_source_event_actions
 333             --D If the designated action is unmask IRQ, then use I/O APIC to
 334             --D unmask the IRQ designated by the event's IRQ number.
 335             IO_Apic.Unmask_IRQ
 336               (RTE_Index => Skp.Interrupts.RTE_Index_Type (Event.IRQ_Number));
 337       end case;
 338
 339       if Event.Target_Subject /= Skp.Invalid_Subject then
 340          if Event.Target_Event /= Skp.Events.Invalid_Target_Event then
 341             --D @Text Section => impl_handle_source_event, Priority => 20
 342             --D If the source event has a valid target subject and target event
 343             --D set, then mark the target event pending for the designated
 344             --D subject.
 345             Subjects_Events.Set_Event_Pending
 346               (Subject  => Event.Target_Subject,
 347                Event_ID => Event.Target_Event);
 348
 349             Dst_CPU := Skp.Subjects.Get_CPU_ID
 350               (Subject_ID => Event.Target_Subject);
 351
 352             --D @Text Section => impl_handle_source_event, Priority => 20
 353             --D Indicate activity for the target subject which may lead to a
 354             --D subject being woken up if it is currently sleeping, see
 355             --D \ref{impl_scheduling_indicate_activity}.
 356             Scheduler.Indicate_Activity
 357               (Subject_ID => Event.Target_Subject,
 358                Same_CPU   => Dst_CPU = CPU_Info.CPU_ID);
 359
 360             if Event.Send_IPI then
 361                --D @Text Section => impl_handle_source_event, Priority => 20
 362                --D Additionally, send an IPI to the CPU running the target
 363                --D subject if specified by the policy.
 364                Apic.Send_IPI (Vector => Constants.IPI_Vector,
 365                               CPU_ID => Dst_CPU);
 366             end if;
 367          end if;
 368
 369          if Event.Handover then
 370             --D @Text Section => impl_handle_source_event, Priority => 20
 371             --D If the source event has a valid target subject and it is a
 372             --D handover event, then set the target subject as the next subject
 373             --D to run.
 374             Next_Subject := Event.Target_Subject;
 375             Scheduler.Set_Current_Subject_ID (Subject_ID => Next_Subject);
 376          end if;
 377       end if;
 378    end Handle_Source_Event;
 379
 380    -------------------------------------------------------------------------
 381
 382    --  Handle hypercall with given event number.
 383    --D @Section Id => hypercall_handling, Label => Hypercall Handling, Parent => impl_exit_handler, Priority => 20
 384    --D @Text Section => hypercall_handling
 385    --D Hypercalls can be triggered by subjects executing the \verb!vmcall!
 386    --D instruction in guest privilege level 0, which is assured by means of a
 387    --D precondition check. If subject user space/ring-3 tries to invoke
 388    --D hypercalls, the VM-Exit is handled as a trap with exit reason
 389    --D \verb!VMCALL!, see \verb!Handle_Trap!.
 390    procedure Handle_Hypercall
 391      (Current_Subject    : Skp.Global_Subject_ID_Type;
 392       Unchecked_Event_Nr : Word64)
 393    with
 394       Global =>
 395         (Input  => (CPU_Info.APIC_ID, CPU_Info.CPU_ID, FPU.State,
 396                     Subjects_Interrupts.State, Timed_Events.State),
 397          In_Out => (Crash_Audit.State, IO_Apic.State, Scheduler.State,
 398                     Scheduler.Group_Activity_Indicator,
 399                     Subjects.State, Subjects_Events.State, X86_64.State)),
 400       Pre    => Subjects.Is_CPL_0 (ID => Current_Subject)
 401    is
 402       --  XXX: Only current wavefronts report that use type clause has no
 403       --       effect. To keep compatibility with earlier toolchains disable
 404       --       all warnings.
 405       pragma $Release_Warnings (Off, -- "use clause for type * has no effect",
 406                                 Reason => "Only used for debug output");
 407       use type Skp.Events.Source_Event_Type;
 408       pragma $Release_Warnings (On);
 409
 410       --  The following code operating on Unchecked_Event_Nr was specifically
 411       --  constructed to defend against Spectre Variant 1 attacks
 412       --  (CVE-2017-5753), i.e. it is important NOT to use the unchecked
 413       --  user-supplied value as index into an array after a conditional
 414       --  checking this variable.
 415
 416       Event_Nr        : constant Skp.Events.Event_Range
 417         := Skp.Events.Event_Range
 418           (Unchecked_Event_Nr and Skp.Events.Event_Mask);
 419       Valid_Event_Nr  : constant Boolean
 420         := Word64 (Event_Nr) = Unchecked_Event_Nr;
 421       Event           : Skp.Events.Source_Event_Type;
 422       Next_Subject_ID : Skp.Global_Subject_ID_Type := Current_Subject;
 423    begin
 424       --D @Text Section => hypercall_handling
 425       --D First the event number of the hypercall is checked. If it is valid
 426       --D then the corresponding subject source event as specified by the
 427       --D policy is looked up and processed, see
 428       --D \ref{impl_handle_source_event}. Note that events that are not
 429       --D specified in the policy are ignored since these are initialized to
 430       --D source events that have no action and an invalid target subject.
 431       if Valid_Event_Nr then
 432          Event := Skp.Events.Get_Source_Event
 433            (Subject_ID => Current_Subject,
 434             Event_Nr   => Event_Nr);
 435          Handle_Source_Event
 436            (Subject       => Current_Subject,
 437             Event         => Event,
 438             Increment_RIP => False,
 439             Next_Subject  => Next_Subject_ID);
 440       end if;
 441
 442       pragma Debug (not Valid_Event_Nr or else
 443                     Event = Skp.Events.Null_Source_Event,
 444                     Dump.Print_Spurious_Event
 445                       (Current_Subject => Current_Subject,
 446                        Event_Nr        => Unchecked_Event_Nr));
 447
 448       --D @Text Section => hypercall_handling
 449       --D After handling the source event, the instruction pointer of the
 450       --D current subject is incremented so execution resumes after the
 451       --D \texttt{vmcall} instruction.
 452       Subjects.Increment_RIP (ID => Current_Subject);
 453
 454       --D @Text Section => hypercall_handling, Priority => 20
 455       --D If the hypercall triggered a handover event, load the new VMCS.
 456       if Current_Subject /= Next_Subject_ID then
 457          VMX.Load (VMCS_Address => Skp.Subjects.Get_VMCS_Address
 458                    (Subject_ID => Next_Subject_ID));
 459       end if;
 460    end Handle_Hypercall;
 461
 462    -------------------------------------------------------------------------
 463
 464    --  Handle external interrupt request with given vector.
 465    --D @Section Id => impl_handle_irq, Label => External Interrupt Handling, Parent => impl_exit_handler, Priority => 10
 466    procedure Handle_Irq (Vector : Byte)
 467    with
 468       Global => (Input  => Scheduler.State,
 469                  In_Out => (IO_Apic.State, Scheduler.Group_Activity_Indicator,
 470                             Subjects_Interrupts.State, X86_64.State))
 471    is
 472       Vect_Nr : Skp.Interrupts.Remapped_Vector_Type;
 473       Route   : Skp.Interrupts.Vector_Route_Type;
 474    begin
 475       --D @Text Section => impl_handle_irq
 476       --D First the vector of the external interrupt is validated. If it is an
 477       --D IPI or VT-d fault vector, no further action is taken since the purpose
 478       --D was to force a VM exit of the currently executing subject. A
 479       --D subsequent subject VM entry leads to the evaluation of pending target
 480       --D events and subject interrupts.
 481       if Vector >= Skp.Interrupts.Remap_Offset
 482         and then Vector < Constants.VTd_Fault_Vector
 483       then
 484          --D @Text Section => impl_handle_irq
 485          --D \paragraph{}
 486          --D If the vector is valid and neither an IPI nor VT-d fault vector,
 487          --D consult the vector routing table to determine the target subject
 488          --D and vector as specified by the policy and insert the target
 489          --D vector by marking it as pending. Note that there is no
 490          --D switching to the destination of the IRQ. The interrupt will be
 491          --D delivered whenever the target subject is executed according to the
 492          --D scheduling plan (i.e. IRQs are not preemptive).
 493          Vect_Nr := Skp.Interrupts.Remapped_Vector_Type (Vector);
 494          Route   := Skp.Interrupts.Vector_Routing (Vect_Nr);
 495          if Route.Subject in Skp.Global_Subject_ID_Type then
 496             Subjects_Interrupts.Insert_Interrupt
 497               (Subject => Route.Subject,
 498                Vector  => Byte (Route.Vector));
 499             --D \paragraph{}
 500             --D Then, indicate activity for the subject in order to make sure
 501             --D that potentially sleeping target subjects are woken up. Note
 502             --D that IRQs are always routed to CPUs executing the target
 503             --D subject.
 504             Scheduler.Indicate_Activity
 505               (Subject_ID => Route.Subject,
 506                Same_CPU   => True);
 507          end if;
 508
 509          --D @Text Section => impl_handle_irq
 510          --D \paragraph{}
 511          --D If the interrupt vector designates an IRQ that must be masked,
 512          --D instruct the I/O APIC to mask the corresponding redirection
 513          --D table entry.
 514          if Vect_Nr in Skp.Interrupts.Mask_IRQ_Type then
 515             IO_Apic.Mask_IRQ
 516               (RTE_Index => Skp.Interrupts.RTE_Index_Type (Vector - 32));
 517          end if;
 518
 519          pragma Debug (Route.Subject not in Skp.Global_Subject_ID_Type,
 520                        Dump.Print_Message
 521                          (Msg => "Spurious IRQ vector "
 522                           & Strings.Img (Vector)));
 523       end if;
 524
 525       pragma Debug (Vector = Constants.VTd_Fault_Vector,
 526                     VTd.Debug.Process_Fault);
 527       pragma Debug (Vector < Skp.Interrupts.Remap_Offset,
 528                     Dump.Print_Message
 529                       (Msg => "IRQ with invalid vector "
 530                        & Strings.Img (Vector)));
 531
 532       --D @Text Section => impl_handle_irq
 533       --D \paragraph{}
 534       --D Finally, signal to the local APIC that the interrupt servicing has
 535       --D completed and other IRQs may be issued once interrupts are re-enabled.
 536       Apic.EOI;
 537    end Handle_Irq;
 538
 539    -------------------------------------------------------------------------
 540
 541    --  Handle Xsetbv trap of current subject by validating new XCR0 value and
 542    --  setting the corresponding register in the associated FPU state.
 543    --D @Section Id => impl_handle_xsetbv, Label => Xsetbv handling, Parent => impl_exit_handler, Priority => 80
 544    procedure Handle_Xsetbv
 545      (Current_Subject : Skp.Global_Subject_ID_Type;
 546       RAX, RDX, RCX   : Word64)
 547    is
 548       Supported : constant Word64 := FPU.Get_Active_XCR0_Features;
 549       Index     : constant Word32 := Word32'Mod (RCX);
 550       New_Value : constant Word64 := Word64 (Word32'Mod (RDX)) * 2 ** 32
 551         + Word64 (Word32'Mod (RAX));
 552    begin
 553       --D @Text Section => impl_handle_xsetbv
 554       --D Subjects can toggle FPU features by writing to XCR0 using the
 555       --D \verb!xsetbv! instruction. The provided value is validated according
 556       --D to Intel SDM Vol. 1,
 557       --D "13.3 Enabling the XSAVE Feature Set and XSAVE-Enabled Features":
 558       --D @OL Id => impl_handle_xsetbv_checks, Section => impl_handle_xsetbv, Priority => 10
 559       --D @Item List => impl_handle_xsetbv_checks
 560       --D Privilege Level (CPL0) must be 0.
 561       if not Subjects.Is_CPL_0 (ID => Current_Subject)
 562         --D @Item List => impl_handle_xsetbv_checks
 563         --D Register index must be 0, only XCR0 is supported.
 564         or else Index /= 0
 565         --D @Item List => impl_handle_xsetbv_checks
 566         --D Only bits that we support must be set.
 567         or else (Supported or New_Value) /= Supported
 568           --D @Item List => impl_handle_xsetbv_checks
 569           --D \verb!XCR0_FPU_STATE_FLAG! must always be set
 570         or else not Bitops.Bit_Test
 571           (Value => New_Value,
 572            Pos   => Constants.XCR0_FPU_STATE_FLAG)
 573         --D @Item List => impl_handle_xsetbv_checks
 574         --D If \verb!XCR0_AVX_STATE_FLAG! is set then \verb!XCR0_SSE_STATE_FLAG!
 575         --D must be set as well.
 576         or else (Bitops.Bit_Test
 577                  (Value => New_Value,
 578                   Pos   => Constants.XCR0_AVX_STATE_FLAG)
 579                  and not Bitops.Bit_Test
 580                    (Value => New_Value,
 581                     Pos   => Constants.XCR0_SSE_STATE_FLAG))
 582         --D @Item List => impl_handle_xsetbv_checks
 583         --D If any of \verb!XCR0_OPMASK_STATE_FLAG! or
 584         --D \verb!XCR0_ZMM_HI256_STATE_FLAG! or \\
 585         --D \verb!XCR0_HI16_ZMM_STATE_FLAG! are set then all must be set.
 586         or else ((Bitops.Bit_Test
 587                   (Value => New_Value,
 588                    Pos   => Constants.XCR0_OPMASK_STATE_FLAG)
 589                   or Bitops.Bit_Test
 590                     (Value => New_Value,
 591                      Pos   => Constants.XCR0_ZMM_HI256_STATE_FLAG)
 592                   or Bitops.Bit_Test
 593                     (Value => New_Value,
 594                      Pos   => Constants.XCR0_ZMM_HI256_STATE_FLAG))
 595                  and not
 596                    (Bitops.Bit_Test
 597                         (Value => New_Value,
 598                          Pos   => Constants.XCR0_OPMASK_STATE_FLAG)
 599                     and Bitops.Bit_Test
 600                       (Value => New_Value,
 601                        Pos   => Constants.XCR0_ZMM_HI256_STATE_FLAG)
 602                     and Bitops.Bit_Test
 603                       (Value => New_Value,
 604                        Pos   => Constants.XCR0_ZMM_HI256_STATE_FLAG)))
 605         --D @Item List => impl_handle_xsetbv_checks
 606         --D If \verb!AVX512! is set then \verb!XCR0_AVX_STATE_FLAG! must be set
 607         --D as well.
 608         or else (Bitops.Bit_Test
 609                  (Value => New_Value,
 610                   Pos   => Constants.XCR0_OPMASK_STATE_FLAG)
 611                  and not Bitops.Bit_Test
 612                    (Value => New_Value,
 613                     Pos   => Constants.XCR0_AVX_STATE_FLAG))
 614       then
 615
 616          --D @Text Section => impl_handle_xsetbv
 617          --D If the value is invalid, inject a \#GP exception. Note that
 618          --D effectively the inserted event has type \emph{external interrupt}.
 619          --D While it would not work in general but in this specific case the
 620          --D exception error code is 0.
 621
 622          Subjects_Interrupts.Insert_Interrupt
 623            (Subject => Current_Subject,
 624             Vector  => Constants.GP_Exception_Vector);
 625       else
 626
 627          --D @Text Section => impl_handle_xsetbv
 628          --D If the value is valid, set the corresponding subject XCR0 value,
 629          --D increment the subject RIP and resume execution.
 630
 631          FPU.Set_XCR0 (ID    => Current_Subject,
 632                        Value => New_Value);
 633          Subjects.Increment_RIP (ID => Current_Subject);
 634       end if;
 635    end Handle_Xsetbv;
 636
 637    -------------------------------------------------------------------------
 638
 639    --D @Section Id => impl_handle_timer_expiry, Label => Timer Expiry, Parent => impl_exit_handler, Priority => 40
 640    --D @Text Section => impl_handle_timer_expiry
 641    --D The VMX timer expiration designates the end of a minor frame. Handle the
 642    --D timer expiry by updating the current scheduling information and checking
 643    --D if a timed event has expired as well.
 644    procedure Handle_Timer_Expiry (Current_Subject : Skp.Global_Subject_ID_Type)
 645      with
 646        Global =>
 647          (Input  => (CPU_Info.APIC_ID, CPU_Info.CPU_ID, CPU_Info.Is_BSP,
 648                      FPU.State, Subjects_Interrupts.State,
 649                      Tau0_Interface.State),
 650           In_Out => (Crash_Audit.State, IO_Apic.State, MP.Barrier,
 651                      Scheduler.State, Scheduler.Group_Activity_Indicator,
 652                      Scheduling_Info.State, Subjects.State,
 653                      Subjects_Events.State, Timed_Events.State, X86_64.State))
 654    is
 655       Next_Subject_ID : Skp.Global_Subject_ID_Type;
 656    begin
 657       Scheduler.Update_Scheduling_Info (Next_Subject => Next_Subject_ID);
 658
 659       --  Check and possibly handle timed event of subject.
 660
 661       declare
 662          Event_Subj    : constant Skp.Global_Subject_ID_Type
 663            := Next_Subject_ID;
 664          Trigger_Value : Word64;
 665          Event_Nr      : Skp.Events.Event_Range;
 666          TSC_Now       : constant Word64 := CPU.RDTSC;
 667       begin
 668
 669          --D @Text Section => impl_handle_timer_expiry, Priority => 20
 670          --D \paragraph{}
 671          --D Check if timed event has expired and handle source event if
 672          --D necessary.
 673          Timed_Events.Get_Event (Subject           => Event_Subj,
 674                                  TSC_Trigger_Value => Trigger_Value,
 675                                  Event_Nr          => Event_Nr);
 676          if Trigger_Value <= TSC_Now then
 677             Handle_Source_Event
 678               (Subject       => Event_Subj,
 679                Event         => Skp.Events.Get_Source_Event
 680                  (Subject_ID => Event_Subj,
 681                   Event_Nr   => Skp.Events.Target_Event_Range (Event_Nr)),
 682                Increment_RIP => False,
 683                Next_Subject  => Next_Subject_ID);
 684             Timed_Events.Clear_Event (Subject => Event_Subj);
 685          end if;
 686       end;
 687
 688       --D @Text Section => impl_handle_timer_expiry, Priority => 20
 689       --D If the new minor frame designates a different subject, load its VMCS.
 690       if Current_Subject /= Next_Subject_ID then
 691
 692          --  New minor frame contains different subject -> Load VMCS.
 693
 694          VMX.Load (VMCS_Address => Skp.Subjects.Get_VMCS_Address
 695                    (Subject_ID => Next_Subject_ID));
 696       end if;
 697    end Handle_Timer_Expiry;
 698
 699    -------------------------------------------------------------------------
 700
 701    --  Handle trap with given number using trap table of current subject.
 702    --D @Section Id => impl_handle_trap, Label => Trap Handling, Parent => impl_exit_handler, Priority => 30
 703    procedure Handle_Trap
 704      (Current_Subject : Skp.Global_Subject_ID_Type;
 705       Trap_Nr         : Word16)
 706    with
 707       Global =>
 708         (Input  => (CPU_Info.APIC_ID, CPU_Info.CPU_ID, FPU.State,
 709                     Subjects_Interrupts.State, Timed_Events.State),
 710          In_Out => (Crash_Audit.State, IO_Apic.State, Scheduler.State,
 711                     Scheduler.Group_Activity_Indicator,
 712                     Subjects.State, Subjects_Events.State, X86_64.State))
 713    is
 714       Trap_Entry      : Skp.Events.Source_Event_Type;
 715       Next_Subject_ID : Skp.Global_Subject_ID_Type;
 716       Valid_Trap_Nr   : Boolean;
 717
 718       ----------------------------------------------------------------------
 719
 720       procedure Panic_Unknown_Trap
 721       with
 722          Global => (Input  => (Current_Subject, CPU_Info.APIC_ID, FPU.State,
 723                                Subjects.State),
 724                     In_Out => (Crash_Audit.State, X86_64.State)),
 725          No_Return
 726       is
 727          S : Crash_Audit_Types.Subj_Context_Type;
 728       begin
 729          Subjects.Create_Context (ID  => Current_Subject,
 730                                   Ctx => S);
 731          FPU.Get_Registers (ID   => Current_Subject,
 732                             Regs => S.FPU_Registers);
 733          pragma Debug (Dump.Print_Message (Msg => ">>> Unknown trap "
 734                                            & Strings.Img (Trap_Nr)));
 735          pragma Debug (Subjects.Debug.Print_State (S => S));
 736          Error (Reason   => Crash_Audit_Types.Subj_Unknown_Trap,
 737                 Subj_Ctx => S);
 738       end Panic_Unknown_Trap;
 739    begin
 740       --D @Text Section => impl_handle_trap
 741       --D First the trap number is checked. If it is outside the valid trap
 742       --D range an appropriate crash audit record is written and an error
 743       --D condition is signaled.
 744       Valid_Trap_Nr := Trap_Nr <= Word16 (Skp.Events.Trap_Range'Last);
 745       if not Valid_Trap_Nr then
 746          Panic_Unknown_Trap;
 747       end if;
 748
 749       --D @Text Section => impl_handle_trap
 750       --D \paragraph{}
 751       --D If the trap number is valid then the corresponding subject trap entry
 752       --D as specified by the policy is looked up. Note that the policy
 753       --D validation tools enforce that an event must be specified for each
 754       --D trap ID.
 755       Trap_Entry := Skp.Events.Get_Trap
 756         (Subject_ID => Current_Subject,
 757          Trap_Nr    => Skp.Events.Trap_Range (Trap_Nr));
 758
 759       --D @Text Section => impl_handle_trap
 760       --D The source event designated by the policy trap entry is processed,
 761       --D see \ref{impl_handle_source_event}.
 762       Handle_Source_Event
 763         (Subject       => Current_Subject,
 764          Event         => Trap_Entry,
 765          Increment_RIP => True,
 766          Next_Subject  => Next_Subject_ID);
 767
 768       --D @Text Section => impl_handle_trap, Priority => 20
 769       --D If the trap triggered a handover event, load the new VMCS.
 770       if Current_Subject /= Next_Subject_ID then
 771          VMX.Load (VMCS_Address => Skp.Subjects.Get_VMCS_Address
 772                    (Subject_ID => Next_Subject_ID));
 773       end if;
 774    end Handle_Trap;
 775
 776    -------------------------------------------------------------------------
 777
 778    --D @Section Id => impl_exit_handler, Label => VMX Exit Handling, Parent => implementation, Priority => -5
 779    --D @Text Section => impl_exit_handler
 780    --D The VMX exit handle procedure \texttt{Handle\_Vmx\_Exit} is the main
 781    --D subprogram of the kernel.
 782    --D It is invoked whenever the execution of a subject stops and an exit into
 783    --D VMX root mode is performed by the hardware. The register state of the
 784    --D current subject is passed to the procedure by the
 785    --D \texttt{vmx\_exit\_handler} assembly code (which is set as kernel entry
 786    --D point/\verb!HOST_RIP! in the VMCS of the trapping subject, see
 787    --D \ref{impl_vmcs_setup_host}).
 788    procedure Handle_Vmx_Exit (Subject_Registers : in out CPU_Registers_Type)
 789    is
 790       --  See Intel SDM Vol. 3C, "27.2.2 Information for VM Exits Due to
 791       --  Vectored Events".
 792       Exception_Mask : constant := 16#07ff#;
 793       Exception_NMI  : constant := 16#0202#;
 794       Exception_MCE  : constant := 16#0312#;
 795
 796       Exit_Reason            : Word64;
 797       Exit_Interruption_Info : Word64;
 798       Basic_Exit_Reason      : Word16;
 799       Current_Subject        : Skp.Global_Subject_ID_Type;
 800    begin
 801       Current_Subject := Scheduler.Get_Current_Subject_ID;
 802
 803       VMX.VMCS_Read (Field => Constants.VMX_EXIT_REASON,
 804                      Value => Exit_Reason);
 805       Basic_Exit_Reason := Word16 (Exit_Reason and 16#ffff#);
 806
 807       --D @Text Section => impl_exit_handler
 808       --D The \texttt{Handle\_Vmx\_Exit} procedure first saves the state of the
 809       --D subject that has just trapped into the exit handler, along with the
 810       --D register values and the exit reason, see
 811       --D \ref{impl_subjects_state_save}.
 812       --D Analogously, the FPU state of the current subject is saved.
 813       Subjects.Save_State (ID          => Current_Subject,
 814                            Exit_Reason => Exit_Reason,
 815                            Regs        => Subject_Registers);
 816
 817       FPU.Save_State (ID => Current_Subject);
 818
 819       VMX.VMCS_Read (Field => Constants.VMX_EXIT_INTR_INFO,
 820                      Value => Exit_Interruption_Info);
 821
 822       --D @Text Section => impl_exit_handler
 823       --D Then, the exit reason is examined and depending on the cause the
 824       --D corresponding handler is called.
 825       --D \paragraph{}
 826       --D If an unrecoverable error occurs, i.e. NMI or MCE, a crash audit
 827       --D record with the appropriate error information is allocated and the
 828       --D kernel performs a controlled system restart.
 829       if Basic_Exit_Reason = Constants.EXIT_REASON_EXTERNAL_INT then
 830          Handle_Irq (Vector => Byte'Mod (Exit_Interruption_Info));
 831       elsif Basic_Exit_Reason = Constants.EXIT_REASON_VMCALL
 832         and then Subjects.Is_CPL_0 (ID => Current_Subject)
 833       then
 834          Handle_Hypercall (Current_Subject    => Current_Subject,
 835                            Unchecked_Event_Nr => Subject_Registers.RAX);
 836       elsif Basic_Exit_Reason = Constants.EXIT_REASON_TIMER_EXPIRY then
 837          Handle_Timer_Expiry (Current_Subject => Current_Subject);
 838       elsif Basic_Exit_Reason = Constants.EXIT_REASON_INTERRUPT_WINDOW then
 839
 840          --  Resume subject to inject pending interrupt.
 841
 842          VMX.VMCS_Set_Interrupt_Window (Value => False);
 843       elsif Basic_Exit_Reason = Constants.EXIT_REASON_EXCEPTION_NMI
 844         and then
 845           (Exit_Interruption_Info and Exception_Mask) = Exception_NMI
 846       then
 847          pragma Debug (Dump.Print_Message
 848                        (Msg => "*** CPU APIC ID " & Strings.Img
 849                         (Byte (CPU_Info.APIC_ID))
 850                         & " VM exit due to NMI; interruption information "
 851                         & Strings.Img (Exit_Interruption_Info)));
 852          Error (Reason => Crash_Audit_Types.Hardware_VMexit_NMI);
 853       elsif Basic_Exit_Reason = Constants.EXIT_REASON_EXCEPTION_NMI
 854         and then (Exit_Interruption_Info and Exception_Mask) = Exception_MCE
 855       then
 856          pragma Debug (Dump.Print_Message
 857                        (Msg => "*** CPU APIC ID " & Strings.Img
 858                         (Byte (CPU_Info.APIC_ID))
 859                         & " VM exit due to MCE; interruption information "
 860                         & Strings.Img (Exit_Interruption_Info)));
 861          declare
 862             Ctx : Crash_Audit_Types.MCE_Context_Type;
 863          begin
 864             MCE.Create_Context (Ctx => Ctx);
 865             Error (Reason  => Crash_Audit_Types.Hardware_VMexit_MCE,
 866                    MCE_Ctx => Ctx);
 867          end;
 868       elsif Basic_Exit_Reason = Constants.EXIT_REASON_ENTRY_FAIL_MCE then
 869          pragma Debug (Dump.Print_Message
 870                        (Msg => "*** CPU APIC ID " & Strings.Img
 871                         (Byte (CPU_Info.APIC_ID))
 872                         & " VM entry failed due to MCE"));
 873          declare
 874             Ctx : Crash_Audit_Types.MCE_Context_Type;
 875          begin
 876             MCE.Create_Context (Ctx => Ctx);
 877             Error (Reason  => Crash_Audit_Types.Hardware_VMentry_MCE,
 878                    MCE_Ctx => Ctx);
 879          end;
 880       elsif Basic_Exit_Reason = Constants.EXIT_REASON_XSETBV then
 881          Handle_Xsetbv (Current_Subject => Current_Subject,
 882                         RAX             => Subject_Registers.RAX,
 883                         RDX             => Subject_Registers.RDX,
 884                         RCX             => Subject_Registers.RCX);
 885       else
 886          Handle_Trap (Current_Subject => Current_Subject,
 887                       Trap_Nr         => Basic_Exit_Reason);
 888       end if;
 889
 890       --D @Text Section => impl_exit_handler
 891       --D \paragraph{}
 892       --D Once the exit has been dealt with, the execution of the next subject
 893       --D is prepared. Pending target events, if present, are handled see
 894       --D \ref{impl_handle_target_event}.
 895       Current_Subject := Scheduler.Get_Current_Subject_ID;
 896       Handle_Pending_Target_Event (Subject_ID => Current_Subject);
 897       --D @Text Section => impl_exit_handler
 898       --D Then, a pending interrupt, if present, is prepared for injection, see
 899       --D \ref{impl_inject_interrupt}.
 900       Inject_Interrupt (Subject_ID => Current_Subject);
 901
 902       --D @Text Section => impl_exit_handler
 903       --D \paragraph{}
 904       --D Finally, the VMX preemption timer is armed, the FPU and subject states
 905       --D are restored, see \ref{impl_subjects_state_restore}. Additionally, to
 906       --D ensure the precondition of \texttt{Subjects.Restore\_State}, the state
 907       --D is filtered beforehand, see \ref{impl_subjects_state_filter}.
 908       Scheduler.Set_VMX_Exit_Timer;
 909       FPU.Restore_State (ID => Current_Subject);
 910       Subjects.Filter_State (ID => Current_Subject);
 911       Subjects.Restore_State
 912         (ID   => Current_Subject,
 913          Regs => Subject_Registers);
 914       --D @Text Section => impl_exit_handler
 915       --D The register values of the subject to be executed are returned by the
 916       --D procedure. The calling assembler code then performs an entry to
 917       --D VMX non-root mode, thereby instructing the hardware to resume
 918       --D execution of the subject designated by the currently active VMCS.
 919    end Handle_Vmx_Exit;
 920
 921    -------------------------------------------------------------------------
 922
 923    --D @Section Id => impl_subject_init, Label => Subject Initialization, Parent => impl_kernel_init_sched, Priority => 20
 924    --D @Text Section => impl_subject_init
 925    --D Clear all state associated with the subject specified by ID and
 926    --D initialize to the values of the subject according to the policy. These
 927    --D steps are performed during startup and whenever a subject is reset.
 928    --D @OL Id => subject_init_steps, Section => impl_subject_init, Priority => 10
 929    procedure Init_Subject (ID : Skp.Global_Subject_ID_Type)
 930    is
 931       Controls  : constant Skp.Subjects.VMX_Controls_Type
 932         := Skp.Subjects.Get_VMX_Controls (Subject_ID => ID);
 933       VMCS_Addr : constant Word64
 934         := Skp.Subjects.Get_VMCS_Address (Subject_ID => ID);
 935       MSR_Count : constant Word32
 936         := Skp.Subjects.Get_MSR_Count (Subject_ID => ID);
 937    begin
 938       --D @Item List => subject_init_steps
 939       --D Reset FPU state for subject with given ID.
 940       FPU.Reset_State (ID => ID);
 941       --D @Item List => subject_init_steps
 942       --D Clear pending events of subject with given ID.
 943       Subjects_Events.Clear_Events (Subject => ID);
 944       --D @Item List => subject_init_steps
 945       --D Initialize pending interrupts of subject with given ID.
 946       Subjects_Interrupts.Init_Interrupts (Subject => ID);
 947       --D @Item List => subject_init_steps
 948       --D Initialize timed event of subject with given ID.
 949       Timed_Events.Init_Event (Subject => ID);
 950
 951       if MSR_Count > 0 then
 952          --D @Item List => subject_init_steps
 953          --D Clear all MSRs in MSR storage area if subject has access to MSRs.
 954          Subjects_MSR_Store.Clear_MSRs (Subject => ID);
 955       end if;
 956
 957       --D @Item List => subject_init_steps
 958       --D Reset VMCS of subject and make it active by loading it.
 959       VMX.Reset (VMCS_Address => VMCS_Addr,
 960                  Subject_ID   => ID);
 961       VMX.Load  (VMCS_Address => VMCS_Addr);
 962       --D @Item List => subject_init_steps
 963       --D Set VMCS control fields according to policy.
 964       VMX.VMCS_Setup_Control_Fields
 965         (IO_Bitmap_Address  => Skp.Subjects.Get_IO_Bitmap_Address
 966            (Subject_ID => ID),
 967          MSR_Bitmap_Address => Skp.Subjects.Get_MSR_Bitmap_Address
 968            (Subject_ID => ID),
 969          MSR_Store_Address  => Skp.Subjects.Get_MSR_Store_Address
 970            (Subject_ID => ID),
 971          MSR_Count          => MSR_Count,
 972          Ctls_Exec_Pin      => Controls.Exec_Pin,
 973          Ctls_Exec_Proc     => Controls.Exec_Proc,
 974          Ctls_Exec_Proc2    => Controls.Exec_Proc2,
 975          Ctls_Exit          => Controls.Exit_Ctrls,
 976          Ctls_Entry         => Controls.Entry_Ctrls,
 977          CR0_Mask           => Skp.Subjects.Get_CR0_Mask
 978            (Subject_ID => ID),
 979          CR4_Mask           => Skp.Subjects.Get_CR4_Mask
 980            (Subject_ID => ID),
 981          Exception_Bitmap   => Skp.Subjects.Get_Exception_Bitmap
 982            (Subject_ID => ID));
 983       --D @Item List => subject_init_steps
 984       --D Setup VMCS host fields.
 985       VMX.VMCS_Setup_Host_Fields;
 986       --D @Item List => subject_init_steps
 987       --D Setup VMCS guest fields according to policy.
 988       VMX.VMCS_Setup_Guest_Fields
 989         (PML4_Address => Skp.Subjects.Get_PML4_Address (Subject_ID => ID),
 990          EPT_Pointer  => Skp.Subjects.Get_EPT_Pointer (Subject_ID => ID));
 991       --D @Item List => subject_init_steps
 992       --D Reset CPU state of subject according to policy.
 993       Subjects.Reset_State
 994         (ID         => ID,
 995          GPRs       => Skp.Subjects.Get_GPRs (Subject_ID => ID),
 996          RIP        => Skp.Subjects.Get_Entry_Point (Subject_ID => ID),
 997          RSP        => Skp.Subjects.Get_Stack_Address (Subject_ID => ID),
 998          CR0        => Skp.Subjects.Get_CR0 (Subject_ID => ID),
 999          CR0_Shadow => Skp.Subjects.Get_CR0_Shadow (Subject_ID => ID),
1000          CR4        => Skp.Subjects.Get_CR4 (Subject_ID => ID),
1001          CR4_Shadow => Skp.Subjects.Get_CR4_Shadow (Subject_ID => ID),
1002          Segments   => Skp.Subjects.Get_Segment_Registers (Subject_ID => ID));
1003    end Init_Subject;
1004
1005    -------------------------------------------------------------------------
1006
1007    procedure Init_Subjects
1008    is
1009       use type Skp.CPU_Range;
1010    begin
1011       --D @Item List => impl_kernel_init_steps, Priority => 10
1012       --D Setup VMCS and state of each subject running on this logical CPU,
1013       --D see \ref{impl_subject_init}.
1014       for I in Skp.Global_Subject_ID_Type loop
1015          if Skp.Subjects.Get_CPU_ID (Subject_ID => I) = CPU_Info.CPU_ID then
1016             Init_Subject (ID => I);
1017          end if;
1018       end loop;
1019    end Init_Subjects;
1020
1021    -------------------------------------------------------------------------
1022
1023    --D @Section Id => impl_kernel_init, Label => Initialization, Parent => implementation, Priority => -10
1024    --D @Text Section => impl_kernel_init
1025    --D The \verb!SK.Kernel.Initialize! procedure is the Ada/SPARK entry point
1026    --D into the kernel during the boot phase. It is invoked from Assembler code
1027    --D after low-level system initialization has been performed.
1028    --D Kernel initialization consists of the following steps:
1029    --D @OL Id => impl_kernel_init_steps, Section => impl_kernel_init, Priority => 10
1030    procedure Initialize (Subject_Registers : out CPU_Registers_Type)
1031    is
1032    begin
1033       --D @Item List => impl_kernel_init_steps
1034       --D Initialize interrupt table (GDT, IDT) and setup interrupt stack.
1035       Interrupt_Tables.Initialize
1036         (Stack_Addr => Skp.Kernel.Intr_Stack_Address);
1037
1038       pragma Debug (CPU_Info.Is_BSP, KC.Init);
1039       pragma Debug (CPU_Info.Is_BSP, KC.Put_Line
1040                     (Item => "Booting Muen kernel "
1041                      & Version.Version_String & " ("
1042                      & Standard'Compiler_Version & ")"));
1043
1044       if CPU_Info.Is_BSP then
1045          --D @Item List => impl_kernel_init_steps
1046          --D Setup crash audit (BSP-only).
1047          Crash_Audit.Init;
1048       end if;
1049
1050       declare
1051          Init_Ctx : Crash_Audit_Types.Init_Context_Type;
1052
1053          Valid_Sys_State, Valid_FPU_State, Valid_MCE_State,
1054          Valid_VTd_State : Boolean;
1055       begin
1056          --D @Item List => impl_kernel_init_steps
1057          --D Validate required CPU (\ref{impl_kernel_init_check_state}),
1058          --D FPU, MCE and VT-d features.
1059          System_State.Check_State
1060            (Is_Valid => Valid_Sys_State,
1061             Ctx      => Init_Ctx.Sys_Ctx);
1062          FPU.Check_State
1063            (Is_Valid => Valid_FPU_State,
1064             Ctx      => Init_Ctx.FPU_Ctx);
1065          MCE.Check_State
1066            (Is_Valid => Valid_MCE_State,
1067             Ctx      => Init_Ctx.MCE_Ctx);
1068          VTd.Check_State
1069            (Is_Valid => Valid_VTd_State,
1070             Ctx      => Init_Ctx.VTd_Ctx);
1071
1072          if not (Valid_Sys_State
1073                  and Valid_FPU_State
1074                  and Valid_MCE_State
1075                  and Valid_VTd_State)
1076          then
1077             declare
1078                Audit_Entry : Crash_Audit.Entry_Type;
1079             begin
1080                pragma Debug (KC.Put_Line
1081                              (Item => "System initialisation error"));
1082
1083                --D @Item List => impl_kernel_init_steps
1084                --D If a required feature is not present, allocate a crash audit
1085                --D entry designating a system initialization failure and
1086                --D provide initialization context information.
1087                Subject_Registers := Null_CPU_Regs;
1088                Crash_Audit.Allocate (Audit => Audit_Entry);
1089                Crash_Audit.Set_Reason
1090                  (Audit  => Audit_Entry,
1091                   Reason => Crash_Audit_Types.System_Init_Failure);
1092                Crash_Audit.Set_Init_Context
1093                  (Audit   => Audit_Entry,
1094                   Context => Init_Ctx);
1095                Crash_Audit.Finalize (Audit => Audit_Entry);
1096             end;
1097          end if;
1098
1099          --D @Item List => impl_kernel_init_steps
1100          --D Enable hardware features (FPU, APIC, MCE).
1101          FPU.Enable;
1102          Apic.Enable;
1103          MCE.Enable;
1104
1105          if CPU_Info.Is_BSP then
1106             --D @Item List => impl_kernel_init_steps
1107             --D Setup of Multicore memory barries (BSP-only).
1108             MP.Initialize_All_Barrier;
1109
1110             --D @Item List => impl_kernel_init_steps
1111             --D Disable legacy PIC/PIT (BSP-only).
1112             Interrupts.Disable_Legacy_PIT;
1113             Interrupts.Disable_Legacy_PIC;
1114
1115             --D @Item List => impl_kernel_init_steps
1116             --D Setup of VT-d DMAR and IR (BSP-only).
1117             VTd.Initialize;
1118             VTd.Interrupts.Setup_IRQ_Routing;
1119
1120             --D @Item List => impl_kernel_init_steps
1121             --D Initialize subject pending events (BSP-only).
1122             Subjects_Events.Initialize;
1123
1124             --D @Item List => impl_kernel_init_steps
1125             --D Wake up application processors (BSP-only).
1126             Apic.Start_AP_Processors;
1127          end if;
1128
1129          --D @Item List => impl_kernel_init_steps
1130          --D Synchronize all CPUs to make sure APs have performed all steps up
1131          --D until this point.
1132          MP.Wait_For_All;
1133
1134          --D @Item List => impl_kernel_init_steps
1135          --D Perform Intel microcode update on all cores. This is only done
1136          --D if the policy specifies an MCU blob.
1137          MCU.Process;
1138
1139          --D @Item List => impl_kernel_init_steps
1140          --D Enable VMX and enter VMX root-mode.
1141          System_State.Enable_VMX_Feature;
1142          VMX.Enter_Root_Mode;
1143          Init_Subjects;
1144
1145          --D @Item List => impl_kernel_init_steps, Priority => 20
1146          --D Finish setup by initializing the scheduler.
1147          Scheduler.Init;
1148
1149          --D @Item List => impl_kernel_init_steps, Priority => 20
1150          --D Synchronize all logical CPUs prior to setting VMX preemption
1151          --D timer.
1152          MP.Wait_For_All;
1153
1154          --D @Item List => impl_kernel_init_steps, Priority => 20
1155          --D Arm VMX Exit timer of scheduler for preemption on end of initial
1156          --D minor frame.
1157          Scheduler.Set_VMX_Exit_Timer;
1158
1159          declare
1160             Current_Subject : constant Skp.Global_Subject_ID_Type
1161               := Scheduler.Get_Current_Subject_ID;
1162          begin
1163             --D @Item List => impl_kernel_init_steps, Priority => 20
1164             --D Prepare state of initial subject for execution.
1165             Subjects.Filter_State (ID => Current_Subject);
1166             Subjects.Restore_State
1167               (ID   => Current_Subject,
1168                Regs => Subject_Registers);
1169             FPU.Restore_State (ID => Current_Subject);
1170          end;
1171       end;
1172
1173       --D @Text Section => impl_kernel_init, Priority => 30
1174       --D Registers of the first subject to schedule are returned by the
1175       --D initialization procedure to the calling assembler code. The assembly
1176       --D then restores the subject register values prior to launching the first
1177       --D subject.
1178       --D This is done this way so the initialization code as well as the main
1179       --D VMX exit handler (\ref{impl_exit_handler}) operate the same way and
1180       --D the Assembler code in charge of resuming subject execution can be
1181       --D shared, which further simplifies the code flow.
1182    end Initialize;
1183
1184 end SK.Kernel;