common/src/sk-cpu.adb

   1 --
   2 --  Copyright (C) 2013, 2014  Reto Buerki <reet@codelabs.ch>
   3 --  Copyright (C) 2013, 2014  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 System.Machine_Code;
  20
  21 package body SK.CPU
  22 is
  23
  24    --  RDTSC (Read Time-Stamp Counter). The EDX register is loaded with the
  25    --  high-order 32 bits of the TSC MSR and the EAX register is loaded with
  26    --  the low-order 32 bits.
  27    procedure RDTSC
  28      (EAX : out SK.Word32;
  29       EDX : out SK.Word32)
  30    with
  31       Global => (Input => X86_64.State),
  32       Inline_Always;
  33    pragma Annotate (GNATprove, Terminating, RDTSC);
  34
  35    -------------------------------------------------------------------------
  36
  37    procedure Cli
  38    with
  39       SPARK_Mode => Off
  40    is
  41    begin
  42       System.Machine_Code.Asm
  43         (Template => "cli",
  44          Volatile => True);
  45    end Cli;
  46
  47    -------------------------------------------------------------------------
  48
  49    procedure CPUID
  50      (EAX : in out SK.Word32;
  51       EBX :    out SK.Word32;
  52       ECX : in out SK.Word32;
  53       EDX :    out SK.Word32)
  54    with
  55       SPARK_Mode => Off
  56    is
  57    begin
  58       System.Machine_Code.Asm
  59         (Template => "cpuid",
  60          Inputs   => (SK.Word32'Asm_Input ("a", EAX),
  61                       SK.Word32'Asm_Input ("c", ECX)),
  62          Outputs  => (SK.Word32'Asm_Output ("=a", EAX),
  63                       SK.Word32'Asm_Output ("=b", EBX),
  64                       SK.Word32'Asm_Output ("=c", ECX),
  65                       SK.Word32'Asm_Output ("=d", EDX)));
  66    end CPUID;
  67
  68    -------------------------------------------------------------------------
  69
  70    function Get_CR0 return SK.Word64
  71    with
  72       SPARK_Mode => Off
  73    is
  74       Result : SK.Word64;
  75    begin
  76       System.Machine_Code.Asm
  77         (Template => "movq %%cr0, %0",
  78          Outputs  => (SK.Word64'Asm_Output ("=r", Result)),
  79          Volatile => True);
  80       return Result;
  81    end Get_CR0;
  82
  83    -------------------------------------------------------------------------
  84
  85    function Get_CR2 return SK.Word64
  86    with
  87       SPARK_Mode => Off
  88    is
  89       Result : SK.Word64;
  90    begin
  91       System.Machine_Code.Asm
  92         (Template => "movq %%cr2, %0",
  93          Outputs  => (SK.Word64'Asm_Output ("=r", Result)),
  94          Volatile => True);
  95       return Result;
  96    end Get_CR2;
  97
  98    -------------------------------------------------------------------------
  99
 100    function Get_CR3 return SK.Word64
 101    with
 102       SPARK_Mode => Off
 103    is
 104       Result : SK.Word64;
 105    begin
 106       System.Machine_Code.Asm
 107         (Template => "movq %%cr3, %0",
 108          Outputs  => (SK.Word64'Asm_Output ("=r", Result)),
 109          Volatile => True);
 110       return Result;
 111    end Get_CR3;
 112
 113    -------------------------------------------------------------------------
 114
 115    function Get_CR4 return SK.Word64
 116    with
 117       SPARK_Mode => Off
 118    is
 119       Result : SK.Word64;
 120    begin
 121       System.Machine_Code.Asm
 122         (Template => "movq %%cr4, %0",
 123          Outputs  => (SK.Word64'Asm_Output ("=r", Result)),
 124          Volatile => True);
 125       return Result;
 126    end Get_CR4;
 127
 128    -------------------------------------------------------------------------
 129
 130    procedure Get_MSR
 131      (Register :     SK.Word32;
 132       Low      : out SK.Word32;
 133       High     : out SK.Word32)
 134    with
 135       SPARK_Mode => Off
 136    is
 137    begin
 138       System.Machine_Code.Asm
 139         (Template => "rdmsr",
 140          Inputs   => (SK.Word32'Asm_Input ("c", Register)),
 141          Outputs  => (SK.Word32'Asm_Output ("=d", High),
 142                       SK.Word32'Asm_Output ("=a", Low)),
 143          Volatile => True);
 144    end Get_MSR;
 145    pragma Annotate (GNATprove, Terminating, Get_MSR);
 146
 147    -------------------------------------------------------------------------
 148
 149    function Get_MSR64 (Register : SK.Word32) return SK.Word64
 150    is
 151       Low_Dword, High_Dword : SK.Word32;
 152    begin
 153       Get_MSR (Register => Register,
 154                Low      => Low_Dword,
 155                High     => High_Dword);
 156       return 2 ** 32 * SK.Word64 (High_Dword) + SK.Word64 (Low_Dword);
 157    end Get_MSR64;
 158
 159    -------------------------------------------------------------------------
 160
 161    function Get_RFLAGS return SK.Word64
 162    with
 163       SPARK_Mode => Off
 164    is
 165       Result : SK.Word64;
 166    begin
 167       System.Machine_Code.Asm
 168         (Template => "pushf; pop %0",
 169          Outputs  => (SK.Word64'Asm_Output ("=m", Result)),
 170          Volatile => True,
 171          Clobber  => "memory");
 172       return Result;
 173    end Get_RFLAGS;
 174
 175    -------------------------------------------------------------------------
 176
 177    procedure Hlt
 178    with
 179       SPARK_Mode => Off
 180    is
 181    begin
 182       System.Machine_Code.Asm
 183         (Template => "hlt",
 184          Volatile => True);
 185    end Hlt;
 186
 187    -------------------------------------------------------------------------
 188
 189    procedure Lgdt (Descriptor : Pseudo_Descriptor_Type)
 190    with
 191       SPARK_Mode => Off
 192    is
 193    begin
 194       System.Machine_Code.Asm
 195         (Template => "lgdt %0",
 196          Inputs   => (Pseudo_Descriptor_Type'Asm_Input ("m", Descriptor)),
 197          Volatile => True);
 198    end Lgdt;
 199
 200    -------------------------------------------------------------------------
 201
 202    procedure Lidt (Descriptor : Pseudo_Descriptor_Type)
 203    with
 204       SPARK_Mode => Off
 205    is
 206    begin
 207       System.Machine_Code.Asm
 208         (Template => "lidt %0",
 209          Inputs   => (Pseudo_Descriptor_Type'Asm_Input ("m", Descriptor)),
 210          Volatile => True);
 211    end Lidt;
 212
 213    -------------------------------------------------------------------------
 214
 215    procedure Ltr (Address : SK.Word16)
 216    with
 217       SPARK_Mode => Off
 218    is
 219    begin
 220       System.Machine_Code.Asm
 221         (Template => "ltr %%ax",
 222          Inputs   => (SK.Word16'Asm_Input ("a", Address)),
 223          Volatile => True);
 224    end Ltr;
 225
 226    -------------------------------------------------------------------------
 227
 228    procedure Pause
 229    with
 230       SPARK_Mode => Off
 231    is
 232    begin
 233       System.Machine_Code.Asm
 234         (Template => "pause",
 235          Volatile => True);
 236    end Pause;
 237
 238    -------------------------------------------------------------------------
 239
 240    procedure RDTSC
 241      (EAX : out SK.Word32;
 242       EDX : out SK.Word32)
 243    with
 244       SPARK_Mode => Off
 245    is
 246    begin
 247       System.Machine_Code.Asm
 248         (Template => "rdtsc",
 249          Outputs  =>
 250            (SK.Word32'Asm_Output ("=a", EAX),
 251             SK.Word32'Asm_Output ("=d", EDX)),
 252          Volatile => True);
 253    end RDTSC;
 254
 255    -------------------------------------------------------------------------
 256
 257    function RDTSC return SK.Word64
 258    is
 259       Low_Dword, High_Dword : SK.Word32;
 260    begin
 261       RDTSC (EAX => Low_Dword,
 262              EDX => High_Dword);
 263       return 2 ** 32 * SK.Word64 (High_Dword) + SK.Word64 (Low_Dword);
 264    end RDTSC;
 265
 266    -------------------------------------------------------------------------
 267
 268    procedure Set_CR2 (Value : SK.Word64)
 269    with
 270       SPARK_Mode => Off
 271    is
 272    begin
 273       System.Machine_Code.Asm
 274         (Template => "movq %0, %%cr2",
 275          Inputs   => (SK.Word64'Asm_Input ("r", Value)),
 276          Volatile => True);
 277    end Set_CR2;
 278
 279    -------------------------------------------------------------------------
 280
 281    procedure Set_CR4 (Value : SK.Word64)
 282    with
 283       SPARK_Mode => Off
 284    is
 285    begin
 286       System.Machine_Code.Asm
 287         (Template => "movq %0, %%cr4",
 288          Inputs   => (SK.Word64'Asm_Input ("r", Value)),
 289          Volatile => True);
 290    end Set_CR4;
 291
 292    -------------------------------------------------------------------------
 293
 294    procedure Sti
 295    with
 296       SPARK_Mode => Off
 297    is
 298    begin
 299       System.Machine_Code.Asm
 300         (Template => "sti",
 301          Volatile => True);
 302    end Sti;
 303
 304    -------------------------------------------------------------------------
 305
 306    procedure Stop
 307    is
 308    begin
 309       loop
 310          Cli;
 311          Hlt;
 312       end loop;
 313    end Stop;
 314
 315    -------------------------------------------------------------------------
 316
 317    procedure Write_MSR
 318      (Register : SK.Word32;
 319       Low      : SK.Word32;
 320       High     : SK.Word32)
 321    with
 322       SPARK_Mode => Off
 323    is
 324    begin
 325       System.Machine_Code.Asm
 326         (Template => "wrmsr",
 327          Inputs   => (Word32'Asm_Input ("a", Low),
 328                       Word32'Asm_Input ("d", High),
 329                       Word32'Asm_Input ("c", Register)),
 330          Volatile => True);
 331    end Write_MSR;
 332
 333    -------------------------------------------------------------------------
 334
 335    procedure Write_MSR64
 336      (Register : SK.Word32;
 337       Value    : SK.Word64)
 338    is
 339       Low_Dword, High_Dword : SK.Word32;
 340    begin
 341       Low_Dword  := SK.Word32'Mod (Value);
 342       High_Dword := SK.Word32'Mod (Value / 2 ** 32);
 343
 344       Write_MSR (Register => Register,
 345                  Low      => Low_Dword,
 346                  High     => High_Dword);
 347    end Write_MSR64;
 348
 349    -------------------------------------------------------------------------
 350
 351    procedure XGETBV
 352      (Register :     SK.Word32;
 353       Value    : out SK.Word64)
 354    with
 355       SPARK_Mode => Off
 356    is
 357       Low_Dword, High_Dword : SK.Word32;
 358    begin
 359       System.Machine_Code.Asm
 360         (Template => "xgetbv",
 361          Inputs   => Word32'Asm_Input ("c", Register),
 362          Outputs  => (Word32'Asm_Output ("=a", Low_Dword),
 363                       Word32'Asm_Output ("=d", High_Dword)));
 364       Value := Word64 (High_Dword) * 2 ** 32 + Word64 (Low_Dword);
 365    end XGETBV;
 366
 367    -------------------------------------------------------------------------
 368
 369    procedure XRSTOR
 370      (Source : XSAVE_Area_Type;
 371       State  : Word64)
 372    with
 373       SPARK_Mode => Off
 374    is
 375       Low_Dword  : constant Word32 := Word32'Mod (State);
 376       High_Dword : constant Word32 := Word32'Mod (State / 2 ** 32);
 377    begin
 378
 379       --  Restore mask in EDX:EAX specifies to restore x87, SSE and AVX
 380       --  registers, see Intel SDM Vol. 3A, "2.6 Extended Control Registers
 381       --  (Including XCR0)".
 382
 383       System.Machine_Code.Asm
 384         (Template => "xrstor64 %2",
 385          Inputs   => (Word32'Asm_Input ("a", Low_Dword),
 386                       Word32'Asm_Input ("d", High_Dword),
 387                       XSAVE_Area_Type'Asm_Input ("m", Source)),
 388          Volatile => True);
 389    end XRSTOR;
 390
 391    -------------------------------------------------------------------------
 392
 393    procedure XSAVE
 394      (Target : out XSAVE_Area_Type;
 395       State  :     Word64)
 396    with
 397       SPARK_Mode => Off
 398    is
 399       Low_Dword  : constant Word32 := Word32'Mod (State);
 400       High_Dword : constant Word32 := Word32'Mod (State / 2 ** 32);
 401    begin
 402
 403       --  Save mask in EDX:EAX specifies to save x87, SSE and AVX registers,
 404       --  see Intel SDM Vol. 3A, "2.6 Extended Control Registers (Including
 405       --  XCR0)".
 406
 407       System.Machine_Code.Asm
 408         (Template => "xsaveopt64 %0",
 409          Inputs   => (Word32'Asm_Input ("a", Low_Dword),
 410                       Word32'Asm_Input ("d", High_Dword)),
 411          Outputs  => (XSAVE_Area_Type'Asm_Output ("=m", Target)),
 412          Volatile => True);
 413    end XSAVE;
 414
 415    -------------------------------------------------------------------------
 416
 417    procedure XSETBV
 418      (Register : SK.Word32;
 419       Value    : SK.Word64)
 420    with
 421       SPARK_Mode => Off
 422    is
 423       Low_Dword, High_Dword : SK.Word32;
 424    begin
 425       Low_Dword  := SK.Word32'Mod (Value);
 426       High_Dword := SK.Word32'Mod (Value / 2 ** 32);
 427
 428       System.Machine_Code.Asm
 429         (Template => "xsetbv",
 430          Inputs   => (Word32'Asm_Input ("a", Low_Dword),
 431                       Word32'Asm_Input ("d", High_Dword),
 432                       Word32'Asm_Input ("c", Register)),
 433          Volatile => True);
 434    end XSETBV;
 435
 436 end SK.CPU;