kernel/src/sk-kernel.ads

   1 --
   2 --  Copyright (C) 2013  Reto Buerki <reet@codelabs.ch>
   3 --  Copyright (C) 2013  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.IOMMU;
  20
  21 with X86_64;
  22
  23 with SK.CPU_Info;
  24 with SK.FPU;
  25 with SK.Interrupt_Tables;
  26 with SK.IO_Apic;
  27 with SK.MCE;
  28 with SK.MP;
  29 with SK.Scheduler;
  30 with SK.Scheduling_Info;
  31 with SK.Subjects;
  32 with SK.Subjects_Events;
  33 with SK.Subjects_Interrupts;
  34 with SK.Subjects_MSR_Store;
  35 with SK.Tau0_Interface;
  36 with SK.Timed_Events;
  37 with SK.VMX;
  38 with SK.Crash_Audit;
  39 with SK.MCU;
  40
  41 --D @Interface
  42 --D This package implements kernel initialization which is the initial entry
  43 --D point from the early boot code into the SPARK kernel implementation. It
  44 --D also contains the VM exit handler procedure which implements the main
  45 --D kernel processing loop.
  46 package SK.Kernel
  47 is
  48
  49    --  Kernel initialization.
  50    procedure Initialize (Subject_Registers : out CPU_Registers_Type)
  51    with
  52       Global =>
  53         (Input  => (CPU_Info.APIC_ID, CPU_Info.CPU_ID, CPU_Info.Is_BSP,
  54                     MCE.State, VMX.Exit_Address, MCU.State),
  55          In_Out => (Crash_Audit.State, FPU.State, Interrupt_Tables.State,
  56                     IO_Apic.State, MP.Barrier, Scheduler.State,
  57                     Scheduling_Info.State, Subjects.State,
  58                     Subjects_Events.State, Subjects_Interrupts.State,
  59                     Subjects_MSR_Store.State, Timed_Events.State,
  60                     VMX.VMCS_State, Skp.IOMMU.State, X86_64.State)),
  61       Post   => MCE.Valid_State,
  62       Export,
  63       Convention => C,
  64       Link_Name  => "sk_initialize";
  65
  66    --  VMX exit handler.
  67    procedure Handle_Vmx_Exit (Subject_Registers : in out CPU_Registers_Type)
  68    with
  69       Global     =>
  70          (Input  => (CPU_Info.APIC_ID, CPU_Info.CPU_ID, CPU_Info.Is_BSP,
  71                      Interrupt_Tables.State, MCE.State, Tau0_Interface.State,
  72                      VMX.Exit_Address),
  73           In_Out => (Crash_Audit.State, FPU.State, IO_Apic.State, MP.Barrier,
  74                      Scheduler.State, Scheduler.Group_Activity_Indicator,
  75                      Subjects.State, Scheduling_Info.State,
  76                      Subjects_Events.State, Subjects_Interrupts.State,
  77                      Subjects_MSR_Store.State, Timed_Events.State,
  78                      VMX.VMCS_State, X86_64.State)),
  79       Pre        => MCE.Valid_State,
  80       Export,
  81       Convention => C,
  82       Link_Name  => "handle_vmx_exit";
  83
  84 end SK.Kernel;