spec: add SetTLSBase invocation and update the registers (VER-807)
This commit is contained in:
Corey Lewis
parent
05281b90fe
commit
2b8a2ebfbe
|
|
@ -381,6 +381,14 @@ where
|
|||
odE
|
||||
| _ \<Rightarrow> throwError IllegalOperation"
|
||||
|
||||
definition
|
||||
decode_set_tls_base :: "data list \<Rightarrow> cap \<Rightarrow> (tcb_invocation,'z::state_ext) se_monad"
|
||||
where
|
||||
"decode_set_tls_base args cap \<equiv> doE
|
||||
whenE (length args = 0) $ throwError TruncatedMessage;
|
||||
returnOk (SetTLSBase (obj_ref_of cap) (ucast (args ! 0)))
|
||||
odE"
|
||||
|
||||
definition
|
||||
decode_tcb_invocation ::
|
||||
"data \<Rightarrow> data list \<Rightarrow> cap \<Rightarrow> cslot_ptr \<Rightarrow> (cap \<times> cslot_ptr) list \<Rightarrow>
|
||||
|
|
@ -401,6 +409,7 @@ where
|
|||
| TCBSetSpace \<Rightarrow> decode_set_space args cap slot excs
|
||||
| TCBBindNotification \<Rightarrow> decode_bind_notification cap excs
|
||||
| TCBUnbindNotification \<Rightarrow> decode_unbind_notification cap
|
||||
| TCBSetTLSBase \<Rightarrow> decode_set_tls_base args cap
|
||||
| _ \<Rightarrow> throwError IllegalOperation"
|
||||
|
||||
definition
|
||||
|
|
|
|||
|
|
@ -59,6 +59,7 @@ datatype tcb_invocation =
|
|||
| Suspend "obj_ref"
|
||||
| Resume "obj_ref"
|
||||
| NotificationControl "obj_ref" "obj_ref option"
|
||||
| SetTLSBase obj_ref machine_word
|
||||
|
||||
datatype irq_control_invocation =
|
||||
IRQControl irq cslot_ptr cslot_ptr
|
||||
|
|
|
|||
|
|
@ -252,6 +252,14 @@ where
|
|||
return []
|
||||
od)"
|
||||
|
||||
| "invoke_tcb (SetTLSBase tcb tls_base) =
|
||||
(liftE $ do
|
||||
as_user tcb $ setRegister tlsBaseRegister tls_base;
|
||||
cur \<leftarrow> gets cur_thread;
|
||||
when (tcb = cur) (do_extended_op reschedule_required);
|
||||
return []
|
||||
od)"
|
||||
|
||||
definition
|
||||
set_domain :: "obj_ref \<Rightarrow> domain \<Rightarrow> unit det_ext_monad" where
|
||||
"set_domain tptr new_dom \<equiv> do
|
||||
|
|
|
|||
|
|
@ -119,6 +119,8 @@ datatype cdl_tcb_intent =
|
|||
| TcbBindNTFNIntent
|
||||
(* UnbindNTFN: (target) *)
|
||||
| TcbUnbindNTFNIntent
|
||||
(* SetTLSBase: (target) *)
|
||||
| TcbSetTLSBaseIntent
|
||||
|
||||
datatype cdl_untyped_intent =
|
||||
(* Retype: (target), (do_reset), type, size_bits, (root), node_index, node_depth, node_offset, node_window, has_children *)
|
||||
|
|
|
|||
|
|
@ -37,6 +37,7 @@ datatype cdl_tcb_invocation =
|
|||
| Suspend cdl_object_id
|
||||
| Resume cdl_object_id
|
||||
| NotificationControl cdl_object_id "cdl_object_id option"
|
||||
| SetTLSBase cdl_object_id
|
||||
|
||||
datatype cdl_irq_control_invocation =
|
||||
IssueIrqHandler cdl_irq cdl_cap_ref cdl_cap_ref
|
||||
|
|
|
|||
|
|
@ -135,6 +135,7 @@ where
|
|||
returnOk (NotificationControl (cap_object target) (Some (cap_object ntfn_cap)))
|
||||
odE \<sqinter> throw
|
||||
| TcbUnbindNTFNIntent \<Rightarrow> returnOk (NotificationControl (cap_object target) None) \<sqinter> throw
|
||||
| TCBSetTLSBaseIntent \<Rightarrow> returnOk (SetTLSBase (cap_object target)) \<sqinter> throw
|
||||
"
|
||||
|
||||
|
||||
|
|
@ -298,7 +299,8 @@ where
|
|||
| NotificationControl tcb ntfn \<Rightarrow>
|
||||
liftE $ (case ntfn of
|
||||
Some ntfn_id \<Rightarrow> bind_notification tcb ntfn_id
|
||||
| None \<Rightarrow> unbind_notification tcb)"
|
||||
| None \<Rightarrow> unbind_notification tcb)
|
||||
| SetTLSBase tcb \<Rightarrow> liftE $ corrupt_tcb_intent tcb"
|
||||
|
||||
|
||||
definition
|
||||
|
|
|
|||
|
|
@ -36,6 +36,7 @@ requalify_consts
|
|||
fromVPtr
|
||||
setTCBIPCBuffer
|
||||
postModifyRegisters
|
||||
tlsBaseRegister
|
||||
end
|
||||
|
||||
abbreviation "mapMaybe \<equiv> option_map"
|
||||
|
|
|
|||
|
|
@ -83,6 +83,9 @@ The following data type defines the set of possible TCB invocation operations. T
|
|||
> copyRegsSuspendSource, copyRegsResumeTarget :: Bool,
|
||||
> copyRegsTransferFrame, copyRegsTransferInteger :: Bool,
|
||||
> copyRegsTransferArch :: Arch.CopyRegisterSets }
|
||||
> | SetTLSBase {
|
||||
> setTLSBaseTCB :: PPtr TCB,
|
||||
> setTLSBaseNewBase :: Word }
|
||||
> deriving Show
|
||||
|
||||
\subsubsection{CNode Invocations}
|
||||
|
|
|
|||
|
|
@ -47,6 +47,7 @@ The following type enumerates all the kinds of invocations that clients can requ
|
|||
> | TCBResume
|
||||
> | TCBBindNotification
|
||||
> | TCBUnbindNotification
|
||||
> | TCBSetTLSBase
|
||||
> | CNodeRevoke
|
||||
> | CNodeDelete
|
||||
> | CNodeCancelBadgedSends
|
||||
|
|
@ -85,22 +86,23 @@ The following type enumerates all the kinds of invocations that clients can requ
|
|||
> TCBResume -> 12
|
||||
> TCBBindNotification -> 13
|
||||
> TCBUnbindNotification -> 14
|
||||
> CNodeRevoke -> 15
|
||||
> CNodeDelete -> 16
|
||||
> CNodeCancelBadgedSends -> 17
|
||||
> CNodeCopy -> 18
|
||||
> CNodeMint -> 19
|
||||
> CNodeMove -> 20
|
||||
> CNodeMutate -> 21
|
||||
> CNodeRotate -> 22
|
||||
> CNodeSaveCaller -> 23
|
||||
> IRQIssueIRQHandler -> 24
|
||||
> IRQAckIRQ -> 25
|
||||
> IRQSetIRQHandler -> 26
|
||||
> IRQClearIRQHandler -> 27
|
||||
> TCBSetTLSBase -> 15
|
||||
> CNodeRevoke -> 16
|
||||
> CNodeDelete -> 17
|
||||
> CNodeCancelBadgedSends -> 18
|
||||
> CNodeCopy -> 19
|
||||
> CNodeMint -> 20
|
||||
> CNodeMove -> 21
|
||||
> CNodeMutate -> 22
|
||||
> CNodeRotate -> 23
|
||||
> CNodeSaveCaller -> 24
|
||||
> IRQIssueIRQHandler -> 25
|
||||
> IRQAckIRQ -> 26
|
||||
> IRQSetIRQHandler -> 27
|
||||
> IRQClearIRQHandler -> 28
|
||||
> DomainSetSet -> apiMax
|
||||
> ArchInvocationLabel a -> apiMax + 1 + fromEnum a
|
||||
> where apiMax = 28
|
||||
> where apiMax = 29
|
||||
> toEnum n
|
||||
> | n == 0 = InvalidInvocation
|
||||
> | n == 1 = UntypedRetype
|
||||
|
|
@ -117,23 +119,24 @@ The following type enumerates all the kinds of invocations that clients can requ
|
|||
> | n == 12 = TCBResume
|
||||
> | n == 13 = TCBBindNotification
|
||||
> | n == 14 = TCBUnbindNotification
|
||||
> | n == 15 = CNodeRevoke
|
||||
> | n == 16 = CNodeDelete
|
||||
> | n == 17 = CNodeCancelBadgedSends
|
||||
> | n == 18 = CNodeCopy
|
||||
> | n == 19 = CNodeMint
|
||||
> | n == 20 = CNodeMove
|
||||
> | n == 21 = CNodeMutate
|
||||
> | n == 22 = CNodeRotate
|
||||
> | n == 23 = CNodeSaveCaller
|
||||
> | n == 24 = IRQIssueIRQHandler
|
||||
> | n == 25 = IRQAckIRQ
|
||||
> | n == 26 = IRQSetIRQHandler
|
||||
> | n == 27 = IRQClearIRQHandler
|
||||
> | n == 28 = DomainSetSet
|
||||
> | n == 15 = TCBSetTLSBase
|
||||
> | n == 16 = CNodeRevoke
|
||||
> | n == 17 = CNodeDelete
|
||||
> | n == 18 = CNodeCancelBadgedSends
|
||||
> | n == 19 = CNodeCopy
|
||||
> | n == 20 = CNodeMint
|
||||
> | n == 21 = CNodeMove
|
||||
> | n == 22 = CNodeMutate
|
||||
> | n == 23 = CNodeRotate
|
||||
> | n == 24 = CNodeSaveCaller
|
||||
> | n == 25 = IRQIssueIRQHandler
|
||||
> | n == 26 = IRQAckIRQ
|
||||
> | n == 27 = IRQSetIRQHandler
|
||||
> | n == 28 = IRQClearIRQHandler
|
||||
> | n == 29 = DomainSetSet
|
||||
> | n > apiMax = ArchInvocationLabel $ toEnum (n - 1 - apiMax)
|
||||
> | otherwise = error "toEnum out of range for InvocationLabel"
|
||||
> where apiMax = 28
|
||||
> where apiMax = 29
|
||||
|
||||
Decode the invocation type requested by a particular message label.
|
||||
|
||||
|
|
|
|||
|
|
@ -132,6 +132,9 @@ This list may be empty, though it should contain as many registers as possible.
|
|||
> syscallMessage :: [Register]
|
||||
> syscallMessage = map Register Arch.syscallMessage
|
||||
|
||||
> tlsBaseRegister :: Register
|
||||
> tlsBaseRegister = Register Arch.tlsBaseRegister
|
||||
|
||||
\end{description}
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -29,7 +29,7 @@ This module defines the ARM register set.
|
|||
|
||||
> data Register =
|
||||
> R0 | R1 | R2 | R3 | R4 | R5 | R6 | R7 | R8 | R9 | SL | FP | IP | SP |
|
||||
> LR | LR_svc | FaultInstruction | CPSR | TPIDRURW
|
||||
> LR | LR_svc | FaultInstruction | CPSR | TLS_BASE | TPIDRURW
|
||||
> deriving (Eq, Enum, Bounded, Ord, Ix, Show)
|
||||
|
||||
> type Word = Data.Word.Word32
|
||||
|
|
@ -42,6 +42,7 @@ This module defines the ARM register set.
|
|||
> gpRegisters = [R2, R3, R4, R5, R6, R7, LR]
|
||||
> exceptionMessage = [FaultInstruction, SP, CPSR]
|
||||
> syscallMessage = [R0 .. R7] ++ [FaultInstruction, SP, LR, CPSR]
|
||||
> tlsBaseRegister = TLS_BASE
|
||||
|
||||
#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
|
||||
> elr_hyp = LR_svc
|
||||
|
|
|
|||
|
|
@ -39,6 +39,7 @@ This module defines the x86 64-bit register set.
|
|||
> frameRegisters = FaultIP : RSP : FLAGS : [RAX .. R15]
|
||||
> gpRegisters = [TLS_BASE]
|
||||
> exceptionMessage = [FaultIP, RSP, FLAGS]
|
||||
> tlsBaseRegister = TLS_BASE
|
||||
|
||||
> syscallMessage = [RAX .. R15] ++ [FaultIP, RSP, FLAGS]
|
||||
|
||||
|
|
|
|||
|
|
@ -87,6 +87,7 @@ There are eleven types of invocation for a thread control block. All require wri
|
|||
> TCBSetSpace -> decodeSetSpace args cap slot extraCaps
|
||||
> TCBBindNotification -> decodeBindNotification cap extraCaps
|
||||
> TCBUnbindNotification -> decodeUnbindNotification cap
|
||||
> TCBSetTLSBase -> decodeSetTLSBase args cap
|
||||
> _ -> throw IllegalOperation
|
||||
|
||||
\subsubsection{Reading, Writing and Copying Registers}
|
||||
|
|
@ -371,6 +372,14 @@ This is to ensure that the source capability is not made invalid by the deletion
|
|||
> notificationTCB = tcb,
|
||||
> notificationPtr = Nothing }
|
||||
|
||||
> decodeSetTLSBase :: [Word] -> Capability ->
|
||||
> KernelF SyscallError TCBInvocation
|
||||
> decodeSetTLSBase (tls_base:_) cap = do
|
||||
> return $ SetTLSBase {
|
||||
> setTLSBaseTCB = capTCBPtr cap,
|
||||
> setTLSBaseNewBase = tls_base }
|
||||
> decodeSetTLSBase _ _ = throw TruncatedMessage
|
||||
|
||||
|
||||
\subsection[invoke]{Performing TCB Invocations}
|
||||
|
||||
|
|
@ -533,6 +542,13 @@ Modifying the current thread may require rescheduling because modified registers
|
|||
> unbindNotification tcb
|
||||
> return []
|
||||
|
||||
> invokeTCB (SetTLSBase tcb tls_base) =
|
||||
> withoutPreemption $ do
|
||||
> asUser tcb $ setRegister tlsBaseRegister tls_base
|
||||
> cur <- getCurThread
|
||||
> when (tcb == cur) rescheduleRequired
|
||||
> return []
|
||||
|
||||
\subsection{Decoding Domain Invocations}
|
||||
|
||||
The domain cap is invoked to set the domain of a given TCB object to a given value.
|
||||
|
|
|
|||
|
|
@ -48,6 +48,7 @@ requalify_consts
|
|||
word_size_bits
|
||||
clearMemory
|
||||
non_kernel_IRQs
|
||||
tlsBaseRegister
|
||||
|
||||
(* HERE IS THE PLACE FOR GENERIC WORD LEMMAS FOR ALL ARCHITECTURES *)
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue