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
11chapter "Thread Control Blocks"
12
13theory TCB_H
14imports
15  NotificationDecls_H
16  TCBDecls_H
17  CNode_H
18  VSpace_H
19  "./$L4V_ARCH/ArchTCB_H"
20begin
21
22context begin interpretation Arch .
23requalify_consts
24  decodeTransfer
25  gpRegisters
26  frameRegisters
27  getRegister
28  setNextPC
29  getRestartPC
30  sanitiseRegister
31  getSanitiseRegisterInfo
32  setRegister
33  performTransfer
34  msgInfoRegister
35  msgRegisters
36  fromVPtr
37  setTCBIPCBuffer
38  postModifyRegisters
39  tlsBaseRegister
40end
41
42abbreviation "mapMaybe \<equiv> option_map"
43
44#INCLUDE_HASKELL SEL4/Object/TCB.lhs Arch= bodies_only NOT liftFnMaybe assertDerived archThreadGet archThreadSet asUser sanitiseRegister getSanitiseRegisterInfo
45
46defs asUser_def:
47"asUser tptr f\<equiv> (do
48        uc \<leftarrow> threadGet  (atcbContextGet o tcbArch) tptr;
49        (a, uc') \<leftarrow> select_f (f uc);
50        threadSet (\<lambda> tcb. tcb \<lparr> tcbArch := atcbContextSet uc' (tcbArch tcb)\<rparr>) tptr;
51        return a
52od)"
53
54end
55