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

arm-hyp haskell: use consistent ARMHYP_SMMU tag

This commit is contained in:
Gerwin Klein 2018-07-15 16:59:34 +01:00
parent d860d1e656
commit 807a9792d9
4 changed files with 14 additions and 16 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
spec/haskell/src/SEL4/Kernel/VSpace/ARM.lhs
View File

@ -1327,7 +1327,7 @@ Note that these capabilities cannot be copied until they have been mapped, so an
Virtual page capabilities may each represent a single mapping into a page table. Unlike page table capabilities, they may be unmapped without deletion, and may be freely copied to allow multiple mappings of the same page. Along with the \emph{Map} and \emph{Unmap} operations, there is a \emph{Remap} operation, which is used to change the access permissions on an existing mapping.
FIXME ARMHYP TODO check SMMU isIOSpaceFrameCap(cap) for remap / unmap
FIXME ARMHYP_SMMU check SMMU isIOSpaceFrameCap(cap) for remap / unmap
FIXME ARMHYP TODO add call to ARMPageMapIO decode for map and unmap; remap not allowed
FIXME ARMHYP capVPMappedAddress is not what we want for ARM\_HYP? C code has capFMappedAddress for ARM, capFBasePtr for ARM\_HYP here
@ -1363,7 +1363,7 @@ FIXME ARMHYP capVPMappedAddress is not what we want for ARM\_HYP? C code has cap
> pageMapEntries = entries }
> (ArchInvocationLabel ARMPageMap, _, _) -> throw TruncatedMessage
#ifdef CONFIG_ARM_SMMU
> (ArchInvocationLabel ARMPageMapIO, _, _) -> error "FIXME ARMHYP TODO IO"
> (ArchInvocationLabel ARMPageMapIO, _, _) -> error "FIXME ARMHYP_SMMU"
#endif
> (ArchInvocationLabel ARMPageRemap, rightsMask:attr:_, (pdCap, _):_) -> do
#ifdef CONFIG_ARM_SMMU
@ -1394,7 +1394,7 @@ FIXME ARMHYP capVPMappedAddress is not what we want for ARM\_HYP? C code has cap
> return $
#ifdef CONFIG_ARM_SMMU
> if (isIOSpaceFrameCap cap)
> then error "FIXME ARMHYP TODO IO"
> then error "FIXME ARMHYP_SMMU"
> else
#endif
> InvokePage $ PageUnmap {

2
spec/haskell/src/SEL4/Model/StateData/ARM.lhs
View File

@ -55,7 +55,7 @@ armKSASIDMap to map from page directories to hardware ASIDs.
armKSKernelVSpace is ghost state.
FIXME ARMHYP missing IO ASID to PD map for SMMU
FIXME ARMHYP_SMMU ARMHYP missing IO ASID to PD map for SMMU
> data KernelState = ARMKernelState {
> armKSASIDTable :: Array ASID (Maybe (PPtr ASIDPool)),

2
spec/haskell/src/SEL4/Object/Interrupt/ARM.lhs
View File

@ -43,8 +43,6 @@ This module defines the machine-specific interrupt handling routines.
> checkIRQ :: Word -> KernelF SyscallError ()
> checkIRQ irq = rangeCheck irq (fromEnum minIRQ) (fromEnum maxIRQ)
FIXME ARMHYP INTERRUPT_SMMU
> handleReservedIRQ :: IRQ -> Kernel ()
> handleReservedIRQ irq = do
#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT

20
spec/haskell/src/SEL4/Object/ObjectType/ARM.lhs
View File

@ -70,7 +70,7 @@ ASID capabilities can be copied without modification.
#ifdef CONFIG_ARM_SMMU
> deriveCap _ (c@IOSpaceCap {}) = return $ ArchObjectCap c
> deriveCap _ (c@IOPageTableCap {}) = error "FIXME ARMHYP TODO IO"
> deriveCap _ (c@IOPageTableCap {}) = error "FIXME ARMHYP_SMMU"
#endif /* CONFIG_ARM_SMMU */
> isCapRevocable :: Capability -> Capability -> Bool
@ -131,7 +131,7 @@ Deletion of any mapped frame capability requires the page table slot to be locat
> capVPSize = s, capVPBasePtr = ptr }) _ =
#ifdef CONFIG_ARM_SMMU
> if capVPisIOSpace cap
> then error "FIXME ARMHYP TODO IO"
> then error "FIXME ARMHYP_SMMU"
> else
#endif
> do
@ -145,8 +145,8 @@ Deletion of any mapped frame capability requires the page table slot to be locat
#endif
#ifdef CONFIG_ARM_SMMU
> finaliseCap (IOSpaceCap {}) _ = error "FIXME ARMHYP TODO IOSpace"
> finaliseCap (IOPageTableCap {}) _ = error "FIXME ARMHYP TODO IOSpace" -- IO page directory does not need to be finalised
> finaliseCap (IOSpaceCap {}) _ = error "FIXME ARMHYP_SMMU"
> finaliseCap (IOPageTableCap {}) _ = error "FIXME ARMHYP_SMMU" -- IO page directory does not need to be finalised
#endif
All other capabilities need no finalisation action.
@ -270,7 +270,7 @@ Create an architecture-specific object.
#ifdef CONFIG_ARM_SMMU
> Arch.Types.IOPageTableObject -> do
> let ptSize = ioptBits -- see comment at ioptBits
> error "FIXME ARMHYP TODO IO"
> error "FIXME ARMHYP_SMMU"
#endif
\subsection{Capability Invocation}
@ -284,8 +284,8 @@ Create an architecture-specific object.
> VCPUCap {} -> decodeARMVCPUInvocation label args capIndex slot cap extraCaps
#endif
#ifdef CONFIG_ARM_SMMU
> IOSpaceCap {} -> error "FIXME ARMHYP TODO IOSpace"
> IOPageTableCap {} -> error "FIXME ARMHYP TODO IO"
> IOSpaceCap {} -> error "FIXME ARMHYP_SMMU"
> IOPageTableCap {} -> error "FIXME ARMHYP_SMMU"
#endif
> _ -> decodeARMMMUInvocation label args capIndex slot cap extraCaps
@ -298,9 +298,9 @@ Create an architecture-specific object.
#endif
#ifdef CONFIG_ARM_SMMU
> ArchInv.InvokeIOSpace _ ->
> withoutPreemption $ error "FIXME ARMHYP TODO IOSpace"
> withoutPreemption $ error "FIXME ARMHYP_SMMU"
> ArchInv.InvokeIOPageTable _ ->
> withoutPreemption $ error "FIXME ARMHYP TODO IO"
> withoutPreemption $ error "FIXME ARMHYP_SMMU"
#endif
> _ -> performARMMMUInvocation i
@ -316,7 +316,7 @@ Create an architecture-specific object.
> capUntypedPtr (VCPUCap { capVCPUPtr = PPtr p }) = PPtr p
#endif
#ifdef CONFIG_ARM_SMMU
> capUntypedPtr (IOSpaceCap {}) = error "FIXME ARMHYP TODO IOSpace"
> capUntypedPtr (IOSpaceCap {}) = error "FIXME ARMHYP_SMMU"
> capUntypedPtr (IOPageTableCap { capIOPTBasePtr = PPtr p }) = PPtr p
#endif