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 11theory PSpace_C 12imports Ctac_lemmas_C 13begin 14 15context kernel begin 16 17lemma koTypeOf_injectKO: 18 fixes v :: "'a :: pspace_storable" shows 19 "koTypeOf (injectKO v) = koType TYPE('a)" 20 apply (cut_tac v1=v in iffD2 [OF project_inject, OF refl]) 21 apply (simp add: project_koType[symmetric]) 22 done 23 24lemma setObject_obj_at_pre: 25 "\<lbrakk> updateObject ko = updateObject_default ko; 26 (1 :: machine_word) < 2 ^ objBits ko \<rbrakk> 27 \<Longrightarrow> 28 setObject p ko 29 = (stateAssert (typ_at' (koTypeOf (injectKO ko)) p) [] 30 >>= (\<lambda>_. setObject p ko))" 31 apply (rule ext) 32 apply (case_tac "typ_at' (koTypeOf (injectKO ko)) p x") 33 apply (simp add: stateAssert_def bind_def 34 get_def return_def) 35 apply (simp add: stateAssert_def bind_def 36 get_def assert_def fail_def) 37 apply (simp add: setObject_def exec_gets split_def 38 assert_opt_def split: option.split) 39 apply (clarsimp simp add: fail_def) 40 apply (simp add: bind_def simpler_modify_def split_def) 41 apply (rule context_conjI) 42 apply (clarsimp simp: updateObject_default_def 43 in_monad) 44 apply (clarsimp simp: projectKOs in_magnitude_check) 45 apply (frule iffD1[OF project_koType, OF exI]) 46 apply (clarsimp simp: typ_at'_def ko_wp_at'_def) 47 apply (simp only: objBitsT_koTypeOf[symmetric] objBits_def) 48 apply simp 49 apply (simp add: koTypeOf_injectKO) 50 apply (rule empty_failD[OF empty_fail_updateObject_default]) 51 apply (rule ccontr, erule nonemptyE) 52 apply clarsimp 53 done 54 55 56 57lemma setObject_ccorres_helper: 58 fixes ko :: "'a :: pspace_storable" 59 assumes valid: "\<And>\<sigma> (ko' :: 'a). 60 \<Gamma> \<turnstile> {s. (\<sigma>, s) \<in> rf_sr \<and> P \<sigma> \<and> s \<in> P' \<and> ko_at' ko' p \<sigma>} 61 c {s. (\<sigma>\<lparr>ksPSpace := ksPSpace \<sigma> (p \<mapsto> injectKO ko)\<rparr>, s) \<in> rf_sr}" 62 shows "\<lbrakk> \<And>ko :: 'a. updateObject ko = updateObject_default ko; 63 \<And>ko :: 'a. (1 :: machine_word) < 2 ^ objBits ko \<rbrakk> 64 \<Longrightarrow> ccorres dc xfdc P P' hs (setObject p ko) c" 65 apply (rule ccorres_guard_imp2) 66 apply (subst setObject_obj_at_pre) 67 apply simp+ 68 apply (rule ccorres_symb_exec_l[where Q'="\<lambda>_. P'"]) 69 defer 70 apply (rule stateAssert_inv) 71 apply (rule stateAssert_sp[where P=P]) 72 apply (rule empty_fail_stateAssert) 73 apply simp 74 apply (rule ccorres_from_vcg) 75 apply (rule allI) 76 apply (rule hoare_complete) 77 apply (clarsimp simp: HoarePartialDef.valid_def) 78 apply (simp add: typ_at_to_obj_at' koTypeOf_injectKO) 79 apply (drule obj_at_ko_at', clarsimp) 80 apply (cut_tac \<sigma>1=\<sigma> and ko'1=koa in valid) 81 apply (drule hoare_sound, 82 clarsimp simp: cvalid_def HoarePartialDef.valid_def) 83 apply (elim allE, drule(1) mp) 84 apply (drule mp, simp) 85 apply clarsimp 86 apply (rule imageI[OF CollectI]) 87 apply (rule rev_bexI) 88 apply (rule setObject_eq, simp+) 89 apply (simp add: objBits_def) 90 apply (simp only: objBitsT_koTypeOf[symmetric] 91 koTypeOf_injectKO) 92 apply assumption 93 apply simp 94 done 95 96 97lemma carray_map_relation_upd_triv: 98 "f x = Some (v :: 'a :: pspace_storable) 99 \<Longrightarrow> carray_map_relation n (f (x \<mapsto> y)) hp ptrf = carray_map_relation n f hp ptrf" 100 by (simp add: carray_map_relation_def objBits_def objBitsT_koTypeOf[symmetric] 101 koTypeOf_injectKO 102 del: objBitsT_koTypeOf) 103 104 105lemma storePTE_Basic_ccorres': 106 "\<lbrakk> cpte_relation pte pte' \<rbrakk> \<Longrightarrow> 107 ccorres dc xfdc \<top> {s. ptr_val (f s) = p} hs 108 (storePTE p pte) 109 (Guard C_Guard {s. s \<Turnstile>\<^sub>c f s} 110 (Basic (\<lambda>s. globals_update( t_hrs_'_update 111 (hrs_mem_update (heap_update (f s) pte'))) s)))" 112 apply (simp add: storePTE_def) 113 apply (rule setObject_ccorres_helper) 114 apply (simp_all add: objBits_simps archObjSize_def bit_simps) 115 apply (rule conseqPre, vcg) 116 apply (rule subsetI, clarsimp simp: Collect_const_mem) 117 apply (rule cmap_relationE1, erule rf_sr_cpte_relation, 118 erule ko_at_projectKO_opt) 119 apply (rule conjI, fastforce intro: typ_heap_simps) 120 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def) 121 apply (rule conjI) 122 apply (clarsimp simp: cpspace_relation_def typ_heap_simps 123 update_pte_map_to_ptes 124 update_pte_map_tos 125 carray_map_relation_upd_triv) 126 127 apply (case_tac "f x", simp) 128 129 apply (erule cmap_relation_updI, 130 erule ko_at_projectKO_opt, simp+) 131 apply (simp add: cready_queues_relation_def 132 carch_state_relation_def 133 fpu_null_state_heap_update_tag_disj_simps 134 cmachine_state_relation_def 135 Let_def typ_heap_simps 136 cteCaps_of_def update_pte_map_tos bit_simps) 137 done 138 139 140lemma storePTE_Basic_ccorres: 141 "\<lbrakk> cpte_relation pte pte' \<rbrakk> \<Longrightarrow> 142 ccorres dc xfdc \<top> {s. f s = p} hs 143 (storePTE p pte) 144 (Guard C_Guard {s. s \<Turnstile>\<^sub>c pte_Ptr (f s)} 145 (Basic (\<lambda>s. globals_update( t_hrs_'_update 146 (hrs_mem_update (heap_update (pte_Ptr (f s)) pte'))) s)))" 147 apply (rule ccorres_guard_imp2) 148 apply (erule storePTE_Basic_ccorres') 149 apply simp 150 done 151 152lemma storePDE_Basic_ccorres': 153 "\<lbrakk> cpde_relation pde pde' \<rbrakk> \<Longrightarrow> 154 ccorres dc xfdc 155 \<top> 156 {s. ptr_val (f s) = p} hs 157 (storePDE p pde) 158 (Guard C_Guard {s. s \<Turnstile>\<^sub>c f s} 159 (Basic (\<lambda>s. globals_update( t_hrs_'_update 160 (hrs_mem_update (heap_update (f s) pde'))) s)))" 161 apply (simp add: storePDE_def) 162 apply (rule setObject_ccorres_helper) 163 apply (simp_all add: objBits_simps archObjSize_def bit_simps) 164 apply (rule conseqPre, vcg) 165 apply (rule subsetI, clarsimp simp: Collect_const_mem) 166 apply (rule cmap_relationE1, erule rf_sr_cpde_relation, 167 erule ko_at_projectKO_opt) 168 apply (rule conjI, fastforce intro: typ_heap_simps) 169 apply (case_tac "f x", clarsimp) 170 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def) 171 apply (rule conjI) 172 apply (clarsimp simp: cpspace_relation_def typ_heap_simps 173 update_pde_map_to_pdes 174 update_pde_map_tos 175 carray_map_relation_upd_triv) 176 apply (erule cmap_relation_updI, 177 erule ko_at_projectKO_opt, simp+) 178 apply (simp add: cready_queues_relation_def 179 carch_state_relation_def 180 fpu_null_state_heap_update_tag_disj_simps 181 cmachine_state_relation_def 182 Let_def typ_heap_simps bit_simps 183 cteCaps_of_def update_pde_map_tos) 184 done 185 186lemma storePDE_Basic_ccorres: 187 "\<lbrakk> cpde_relation pde pde' \<rbrakk> \<Longrightarrow> 188 ccorres dc xfdc \<top> {s. f s = p} hs 189 (storePDE p pde) 190 (Guard C_Guard {s. s \<Turnstile>\<^sub>c pde_Ptr (f s)} 191 (Basic (\<lambda>s. globals_update(t_hrs_'_update 192 (hrs_mem_update (heap_update (pde_Ptr (f s)) pde'))) s)))" 193 apply (rule ccorres_guard_imp2) 194 apply (erule storePDE_Basic_ccorres') 195 apply simp 196 done 197 198lemma storePDPTE_Basic_ccorres': 199 "\<lbrakk> cpdpte_relation pdpte pdpte' \<rbrakk> \<Longrightarrow> 200 ccorres dc xfdc \<top> {s. ptr_val (f s) = p} hs 201 (storePDPTE p pdpte) 202 (Guard C_Guard {s. s \<Turnstile>\<^sub>c f s} 203 (Basic (\<lambda>s. globals_update( t_hrs_'_update 204 (hrs_mem_update (heap_update (f s) pdpte'))) s)))" 205 apply (simp add: storePDPTE_def) 206 apply (rule setObject_ccorres_helper) 207 apply (simp_all add: objBits_simps archObjSize_def bit_simps) 208 apply (rule conseqPre, vcg) 209 apply (rule subsetI, clarsimp simp: Collect_const_mem) 210 apply (rule cmap_relationE1, erule rf_sr_cpdpte_relation, 211 erule ko_at_projectKO_opt) 212 apply (rule conjI, fastforce intro: typ_heap_simps) 213 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def) 214 apply (rule conjI) 215 apply (clarsimp simp: cpspace_relation_def typ_heap_simps 216 update_pdpte_map_to_pdptes 217 update_pdpte_map_tos 218 carray_map_relation_upd_triv) 219 220 apply (case_tac "f x", simp) 221 222 apply (erule cmap_relation_updI, 223 erule ko_at_projectKO_opt, simp+) 224 apply (simp add: cready_queues_relation_def 225 carch_state_relation_def 226 fpu_null_state_heap_update_tag_disj_simps 227 cmachine_state_relation_def 228 Let_def typ_heap_simps 229 cteCaps_of_def update_pdpte_map_tos bit_simps) 230 done 231 232 233lemma storePDPTE_Basic_ccorres: 234 "\<lbrakk> cpdpte_relation pdpte pdpte' \<rbrakk> \<Longrightarrow> 235 ccorres dc xfdc \<top> {s. f s = p} hs 236 (storePDPTE p pdpte) 237 (Guard C_Guard {s. s \<Turnstile>\<^sub>c pdpte_Ptr (f s)} 238 (Basic (\<lambda>s. globals_update( t_hrs_'_update 239 (hrs_mem_update (heap_update (pdpte_Ptr (f s)) pdpte'))) s)))" 240 apply (rule ccorres_guard_imp2) 241 apply (erule storePDPTE_Basic_ccorres') 242 apply simp 243 done 244 245lemma storePML4E_Basic_ccorres': 246 "\<lbrakk> cpml4e_relation pml4e pml4e' \<rbrakk> \<Longrightarrow> 247 ccorres dc xfdc 248 \<top> 249 {s. ptr_val (f s) = p} hs 250 (storePML4E p pml4e) 251 (Guard C_Guard {s. s \<Turnstile>\<^sub>c f s} 252 (Basic (\<lambda>s. globals_update( t_hrs_'_update 253 (hrs_mem_update (heap_update (f s) pml4e'))) s)))" 254 apply (simp add: storePML4E_def) 255 apply (rule setObject_ccorres_helper) 256 apply (simp_all add: objBits_simps archObjSize_def bit_simps) 257 apply (rule conseqPre, vcg) 258 apply (rule subsetI, clarsimp simp: Collect_const_mem) 259 apply (rule cmap_relationE1, erule rf_sr_cpml4e_relation, 260 erule ko_at_projectKO_opt) 261 apply (rule conjI, fastforce intro: typ_heap_simps) 262 apply (case_tac "f x", clarsimp) 263 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def) 264 apply (rule conjI) 265 apply (clarsimp simp: cpspace_relation_def typ_heap_simps 266 update_pml4e_map_to_pml4es 267 update_pml4e_map_tos 268 carray_map_relation_upd_triv) 269 apply (erule cmap_relation_updI, 270 erule ko_at_projectKO_opt, simp+) 271 apply (simp add: cready_queues_relation_def 272 carch_state_relation_def 273 fpu_null_state_heap_update_tag_disj_simps 274 cmachine_state_relation_def 275 Let_def typ_heap_simps bit_simps 276 cteCaps_of_def update_pml4e_map_tos) 277 done 278 279lemma storePML4E_Basic_ccorres: 280 "\<lbrakk> cpml4e_relation pml4e pml4e' \<rbrakk> \<Longrightarrow> 281 ccorres dc xfdc \<top> {s. f s = p} hs 282 (storePML4E p pml4e) 283 (Guard C_Guard {s. s \<Turnstile>\<^sub>c pml4e_Ptr (f s)} 284 (Basic (\<lambda>s. globals_update(t_hrs_'_update 285 (hrs_mem_update (heap_update (pml4e_Ptr (f s)) pml4e'))) s)))" 286 apply (rule ccorres_guard_imp2) 287 apply (erule storePML4E_Basic_ccorres') 288 apply simp 289 done 290 291end 292end 293