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 ArchTcbAcc_AI 12imports "../TcbAcc_AI" 13begin 14 15context Arch begin global_naming ARM 16 17named_theorems TcbAcc_AI_assms 18 19lemmas cap_master_cap_simps = 20 cap_master_cap_def[simplified cap_master_arch_cap_def, split_simps cap.split arch_cap.split] 21 22lemma cap_master_cap_arch_eqDs: 23 "cap_master_cap cap = cap.ArchObjectCap (arch_cap.PageCap dev ref rghts sz mapdata) 24 \<Longrightarrow> rghts = UNIV \<and> mapdata = None 25 \<and> (\<exists>rghts mapdata. cap = cap.ArchObjectCap (arch_cap.PageCap dev ref rghts sz mapdata))" 26 "cap_master_cap cap = cap.ArchObjectCap arch_cap.ASIDControlCap 27 \<Longrightarrow> cap = cap.ArchObjectCap arch_cap.ASIDControlCap" 28 "cap_master_cap cap = cap.ArchObjectCap (arch_cap.ASIDPoolCap pool asid) 29 \<Longrightarrow> asid = 0 \<and> (\<exists>asid. cap = cap.ArchObjectCap (arch_cap.ASIDPoolCap pool asid))" 30 "cap_master_cap cap = cap.ArchObjectCap (arch_cap.PageTableCap ptr data) 31 \<Longrightarrow> data = None \<and> (\<exists>data. cap = cap.ArchObjectCap (arch_cap.PageTableCap ptr data))" 32 "cap_master_cap cap = cap.ArchObjectCap (arch_cap.PageDirectoryCap ptr data2) 33 \<Longrightarrow> data2 = None \<and> (\<exists>data2. cap = cap.ArchObjectCap (arch_cap.PageDirectoryCap ptr data2))" 34 by (clarsimp simp: cap_master_cap_def 35 split: cap.split_asm arch_cap.split_asm)+ 36 37lemmas cap_master_cap_eqDs = 38 cap_master_cap_eqDs1 cap_master_cap_arch_eqDs 39 cap_master_cap_eqDs1 [OF sym] cap_master_cap_arch_eqDs[OF sym] 40 41 42lemma vm_sets_diff[simp]: 43 "vm_read_only \<noteq> vm_read_write" 44 by (simp add: vm_read_write_def vm_read_only_def) 45 46 47lemmas vm_sets_diff2[simp] = not_sym[OF vm_sets_diff] 48 49lemma cap_master_cap_tcb_cap_valid_arch: 50 "\<lbrakk> cap_master_cap c = cap_master_cap c'; is_arch_cap c \<rbrakk> \<Longrightarrow> 51 tcb_cap_valid c p s = tcb_cap_valid c' p s" 52 by (auto simp add: cap_master_cap_def tcb_cap_valid_def tcb_cap_cases_def 53 valid_ipc_buffer_cap_def is_cap_simps 54 is_nondevice_page_cap_simps is_nondevice_page_cap_arch_def 55 split: option.splits cap.splits arch_cap.splits 56 Structures_A.thread_state.splits) 57 58crunch device_state_inv[wp]: invalidateLocalTLB_ASID "\<lambda>ms. P (device_state ms)" 59 (ignore: ignore_failure) 60 61crunch device_state_inv[wp]: invalidateLocalTLB_VAASID "\<lambda>ms. P (device_state ms)" 62crunch device_state_inv[wp]: setHardwareASID "\<lambda>ms. P (device_state ms)" 63crunch device_state_inv[wp]: isb "\<lambda>ms. P (device_state ms)" 64crunch device_state_inv[wp]: dsb "\<lambda>ms. P (device_state ms)" 65crunch device_state_inv[wp]: storeWord "\<lambda>ms. P (device_state ms)" 66crunch device_state_inv[wp]: cleanByVA_PoU "\<lambda>ms. P (device_state ms)" 67crunch device_state_inv[wp]: cleanL2Range "\<lambda>ms. P (device_state ms)" 68 69lemma storeWord_invs[wp, TcbAcc_AI_assms]: 70 "\<lbrace>in_user_frame p and invs\<rbrace> do_machine_op (storeWord p w) \<lbrace>\<lambda>rv. invs\<rbrace>" 71proof - 72 have aligned_offset_ignore: 73 "\<And>l sz. l<4 \<Longrightarrow> p && mask 2 = 0 \<Longrightarrow> 74 p+l && ~~ mask (pageBitsForSize sz) = p && ~~ mask (pageBitsForSize sz)" 75 proof - 76 fix l sz 77 assume al: "p && mask 2 = 0" 78 assume "(l::word32) < 4" hence less: "l<2^2" by simp 79 have le: "2 \<le> pageBitsForSize sz" by (case_tac sz, simp_all) 80 show "?thesis l sz" 81 by (rule is_aligned_add_helper[simplified is_aligned_mask, 82 THEN conjunct2, THEN mask_out_first_mask_some, 83 where n=2, OF al less le]) 84 qed 85 86 show ?thesis 87 apply (wp dmo_invs) 88 apply (clarsimp simp: storeWord_def invs_def valid_state_def) 89 apply (fastforce simp: valid_machine_state_def in_user_frame_def 90 assert_def simpler_modify_def fail_def bind_def return_def 91 pageBits_def aligned_offset_ignore 92 split: if_split_asm) 93 done 94qed 95 96lemma valid_ipc_buffer_cap_0[simp, TcbAcc_AI_assms]: 97 "valid_ipc_buffer_cap cap a \<Longrightarrow> valid_ipc_buffer_cap cap 0" 98 by (auto simp add: valid_ipc_buffer_cap_def case_bool_If 99 split: cap.split arch_cap.split) 100 101lemma thread_set_hyp_refs_trivial [TcbAcc_AI_assms]: 102 assumes x: "\<And>tcb. tcb_state (f tcb) = tcb_state tcb" 103 assumes y: "\<And>tcb. tcb_arch_ref (f tcb) = tcb_arch_ref tcb" 104 shows "\<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace> thread_set f t \<lbrace>\<lambda>rv s. P (state_hyp_refs_of s)\<rbrace>" 105 apply (simp add: thread_set_def set_object_def) 106 apply wp 107 apply (clarsimp dest!: get_tcb_SomeD) 108 apply (clarsimp elim!: rsubst[where P=P]) 109 apply (rule all_ext; 110 clarsimp simp: state_hyp_refs_of_def hyp_refs_of_def tcb_hyp_refs_def get_tcb_def x y[simplified tcb_arch_ref_def]) 111 done 112 113lemma mab_pb [simp]: 114 "msg_align_bits \<le> pageBits" 115 unfolding msg_align_bits pageBits_def by simp 116 117lemma mab_wb [simp]: 118 "msg_align_bits < word_bits" 119 unfolding msg_align_bits word_bits_conv by simp 120 121 122lemma get_cap_valid_ipc [TcbAcc_AI_assms]: 123 "\<lbrace>valid_objs and obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> tcb_ipc_buffer tcb = v) t\<rbrace> 124 get_cap (t, tcb_cnode_index 4) 125 \<lbrace>\<lambda>rv s. valid_ipc_buffer_cap rv v\<rbrace>" 126 apply (wp get_cap_wp) 127 apply clarsimp 128 apply (drule(1) cte_wp_tcb_cap_valid) 129 apply (clarsimp simp add: tcb_cap_valid_def obj_at_def) 130 apply (simp add: valid_ipc_buffer_cap_def mask_cap_def cap_rights_update_def 131 acap_rights_update_def is_tcb 132 split: cap.split_asm arch_cap.split_asm) 133 done 134 135 136 137lemma pred_tcb_cap_wp_at [TcbAcc_AI_assms]: 138 "\<lbrakk>pred_tcb_at proj P t s; valid_objs s; 139 ref \<in> dom tcb_cap_cases; 140 \<forall>cap. (pred_tcb_at proj P t s \<and> tcb_cap_valid cap (t, ref) s) \<longrightarrow> Q cap\<rbrakk> \<Longrightarrow> 141 cte_wp_at Q (t, ref) s" 142 apply (clarsimp simp: cte_wp_at_cases tcb_at_def dest!: get_tcb_SomeD) 143 apply (rename_tac getF setF restr) 144 apply (clarsimp simp: tcb_cap_valid_def pred_tcb_at_def obj_at_def) 145 apply (erule(1) valid_objsE) 146 apply (clarsimp simp add: valid_obj_def valid_tcb_def) 147 apply (erule_tac x="(getF, setF, restr)" in ballE) 148 apply fastforce+ 149 done 150 151lemma as_user_hyp_refs_of[wp, TcbAcc_AI_assms]: 152 "\<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace> 153 as_user t m 154 \<lbrace>\<lambda>rv s. P (state_hyp_refs_of s)\<rbrace>" 155 apply (wp as_user_wp_thread_set_helper 156 thread_set_hyp_refs_trivial | simp)+ 157 done 158 159lemmas sts_typ_ats = sts_typ_ats abs_atyp_at_lifts [OF set_thread_state_typ_at] 160 161lemma arch_tcb_context_set_eq_ARM[TcbAcc_AI_assms]: "arch_tcb_context_set (arch_tcb_context_get t) t = t" 162 unfolding arch_tcb_context_get_def arch_tcb_context_set_def 163 by simp 164 165lemma arch_tcb_context_get_eq_ARM[TcbAcc_AI_assms]: "arch_tcb_context_get (arch_tcb_context_set uc t) = uc" 166 unfolding arch_tcb_context_get_def arch_tcb_context_set_def 167 by simp 168 169lemma arch_tcb_update_aux2: "(\<lambda>tcb. tcb\<lparr> tcb_arch := f (tcb_arch tcb) \<rparr>) = tcb_arch_update f" 170 by (rule ext, simp) 171 172lemma arch_tcb_update_aux3: "tcb\<lparr>tcb_arch := f (tcb_arch tcb)\<rparr> = tcb_arch_update f tcb" 173 by(simp) 174 175lemma tcb_context_update_aux: "arch_tcb_context_set (P (arch_tcb_context_get atcb)) atcb 176 = tcb_context_update (\<lambda>ctx. P ctx) atcb" 177 by (simp add: arch_tcb_context_set_def arch_tcb_context_get_def) 178 179end 180 181global_interpretation TcbAcc_AI?: TcbAcc_AI 182 proof goal_cases 183 interpret Arch . 184 case 1 show ?case by (unfold_locales; (fact TcbAcc_AI_assms)?) 185 qed 186 187end 188