adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

x64: add HypFault to machine skel

This commit is contained in:
Joel Beeren 2017-03-14 13:56:18 +11:00
parent a0eb3c6f23
commit 421c42e935
3 changed files with 12 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
spec/design/m-skel/X64/MachineTypes.thy
View File

@ -118,7 +118,7 @@ definition
device_state = empty,
machine_state_rest = undefined \<rparr>"
#INCLUDE_HASKELL SEL4/Machine/Hardware/X64.lhs CONTEXT X64 ONLY HardwareASID VMFaultType VMPageSize pageBits ptTranslationBits pageBitsForSize
#INCLUDE_HASKELL SEL4/Machine/Hardware/X64.lhs CONTEXT X64 ONLY HardwareASID VMFaultType HypFaultType VMPageSize pageBits ptTranslationBits pageBitsForSize
end
@ -128,7 +128,7 @@ end
context Arch begin global_naming X64
#INCLUDE_HASKELL SEL4/Machine/Hardware/X64.lhs CONTEXT X64 instanceproofs ONLY HardwareASID VMFaultType VMPageSize
#INCLUDE_HASKELL SEL4/Machine/Hardware/X64.lhs CONTEXT X64 instanceproofs ONLY HardwareASID VMFaultType HypFaultType VMPageSize
end
end

3
spec/haskell/src/SEL4/Machine/Hardware/X64.lhs
View File

@ -66,6 +66,9 @@ x86 virtual memory faults are handled by one of two trap handlers: one for data
> | X64InstructionFault
> deriving Show
> data HypFaultType
> = X64NoHypFaults
\subsubsection{Physical Memory}
The MMU does not allow access to physical addresses while translation is enabled; the kernel must access its objects via virtual addresses. Depending on the platform, these virtual addresses may either be the same as the physical addresses, or offset by a constant.

14
spec/haskell/src/SEL4/Machine/RegisterSet/X64.lhs
View File

@ -22,9 +22,9 @@ This module defines the x86 64-bit register set.
> data Register =
> RAX | RBX | RCX | RDX | RSI | RDI | RBP |
> R8 | R9 | R10 | R11 | R12 | R13 | R14 | R15 | DS | ES | FS | GS |
> FaultInstruction | -- "FaultIP"
> FaultIP | -- "FaultIP"
> TLS_BASE | PADDING_REGISTER |
> ErrorRegister | NextIP | CS | RFLAGS | RSP | SS
> ErrorRegister | NextIP | CS | FLAGS | RSP | SS
> deriving (Eq, Enum, Bounded, Ord, Ix, Show)
> type Word = Data.Word.Word64
@ -33,11 +33,11 @@ This module defines the x86 64-bit register set.
> msgInfoRegister = RSI
> msgRegisters = [RDI, RBP]
> badgeRegister = capRegister
> frameRegisters = FaultInstruction : RSP : RFLAGS : [RAX .. R15]
> frameRegisters = FaultIP : RSP : FLAGS : [RAX .. R15]
> gpRegisters = [TLS_BASE, FS, GS]
> exceptionMessage = [FaultInstruction, RSP, RFLAGS]
> exceptionMessage = [FaultIP, RSP, FLAGS]
> syscallMessage = [RAX .. RBP] ++ [NextIP, RSP, RFLAGS]
> syscallMessage = [RAX .. RBP] ++ [NextIP, RSP, FLAGS]
> data GDTSlot
> = GDT_NULL
@ -67,12 +67,12 @@ This module defines the x86 64-bit register set.
> initContext :: [(Register, Word)]
> initContext = [(DS, selDS3), (ES, selDS3), (CS, selCS3), (SS, selDS3)
> ,(RFLAGS, bit 9 .|. bit 1)] -- User mode
> ,(FLAGS, bit 9 .|. bit 1)] -- User mode
%FIXME x64: add FPU context
> sanitiseRegister :: Register -> Word -> Word
> sanitiseRegister RFLAGS v =
> sanitiseRegister FLAGS v =
> v .|. bit 1 .&. (complement (bit 3)) .&. (complement (bit 5)) .|. bit 9
> .&. (bit 12 - 1)
> sanitiseRegister FS v = if v /= selTLS && v /= selIPCBUF then 0 else v