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