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 ArchTcb_AI 12imports "../Tcb_AI" 13begin 14 15context Arch begin global_naming ARM 16 17named_theorems Tcb_AI_asms 18 19 20lemma activate_idle_invs[Tcb_AI_asms]: 21 "\<lbrace>invs and ct_idle\<rbrace> 22 arch_activate_idle_thread thread 23 \<lbrace>\<lambda>rv. invs and ct_idle\<rbrace>" 24 by (simp add: arch_activate_idle_thread_def) 25 26 27lemma empty_fail_getRegister [intro!, simp, Tcb_AI_asms]: 28 "empty_fail (getRegister r)" 29 by (simp add: getRegister_def) 30 31 32lemma same_object_also_valid: (* arch specific *) 33 "\<lbrakk> same_object_as cap cap'; s \<turnstile> cap'; wellformed_cap cap; 34 cap_asid cap = None \<or> (\<exists>asid. cap_asid cap = Some asid \<and> 0 < asid \<and> asid \<le> 2^asid_bits - 1); 35 cap_vptr cap = None; cap_asid_base cap = None \<rbrakk> 36 \<Longrightarrow> s \<turnstile> cap" 37 apply (cases cap, 38 (clarsimp simp: same_object_as_def is_cap_simps cap_asid_def 39 wellformed_cap_def wellformed_acap_def 40 valid_cap_def bits_of_def cap_aligned_def 41 split: cap.split_asm arch_cap.split_asm option.splits)+) 42 done 43 44lemma same_object_obj_refs[Tcb_AI_asms]: 45 "\<lbrakk> same_object_as cap cap' \<rbrakk> 46 \<Longrightarrow> obj_refs cap = obj_refs cap'" 47 apply (cases cap, simp_all add: same_object_as_def) 48 apply ((clarsimp simp: is_cap_simps bits_of_def same_aobject_as_def 49 split: cap.split_asm )+) 50 by (cases "the_arch_cap cap"; cases "the_arch_cap cap'"; simp) 51 52 53definition 54 is_cnode_or_valid_arch :: "cap \<Rightarrow> bool" 55where 56 "is_cnode_or_valid_arch cap \<equiv> 57 is_cnode_cap cap 58 \<or> (is_arch_cap cap 59 \<and> (is_pt_cap cap \<longrightarrow> cap_asid cap \<noteq> None) 60 \<and> (is_pd_cap cap \<longrightarrow> cap_asid cap \<noteq> None))" 61 62 63definition (* arch specific *) 64 "pt_pd_asid cap \<equiv> case cap of 65 ArchObjectCap (PageTableCap _ (Some (asid, _))) \<Rightarrow> Some asid 66 | ArchObjectCap (PageDirectoryCap _ (Some asid)) \<Rightarrow> Some asid 67 | _ \<Rightarrow> None" 68 69lemmas pt_pd_asid_simps [simp] = (* arch specific *) 70 pt_pd_asid_def [split_simps cap.split arch_cap.split option.split prod.split] 71 72lemma checked_insert_is_derived: (* arch specific *) 73 "\<lbrakk> same_object_as new_cap old_cap; is_cnode_or_valid_arch new_cap; 74 obj_refs new_cap = obj_refs old_cap 75 \<longrightarrow> table_cap_ref old_cap = table_cap_ref new_cap 76 \<and> pt_pd_asid old_cap = pt_pd_asid new_cap\<rbrakk> 77 \<Longrightarrow> is_derived m slot new_cap old_cap" 78 apply (cases slot) 79 apply (frule same_object_as_cap_master) 80 apply (frule master_cap_obj_refs) 81 apply (frule cap_master_eq_badge_none) 82 apply (frule same_master_cap_same_types) 83 apply (simp add: is_derived_def) 84 apply clarsimp 85 apply (auto simp: is_cap_simps cap_master_cap_def 86 is_cnode_or_valid_arch_def vs_cap_ref_def 87 table_cap_ref_def pt_pd_asid_def up_ucast_inj_eq 88 split: cap.split_asm arch_cap.split_asm 89 option.split_asm)[1] 90 done 91 92lemma is_cnode_or_valid_arch_cap_asid: (* arch specific *) 93 "is_cnode_or_valid_arch cap 94 \<Longrightarrow> (is_pt_cap cap \<longrightarrow> cap_asid cap \<noteq> None) 95 \<and> (is_pd_cap cap \<longrightarrow> cap_asid cap \<noteq> None)" 96 by (auto simp add: is_cnode_or_valid_arch_def 97 is_cap_simps) 98 99lemma checked_insert_tcb_invs[wp]: (* arch specific *) 100 "\<lbrace>invs and cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) 101 and K (is_cnode_or_valid_arch new_cap) and valid_cap new_cap 102 and tcb_cap_valid new_cap (target, ref) 103 and K (is_pt_cap new_cap \<or> is_pd_cap new_cap 104 \<longrightarrow> cap_asid new_cap \<noteq> None) 105 and (cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap 106 \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> 107 pt_pd_asid c = pt_pd_asid new_cap) src_slot)\<rbrace> 108 check_cap_at new_cap src_slot 109 (check_cap_at (cap.ThreadCap target) slot 110 (cap_insert new_cap src_slot (target, ref))) \<lbrace>\<lambda>rv. invs\<rbrace>" 111 apply (simp add: check_cap_at_def) 112 apply (rule hoare_pre) 113 apply (wp get_cap_wp) 114 apply (clarsimp simp: cte_wp_at_caps_of_state) 115 apply (frule caps_of_state_valid_cap[where p=src_slot], fastforce) 116 apply (frule caps_of_state_valid_cap[where p=slot], fastforce) 117 apply (rule conjI, simp only: ex_cte_cap_wp_to_def) 118 apply (rule_tac x=slot in exI) 119 apply (clarsimp simp: cte_wp_at_caps_of_state same_object_as_cte_refs) 120 apply (clarsimp simp: same_object_as_def2 cap_master_cap_simps 121 dest!: cap_master_cap_eqDs) 122 apply (clarsimp simp: valid_cap_def[where c="cap.ThreadCap x" for x]) 123 apply (erule cte_wp_atE[OF caps_of_state_cteD]) 124 apply (fastforce simp: obj_at_def is_obj_defs) 125 apply clarsimp 126 apply (rule conjI) 127 apply clarsimp 128 apply (subgoal_tac "\<not> is_zombie new_cap") 129 apply (simp add: same_object_zombies same_object_obj_refs) 130 apply (erule(2) zombies_final_helperE) 131 apply fastforce 132 apply (fastforce simp add: cte_wp_at_caps_of_state) 133 apply assumption 134 apply (clarsimp simp: is_cnode_or_valid_arch_def is_cap_simps 135 is_valid_vtable_root_def) 136 apply (rule conjI) 137 apply (erule(1) checked_insert_is_derived, simp+) 138 apply (auto simp: is_cnode_or_valid_arch_def is_cap_simps) 139 done 140 141crunch tcb_at[wp, Tcb_AI_asms]: arch_get_sanitise_register_info, arch_post_modify_registers "tcb_at a" 142crunch invs[wp, Tcb_AI_asms]: arch_get_sanitise_register_info, arch_post_modify_registers "invs" 143crunch ex_nonz_cap_to[wp, Tcb_AI_asms]: arch_get_sanitise_register_info, arch_post_modify_registers "ex_nonz_cap_to a" 144 145lemma finalise_cap_not_cte_wp_at[Tcb_AI_asms]: 146 assumes x: "P cap.NullCap" 147 shows "\<lbrace>\<lambda>s. \<forall>cp \<in> ran (caps_of_state s). P cp\<rbrace> 148 finalise_cap cap fin 149 \<lbrace>\<lambda>rv s. \<forall>cp \<in> ran (caps_of_state s). P cp\<rbrace>" 150 apply (cases cap, simp_all) 151 apply (wp suspend_caps_of_state hoare_vcg_all_lift 152 | simp 153 | rule impI 154 | rule hoare_drop_imps)+ 155 apply (clarsimp simp: ball_ran_eq x) 156 apply (wp delete_one_caps_of_state 157 | rule impI 158 | simp add: deleting_irq_handler_def get_irq_slot_def x ball_ran_eq)+ 159 done 160 161 162lemma table_cap_ref_max_free_index_upd[simp,Tcb_AI_asms]: 163 "table_cap_ref (max_free_index_update cap) = table_cap_ref cap" 164 by (simp add: free_index_update_def table_cap_ref_def split: cap.splits) 165 166 167interpretation Tcb_AI_1? : Tcb_AI_1 168 where state_ext_t = state_ext_t 169 and is_cnode_or_valid_arch = is_cnode_or_valid_arch 170by (unfold_locales; fact Tcb_AI_asms) 171 172 173lemma use_no_cap_to_obj_asid_strg: (* arch specific *) 174 "(cte_at p s \<and> no_cap_to_obj_dr_emp cap s \<and> valid_cap cap s \<and> invs s) 175 \<longrightarrow> cte_wp_at (\<lambda>c. obj_refs c = obj_refs cap 176 \<longrightarrow> table_cap_ref c = table_cap_ref cap \<and> pt_pd_asid c = pt_pd_asid cap) p s" 177 apply (clarsimp simp: cte_wp_at_caps_of_state 178 no_cap_to_obj_with_diff_ref_def 179 simp del: split_paired_All) 180 apply (frule caps_of_state_valid_cap, fastforce) 181 apply (erule allE)+ 182 apply (erule (1) impE)+ 183 apply (simp add: table_cap_ref_def pt_pd_asid_def split: cap.splits arch_cap.splits option.splits prod.splits) 184 apply (fastforce simp: table_cap_ref_def valid_cap_simps elim!: asid_low_high_bits)+ 185 done 186 187lemma cap_delete_no_cap_to_obj_asid[wp, Tcb_AI_asms]: 188 "\<lbrace>no_cap_to_obj_dr_emp cap\<rbrace> 189 cap_delete slot 190 \<lbrace>\<lambda>rv. no_cap_to_obj_dr_emp cap\<rbrace>" 191 apply (simp add: cap_delete_def 192 no_cap_to_obj_with_diff_ref_ran_caps_form) 193 apply wp 194 apply simp 195 apply (rule use_spec) 196 apply (rule rec_del_all_caps_in_range) 197 apply (simp add: table_cap_ref_def[simplified, split_simps cap.split] 198 | rule obj_ref_none_no_asid)+ 199 done 200 201lemma as_user_valid_cap[wp]: 202 "\<lbrace>valid_cap c\<rbrace> as_user a b \<lbrace>\<lambda>rv. valid_cap c\<rbrace>" 203 by (wp valid_cap_typ) 204 205lemma as_user_ipc_tcb_cap_valid4[wp]: 206 "\<lbrace>\<lambda>s. tcb_cap_valid cap (t, tcb_cnode_index 4) s\<rbrace> 207 as_user a b 208 \<lbrace>\<lambda>rv. tcb_cap_valid cap (t, tcb_cnode_index 4)\<rbrace>" 209 apply (simp add: as_user_def set_object_def) 210 apply (wp | wpc | simp)+ 211 apply (clarsimp simp: tcb_cap_valid_def obj_at_def 212 pred_tcb_at_def is_tcb 213 dest!: get_tcb_SomeD) 214 apply (clarsimp simp: get_tcb_def) 215 done 216 217lemma tc_invs[Tcb_AI_asms]: 218 "\<lbrace>invs and tcb_at a 219 and (case_option \<top> (valid_cap o fst) e) 220 and (case_option \<top> (valid_cap o fst) f) 221 and (case_option \<top> (case_option \<top> (valid_cap o fst) o snd) g) 222 and (case_option \<top> (cte_at o snd) e) 223 and (case_option \<top> (cte_at o snd) f) 224 and (case_option \<top> (case_option \<top> (cte_at o snd) o snd) g) 225 and (case_option \<top> (no_cap_to_obj_dr_emp o fst) e) 226 and (case_option \<top> (no_cap_to_obj_dr_emp o fst) f) 227 and (case_option \<top> (case_option \<top> (no_cap_to_obj_dr_emp o fst) o snd) g) 228 (* only set prio \<le> mcp of authorising thread *) 229 and (\<lambda>s. case_option True (\<lambda>(pr, auth). mcpriority_tcb_at (\<lambda>mcp. pr \<le> mcp) auth s) pr) 230 (* only set mcp \<le> mcp of authorising thread *) 231 and (\<lambda>s. case_option True (\<lambda>(mcp, auth). mcpriority_tcb_at (\<lambda>m. mcp \<le> m) auth s) mcp) 232 and K (case_option True (is_cnode_cap o fst) e) 233 and K (case_option True (is_valid_vtable_root o fst) f) 234 and K (case_option True (\<lambda>v. case_option True 235 ((swp valid_ipc_buffer_cap (fst v) 236 and is_arch_cap and is_cnode_or_valid_arch) 237 o fst) (snd v)) g) 238 and K (case_option True (\<lambda>bl. length bl = word_bits) b)\<rbrace> 239 invoke_tcb (ThreadControl a sl b mcp pr e f g) 240 \<lbrace>\<lambda>rv. invs\<rbrace>" 241 apply (rule hoare_gen_asm)+ 242 apply (simp add: split_def set_mcpriority_def cong: option.case_cong) 243 apply (rule hoare_vcg_precond_imp) 244 apply wp 245 apply ((simp only: simp_thms 246 | rule wp_split_const_if wp_split_const_if_R 247 hoare_vcg_all_lift_R 248 hoare_vcg_E_elim hoare_vcg_const_imp_lift_R 249 hoare_vcg_R_conj 250 | (wp out_invs_trivial case_option_wpE cap_delete_deletes 251 cap_delete_valid_cap cap_insert_valid_cap out_cte_at 252 cap_insert_cte_at cap_delete_cte_at out_valid_cap 253 hoare_vcg_const_imp_lift_R hoare_vcg_all_lift_R 254 thread_set_tcb_ipc_buffer_cap_cleared_invs 255 thread_set_invs_trivial[OF ball_tcb_cap_casesI] 256 hoare_vcg_all_lift thread_set_valid_cap out_emptyable 257 check_cap_inv [where P="valid_cap c" for c] 258 check_cap_inv [where P="tcb_cap_valid c p" for c p] 259 check_cap_inv[where P="cte_at p0" for p0] 260 check_cap_inv[where P="tcb_at p0" for p0] 261 thread_set_cte_at 262 thread_set_cte_wp_at_trivial[where Q="\<lambda>x. x", OF ball_tcb_cap_casesI] 263 thread_set_no_cap_to_trivial[OF ball_tcb_cap_casesI] 264 checked_insert_no_cap_to 265 out_no_cap_to_trivial[OF ball_tcb_cap_casesI] 266 thread_set_ipc_tcb_cap_valid 267 static_imp_wp static_imp_conj_wp)[1] 268 | simp add: ran_tcb_cap_cases dom_tcb_cap_cases[simplified] 269 emptyable_def 270 del: hoare_True_E_R 271 | wpc 272 | strengthen use_no_cap_to_obj_asid_strg 273 tcb_cap_always_valid_strg[where p="tcb_cnode_index 0"] 274 tcb_cap_always_valid_strg[where p="tcb_cnode_index (Suc 0)"])+) 275 apply (clarsimp simp: tcb_at_cte_at_0 tcb_at_cte_at_1[simplified] is_nondevice_page_cap_arch_def 276 is_cap_simps is_valid_vtable_root_def is_nondevice_page_cap_simps 277 is_cnode_or_valid_arch_def tcb_cap_valid_def 278 invs_valid_objs cap_asid_def vs_cap_ref_def 279 split: option.split_asm )+ 280 apply (simp add: case_bool_If valid_ipc_buffer_cap_def is_nondevice_page_cap_simps 281 is_nondevice_page_cap_arch_def 282 split: arch_cap.splits if_splits)+ 283 done 284 285 286lemma check_valid_ipc_buffer_inv: 287 "\<lbrace>P\<rbrace> check_valid_ipc_buffer vptr cap \<lbrace>\<lambda>rv. P\<rbrace>" 288 apply (simp add: check_valid_ipc_buffer_def whenE_def 289 cong: cap.case_cong arch_cap.case_cong 290 split del: if_split) 291 apply (rule hoare_pre) 292 apply (wp | simp add: whenE_def if_apply_def2 | wpcw)+ 293 done 294 295lemma check_valid_ipc_buffer_wp[Tcb_AI_asms]: 296 "\<lbrace>\<lambda>(s::'state_ext::state_ext state). is_arch_cap cap \<and> is_cnode_or_valid_arch cap 297 \<and> valid_ipc_buffer_cap cap vptr 298 \<and> is_aligned vptr msg_align_bits 299 \<longrightarrow> P s\<rbrace> 300 check_valid_ipc_buffer vptr cap 301 \<lbrace>\<lambda>rv. P\<rbrace>,-" 302 apply (simp add: check_valid_ipc_buffer_def whenE_def 303 cong: cap.case_cong arch_cap.case_cong 304 split del: if_split) 305 apply (rule hoare_pre) 306 apply (wp | simp add: whenE_def split del: if_split | wpc)+ 307 apply (clarsimp simp: is_cap_simps is_cnode_or_valid_arch_def 308 valid_ipc_buffer_cap_def) 309 done 310 311lemma derive_no_cap_asid[wp,Tcb_AI_asms]: 312 "\<lbrace>(no_cap_to_obj_with_diff_ref cap S)::'state_ext::state_ext state\<Rightarrow>bool\<rbrace> 313 derive_cap slot cap 314 \<lbrace>\<lambda>rv. no_cap_to_obj_with_diff_ref rv S\<rbrace>,-" 315 apply (simp add: derive_cap_def arch_derive_cap_def 316 cong: cap.case_cong) 317 apply (rule hoare_pre) 318 apply (wp | simp | wpc)+ 319 apply (auto simp add: no_cap_to_obj_with_diff_ref_Null, 320 auto simp add: no_cap_to_obj_with_diff_ref_def 321 table_cap_ref_def) 322 done 323 324 325lemma decode_set_ipc_inv[wp,Tcb_AI_asms]: 326 "\<lbrace>P::'state_ext::state_ext state \<Rightarrow> bool\<rbrace> decode_set_ipc_buffer args cap slot excaps \<lbrace>\<lambda>rv. P\<rbrace>" 327 apply (simp add: decode_set_ipc_buffer_def whenE_def 328 split_def 329 split del: if_split) 330 apply (rule hoare_pre, wp check_valid_ipc_buffer_inv) 331 apply simp 332 done 333 334lemma no_cap_to_obj_with_diff_ref_update_cap_data[Tcb_AI_asms]: 335 "no_cap_to_obj_with_diff_ref c S s \<longrightarrow> 336 no_cap_to_obj_with_diff_ref (update_cap_data P x c) S s" 337 apply (case_tac "update_cap_data P x c = NullCap") 338 apply (simp add: no_cap_to_obj_with_diff_ref_Null) 339 apply (subgoal_tac "vs_cap_ref (update_cap_data P x c) 340 = vs_cap_ref c") 341 apply (simp add: no_cap_to_obj_with_diff_ref_def 342 update_cap_objrefs) 343 apply (clarsimp simp: update_cap_data_closedform 344 table_cap_ref_def 345 arch_update_cap_data_def 346 split: cap.split) 347 apply simp 348 done 349 350 351lemma update_cap_valid[Tcb_AI_asms]: 352 "valid_cap cap (s::'state_ext::state_ext state) \<Longrightarrow> 353 valid_cap (case capdata of 354 None \<Rightarrow> cap_rights_update rs cap 355 | Some x \<Rightarrow> update_cap_data p x 356 (cap_rights_update rs cap)) s" 357 apply (case_tac capdata, simp_all)[1] 358 apply (case_tac cap, 359 simp_all add: update_cap_data_def cap_rights_update_def 360 is_cap_defs Let_def split_def valid_cap_def 361 badge_update_def the_cnode_cap_def cap_aligned_def 362 arch_update_cap_data_def 363 split del: if_split) 364 apply (simp add: badge_update_def cap_rights_update_def) 365 apply (simp add: badge_update_def) 366 apply (simp add: word_bits_def) 367 apply (rename_tac arch_cap) 368 using valid_validate_vm_rights[simplified valid_vm_rights_def] 369 apply (case_tac arch_cap, simp_all add: acap_rights_update_def 370 split: option.splits prod.splits) 371 done 372 373 374crunch pred_tcb_at: switch_to_thread "pred_tcb_at proj P t" 375 (wp: crunch_wps simp: crunch_simps) 376 377crunch typ_at[wp]: invoke_tcb "\<lambda>s. P (typ_at T p s)" 378 (ignore: check_cap_at setNextPC zipWithM 379 wp: hoare_drop_imps mapM_x_wp' check_cap_inv 380 simp: crunch_simps) 381 382end 383 384context begin interpretation Arch . 385requalify_consts is_cnode_or_valid_arch 386requalify_facts invoke_tcb_typ_at 387end 388 389global_interpretation Tcb_AI?: Tcb_AI 390 where is_cnode_or_valid_arch = ARM.is_cnode_or_valid_arch 391 proof goal_cases 392 interpret Arch . 393 case 1 show ?case 394 by (unfold_locales; fact Tcb_AI_asms) 395qed 396 397end 398