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 :: word32) < 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 :: word32) < 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 104lemma headM_wordsFromPTE[simp]: 105 "headM (wordsFromPTE pte) = (return (hd (wordsFromPTE pte)))" 106 unfolding wordsFromPTE_def 107 by (cases pte; simp) 108 109lemma length_wordsFromPTE: 110 "length (wordsFromPTE pte) = 2" 111 unfolding wordsFromPTE_def 112 by (cases pte; simp) 113 114lemma length_wordsFromPDE: 115 "length (wordsFromPDE pde) = 2" 116 unfolding wordsFromPDE_def 117 by (cases pde; simp) 118 119lemma storePTE_Basic_ccorres': 120 "\<lbrakk> cpte_relation pte pte' \<rbrakk> \<Longrightarrow> 121 ccorres dc xfdc \<top> {s. ptr_val (f s) = p} hs 122 (storePTE p pte) 123 (Guard C_Guard {s. s \<Turnstile>\<^sub>c f s} 124 (Basic (\<lambda>s. globals_update( t_hrs_'_update 125 (hrs_mem_update (heap_update (f s) pte'))) s)))" 126 using length_wordsFromPTE[where pte=pte] 127 apply (simp add: storePTE_def tailM_def headM_def) 128 apply (case_tac "wordsFromPTE pte"; clarsimp) 129 apply (case_tac list; clarsimp) 130 apply (rule setObject_ccorres_helper) 131 apply (simp_all add: objBits_simps archObjSize_def table_bits_defs) 132 apply (rule conseqPre, vcg) 133 apply (rule subsetI, clarsimp simp: Collect_const_mem) 134 apply (rule cmap_relationE1, erule rf_sr_cpte_relation, 135 erule ko_at_projectKO_opt) 136 apply (rule conjI, fastforce intro: typ_heap_simps) 137 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def) 138 apply (rule conjI) 139 apply (clarsimp simp: cpspace_relation_def typ_heap_simps 140 update_pte_map_to_ptes 141 update_pte_map_tos 142 carray_map_relation_upd_triv) 143 144 apply (case_tac "f x", simp) 145 146 apply (erule cmap_relation_updI, 147 erule ko_at_projectKO_opt, simp+) 148 apply (simp add: cready_queues_relation_def 149 carch_state_relation_def 150 cmachine_state_relation_def 151 Let_def typ_heap_simps 152 cteCaps_of_def update_pte_map_tos table_bits_defs 153 ) 154 done 155 156 157lemma storePTE_Basic_ccorres: 158 "\<lbrakk> cpte_relation pte pte' \<rbrakk> \<Longrightarrow> 159 ccorres dc xfdc \<top> {s. f s = p} hs 160 (storePTE p pte) 161 (Guard C_Guard {s. s \<Turnstile>\<^sub>c pte_Ptr (f s)} 162 (Basic (\<lambda>s. globals_update( t_hrs_'_update 163 (hrs_mem_update (heap_update (pte_Ptr (f s)) pte'))) s)))" 164 apply (rule ccorres_guard_imp2) 165 apply (erule storePTE_Basic_ccorres') 166 apply simp 167 done 168 169lemma pde_stored_asid_update_valid_offset: 170 "valid_pde_mapping_offset' (ptr_val p && mask pdBits) 171 \<Longrightarrow> (pde_stored_asid \<circ>\<^sub>m (clift (t_hrs_' cstate))(p \<mapsto> pde) \<circ>\<^sub>m pd_pointer_to_asid_slot) 172 = (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot)" 173 apply (rule ext, clarsimp simp add: pd_pointer_to_asid_slot_def map_comp_eq) 174 apply (simp add: valid_pde_mapping_offset'_def mask_add_aligned) 175 apply (simp add: pd_asid_slot_def mask_def table_bits_defs) 176 done 177 178lemma storePDE_Basic_ccorres': 179 "\<lbrakk> cpde_relation pde pde' \<rbrakk> \<Longrightarrow> 180 ccorres dc xfdc 181 (\<lambda>_. valid_pde_mapping_offset' (p && mask pdBits)) 182 {s. ptr_val (f s) = p} hs 183 (storePDE p pde) 184 (Guard C_Guard {s. s \<Turnstile>\<^sub>c f s} 185 (Basic (\<lambda>s. globals_update( t_hrs_'_update 186 (hrs_mem_update (heap_update (f s) pde'))) s)))" 187 using length_wordsFromPDE[where pde=pde] 188 apply (simp add: storePDE_def tailM_def headM_def) 189 apply (case_tac "wordsFromPDE pde"; clarsimp) 190 apply (case_tac list; clarsimp) 191 apply (rule setObject_ccorres_helper) 192 apply (simp_all add: objBits_simps archObjSize_def table_bits_defs) 193 apply (rule conseqPre, vcg) 194 apply (rule subsetI, clarsimp simp: Collect_const_mem) 195 apply (rule cmap_relationE1, erule rf_sr_cpde_relation, 196 erule ko_at_projectKO_opt) 197 apply (rule conjI, fastforce intro: typ_heap_simps) 198 apply (case_tac "f x", clarsimp) 199 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def) 200 apply (rule conjI) 201 apply (clarsimp simp: cpspace_relation_def typ_heap_simps 202 update_pde_map_to_pdes 203 update_pde_map_tos 204 carray_map_relation_upd_triv) 205 apply (erule cmap_relation_updI, 206 erule ko_at_projectKO_opt, simp+) 207 apply (simp add: cready_queues_relation_def 208 carch_state_relation_def 209 cmachine_state_relation_def 210 Let_def typ_heap_simps table_bits_defs 211 pde_stored_asid_update_valid_offset 212 cteCaps_of_def update_pde_map_tos) 213 done 214 215lemma storePDE_Basic_ccorres: 216 "\<lbrakk> cpde_relation pde pde' \<rbrakk> \<Longrightarrow> 217 ccorres dc xfdc (\<lambda>_. valid_pde_mapping_offset' (p && mask pdBits)) {s. f s = p} hs 218 (storePDE p pde) 219 (Guard C_Guard {s. s \<Turnstile>\<^sub>c pde_Ptr (f s)} 220 (Basic (\<lambda>s. globals_update(t_hrs_'_update 221 (hrs_mem_update (heap_update (pde_Ptr (f s)) pde'))) s)))" 222 apply (rule ccorres_guard_imp2) 223 apply (erule storePDE_Basic_ccorres') 224 apply simp 225 done 226 227end 228end 229