1(*
2 * Copyright 2014, General Dynamics C4 Systems
3 *
4 * This software may be distributed and modified according to the terms of
5 * the GNU General Public License version 2. Note that NO WARRANTY is provided.
6 * See "LICENSE_GPLv2.txt" for details.
7 *
8 * @TAG(GD_GPL)
9 *)
10
11theory Hardware_H
12imports
13  "../../machine/X64/MachineOps"
14  State_H
15begin
16
17context Arch begin global_naming X64_H
18
19#INCLUDE_HASKELL SEL4/Machine/Hardware/X64.lhs Platform=Platform.X64 CONTEXT X64_H NOT getMemoryRegions getDeviceRegions getKernelDevices loadWord storeWord storeWordVM getActiveIRQ ackInterrupt maskInterrupt configureTimer resetTimer debugPrint getRestartPC setNextPC clearMemory clearMemoryVM initMemory freeMemory wordFromPDE wordFromPTE VMFaultType HypFaultType VMMapType VMPageSize pageBits pageBitsForSize toPAddr addrFromPPtr ptrFromPAddr setCurrentUserCR3 getCurrentUserCR3 invalidateTLB invalidateTLBEntry mfence wordFromPML4E wordFromPDPTE firstValidIODomain numIODomainIDBits hwASIDInvalidate getFaultAddress irqIntOffset maxPCIBus maxPCIDev maxPCIFunc ioapicIRQLines ioapicMapPinToVector irqStateIRQIOAPICNew irqStateIRQMSINew updateIRQState in8 out8 in16 out16 in32 out32 invalidatePageStructureCache writeCR3 invalidateASID invalidateTranslationSingleASID invalidateLocalPageStructureCacheASID ptTranslationBits nativeThreadUsingFPU switchFpuOwner
20
21end
22
23context begin interpretation Arch .
24requalify_types vmrights
25end
26
27context Arch begin global_naming X64_H
28
29#INCLUDE_HASKELL SEL4/Machine/Hardware/X64.lhs CONTEXT X64_H instanceproofs NOT VMFaultType VMPageSize VMPageEntry VMMapType HypFaultType
30
31#INCLUDE_HASKELL SEL4/Machine/Hardware/X64.lhs CONTEXT X64_H ONLY wordFromPDE wordFromPTE wordFromPML4E wordFromPDPTE
32
33end (* context X64 *)
34
35end
36