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 ArchAInvsPre 12imports "../AInvsPre" 13begin 14 15context Arch begin 16 17global_naming ARM 18 19lemma get_pd_of_thread_reachable: 20 "get_pd_of_thread (kheap s) (arch_state s) t \<noteq> 0 21 \<Longrightarrow> (\<exists>\<rhd> get_pd_of_thread (kheap s) (arch_state s) t) s" 22 by (auto simp: get_pd_of_thread_vs_lookup 23 split: Structures_A.kernel_object.splits if_split_asm option.splits 24 cap.splits arch_cap.splits) 25 26lemma is_aligned_ptrFromPAddrD: 27"\<lbrakk>is_aligned (ptrFromPAddr b) a; a \<le> 25\<rbrakk> \<Longrightarrow> is_aligned b a" 28 apply (clarsimp simp: ptrFromPAddr_def physMappingOffset_def kernelBase_addr_def physBase_def) 29 apply (erule is_aligned_addD2) 30 apply (rule is_aligned_weaken[where x = 25]) 31 apply (simp add: is_aligned_def) 32 apply simp 33 done 34 35lemma obj_bits_data_at: 36 "data_at sz (ptrFromPAddr b) s 37 \<Longrightarrow> obj_bits (the (kheap s (ptrFromPAddr b))) = pageBitsForSize sz" 38 apply (clarsimp simp add: obj_at_def a_type_def data_at_def 39 split: kernel_object.splits arch_kernel_obj.split_asm if_splits) 40 apply (case_tac ko,simp_all) 41 apply fastforce 42 subgoal for ko archko 43 by (case_tac archko,fastforce+) 44 done 45 46lemma some_get_page_info_umapsD: 47 "\<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) pd_ref p = Some (b, a, attr, r); 48 (\<exists>\<rhd> pd_ref) s; valid_vspace_objs s; pspace_aligned s; 49 valid_asid_table (arm_asid_table (arch_state s)) s; valid_objs s\<rbrakk> 50 \<Longrightarrow> (\<exists>sz. pageBitsForSize sz = a \<and> is_aligned b a \<and> 51 data_at sz (ptrFromPAddr b) s)" 52 apply (clarsimp simp: get_page_info_def get_pd_entry_def get_arch_obj_def 53 split: option.splits Structures_A.kernel_object.splits 54 arch_kernel_obj.splits if_splits) 55 apply (frule (1) valid_vspace_objsD[rotated 2]) 56 apply (simp add: obj_at_def) 57 apply (simp add: valid_vspace_obj_def vspace_bits_defs) 58 apply (drule_tac x="ucast (p >> 21)" in spec) 59 apply (simp split: pde.splits) 60 apply (rename_tac rs pd pt_ref) 61 apply (subgoal_tac 62 "((rs, pd_ref) \<rhd>1 63 (VSRef (ucast (ucast (p >> 21))) (Some APageDirectory) # rs, 64 ptrFromPAddr pt_ref)) s") 65 prefer 2 66 apply (rule vs_lookup1I[rotated 2], simp) 67 apply (simp add: obj_at_def) 68 apply (simp add: vs_refs_def pde_ref_def image_def graph_of_def) 69 apply (rule_tac x="ucast (p >> 21)" in exI, rule conjI, simp+) 70 apply (frule (1) vs_lookup_step) 71 apply (drule (2) stronger_vspace_objsD[where ref="x # xs" for x xs]) 72 apply clarsimp 73 apply (case_tac ao, simp_all add: a_type_simps obj_at_def)[1] 74 apply (simp add: get_pt_info_def get_pt_entry_def) 75 apply (drule_tac x="(ucast ((p >> 12) && mask 9))" in spec) 76 apply (clarsimp simp: obj_at_def 77 split: pte.splits,intro exI conjI,simp_all)[1] 78 apply (frule obj_bits_data_at) 79 apply (clarsimp simp: pspace_aligned_def data_at_def) 80 apply (drule_tac x = "(ptrFromPAddr b)" in bspec ) 81 apply (fastforce simp: obj_at_def) 82 apply (clarsimp dest!: is_aligned_ptrFromPAddrD) 83 apply (intro exI conjI, simp_all add: pageBits_def)[1] 84 apply (simp add: get_pt_info_def get_pt_entry_def) 85 apply clarsimp 86 apply (frule obj_bits_data_at) 87 apply (intro exI conjI, simp_all add: pageBits_def)[1] 88 apply (clarsimp simp: pspace_aligned_def data_at_def) 89 apply (drule_tac x = "(ptrFromPAddr b)" in bspec) 90 apply (fastforce simp: obj_at_def) 91 apply (clarsimp dest!: is_aligned_ptrFromPAddrD) 92 apply clarsimp 93 apply (frule obj_bits_data_at) 94 apply (intro exI conjI, simp_all add: pageBits_def)[1] 95 apply (clarsimp simp: pspace_aligned_def data_at_def) 96 apply (drule_tac x = "(ptrFromPAddr b)" in bspec) 97 apply (fastforce simp: obj_at_def) 98 apply (clarsimp dest!: is_aligned_ptrFromPAddrD) 99 done 100 101lemma user_mem_dom_cong: 102 "kheap s = kheap s' \<Longrightarrow> dom (user_mem s) = dom (user_mem s')" 103 by (simp add: user_mem_def in_user_frame_def dom_def obj_at_def) 104 105lemma device_mem_dom_cong: 106 "kheap s = kheap s' \<Longrightarrow> dom (device_mem s) = dom (device_mem s')" 107 by (simp add: device_mem_def in_device_frame_def dom_def obj_at_def) 108 109lemma device_frame_in_device_region: 110 "\<lbrakk>in_device_frame p s; pspace_respects_device_region s\<rbrakk> 111 \<Longrightarrow> device_state (machine_state s) p \<noteq> None" 112 by (auto simp add: pspace_respects_device_region_def dom_def device_mem_def) 113 114lemma is_aligned_physMappingOffset: 115"is_aligned physMappingOffset (pageBitsForSize sz)" 116 by (case_tac sz, simp_all add: physMappingOffset_def 117 kernelBase_addr_def physBase_def is_aligned_def)[1] 118 119global_naming Arch 120named_theorems AInvsPre_asms 121 122lemma get_page_info_0[simp]: 123 "get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) 0 x = None" 124 by (simp add: get_page_info_def) 125 126lemma (* ptable_rights_imp_frame *)[AInvsPre_asms]: 127 assumes "valid_state s" 128 shows "ptable_rights t s x \<noteq> {} \<Longrightarrow> 129 ptable_lift t s x = Some (addrFromPPtr y) \<Longrightarrow> 130 in_user_frame y s \<or> in_device_frame y s" 131 apply (clarsimp simp: ptable_rights_def ptable_lift_def in_user_frame_def 132 in_device_frame_def data_at_def 133 split: option.splits) 134 apply (rename_tac b a r) 135 apply (frule some_get_page_info_umapsD) 136 apply (rule get_pd_of_thread_reachable, clarsimp) 137 using assms 138 apply (simp_all add: valid_state_def valid_pspace_def 139 valid_arch_state_def) 140 apply clarsimp 141 apply (frule is_aligned_add_helper[OF _ and_mask_less', 142 THEN conjunct2, of _ _ x]) 143 apply (simp only: pbfs_less_wb'[simplified word_bits_def]) 144 apply (clarsimp simp: ptrFromPAddr_def addrFromPPtr_def 145 field_simps) 146 apply (rule_tac x=sz in exI) 147 apply (drule_tac x = sz in spec) 148 apply (subst add.assoc[symmetric]) 149 apply (frule is_aligned_add_helper[OF aligned_add_aligned[OF _ is_aligned_physMappingOffset]]) 150 apply (rule le_refl) 151 apply (rule_tac w = x in and_mask_less') 152 apply (case_tac sz, simp_all add: word_bits_conv)[1] 153 apply (clarsimp simp: field_simps simp: data_at_def) 154 done 155end 156 157global_interpretation AInvsPre?: AInvsPre 158 proof goal_cases 159 interpret Arch . 160 case 1 show ?case by (intro_locales; (unfold_locales, fact AInvsPre_asms)?) 161 qed 162 163requalify_facts 164 ARM.user_mem_dom_cong 165 ARM.device_mem_dom_cong 166 ARM.device_frame_in_device_region 167 ARM.is_aligned_physMappingOffset 168end 169