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 Arch Object Instances" 16 17theory ArchObjInsts_H 18imports 19 ArchTypes_H 20 "../PSpaceStorable_H" 21 "../ObjectInstances_H" 22begin 23qualify X64_H (in Arch) 24 25instantiation X64_H.pde :: pre_storable 26begin 27interpretation Arch . 28 29definition 30 projectKO_opt_pde: 31 "projectKO_opt e \<equiv> case e of KOArch (KOPDE e) \<Rightarrow> Some e | _ \<Rightarrow> None" 32 33definition 34 injectKO_pde [simp]: 35 "injectKO e \<equiv> KOArch (KOPDE e)" 36 37definition 38 koType_pde [simp]: 39 "koType (t::pde itself) \<equiv> ArchT PDET" 40 41instance 42 by (intro_classes, 43 auto simp: projectKO_opt_pde split: kernel_object.splits arch_kernel_object.splits) 44 45end 46 47 48instantiation X64_H.pte :: pre_storable 49begin 50interpretation Arch . 51 52definition 53 projectKO_opt_pte: 54 "projectKO_opt e \<equiv> case e of (KOArch (KOPTE e)) \<Rightarrow> Some e | _ \<Rightarrow> None" 55 56definition 57 injectKO_pte [simp]: 58 "injectKO e \<equiv> KOArch (KOPTE e)" 59 60definition 61 koType_pte [simp]: 62 "koType (t::pte itself) \<equiv> ArchT PTET" 63 64instance 65 by (intro_classes, 66 auto simp: projectKO_opt_pte split: kernel_object.splits arch_kernel_object.splits) 67 68end 69 70instantiation X64_H.pdpte :: pre_storable 71begin 72interpretation Arch . 73 74definition 75 projectKO_opt_pdpte: 76 "projectKO_opt e \<equiv> case e of (KOArch (KOPDPTE e)) \<Rightarrow> Some e | _ \<Rightarrow> None" 77 78definition 79 injectKO_pdpte [simp]: 80 "injectKO e \<equiv> KOArch (KOPDPTE e)" 81 82definition 83 koType_pdpte [simp]: 84 "koType (t::pdpte itself) \<equiv> ArchT PDPTET" 85 86instance 87 by (intro_classes, 88 auto simp: projectKO_opt_pdpte split: kernel_object.splits arch_kernel_object.splits) 89 90end 91 92instantiation X64_H.pml4e :: pre_storable 93begin 94interpretation Arch . 95 96definition 97 projectKO_opt_pml4e: 98 "projectKO_opt e \<equiv> case e of (KOArch (KOPML4E e)) \<Rightarrow> Some e | _ \<Rightarrow> None" 99 100definition 101 injectKO_pml4e [simp]: 102 "injectKO e \<equiv> KOArch (KOPML4E e)" 103 104definition 105 koType_pml4e [simp]: 106 "koType (t::pml4e itself) \<equiv> ArchT PML4ET" 107 108instance 109 by (intro_classes, 110 auto simp: projectKO_opt_pml4e split: kernel_object.splits arch_kernel_object.splits) 111 112end 113 114instantiation X64_H.asidpool :: pre_storable 115begin 116interpretation Arch . 117 118definition 119 injectKO_asidpool [simp]: 120 "injectKO e \<equiv> KOArch (KOASIDPool e)" 121 122definition 123 koType_asidpool [simp]: 124 "koType (t::asidpool itself) \<equiv> ArchT ASIDPoolT" 125 126definition 127 projectKO_opt_asidpool: 128 "projectKO_opt e \<equiv> case e of (KOArch (KOASIDPool e)) \<Rightarrow> Some e | _ \<Rightarrow> None" 129 130instance 131 by (intro_classes, 132 auto simp: projectKO_opt_asidpool split: kernel_object.splits arch_kernel_object.splits) 133 134end 135 136lemmas (in Arch) projectKO_opts_defs = 137 projectKO_opt_pte projectKO_opt_pde 138 projectKO_opt_pdpte projectKO_opt_pml4e 139 projectKO_opt_asidpool 140 ObjectInstances_H.projectKO_opts_defs 141 142lemmas (in Arch) [simp] = 143 injectKO_pte koType_pte 144 injectKO_pde koType_pde 145 injectKO_pdpte koType_pdpte 146 injectKO_pml4e koType_pml4e 147 injectKO_asidpool koType_asidpool 148 149 150\<comment> \<open>--------------------------------------\<close> 151 152#INCLUDE_SETTINGS keep_constructor = asidpool 153 154#INCLUDE_HASKELL_PREPARSE SEL4/Object/Structures/X64.lhs 155#INCLUDE_HASKELL_PREPARSE SEL4/Machine/Hardware/X64.lhs 156 157 158instantiation X64_H.pde :: pspace_storable 159begin 160interpretation Arch . 161 162#INCLUDE_HASKELL SEL4/Object/Instances/X64.lhs instanceproofs bodies_only ONLY PDE 163 164instance 165 apply (intro_classes) 166 apply (clarsimp simp add: updateObject_default_def in_monad projectKO_opts_defs 167 projectKO_eq2 168 split: kernel_object.splits arch_kernel_object.splits) 169 done 170 171end 172 173instantiation X64_H.pte :: pspace_storable 174begin 175interpretation Arch . 176 177#INCLUDE_HASKELL SEL4/Object/Instances/X64.lhs instanceproofs bodies_only ONLY PTE 178 179instance 180 apply (intro_classes) 181 apply (clarsimp simp add: updateObject_default_def in_monad projectKO_opts_defs 182 projectKO_eq2 183 split: kernel_object.splits arch_kernel_object.splits) 184 done 185 186end 187 188 189instantiation X64_H.pdpte :: pspace_storable 190begin 191interpretation Arch . 192 193#INCLUDE_HASKELL SEL4/Object/Instances/X64.lhs instanceproofs bodies_only ONLY PDPTE 194 195instance 196 apply (intro_classes) 197 apply (clarsimp simp add: updateObject_default_def in_monad projectKO_opts_defs 198 projectKO_eq2 199 split: kernel_object.splits arch_kernel_object.splits) 200 done 201 202end 203 204instantiation X64_H.pml4e :: pspace_storable 205begin 206interpretation Arch . 207 208#INCLUDE_HASKELL SEL4/Object/Instances/X64.lhs instanceproofs bodies_only ONLY PML4E 209 210instance 211 apply (intro_classes) 212 apply (clarsimp simp add: updateObject_default_def in_monad projectKO_opts_defs 213 projectKO_eq2 214 split: kernel_object.splits arch_kernel_object.splits) 215 done 216 217end 218 219(* This is hard coded since using funArray in haskell for 2^32 bound is risky *) 220 221instantiation X64_H.asidpool :: pspace_storable 222begin 223interpretation Arch . 224 225definition 226 makeObject_asidpool: "(makeObject :: asidpool) \<equiv> ASIDPool $ 227 funArray (const Nothing)" 228 229definition 230 loadObject_asidpool[simp]: 231 "(loadObject p q n obj) :: asidpool kernel \<equiv> 232 loadObject_default p q n obj" 233 234definition 235 updateObject_asidpool[simp]: 236 "updateObject (val :: asidpool) \<equiv> 237 updateObject_default val" 238 239instance 240 apply (intro_classes) 241 apply (clarsimp simp add: updateObject_default_def in_monad projectKO_opts_defs 242 projectKO_eq2 243 split: kernel_object.splits arch_kernel_object.splits) 244 done 245 246end 247 248lemmas load_update_defs = 249 loadObject_pte updateObject_pte 250 loadObject_pde updateObject_pde 251 loadObject_pdpte updateObject_pdpte 252 loadObject_pml4e updateObject_pml4e 253 loadObject_asidpool updateObject_asidpool 254 255declare load_update_defs[simp del] 256 257end_qualify 258 259declare (in Arch) load_update_defs[simp] 260 261end 262