rt haskell: set handler params when configuring TCBs

Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
seL4 · Aug 16, 2022 · f894caa · f894caa
1 parent af08a1c
commit f894caa
Show file tree

Hide file tree

Showing 3 changed files with 34 additions and 19 deletions.
diff --git a/spec/design/skel/Structures_H.thy b/spec/design/skel/Structures_H.thy
@@ -41,8 +41,8 @@ requalify_consts
 
 end
 
-#INCLUDE_HASKELL SEL4/Object/Structures.lhs decls_only NOT isNullCap isUntypedCap isIRQControlCap isReplyCap isDomainCap isNotificationCap isThreadCap isSchedContextCap scBitsFromRefillLength scBitsFromRefillLength' objBitsKO
-#INCLUDE_HASKELL SEL4/Object/Structures.lhs bodies_only NOT kernelObjectTypeName isNullCap isUntypedCap isIRQControlCap isReplyCap isDomainCap isNotificationCap isThreadCap isSchedContextCap scBitsFromRefillLength' scBitsFromRefillLength objBitsKO
+#INCLUDE_HASKELL SEL4/Object/Structures.lhs decls_only NOT isNullCap isUntypedCap isIRQControlCap isReplyCap isDomainCap isNotificationCap isEndpointCap isThreadCap isSchedContextCap scBitsFromRefillLength scBitsFromRefillLength' objBitsKO
+#INCLUDE_HASKELL SEL4/Object/Structures.lhs bodies_only NOT kernelObjectTypeName isNullCap isUntypedCap isIRQControlCap isReplyCap isDomainCap isNotificationCap isEndpointCap isThreadCap isSchedContextCap scBitsFromRefillLength' scBitsFromRefillLength objBitsKO
 
 definition scBitsFromRefillLength' :: "nat => nat"
 where

diff --git a/spec/haskell/src/SEL4/Object/Structures.lhs b/spec/haskell/src/SEL4/Object/Structures.lhs
@@ -119,6 +119,10 @@ This is the type used to represent a capability.
 > isNotificationCap (NotificationCap {}) = True
 > isNotificationCap _ = False
 
+> isEndpointCap :: Capability -> Bool
+> isEndpointCap (EndpointCap {}) = True
+> isEndpointCap _ = False
+
 > isSchedContextCap :: Capability -> Bool
 > isSchedContextCap (SchedContextCap {}) = True
 > isSchedContextCap _ = False

diff --git a/spec/haskell/src/SEL4/Object/TCB.lhs b/spec/haskell/src/SEL4/Object/TCB.lhs
@@ -87,7 +87,7 @@ There are eleven types of invocation for a thread control block. All require wri
 >         TCBSetMCPriority -> decodeSetMCPriority args cap extraCaps
 >         TCBSetSchedParams -> decodeSetSchedParams args cap slot extraCaps
 >         TCBSetIPCBuffer -> decodeSetIPCBuffer args cap slot extraCaps
->         TCBSetTimeoutEndpoint -> decodeSetTimeoutEndpoint cap slot extraCaps
+>         TCBSetTimeoutEndpoint -> decodeSetTimeoutEndpoint args cap slot extraCaps
 >         TCBSetSpace -> decodeSetSpace args cap slot extraCaps
 >         TCBBindNotification -> decodeBindNotification cap extraCaps
 >         TCBUnbindNotification -> decodeUnbindNotification cap
@@ -256,7 +256,7 @@ The "SetSchedParams" call sets both the priority and the MCP in a single call.
 
 > decodeSetSchedParams :: [Word] -> Capability -> PPtr CTE -> [(Capability, PPtr CTE)] ->
 >         KernelF SyscallError TCBInvocation
-> decodeSetSchedParams (newMCP : newPrio : _) cap slot ((authCap, _) : (scCap, _) : (fhCap, fhSlot) : _) = do
+> decodeSetSchedParams (newMCP:newPrio:fhData:fhRights:_) cap slot ((authCap, _):(scCap, _):fhArg:_) = do
 >     authTCB <- case authCap of
 >         ThreadCap { capTCBPtr = tcbPtr } -> return tcbPtr
 >         _ -> throw $ InvalidCapability 1
@@ -280,11 +280,11 @@ The "SetSchedParams" call sets both the priority and the MCP in a single call.
 >             when (tcbPtr == curTcbPtr) $ throw IllegalOperation
 >             return Nothing
 >         _ -> throw $ InvalidCapability 2
