common/src/sk-cpu.ads

   1 --
   2 --  Copyright (C) 2013-2016  Reto Buerki <reet@codelabs.ch>
   3 --  Copyright (C) 2013-2016  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 X86_64;
  20
  21 --D @Interface
  22 --D Package providing access to low-level CPU instructions.
  23 package SK.CPU
  24 is
  25
  26    --  Clear Interrupt Flag.
  27    procedure Cli
  28    with
  29       Global  => (In_Out => X86_64.State),
  30       Depends => (X86_64.State =>+ null),
  31       Inline_Always;
  32
  33    --  Execute CPUID instruction.
  34    procedure CPUID
  35      (EAX : in out SK.Word32;
  36       EBX :    out SK.Word32;
  37       ECX : in out SK.Word32;
  38       EDX :    out SK.Word32)
  39    with
  40       Global  => (Input => X86_64.State),
  41       Depends => ((EAX, EBX, ECX, EDX) => (EAX, ECX, X86_64.State)),
  42       Inline_Always;
  43
  44    --  Halt the CPU.
  45    procedure Hlt
  46    with
  47       Global  => (In_Out => X86_64.State),
  48       Depends => (X86_64.State =>+ null),
  49       Inline_Always;
  50
  51    --  Set Interrupt Flag.
  52    procedure Sti
  53    with
  54       Global  => (In_Out => X86_64.State),
  55       Depends => (X86_64.State =>+ null),
  56       Inline_Always;
  57
  58    --  Load Global Descriptor Table (GDT) register.
  59    procedure Lgdt (Descriptor : Pseudo_Descriptor_Type)
  60    with
  61       Global  => (In_Out => X86_64.State),
  62       Depends => (X86_64.State =>+ Descriptor),
  63       Inline_Always;
  64
  65    --  Load Interrupt Descriptor Table (IDT) register.
  66    procedure Lidt (Descriptor : Pseudo_Descriptor_Type)
  67    with
  68       Global  => (In_Out => X86_64.State),
  69       Depends => (X86_64.State =>+ Descriptor),
  70       Inline_Always;
  71
  72    --  Load Task Register (TR).
  73    procedure Ltr (Address : SK.Word16)
  74    with
  75      Global  => (In_Out => X86_64.State),
  76      Depends => (X86_64.State =>+ Address),
  77      Inline_Always;
  78
  79    --  Spin Loop Hint.
  80    procedure Pause
  81    with
  82       Global => null,
  83       Inline_Always;
  84
  85    --  RDTSC (Read Time-Stamp Counter).
  86    function RDTSC return SK.Word64
  87    with
  88       Global => (Input => X86_64.State),
  89       Volatile_Function,
  90       Inline_Always;
  91    pragma Annotate (GNATprove, Terminating, RDTSC);
  92
  93    --  Stop CPU.
  94    procedure Stop
  95    with
  96       Global  => (In_Out => X86_64.State),
  97       Depends => (X86_64.State =>+ null),
  98       Inline_Always,
  99       No_Return;
 100
 101    --  Return current value of CR0 register.
 102    function Get_CR0 return SK.Word64
 103    with
 104       Global  => (Input => X86_64.State),
 105       Volatile_Function,
 106       Inline_Always;
 107    pragma Annotate (GNATprove, Terminating, Get_CR0);
 108
 109    --  Return current value of CR2 register.
 110    function Get_CR2 return SK.Word64
 111    with
 112       Global  => (Input => X86_64.State),
 113       Volatile_Function,
 114       Inline_Always;
 115    pragma Annotate (GNATprove, Terminating, Get_CR2);
 116
 117    --  Return current value of CR3 register.
 118    function Get_CR3 return SK.Word64
 119    with
 120       Global  => (Input => X86_64.State),
 121       Volatile_Function,
 122       Inline_Always;
 123    pragma Annotate (GNATprove, Terminating, Get_CR3);
 124
 125    --  Return current value of CR4 register.
 126    function Get_CR4 return SK.Word64
 127    with
 128       Global  => (Input => X86_64.State),
 129       Volatile_Function,
 130       Inline_Always;
 131    pragma Annotate (GNATprove, Terminating, Get_CR4);
 132
 133       --  Set value of CR2.
 134    procedure Set_CR2 (Value : SK.Word64)
 135    with
 136       Global  => (In_Out => X86_64.State),
 137       Depends => (X86_64.State =>+ Value),
 138       Inline_Always;
 139
 140    --  Set value of CR4.
 141    procedure Set_CR4 (Value : SK.Word64)
 142    with
 143       Global  => (In_Out => X86_64.State),
 144       Depends => (X86_64.State =>+ Value),
 145       Inline_Always;
 146
 147    --  Return current value of given model specific register.
 148    function Get_MSR64 (Register : SK.Word32) return SK.Word64
 149    with
 150       Global  => (Input => X86_64.State),
 151       Volatile_Function,
 152       Inline_Always;
 153    pragma Annotate (GNATprove, Terminating, Get_MSR64);
 154
 155    --  Return value of given MSR as low/high doublewords.
 156    procedure Get_MSR
 157      (Register :     SK.Word32;
 158       Low      : out SK.Word32;
 159       High     : out SK.Word32)
 160    with
 161       Global  => (Input => X86_64.State),
 162       Depends => ((Low, High) => (X86_64.State, Register)),
 163       Inline_Always;
 164
 165    --  Write specified quadword to given MSR.
 166    procedure Write_MSR64
 167      (Register : SK.Word32;
 168       Value    : SK.Word64)
 169    with
 170       Global  => (In_Out => X86_64.State),
 171       Depends => (X86_64.State =>+ (Register, Value)),
 172       Inline_Always;
 173
 174    --  Write specified low/high doublewords to given MSR.
 175    procedure Write_MSR
 176      (Register : SK.Word32;
 177       Low      : SK.Word32;
 178       High     : SK.Word32)
 179    with
 180       Global  => (In_Out => X86_64.State),
 181       Depends => (X86_64.State =>+ (Register, Low, High)),
 182       Inline_Always;
 183
 184    --  Return current RFLAGS.
 185    function Get_RFLAGS return SK.Word64
 186    with
 187       Global  => (Input => X86_64.State),
 188       Volatile_Function,
 189       Inline_Always;
 190    pragma Annotate (GNATprove, Terminating, Get_RFLAGS);
 191
 192    --  Restore specified Processor Extended States from given XSAVE area.
 193    procedure XRSTOR
 194      (Source : XSAVE_Area_Type;
 195       State  : Word64)
 196    with
 197       Global  => (In_Out => X86_64.State),
 198       Depends => (X86_64.State =>+ (Source, State)),
 199       Inline_Always;
 200
 201    --  Save specified Processor Extended States to given XSAVE area.
 202    procedure XSAVE
 203      (Target : out XSAVE_Area_Type;
 204       State  :     Word64)
 205    with
 206       Global  => (Input => X86_64.State),
 207       Depends => (Target => (X86_64.State, State)),
 208       Inline_Always;
 209
 210    --  Get current value of specified Extended Control Register (XCR).
 211    procedure XGETBV
 212      (Register :     SK.Word32;
 213       Value    : out SK.Word64)
 214    with
 215       Global  => (Input => X86_64.State),
 216       Depends => (Value => (X86_64.State, Register)),
 217       Inline_Always;
 218
 219    --  Set specified Extended Control Register (XCR) to given value.
 220    procedure XSETBV
 221      (Register : SK.Word32;
 222       Value    : SK.Word64)
 223    with
 224       Global  => (In_Out => X86_64.State),
 225       Depends => (X86_64.State =>+ (Register, Value)),
 226       Inline_Always;
 227
 228 end SK.CPU;