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 11(* 12 Defines the instances of pspace_storable objects. 13*) 14 15chapter "Storable Object Instances" 16 17theory ObjectInstances_H 18imports 19 Structures_H 20 "./$L4V_ARCH/State_H" 21 PSpaceStorable_H 22 Config_H 23begin 24 25context begin interpretation Arch . 26requalify_consts 27 VPtr 28 newContext 29end 30 31lemma projectKO_eq2: 32 "((obj,s') \<in> fst (projectKO ko s)) = (projectKO_opt ko = Some obj \<and> s' = s)" 33 by (auto simp: projectKO_def fail_def return_def split: option.splits) 34 35 36\<comment> \<open>-----------------------------------\<close> 37 38instantiation endpoint :: pre_storable 39begin 40 41definition 42 projectKO_opt_ep: 43 "projectKO_opt e \<equiv> case e of KOEndpoint e \<Rightarrow> Some e | _ \<Rightarrow> None" 44 45definition 46 injectKO_ep [simp]: 47 "injectKO e \<equiv> KOEndpoint e" 48 49definition 50 koType_ep [simp]: 51 "koType (t::endpoint itself) \<equiv> EndpointT" 52 53instance 54 by (intro_classes, 55 auto simp: projectKO_opt_ep split: kernel_object.splits) 56 57end 58 59instantiation notification :: pre_storable 60begin 61 62definition 63 projectKO_opt_ntfn: 64 "projectKO_opt e \<equiv> case e of KONotification e \<Rightarrow> Some e | _ \<Rightarrow> None" 65 66definition 67 injectKO_ntfn [simp]: 68 "injectKO e \<equiv> KONotification e" 69 70definition 71 koType_ntfn [simp]: 72 "koType (t::notification itself) \<equiv> NotificationT" 73 74instance 75 by (intro_classes, 76 auto simp: projectKO_opt_ntfn split: kernel_object.splits) 77 78end 79 80 81instantiation cte :: pre_storable 82begin 83 84definition 85 projectKO_opt_cte: 86 "projectKO_opt e \<equiv> case e of KOCTE e \<Rightarrow> Some e | _ \<Rightarrow> None" 87 88definition 89 injectKO_cte [simp]: 90 "injectKO c \<equiv> KOCTE c" 91 92definition 93 koType_cte [simp]: 94 "koType (t::cte itself) \<equiv> CTET" 95 96instance 97 by (intro_classes, 98 auto simp: projectKO_opt_cte split: kernel_object.splits) 99 100end 101 102instantiation user_data_device :: pre_storable 103begin 104 105definition 106 projectKO_opt_user_data_device: 107 "projectKO_opt e \<equiv> case e of KOUserDataDevice \<Rightarrow> Some UserDataDevice | _ \<Rightarrow> None" 108 109definition 110 injectKO_user_data_device [simp]: 111 "injectKO (t :: user_data_device) \<equiv> KOUserDataDevice" 112 113definition 114 koType_user_data_device [simp]: 115 "koType (t::user_data_device itself) \<equiv> UserDataDeviceT" 116 117instance 118 by (intro_classes, 119 auto simp: projectKO_opt_user_data_device split: kernel_object.splits) 120end 121 122instantiation user_data :: pre_storable 123begin 124 125definition 126 projectKO_opt_user_data: 127 "projectKO_opt e \<equiv> case e of KOUserData \<Rightarrow> Some UserData | _ \<Rightarrow> None" 128 129definition 130 injectKO_user_data [simp]: 131 "injectKO (t :: user_data) \<equiv> KOUserData" 132 133definition 134 koType_user_data [simp]: 135 "koType (t::user_data itself) \<equiv> UserDataT" 136 137instance 138 by (intro_classes, 139 auto simp: projectKO_opt_user_data split: kernel_object.splits) 140 141end 142 143 144instantiation tcb :: pre_storable 145begin 146 147definition 148 projectKO_opt_tcb: 149 "projectKO_opt e \<equiv> case e of KOTCB e \<Rightarrow> Some e | _ \<Rightarrow> None" 150 151definition 152 injectKO_tcb [simp]: 153 "injectKO t \<equiv> KOTCB t" 154 155definition 156 koType_tcb [simp]: 157 "koType (t::tcb itself) \<equiv> TCBT" 158 159instance 160 by (intro_classes, 161 auto simp: projectKO_opt_tcb split: kernel_object.splits) 162 163end 164 165 166lemmas projectKO_opts_defs = 167 projectKO_opt_tcb projectKO_opt_cte projectKO_opt_ntfn projectKO_opt_ep 168 projectKO_opt_user_data projectKO_opt_user_data_device 169 170lemmas injectKO_defs = 171 injectKO_tcb injectKO_cte injectKO_ntfn injectKO_ep injectKO_user_data injectKO_user_data_device 172 173lemmas koType_defs = 174 koType_tcb koType_cte koType_ntfn koType_ep koType_user_data koType_user_data_device 175 176\<comment> \<open>-----------------------------------\<close> 177 178instantiation endpoint :: pspace_storable 179begin 180 181#INCLUDE_HASKELL SEL4/Object/Instances.lhs instanceproofs bodies_only ONLY Endpoint 182 183instance 184 apply (intro_classes) 185 apply simp 186 apply (case_tac ko, auto simp: projectKO_opt_ep updateObject_default_def 187 in_monad projectKO_eq2 188 split: kernel_object.splits) 189 done 190 191end 192 193 194instantiation notification :: pspace_storable 195begin 196 197#INCLUDE_HASKELL SEL4/Object/Instances.lhs instanceproofs bodies_only ONLY Notification 198 199instance 200 apply (intro_classes) 201 apply (case_tac ko, auto simp: projectKO_opt_ntfn updateObject_default_def 202 in_monad projectKO_eq2 203 split: kernel_object.splits) 204 done 205 206end 207 208 209instantiation cte :: pspace_storable 210begin 211 212#INCLUDE_HASKELL SEL4/Object/Instances.lhs instanceproofs bodies_only ONLY CTE 213 214instance 215 apply (intro_classes) 216 apply (case_tac ko, auto simp: projectKO_opt_cte updateObject_cte 217 in_monad projectKO_eq2 typeError_def alignError_def 218 split: kernel_object.splits if_split_asm) 219 done 220 221end 222 223 224instantiation user_data :: pspace_storable 225begin 226 227#INCLUDE_HASKELL SEL4/Object/Instances.lhs instanceproofs bodies_only ONLY UserData 228 229instance 230 apply (intro_classes) 231 apply (case_tac ko, auto simp: projectKO_opt_user_data updateObject_default_def 232 in_monad projectKO_eq2 233 split: kernel_object.splits) 234 done 235 236end 237 238 239instantiation user_data_device :: pspace_storable 240begin 241 242#INCLUDE_HASKELL SEL4/Object/Instances.lhs instanceproofs bodies_only ONLY UserDataDevice 243 244instance 245 apply (intro_classes) 246 apply (case_tac ko, auto simp: projectKO_opt_user_data_device updateObject_default_def 247 in_monad projectKO_eq2 248 split: kernel_object.splits) 249 done 250 251end 252 253 254instantiation tcb :: pspace_storable 255begin 256 257#INCLUDE_HASKELL SEL4/Object/Instances.lhs instanceproofs bodies_only ONLY TCB 258 259instance 260 apply (intro_classes) 261 apply (case_tac ko, auto simp: projectKO_opt_tcb updateObject_default_def 262 in_monad projectKO_eq2 263 split: kernel_object.splits) 264 done 265 266end 267 268 269end 270