->     when (not $ isValidFaultHandler fhCap) $ throw $ InvalidCapability 3
+>     faultHandler <- updateAndCheckHandlerEP [fhData,fhRights] 3 [fhArg]
 >     return $ ThreadControlSched {
 >         tcSchedTarget = tcbPtr,
 >         tcSchedSlot = slot,
->         tcSchedFaultHandler = Just (fhCap, fhSlot),
+>         tcSchedFaultHandler = Just faultHandler,
 >         tcSchedMCPriority = Just (fromIntegral newMCP, authTCB),
 >         tcSchedPriority = Just (fromIntegral newPrio, authTCB),
 >         tcSchedSchedContext = Just scPtr }
@@ -352,14 +352,29 @@ This is to ensure that the source capability is not made invalid by the deletion
 >         tcCapsBuffer = Nothing }
 > decodeCVSpace _ _ _ _ = throw TruncatedMessage
 
+> updateAndCheckHandlerEP :: [Word] -> Int -> [(Capability, PPtr CTE)] ->
+>         KernelF SyscallError (Capability, PPtr CTE)
+> updateAndCheckHandlerEP (fhData:fhRights:_) pos ((fhCap, fhSlot):_) = do
+>     unless (isEndpointCap fhCap || isNullCap fhCap) $ throw $ InvalidCapability pos
+>     fhCap' <- if fhData /= 0
+>         then do
+>             let fhDataCap = updateCapData False fhData fhCap
+>             when (isNullCap fhDataCap) $ throw IllegalOperation
+>             return fhDataCap
+>         else return fhCap
+>     fhCap'' <- if fhRights /= 0
+>         then return $ maskCapRights (rightsFromWord fhRights) fhCap'
+>         else return fhCap'
+>     fhCap''' <- deriveCap fhSlot fhCap''
+>     unless (isValidFaultHandler fhCap''') $ throw $ InvalidCapability pos
+>     return (fhCap''', fhSlot)
+> updateAndCheckHandlerEP _ _ _ = throw TruncatedMessage
+
 > decodeSetSpace :: [Word] -> Capability -> PPtr CTE ->
 >         [(Capability, PPtr CTE)] -> KernelF SyscallError TCBInvocation
-> decodeSetSpace (cRootData:vRootData:_) cap slot (fhArg:cRootArg:vRootArg:_) = do
+> decodeSetSpace (fhData:fhRights:cRootData:vRootData:_) cap slot (fhArg:cRootArg:vRootArg:_) = do
 >     space <- decodeCVSpace [cRootData,vRootData] cap slot [cRootArg,vRootArg]
->     let (fhCap, fhSlot) = fhArg
->     faultHandler <- if isValidFaultHandler fhCap
->         then return (fhCap, fhSlot)
->         else throw $ InvalidCapability 1
+>     faultHandler <- updateAndCheckHandlerEP [fhData,fhRights] 1 [fhArg]
 >     return $ ThreadControlCaps {
 >         tcCapsTarget = capTCBPtr cap,
 >         tcCapsSlot = slot,
@@ -370,18 +385,14 @@ This is to ensure that the source capability is not made invalid by the deletion
 >         tcCapsBuffer = Nothing }
 > decodeSetSpace _ _ _ _ = throw TruncatedMessage
 
-> decodeSetTimeoutEndpoint :: Capability -> PPtr CTE ->
+> decodeSetTimeoutEndpoint :: [Word] -> Capability -> PPtr CTE ->
 >         [(Capability, PPtr CTE)] -> KernelF SyscallError TCBInvocation
-> decodeSetTimeoutEndpoint cap slot (thArg:_)
->         = do
->     let (thCap, thSlot) = thArg
->     timeoutHandler <- if isValidFaultHandler thCap
->         then return (thCap, thSlot)
->         else throw $ InvalidCapability 1
+> decodeSetTimeoutEndpoint (thData:thRights:_) cap slot (thArg:_) = do
+>     timeoutHandler <- updateAndCheckHandlerEP [thData,thRights] 1 [thArg]
 >     return $ (emptyTCCaps $ capTCBPtr cap) {
 >         tcCapsSlot = slot,
 >         tcCapsTimeoutHandler = Just timeoutHandler }
-> decodeSetTimeoutEndpoint _ _ _ = throw TruncatedMessage
+> decodeSetTimeoutEndpoint _ _ _ _ = throw TruncatedMessage
 
 \subsubsection{Decode Bound Notification Invocations}