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 Finalise_C 12imports IpcCancel_C 13begin 14 15context kernel_m 16begin 17 18declare if_split [split del] 19 20lemma empty_fail_getEndpoint: 21 "empty_fail (getEndpoint ep)" 22 unfolding getEndpoint_def 23 by (auto intro: empty_fail_getObject) 24 25definition 26 "option_map2 f m = option_map f \<circ> m" 27 28lemma tcbSchedEnqueue_cslift_spec: 29 "\<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> \<lbrace>s. \<exists>d v. option_map2 tcbPriority_C (cslift s) \<acute>tcb = Some v 30 \<and> v \<le> ucast maxPrio 31 \<and> option_map2 tcbDomain_C (cslift s) \<acute>tcb = Some d 32 \<and> d \<le> ucast maxDom 33 \<and> (end_C (index \<acute>ksReadyQueues (unat (d*0x100 + v))) \<noteq> NULL 34 \<longrightarrow> option_map2 tcbPriority_C (cslift s) 35 (head_C (index \<acute>ksReadyQueues (unat (d*0x100 + v)))) 36 \<noteq> None 37 \<and> option_map2 tcbDomain_C (cslift s) 38 (head_C (index \<acute>ksReadyQueues (unat (d*0x100 + v)))) 39 \<noteq> None)\<rbrace> 40 Call tcbSchedEnqueue_'proc 41 {s'. option_map2 tcbEPNext_C (cslift s') = option_map2 tcbEPNext_C (cslift s) 42 \<and> option_map2 tcbEPPrev_C (cslift s') = option_map2 tcbEPPrev_C (cslift s) 43 \<and> option_map2 tcbPriority_C (cslift s') = option_map2 tcbPriority_C (cslift s) 44 \<and> option_map2 tcbDomain_C (cslift s') = option_map2 tcbDomain_C (cslift s)}" 45 apply (hoare_rule HoarePartial.ProcNoRec1) 46 apply (rule allI, rule conseqPre, vcg) 47 apply (clarsimp simp: option_map2_def fun_eq_iff h_t_valid_clift 48 h_t_valid_field[OF h_t_valid_clift]) 49 apply (rule conjI) 50 apply (clarsimp simp: typ_heap_simps cong: if_cong) 51 apply (simp split: if_split) 52 apply (clarsimp simp: typ_heap_simps if_Some_helper cong: if_cong) 53 by (simp split: if_split) 54 55lemma setThreadState_cslift_spec: 56 "\<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> \<lbrace>s. s \<Turnstile>\<^sub>c \<acute>tptr \<and> (\<forall>x. ksSchedulerAction_' (globals s) = tcb_Ptr x 57 \<and> x \<noteq> 0 \<and> x \<noteq> 1 58 \<longrightarrow> (\<exists>d v. option_map2 tcbPriority_C (cslift s) (tcb_Ptr x) = Some v 59 \<and> v \<le> ucast maxPrio 60 \<and> option_map2 tcbDomain_C (cslift s) (tcb_Ptr x) = Some d 61 \<and> d \<le> ucast maxDom 62 \<and> (end_C (index \<acute>ksReadyQueues (unat (d*0x100 + v))) \<noteq> NULL 63 \<longrightarrow> option_map2 tcbPriority_C (cslift s) 64 (head_C (index \<acute>ksReadyQueues (unat (d*0x100 + v)))) 65 \<noteq> None 66 \<and> option_map2 tcbDomain_C (cslift s) 67 (head_C (index \<acute>ksReadyQueues (unat (d*0x100 + v)))) 68 \<noteq> None)))\<rbrace> 69 Call setThreadState_'proc 70 {s'. option_map2 tcbEPNext_C (cslift s') = option_map2 tcbEPNext_C (cslift s) 71 \<and> option_map2 tcbEPPrev_C (cslift s') = option_map2 tcbEPPrev_C (cslift s) 72 \<and> option_map2 tcbPriority_C (cslift s') = option_map2 tcbPriority_C (cslift s) 73 \<and> option_map2 tcbDomain_C (cslift s') = option_map2 tcbDomain_C (cslift s) 74 \<and> ksReadyQueues_' (globals s') = ksReadyQueues_' (globals s)}" 75 apply (rule allI, rule conseqPre) 76 apply vcg_step 77 apply vcg_step 78 apply vcg_step 79 apply vcg_step 80 apply vcg_step 81 apply vcg_step 82 apply vcg_step 83 apply (vcg exspec=tcbSchedEnqueue_cslift_spec) 84 apply (vcg_step+)[2] 85 apply vcg_step 86 apply (vcg exspec=isRunnable_modifies) 87 apply vcg 88 apply vcg_step 89 apply vcg_step 90 apply (vcg_step+)[1] 91 apply vcg 92 apply vcg_step+ 93 apply (clarsimp simp: typ_heap_simps h_t_valid_clift_Some_iff 94 fun_eq_iff option_map2_def if_1_0_0) 95 by (simp split: if_split) 96 97lemma ep_queue_relation_shift: 98 "(option_map2 tcbEPNext_C (cslift s') 99 = option_map2 tcbEPNext_C (cslift s) 100 \<and> option_map2 tcbEPPrev_C (cslift s') 101 = option_map2 tcbEPPrev_C (cslift s)) 102 \<longrightarrow> ep_queue_relation (cslift s') ts qPrev qHead 103 = ep_queue_relation (cslift s) ts qPrev qHead" 104 apply clarsimp 105 apply (induct ts arbitrary: qPrev qHead) 106 apply simp 107 apply simp 108 apply (simp add: option_map2_def fun_eq_iff 109 map_option_case) 110 apply (drule_tac x=qHead in spec)+ 111 apply (clarsimp split: option.split_asm) 112 done 113 114lemma rf_sr_cscheduler_relation: 115 "(s, s') \<in> rf_sr \<Longrightarrow> cscheduler_action_relation 116 (ksSchedulerAction s) (ksSchedulerAction_' (globals s'))" 117 by (clarsimp simp: rf_sr_def cstate_relation_def Let_def) 118 119lemma obj_at_ko_at2': 120 "\<lbrakk> obj_at' P p s; ko_at' ko p s \<rbrakk> \<Longrightarrow> P ko" 121 apply (drule obj_at_ko_at') 122 apply clarsimp 123 apply (drule ko_at_obj_congD', simp+) 124 done 125 126lemma ctcb_relation_tcbDomain: 127 "ctcb_relation tcb tcb' \<Longrightarrow> ucast (tcbDomain tcb) = tcbDomain_C tcb'" 128 by (simp add: ctcb_relation_def) 129 130lemma ctcb_relation_tcbPriority: 131 "ctcb_relation tcb tcb' \<Longrightarrow> ucast (tcbPriority tcb) = tcbPriority_C tcb'" 132 by (simp add: ctcb_relation_def) 133 134lemma ctcb_relation_tcbDomain_maxDom: 135 "\<lbrakk> ctcb_relation tcb tcb'; tcbDomain tcb \<le> maxDomain \<rbrakk> \<Longrightarrow> tcbDomain_C tcb' \<le> ucast maxDom" 136 apply (subst ctcb_relation_tcbDomain[symmetric], simp) 137 apply (subst ucast_le_migrate) 138 apply ((simp add:maxDom_def word_size)+)[2] 139 apply (simp add: ucast_up_ucast is_up_def source_size_def word_size target_size_def) 140 apply (simp add: maxDom_to_H) 141 done 142 143lemma ctcb_relation_tcbPriority_maxPrio: 144 "\<lbrakk> ctcb_relation tcb tcb'; tcbPriority tcb \<le> maxPriority \<rbrakk> 145 \<Longrightarrow> tcbPriority_C tcb' \<le> ucast maxPrio" 146 apply (subst ctcb_relation_tcbPriority[symmetric], simp) 147 apply (subst ucast_le_migrate) 148 apply ((simp add: seL4_MaxPrio_def word_size)+)[2] 149 apply (simp add: ucast_up_ucast is_up_def source_size_def word_size target_size_def) 150 apply (simp add: maxPrio_to_H) 151 done 152 153lemma tcbSchedEnqueue_cslift_precond_discharge: 154 "\<lbrakk> (s, s') \<in> rf_sr; obj_at' (P :: tcb \<Rightarrow> bool) x s; 155 valid_queues s; valid_objs' s \<rbrakk> \<Longrightarrow> 156 (\<exists>d v. option_map2 tcbPriority_C (cslift s') (tcb_ptr_to_ctcb_ptr x) = Some v 157 \<and> v \<le> ucast maxPrio 158 \<and> option_map2 tcbDomain_C (cslift s') (tcb_ptr_to_ctcb_ptr x) = Some d 159 \<and> d \<le> ucast maxDom 160 \<and> (end_C (index (ksReadyQueues_' (globals s')) (unat (d*0x100 + v))) \<noteq> NULL 161 \<longrightarrow> option_map2 tcbPriority_C (cslift s') 162 (head_C (index (ksReadyQueues_' (globals s')) (unat (d*0x100 + v)))) 163 \<noteq> None 164 \<and> option_map2 tcbDomain_C (cslift s') 165 (head_C (index (ksReadyQueues_' (globals s')) (unat (d*0x100 + v)))) 166 \<noteq> None))" 167 apply (drule(1) obj_at_cslift_tcb) 168 apply (clarsimp simp: typ_heap_simps' option_map2_def) 169 apply (frule_tac t=x in valid_objs'_maxPriority, fastforce simp: obj_at'_def) 170 apply (frule_tac t=x in valid_objs'_maxDomain, fastforce simp: obj_at'_def) 171 apply (drule_tac P="\<lambda>tcb. tcbPriority tcb \<le> maxPriority" in obj_at_ko_at2', simp) 172 apply (drule_tac P="\<lambda>tcb. tcbDomain tcb \<le> maxDomain" in obj_at_ko_at2', simp) 173 174 apply (simp add: ctcb_relation_tcbDomain_maxDom ctcb_relation_tcbPriority_maxPrio) 175 apply (frule_tac d="tcbDomain ko" and p="tcbPriority ko" 176 in rf_sr_sched_queue_relation) 177 apply (simp add: maxDom_to_H maxPrio_to_H)+ 178 apply (simp add: cready_queues_index_to_C_def2 numPriorities_def) 179 apply (clarsimp simp: ctcb_relation_def) 180 apply (frule arg_cong[where f=unat], subst(asm) unat_ucast_8_32) 181 apply (frule tcb_queue'_head_end_NULL) 182 apply (erule conjunct1[OF valid_queues_valid_q]) 183 apply (frule(1) tcb_queue_relation_qhead_valid') 184 apply (simp add: valid_queues_valid_q) 185 apply (clarsimp simp: h_t_valid_clift_Some_iff) 186 done 187 188lemma cancel_all_ccorres_helper: 189 "ccorres dc xfdc 190 (\<lambda>s. valid_objs' s \<and> valid_queues s 191 \<and> (\<forall>t\<in>set ts. tcb_at' t s \<and> t \<noteq> 0) 192 \<and> sch_act_wf (ksSchedulerAction s) s) 193 {s'. \<exists>p. ep_queue_relation (cslift s') ts 194 p (thread_' s')} hs 195 (mapM_x (\<lambda>t. do 196 y \<leftarrow> setThreadState Restart t; 197 tcbSchedEnqueue t 198 od) ts) 199 (WHILE \<acute>thread \<noteq> tcb_Ptr 0 DO 200 (CALL setThreadState(\<acute>thread, scast ThreadState_Restart));; 201 (CALL tcbSchedEnqueue(\<acute>thread));; 202 Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>thread\<rbrace> 203 (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (Ptr &(\<acute>thread\<rightarrow>[''tcbEPNext_C'']) :: tcb_C ptr ptr)) 204 OD)" 205 unfolding whileAnno_def 206proof (induct ts) 207 case Nil 208 show ?case 209 apply (simp del: Collect_const) 210 apply (rule iffD1 [OF ccorres_expand_while_iff]) 211 apply (rule ccorres_tmp_lift2[where G'=UNIV and G''="\<lambda>x. UNIV", simplified]) 212 apply ceqv 213 apply (simp add: ccorres_cond_iffs mapM_x_def sequence_x_def 214 dc_def[symmetric]) 215 apply (rule ccorres_guard_imp2, rule ccorres_return_Skip) 216 apply simp 217 done 218next 219 case (Cons thread threads) 220 show ?case 221 apply (rule iffD1 [OF ccorres_expand_while_iff]) 222 apply (simp del: Collect_const 223 add: dc_def[symmetric] mapM_x_Cons) 224 apply (rule ccorres_guard_imp2) 225 apply (rule_tac xf'=thread_' in ccorres_abstract) 226 apply ceqv 227 apply (rule_tac P="rv' = tcb_ptr_to_ctcb_ptr thread" 228 in ccorres_gen_asm2) 229 apply (rule_tac P="tcb_ptr_to_ctcb_ptr thread \<noteq> Ptr 0" 230 in ccorres_gen_asm) 231 apply (clarsimp simp add: Collect_True ccorres_cond_iffs 232 simp del: Collect_const) 233 apply (rule_tac r'=dc and xf'=xfdc in ccorres_split_nothrow[where F=UNIV]) 234 apply (intro ccorres_rhs_assoc) 235 apply (ctac(no_vcg) add: setThreadState_ccorres) 236 apply (rule ccorres_add_return2) 237 apply (ctac(no_vcg) add: tcbSchedEnqueue_ccorres) 238 apply (rule_tac P="tcb_at' thread" 239 in ccorres_from_vcg[where P'=UNIV]) 240 apply (rule allI, rule conseqPre, vcg) 241 apply (clarsimp simp: return_def) 242 apply (drule obj_at_ko_at', clarsimp) 243 apply (erule cmap_relationE1 [OF cmap_relation_tcb]) 244 apply (erule ko_at_projectKO_opt) 245 apply (fastforce intro: typ_heap_simps) 246 apply (wp sts_running_valid_queues | simp)+ 247 apply (rule ceqv_refl) 248 apply (rule "Cons.hyps") 249 apply (wp sts_valid_objs' sts_sch_act sch_act_wf_lift hoare_vcg_const_Ball_lift 250 sts_running_valid_queues sts_st_tcb' setThreadState_oa_queued | simp)+ 251 252 apply (vcg exspec=setThreadState_cslift_spec exspec=tcbSchedEnqueue_cslift_spec) 253 apply (clarsimp simp: tcb_at_not_NULL 254 Collect_const_mem valid_tcb_state'_def 255 ThreadState_Restart_def mask_def 256 valid_objs'_maxDomain valid_objs'_maxPriority) 257 apply (drule(1) obj_at_cslift_tcb) 258 apply (clarsimp simp: typ_heap_simps) 259 apply (rule conjI) 260 apply clarsimp 261 apply (frule rf_sr_cscheduler_relation) 262 apply (clarsimp simp: cscheduler_action_relation_def 263 st_tcb_at'_def 264 split: scheduler_action.split_asm) 265 apply (rename_tac word) 266 apply (frule_tac x=word in tcbSchedEnqueue_cslift_precond_discharge) 267 apply simp 268 apply clarsimp 269 apply clarsimp 270 apply clarsimp 271 apply clarsimp 272 apply (rule conjI) 273 apply (frule(3) tcbSchedEnqueue_cslift_precond_discharge) 274 apply clarsimp 275 apply clarsimp 276 apply (subst ep_queue_relation_shift, fastforce) 277 apply (drule_tac x="tcb_ptr_to_ctcb_ptr thread" 278 in fun_cong)+ 279 apply (clarsimp simp add: option_map2_def typ_heap_simps) 280 apply fastforce 281 done 282qed 283 284lemma cancelAllIPC_ccorres: 285 "ccorres dc xfdc 286 (invs') (UNIV \<inter> {s. epptr_' s = Ptr epptr}) [] 287 (cancelAllIPC epptr) (Call cancelAllIPC_'proc)" 288 apply (cinit lift: epptr_') 289 apply (rule ccorres_symb_exec_l [OF _ getEndpoint_inv _ empty_fail_getEndpoint]) 290 apply (rule_tac xf'=ret__unsigned_' 291 and val="case rv of IdleEP \<Rightarrow> scast EPState_Idle 292 | RecvEP _ \<Rightarrow> scast EPState_Recv | SendEP _ \<Rightarrow> scast EPState_Send" 293 and R="ko_at' rv epptr" 294 in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV]) 295 apply vcg 296 apply clarsimp 297 apply (erule cmap_relationE1 [OF cmap_relation_ep]) 298 apply (erule ko_at_projectKO_opt) 299 apply (clarsimp simp add: typ_heap_simps) 300 apply (simp add: cendpoint_relation_def Let_def 301 split: endpoint.split_asm) 302 apply ceqv 303 apply (rule_tac A="invs' and ko_at' rv epptr" 304 in ccorres_guard_imp2[where A'=UNIV]) 305 apply wpc 306 apply (rename_tac list) 307 apply (simp add: endpoint_state_defs 308 Collect_False Collect_True 309 ccorres_cond_iffs 310 del: Collect_const) 311 apply (rule ccorres_rhs_assoc)+ 312 apply csymbr 313 apply (rule ccorres_abstract_cleanup) 314 apply csymbr 315 apply (rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2) 316 apply (rule_tac r'=dc and xf'=xfdc 317 in ccorres_split_nothrow) 318 apply (rule_tac P="ko_at' (RecvEP list) epptr and invs'" 319 in ccorres_from_vcg[where P'=UNIV]) 320 apply (rule allI, rule conseqPre, vcg) 321 apply clarsimp 322 apply (rule cmap_relationE1 [OF cmap_relation_ep]) 323 apply assumption 324 apply (erule ko_at_projectKO_opt) 325 apply (clarsimp simp: typ_heap_simps setEndpoint_def) 326 apply (rule rev_bexI) 327 apply (rule setObject_eq; simp add: objBits_simps')[1] 328 apply (clarsimp simp: rf_sr_def cstate_relation_def 329 Let_def carch_state_relation_def carch_globals_def 330 cmachine_state_relation_def) 331 apply (clarsimp simp: cpspace_relation_def 332 update_ep_map_tos typ_heap_simps') 333 apply (erule(2) cpspace_relation_ep_update_ep) 334 subgoal by (simp add: cendpoint_relation_def endpoint_state_defs) 335 subgoal by simp 336 apply (rule ceqv_refl) 337 apply (simp only: ccorres_seq_skip dc_def[symmetric]) 338 apply (rule ccorres_split_nothrow_novcg) 339 apply (rule cancel_all_ccorres_helper) 340 apply ceqv 341 apply (ctac add: rescheduleRequired_ccorres) 342 apply (wp weak_sch_act_wf_lift_linear 343 cancelAllIPC_mapM_x_valid_queues 344 | simp)+ 345 apply (rule mapM_x_wp', wp)+ 346 apply (wp sts_st_tcb') 347 apply (clarsimp split: if_split) 348 apply (rule mapM_x_wp', wp)+ 349 apply (clarsimp simp: valid_tcb_state'_def) 350 apply (simp add: guard_is_UNIV_def) 351 apply (wp set_ep_valid_objs' hoare_vcg_const_Ball_lift 352 weak_sch_act_wf_lift_linear) 353 apply vcg 354 apply (simp add: ccorres_cond_iffs dc_def[symmetric]) 355 apply (rule ccorres_return_Skip) 356 apply (rename_tac list) 357 apply (simp add: endpoint_state_defs 358 Collect_False Collect_True 359 ccorres_cond_iffs dc_def[symmetric] 360 del: Collect_const) 361 apply (rule ccorres_rhs_assoc)+ 362 apply csymbr 363 apply (rule ccorres_abstract_cleanup) 364 apply csymbr 365 apply (rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2) 366 apply (rule_tac r'=dc and xf'=xfdc 367 in ccorres_split_nothrow) 368 apply (rule_tac P="ko_at' (SendEP list) epptr and invs'" 369 in ccorres_from_vcg[where P'=UNIV]) 370 apply (rule allI, rule conseqPre, vcg) 371 apply clarsimp 372 apply (rule cmap_relationE1 [OF cmap_relation_ep]) 373 apply assumption 374 apply (erule ko_at_projectKO_opt) 375 apply (clarsimp simp: typ_heap_simps setEndpoint_def) 376 apply (rule rev_bexI) 377 apply (rule setObject_eq, simp_all add: objBits_simps')[1] 378 apply (clarsimp simp: rf_sr_def cstate_relation_def 379 Let_def carch_state_relation_def carch_globals_def 380 cmachine_state_relation_def) 381 apply (clarsimp simp: cpspace_relation_def typ_heap_simps' 382 update_ep_map_tos) 383 apply (erule(2) cpspace_relation_ep_update_ep) 384 subgoal by (simp add: cendpoint_relation_def endpoint_state_defs) 385 subgoal by simp 386 apply (rule ceqv_refl) 387 apply (simp only: ccorres_seq_skip dc_def[symmetric]) 388 apply (rule ccorres_split_nothrow_novcg) 389 apply (rule cancel_all_ccorres_helper) 390 apply ceqv 391 apply (ctac add: rescheduleRequired_ccorres) 392 apply (wp cancelAllIPC_mapM_x_valid_queues) 393 apply (wp mapM_x_wp' weak_sch_act_wf_lift_linear 394 sts_st_tcb' | clarsimp simp: valid_tcb_state'_def split: if_split)+ 395 apply (simp add: guard_is_UNIV_def) 396 apply (wp set_ep_valid_objs' hoare_vcg_const_Ball_lift 397 weak_sch_act_wf_lift_linear) 398 apply vcg 399 apply (clarsimp simp: valid_ep'_def invs_valid_objs' invs_queues) 400 apply (rule cmap_relationE1[OF cmap_relation_ep], assumption) 401 apply (erule ko_at_projectKO_opt) 402 apply (frule obj_at_valid_objs', clarsimp+) 403 apply (clarsimp simp: projectKOs valid_obj'_def valid_ep'_def) 404 subgoal by (auto simp: typ_heap_simps cendpoint_relation_def 405 Let_def tcb_queue_relation'_def 406 invs_valid_objs' valid_objs'_maxDomain valid_objs'_maxPriority 407 intro!: obj_at_conj') 408 apply (clarsimp simp: guard_is_UNIV_def) 409 apply (wp getEndpoint_wp) 410 apply clarsimp 411 done 412 413lemma empty_fail_getNotification: 414 "empty_fail (getNotification ep)" 415 unfolding getNotification_def 416 by (auto intro: empty_fail_getObject) 417 418lemma cancelAllSignals_ccorres: 419 "ccorres dc xfdc 420 (invs') (UNIV \<inter> {s. ntfnPtr_' s = Ptr ntfnptr}) [] 421 (cancelAllSignals ntfnptr) (Call cancelAllSignals_'proc)" 422 apply (cinit lift: ntfnPtr_') 423 apply (rule ccorres_symb_exec_l [OF _ get_ntfn_inv' _ empty_fail_getNotification]) 424 apply (rule_tac xf'=ret__unsigned_' 425 and val="case ntfnObj rv of IdleNtfn \<Rightarrow> scast NtfnState_Idle 426 | ActiveNtfn _ \<Rightarrow> scast NtfnState_Active | WaitingNtfn _ \<Rightarrow> scast NtfnState_Waiting" 427 and R="ko_at' rv ntfnptr" 428 in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV]) 429 apply vcg 430 apply clarsimp 431 apply (erule cmap_relationE1 [OF cmap_relation_ntfn]) 432 apply (erule ko_at_projectKO_opt) 433 apply (clarsimp simp add: typ_heap_simps) 434 apply (simp add: cnotification_relation_def Let_def 435 split: ntfn.split_asm) 436 apply ceqv 437 apply (rule_tac A="invs' and ko_at' rv ntfnptr" 438 in ccorres_guard_imp2[where A'=UNIV]) 439 apply wpc 440 apply (simp add: notification_state_defs ccorres_cond_iffs 441 dc_def[symmetric]) 442 apply (rule ccorres_return_Skip) 443 apply (simp add: notification_state_defs ccorres_cond_iffs 444 dc_def[symmetric]) 445 apply (rule ccorres_return_Skip) 446 apply (rename_tac list) 447 apply (simp add: notification_state_defs ccorres_cond_iffs 448 dc_def[symmetric] Collect_True 449 del: Collect_const) 450 apply (rule ccorres_rhs_assoc)+ 451 apply csymbr 452 apply (rule ccorres_abstract_cleanup) 453 apply csymbr 454 apply (rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2) 455 apply (rule_tac r'=dc and xf'=xfdc in ccorres_split_nothrow) 456 apply (rule_tac P="ko_at' rv ntfnptr and invs'" 457 in ccorres_from_vcg[where P'=UNIV]) 458 apply (rule allI, rule conseqPre, vcg) 459 apply clarsimp 460 apply (rule_tac x=ntfnptr in cmap_relationE1 [OF cmap_relation_ntfn], assumption) 461 apply (erule ko_at_projectKO_opt) 462 apply (clarsimp simp: typ_heap_simps setNotification_def) 463 apply (rule rev_bexI) 464 apply (rule setObject_eq, simp_all add: objBits_simps')[1] 465 apply (clarsimp simp: rf_sr_def cstate_relation_def 466 Let_def carch_state_relation_def carch_globals_def 467 cmachine_state_relation_def) 468 apply (clarsimp simp: cpspace_relation_def typ_heap_simps' 469 update_ntfn_map_tos) 470 apply (erule(2) cpspace_relation_ntfn_update_ntfn) 471 subgoal by (simp add: cnotification_relation_def notification_state_defs Let_def) 472 subgoal by simp 473 apply (rule ceqv_refl) 474 apply (simp only: ccorres_seq_skip dc_def[symmetric]) 475 apply (rule ccorres_split_nothrow_novcg) 476 apply (rule cancel_all_ccorres_helper) 477 apply ceqv 478 apply (ctac add: rescheduleRequired_ccorres) 479 apply (wp cancelAllIPC_mapM_x_valid_queues) 480 apply (wp mapM_x_wp' weak_sch_act_wf_lift_linear 481 sts_st_tcb' | clarsimp simp: valid_tcb_state'_def split: if_split)+ 482 apply (simp add: guard_is_UNIV_def) 483 apply (wp set_ntfn_valid_objs' hoare_vcg_const_Ball_lift 484 weak_sch_act_wf_lift_linear) 485 apply vcg 486 apply clarsimp 487 apply (rule cmap_relationE1[OF cmap_relation_ntfn], assumption) 488 apply (erule ko_at_projectKO_opt) 489 apply (frule obj_at_valid_objs', clarsimp+) 490 apply (clarsimp simp add: valid_obj'_def valid_ntfn'_def projectKOs) 491 subgoal by (auto simp: typ_heap_simps cnotification_relation_def 492 Let_def tcb_queue_relation'_def 493 invs_valid_objs' valid_objs'_maxDomain valid_objs'_maxPriority 494 intro!: obj_at_conj') 495 apply (clarsimp simp: guard_is_UNIV_def) 496 apply (wp getNotification_wp) 497 apply clarsimp 498 done 499 500lemma tcb_queue_concat: 501 "tcb_queue_relation getNext getPrev mp (xs @ z # ys) qprev qhead 502 \<Longrightarrow> tcb_queue_relation getNext getPrev mp (z # ys) 503 (tcb_ptr_to_ctcb_ptr (last ((ctcb_ptr_to_tcb_ptr qprev) # xs))) (tcb_ptr_to_ctcb_ptr z)" 504 apply (induct xs arbitrary: qprev qhead) 505 apply clarsimp 506 apply clarsimp 507 apply (elim meta_allE, drule(1) meta_mp) 508 apply (clarsimp cong: if_cong) 509 done 510 511lemma tcb_fields_ineq_helper: 512 "\<lbrakk> tcb_at' (ctcb_ptr_to_tcb_ptr x) s; tcb_at' (ctcb_ptr_to_tcb_ptr y) s \<rbrakk> \<Longrightarrow> 513 &(x\<rightarrow>[''tcbSchedPrev_C'']) \<noteq> &(y\<rightarrow>[''tcbSchedNext_C''])" 514 apply (clarsimp dest!: tcb_aligned'[OF obj_at'_weakenE, OF _ TrueI] 515 ctcb_ptr_to_tcb_ptr_aligned) 516 apply (clarsimp simp: field_lvalue_def ctcb_size_bits_def) 517 apply (subgoal_tac "is_aligned (ptr_val y - ptr_val x) 8") 518 apply (drule sym, fastforce simp: is_aligned_def dvd_def) 519 apply (erule(1) aligned_sub_aligned) 520 apply (simp add: word_bits_conv) 521 done 522 523end 524 525primrec 526 tcb_queue_relation2 :: "(tcb_C \<Rightarrow> tcb_C ptr) \<Rightarrow> (tcb_C \<Rightarrow> tcb_C ptr) 527 \<Rightarrow> (tcb_C ptr \<rightharpoonup> tcb_C) \<Rightarrow> tcb_C ptr list 528 \<Rightarrow> tcb_C ptr \<Rightarrow> tcb_C ptr \<Rightarrow> bool" 529where 530 "tcb_queue_relation2 getNext getPrev hp [] before after = True" 531| "tcb_queue_relation2 getNext getPrev hp (x # xs) before after = 532 (\<exists>tcb. hp x = Some tcb \<and> getPrev tcb = before 533 \<and> getNext tcb = hd (xs @ [after]) 534 \<and> tcb_queue_relation2 getNext getPrev hp xs x after)" 535 536lemma use_tcb_queue_relation2: 537 "tcb_queue_relation getNext getPrev hp xs qprev qhead 538 = (tcb_queue_relation2 getNext getPrev hp 539 (map tcb_ptr_to_ctcb_ptr xs) qprev (tcb_Ptr 0) 540 \<and> qhead = (hd (map tcb_ptr_to_ctcb_ptr xs @ [tcb_Ptr 0])))" 541 apply (induct xs arbitrary: qhead qprev) 542 apply simp 543 apply (simp add: conj_comms cong: conj_cong) 544 done 545 546lemma tcb_queue_relation2_concat: 547 "tcb_queue_relation2 getNext getPrev hp 548 (xs @ ys) before after 549 = (tcb_queue_relation2 getNext getPrev hp 550 xs before (hd (ys @ [after])) 551 \<and> tcb_queue_relation2 getNext getPrev hp 552 ys (last (before # xs)) after)" 553 apply (induct xs arbitrary: before) 554 apply simp 555 apply (rename_tac x xs before) 556 apply (simp split del: if_split) 557 apply (case_tac "hp x") 558 apply simp 559 apply simp 560 done 561 562lemma tcb_queue_relation2_cong: 563 "\<lbrakk>queue = queue'; before = before'; after = after'; 564 \<And>p. p \<in> set queue' \<Longrightarrow> mp p = mp' p\<rbrakk> 565 \<Longrightarrow> tcb_queue_relation2 getNext getPrev mp queue before after = 566 tcb_queue_relation2 getNext getPrev mp' queue' before' after'" 567 using [[hypsubst_thin = true]] 568 apply clarsimp 569 apply (induct queue' arbitrary: before') 570 apply simp+ 571 done 572 573context kernel_m begin 574 575lemma setThreadState_ccorres_valid_queues'_simple: 576 "ccorres dc xfdc (\<lambda>s. tcb_at' thread s \<and> valid_queues' s \<and> \<not> runnable' st \<and> sch_act_simple s) 577 ({s'. (\<forall>cl fl. cthread_state_relation_lifted st (cl\<lparr>tsType_CL := ts_' s' && mask 4\<rparr>, fl))} 578 \<inter> {s. tptr_' s = tcb_ptr_to_ctcb_ptr thread}) [] 579 (setThreadState st thread) (Call setThreadState_'proc)" 580 apply (cinit lift: tptr_' cong add: call_ignore_cong) 581 apply (ctac (no_vcg) add: threadSet_tcbState_simple_corres) 582 apply (ctac add: scheduleTCB_ccorres_valid_queues'_simple) 583 apply (wp threadSet_valid_queues'_and_not_runnable') 584 apply (clarsimp simp: weak_sch_act_wf_def valid_queues'_def) 585 done 586 587lemma suspend_ccorres: 588 assumes cteDeleteOne_ccorres: 589 "\<And>w slot. ccorres dc xfdc 590 (invs' and cte_wp_at' (\<lambda>ct. w = -1 \<or> cteCap ct = NullCap 591 \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = w)) slot) 592 ({s. gs_get_assn cteDeleteOne_'proc (ghost'state_' (globals s)) = w} 593 \<inter> {s. slot_' s = Ptr slot}) [] 594 (cteDeleteOne slot) (Call cteDeleteOne_'proc)" 595 shows 596 "ccorres dc xfdc 597 (invs' and sch_act_simple and tcb_at' thread and (\<lambda>s. thread \<noteq> ksIdleThread s)) 598 (UNIV \<inter> {s. target_' s = tcb_ptr_to_ctcb_ptr thread}) [] 599 (suspend thread) (Call suspend_'proc)" 600 apply (cinit lift: target_') 601 apply (ctac(no_vcg) add: cancelIPC_ccorres1 [OF cteDeleteOne_ccorres]) 602 apply (ctac(no_vcg) add: setThreadState_ccorres_valid_queues'_simple) 603 apply (ctac add: tcbSchedDequeue_ccorres') 604 apply (rule_tac Q="\<lambda>_. 605 (\<lambda>s. \<forall>t' d p. (t' \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> 606 obj_at' (\<lambda>tcb. tcbQueued tcb \<and> tcbDomain tcb = d 607 \<and> tcbPriority tcb = p) t' s \<and> 608 (t' \<noteq> thread \<longrightarrow> st_tcb_at' runnable' t' s)) \<and> 609 distinct (ksReadyQueues s (d, p))) and valid_queues' and valid_objs' and tcb_at' thread" 610 in hoare_post_imp) 611 apply clarsimp 612 apply (drule_tac x="t" in spec) 613 apply (drule_tac x=d in spec) 614 apply (drule_tac x=p in spec) 615 apply (clarsimp elim!: obj_at'_weakenE simp: inQ_def) 616 apply (wp_trace sts_valid_queues_partial)[1] 617 apply (rule hoare_strengthen_post) 618 apply (rule hoare_vcg_conj_lift) 619 apply (rule hoare_vcg_conj_lift) 620 apply (rule cancelIPC_sch_act_simple) 621 apply (rule cancelIPC_tcb_at'[where t=thread]) 622 apply (rule delete_one_conc_fr.cancelIPC_invs) 623 apply (fastforce simp: invs_valid_queues' invs_queues invs_valid_objs' 624 valid_tcb_state'_def) 625 apply (auto simp: "StrictC'_thread_state_defs") 626 done 627 628lemma cap_to_H_NTFNCap_tag: 629 "\<lbrakk> cap_to_H cap = NotificationCap word1 word2 a b; 630 cap_lift C_cap = Some cap \<rbrakk> \<Longrightarrow> 631 cap_get_tag C_cap = scast cap_notification_cap" 632 apply (clarsimp simp: cap_to_H_def Let_def split: cap_CL.splits if_split_asm) 633 by (simp_all add: Let_def cap_lift_def split: if_splits) 634 635lemmas ccorres_pre_getBoundNotification = ccorres_pre_threadGet [where f=tcbBoundNotification, folded getBoundNotification_def] 636 637lemma option_to_ptr_not_NULL: 638 "option_to_ptr x \<noteq> NULL \<Longrightarrow> x \<noteq> None" 639 by (auto simp: option_to_ptr_def option_to_0_def split: option.splits) 640 641lemma doUnbindNotification_ccorres: 642 "ccorres dc xfdc (invs' and tcb_at' tcb) 643 (UNIV \<inter> {s. ntfnPtr_' s = ntfn_Ptr ntfnptr} \<inter> {s. tcbptr_' s = tcb_ptr_to_ctcb_ptr tcb}) [] 644 (do ntfn \<leftarrow> getNotification ntfnptr; doUnbindNotification ntfnptr ntfn tcb od) 645 (Call doUnbindNotification_'proc)" 646 apply (cinit' lift: ntfnPtr_' tcbptr_') 647 apply (rule ccorres_symb_exec_l [OF _ get_ntfn_inv' _ empty_fail_getNotification]) 648 apply (rule_tac P="invs' and ko_at' rv ntfnptr" and P'=UNIV 649 in ccorres_split_nothrow_novcg) 650 apply (rule ccorres_from_vcg[where rrel=dc and xf=xfdc]) 651 apply (rule allI, rule conseqPre, vcg) 652 apply (clarsimp simp: option_to_ptr_def option_to_0_def) 653 apply (frule cmap_relation_ntfn) 654 apply (erule (1) cmap_relation_ko_atE) 655 apply (rule conjI) 656 apply (erule h_t_valid_clift) 657 apply (clarsimp simp: setNotification_def split_def) 658 apply (rule bexI [OF _ setObject_eq]) 659 apply (simp add: rf_sr_def cstate_relation_def Let_def init_def 660 typ_heap_simps' 661 cpspace_relation_def update_ntfn_map_tos) 662 apply (elim conjE) 663 apply (intro conjI) 664 \<comment> \<open>tcb relation\<close> 665 apply (rule cpspace_relation_ntfn_update_ntfn, assumption+) 666 apply (clarsimp simp: cnotification_relation_def Let_def 667 mask_def [where n=2] NtfnState_Waiting_def) 668 apply (case_tac "ntfnObj rv", ((simp add: option_to_ctcb_ptr_def)+)[4]) 669 subgoal by (simp add: carch_state_relation_def typ_heap_simps') 670 subgoal by (simp add: cmachine_state_relation_def) 671 subgoal by (simp add: h_t_valid_clift_Some_iff) 672 subgoal by (simp add: objBits_simps') 673 subgoal by (simp add: objBits_simps) 674 apply assumption 675 apply ceqv 676 apply (rule ccorres_move_c_guard_tcb) 677 apply (simp add: setBoundNotification_def) 678 apply (rule_tac P'="\<top>" and P="\<top>" 679 in threadSet_ccorres_lemma3[unfolded dc_def]) 680 apply vcg 681 apply simp 682 apply (erule(1) rf_sr_tcb_update_no_queue2) 683 apply (simp add: typ_heap_simps')+ 684 apply (simp add: tcb_cte_cases_def) 685 apply (simp add: ctcb_relation_def option_to_ptr_def option_to_0_def) 686 apply (simp add: invs'_def valid_state'_def) 687 apply (wp get_ntfn_ko' | simp add: guard_is_UNIV_def)+ 688 done 689 690lemma doUnbindNotification_ccorres': 691 "ccorres dc xfdc (invs' and tcb_at' tcb and ko_at' ntfn ntfnptr) 692 (UNIV \<inter> {s. ntfnPtr_' s = ntfn_Ptr ntfnptr} \<inter> {s. tcbptr_' s = tcb_ptr_to_ctcb_ptr tcb}) [] 693 (doUnbindNotification ntfnptr ntfn tcb) 694 (Call doUnbindNotification_'proc)" 695 apply (cinit' lift: ntfnPtr_' tcbptr_') 696 apply (rule_tac P="invs' and ko_at' ntfn ntfnptr" and P'=UNIV 697 in ccorres_split_nothrow_novcg) 698 apply (rule ccorres_from_vcg[where rrel=dc and xf=xfdc]) 699 apply (rule allI, rule conseqPre, vcg) 700 apply (clarsimp simp: option_to_ptr_def option_to_0_def) 701 apply (frule cmap_relation_ntfn) 702 apply (erule (1) cmap_relation_ko_atE) 703 apply (rule conjI) 704 apply (erule h_t_valid_clift) 705 apply (clarsimp simp: setNotification_def split_def) 706 apply (rule bexI [OF _ setObject_eq]) 707 apply (simp add: rf_sr_def cstate_relation_def Let_def init_def 708 typ_heap_simps' 709 cpspace_relation_def update_ntfn_map_tos) 710 apply (elim conjE) 711 apply (intro conjI) 712 \<comment> \<open>tcb relation\<close> 713 apply (rule cpspace_relation_ntfn_update_ntfn, assumption+) 714 apply (clarsimp simp: cnotification_relation_def Let_def 715 mask_def [where n=2] NtfnState_Waiting_def) 716 apply (fold_subgoals (prefix))[2] 717 subgoal premises prems using prems 718 by (case_tac "ntfnObj ntfn", (simp add: option_to_ctcb_ptr_def)+) 719 subgoal by (simp add: carch_state_relation_def typ_heap_simps') 720 subgoal by (simp add: cmachine_state_relation_def) 721 subgoal by (simp add: h_t_valid_clift_Some_iff) 722 subgoal by (simp add: objBits_simps') 723 subgoal by (simp add: objBits_simps) 724 apply assumption 725 apply ceqv 726 apply (rule ccorres_move_c_guard_tcb) 727 apply (simp add: setBoundNotification_def) 728 apply (rule_tac P'="\<top>" and P="\<top>" 729 in threadSet_ccorres_lemma3[unfolded dc_def]) 730 apply vcg 731 apply simp 732 apply (erule(1) rf_sr_tcb_update_no_queue2) 733 apply (simp add: typ_heap_simps')+ 734 apply (simp add: tcb_cte_cases_def) 735 apply (simp add: ctcb_relation_def option_to_ptr_def option_to_0_def) 736 apply (simp add: invs'_def valid_state'_def) 737 apply (wp get_ntfn_ko' | simp add: guard_is_UNIV_def)+ 738 done 739 740 741lemma unbindNotification_ccorres: 742 "ccorres dc xfdc 743 (invs') (UNIV \<inter> {s. tcb_' s = tcb_ptr_to_ctcb_ptr tcb}) [] 744 (unbindNotification tcb) (Call unbindNotification_'proc)" 745 apply (cinit lift: tcb_') 746 apply (rule_tac xf'=ntfnPtr_' 747 and r'="\<lambda>rv rv'. rv' = option_to_ptr rv \<and> rv \<noteq> Some 0" 748 in ccorres_split_nothrow) 749 apply (simp add: getBoundNotification_def) 750 apply (rule_tac P="no_0_obj' and valid_objs'" in threadGet_vcg_corres_P) 751 apply (rule allI, rule conseqPre, vcg) 752 apply clarsimp 753 apply (drule obj_at_ko_at', clarsimp) 754 apply (drule spec, drule(1) mp, clarsimp) 755 apply (clarsimp simp: typ_heap_simps ctcb_relation_def) 756 apply (drule(1) ko_at_valid_objs', simp add: projectKOs) 757 apply (clarsimp simp: option_to_ptr_def option_to_0_def projectKOs 758 valid_obj'_def valid_tcb'_def) 759 apply ceqv 760 apply simp 761 apply wpc 762 apply (rule ccorres_cond_false) 763 apply (rule ccorres_return_Skip[unfolded dc_def]) 764 apply (rule ccorres_cond_true) 765 apply (ctac (no_vcg) add: doUnbindNotification_ccorres[unfolded dc_def, simplified]) 766 apply (wp gbn_wp') 767 apply vcg 768 apply (clarsimp simp: option_to_ptr_def option_to_0_def pred_tcb_at'_def 769 obj_at'_weakenE[OF _ TrueI] 770 split: option.splits) 771 apply (clarsimp simp: invs'_def valid_pspace'_def valid_state'_def) 772 done 773 774 775lemma unbindMaybeNotification_ccorres: 776 "ccorres dc xfdc (invs') (UNIV \<inter> {s. ntfnPtr_' s = ntfn_Ptr ntfnptr}) [] 777 (unbindMaybeNotification ntfnptr) (Call unbindMaybeNotification_'proc)" 778 apply (cinit lift: ntfnPtr_') 779 apply (rule ccorres_symb_exec_l [OF _ get_ntfn_inv' _ empty_fail_getNotification]) 780 apply (rule ccorres_rhs_assoc2) 781 apply (rule_tac P="ntfnBoundTCB rv \<noteq> None \<longrightarrow> 782 option_to_ctcb_ptr (ntfnBoundTCB rv) \<noteq> NULL" 783 in ccorres_gen_asm) 784 apply (rule_tac xf'=boundTCB_' 785 and val="option_to_ctcb_ptr (ntfnBoundTCB rv)" 786 and R="ko_at' rv ntfnptr and valid_bound_tcb' (ntfnBoundTCB rv)" 787 in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV]) 788 apply vcg 789 apply clarsimp 790 apply (erule cmap_relationE1[OF cmap_relation_ntfn]) 791 apply (erule ko_at_projectKO_opt) 792 apply (clarsimp simp: typ_heap_simps cnotification_relation_def Let_def) 793 apply ceqv 794 apply wpc 795 apply (rule ccorres_cond_false) 796 apply (rule ccorres_return_Skip) 797 apply (rule ccorres_cond_true) 798 apply (rule ccorres_call[where xf'=xfdc]) 799 apply (rule doUnbindNotification_ccorres'[simplified]) 800 apply simp 801 apply simp 802 apply simp 803 apply (clarsimp simp add: guard_is_UNIV_def option_to_ctcb_ptr_def ) 804 apply (wp getNotification_wp) 805 apply (clarsimp ) 806 apply (frule (1) ko_at_valid_ntfn'[OF _ invs_valid_objs']) 807 by (auto simp: valid_ntfn'_def valid_bound_tcb'_def obj_at'_def projectKOs 808 objBitsKO_def is_aligned_def option_to_ctcb_ptr_def tcb_at_not_NULL 809 split: ntfn.splits) 810 811lemma finaliseCap_True_cases_ccorres: 812 "\<And>final. isEndpointCap cap \<or> isNotificationCap cap 813 \<or> isReplyCap cap \<or> isDomainCap cap \<or> cap = NullCap \<Longrightarrow> 814 ccorres (\<lambda>rv rv'. ccap_relation (fst rv) (finaliseCap_ret_C.remainder_C rv') 815 \<and> ccap_relation (snd rv) (finaliseCap_ret_C.cleanupInfo_C rv')) 816 ret__struct_finaliseCap_ret_C_' 817 (invs') (UNIV \<inter> {s. ccap_relation cap (cap_' s)} \<inter> {s. final_' s = from_bool final} 818 \<inter> {s. exposed_' s = from_bool flag (* dave has name wrong *)}) [] 819 (finaliseCap cap final flag) (Call finaliseCap_'proc)" 820 apply (subgoal_tac "\<not> isArchCap \<top> cap") 821 prefer 2 822 apply (clarsimp simp: isCap_simps) 823 apply (cinit lift: cap_' final_' exposed_' cong: call_ignore_cong) 824 apply csymbr 825 apply (simp add: cap_get_tag_isCap Collect_False del: Collect_const) 826 apply (fold case_bool_If) 827 apply (simp add: false_def) 828 apply csymbr 829 apply wpc 830 apply (simp add: cap_get_tag_isCap ccorres_cond_univ_iff Let_def) 831 apply (rule ccorres_rhs_assoc)+ 832 apply (rule ccorres_split_nothrow_novcg) 833 apply (simp add: when_def) 834 apply (rule ccorres_cond2) 835 apply (clarsimp simp: Collect_const_mem from_bool_0) 836 apply csymbr 837 apply (rule ccorres_call[where xf'=xfdc], rule cancelAllIPC_ccorres) 838 apply simp 839 apply simp 840 apply simp 841 apply (rule ccorres_from_vcg[where P=\<top> and P'=UNIV]) 842 apply (simp add: return_def, vcg) 843 apply (rule ceqv_refl) 844 apply (rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2, 845 rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2, 846 rule ccorres_split_throws) 847 apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV]) 848 apply (rule allI, rule conseqPre, vcg) 849 apply (clarsimp simp add: return_def ccap_relation_NullCap_iff 850 irq_opt_relation_def) 851 apply vcg 852 apply wp 853 apply (simp add: guard_is_UNIV_def) 854 apply wpc 855 apply (simp add: cap_get_tag_isCap Let_def 856 ccorres_cond_empty_iff ccorres_cond_univ_iff) 857 apply (rule ccorres_rhs_assoc)+ 858 apply (rule ccorres_split_nothrow_novcg) 859 apply (simp add: when_def) 860 apply (rule ccorres_cond2) 861 apply (clarsimp simp: Collect_const_mem from_bool_0) 862 apply (subgoal_tac "cap_get_tag capa = scast cap_notification_cap") prefer 2 863 apply (clarsimp simp: ccap_relation_def isNotificationCap_def) 864 apply (case_tac cap, simp_all)[1] 865 apply (clarsimp simp: option_map_def split: option.splits) 866 apply (drule (2) cap_to_H_NTFNCap_tag[OF sym]) 867 apply (rule ccorres_rhs_assoc) 868 apply (rule ccorres_rhs_assoc) 869 apply csymbr 870 apply csymbr 871 apply (ctac (no_vcg) add: unbindMaybeNotification_ccorres) 872 apply (rule ccorres_call[where xf'=xfdc], rule cancelAllSignals_ccorres) 873 apply simp 874 apply simp 875 apply simp 876 apply (wp | wpc | simp add: guard_is_UNIV_def)+ 877 apply (rule ccorres_return_Skip') 878 apply (rule ceqv_refl) 879 apply (rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2, 880 rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2, 881 rule ccorres_split_throws) 882 apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV]) 883 apply (rule allI, rule conseqPre, vcg) 884 apply (clarsimp simp add: return_def ccap_relation_NullCap_iff 885 irq_opt_relation_def) 886 apply vcg 887 apply wp 888 apply (simp add: guard_is_UNIV_def) 889 apply wpc 890 apply (simp add: cap_get_tag_isCap Let_def 891 ccorres_cond_empty_iff ccorres_cond_univ_iff) 892 apply (rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2, 893 rule ccorres_split_throws) 894 apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV]) 895 apply (rule allI, rule conseqPre, vcg) 896 apply (clarsimp simp add: return_def ccap_relation_NullCap_iff 897 irq_opt_relation_def) 898 apply vcg 899 apply wpc 900 apply (simp add: cap_get_tag_isCap Let_def 901 ccorres_cond_empty_iff ccorres_cond_univ_iff) 902 apply (rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2, 903 rule ccorres_split_throws) 904 apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV]) 905 apply (rule allI, rule conseqPre, vcg) 906 apply (clarsimp simp add: return_def ccap_relation_NullCap_iff) 907 apply (clarsimp simp add: irq_opt_relation_def) 908 apply vcg 909 \<comment> \<open>NullCap case by exhaustion\<close> 910 apply (simp add: cap_get_tag_isCap Let_def 911 ccorres_cond_empty_iff ccorres_cond_univ_iff) 912 apply (rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2, 913 rule ccorres_split_throws) 914 apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV]) 915 apply (rule allI, rule conseqPre, vcg) 916 apply (clarsimp simp add: return_def ccap_relation_NullCap_iff 917 irq_opt_relation_def) 918 apply vcg 919 apply (clarsimp simp: Collect_const_mem cap_get_tag_isCap) 920 apply (rule TrueI conjI impI TrueI)+ 921 apply (frule cap_get_tag_to_H, erule(1) cap_get_tag_isCap [THEN iffD2]) 922 apply (clarsimp simp: invs'_def valid_state'_def valid_pspace'_def isNotificationCap_def 923 isEndpointCap_def valid_obj'_def projectKOs valid_ntfn'_def 924 valid_bound_tcb'_def 925 dest!: obj_at_valid_objs') 926 apply clarsimp 927 apply (frule cap_get_tag_to_H, erule(1) cap_get_tag_isCap [THEN iffD2]) 928 apply clarsimp 929 done 930 931lemma finaliseCap_True_standin_ccorres: 932 "\<And>final. 933 ccorres (\<lambda>rv rv'. ccap_relation (fst rv) (finaliseCap_ret_C.remainder_C rv') 934 \<and> ccap_relation (snd rv) (finaliseCap_ret_C.cleanupInfo_C rv')) 935 ret__struct_finaliseCap_ret_C_' 936 (invs') (UNIV \<inter> {s. ccap_relation cap (cap_' s)} \<inter> {s. final_' s = from_bool final} 937 \<inter> {s. exposed_' s = from_bool True (* dave has name wrong *)}) [] 938 (finaliseCapTrue_standin cap final) (Call finaliseCap_'proc)" 939 unfolding finaliseCapTrue_standin_simple_def 940 apply (case_tac "P :: bool" for P) 941 apply (erule finaliseCap_True_cases_ccorres) 942 apply (simp add: finaliseCap_def ccorres_fail') 943 done 944 945lemma offset_xf_for_sequence: 946 "\<forall>s f. offset_' (offset_'_update f s) = f (offset_' s) 947 \<and> globals (offset_'_update f s) = globals s" 948 by simp 949 950end 951 952context begin interpretation Arch . (*FIXME: arch_split*) 953crunch pde_mappings'[wp]: invalidateHWASIDEntry "valid_pde_mappings'" 954end 955 956context kernel_m begin 957 958 959lemma invalidateASIDEntry_ccorres: 960 "ccorres dc xfdc (\<lambda>s. valid_pde_mappings' s \<and> asid \<le> mask asid_bits) 961 (UNIV \<inter> {s. asid_' s = asid}) [] 962 (invalidateASIDEntry asid) (Call invalidateASIDEntry_'proc)" 963 apply (cinit lift: asid_') 964 apply (ctac(no_vcg) add: loadHWASID_ccorres) 965 apply csymbr 966 apply (simp(no_asm) add: when_def del: Collect_const) 967 apply (rule ccorres_split_nothrow_novcg_dc) 968 apply (rule ccorres_cond2[where R=\<top>]) 969 apply (clarsimp simp: Collect_const_mem pde_stored_asid_def to_bool_def 970 split: if_split) 971 apply csymbr 972 apply (rule ccorres_Guard)+ 973 apply (rule_tac P="rv \<noteq> None" in ccorres_gen_asm) 974 apply (ctac(no_simp) add: invalidateHWASIDEntry_ccorres) 975 apply (clarsimp simp: pde_stored_asid_def unat_ucast 976 split: if_split_asm) 977 apply (rule sym, rule nat_mod_eq') 978 apply (simp add: pde_pde_invalid_lift_def pde_lift_def) 979 apply (rule unat_less_power[where sz=8, simplified]) 980 apply (simp add: word_bits_conv) 981 apply (rule order_le_less_trans, rule word_and_le1) 982 apply (simp add: mask_def) 983 apply (rule ccorres_return_Skip) 984 apply (fold dc_def) 985 apply (ctac add: invalidateASID_ccorres) 986 apply wp 987 apply (simp add: guard_is_UNIV_def) 988 apply wp 989 apply (clarsimp simp: Collect_const_mem pde_pde_invalid_lift_def pde_lift_def 990 order_le_less_trans[OF word_and_le1] mask_def) 991 done 992 993end 994 995context begin interpretation Arch . (*FIXME: arch_split*) 996crunch obj_at'[wp]: invalidateASIDEntry "obj_at' P p" 997crunch obj_at'[wp]: flushSpace "obj_at' P p" 998crunch valid_objs'[wp]: invalidateASIDEntry "valid_objs'" 999crunch valid_objs'[wp]: flushSpace "valid_objs'" 1000crunch pde_mappings'[wp]: invalidateASIDEntry "valid_pde_mappings'" 1001crunch pde_mappings'[wp]: flushSpace "valid_pde_mappings'" 1002end 1003 1004context kernel_m begin 1005 1006lemma invs'_invs_no_cicd': 1007 "invs' s \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s" 1008 by (simp add: invs'_invs_no_cicd) 1009 1010lemma deleteASIDPool_ccorres: 1011 "ccorres dc xfdc (invs' and (\<lambda>_. base < 2 ^ 17 \<and> pool \<noteq> 0)) 1012 (UNIV \<inter> {s. asid_base_' s = base} \<inter> {s. pool_' s = Ptr pool}) [] 1013 (deleteASIDPool base pool) (Call deleteASIDPool_'proc)" 1014 apply (rule ccorres_gen_asm) 1015 apply (cinit lift: asid_base_' pool_' simp: whileAnno_def) 1016 apply (rule ccorres_assert) 1017 apply (clarsimp simp: liftM_def dc_def[symmetric] fun_upd_def[symmetric] 1018 when_def 1019 simp del: Collect_const) 1020 apply (rule ccorres_Guard)+ 1021 apply (rule ccorres_pre_gets_armKSASIDTable_ksArchState) 1022 apply (rule_tac R="\<lambda>s. rv = armKSASIDTable (ksArchState s)" in ccorres_cond2) 1023 apply clarsimp 1024 apply (subst rf_sr_armKSASIDTable, assumption) 1025 apply (simp add: asid_high_bits_word_bits) 1026 apply (rule shiftr_less_t2n) 1027 apply (simp add: asid_low_bits_def asid_high_bits_def) 1028 apply (subst ucast_asid_high_bits_is_shift) 1029 apply (simp add: mask_def, simp add: asid_bits_def) 1030 apply (simp add: option_to_ptr_def option_to_0_def split: option.split) 1031 apply (rule ccorres_Guard_Seq ccorres_rhs_assoc)+ 1032 apply (rule ccorres_pre_getObject_asidpool) 1033 apply (rename_tac poolKO) 1034 apply (simp only: mapM_discarded) 1035 apply (rule ccorres_rhs_assoc2, 1036 rule ccorres_split_nothrow_novcg) 1037 apply (simp add: word_sle_def Kernel_C.asidLowBits_def Collect_True 1038 del: Collect_const) 1039 apply (rule ccorres_semantic_equivD2[rotated]) 1040 apply (simp only: semantic_equiv_def) 1041 apply (rule Seq_ceqv [OF ceqv_refl _ xpres_triv]) 1042 apply (simp only: ceqv_Guard_UNIV) 1043 apply (rule While_ceqv [OF _ _ xpres_triv], rule impI, rule refl) 1044 apply (rule ceqv_remove_eqv_skip) 1045 apply (simp add: ceqv_Guard_UNIV ceqv_refl) 1046 apply (rule_tac F="\<lambda>n. ko_at' poolKO pool and valid_objs' and valid_pde_mappings'" 1047 in ccorres_mapM_x_while_gen[OF _ _ _ _ _ offset_xf_for_sequence, 1048 where j=1, simplified]) 1049 apply (intro allI impI) 1050 apply (rule ccorres_guard_imp2) 1051 apply (rule_tac xf'="offset_'" in ccorres_abstract, ceqv) 1052 apply (rule_tac P="rv' = of_nat n" in ccorres_gen_asm2) 1053 apply (rule ccorres_Guard[where F=ArrayBounds]) 1054 apply (rule ccorres_move_c_guard_ap) 1055 apply (rule_tac R="ko_at' poolKO pool and valid_objs'" in ccorres_cond2) 1056 apply (clarsimp dest!: rf_sr_cpspace_asidpool_relation) 1057 apply (erule cmap_relationE1, erule ko_at_projectKO_opt) 1058 apply (clarsimp simp: casid_pool_relation_def typ_heap_simps 1059 inv_ASIDPool 1060 split: asidpool.split_asm asid_pool_C.split_asm) 1061 apply (simp add: upto_enum_word del: upt.simps) 1062 apply (drule(1) ko_at_valid_objs') 1063 apply (simp add: projectKOs) 1064 apply (clarsimp simp: array_relation_def valid_obj'_def 1065 ran_def) 1066 apply (drule_tac x="of_nat n" in spec)+ 1067 apply (simp add: asid_low_bits_def word_le_nat_alt) 1068 apply (simp add: word_unat.Abs_inverse unats_def) 1069 apply (simp add: option_to_ptr_def option_to_0_def split: option.split_asm) 1070 apply clarsimp 1071 apply (ctac(no_vcg) add: flushSpace_ccorres) 1072 apply (ctac add: invalidateASIDEntry_ccorres) 1073 apply wp 1074 apply (rule ccorres_return_Skip) 1075 apply (clarsimp simp: Collect_const_mem) 1076 apply (simp add: upto_enum_word typ_at_to_obj_at_arches 1077 obj_at'_weakenE[OF _ TrueI] 1078 del: upt.simps) 1079 apply (simp add: is_aligned_mask[symmetric]) 1080 apply (rule conjI[rotated]) 1081 apply (simp add: asid_low_bits_def word_of_nat_less) 1082 apply (clarsimp simp: mask_def) 1083 apply (erule is_aligned_add_less_t2n) 1084 apply (subst(asm) Suc_unat_diff_1) 1085 apply (simp add: asid_low_bits_def) 1086 apply (simp add: unat_power_lower asid_low_bits_word_bits) 1087 apply (erule of_nat_less_pow_32 [OF _ asid_low_bits_word_bits]) 1088 apply (simp add: asid_low_bits_def asid_bits_def) 1089 apply (simp add: asid_bits_def) 1090 apply (simp add: upto_enum_word ) 1091 apply (vcg exspec=flushSpace_modifies exspec=invalidateASIDEntry_modifies) 1092 apply clarsimp 1093 apply (rule hoare_pre, wp) 1094 apply simp 1095 apply (simp add: upto_enum_word asid_low_bits_def) 1096 apply ceqv 1097 apply (rule ccorres_move_const_guard)+ 1098 apply (rule ccorres_split_nothrow_novcg_dc) 1099 apply (rule_tac P="\<lambda>s. rv = armKSASIDTable (ksArchState s)" 1100 in ccorres_from_vcg[where P'=UNIV]) 1101 apply (rule allI, rule conseqPre, vcg) 1102 apply (clarsimp simp: simpler_modify_def) 1103 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def 1104 carch_state_relation_def cmachine_state_relation_def 1105 carch_globals_def h_t_valid_clift_Some_iff) 1106 apply (erule array_relation_update[unfolded fun_upd_def]) 1107 apply (simp add: asid_high_bits_of_def unat_ucast asid_low_bits_def) 1108 apply (rule sym, rule nat_mod_eq') 1109 apply (rule order_less_le_trans, rule iffD1[OF word_less_nat_alt]) 1110 apply (rule shiftr_less_t2n[where m=7]) 1111 subgoal by simp 1112 subgoal by simp 1113 subgoal by (simp add: option_to_ptr_def option_to_0_def) 1114 subgoal by (simp add: asid_high_bits_def) 1115 apply (rule ccorres_pre_getCurThread) 1116 apply (ctac add: setVMRoot_ccorres) 1117 apply wp 1118 apply (simp add: guard_is_UNIV_def) 1119 apply (simp add: pred_conj_def fun_upd_def[symmetric] 1120 cur_tcb'_def[symmetric]) 1121 apply (strengthen invs'_invs_no_cicd', strengthen invs_asid_update_strg') 1122 apply (rule mapM_x_wp') 1123 apply (rule hoare_pre, wp) 1124 apply simp 1125 apply (simp add: guard_is_UNIV_def Kernel_C.asidLowBits_def 1126 word_sle_def word_sless_def Collect_const_mem 1127 mask_def asid_bits_def plus_one_helper 1128 asid_shiftr_low_bits_less) 1129 apply (rule ccorres_return_Skip) 1130 apply (simp add: Kernel_C.asidLowBits_def 1131 word_sle_def word_sless_def) 1132 apply (auto simp: asid_shiftr_low_bits_less Collect_const_mem 1133 mask_def asid_bits_def plus_one_helper) 1134 done 1135 1136lemma deleteASID_ccorres: 1137 "ccorres dc xfdc (invs' and K (asid < 2 ^ 17) and K (pdPtr \<noteq> 0)) 1138 (UNIV \<inter> {s. asid_' s = asid} \<inter> {s. pd_' s = Ptr pdPtr}) [] 1139 (deleteASID asid pdPtr) (Call deleteASID_'proc)" 1140 apply (cinit lift: asid_' pd_' cong: call_ignore_cong) 1141 apply (rule ccorres_Guard_Seq)+ 1142 apply (rule_tac r'="\<lambda>rv rv'. case rv (ucast (asid_high_bits_of asid)) of 1143 None \<Rightarrow> rv' = NULL 1144 | Some v \<Rightarrow> rv' = Ptr v \<and> rv' \<noteq> NULL" 1145 and xf'="poolPtr_'" in ccorres_split_nothrow) 1146 apply (rule_tac P="invs' and K (asid < 2 ^ 17)" 1147 and P'=UNIV in ccorres_from_vcg) 1148 apply (rule allI, rule conseqPre, vcg) 1149 apply (clarsimp simp: simpler_gets_def Let_def) 1150 apply (erule(1) getKSASIDTable_ccorres_stuff) 1151 apply (simp add: asid_high_bits_of_def 1152 asidLowBits_def Kernel_C.asidLowBits_def 1153 asid_low_bits_def unat_ucast) 1154 apply (rule sym, rule Divides.mod_less, simp) 1155 apply (rule unat_less_power[where sz=7, simplified]) 1156 apply (simp add: word_bits_conv) 1157 apply (rule shiftr_less_t2n[where m=7, simplified]) 1158 apply simp 1159 apply (rule order_less_le_trans, rule ucast_less) 1160 apply simp 1161 apply (simp add: asid_high_bits_def) 1162 apply ceqv 1163 apply csymbr 1164 apply wpc 1165 apply (simp add: ccorres_cond_iffs dc_def[symmetric] 1166 Collect_False 1167 del: Collect_const 1168 cong: call_ignore_cong) 1169 apply (rule ccorres_cond_false) 1170 apply (rule ccorres_return_Skip) 1171 apply (simp add: dc_def[symmetric] when_def 1172 Collect_True liftM_def 1173 cong: conj_cong call_ignore_cong 1174 del: Collect_const) 1175 apply (rule ccorres_pre_getObject_asidpool) 1176 apply (rule ccorres_Guard_Seq[where F=ArrayBounds]) 1177 apply (rule ccorres_move_c_guard_ap) 1178 apply (rule ccorres_Guard_Seq)+ 1179 apply (rename_tac pool) 1180 apply (rule_tac xf'=ret__int_' 1181 and val="from_bool (inv ASIDPool pool (asid && mask asid_low_bits) 1182 = Some pdPtr)" 1183 and R="ko_at' pool x2 and K (pdPtr \<noteq> 0)" 1184 in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV]) 1185 apply (vcg, clarsimp) 1186 apply (clarsimp dest!: rf_sr_cpspace_asidpool_relation) 1187 apply (erule(1) cmap_relation_ko_atE) 1188 apply (clarsimp simp: typ_heap_simps casid_pool_relation_def 1189 array_relation_def 1190 split: asidpool.split_asm asid_pool_C.split_asm) 1191 apply (drule_tac x="asid && mask asid_low_bits" in spec) 1192 apply (simp add: asid_low_bits_def Kernel_C.asidLowBits_def 1193 mask_def word_and_le1) 1194 apply (drule sym, simp) 1195 apply (simp add: option_to_ptr_def option_to_0_def 1196 from_bool_def inv_ASIDPool 1197 split: option.split if_split bool.split) 1198 apply ceqv 1199 apply (rule ccorres_cond2[where R=\<top>]) 1200 apply (simp add: Collect_const_mem from_bool_0) 1201 apply (rule ccorres_rhs_assoc)+ 1202 apply (ctac (no_vcg) add: flushSpace_ccorres) 1203 apply (ctac (no_vcg) add: invalidateASIDEntry_ccorres) 1204 apply (rule ccorres_Guard_Seq[where F=ArrayBounds]) 1205 apply (rule ccorres_move_c_guard_ap) 1206 apply (rule ccorres_Guard_Seq)+ 1207 apply (rule ccorres_split_nothrow_novcg_dc) 1208 apply (rule_tac P="ko_at' pool x2" in ccorres_from_vcg[where P'=UNIV]) 1209 apply (rule allI, rule conseqPre, vcg) 1210 apply clarsimp 1211 apply (rule cmap_relationE1[OF rf_sr_cpspace_asidpool_relation], 1212 assumption, erule ko_at_projectKO_opt) 1213 apply (rule bexI [OF _ setObject_eq], 1214 simp_all add: objBits_simps archObjSize_def pageBits_def)[1] 1215 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def typ_heap_simps) 1216 apply (rule conjI) 1217 apply (clarsimp simp: cpspace_relation_def typ_heap_simps' 1218 update_asidpool_map_tos 1219 update_asidpool_map_to_asidpools) 1220 apply (rule cmap_relation_updI, simp_all)[1] 1221 apply (simp add: casid_pool_relation_def fun_upd_def[symmetric] 1222 inv_ASIDPool 1223 split: asidpool.split_asm asid_pool_C.split_asm) 1224 apply (erule array_relation_update) 1225 subgoal by (simp add: mask_def) 1226 subgoal by (simp add: option_to_ptr_def option_to_0_def) 1227 subgoal by (simp add: asid_low_bits_def) 1228 subgoal by (simp add: carch_state_relation_def cmachine_state_relation_def 1229 carch_globals_def update_asidpool_map_tos 1230 typ_heap_simps') 1231 apply (rule ccorres_pre_getCurThread) 1232 apply (ctac add: setVMRoot_ccorres) 1233 apply (simp add: cur_tcb'_def[symmetric]) 1234 apply (strengthen invs'_invs_no_cicd') 1235 apply wp 1236 apply (clarsimp simp: rf_sr_def guard_is_UNIV_def 1237 cstate_relation_def Let_def) 1238 apply wp[1] 1239 apply (simp add: fun_upd_def[symmetric]) 1240 apply wp 1241 apply (rule ccorres_return_Skip) 1242 subgoal by (clarsimp simp: guard_is_UNIV_def Collect_const_mem 1243 word_sle_def word_sless_def 1244 Kernel_C.asidLowBits_def 1245 asid_low_bits_def order_le_less_trans [OF word_and_le1]) 1246 apply wp 1247 apply vcg 1248 apply (clarsimp simp: Collect_const_mem if_1_0_0 1249 word_sless_def word_sle_def 1250 Kernel_C.asidLowBits_def 1251 typ_at_to_obj_at_arches) 1252 apply (rule conjI) 1253 apply (clarsimp simp: mask_def inv_ASIDPool 1254 split: asidpool.split) 1255 apply (frule obj_at_valid_objs', clarsimp+) 1256 apply (clarsimp simp: asid_bits_def typ_at_to_obj_at_arches 1257 obj_at'_weakenE[OF _ TrueI] 1258 fun_upd_def[symmetric] valid_obj'_def 1259 projectKOs invs_valid_pde_mappings' 1260 invs_cur') 1261 apply (rule conjI, blast) 1262 subgoal by (fastforce simp: inv_into_def ran_def split: if_split_asm) 1263 by (clarsimp simp: order_le_less_trans [OF word_and_le1] 1264 asid_shiftr_low_bits_less asid_bits_def mask_def 1265 plus_one_helper arg_cong[where f="\<lambda>x. 2 ^ x", OF meta_eq_to_obj_eq, OF asid_low_bits_def] 1266 split: option.split_asm) 1267 1268lemma setObject_ccorres_lemma: 1269 fixes val :: "'a :: pspace_storable" shows 1270 "\<lbrakk> \<And>s. \<Gamma> \<turnstile> (Q s) c {s'. (s \<lparr> ksPSpace := ksPSpace s (ptr \<mapsto> injectKO val) \<rparr>, s') \<in> rf_sr},{}; 1271 \<And>s s' val (val' :: 'a). \<lbrakk> ko_at' val' ptr s; (s, s') \<in> rf_sr \<rbrakk> 1272 \<Longrightarrow> s' \<in> Q s; 1273 \<And>val :: 'a. updateObject val = updateObject_default val; 1274 \<And>val :: 'a. (1 :: word32) < 2 ^ objBits val; 1275 \<And>(val :: 'a) (val' :: 'a). objBits val = objBits val'; 1276 \<Gamma> \<turnstile> Q' c UNIV \<rbrakk> 1277 \<Longrightarrow> ccorres dc xfdc \<top> Q' hs 1278 (setObject ptr val) c" 1279 apply (rule ccorres_from_vcg_nofail) 1280 apply (rule allI) 1281 apply (case_tac "obj_at' (\<lambda>x :: 'a. True) ptr \<sigma>") 1282 apply (rule_tac P'="Q \<sigma>" in conseqPre, rule conseqPost, assumption) 1283 apply clarsimp 1284 apply (rule bexI [OF _ setObject_eq], simp+) 1285 apply (drule obj_at_ko_at') 1286 apply clarsimp 1287 apply clarsimp 1288 apply (rule conseqPre, erule conseqPost) 1289 apply clarsimp 1290 apply (subgoal_tac "fst (setObject ptr val \<sigma>) = {}") 1291 apply simp 1292 apply (erule notE, erule_tac s=\<sigma> in empty_failD[rotated]) 1293 apply (simp add: setObject_def split_def) 1294 apply (rule ccontr) 1295 apply (clarsimp elim!: nonemptyE) 1296 apply (frule use_valid [OF _ obj_at_setObject3[where P=\<top>]], simp_all)[1] 1297 apply (simp add: typ_at_to_obj_at'[symmetric]) 1298 apply (frule(1) use_valid [OF _ setObject_typ_at']) 1299 apply simp 1300 apply simp 1301 apply clarsimp 1302 done 1303 1304lemma findPDForASID_nonzero: 1305 "\<lbrace>\<top>\<rbrace> findPDForASID asid \<lbrace>\<lambda>rv s. rv \<noteq> 0\<rbrace>,-" 1306 apply (simp add: findPDForASID_def cong: option.case_cong) 1307 apply (wp | wpc | simp only: o_def simp_thms)+ 1308 done 1309 1310lemma pageTableMapped_ccorres: 1311 "ccorres (\<lambda>rv rv'. rv' = option_to_ptr rv \<and> rv \<noteq> Some 0) ret__ptr_to_struct_pde_C_' 1312 (invs' and K (asid \<le> mask asid_bits)) 1313 (UNIV \<inter> {s. asid_' s = asid} \<inter> {s. vaddr_' s = vaddr} \<inter> {s. pt_' s = Ptr ptPtr}) [] 1314 (pageTableMapped asid vaddr ptPtr) (Call pageTableMapped_'proc)" 1315 apply (cinit lift: asid_' vaddr_' pt_') 1316 apply (simp add: ignoreFailure_def catch_def 1317 bindE_bind_linearise liftE_def 1318 del: Collect_const cong: call_ignore_cong) 1319 apply (rule ccorres_split_nothrow_novcg_case_sum) 1320 apply clarsimp 1321 apply (ctac (no_vcg) add: findPDForASID_ccorres) 1322 apply ceqv 1323 apply (simp add: Collect_False del: Collect_const cong: call_ignore_cong) 1324 apply csymbr 1325 apply (rule_tac xf'=pde_' and r'=cpde_relation in ccorres_split_nothrow_novcg) 1326 apply (rule ccorres_add_return2, rule ccorres_pre_getObject_pde) 1327 apply (rule ccorres_move_array_assertion_pd 1328 | (rule ccorres_flip_Guard, rule ccorres_move_array_assertion_pd))+ 1329 apply (rule_tac P="ko_at' x (lookup_pd_slot rv vaddr) and no_0_obj' 1330 and page_directory_at' rv" 1331 in ccorres_from_vcg[where P'=UNIV]) 1332 apply (rule allI, rule conseqPre, vcg) 1333 apply (clarsimp simp: return_def lookup_pd_slot_def Let_def) 1334 apply (drule(1) page_directory_at_rf_sr) 1335 apply (erule cmap_relationE1[OF rf_sr_cpde_relation], 1336 erule ko_at_projectKO_opt) 1337 apply (clarsimp simp: typ_heap_simps' shiftl_t2n field_simps) 1338 apply ceqv 1339 apply (rule_tac P="rv \<noteq> 0" in ccorres_gen_asm) 1340 apply csymbr+ 1341 apply (wpc, simp_all add: if_1_0_0 returnOk_bind throwError_bind 1342 del: Collect_const) 1343 prefer 2 1344 apply (rule ccorres_cond_true_seq) 1345 apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV]) 1346 apply (rule allI, rule conseqPre, vcg) 1347 apply (clarsimp simp: if_1_0_0 cpde_relation_def Let_def 1348 return_def addrFromPPtr_def 1349 pde_pde_coarse_lift_def) 1350 apply (rule conjI) 1351 apply (simp add: pde_lift_def Let_def split: if_split_asm) 1352 apply (clarsimp simp: option_to_0_def option_to_ptr_def split: if_split) 1353 apply (clarsimp simp: ARM.addrFromPPtr_def ARM.ptrFromPAddr_def) 1354 apply ((rule ccorres_cond_false_seq ccorres_cond_false 1355 ccorres_return_C | simp)+)[3] 1356 apply (simp only: simp_thms) 1357 apply wp 1358 apply (clarsimp simp: guard_is_UNIV_def Collect_const_mem if_1_0_0) 1359 apply (simp add: cpde_relation_def Let_def pde_lift_def 1360 split: if_split_asm, 1361 auto simp: option_to_0_def option_to_ptr_def pde_tag_defs)[1] 1362 apply simp 1363 apply (rule ccorres_split_throws) 1364 apply (rule ccorres_return_C, simp+) 1365 apply vcg 1366 apply (wp hoare_drop_imps findPDForASID_nonzero) 1367 apply (simp add: guard_is_UNIV_def word_sle_def pdBits_def pageBits_def 1368 unat_gt_0 unat_shiftr_le_bound pdeBits_def) 1369 apply (simp add: guard_is_UNIV_def option_to_0_def option_to_ptr_def) 1370 apply auto[1] 1371 done 1372 1373lemma pageTableMapped_pd: 1374 "\<lbrace>\<top>\<rbrace> pageTableMapped asid vaddr ptPtr 1375 \<lbrace>\<lambda>rv s. case rv of Some x \<Rightarrow> page_directory_at' x s | _ \<Rightarrow> True\<rbrace>" 1376 apply (simp add: pageTableMapped_def) 1377 apply (rule hoare_pre) 1378 apply (wp getPDE_wp hoare_vcg_all_lift_R | wpc)+ 1379 apply (rule hoare_post_imp_R, rule findPDForASID_page_directory_at'_simple) 1380 apply (clarsimp split: if_split) 1381 apply simp 1382 done 1383 1384lemma unmapPageTable_ccorres: 1385 "ccorres dc xfdc (invs' and (\<lambda>s. asid \<le> mask asid_bits \<and> vaddr < kernelBase)) 1386 (UNIV \<inter> {s. asid_' s = asid} \<inter> {s. vaddr_' s = vaddr} \<inter> {s. pt_' s = Ptr ptPtr}) [] 1387 (unmapPageTable asid vaddr ptPtr) (Call unmapPageTable_'proc)" 1388 apply (rule ccorres_gen_asm) 1389 apply (cinit lift: asid_' vaddr_' pt_') 1390 apply (ctac(no_vcg) add: pageTableMapped_ccorres) 1391 apply wpc 1392 apply (simp add: option_to_ptr_def option_to_0_def ccorres_cond_iffs) 1393 apply (rule ccorres_return_Skip[unfolded dc_def]) 1394 apply (simp add: option_to_ptr_def option_to_0_def ccorres_cond_iffs) 1395 apply (rule ccorres_rhs_assoc)+ 1396 apply csymbr 1397 apply (rule ccorres_move_array_assertion_pd) 1398 apply csymbr 1399 apply csymbr 1400 apply (rule ccorres_split_nothrow_novcg_dc) 1401 apply (rule storePDE_Basic_ccorres) 1402 apply (simp add: cpde_relation_def Let_def pde_lift_pde_invalid) 1403 apply (fold dc_def) 1404 apply csymbr 1405 apply (ctac add: cleanByVA_PoU_ccorres) 1406 apply (ctac(no_vcg) add:flushTable_ccorres) 1407 apply wp 1408 apply (vcg exspec=cleanByVA_PoU_modifies) 1409 apply wp 1410 apply (fastforce simp: guard_is_UNIV_def Collect_const_mem Let_def 1411 shiftl_t2n field_simps lookup_pd_slot_def) 1412 apply (rule_tac Q="\<lambda>rv s. (case rv of Some pd \<Rightarrow> page_directory_at' pd s | _ \<Rightarrow> True) \<and> invs' s" 1413 in hoare_post_imp) 1414 apply (clarsimp simp: lookup_pd_slot_def Let_def 1415 mask_add_aligned less_kernelBase_valid_pde_offset'' 1416 page_directory_at'_def) 1417 apply (wp pageTableMapped_pd) 1418 apply (clarsimp simp: word_sle_def lookup_pd_slot_def 1419 Let_def shiftl_t2n field_simps 1420 Collect_const_mem pdBits_def pageBits_def) 1421 apply (simp add: unat_shiftr_le_bound unat_eq_0 pdeBits_def) 1422 done 1423 1424lemma return_Null_ccorres: 1425 "ccorres ccap_relation ret__struct_cap_C_' 1426 \<top> UNIV (SKIP # hs) 1427 (return NullCap) (\<acute>ret__struct_cap_C :== CALL cap_null_cap_new() 1428 ;; return_C ret__struct_cap_C_'_update ret__struct_cap_C_')" 1429 apply (rule ccorres_from_vcg_throws) 1430 apply (rule allI, rule conseqPre, vcg) 1431 apply (clarsimp simp add: ccap_relation_NullCap_iff return_def) 1432 done 1433 1434lemma no_0_pd_at'[elim!]: 1435 "\<lbrakk> page_directory_at' 0 s; no_0_obj' s \<rbrakk> \<Longrightarrow> P" 1436 apply (clarsimp simp: page_directory_at'_def) 1437 apply (drule spec[where x=0], clarsimp) 1438 done 1439 1440lemma capFSize_eq: "\<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 (Some (a, b)))) cap; 1441 x34 \<noteq> Wellformed_C.ARMSmallPage\<rbrakk> 1442 \<Longrightarrow> gen_framesize_to_H (capFSize_CL (cap_frame_cap_lift cap)) = x34" 1443 apply (frule (1) cap_get_tag_isCap_unfolded_H_cap) 1444 apply (clarsimp simp: cap_frame_cap_lift cap_to_H_def 1445 case_option_over_if gen_framesize_to_H_def 1446 ARM_H.kernelBase_def 1447 framesize_to_H_def valid_cap'_def 1448 elim!: ccap_relationE simp del: Collect_const) 1449 apply (subgoal_tac "capFSize_CL (cap_frame_cap_lift cap) \<noteq> scast Kernel_C.ARMSmallPage") 1450 apply simp 1451 apply (clarsimp simp: c_valid_cap_def cl_valid_cap_def) 1452 done 1453 1454method return_NullCap_pair_ccorres = 1455 solves \<open>((rule ccorres_rhs_assoc2)+), (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV]), 1456 (rule allI, rule conseqPre, vcg), (clarsimp simp: return_def ccap_relation_NullCap_iff)\<close> 1457 1458lemma Arch_finaliseCap_ccorres: 1459 notes dc_simp[simp del] Collect_const[simp del] 1460 shows 1461 "ccorres (\<lambda>rv rv'. ccap_relation (fst rv) (remainder_C rv') \<and> 1462 ccap_relation (snd rv) (finaliseCap_ret_C.cleanupInfo_C rv')) 1463 ret__struct_finaliseCap_ret_C_' 1464 (invs' and valid_cap' (ArchObjectCap cp) 1465 and (\<lambda>s. 2 ^ acapBits cp \<le> gsMaxObjectSize s)) 1466 (UNIV \<inter> {s. ccap_relation (ArchObjectCap cp) (cap_' s)} 1467 \<inter> {s. final_' s = from_bool is_final}) [] 1468 (Arch.finaliseCap cp is_final) (Call Arch_finaliseCap_'proc)" 1469 apply (cinit lift: cap_' final_' cong: call_ignore_cong) 1470 apply csymbr 1471 apply (simp add: ARM_H.finaliseCap_def cap_get_tag_isCap_ArchObject) 1472 apply (simp add: split_def) 1473 apply (rule ccorres_cases[where P=is_final]; clarsimp) 1474 prefer 2 1475 apply (subgoal_tac "isPageCap cp \<longrightarrow> \<not> isPageTableCap cp \<and> \<not> isASIDPoolCap cp \<and> \<not> isPageDirectoryCap cp") 1476 apply (rule ccorres_cases[where P="isPageCap cp"]; clarsimp) 1477 prefer 2 1478 apply (rule ccorres_inst[where P=\<top> and P'=UNIV]) 1479 apply (cases cp; ccorres_rewrite C_simp_simps: isCap_simps) 1480 apply return_NullCap_pair_ccorres 1481 apply return_NullCap_pair_ccorres 1482 apply return_NullCap_pair_ccorres 1483 apply (subst ccorres_cond_seq2_seq[symmetric]) 1484 apply (rule ccorres_guard_imp) 1485 apply (rule ccorres_rhs_assoc) 1486 apply csymbr 1487 apply ccorres_rewrite 1488 apply (return_NullCap_pair_ccorres, simp+) 1489 apply (subst ccorres_cond_seq2_seq[symmetric]) 1490 apply (rule ccorres_guard_imp) 1491 apply (rule ccorres_rhs_assoc) 1492 apply csymbr 1493 apply ccorres_rewrite 1494 apply (return_NullCap_pair_ccorres, simp+) 1495 apply ccorres_rewrite 1496 apply (rule ccorres_Cond_rhs_Seq) 1497 apply (subgoal_tac "isPageCap cp \<longrightarrow> \<not> isPageDirectoryCap cp \<and> \<not> isASIDPoolCap cp \<and> \<not> isPageTableCap cp") 1498 apply clarsimp 1499 apply (rule ccorres_rhs_assoc)+ 1500 apply csymbr 1501 apply clarsimp 1502 apply (rule ccorres_Cond_rhs_Seq) 1503 apply (subgoal_tac "capVPMappedAddress cp \<noteq> None") 1504 prefer 2 1505 apply (clarsimp simp: isCap_simps) 1506 apply (frule cap_get_tag_isCap_unfolded_H_cap, simp) 1507 apply (frule small_frame_cap_is_mapped_alt) 1508 apply (clarsimp simp: cap_small_frame_cap_lift cap_to_H_def 1509 case_option_over_if 1510 elim!: ccap_relationE simp del: Collect_const) 1511 apply (simp add: split_def) 1512 apply (rule ccorres_rhs_assoc)+ 1513 apply csymbr 1514 apply csymbr 1515 apply csymbr 1516 apply (ctac (no_vcg) add: unmapPage_ccorres) 1517 apply return_NullCap_pair_ccorres 1518 apply (rule wp_post_taut) 1519 apply (subgoal_tac "capVPMappedAddress cp = None") 1520 prefer 2 1521 apply (clarsimp simp: isCap_simps) 1522 apply (frule cap_get_tag_isCap_unfolded_H_cap, simp) 1523 apply (frule small_frame_cap_is_mapped_alt) 1524 apply (clarsimp simp: cap_small_frame_cap_lift cap_to_H_def 1525 case_option_over_if 1526 elim!: ccap_relationE simp del: Collect_const) 1527 apply (simp add: split_def) 1528 apply return_NullCap_pair_ccorres 1529 apply (clarsimp simp: isCap_simps) 1530 apply (rule ccorres_Cond_rhs_Seq) 1531 apply (subgoal_tac "isPageCap cp \<longrightarrow> \<not> isPageDirectoryCap cp \<and> \<not> isASIDPoolCap cp \<and> \<not> isPageTableCap cp") 1532 apply clarsimp 1533 apply (rule ccorres_rhs_assoc)+ 1534 apply csymbr 1535 apply clarsimp 1536 apply (rule ccorres_Cond_rhs_Seq) 1537 apply (subgoal_tac "capVPMappedAddress cp \<noteq> None") 1538 prefer 2 1539 apply (clarsimp simp: isCap_simps) 1540 apply (frule (1) cap_get_tag_isCap_unfolded_H_cap) 1541 apply (frule frame_cap_is_mapped_alt) 1542 apply (clarsimp simp: cap_frame_cap_lift cap_to_H_def 1543 case_option_over_if 1544 elim!: ccap_relationE simp del: Collect_const) 1545 apply simp 1546 apply (rule ccorres_rhs_assoc)+ 1547 apply csymbr 1548 apply csymbr 1549 apply csymbr 1550 apply csymbr 1551 apply (ctac (no_vcg) add: unmapPage_ccorres) 1552 apply return_NullCap_pair_ccorres 1553 apply (rule wp_post_taut) 1554 apply (subgoal_tac "capVPMappedAddress cp = None") 1555 prefer 2 1556 apply (clarsimp simp: isCap_simps) 1557 apply (frule (1) cap_get_tag_isCap_unfolded_H_cap) 1558 apply (frule frame_cap_is_mapped_alt) 1559 apply (clarsimp simp: cap_frame_cap_lift cap_to_H_def 1560 case_option_over_if 1561 elim!: ccap_relationE simp del: Collect_const) 1562 apply clarsimp 1563 apply return_NullCap_pair_ccorres 1564 apply (clarsimp simp: isCap_simps) 1565 apply (clarsimp simp: isCap_simps) 1566 apply (clarsimp simp: isCap_simps) 1567 apply ccorres_rewrite 1568 apply (rule ccorres_Cond_rhs_Seq; clarsimp) 1569 apply (rule ccorres_rhs_assoc)+ 1570 apply csymbr 1571 apply csymbr 1572 apply (ctac (no_vcg) add: deleteASIDPool_ccorres) 1573 apply return_NullCap_pair_ccorres 1574 apply (rule wp_post_taut) 1575 apply (rule ccorres_Cond_rhs_Seq; clarsimp) 1576 apply (rule ccorres_rhs_assoc)+ 1577 apply csymbr 1578 apply clarsimp 1579 apply ccorres_rewrite 1580 apply (rule ccorres_rhs_assoc)+ 1581 apply csymbr 1582 apply csymbr 1583 apply (simp add: if_1_0_0) 1584 apply (subgoal_tac "isPageDirectoryCap cp \<longrightarrow> \<not> isPageTableCap cp \<and> \<not> isASIDPoolCap cp \<and> \<not> isPageCap cp") 1585 apply clarsimp 1586 apply (rule ccorres_Cond_rhs_Seq) 1587 apply (subgoal_tac "capPDMappedASID cp \<noteq> None") 1588 prefer 2 1589 apply (clarsimp simp add: isCap_simps) 1590 apply (frule cap_get_tag_isCap_unfolded_H_cap) 1591 apply (frule cap_lift_page_directory_cap) 1592 apply (clarsimp simp: ccap_relation_def cap_to_H_def capAligned_def 1593 to_bool_def cap_page_directory_cap_lift_def 1594 asid_bits_def 1595 split: if_split_asm) 1596 apply simp 1597 apply (rule ccorres_rhs_assoc)+ 1598 apply csymbr 1599 apply csymbr 1600 apply (ctac (no_vcg) add: deleteASID_ccorres) 1601 apply return_NullCap_pair_ccorres 1602 apply (rule wp_post_taut) 1603 apply (subgoal_tac "capPDMappedASID cp = None") 1604 prefer 2 1605 apply (clarsimp simp add: isCap_simps) 1606 apply (frule cap_get_tag_isCap_unfolded_H_cap) 1607 apply (frule cap_lift_page_directory_cap) 1608 apply (clarsimp simp: ccap_relation_def cap_to_H_def capAligned_def 1609 to_bool_def cap_page_directory_cap_lift_def 1610 asid_bits_def 1611 split: if_split_asm) 1612 apply simp 1613 apply return_NullCap_pair_ccorres 1614 apply (clarsimp simp add: isCap_simps) 1615 apply (rule ccorres_Cond_rhs_Seq) 1616 apply (subgoal_tac "isPageTableCap cp \<longrightarrow> \<not> isPageDirectoryCap cp \<and> \<not> isASIDPoolCap cp \<and> \<not> isPageCap cp") 1617 apply clarsimp 1618 apply (rule ccorres_rhs_assoc)+ 1619 apply csymbr 1620 apply ccorres_rewrite 1621 apply (rule ccorres_rhs_assoc)+ 1622 apply csymbr 1623 apply csymbr 1624 apply (simp add: if_1_0_0) 1625 apply clarsimp 1626 apply (rule ccorres_Cond_rhs_Seq) 1627 apply (subgoal_tac "capPTMappedAddress cp \<noteq> None") 1628 prefer 2 1629 apply (clarsimp simp add: isCap_simps) 1630 apply (frule cap_get_tag_isCap_unfolded_H_cap) 1631 apply (frule cap_lift_page_table_cap) 1632 apply (clarsimp simp: ccap_relation_def cap_to_H_def capAligned_def 1633 to_bool_def cap_page_table_cap_lift_def 1634 asid_bits_def 1635 split: if_split_asm) 1636 apply simp 1637 apply (rule ccorres_rhs_assoc)+ 1638 apply csymbr 1639 apply csymbr 1640 apply csymbr 1641 apply (simp add: split_def) 1642 apply (ctac (no_vcg) add: unmapPageTable_ccorres) 1643 apply return_NullCap_pair_ccorres 1644 apply (rule wp_post_taut) 1645 apply clarsimp 1646 apply (subgoal_tac "capPTMappedAddress cp = None") 1647 prefer 2 1648 apply (clarsimp simp add: isCap_simps) 1649 apply (frule cap_get_tag_isCap_unfolded_H_cap) 1650 apply (frule cap_lift_page_table_cap) 1651 apply (clarsimp simp: ccap_relation_def cap_to_H_def capAligned_def 1652 to_bool_def cap_page_table_cap_lift_def 1653 asid_bits_def 1654 split: if_split_asm) 1655 apply simp 1656 apply return_NullCap_pair_ccorres 1657 apply (clarsimp simp: isCap_simps) 1658 apply (rule ccorres_Cond_rhs_Seq) 1659 apply (subgoal_tac "isPageCap cp \<longrightarrow> \<not> isPageDirectoryCap cp \<and> \<not> isASIDPoolCap cp \<and> \<not> isPageTableCap cp") 1660 apply clarsimp 1661 apply (rule ccorres_rhs_assoc)+ 1662 apply csymbr 1663 apply clarsimp 1664 apply (rule ccorres_Cond_rhs_Seq) 1665 apply (subgoal_tac "capVPMappedAddress cp \<noteq> None") 1666 prefer 2 1667 apply (clarsimp simp: isCap_simps) 1668 apply (frule cap_get_tag_isCap_unfolded_H_cap, simp) 1669 apply (frule small_frame_cap_is_mapped_alt) 1670 apply (clarsimp simp: cap_small_frame_cap_lift cap_to_H_def 1671 case_option_over_if 1672 elim!: ccap_relationE simp del: Collect_const) 1673 apply (simp add: split_def) 1674 apply (rule ccorres_rhs_assoc)+ 1675 apply csymbr 1676 apply csymbr 1677 apply csymbr 1678 apply (ctac (no_vcg) add: unmapPage_ccorres) 1679 apply return_NullCap_pair_ccorres 1680 apply (rule wp_post_taut) 1681 apply (subgoal_tac "capVPMappedAddress cp = None") 1682 prefer 2 1683 apply (clarsimp simp: isCap_simps) 1684 apply (frule cap_get_tag_isCap_unfolded_H_cap, simp) 1685 apply (frule small_frame_cap_is_mapped_alt) 1686 apply (clarsimp simp: cap_small_frame_cap_lift cap_to_H_def 1687 case_option_over_if 1688 elim!: ccap_relationE simp del: Collect_const) 1689 apply (simp add: split_def) 1690 apply return_NullCap_pair_ccorres 1691 apply (clarsimp simp: isCap_simps) 1692 apply (rule ccorres_Cond_rhs_Seq) 1693 apply (subgoal_tac "isPageCap cp \<longrightarrow> \<not> isPageDirectoryCap cp \<and> \<not> isASIDPoolCap cp \<and> \<not> isPageTableCap cp") 1694 apply clarsimp 1695 apply (rule ccorres_rhs_assoc)+ 1696 apply csymbr 1697 apply clarsimp 1698 apply (rule ccorres_Cond_rhs_Seq) 1699 apply (subgoal_tac "capVPMappedAddress cp \<noteq> None") 1700 prefer 2 1701 apply (clarsimp simp: isCap_simps) 1702 apply (frule (1) cap_get_tag_isCap_unfolded_H_cap) 1703 apply (frule frame_cap_is_mapped_alt) 1704 apply (clarsimp simp: cap_frame_cap_lift cap_to_H_def 1705 case_option_over_if 1706 elim!: ccap_relationE simp del: Collect_const) 1707 apply simp 1708 apply (rule ccorres_rhs_assoc)+ 1709 apply csymbr 1710 apply csymbr 1711 apply csymbr 1712 apply csymbr 1713 apply (ctac (no_vcg) add: unmapPage_ccorres) 1714 apply return_NullCap_pair_ccorres 1715 apply (rule wp_post_taut) 1716 apply (subgoal_tac "capVPMappedAddress cp = None") 1717 prefer 2 1718 apply (clarsimp simp: isCap_simps) 1719 apply (frule (1) cap_get_tag_isCap_unfolded_H_cap) 1720 apply (frule frame_cap_is_mapped_alt) 1721 apply (clarsimp simp: cap_frame_cap_lift cap_to_H_def 1722 case_option_over_if 1723 elim!: ccap_relationE simp del: Collect_const) 1724 apply clarsimp 1725 apply return_NullCap_pair_ccorres 1726 apply (clarsimp simp: isCap_simps) 1727 apply clarsimp 1728 apply return_NullCap_pair_ccorres 1729 apply (cases cp ; clarsimp simp: isCap_simps) 1730 apply (cases is_final; clarsimp simp: isCap_simps) 1731 apply (frule cap_get_tag_isCap_unfolded_H_cap) 1732 apply (frule cap_lift_asid_pool_cap) 1733 apply (clarsimp simp: valid_cap'_def) 1734 apply (clarsimp simp: ccap_relation_def cap_to_H_def 1735 cap_asid_pool_cap_lift_def asid_bits_def) 1736 apply (intro conjI; clarsimp) 1737 apply (subgoal_tac "capVPMappedAddress cp \<noteq> None") 1738 apply (clarsimp simp: valid_cap'_def asid_bits_def mask_def word_less_sub_1) 1739 apply (frule cap_get_tag_isCap_unfolded_H_cap, simp) 1740 apply (frule small_frame_cap_is_mapped_alt) 1741 apply (clarsimp simp: cap_small_frame_cap_lift cap_to_H_def 1742 case_option_over_if 1743 elim!: ccap_relationE) 1744 apply (subgoal_tac "capVPMappedAddress cp \<noteq> None") 1745 apply (clarsimp simp: valid_cap'_def asid_bits_def mask_def word_less_sub_1) 1746 apply (frule (1) cap_get_tag_isCap_unfolded_H_cap, simp) 1747 apply (frule frame_cap_is_mapped_alt) 1748 apply (clarsimp simp: cap_frame_cap_lift cap_to_H_def 1749 case_option_over_if 1750 elim!: ccap_relationE) 1751 apply (rule conjI, clarsimp) 1752 apply (frule cap_get_tag_isCap_unfolded_H_cap, simp) 1753 apply (frule small_frame_cap_is_mapped_alt) 1754 apply (subgoal_tac "capVPMappedAddress cp \<noteq> None") 1755 apply (clarsimp simp: cap_small_frame_cap_lift cap_to_H_def 1756 case_option_over_if gen_framesize_to_H_def 1757 Kernel_C.ARMSmallPage_def ARM_H.kernelBase_def 1758 if_split 1759 elim!: ccap_relationE simp del: Collect_const) 1760 apply (clarsimp simp: cap_small_frame_cap_lift cap_to_H_def 1761 case_option_over_if 1762 elim!: ccap_relationE simp del: Collect_const) 1763 apply (frule cap_get_tag_isCap_unfolded_H_cap, simp, simp) 1764 apply (rule conjI, clarsimp) 1765 apply (subgoal_tac "capVPMappedAddress cp \<noteq> None") 1766 apply clarsimp 1767 apply (frule (1) cap_get_tag_isCap_unfolded_H_cap) 1768 apply (frule frame_cap_is_mapped_alt) 1769 apply (frule capFSize_eq, simp) 1770 apply simp 1771 apply (rule conjI) 1772 apply (frule (1) cap_get_tag_isCap_unfolded_H_cap) 1773 apply (frule capFSize_range) 1774 apply (rule order_le_less_trans, assumption, simp) 1775 apply (clarsimp simp: word_less_sub_1) 1776 apply (clarsimp simp: cap_frame_cap_lift cap_to_H_def 1777 case_option_over_if gen_framesize_to_H_def 1778 if_split 1779 elim!: ccap_relationE) 1780 apply (frule (1) cap_get_tag_isCap_unfolded_H_cap) 1781 apply (frule frame_cap_is_mapped_alt) 1782 apply (clarsimp simp: cap_frame_cap_lift cap_to_H_def 1783 case_option_over_if 1784 elim!: ccap_relationE simp del: Collect_const) 1785 apply (frule (1) cap_get_tag_isCap_unfolded_H_cap, simp) 1786 apply (cases is_final; clarsimp) 1787 apply (intro conjI; clarsimp?) 1788 apply (frule cap_get_tag_isCap_unfolded_H_cap) 1789 apply (frule cap_lift_page_table_cap) 1790 apply (subgoal_tac "x42 \<noteq> None") 1791 apply (clarsimp simp: valid_cap'_def asid_bits_def mask_def word_less_sub_1) 1792 apply (clarsimp simp: ccap_relation_def cap_to_H_def capAligned_def 1793 to_bool_def cap_page_table_cap_lift_def 1794 asid_bits_def 1795 split: if_split_asm) 1796 apply (frule cap_get_tag_isCap_unfolded_H_cap) 1797 apply (frule cap_lift_page_table_cap) 1798 apply (subgoal_tac "x42 \<noteq> None") 1799 apply ((clarsimp simp: ccap_relation_def cap_to_H_def capAligned_def 1800 to_bool_def cap_page_table_cap_lift_def 1801 asid_bits_def 1802 split: if_split_asm)+)[2] 1803 apply (frule cap_get_tag_isCap_unfolded_H_cap, simp) 1804 apply (cases is_final; clarsimp) 1805 apply (intro conjI; clarsimp?) 1806 apply (subgoal_tac "x52 \<noteq> None") 1807 apply (clarsimp simp: valid_cap'_def) 1808 apply (clarsimp simp: asid_bits_def mask_def word_less_sub_1) 1809 apply (frule cap_get_tag_isCap_unfolded_H_cap) 1810 apply (frule cap_lift_page_directory_cap) 1811 apply (clarsimp simp: ccap_relation_def cap_to_H_def capAligned_def 1812 to_bool_def cap_page_directory_cap_lift_def 1813 asid_bits_def 1814 split: if_split_asm) 1815 apply (subgoal_tac "x52 \<noteq> None") 1816 apply (frule cap_get_tag_isCap_unfolded_H_cap) 1817 apply (frule cap_lift_page_directory_cap) 1818 apply (clarsimp simp: ccap_relation_def cap_to_H_def capAligned_def 1819 to_bool_def cap_page_directory_cap_lift_def 1820 asid_bits_def 1821 split: if_split_asm) 1822 apply (frule cap_get_tag_isCap_unfolded_H_cap) 1823 apply (frule cap_lift_page_directory_cap) 1824 apply (clarsimp simp: ccap_relation_def cap_to_H_def capAligned_def 1825 to_bool_def cap_page_directory_cap_lift_def 1826 asid_bits_def 1827 split: if_split_asm) 1828 apply (frule cap_get_tag_isCap_unfolded_H_cap, simp) 1829 done 1830 1831lemma ccte_relation_ccap_relation: 1832 "ccte_relation cte cte' \<Longrightarrow> ccap_relation (cteCap cte) (cte_C.cap_C cte')" 1833 by (clarsimp simp: ccte_relation_def ccap_relation_def 1834 cte_to_H_def map_option_Some_eq2 1835 c_valid_cte_def) 1836 1837lemma isFinalCapability_ccorres: 1838 "ccorres ((=) \<circ> from_bool) ret__unsigned_long_' 1839 (cte_wp_at' ((=) cte) slot and invs') 1840 (UNIV \<inter> {s. cte_' s = Ptr slot}) [] 1841 (isFinalCapability cte) (Call isFinalCapability_'proc)" 1842 apply (cinit lift: cte_') 1843 apply (rule ccorres_Guard_Seq) 1844 apply (simp add: Let_def del: Collect_const) 1845 apply (rule ccorres_symb_exec_r) 1846 apply (rule_tac xf'="mdb_'" in ccorres_abstract) 1847 apply ceqv 1848 apply (rule_tac P="mdb_node_to_H (mdb_node_lift rv') = cteMDBNode cte" in ccorres_gen_asm2) 1849 apply csymbr 1850 apply (rule_tac r'="(=) \<circ> from_bool" and xf'="prevIsSameObject_'" 1851 in ccorres_split_nothrow_novcg) 1852 apply (rule ccorres_cond2[where R=\<top>]) 1853 apply (clarsimp simp: Collect_const_mem nullPointer_def) 1854 apply (simp add: mdbPrev_to_H[symmetric]) 1855 apply (rule ccorres_from_vcg[where P=\<top> and P'=UNIV]) 1856 apply (rule allI, rule conseqPre, vcg) 1857 apply (simp add: return_def from_bool_def false_def) 1858 apply (rule ccorres_rhs_assoc)+ 1859 apply (rule ccorres_symb_exec_l[OF _ getCTE_inv getCTE_wp empty_fail_getCTE]) 1860 apply (rule_tac P="cte_wp_at' ((=) cte) slot 1861 and cte_wp_at' ((=) rv) (mdbPrev (cteMDBNode cte)) 1862 and valid_cap' (cteCap rv) 1863 and K (capAligned (cteCap cte) \<and> capAligned (cteCap rv))" 1864 and P'=UNIV in ccorres_from_vcg) 1865 apply (rule allI, rule conseqPre, vcg) 1866 apply (clarsimp simp: return_def mdbPrev_to_H[symmetric]) 1867 apply (simp add: rf_sr_cte_at_validD) 1868 apply (clarsimp simp: cte_wp_at_ctes_of) 1869 apply (rule cmap_relationE1 [OF cmap_relation_cte], assumption+, 1870 simp?, simp add: typ_heap_simps)+ 1871 apply (drule ccte_relation_ccap_relation)+ 1872 apply (rule exI, rule conjI, assumption)+ 1873 apply (auto)[1] 1874 apply ceqv 1875 apply (clarsimp simp del: Collect_const) 1876 apply (rule ccorres_cond2[where R=\<top>]) 1877 apply (simp add: from_bool_0 Collect_const_mem) 1878 apply (rule ccorres_return_C, simp+)[1] 1879 apply csymbr 1880 apply (rule ccorres_cond2[where R=\<top>]) 1881 apply (simp add: nullPointer_def Collect_const_mem mdbNext_to_H[symmetric]) 1882 apply (rule ccorres_return_C, simp+)[1] 1883 apply (rule ccorres_symb_exec_l[OF _ getCTE_inv getCTE_wp empty_fail_getCTE]) 1884 apply (rule_tac P="cte_wp_at' ((=) cte) slot 1885 and cte_wp_at' ((=) rva) (mdbNext (cteMDBNode cte)) 1886 and K (capAligned (cteCap rva) \<and> capAligned (cteCap cte)) 1887 and valid_cap' (cteCap cte)" 1888 and P'=UNIV in ccorres_from_vcg_throws) 1889 apply (rule allI, rule conseqPre, vcg) 1890 apply (clarsimp simp: return_def from_bool_eq_if from_bool_0 1891 mdbNext_to_H[symmetric] rf_sr_cte_at_validD) 1892 apply (clarsimp simp: cte_wp_at_ctes_of split: if_split) 1893 apply (rule cmap_relationE1 [OF cmap_relation_cte], assumption+, 1894 simp?, simp add: typ_heap_simps)+ 1895 apply (drule ccte_relation_ccap_relation)+ 1896 apply (auto simp: false_def true_def from_bool_def split: bool.splits)[1] 1897 apply (wp getCTE_wp') 1898 apply (clarsimp simp add: guard_is_UNIV_def Collect_const_mem false_def 1899 from_bool_0 true_def from_bool_def) 1900 apply vcg 1901 apply (rule conseqPre, vcg) 1902 apply clarsimp 1903 apply (clarsimp simp: Collect_const_mem) 1904 apply (frule(1) rf_sr_cte_at_validD, simp add: typ_heap_simps) 1905 apply (clarsimp simp: cte_wp_at_ctes_of) 1906 apply (erule(1) cmap_relationE1 [OF cmap_relation_cte]) 1907 apply (simp add: typ_heap_simps) 1908 apply (clarsimp simp add: ccte_relation_def map_option_Some_eq2) 1909 by (auto, 1910 auto dest!: ctes_of_valid' [OF _ invs_valid_objs'] 1911 elim!: valid_capAligned) 1912 1913lemmas cleanup_info_wf'_simps[simp] = cleanup_info_wf'_def[split_simps capability.split] 1914 1915lemma cteDeleteOne_ccorres: 1916 "ccorres dc xfdc 1917 (invs' and cte_wp_at' (\<lambda>ct. w = -1 \<or> cteCap ct = NullCap 1918 \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = w)) slot) 1919 ({s. gs_get_assn cteDeleteOne_'proc (ghost'state_' (globals s)) = w} 1920 \<inter> {s. slot_' s = Ptr slot}) [] 1921 (cteDeleteOne slot) (Call cteDeleteOne_'proc)" 1922 unfolding cteDeleteOne_def 1923 apply (rule ccorres_symb_exec_l' 1924 [OF _ getCTE_inv getCTE_sp empty_fail_getCTE]) 1925 apply (cinit' lift: slot_' cong: call_ignore_cong) 1926 apply (rule ccorres_move_c_guard_cte) 1927 apply csymbr 1928 apply (rule ccorres_abstract_cleanup) 1929 apply csymbr 1930 apply (rule ccorres_gen_asm2, 1931 erule_tac t="ret__unsigned = scast cap_null_cap" 1932 and s="cteCap cte = NullCap" 1933 in ssubst) 1934 apply (clarsimp simp only: when_def unless_def dc_def[symmetric]) 1935 apply (rule ccorres_cond2[where R=\<top>]) 1936 apply (clarsimp simp: Collect_const_mem) 1937 apply (rule ccorres_rhs_assoc)+ 1938 apply csymbr 1939 apply csymbr 1940 apply (rule ccorres_Guard_Seq) 1941 apply (rule ccorres_basic_srnoop) 1942 apply (ctac(no_vcg) add: isFinalCapability_ccorres[where slot=slot]) 1943 apply (rule_tac A="invs' and cte_wp_at' ((=) cte) slot" 1944 in ccorres_guard_imp2[where A'=UNIV]) 1945 apply (simp add: split_def dc_def[symmetric] 1946 del: Collect_const) 1947 apply (rule ccorres_move_c_guard_cte) 1948 apply (ctac(no_vcg) add: finaliseCap_True_standin_ccorres) 1949 apply (rule ccorres_assert) 1950 apply (simp add: dc_def[symmetric]) 1951 apply csymbr 1952 apply (ctac add: emptySlot_ccorres) 1953 apply (simp add: pred_conj_def finaliseCapTrue_standin_simple_def) 1954 apply (strengthen invs_mdb_strengthen' invs_urz) 1955 apply (wp typ_at_lifts isFinalCapability_inv 1956 | strengthen invs_valid_objs')+ 1957 apply (clarsimp simp: from_bool_def true_def irq_opt_relation_def 1958 invs_pspace_aligned' cte_wp_at_ctes_of) 1959 apply (erule(1) cmap_relationE1 [OF cmap_relation_cte]) 1960 apply (clarsimp simp: typ_heap_simps ccte_relation_ccap_relation ccap_relation_NullCap_iff) 1961 apply (wp isFinalCapability_inv) 1962 apply simp 1963 apply (simp del: Collect_const add: false_def) 1964 apply (rule ccorres_return_Skip) 1965 apply (clarsimp simp: Collect_const_mem cte_wp_at_ctes_of) 1966 apply (erule(1) cmap_relationE1 [OF cmap_relation_cte]) 1967 apply (clarsimp simp: typ_heap_simps cap_get_tag_isCap 1968 dest!: ccte_relation_ccap_relation) 1969 apply (auto simp: o_def) 1970 done 1971 1972lemma getIRQSlot_ccorres_stuff: 1973 "\<lbrakk> (s, s') \<in> rf_sr \<rbrakk> \<Longrightarrow> 1974 CTypesDefs.ptr_add (intStateIRQNode_' (globals s')) (uint (irq :: 10 word)) 1975 = Ptr (irq_node' s + 2 ^ cte_level_bits * ucast irq)" 1976 apply (clarsimp simp add: rf_sr_def cstate_relation_def Let_def 1977 cinterrupt_relation_def) 1978 apply (simp add: objBits_simps cte_level_bits_def 1979 size_of_def mult.commute mult.left_commute of_int_uint_ucast ) 1980 done 1981 1982lemma deletingIRQHandler_ccorres: 1983 "ccorres dc xfdc (invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) 1984 (UNIV \<inter> {s. irq_opt_relation (Some irq) (irq_' s)}) [] 1985 (deletingIRQHandler irq) (Call deletingIRQHandler_'proc)" 1986 apply (cinit lift: irq_' cong: call_ignore_cong) 1987 apply (clarsimp simp: irq_opt_relation_def ptr_add_assertion_def dc_def[symmetric] 1988 cong: call_ignore_cong ) 1989 apply (rule_tac r'="\<lambda>rv rv'. rv' = Ptr rv" 1990 and xf'="slot_'" in ccorres_split_nothrow) 1991 apply (simp add: sint_ucast_eq_uint is_down) 1992 apply (rule ccorres_move_array_assertion_irq) 1993 apply (rule ccorres_from_vcg[where P=\<top> and P'=UNIV]) 1994 1995 apply (rule allI, rule conseqPre, vcg) 1996 apply (clarsimp simp: getIRQSlot_def liftM_def getInterruptState_def 1997 locateSlot_conv) 1998 apply (simp add: bind_def simpler_gets_def return_def 1999 ucast_nat_def uint_up_ucast is_up) 2000 apply (erule getIRQSlot_ccorres_stuff) 2001 apply ceqv 2002 apply (rule ccorres_symb_exec_l) 2003 apply (rule ccorres_symb_exec_l) 2004 apply (rule ccorres_symb_exec_r) 2005 apply (ctac add: cteDeleteOne_ccorres[where w="scast cap_notification_cap"]) 2006 apply vcg 2007 apply (rule conseqPre, vcg, clarsimp simp: rf_sr_def 2008 gs_set_assn_Delete_cstate_relation[unfolded o_def]) 2009 apply (wp getCTE_wp' | simp add: getSlotCap_def getIRQSlot_def locateSlot_conv 2010 getInterruptState_def)+ 2011 apply vcg 2012 apply (clarsimp simp: cap_get_tag_isCap ghost_assertion_data_get_def 2013 ghost_assertion_data_set_def) 2014 apply (simp add: cap_tag_defs) 2015 apply (clarsimp simp: cte_wp_at_ctes_of Collect_const_mem 2016 irq_opt_relation_def Kernel_C.maxIRQ_def) 2017 apply (drule word_le_nat_alt[THEN iffD1]) 2018 apply (clarsimp simp:uint_0_iff unat_gt_0 uint_up_ucast is_up unat_def[symmetric]) 2019 done 2020 2021lemma Zombie_new_spec: 2022 "\<forall>s. \<Gamma>\<turnstile> ({s} \<inter> {s. type_' s = 32 \<or> type_' s < 31}) Call Zombie_new_'proc 2023 {s'. cap_zombie_cap_lift (ret__struct_cap_C_' s') = 2024 \<lparr> capZombieID_CL = \<^bsup>s\<^esup>ptr && ~~ mask (if \<^bsup>s\<^esup>type = (1 << 5) then 5 else unat (\<^bsup>s\<^esup>type + 1)) 2025 || \<^bsup>s\<^esup>number___unsigned_long && mask (if \<^bsup>s\<^esup>type = (1 << 5) then 5 else unat (\<^bsup>s\<^esup>type + 1)), 2026 capZombieType_CL = \<^bsup>s\<^esup>type && mask 6 \<rparr> 2027 \<and> cap_get_tag (ret__struct_cap_C_' s') = scast cap_zombie_cap}" 2028 apply vcg 2029 apply (clarsimp simp: word_sle_def) 2030 apply (simp add: mask_def word_log_esimps[where 'a=32, simplified]) 2031 apply clarsimp 2032 apply (simp add: word_add_less_mono1[where k=1 and j="0x1F", simplified]) 2033 done 2034 2035lemma irq_opt_relation_Some_ucast: 2036 "\<lbrakk> x && mask 10 = x; ucast x \<le> (scast Kernel_C.maxIRQ :: 10 word) \<or> x \<le> (scast Kernel_C.maxIRQ :: word32) \<rbrakk> 2037 \<Longrightarrow> irq_opt_relation (Some (ucast x)) (ucast ((ucast x):: 10 word))" 2038 using ucast_ucast_mask[where x=x and 'a=10, symmetric] 2039 apply (simp add: irq_opt_relation_def) 2040 apply (rule conjI, clarsimp simp: irqInvalid_def Kernel_C.maxIRQ_def) 2041 apply (simp only: unat_arith_simps ) 2042 apply (clarsimp simp: word_le_nat_alt Kernel_C.maxIRQ_def) 2043 done 2044 2045lemmas upcast_ucast_id = Word_Lemmas.ucast_up_inj 2046 2047lemma irq_opt_relation_Some_ucast': 2048 "\<lbrakk> x && mask 10 = x; ucast x \<le> (scast Kernel_C.maxIRQ :: 10 word) \<or> x \<le> (scast Kernel_C.maxIRQ :: word32) \<rbrakk> 2049 \<Longrightarrow> irq_opt_relation (Some (ucast x)) (ucast x)" 2050 apply (rule_tac P = "%y. irq_opt_relation (Some (ucast x)) y" in subst[rotated]) 2051 apply (rule irq_opt_relation_Some_ucast[rotated]) 2052 apply simp+ 2053 apply (rule word_eqI) 2054 apply (drule_tac f = "%x. (x !! n)" in arg_cong) 2055 apply (clarsimp simp add:nth_ucast and_bang word_size) 2056done 2057 2058lemma ccap_relation_IRQHandler_mask: 2059 "\<lbrakk> ccap_relation acap ccap; isIRQHandlerCap acap \<rbrakk> 2060 \<Longrightarrow> capIRQ_CL (cap_irq_handler_cap_lift ccap) && mask 10 2061 = capIRQ_CL (cap_irq_handler_cap_lift ccap)" 2062 apply (simp only: cap_get_tag_isCap[symmetric]) 2063 apply (drule ccap_relation_c_valid_cap) 2064 apply (simp add: c_valid_cap_def cap_irq_handler_cap_lift cl_valid_cap_def) 2065 done 2066 2067lemma prepare_thread_delete_ccorres: 2068 "ccorres dc xfdc \<top> UNIV [] 2069 (prepareThreadDelete thread) (Call Arch_prepareThreadDelete_'proc)" 2070 unfolding prepareThreadDelete_def 2071 apply (rule ccorres_Call) 2072 apply (rule Arch_prepareThreadDelete_impl[unfolded Arch_prepareThreadDelete_body_def]) 2073 apply (rule ccorres_return_Skip) 2074 done 2075 2076lemma finaliseCap_ccorres: 2077 "\<And>final. 2078 ccorres (\<lambda>rv rv'. ccap_relation (fst rv) (finaliseCap_ret_C.remainder_C rv') 2079 \<and> ccap_relation (snd rv) (finaliseCap_ret_C.cleanupInfo_C rv')) 2080 ret__struct_finaliseCap_ret_C_' 2081 (invs' and sch_act_simple and valid_cap' cap and (\<lambda>s. ksIdleThread s \<notin> capRange cap) 2082 and (\<lambda>s. 2 ^ capBits cap \<le> gsMaxObjectSize s)) 2083 (UNIV \<inter> {s. ccap_relation cap (cap_' s)} \<inter> {s. final_' s = from_bool final} 2084 \<inter> {s. exposed_' s = from_bool flag (* dave has name wrong *)}) [] 2085 (finaliseCap cap final flag) (Call finaliseCap_'proc)" 2086 apply (rule_tac F="capAligned cap" in Corres_UL_C.ccorres_req) 2087 apply (clarsimp simp: valid_capAligned) 2088 apply (case_tac "P :: bool" for P) 2089 apply (rule ccorres_guard_imp2, erule finaliseCap_True_cases_ccorres) 2090 apply simp 2091 apply (subgoal_tac "\<exists>acap. (0 <=s (-1 :: word8)) \<or> acap = capCap cap") 2092 prefer 2 apply simp 2093 apply (erule exE) 2094 apply (cinit lift: cap_' final_' exposed_' cong: call_ignore_cong) 2095 apply csymbr 2096 apply (simp del: Collect_const) 2097 apply (rule ccorres_Cond_rhs_Seq) 2098 apply (clarsimp simp: cap_get_tag_isCap isCap_simps from_bool_neq_0 2099 cong: if_cong simp del: Collect_const) 2100 apply (clarsimp simp: word_sle_def) 2101 apply (rule ccorres_if_lhs) 2102 apply (rule ccorres_fail) 2103 apply (simp add: liftM_def del: Collect_const) 2104 apply (rule ccorres_rhs_assoc)+ 2105 apply (rule ccorres_add_return2) 2106 apply (ccorres_rewrite) 2107 apply (ctac add: Arch_finaliseCap_ccorres) 2108 apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV]) 2109 apply (rule allI, rule conseqPre, vcg) 2110 apply (clarsimp simp: return_def Collect_const_mem) 2111 apply wp 2112 apply (vcg exspec=Arch_finaliseCap_modifies) 2113 apply (simp add: cap_get_tag_isCap Collect_False 2114 del: Collect_const) 2115 apply csymbr 2116 apply (simp add: cap_get_tag_isCap Collect_False Collect_True 2117 del: Collect_const) 2118 apply (rule ccorres_if_lhs) 2119 apply (simp, rule ccorres_fail) 2120 apply (simp add: from_bool_0 Collect_True Collect_False false_def 2121 del: Collect_const) 2122 apply csymbr 2123 apply (simp add: cap_get_tag_isCap Collect_False Collect_True 2124 del: Collect_const) 2125 apply (rule ccorres_if_lhs) 2126 apply (simp add: Let_def) 2127 apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV]) 2128 apply (rule allI, rule conseqPre, vcg) 2129 apply (clarsimp simp: cap_get_tag_isCap word_sle_def 2130 return_def word_mod_less_divisor 2131 less_imp_neq [OF word_mod_less_divisor]) 2132 apply (frule cap_get_tag_to_H, erule(1) cap_get_tag_isCap [THEN iffD2]) 2133 apply (clarsimp simp: isCap_simps capAligned_def ccap_relation_NullCap_iff 2134 objBits_simps' word_bits_conv 2135 signed_shift_guard_simpler_32) 2136 apply (rule conjI) 2137 apply (simp add: word_less_nat_alt) 2138 apply (rule conjI) 2139 apply (auto simp: word_less_nat_alt)[1] 2140 apply (simp add: ccap_relation_def cap_zombie_cap_lift) 2141 apply (simp add: cap_to_H_def isZombieTCB_C_def ZombieTCB_C_def) 2142 apply (simp add: less_mask_eq word_less_nat_alt less_imp_neq) 2143 apply (simp add: mod_mask_drop[where n=5] mask_def[where n=5] 2144 less_imp_neq [OF word_mod_less_divisor] 2145 less_imp_neq Let_def) 2146 apply (thin_tac "a = b" for a b)+ 2147 apply (subgoal_tac "P" for P) 2148 apply (subst add.commute, subst unatSuc, assumption)+ 2149 apply (intro impI, rule conjI) 2150 apply (rule word_eqI) 2151 apply (simp add: word_size word_ops_nth_size nth_w2p 2152 less_Suc_eq_le is_aligned_nth) 2153 apply (safe, simp_all)[1] 2154 apply (simp add: shiftL_nat ccap_relation_NullCap_iff) 2155 apply (rule trans, rule unat_power_lower32[symmetric]) 2156 apply (simp add: word_bits_conv) 2157 apply (rule unat_cong, rule word_eqI) 2158 apply (simp add: word_size word_ops_nth_size nth_w2p 2159 is_aligned_nth less_Suc_eq_le) 2160 apply (safe, simp_all)[1] 2161 apply (subst add.commute, subst eq_diff_eq[symmetric]) 2162 apply (clarsimp simp: minus_one_norm) 2163 apply (rule ccorres_if_lhs) 2164 apply (simp add: Let_def getThreadCSpaceRoot_def locateSlot_conv 2165 Collect_True Collect_False 2166 del: Collect_const) 2167 apply (rule ccorres_rhs_assoc)+ 2168 apply csymbr 2169 apply csymbr 2170 apply csymbr 2171 apply csymbr 2172 apply (rule ccorres_Guard_Seq)+ 2173 apply csymbr 2174 apply (ctac(no_vcg) add: unbindNotification_ccorres) 2175 apply (ctac(no_vcg) add: suspend_ccorres[OF cteDeleteOne_ccorres]) 2176 apply (ctac(no_vcg) add: prepare_thread_delete_ccorres) 2177 apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV]) 2178 apply (rule allI, rule conseqPre, vcg) 2179 apply (clarsimp simp: word_sle_def return_def) 2180 apply (subgoal_tac "cap_get_tag capa = scast cap_thread_cap") 2181 apply (drule(1) cap_get_tag_to_H) 2182 apply (clarsimp simp: isCap_simps capAligned_def ccap_relation_NullCap_iff) 2183 apply (simp add: ccap_relation_def cap_zombie_cap_lift) 2184 apply (simp add: cap_to_H_def isZombieTCB_C_def ZombieTCB_C_def 2185 mask_def) 2186 apply (simp add: cte_level_bits_def tcbCTableSlot_def 2187 Kernel_C.tcbCTable_def tcbCNodeEntries_def 2188 word_bool_alg.conj_disj_distrib2 2189 word_bw_assocs) 2190 apply (simp add: objBits_simps ctcb_ptr_to_tcb_ptr_def) 2191 apply (frule is_aligned_add_helper[where p="tcbptr - ctcb_offset" and d=ctcb_offset for tcbptr]) 2192 apply (simp add: ctcb_offset_defs objBits_defs) 2193 apply (simp add: mask_def irq_opt_relation_def objBits_defs) 2194 apply (simp add: cap_get_tag_isCap) 2195 apply wp+ 2196 apply (rule ccorres_if_lhs) 2197 apply (simp add: Let_def) 2198 apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV]) 2199 apply (rule allI, rule conseqPre, vcg) 2200 apply (clarsimp simp: return_def ccap_relation_NullCap_iff) 2201 apply (simp add: isArchCap_T_isArchObjectCap[symmetric] 2202 del: Collect_const) 2203 apply (rule ccorres_if_lhs) 2204 apply (simp add: Collect_False Collect_True Let_def true_def 2205 del: Collect_const) 2206 apply (rule_tac P="(capIRQ cap) \<le> ARM.maxIRQ" in ccorres_gen_asm) 2207 apply (rule ccorres_rhs_assoc)+ 2208 apply csymbr 2209 apply csymbr 2210 apply (rule_tac xf'=irq_' in ccorres_abstract,ceqv) 2211 apply (rule_tac P="rv' = ucast (capIRQ cap)" in ccorres_gen_asm2) 2212 apply (ctac(no_vcg) add: deletingIRQHandler_ccorres) 2213 apply (rule ccorres_from_vcg_throws[where P=\<top> ]) 2214 apply (rule allI, rule conseqPre, vcg) 2215 apply (clarsimp simp: return_def) 2216 apply (frule cap_get_tag_to_H, erule(1) cap_get_tag_isCap [THEN iffD2]) 2217 apply (simp add: ccap_relation_NullCap_iff split: if_split) 2218 apply wp 2219 apply (rule ccorres_if_lhs) 2220 apply simp 2221 apply (rule ccorres_fail) 2222 apply (rule ccorres_add_return, rule ccorres_split_nothrow_novcg[where r'=dc and xf'=xfdc]) 2223 apply (rule ccorres_Cond_rhs) 2224 apply (simp add: ccorres_cond_iffs dc_def[symmetric]) 2225 apply (rule ccorres_return_Skip) 2226 apply (rule ccorres_Cond_rhs) 2227 apply (simp add: ccorres_cond_iffs dc_def[symmetric]) 2228 apply (rule ccorres_return_Skip) 2229 apply (rule ccorres_Cond_rhs) 2230 apply (rule ccorres_inst[where P=\<top> and P'=UNIV]) 2231 apply simp 2232 apply (rule ccorres_Cond_rhs) 2233 apply (simp add: ccorres_cond_iffs dc_def[symmetric]) 2234 apply (rule ccorres_return_Skip) 2235 apply (simp add: ccorres_cond_iffs dc_def[symmetric]) 2236 apply (rule ccorres_return_Skip) 2237 apply (rule ceqv_refl) 2238 apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV]) 2239 apply (rule allI, rule conseqPre, vcg) 2240 apply (clarsimp simp: return_def ccap_relation_NullCap_iff 2241 irq_opt_relation_def) 2242 apply wp 2243 apply (simp add: guard_is_UNIV_def) 2244 apply (clarsimp simp: cap_get_tag_isCap word_sle_def Collect_const_mem 2245 false_def from_bool_def) 2246 apply (intro impI conjI) 2247 apply (clarsimp split: bool.splits) 2248 apply (clarsimp split: bool.splits) 2249 apply (clarsimp simp: valid_cap'_def isCap_simps) 2250 apply (clarsimp simp: isCap_simps capRange_def capAligned_def) 2251 apply (clarsimp simp: isCap_simps valid_cap'_def) 2252 apply (clarsimp simp: isCap_simps capRange_def capAligned_def) 2253 apply (clarsimp simp: isCap_simps valid_cap'_def ) 2254 apply clarsimp 2255 apply (clarsimp simp: isCap_simps valid_cap'_def ) 2256 apply (clarsimp simp: tcb_ptr_to_ctcb_ptr_def ccap_relation_def isCap_simps 2257 c_valid_cap_def cap_thread_cap_lift_def cap_to_H_def 2258 ctcb_ptr_to_tcb_ptr_def Let_def 2259 split: option.splits cap_CL.splits if_splits) 2260 apply clarsimp 2261 apply (frule cap_get_tag_to_H, erule(1) cap_get_tag_isCap [THEN iffD2]) 2262 apply (clarsimp simp: isCap_simps from_bool_def false_def) 2263 apply (clarsimp simp: tcb_cnode_index_defs ptr_add_assertion_def) 2264 apply clarsimp 2265 apply (frule cap_get_tag_to_H, erule(1) cap_get_tag_isCap [THEN iffD2]) 2266 apply (frule(1) ccap_relation_IRQHandler_mask) 2267 apply (clarsimp simp: isCap_simps irqInvalid_def 2268 valid_cap'_def ARM.maxIRQ_def 2269 Kernel_C.maxIRQ_def) 2270 apply (rule irq_opt_relation_Some_ucast', simp) 2271 apply (clarsimp simp: isCap_simps irqInvalid_def 2272 valid_cap'_def ARM.maxIRQ_def 2273 Kernel_C.maxIRQ_def) 2274 apply fastforce 2275 apply clarsimp 2276 apply (frule cap_get_tag_to_H, erule(1) cap_get_tag_isCap [THEN iffD2]) 2277 apply (frule(1) ccap_relation_IRQHandler_mask) 2278 apply (clarsimp simp add:mask_eq_ucast_eq) 2279 done 2280 end 2281 2282end 2283