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 Syscall_C 12imports 13 Interrupt_C 14 Ipc_C 15 Invoke_C 16 Schedule_C 17 Arch_C 18begin 19 20context begin interpretation Arch . (*FIXME: arch_split*) 21crunch sch_act_wf [wp]: replyFromKernel "\<lambda>s. sch_act_wf (ksSchedulerAction s) s" 22end 23 24context kernel_m begin 25 26(* FIXME: should do this from the beginning *) 27declare true_def [simp] false_def [simp] 28 29lemma ccorres_If_False: 30 "ccorres_underlying sr Gamm r xf arrel axf R R' hs b c 31 \<Longrightarrow> ccorres_underlying sr Gamm r xf arrel axf 32 (R and (\<lambda>_. \<not> P)) R' hs (If P a b) c" 33 by (rule ccorres_gen_asm, simp) 34 35definition 36 one_on_true :: "bool \<Rightarrow> nat" 37where 38 "one_on_true P \<equiv> if P then 1 else 0" 39 40lemma one_on_true_True[simp]: "one_on_true True = 1" 41 by (simp add: one_on_true_def) 42 43lemma one_on_true_eq_0[simp]: "(one_on_true P = 0) = (\<not> P)" 44 by (simp add: one_on_true_def split: if_split) 45 46lemma cap_cases_one_on_true_sum: 47 "one_on_true (isZombie cap) + one_on_true (isArchObjectCap cap) 48 + one_on_true (isThreadCap cap) + one_on_true (isCNodeCap cap) 49 + one_on_true (isNotificationCap cap) + one_on_true (isEndpointCap cap) 50 + one_on_true (isUntypedCap cap) + one_on_true (isReplyCap cap) 51 + one_on_true (isIRQControlCap cap) + one_on_true (isIRQHandlerCap cap) 52 + one_on_true (isNullCap cap) + one_on_true (isDomainCap cap) = 1" 53 by (cases cap, simp_all add: isCap_simps) 54 55lemma performInvocation_Endpoint_ccorres: 56 "ccorres (K (K \<bottom>) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') 57 (invs' and st_tcb_at' simple' thread and ep_at' epptr 58 and sch_act_sane and (\<lambda>s. thread = ksCurThread s 59 \<and> (\<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)))) 60 (UNIV \<inter> {s. block_' s = from_bool blocking} 61 \<inter> {s. call_' s = from_bool do_call} 62 \<inter> {s. badge_' s = badge} 63 \<inter> {s. canGrant_' s = from_bool canGrant} 64 \<inter> {s. ep_' s = ep_Ptr epptr} 65 \<inter> \<lbrace>badge && mask 28 = badge\<rbrace>) [] 66 (liftE (sendIPC blocking do_call badge canGrant thread epptr)) 67 (Call performInvocation_Endpoint_'proc)" 68 apply cinit 69 apply (ctac add: sendIPC_ccorres) 70 apply (simp add: return_returnOk) 71 apply (rule ccorres_return_CE, simp+)[1] 72 apply wp 73 apply simp 74 apply (vcg exspec=sendIPC_modifies) 75 apply (clarsimp simp add: rf_sr_ksCurThread sch_act_sane_not) 76 done 77 78(* This lemma now assumes 'weak_sch_act_wf (ksSchedulerAction s) s' in place of 'sch_act_simple'. *) 79 80lemma performInvocation_Notification_ccorres: 81 "ccorres (K (K \<bottom>) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') 82 (invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) 83 (UNIV \<inter> {s. ntfn_' s = ntfn_Ptr ntfnptr} 84 \<inter> {s. badge_' s = badge} 85 \<inter> {s. message_' s = message}) [] 86 (liftE (sendSignal ntfnptr badge)) 87 (Call performInvocation_Notification_'proc)" 88 apply cinit 89 apply (ctac add: sendSignal_ccorres) 90 apply (simp add: return_returnOk) 91 apply (rule ccorres_return_CE, simp+)[1] 92 apply wp 93 apply simp 94 apply (vcg exspec=sendSignal_modifies) 95 apply simp 96 done 97 98lemma performInvocation_Reply_ccorres: 99 "ccorres (K (K \<bottom>) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') 100 (invs' and tcb_at' receiver and st_tcb_at' active' sender and sch_act_simple 101 and ((Not o real_cte_at' slot) or cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot) 102 and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte)) 103 slot and (\<lambda>s. ksCurThread s = sender)) 104 (UNIV \<inter> {s. thread_' s = tcb_ptr_to_ctcb_ptr receiver} 105 \<inter> {s. slot_' s = cte_Ptr slot}) [] 106 (liftE (doReplyTransfer sender receiver slot)) 107 (Call performInvocation_Reply_'proc)" 108 apply cinit 109 apply (ctac add: doReplyTransfer_ccorres) 110 apply (simp add: return_returnOk) 111 apply (rule ccorres_return_CE, simp+)[1] 112 apply wp 113 apply simp 114 apply (vcg exspec=doReplyTransfer_modifies) 115 apply (simp add: rf_sr_ksCurThread) 116 apply (auto simp: isReply_def elim!: pred_tcb'_weakenE) 117 done 118 119lemma decodeInvocation_ccorres: 120 "interpret_excaps extraCaps' = excaps_map extraCaps 121 \<Longrightarrow> 122 ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') 123 (invs' and (\<lambda>s. ksCurThread s = thread) and ct_active' and sch_act_simple 124 and valid_cap' cp and (\<lambda>s. \<forall>x \<in> zobj_refs' cp. ex_nonz_cap_to' x s) 125 and (excaps_in_mem extraCaps \<circ> ctes_of) 126 and cte_wp_at' (diminished' cp \<circ> cteCap) slot 127 and (\<lambda>s. \<forall>v \<in> set extraCaps. ex_cte_cap_wp_to' isCNodeCap (snd v) s) 128 and (\<lambda>s. \<forall>v \<in> set extraCaps. s \<turnstile>' fst v \<and> cte_at' (snd v) s) 129 and (\<lambda>s. \<forall>v \<in> set extraCaps. \<forall>y \<in> zobj_refs' (fst v). ex_nonz_cap_to' y s) 130 and (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)) 131 and sysargs_rel args buffer) 132 (UNIV \<inter> {s. call_' s = from_bool isCall} 133 \<inter> {s. block_' s = from_bool isBlocking} 134 \<inter> {s. call_' s = from_bool isCall} 135 \<inter> {s. block_' s = from_bool isBlocking} 136 \<inter> {s. invLabel_' s = label} 137 \<inter> {s. unat (length___unsigned_long_' s) = length args} 138 \<inter> {s. capIndex_' s = cptr} 139 \<inter> {s. slot_' s = cte_Ptr slot} 140 \<inter> {s. excaps_' s = extraCaps'} 141 \<inter> {s. ccap_relation cp (cap_' s)} 142 \<inter> {s. buffer_' s = option_to_ptr buffer}) [] 143 (decodeInvocation label args cptr slot cp extraCaps 144 >>= invocationCatch thread isBlocking isCall id) 145 (Call decodeInvocation_'proc)" 146 apply (cinit' lift: call_' block_' invLabel_' length___unsigned_long_' 147 capIndex_' slot_' excaps_' cap_' buffer_') 148 apply csymbr 149 apply (simp add: cap_get_tag_isCap decodeInvocation_def 150 cong: if_cong StateSpace.state.fold_congs 151 globals.fold_congs 152 del: Collect_const) 153 apply (cut_tac cap=cp in cap_cases_one_on_true_sum) 154 apply (rule ccorres_Cond_rhs_Seq) 155 apply (simp add: Let_def isArchCap_T_isArchObjectCap 156 liftME_invocationCatch from_bool_neq_0) 157 apply (rule ccorres_split_throws) 158 apply (rule ccorres_trim_returnE) 159 apply simp 160 apply simp 161 apply (rule ccorres_call, rule Arch_decodeInvocation_ccorres [where buffer=buffer]) 162 apply assumption 163 apply simp+ 164 apply (vcg exspec=Arch_decodeInvocation_modifies) 165 apply simp 166 apply csymbr 167 apply (simp add: cap_get_tag_isCap del: Collect_const) 168 apply (rule ccorres_Cond_rhs) 169 apply (simp add: invocationCatch_def throwError_bind) 170 apply (rule syscall_error_throwError_ccorres_n) 171 apply (simp add: syscall_error_to_H_cases) 172 apply (rule ccorres_Cond_rhs) 173 apply (simp add: invocationCatch_def throwError_bind) 174 apply (rule syscall_error_throwError_ccorres_n) 175 apply (simp add: syscall_error_to_H_cases) 176 apply (rule ccorres_Cond_rhs) 177 apply (simp add: if_to_top_of_bind) 178 apply (rule ccorres_rhs_assoc)+ 179 apply csymbr 180 apply (rule ccorres_if_cond_throws2[where Q=\<top> and Q'=\<top>]) 181 apply (clarsimp simp: isCap_simps Collect_const_mem) 182 apply (frule cap_get_tag_isCap_unfolded_H_cap) 183 apply (drule(1) cap_get_tag_to_H) 184 apply (clarsimp simp: to_bool_def) 185 apply (simp add: throwError_bind invocationCatch_def) 186 apply (rule syscall_error_throwError_ccorres_n) 187 apply (simp add: syscall_error_to_H_cases) 188 apply (simp add: returnOk_bind ccorres_invocationCatch_Inr 189 performInvocation_def bind_assoc liftE_bindE) 190 apply (ctac add: setThreadState_ccorres) 191 apply csymbr 192 apply csymbr 193 apply csymbr 194 apply (rule ccorres_pre_getCurThread) 195 apply (simp only: liftE_bindE[symmetric]) 196 apply (ctac add: performInvocation_Endpoint_ccorres) 197 apply (rule ccorres_alternative2) 198 apply (rule ccorres_return_CE, simp+)[1] 199 apply (rule ccorres_return_C_errorE, simp+)[1] 200 apply wp 201 apply simp 202 apply (vcg exspec=performInvocation_Endpoint_modifies) 203 apply simp 204 apply (rule hoare_use_eq[where f=ksCurThread]) 205 apply (wp sts_invs_minor' sts_st_tcb_at'_cases 206 setThreadState_ct' hoare_vcg_all_lift sts_ksQ')+ 207 apply simp 208 apply (vcg exspec=setThreadState_modifies) 209 apply vcg 210 apply (rule ccorres_Cond_rhs) 211 apply (rule ccorres_rhs_assoc)+ 212 apply (csymbr) 213 apply (simp add: if_to_top_of_bind Collect_const[symmetric] 214 del: Collect_const) 215 apply (rule ccorres_if_cond_throws2[where Q=\<top> and Q'=\<top>]) 216 apply (clarsimp simp: isCap_simps Collect_const_mem) 217 apply (frule cap_get_tag_isCap_unfolded_H_cap) 218 apply (drule(1) cap_get_tag_to_H) 219 apply (clarsimp simp: to_bool_def) 220 apply (simp add: throwError_bind invocationCatch_def) 221 apply (rule syscall_error_throwError_ccorres_n) 222 apply (simp add: syscall_error_to_H_cases) 223 apply (simp add: returnOk_bind ccorres_invocationCatch_Inr 224 performInvocation_def bindE_assoc) 225 apply (simp add: liftE_bindE) 226 apply (ctac add: setThreadState_ccorres) 227 apply csymbr 228 apply csymbr 229 apply (simp only: liftE_bindE[symmetric]) 230 apply (ctac(no_vcg) add: performInvocation_Notification_ccorres) 231 apply (rule ccorres_alternative2) 232 apply (rule ccorres_return_CE, simp+)[1] 233 apply (rule ccorres_return_C_errorE, simp+)[1] 234 apply wp 235 apply (wp sts_invs_minor') 236 apply simp 237 apply (vcg exspec=setThreadState_modifies) 238 apply vcg 239 apply (rule ccorres_Cond_rhs) 240 apply (simp add: if_to_top_of_bind) 241 apply (rule ccorres_rhs_assoc)+ 242 apply csymbr 243 apply (rule ccorres_if_cond_throws2[where Q=\<top> and Q'=\<top>]) 244 apply (clarsimp simp: isCap_simps Collect_const_mem) 245 apply (frule cap_get_tag_isCap_unfolded_H_cap) 246 apply (clarsimp simp: cap_get_tag_ReplyCap to_bool_def) 247 apply (simp add: throwError_bind invocationCatch_def) 248 apply (rule syscall_error_throwError_ccorres_n) 249 apply (simp add: syscall_error_to_H_cases) 250 apply (simp add: returnOk_bind ccorres_invocationCatch_Inr 251 performInvocation_def liftE_bindE 252 bind_assoc) 253 apply (ctac add: setThreadState_ccorres) 254 apply csymbr 255 apply (rule ccorres_pre_getCurThread) 256 apply (simp only: liftE_bindE[symmetric]) 257 apply (ctac add: performInvocation_Reply_ccorres) 258 apply (rule ccorres_alternative2) 259 apply (rule ccorres_return_CE, simp+)[1] 260 apply (rule ccorres_return_C_errorE, simp+)[1] 261 apply wp 262 apply simp 263 apply (vcg exspec=performInvocation_Reply_modifies) 264 apply (simp add: cur_tcb'_def[symmetric]) 265 apply (rule_tac R="\<lambda>rv s. ksCurThread s = thread" in hoare_post_add) 266 apply (simp cong: conj_cong) 267 apply (strengthen imp_consequent) 268 apply (wp sts_invs_minor' sts_st_tcb_at'_cases) 269 apply simp 270 apply (vcg exspec=setThreadState_modifies) 271 apply vcg 272 apply (rule ccorres_Cond_rhs) 273 apply (simp add: if_to_top_of_bind) 274 apply (rule ccorres_trim_returnE, simp+) 275 apply (simp add: liftME_invocationCatch o_def) 276 apply (rule ccorres_call, rule decodeTCBInvocation_ccorres) 277 apply assumption 278 apply (simp+)[3] 279 apply (rule ccorres_Cond_rhs) 280 apply (rule ccorres_trim_returnE, simp+) 281 apply (simp add: liftME_invocationCatch o_def) 282 apply (rule ccorres_call, 283 erule decodeDomainInvocation_ccorres[unfolded o_def], 284 simp+)[1] 285 apply (rule ccorres_Cond_rhs) 286 apply (simp add: if_to_top_of_bind) 287 apply (rule ccorres_trim_returnE, simp+) 288 apply (simp add: liftME_invocationCatch o_def) 289 apply (rule ccorres_call, 290 erule decodeCNodeInvocation_ccorres[unfolded o_def], 291 simp+)[1] 292 apply (rule ccorres_Cond_rhs) 293 apply simp 294 apply (rule ccorres_trim_returnE, simp+) 295 apply (simp add: liftME_invocationCatch) 296 apply (rule ccorres_call, 297 erule decodeUntypedInvocation_ccorres, simp+)[1] 298 apply (rule ccorres_Cond_rhs) 299 apply (simp add: liftME_invocationCatch) 300 apply (rule ccorres_trim_returnE, simp+) 301 apply (rule ccorres_call, erule decodeIRQControlInvocation_ccorres, 302 simp+)[1] 303 apply (rule ccorres_Cond_rhs) 304 apply (simp add: Let_def liftME_invocationCatch) 305 apply (rule ccorres_rhs_assoc)+ 306 apply csymbr 307 apply (rule ccorres_trim_returnE, simp+) 308 apply (rule ccorres_call, 309 erule decodeIRQHandlerInvocation_ccorres, simp+) 310 apply (rule ccorres_inst[where P=\<top> and P'=UNIV]) 311 apply (simp add: isArchCap_T_isArchObjectCap one_on_true_def from_bool_0) 312 apply (rule conjI) 313 apply (clarsimp simp: tcb_at_invs' ct_in_state'_def 314 simple_sane_strg) 315 apply (clarsimp simp: cte_wp_at_ctes_of valid_cap'_def isCap_simps from_bool_neq_0 316 unat_eq_0 sysargs_rel_n_def n_msgRegisters_def valid_tcb_state'_def 317 | rule conjI | erule pred_tcb'_weakenE disjE 318 | drule st_tcb_at_idle_thread')+ 319 apply fastforce 320 apply (simp add: cap_lift_capEPBadge_mask_eq) 321 apply (clarsimp simp: rf_sr_ksCurThread Collect_const_mem 322 cap_get_tag_isCap "StrictC'_thread_state_defs") 323 apply (frule word_unat.Rep_inverse') 324 apply (simp add: cap_get_tag_isCap[symmetric] cap_get_tag_ReplyCap) 325 apply (rule conjI) 326 apply (simp add: cap_get_tag_isCap) 327 apply (clarsimp simp: isCap_simps cap_get_tag_to_H from_bool_neq_0) 328 apply (insert ccap_relation_IRQHandler_mask, elim meta_allE, drule(1) meta_mp) 329 apply (rule conjI | clarsimp 330 | drule(1) cap_get_tag_to_H 331 | simp add: cap_endpoint_cap_lift_def 332 cap_notification_cap_lift_def 333 cap_reply_cap_lift_def cap_lift_endpoint_cap 334 cap_lift_notification_cap cap_lift_reply_cap 335 from_bool_to_bool_and_1 word_size 336 order_le_less_trans[OF word_and_le1] 337 mask_eq_iff_w2p word_size ucast_ucast_mask 338 isCap_simps mask_eq_ucast_eq 339 mask_eq_iff_w2p[THEN trans[OF eq_commute]])+ 340 done 341 342lemma ccorres_Call_Seq: 343 "\<lbrakk> \<Gamma> f = Some v; ccorres r xf P P' hs a (v ;; c) \<rbrakk> 344 \<Longrightarrow> ccorres r xf P P' hs a (Call f ;; c)" 345 apply (erule ccorres_semantic_equivD1) 346 apply (rule semantic_equivI) 347 apply (auto elim!: exec_elim_cases intro: exec.intros) 348 done 349 350lemma wordFromRights_mask_0: 351 "wordFromRights rghts && ~~ mask 4 = 0" 352 apply (simp add: wordFromRights_def word_ao_dist word_or_zero 353 split: cap_rights.split) 354 apply (simp add: mask_def split: if_split) 355 done 356 357lemma wordFromRights_mask_eq: 358 "wordFromRights rghts && mask 4 = wordFromRights rghts" 359 apply (cut_tac x="wordFromRights rghts" and y="mask 4" and z="~~ mask 4" 360 in word_bool_alg.conj_disj_distrib) 361 apply (simp add: wordFromRights_mask_0) 362 done 363 364lemma loadWordUser_user_word_at: 365 "\<lbrace>\<lambda>s. \<forall>rv. user_word_at rv x s \<longrightarrow> Q rv s\<rbrace> loadWordUser x \<lbrace>Q\<rbrace>" 366 apply (simp add: loadWordUser_def user_word_at_def 367 doMachineOp_def split_def) 368 apply wp 369 apply (clarsimp simp: pointerInUserData_def 370 loadWord_def in_monad 371 is_aligned_mask) 372 done 373 374lemma mapM_loadWordUser_user_words_at: 375 "\<lbrace>\<lambda>s. \<forall>rv. (\<forall>x < length xs. user_word_at (rv ! x) (xs ! x) s) 376 \<and> length rv = length xs \<longrightarrow> Q rv s\<rbrace> 377 mapM loadWordUser xs \<lbrace>Q\<rbrace>" 378 apply (induct xs arbitrary: Q) 379 apply (simp add: mapM_def sequence_def) 380 apply wp 381 apply (simp add: mapM_Cons) 382 apply wp 383 apply assumption 384 apply (wp loadWordUser_user_word_at) 385 apply clarsimp 386 apply (drule spec, erule mp) 387 apply clarsimp 388 apply (case_tac x) 389 apply simp 390 apply simp 391 done 392 393lemma getSlotCap_slotcap_in_mem: 394 "\<lbrace>\<top>\<rbrace> getSlotCap slot \<lbrace>\<lambda>cap s. slotcap_in_mem cap slot (ctes_of s)\<rbrace>" 395 apply (simp add: getSlotCap_def) 396 apply (wp getCTE_wp') 397 apply (clarsimp simp: cte_wp_at_ctes_of slotcap_in_mem_def) 398 done 399 400lemma lookupExtraCaps_excaps_in_mem[wp]: 401 "\<lbrace>\<top>\<rbrace> lookupExtraCaps thread buffer info \<lbrace>\<lambda>rv s. excaps_in_mem rv (ctes_of s)\<rbrace>,-" 402 apply (simp add: excaps_in_mem_def lookupExtraCaps_def lookupCapAndSlot_def 403 split_def) 404 apply (wp mapME_set) 405 apply (wp getSlotCap_slotcap_in_mem | simp)+ 406 done 407 408lemma getCurThread_ccorres: 409 "ccorres ((=) \<circ> tcb_ptr_to_ctcb_ptr) thread_' 410 \<top> UNIV hs getCurThread (\<acute>thread :== \<acute>ksCurThread)" 411 apply (rule ccorres_from_vcg) 412 apply (rule allI, rule conseqPre, vcg) 413 apply (clarsimp simp: getCurThread_def simpler_gets_def 414 rf_sr_ksCurThread) 415 done 416 417lemma getMessageInfo_ccorres: 418 "ccorres (\<lambda>rv rv'. rv = messageInfoFromWord rv') ret__unsigned_long_' \<top> 419 (UNIV \<inter> {s. thread_' s = tcb_ptr_to_ctcb_ptr thread} 420 \<inter> {s. reg_' s = register_from_H ARM_HYP_H.msgInfoRegister}) [] 421 (getMessageInfo thread) (Call getRegister_'proc)" 422 apply (simp add: getMessageInfo_def liftM_def[symmetric] 423 ccorres_liftM_simp) 424 apply (rule ccorres_rel_imp, rule ccorres_guard_imp2, rule getRegister_ccorres) 425 apply simp 426 apply simp 427 done 428 429lemma messageInfoFromWord_spec: 430 "\<forall>s. \<Gamma> \<turnstile> {s} Call messageInfoFromWord_'proc 431 {s'. seL4_MessageInfo_lift (ret__struct_seL4_MessageInfo_C_' s') 432 = mi_from_H (messageInfoFromWord (w_' s))}" 433 apply (rule allI, rule conseqPost, rule messageInfoFromWord_spec[rule_format]) 434 apply simp_all 435 apply (clarsimp simp: seL4_MessageInfo_lift_def mi_from_H_def 436 messageInfoFromWord_def Let_def msgLabelBits_def 437 Types_H.msgLengthBits_def Types_H.msgExtraCapBits_def 438 Types_H.msgMaxExtraCaps_def shiftL_nat) 439 done 440 441lemma threadGet_tcbIpcBuffer_ccorres [corres]: 442 "ccorres (=) w_bufferPtr_' (tcb_at' tptr) UNIV hs 443 (threadGet tcbIPCBuffer tptr) 444 (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t (Ptr &(tcb_ptr_to_ctcb_ptr tptr\<rightarrow> 445 [''tcbIPCBuffer_C''])::word32 ptr)\<rbrace> 446 (\<acute>w_bufferPtr :== 447 h_val (hrs_mem \<acute>t_hrs) 448 (Ptr &(tcb_ptr_to_ctcb_ptr tptr\<rightarrow>[''tcbIPCBuffer_C''])::word32 ptr)))" 449 apply (rule ccorres_guard_imp2) 450 apply (rule ccorres_add_return2) 451 apply (rule ccorres_pre_threadGet) 452 apply (rule_tac P = "obj_at' (\<lambda>tcb. tcbIPCBuffer tcb = x) tptr" and 453 P'="{s'. \<exists>ctcb. 454 cslift s' (tcb_ptr_to_ctcb_ptr tptr) = Some ctcb \<and> 455 tcbIPCBuffer_C ctcb = x }" in ccorres_from_vcg) 456 apply (rule allI, rule conseqPre, vcg) 457 apply clarsimp 458 apply (clarsimp simp: return_def typ_heap_simps') 459 apply (clarsimp simp: obj_at'_def ctcb_relation_def) 460 done 461 462lemma handleInvocation_def2: 463 "handleInvocation isCall isBlocking = 464 do thread \<leftarrow> getCurThread; 465 info \<leftarrow> getMessageInfo thread; 466 ptr \<leftarrow> asUser thread (getRegister ARM_HYP_H.capRegister); 467 v \<leftarrow> (doE (cap, slot) \<leftarrow> capFaultOnFailure ptr False (lookupCapAndSlot thread ptr); 468 buffer \<leftarrow> withoutFailure (VSpace_H.lookupIPCBuffer False thread); 469 extracaps \<leftarrow> lookupExtraCaps thread buffer info; 470 returnOk (slot, cap, extracaps, buffer) 471 odE); 472 case v of Inl f \<Rightarrow> liftE (when isBlocking (handleFault thread f)) 473 | Inr (slot, cap, extracaps, buffer) \<Rightarrow> 474 do args \<leftarrow> getMRs thread buffer info; 475 v' \<leftarrow> do v \<leftarrow> RetypeDecls_H.decodeInvocation (msgLabel info) args ptr slot cap extracaps; 476 invocationCatch thread isBlocking isCall id v od; 477 case v' of Inr _ \<Rightarrow> liftE (replyOnRestart thread [] isCall) 478 | Inl (Inl syserr) \<Rightarrow> liftE (when isCall (replyFromKernel thread 479 (msgFromSyscallError syserr))) 480 | Inl (Inr preempt) \<Rightarrow> throwError preempt 481 od 482 od" 483 apply (simp add: handleInvocation_def Syscall_H.syscall_def runExceptT_def 484 liftE_bindE cong: sum.case_cong) 485 apply (rule ext, (rule bind_apply_cong [OF refl])+) 486 apply (clarsimp simp: bind_assoc split: sum.split) 487 apply (rule bind_apply_cong [OF refl])+ 488 apply (clarsimp simp: invocationCatch_def throwError_bind 489 liftE_bindE bind_assoc 490 split: sum.split) 491 apply (rule bind_apply_cong [OF refl])+ 492 apply (simp add: bindE_def bind_assoc) 493 apply (rule bind_apply_cong [OF refl])+ 494 apply (clarsimp simp: lift_def throwError_bind returnOk_bind split: sum.split) 495 apply (simp cong: bind_cong add: ts_Restart_case_helper') 496 apply (simp add: when_def[symmetric] replyOnRestart_def[symmetric]) 497 apply (simp add: liftE_def replyOnRestart_twice alternative_bind 498 alternative_refl split: if_split) 499 done 500 501lemma thread_state_to_tsType_eq_Restart: 502 "(thread_state_to_tsType ts = scast ThreadState_Restart) 503 = (ts = Restart)" 504 by (cases ts, simp_all add: "StrictC'_thread_state_defs") 505 506lemma wordFromMessageInfo_spec: 507 "\<forall>s. \<Gamma>\<turnstile> {s} Call wordFromMessageInfo_'proc 508 {s'. \<forall>mi. seL4_MessageInfo_lift (mi_' s) = mi_from_H mi 509 \<longrightarrow> ret__unsigned_long_' s' = wordFromMessageInfo mi}" 510 apply (rule allI, rule conseqPost, rule wordFromMessageInfo_spec2[rule_format]) 511 prefer 2 512 apply simp 513 apply (clarsimp simp: wordFromMessageInfo_def Let_def Types_H.msgExtraCapBits_def 514 Types_H.msgLengthBits_def Types_H.msgMaxExtraCaps_def 515 shiftL_nat) 516 apply (clarsimp simp: mi_from_H_def seL4_MessageInfo_lift_def 517 word_bw_comms word_bw_assocs word_bw_lcs) 518 done 519 520lemma handleDoubleFault_ccorres: 521 "ccorres dc xfdc (invs' and tcb_at' tptr and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and 522 sch_act_not tptr and (\<lambda>s. \<forall>p. tptr \<notin> set (ksReadyQueues s p))) 523 (UNIV \<inter> {s. tptr_' s = tcb_ptr_to_ctcb_ptr tptr}) 524 [] (handleDoubleFault tptr ex1 ex2) 525 (Call handleDoubleFault_'proc)" 526 apply (cinit lift: tptr_') 527 apply (subst ccorres_seq_skip'[symmetric]) 528 apply (ctac (no_vcg)) 529 apply (rule ccorres_symb_exec_l) 530 apply (rule ccorres_return_Skip) 531 apply (wp asUser_inv getRestartPC_inv)+ 532 apply (rule empty_fail_asUser) 533 apply (simp add: getRestartPC_def) 534 apply wp 535 apply clarsimp 536 apply (simp add: ThreadState_Inactive_def) 537 apply (fastforce simp: valid_tcb_state'_def) 538 done 539 540lemma cap_case_EndpointCap_CanSend_CanGrant: 541 "(case cap of EndpointCap v0 v1 True v3 True \<Rightarrow> f v0 v1 v3 542 | _ \<Rightarrow> g) 543 = (if (isEndpointCap cap \<and> capEPCanSend cap \<and> capEPCanGrant cap) 544 then f (capEPPtr cap) (capEPBadge cap) (capEPCanReceive cap) 545 else g)" 546 by (simp add: isCap_simps 547 split: capability.split bool.split) 548 549lemma threadGet_tcbFaultHandler_ccorres [corres]: 550 "ccorres (=) handlerCPtr_' (tcb_at' tptr) UNIV hs 551 (threadGet tcbFaultHandler tptr) 552 (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t (tcb_ptr_to_ctcb_ptr tptr)\<rbrace> 553 (\<acute>handlerCPtr :== 554 h_val (hrs_mem \<acute>t_hrs) 555 (Ptr &(tcb_ptr_to_ctcb_ptr tptr\<rightarrow>[''tcbFaultHandler_C''])::word32 ptr)))" 556 apply (rule ccorres_guard_imp2) 557 apply (rule ccorres_add_return2) 558 apply (rule ccorres_pre_threadGet) 559 apply (rule_tac P = "obj_at' (\<lambda>tcb. tcbFaultHandler tcb = x) tptr" and 560 P'="{s'. \<exists> ctcb. 561 cslift s' (tcb_ptr_to_ctcb_ptr tptr) = Some ctcb \<and> 562 tcbFaultHandler_C ctcb = x }" in ccorres_from_vcg) 563 apply (rule allI, rule conseqPre, vcg) 564 apply clarsimp 565 apply (clarsimp simp: return_def typ_heap_simps') 566 apply (clarsimp simp: obj_at'_def ctcb_relation_def) 567done 568 569lemma rf_sr_tcb_update_twice: 570 "h_t_valid (hrs_htd (hrs2 (globals s') (t_hrs_' (gs2 (globals s'))))) c_guard 571 (ptr (t_hrs_' (gs2 (globals s'))) (globals s')) 572 \<Longrightarrow> ((s, globals_update (\<lambda>gs. t_hrs_'_update (\<lambda>ths. 573 hrs_mem_update (heap_update (ptr ths gs :: tcb_C ptr) (v ths gs)) 574 (hrs_mem_update (heap_update (ptr ths gs) (v' ths gs)) (hrs2 gs ths))) (gs2 gs)) s') \<in> rf_sr) 575 = ((s, globals_update (\<lambda>gs. t_hrs_'_update (\<lambda>ths. 576 hrs_mem_update (heap_update (ptr ths gs) (v ths gs)) (hrs2 gs ths)) (gs2 gs)) s') \<in> rf_sr)" 577 by (simp add: rf_sr_def cstate_relation_def Let_def 578 cpspace_relation_def typ_heap_simps' 579 carch_state_relation_def 580 cmachine_state_relation_def) 581 582lemma hrs_mem_update_use_hrs_mem: 583 "hrs_mem_update f = (\<lambda>hrs. (hrs_mem_update $ (\<lambda>_. f (hrs_mem hrs))) hrs)" 584 by (simp add: hrs_mem_update_def hrs_mem_def fun_eq_iff) 585 586lemma sendFaultIPC_ccorres: 587 "ccorres (cfault_rel2 \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') 588 (invs' and st_tcb_at' simple' tptr and sch_act_not tptr and 589 (\<lambda>s. \<forall>p. tptr \<notin> set (ksReadyQueues s p))) 590 (UNIV \<inter> {s. (cfault_rel (Some fault) (seL4_Fault_lift(current_fault_' (globals s))) 591 (lookup_fault_lift(current_lookup_fault_' (globals s))))} 592 \<inter> {s. tptr_' s = tcb_ptr_to_ctcb_ptr tptr}) 593 [] (sendFaultIPC tptr fault) 594 (Call sendFaultIPC_'proc)" 595 apply (cinit lift: tptr_' cong: call_ignore_cong) 596 apply (simp add: liftE_bindE del:Collect_const cong:call_ignore_cong) 597 apply (rule ccorres_symb_exec_r) 598 apply (rule ccorres_split_nothrow) 599 apply (rule threadGet_tcbFaultHandler_ccorres) 600 apply ceqv 601 602 apply (rule_tac xf'=lu_ret___struct_lookupCap_ret_C_' 603 in ccorres_split_nothrow_callE) 604 apply (rule capFaultOnFailure_ccorres) 605 apply (rule lookupCap_ccorres) 606 apply simp 607 apply simp 608 apply simp 609 apply simp 610 apply ceqv 611 apply clarsimp 612 apply csymbr+ 613 614 apply (simp add: cap_case_EndpointCap_CanSend_CanGrant) 615 616 apply (rule ccorres_rhs_assoc2) 617 618 apply (rule ccorres_symb_exec_r) 619 apply (rule_tac Q=\<top> 620 and Q'="\<lambda>s'. 621 ( ret__int_' s' = 622 (if ( (cap_get_tag (lookupCap_ret_C.cap_C rv'a) = scast cap_endpoint_cap) \<and> 623 (capCanSend_CL (cap_endpoint_cap_lift (lookupCap_ret_C.cap_C rv'a)))\<noteq>0 \<and> 624 (capCanGrant_CL (cap_endpoint_cap_lift (lookupCap_ret_C.cap_C rv'a)))\<noteq>0) 625 then 1 else 0))" 626 in ccorres_cond_both') 627 apply clarsimp 628 apply (frule cap_get_tag_isCap(4)[symmetric], 629 fastforce simp: cap_get_tag_EndpointCap to_bool_def) 630 631 apply (rule ccorres_rhs_assoc) 632 apply (rule ccorres_rhs_assoc) 633 apply (rule ccorres_rhs_assoc) 634 apply (simp add: liftE_def bind_assoc) 635 636 apply (rule_tac ccorres_split_nothrow_novcg) 637 apply (rule_tac P=\<top> and P'=invs' 638 and R="{s. 639 (cfault_rel (Some fault) 640 (seL4_Fault_lift(current_fault_' (globals s))) 641 (lookup_fault_lift(original_lookup_fault_' s)))}" 642 in threadSet_ccorres_lemma4) 643 apply vcg 644 apply (clarsimp simp: typ_heap_simps' rf_sr_tcb_update_twice) 645 646 apply (intro conjI allI impI) 647 apply (simp add: typ_heap_simps' rf_sr_def) 648 apply (rule rf_sr_tcb_update_no_queue2[unfolded rf_sr_def, simplified], 649 assumption+, (simp add: typ_heap_simps')+) 650 apply (rule ball_tcb_cte_casesI, simp+) 651 apply (simp add: ctcb_relation_def cthread_state_relation_def ) 652 apply (case_tac "tcbState tcb", simp+) 653 apply (simp add: rf_sr_def) 654 apply (rule rf_sr_tcb_update_no_queue2[unfolded rf_sr_def, simplified], 655 assumption+, (simp add: typ_heap_simps' | simp only: hrs_mem_update_use_hrs_mem)+) 656 apply (rule ball_tcb_cte_casesI, simp+) 657 apply (clarsimp simp: typ_heap_simps') 658 apply (simp add: ctcb_relation_def cthread_state_relation_def) 659 apply (rule conjI) 660 apply (case_tac "tcbState tcb", simp+) 661 apply (simp add: cfault_rel_def) 662 apply (clarsimp) 663 apply (clarsimp simp: seL4_Fault_lift_def Let_def is_cap_fault_def 664 split: if_split_asm) 665 apply ceqv 666 667 apply csymbr 668 apply csymbr 669 apply (ctac (no_vcg) add: sendIPC_ccorres) 670 apply (ctac (no_vcg) add: ccorres_return_CE [unfolded returnOk_def comp_def]) 671 apply wp 672 apply (wp threadSet_pred_tcb_no_state threadSet_invs_trivial threadSet_typ_at_lifts 673 | simp)+ 674 675 apply (clarsimp simp: guard_is_UNIV_def) 676 apply (frule cap_get_tag_isCap(4)[symmetric]) 677 apply (clarsimp simp: cap_get_tag_EndpointCap to_bool_def) 678 apply (drule cap_get_tag_isCap(4) [symmetric]) 679 apply (clarsimp simp: isCap_simps cap_endpoint_cap_lift cap_lift_capEPBadge_mask_eq) 680 681 apply clarsimp 682 apply (rule_tac P=\<top> and P'=UNIV 683 in ccorres_from_vcg_throws) 684 apply clarsimp 685 apply (clarsimp simp add: throwError_def throw_def return_def) 686 apply (rule conseqPre, vcg) 687 apply (clarsimp simp: EXCEPTION_FAULT_def EXCEPTION_NONE_def) 688 apply (simp add: cfault_rel2_def cfault_rel_def EXCEPTION_FAULT_def) 689 apply (simp add: seL4_Fault_CapFault_lift) 690 apply (simp add: lookup_fault_missing_capability_lift is_cap_fault_def) 691 692 apply vcg 693 694 apply (clarsimp simp: if_1_0_0) 695 apply (rule conseqPre, vcg) 696 apply clarsimp 697 698 apply clarsimp 699 apply (rule ccorres_split_throws) 700 apply (rule_tac P=\<top> and P'="{x. errstate x= err'}" 701 in ccorres_from_vcg_throws) 702 apply clarsimp 703 apply (clarsimp simp add: throwError_def throw_def return_def) 704 apply (rule conseqPre, vcg) 705 apply (clarsimp simp: EXCEPTION_FAULT_def EXCEPTION_NONE_def) 706 apply (simp add: cfault_rel2_def cfault_rel_def EXCEPTION_FAULT_def) 707 apply (simp add: seL4_Fault_CapFault_lift is_cap_fault_def) 708 apply (erule lookup_failure_rel_fault_lift [rotated, unfolded EXCEPTION_NONE_def, simplified], 709 assumption) 710 711 apply vcg 712 apply (clarsimp simp: inQ_def) 713 apply (rule_tac Q="\<lambda>a b. invs' b \<and> st_tcb_at' simple' tptr b 714 \<and> sch_act_not tptr b \<and> valid_cap' a b 715 \<and> (\<forall>p. tptr \<notin> set (ksReadyQueues b p))" 716 and E="\<lambda> _. \<top>" 717 in hoare_post_impErr) 718 apply (wp) 719 apply (clarsimp simp: isCap_simps) 720 apply (clarsimp simp: valid_cap'_def pred_tcb_at') 721 apply simp 722 723 apply (clarsimp simp: if_1_0_0) 724 apply (vcg exspec=lookupCap_modifies) 725 apply clarsimp 726 apply wp 727 apply (clarsimp simp: if_1_0_0) 728 apply (vcg) 729 730 apply (clarsimp, vcg) 731 apply (rule conseqPre, vcg) 732 apply clarsimp 733 apply (clarsimp simp: if_1_0_0) 734 apply fastforce 735 done 736 737lemma handleFault_ccorres: 738 "ccorres dc xfdc (invs' and st_tcb_at' simple' t and 739 sch_act_not t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p))) 740 (UNIV \<inter> {s. (cfault_rel (Some flt) (seL4_Fault_lift(current_fault_' (globals s))) 741 (lookup_fault_lift(current_lookup_fault_' (globals s))) )} 742 \<inter> {s. tptr_' s = tcb_ptr_to_ctcb_ptr t}) 743 hs (handleFault t flt) 744 (Call handleFault_'proc)" 745 apply (cinit lift: tptr_') 746 apply (simp add: catch_def) 747 apply (rule ccorres_symb_exec_r) 748 apply (rule ccorres_split_nothrow_novcg_case_sum) 749 apply (ctac (no_vcg) add: sendFaultIPC_ccorres) 750 apply ceqv 751 apply clarsimp 752 apply (rule ccorres_cond_empty) 753 apply (rule ccorres_return_Skip') 754 apply clarsimp 755 apply (rule ccorres_cond_univ) 756 apply (ctac (no_vcg) add: handleDoubleFault_ccorres [unfolded dc_def]) 757 apply (simp add: sendFaultIPC_def) 758 apply wp 759 apply ((wp hoare_vcg_all_lift_R hoare_drop_impE_R |wpc |simp add: throw_def)+)[1] 760 apply clarsimp 761 apply ((wp hoare_vcg_all_lift_R hoare_drop_impE_R |wpc |simp add: throw_def)+)[1] 762 apply (wp) 763 apply (simp add: guard_is_UNIV_def) 764 apply (simp add: guard_is_UNIV_def) 765 apply clarsimp 766 apply vcg 767 apply clarsimp 768 apply (rule conseqPre, vcg) 769 apply clarsimp 770 apply (clarsimp simp: pred_tcb_at') 771 done 772 773lemma getMessageInfo_less_4: 774 "\<lbrace>\<top>\<rbrace> getMessageInfo t \<lbrace>\<lambda>rv s. msgExtraCaps rv < 4\<rbrace>" 775 including no_pre 776 apply (simp add: getMessageInfo_def) 777 apply wp 778 apply (rule hoare_strengthen_post, rule hoare_vcg_prop) 779 apply (simp add: messageInfoFromWord_def Let_def 780 Types_H.msgExtraCapBits_def) 781 apply (rule minus_one_helper5, simp) 782 apply simp 783 apply (rule word_and_le1) 784 done 785 786lemma invs_queues_imp: 787 "invs' s \<longrightarrow> valid_queues s" 788 by clarsimp 789 790(* FIXME: move *) 791lemma length_CL_from_H [simp]: 792 "length_CL (mi_from_H mi) = msgLength mi" 793 by (simp add: mi_from_H_def) 794 795lemma getMRs_length: 796 "\<lbrace>\<lambda>s. msgLength mi \<le> 120\<rbrace> getMRs thread buffer mi 797 \<lbrace>\<lambda>args s. if buffer = None then length args = min (unat n_msgRegisters) (unat (msgLength mi)) 798 else length args = unat (msgLength mi)\<rbrace>" 799 apply (cases buffer) 800 apply (simp add: getMRs_def) 801 apply (rule hoare_pre, wp) 802 apply (rule asUser_const_rv) 803 apply simp 804 apply (wp mapM_length) 805 apply (simp add: min_def length_msgRegisters) 806 apply (clarsimp simp: n_msgRegisters_def) 807 apply (simp add: getMRs_def) 808 apply (rule hoare_pre, wp) 809 apply simp 810 apply (wp mapM_length asUser_const_rv mapM_length)+ 811 apply (clarsimp simp: length_msgRegisters) 812 apply (simp add: min_def split: if_splits) 813 apply (clarsimp simp: word_le_nat_alt) 814 apply (simp add: msgMaxLength_def msgLengthBits_def n_msgRegisters_def) 815 done 816 817lemma getMessageInfo_msgLength': 818 "\<lbrace>\<top>\<rbrace> getMessageInfo t \<lbrace>\<lambda>rv s. msgLength rv \<le> 0x78\<rbrace>" 819 including no_pre 820 apply (simp add: getMessageInfo_def) 821 apply wp 822 apply (rule hoare_strengthen_post, rule hoare_vcg_prop) 823 apply (simp add: messageInfoFromWord_def Let_def msgMaxLength_def not_less 824 Types_H.msgExtraCapBits_def split: if_split ) 825 done 826 827lemma handleInvocation_ccorres: 828 "ccorres (K dc \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') 829 (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and 830 ct_active' and sch_act_simple and 831 (\<lambda>s. \<forall>x. ksCurThread s \<notin> set (ksReadyQueues s x))) 832 (UNIV \<inter> {s. isCall_' s = from_bool isCall} 833 \<inter> {s. isBlocking_' s = from_bool isBlocking}) [] 834 (handleInvocation isCall isBlocking) (Call handleInvocation_'proc)" 835 apply (cinit' lift: isCall_' isBlocking_' 836 simp: whileAnno_def handleInvocation_def2) 837 apply (simp add: liftE_bindE del: Collect_const cong: call_ignore_cong) 838 apply (ctac(no_vcg) add: getCurThread_ccorres) 839 apply (ctac(no_vcg) add: getMessageInfo_ccorres) 840 apply (simp del: Collect_const cong: call_ignore_cong) 841 apply csymbr 842 apply (ctac(no_vcg) add: getRegister_ccorres) 843 apply (simp add: Syscall_H.syscall_def 844 liftE_bindE split_def bindE_bind_linearise 845 cong: call_ignore_cong 846 del: Collect_const) 847 apply (rule_tac ccorres_split_nothrow_case_sum) 848 apply (ctac add: capFaultOnFailure_ccorres 849 [OF lookupCapAndSlot_ccorres]) 850 apply ceqv 851 apply (simp add: ccorres_cond_iffs Collect_False 852 cong: call_ignore_cong 853 del: Collect_const) 854 apply (simp only: bind_assoc) 855 apply (ctac(no_vcg) add: lookupIPCBuffer_ccorres) 856 apply (simp add: liftME_def bindE_assoc del: Collect_const) 857 apply (simp add: bindE_bind_linearise del: Collect_const) 858 apply (rule_tac xf'="\<lambda>s. (status_' s, 859 current_extra_caps_' (globals s))" 860 and ef'=fst and vf'=snd and es=errstate 861 in ccorres_split_nothrow_novcg_case_sum) 862 apply (rule ccorres_call, rule lookupExtraCaps_ccorres, simp+) 863 apply (rule ceqv_tuple2, ceqv, ceqv) 864 apply (simp add: returnOk_bind liftE_bindE 865 Collect_False 866 ccorres_cond_iffs ts_Restart_case_helper' 867 del: Collect_const cong: bind_cong) 868 apply (rule ccorres_rhs_assoc2, 869 rule ccorres_rhs_assoc2, 870 rule_tac xf'="length___unsigned_long_'" 871 and r'="\<lambda>rv rv'. unat rv' = length rv" 872 in ccorres_split_nothrow) 873 apply (rule ccorres_add_return2) 874 apply (rule ccorres_symb_exec_l) 875 apply (rule_tac P="\<lambda>s. rvd \<noteq> Some 0 \<and> (if rvd = None then 876 length x = min (unat (n_msgRegisters)) 877 (unat (msgLength (messageInfoFromWord ret__unsigned_long))) 878 else 879 length x = (unat (msgLength (messageInfoFromWord ret__unsigned_long))))" 880 and P'=UNIV 881 in ccorres_from_vcg) 882 apply (clarsimp simp: return_def) 883 apply (rule conseqPre, vcg) 884 apply (clarsimp simp: word_less_nat_alt) 885 apply (rule conjI) 886 apply clarsimp 887 apply (case_tac rvd, clarsimp simp: option_to_ptr_def option_to_0_def min_def n_msgRegisters_def) 888 apply (clarsimp simp: option_to_0_def option_to_ptr_def) 889 apply clarsimp 890 apply (case_tac rvd, 891 clarsimp simp: option_to_0_def min_def option_to_ptr_def 892 n_msgRegisters_def 893 split: if_splits) 894 apply (clarsimp simp: option_to_0_def option_to_ptr_def) 895 apply wp 896 apply (wp getMRs_length) 897 apply simp 898 apply ceqv 899 apply csymbr 900 apply (simp only: bind_assoc[symmetric]) 901 apply (rule ccorres_split_nothrow_novcg_case_sum) 902 apply (ctac add: decodeInvocation_ccorres) 903 apply ceqv 904 apply (simp add: Collect_False exception_defs 905 replyOnRestart_def liftE_def bind_assoc 906 del: Collect_const) 907 apply (rule ccorres_move_c_guard_tcb) 908 apply (rule getThreadState_ccorres_foo) 909 apply csymbr 910 apply (rule ccorres_abstract_cleanup) 911 apply (rule_tac P="ret__unsigned = thread_state_to_tsType rvg" 912 in ccorres_gen_asm2) 913 apply (simp add: thread_state_to_tsType_eq_Restart from_bool_0 914 del: Collect_const add: Collect_const[symmetric]) 915 apply (rule ccorres_Cond_rhs_Seq) 916 apply (rule ccorres_rhs_assoc)+ 917 apply (rule ccorres_Cond_rhs_Seq) 918 apply (simp add: bind_assoc) 919 apply (ctac(no_vcg) add: replyFromKernel_success_empty_ccorres) 920 apply (ctac(no_vcg) add: setThreadState_ccorres) 921 apply (rule ccorres_return_CE[folded return_returnOk], simp+)[1] 922 apply wp+ 923 apply (rule hoare_strengthen_post, rule rfk_invs') 924 apply auto[1] 925 apply simp 926 apply (ctac(no_vcg) add: setThreadState_ccorres) 927 apply (rule ccorres_return_CE[folded return_returnOk], simp+)[1] 928 apply wp 929 apply simp 930 apply (rule ccorres_return_CE[folded return_returnOk], simp+)[1] 931 apply wpc 932 apply (simp add: syscall_error_rel_def from_bool_0 exception_defs 933 Collect_False ccorres_cond_iffs Collect_True 934 del: Collect_const) 935 apply (rule ccorres_rhs_assoc)+ 936 apply (simp add: liftE_def Collect_const[symmetric] 937 del: Collect_const) 938 apply (rule ccorres_Cond_rhs_Seq) 939 apply simp 940 apply (ctac(no_vcg) add: replyFromKernel_error_ccorres) 941 apply (rule ccorres_split_throws) 942 apply (rule ccorres_return_CE[folded return_returnOk], simp+)[1] 943 apply vcg 944 apply wp 945 apply simp 946 apply (rule ccorres_split_throws) 947 apply (rule ccorres_return_CE[folded return_returnOk], simp+)[1] 948 apply vcg 949 apply (simp add: cintr_def) 950 apply (rule ccorres_split_throws) 951 apply (rule ccorres_return_C_errorE, simp+)[1] 952 apply vcg 953 apply (simp add: invocationCatch_def o_def) 954 apply (rule_tac Q="\<lambda>rv'. invs' and tcb_at' rv" 955 and E="\<lambda>ft. invs' and tcb_at' rv" 956 in hoare_post_impErr) 957 apply (wp hoare_split_bind_case_sumE 958 alternative_wp hoare_drop_imps 959 setThreadState_nonqueued_state_update 960 ct_in_state'_set setThreadState_st_tcb 961 hoare_vcg_all_lift sts_ksQ' 962 | wpc | wps)+ 963 apply auto[1] 964 apply clarsimp 965 apply (clarsimp simp: guard_is_UNIV_def Collect_const_mem) 966 apply (simp add: "StrictC'_thread_state_defs" mask_def) 967 apply (simp add: typ_heap_simps) 968 apply (case_tac ts, simp_all add: cthread_state_relation_def)[1] 969 apply (clarsimp simp: guard_is_UNIV_def Collect_const_mem) 970 apply (clarsimp simp add: intr_and_se_rel_def exception_defs 971 syscall_error_rel_def cintr_def 972 split: sum.split_asm) 973 apply (simp add: conj_comms) 974 apply (wp getMRs_sysargs_rel) 975 apply (simp add: ) 976 apply vcg 977 apply (simp add: ccorres_cond_iffs ccorres_seq_cond_raise 978 Collect_True Collect_False 979 del: Collect_const) 980 apply (rule ccorres_rhs_assoc)+ 981 apply (simp add: ccorres_cond_iffs Collect_const[symmetric] 982 del: Collect_const) 983 apply (rule ccorres_Cond_rhs_Seq) 984 apply (simp add: from_bool_0 liftE_def) 985 apply (ctac(no_vcg) add: handleFault_ccorres) 986 apply (rule ccorres_split_throws) 987 apply (rule ccorres_return_CE[folded return_returnOk], simp+)[1] 988 apply vcg 989 apply wp 990 apply (simp add: from_bool_0 liftE_def) 991 apply (rule ccorres_split_throws) 992 apply (rule ccorres_return_CE[folded return_returnOk], simp+)[1] 993 apply vcg 994 apply (simp add: ball_conj_distrib) 995 apply (wp lookupExtraCaps_excaps_in_mem 996 lec_dimished'[unfolded o_def] 997 lec_derived'[unfolded o_def]) 998 apply (clarsimp simp: guard_is_UNIV_def option_to_ptr_def 999 mi_from_H_def) 1000 apply (clarsimp simp: guard_is_UNIV_def) 1001 apply simp 1002 apply (wp lookupIPCBuffer_Some_0) 1003 apply (simp add: Collect_True liftE_def return_returnOk 1004 del: Collect_const) 1005 apply (rule ccorres_rhs_assoc)+ 1006 apply (rule_tac P=\<top> in ccorres_cross_over_guard) 1007 apply (rule ccorres_symb_exec_r) 1008 apply (rule ccorres_split_nothrow_novcg_dc) 1009 apply (rule ccorres_when[where R=\<top>]) 1010 apply (simp add: from_bool_0 Collect_const_mem) 1011 apply (ctac add: handleFault_ccorres) 1012 apply (rule ccorres_split_throws) 1013 apply (rule ccorres_return_CE, simp+)[1] 1014 apply vcg 1015 apply wp 1016 apply (simp add: guard_is_UNIV_def) 1017 apply vcg 1018 apply (rule conseqPre, vcg) 1019 apply clarsimp 1020 apply (simp, wp lcs_diminished'[unfolded o_def]) 1021 apply clarsimp 1022 apply (vcg exspec= lookupCapAndSlot_modifies) 1023 apply simp 1024 apply (wp getMessageInfo_less_4 getMessageInfo_le3 getMessageInfo_msgLength')+ 1025 apply (simp add: msgMaxLength_def, wp getMessageInfo_msgLength')[1] 1026 apply simp 1027 apply wp 1028 apply (clarsimp simp: Collect_const_mem) 1029 apply (simp add: Kernel_C.msgInfoRegister_def ARM_HYP_H.msgInfoRegister_def 1030 ARM_HYP.msgInfoRegister_def Kernel_C.R1_def 1031 Kernel_C.capRegister_def ARM_HYP_H.capRegister_def 1032 ARM_HYP.capRegister_def Kernel_C.R0_def) 1033 apply (clarsimp simp: cfault_rel_def option_to_ptr_def) 1034 apply (simp add: seL4_Fault_CapFault_lift is_cap_fault_def) 1035 apply (frule lookup_failure_rel_fault_lift, assumption) 1036 apply clarsimp 1037 apply (clarsimp simp: ct_in_state'_def pred_tcb_at') 1038 apply (auto simp: ct_in_state'_def sch_act_simple_def intro!: active_ex_cap' 1039 elim!: pred_tcb'_weakenE dest!: st_tcb_at_idle_thread')[1] 1040 done 1041 1042lemma ccorres_return_void_catchbrk: 1043 "ccorres_underlying sr G r xf ar axf P P' hs 1044 f return_void_C 1045 \<Longrightarrow> ccorres_underlying sr G r xf ar axf P P' (catchbrk_C # hs) 1046 f return_void_C" 1047 apply (simp add: return_void_C_def catchbrk_C_def) 1048 apply (rule ccorresI') 1049 apply clarsimp 1050 apply (erule exec_handlers_Seq_cases') 1051 prefer 2 1052 apply (clarsimp elim!: exec_Normal_elim_cases) 1053 apply (clarsimp elim!: exec_Normal_elim_cases) 1054 apply (erule exec_handlers.cases, simp_all) 1055 prefer 2 1056 apply (auto elim!: exec_Normal_elim_cases)[1] 1057 apply (clarsimp elim!: exec_Normal_elim_cases) 1058 apply (erule exec_Normal_elim_cases, simp_all) 1059 apply (clarsimp elim!: exec_Normal_elim_cases) 1060 apply (erule(4) ccorresE) 1061 apply (rule EHAbrupt) 1062 apply (fastforce intro: exec.intros) 1063 apply assumption 1064 apply clarsimp 1065 apply (frule exec_handlers_less) 1066 apply clarsimp 1067 apply fastforce 1068 done 1069 1070lemma real_cte_tcbCallerSlot: 1071 "tcb_at' t s \<Longrightarrow> \<not> real_cte_at' (t + 2 ^ cte_level_bits * tcbCallerSlot) s" 1072 apply (clarsimp simp: obj_at'_def projectKOs objBits_simps' 1073 cte_level_bits_def tcbCallerSlot_def) 1074 apply (drule_tac x=t and y="t + a" for a in ps_clearD, assumption) 1075 apply (rule le_neq_trans, simp_all)[1] 1076 apply (erule is_aligned_no_wrap') 1077 apply simp 1078 apply (subst field_simps[symmetric], rule is_aligned_no_overflow3, assumption, simp_all) 1079 done 1080 1081lemma handleReply_ccorres: 1082 "ccorres dc xfdc 1083 (\<lambda>s. invs' s \<and> st_tcb_at' (\<lambda>a. \<not> isReply a) (ksCurThread s) s \<and> sch_act_simple s) 1084 UNIV 1085 [] 1086 (handleReply) 1087 (Call handleReply_'proc)" 1088 apply cinit 1089 apply (rule ccorres_pre_getCurThread) 1090 1091 apply (simp only: getThreadCallerSlot_def locateSlot_conv) 1092 1093 1094 apply (rule_tac P="\<lambda>s. thread=ksCurThread s \<and> invs' s \<and> is_aligned thread tcbBlockSizeBits" 1095 and r'="\<lambda> a c. c = cte_Ptr a" 1096 and xf'="callerSlot_'" and P'=UNIV in ccorres_split_nothrow) 1097 apply (rule ccorres_from_vcg) 1098 apply (rule allI, rule conseqPre, vcg) 1099 apply (clarsimp simp: return_def word_sle_def) 1100 apply (frule is_aligned_neg_mask_eq) 1101 apply (frule tcb_at_invs') 1102 apply (simp add: mask_def tcbCallerSlot_def 1103 cte_level_bits_def size_of_def 1104 ptr_add_assertion_positive 1105 tcb_cnode_index_defs rf_sr_ksCurThread 1106 rf_sr_tcb_ctes_array_assertion2[THEN array_assertion_shrink_right]) 1107 apply ceqv 1108 1109 apply (simp del: Collect_const) 1110 apply (rule ccorres_getSlotCap_cte_at) 1111 apply (rule ccorres_move_c_guard_cte) 1112 apply ctac 1113 apply (wpc, simp_all) 1114 apply (rule ccorres_fail) 1115 apply (simp add: ccap_relation_NullCap_iff cap_tag_defs) 1116 apply (rule ccorres_split_throws) 1117 apply (rule ccorres_Catch) 1118 apply csymbr 1119 apply (rule ccorres_cond_false) 1120 apply (rule ccorres_cond_true) 1121 apply simp 1122 apply (rule ccorres_return_void_catchbrk) 1123 apply (rule ccorres_return_void_C[unfolded dc_def]) 1124 apply (vcg exspec=doReplyTransfer_modifies) 1125 apply (rule ccorres_fail)+ 1126 apply (wpc, simp_all) 1127 apply (rule ccorres_fail) 1128 apply (rule ccorres_split_throws) 1129 apply (rule ccorres_Catch) 1130 apply csymbr 1131 apply (rule ccorres_cond_true) 1132 apply (frule cap_get_tag_isCap_unfolded_H_cap(8)) 1133 apply simp 1134 apply (rule ccorres_rhs_assoc)+ 1135 apply csymbr+ 1136 apply (frule cap_get_tag_ReplyCap) 1137 apply (clarsimp simp: to_bool_def) 1138 apply (csymbr, csymbr) 1139 apply simp 1140 apply (rule ccorres_assert2) 1141 apply (fold dc_def) 1142 apply (rule ccorres_add_return2) 1143 apply (ctac (no_vcg)) 1144 apply (rule ccorres_return_void_catchbrk) 1145 apply (rule ccorres_return_void_C) 1146 apply wp 1147 apply (vcg exspec=doReplyTransfer_modifies) 1148 apply (rule ccorres_fail)+ 1149 apply simp_all 1150 apply (simp add: getSlotCap_def) 1151 apply (wp getCTE_wp')[1] 1152 apply vcg 1153 apply wp 1154 apply vcg 1155 apply clarsimp 1156 apply (intro allI conjI impI, 1157 simp_all add: cap_get_tag_isCap_unfolded_H_cap cap_tag_defs) 1158 apply (rule tcb_aligned', rule tcb_at_invs', simp) 1159 apply (auto simp: cte_wp_at_ctes_of valid_cap'_def 1160 dest!: ctes_of_valid')[1] 1161 apply (clarsimp simp: cte_wp_at_ctes_of isCap_simps) 1162 apply (simp add: real_cte_tcbCallerSlot[OF pred_tcb_at']) 1163 apply (clarsimp simp: cte_wp_at_ctes_of isCap_simps) 1164 apply clarsimp 1165 apply (frule cap_get_tag_isCap_unfolded_H_cap) 1166 apply (simp add: cap_get_tag_ReplyCap) 1167 apply clarsimp 1168 apply (frule cap_get_tag_isCap_unfolded_H_cap) 1169 apply (simp add: cap_get_tag_ReplyCap to_bool_def) 1170 done 1171 1172lemma deleteCallerCap_ccorres [corres]: 1173 "ccorres dc xfdc 1174 (\<lambda>s. invs' s \<and> tcb_at' receiver s) 1175 (UNIV \<inter> {s. receiver_' s = tcb_ptr_to_ctcb_ptr receiver}) 1176 [] 1177 (deleteCallerCap receiver) 1178 (Call deleteCallerCap_'proc)" 1179 apply (cinit lift: receiver_') 1180 apply (simp only: getThreadCallerSlot_def locateSlot_conv) 1181 apply (rule ccorres_move_array_assertion_tcb_ctes ccorres_Guard_Seq)+ 1182 apply (rule_tac P="\<lambda>_. is_aligned receiver tcbBlockSizeBits" and r'="\<lambda> a c. cte_Ptr a = c" 1183 and xf'="callerSlot_'" and P'=UNIV in ccorres_split_nothrow_novcg) 1184 apply (rule ccorres_from_vcg) 1185 apply (rule allI, rule conseqPre, vcg) 1186 apply (clarsimp simp: return_def word_sle_def) 1187 apply (frule is_aligned_neg_mask_eq) 1188 apply (simp add: mask_def tcbCallerSlot_def Kernel_C.tcbCaller_def 1189 cte_level_bits_def size_of_def) 1190 apply (drule ptr_val_tcb_ptr_mask2) 1191 apply (simp add: mask_def objBits_defs) 1192 apply ceqv 1193 apply (rule ccorres_symb_exec_l) 1194 apply (rule ccorres_symb_exec_l) 1195 apply (rule ccorres_symb_exec_r) 1196 apply (ctac add: cteDeleteOne_ccorres[where w="ucast cap_reply_cap"]) 1197 apply vcg 1198 apply (rule conseqPre, vcg, clarsimp simp: rf_sr_def 1199 gs_set_assn_Delete_cstate_relation[unfolded o_def]) 1200 apply (wp | simp)+ 1201 apply (simp add: getSlotCap_def) 1202 apply (wp getCTE_wp)+ 1203 apply clarsimp 1204 apply (simp add: guard_is_UNIV_def ghost_assertion_data_get_def 1205 ghost_assertion_data_set_def) 1206 apply (clarsimp simp: cte_wp_at_ctes_of cap_get_tag_isCap[symmetric] 1207 cap_tag_defs tcb_cnode_index_defs word_sle_def 1208 tcb_aligned') 1209 done 1210 1211 1212(* FIXME: MOVE *) 1213lemma cap_case_EndpointCap_NotificationCap: 1214 "(case cap of EndpointCap v0 v1 v2 v3 v4 \<Rightarrow> f v0 v1 v2 v3 v4 1215 | NotificationCap v0 v1 v2 v3 \<Rightarrow> g v0 v1 v2 v3 1216 | _ \<Rightarrow> h) 1217 = (if isEndpointCap cap 1218 then f (capEPPtr cap) (capEPBadge cap) (capEPCanSend cap) (capEPCanReceive cap) (capEPCanGrant cap) 1219 else if isNotificationCap cap 1220 then g (capNtfnPtr cap) (capNtfnBadge cap) (capNtfnCanSend cap) (capNtfnCanReceive cap) 1221 else h)" 1222 by (simp add: isCap_simps 1223 split: capability.split) 1224 1225 1226(* FIXME: MOVE *) 1227lemma capFaultOnFailure_if_case_sum: 1228 " (capFaultOnFailure epCPtr b (if c then f else g) >>= 1229 sum.case_sum (handleFault thread) return) = 1230 (if c then ((capFaultOnFailure epCPtr b f) 1231 >>= sum.case_sum (handleFault thread) return) 1232 else ((capFaultOnFailure epCPtr b g) 1233 >>= sum.case_sum (handleFault thread) return))" 1234 by (case_tac c, clarsimp, clarsimp) 1235 1236 1237 1238(* FIXME: MOVE to Corres_C.thy *) 1239lemma ccorres_trim_redundant_throw_break: 1240 "\<lbrakk>ccorres_underlying rf_sr \<Gamma> arrel axf arrel axf G G' (SKIP # hs) a c; 1241 \<And>s f. axf (global_exn_var_'_update f s) = axf s \<rbrakk> 1242 \<Longrightarrow> ccorres_underlying rf_sr \<Gamma> r xf arrel axf G G' (SKIP # hs) 1243 a (c;; Basic (global_exn_var_'_update (\<lambda>_. Break));; THROW)" 1244 apply - 1245 apply (rule ccorres_trim_redundant_throw') 1246 apply simp 1247 apply simp 1248 apply simp 1249 done 1250 1251lemma invs_valid_objs_strengthen: 1252 "invs' s \<longrightarrow> valid_objs' s" by fastforce 1253 1254lemma ct_not_ksQ_strengthen: 1255 "thread = ksCurThread s \<and> ksCurThread s \<notin> set (ksReadyQueues s p) \<longrightarrow> thread \<notin> set (ksReadyQueues s p)" by fastforce 1256 1257lemma option_to_ctcb_ptr_valid_ntfn: 1258 "valid_ntfn' ntfn s ==> (option_to_ctcb_ptr (ntfnBoundTCB ntfn) = NULL) = (ntfnBoundTCB ntfn = None)" 1259 apply (cases "ntfnBoundTCB ntfn", simp_all add: option_to_ctcb_ptr_def) 1260 apply (clarsimp simp: valid_ntfn'_def tcb_at_not_NULL) 1261 done 1262 1263 1264lemma deleteCallerCap_valid_ntfn'[wp]: 1265 "\<lbrace>\<lambda>s. valid_ntfn' x s\<rbrace> deleteCallerCap c \<lbrace>\<lambda>rv s. valid_ntfn' x s\<rbrace>" 1266 apply (wp hoare_vcg_ex_lift hoare_vcg_all_lift hoare_vcg_ball_lift hoare_vcg_imp_lift 1267 | simp add: valid_ntfn'_def split: ntfn.splits)+ 1268 apply auto 1269 done 1270 1271lemma hoare_vcg_imp_liftE: 1272 "\<lbrakk>\<lbrace>P'\<rbrace> f \<lbrace>\<lambda>rv s. \<not> P rv s\<rbrace>, \<lbrace>E\<rbrace>; \<lbrace>Q'\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P' s \<or> Q' s\<rbrace> f \<lbrace>\<lambda>rv s. P rv s \<longrightarrow> Q rv s\<rbrace>, \<lbrace>E\<rbrace>" 1273 apply (simp add: validE_def valid_def split_def split: sum.splits) 1274 done 1275 1276 1277lemma not_obj_at'_ntfn: 1278 "(\<not>obj_at' (P::Structures_H.notification \<Rightarrow> bool) t s) = (\<not> typ_at' NotificationT t s \<or> obj_at' (Not \<circ> P) t s)" 1279 apply (simp add: obj_at'_real_def projectKOs typ_at'_def ko_wp_at'_def objBits_simps) 1280 apply (rule iffI) 1281 apply (clarsimp) 1282 apply (case_tac ko) 1283 apply (clarsimp)+ 1284 done 1285 1286lemma handleRecv_ccorres: 1287 notes rf_sr_upd_safe[simp del] 1288 shows 1289 "ccorres dc xfdc 1290 (\<lambda>s. invs' s \<and> st_tcb_at' simple' (ksCurThread s) s 1291 \<and> sch_act_sane s \<and> (\<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))) 1292 {s. isBlocking_' s = from_bool isBlocking} 1293 [] 1294 (handleRecv isBlocking) 1295 (Call handleRecv_'proc)" 1296 apply (cinit lift: isBlocking_') 1297 apply (rule ccorres_pre_getCurThread) 1298 apply (ctac) 1299 apply (simp add: catch_def) 1300 apply (simp add: capFault_bindE) 1301 apply (simp add: bindE_bind_linearise) 1302 apply (rule_tac xf'=lu_ret___struct_lookupCap_ret_C_' 1303 in ccorres_split_nothrow_case_sum) 1304 apply (rule capFaultOnFailure_ccorres) 1305 apply (ctac add: lookupCap_ccorres) 1306 apply ceqv 1307 apply clarsimp 1308 apply (rule ccorres_Catch) 1309 apply csymbr 1310 apply (simp add: cap_get_tag_isCap del: Collect_const) 1311 apply (clarsimp simp: cap_case_EndpointCap_NotificationCap 1312 capFaultOnFailure_if_case_sum) 1313 apply (rule ccorres_cond_both' [where Q=\<top> and Q'=\<top>]) 1314 apply clarsimp 1315 apply (rule ccorres_rhs_assoc)+ 1316 apply csymbr 1317 apply (simp add: case_bool_If capFaultOnFailure_if_case_sum) 1318 apply (rule ccorres_if_cond_throws_break2 [where Q=\<top> and Q'=\<top>]) 1319 apply clarsimp 1320 apply (simp add: cap_get_tag_isCap[symmetric] cap_get_tag_EndpointCap 1321 del: Collect_const) 1322 apply (simp add: to_bool_def) 1323 apply (rule ccorres_rhs_assoc)+ 1324 apply (simp add: capFaultOnFailure_def rethrowFailure_def 1325 handleE'_def throwError_def) 1326 apply (rule ccorres_cross_over_guard[where P=\<top>]) 1327 apply (rule ccorres_symb_exec_r) 1328 apply (rule ccorres_cross_over_guard[where P=\<top>]) 1329 apply (rule ccorres_symb_exec_r) 1330 apply (rule ccorres_add_return2) 1331 apply (rule ccorres_split_nothrow_call[where xf'=xfdc and d'="\<lambda>_. break_C" 1332 and Q="\<lambda>_ _. True" and Q'="\<lambda>_ _. UNIV"]) 1333 apply (ctac add: handleFault_ccorres[unfolded dc_def]) 1334 apply simp+ 1335 apply ceqv 1336 apply (rule ccorres_break_return) 1337 apply simp+ 1338 apply wp 1339 apply (vcg exspec=handleFault_modifies) 1340 1341 apply vcg 1342 apply (rule conseqPre, vcg) 1343 apply (clarsimp simp: rf_sr_upd_safe) 1344 1345 apply vcg 1346 apply (rule conseqPre, vcg) 1347 apply (clarsimp simp: rf_sr_upd_safe) 1348 1349 apply (simp add: liftE_bind) 1350 apply (ctac) 1351 apply (rule_tac P="\<lambda>s. ksCurThread s = rv" in ccorres_cross_over_guard) 1352 apply (ctac add: receiveIPC_ccorres[unfolded dc_def]) 1353 1354 apply (wp deleteCallerCap_ksQ_ct' hoare_vcg_all_lift) 1355 apply (rule conseqPost[where Q'=UNIV and A'="{}"], vcg exspec=deleteCallerCap_modifies) 1356 apply (clarsimp dest!: rf_sr_ksCurThread) 1357 apply simp 1358 apply clarsimp 1359 apply (vcg exspec=handleFault_modifies) 1360 1361 apply (clarsimp simp: case_bool_If capFaultOnFailure_if_case_sum capFault_bindE) 1362 apply (simp add: liftE_bindE bind_bindE_assoc bind_assoc) 1363 apply (rule ccorres_cond_both' [where Q=\<top> and Q'=\<top>]) 1364 apply clarsimp 1365 1366 apply (rule ccorres_rhs_assoc)+ 1367 apply csymbr 1368 apply csymbr 1369 apply csymbr 1370 apply csymbr 1371 apply (rename_tac thread epCPtr rv rva ntfnptr) 1372 apply (rule_tac P="valid_cap' rv" in ccorres_cross_over_guard) 1373 apply (simp only: capFault_injection injection_handler_If injection_liftE 1374 injection_handler_throwError if_to_top_of_bind) 1375 apply csymbr 1376 apply (rule ccorres_abstract_cleanup) 1377 apply csymbr 1378 apply csymbr 1379 apply (rule ccorres_if_lhs) 1380 1381 apply (rule ccorres_pre_getNotification) 1382 apply (rename_tac ntfn) 1383 apply (rule_tac Q="valid_ntfn' ntfn and (\<lambda>s. thread = ksCurThread s)" 1384 and Q'="\<lambda>s. ret__unsigneda = ptr_val (option_to_ctcb_ptr (ntfnBoundTCB ntfn))" 1385 in ccorres_if_cond_throws_break2) 1386 apply (clarsimp simp: cap_get_tag_isCap[symmetric] cap_get_tag_NotificationCap 1387 option_to_ctcb_ptr_valid_ntfn rf_sr_ksCurThread) 1388 apply (auto simp: option_to_ctcb_ptr_def)[1] 1389 apply (rule ccorres_rhs_assoc)+ 1390 1391 apply (simp add: capFaultOnFailure_def rethrowFailure_def 1392 handleE'_def throwError_def) 1393 apply (rule ccorres_cross_over_guard[where P=\<top>]) 1394 apply (rule ccorres_symb_exec_r) 1395 apply (rule ccorres_cross_over_guard[where P=\<top>]) 1396 apply (rule ccorres_symb_exec_r) 1397 apply (rule ccorres_add_return2) 1398 apply (rule ccorres_split_nothrow_call[where xf'=xfdc and d'="\<lambda>_. break_C" 1399 and Q="\<lambda>_ _. True" and Q'="\<lambda>_ _. UNIV"]) 1400 apply (ctac add: handleFault_ccorres[unfolded dc_def]) 1401 apply simp+ 1402 apply ceqv 1403 apply (rule ccorres_break_return) 1404 apply simp+ 1405 apply wp 1406 apply (vcg exspec=handleFault_modifies) 1407 1408 apply vcg 1409 apply (rule conseqPre, vcg) 1410 apply (clarsimp simp: rf_sr_upd_safe) 1411 1412 apply vcg 1413 apply (rule conseqPre, vcg) 1414 apply (clarsimp simp: rf_sr_upd_safe) 1415 1416 apply (simp add: liftE_bind) 1417 apply (ctac add: receiveSignal_ccorres[unfolded dc_def]) 1418 apply clarsimp 1419 apply (vcg exspec=handleFault_modifies) 1420 apply (rule ccorres_cond_true_seq) 1421 apply (rule ccorres_split_throws) 1422 apply (rule ccorres_rhs_assoc)+ 1423 apply (simp add: capFaultOnFailure_def rethrowFailure_def 1424 handleE'_def throwError_def) 1425 apply (rule ccorres_cross_over_guard[where P=\<top>]) 1426 apply (rule ccorres_symb_exec_r) 1427 apply (rule ccorres_cross_over_guard[where P=\<top>]) 1428 apply (rule ccorres_symb_exec_r) 1429 apply (rule ccorres_add_return2) 1430 apply (ctac add: handleFault_ccorres[unfolded dc_def]) 1431 apply (rule ccorres_break_return[where P=\<top> and P'=UNIV]) 1432 apply simp+ 1433 apply wp 1434 apply (vcg exspec=handleFault_modifies) 1435 1436 apply vcg 1437 apply (rule conseqPre, vcg) 1438 apply (clarsimp simp: rf_sr_upd_safe) 1439 apply vcg 1440 apply (rule conseqPre, vcg) 1441 apply (clarsimp simp: rf_sr_upd_safe) 1442 apply (vcg exspec=handleFault_modifies) 1443 apply (simp add: capFaultOnFailure_def rethrowFailure_def 1444 handleE'_def throwError_def) 1445 1446 apply (rule ccorres_rhs_assoc)+ 1447 apply (rule ccorres_cross_over_guard[where P=\<top>]) 1448 apply (rule ccorres_symb_exec_r) 1449 apply (rule ccorres_cross_over_guard[where P=\<top>]) 1450 apply (rule ccorres_symb_exec_r) 1451 apply (ctac add: handleFault_ccorres[unfolded dc_def]) 1452 apply vcg 1453 apply (rule conseqPre, vcg) 1454 apply (clarsimp simp: rf_sr_upd_safe) 1455 apply vcg 1456 apply (rule conseqPre, vcg) 1457 apply (clarsimp simp: rf_sr_upd_safe) 1458 1459 apply clarsimp 1460 apply (rule ccorres_add_return2) 1461 apply (rule ccorres_rhs_assoc)+ 1462 apply (rule ccorres_cross_over_guard[where P=\<top>]) 1463 apply (rule ccorres_symb_exec_r) 1464 apply (ctac add: handleFault_ccorres[unfolded dc_def]) 1465 apply (rule ccorres_split_throws) 1466 apply (rule ccorres_return_void_C [unfolded dc_def]) 1467 apply vcg 1468 apply wp 1469 apply (vcg exspec=handleFault_modifies) 1470 apply vcg 1471 apply (rule conseqPre, vcg) 1472 apply (clarsimp simp: rf_sr_upd_safe) 1473 apply (wp) 1474 apply clarsimp 1475 apply (rename_tac thread epCPtr) 1476 apply (rule_tac Q'="(\<lambda>rv s. invs' s \<and> st_tcb_at' simple' thread s 1477 \<and> sch_act_sane s \<and> (\<forall>p. thread \<notin> set (ksReadyQueues s p)) \<and> thread = ksCurThread s 1478 \<and> valid_cap' rv s)" in hoare_post_imp_R[rotated]) 1479 apply (clarsimp simp: sch_act_sane_def) 1480 apply (auto dest!: obj_at_valid_objs'[OF _ invs_valid_objs'] 1481 simp: projectKOs valid_obj'_def, 1482 auto simp: pred_tcb_at'_def obj_at'_def objBits_simps projectKOs ct_in_state'_def)[1] 1483 apply wp 1484 apply clarsimp 1485 apply (vcg exspec=isBlocked_modifies exspec=lookupCap_modifies) 1486 1487 apply wp 1488 apply clarsimp 1489 apply vcg 1490 1491 apply (clarsimp simp add: sch_act_sane_def) 1492 apply (simp add: cap_get_tag_isCap[symmetric] del: rf_sr_upd_safe) 1493 apply (simp add: Kernel_C.capRegister_def ARM_HYP_H.capRegister_def ct_in_state'_def 1494 ARM_HYP.capRegister_def Kernel_C.R0_def 1495 tcb_at_invs') 1496 apply (frule invs_valid_objs') 1497 apply (frule tcb_aligned'[OF tcb_at_invs']) 1498 apply clarsimp 1499 apply (intro conjI impI allI) 1500 apply (clarsimp simp: cfault_rel_def seL4_Fault_CapFault_lift 1501 lookup_fault_missing_capability_lift is_cap_fault_def)+ 1502 apply (clarsimp simp: cap_get_tag_NotificationCap) 1503 apply (rule cmap_relationE1[OF cmap_relation_ntfn], assumption, erule ko_at_projectKO_opt) 1504 apply (clarsimp simp: cnotification_relation_def Let_def) 1505 apply (clarsimp simp: cfault_rel_def seL4_Fault_CapFault_lift 1506 lookup_fault_missing_capability_lift is_cap_fault_def)+ 1507 apply (clarsimp simp: cap_get_tag_NotificationCap) 1508 apply (simp add: ccap_relation_def to_bool_def) 1509 apply (clarsimp simp: cap_get_tag_NotificationCap valid_cap'_def) 1510 apply (drule obj_at_ko_at', clarsimp) 1511 apply (rule cmap_relationE1[OF cmap_relation_ntfn], assumption, erule ko_at_projectKO_opt) 1512 apply (clarsimp simp: typ_heap_simps) 1513 apply (clarsimp simp: cfault_rel_def seL4_Fault_CapFault_lift 1514 lookup_fault_missing_capability_lift is_cap_fault_def)+ 1515 apply (case_tac w, clarsimp+) 1516 done 1517 1518lemma handleYield_ccorres: 1519 "ccorres dc xfdc 1520 (invs' and ct_active') 1521 UNIV 1522 [] 1523 (handleYield) 1524 (Call handleYield_'proc)" 1525 apply cinit 1526 apply (rule ccorres_pre_getCurThread) 1527 apply (ctac add: tcbSchedDequeue_ccorres) 1528 apply (ctac add: tcbSchedAppend_ccorres) 1529 apply (ctac add: rescheduleRequired_ccorres) 1530 apply (wp weak_sch_act_wf_lift_linear tcbSchedAppend_valid_objs') 1531 apply (vcg exspec= tcbSchedAppend_modifies) 1532 apply (wp weak_sch_act_wf_lift_linear tcbSchedDequeue_valid_queues) 1533 apply (vcg exspec= tcbSchedDequeue_modifies) 1534 apply (clarsimp simp: tcb_at_invs' invs_valid_objs' 1535 valid_objs'_maxPriority valid_objs'_maxDomain) 1536 apply (auto simp: obj_at'_def st_tcb_at'_def ct_in_state'_def valid_objs'_maxDomain) 1537 done 1538 1539 1540lemma getIRQState_sp: 1541 "\<lbrace>P\<rbrace> getIRQState irq \<lbrace>\<lambda>rv s. rv = intStateIRQTable (ksInterruptState s) irq \<and> P s\<rbrace>" 1542 apply (simp add: getIRQState_def getInterruptState_def) 1543 apply wp 1544 apply simp 1545 done 1546 1547lemma ccorres_pre_getIRQState: 1548 assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c" 1549 shows "ccorres r xf 1550 (\<lambda>s. irq \<le> ucast Kernel_C.maxIRQ \<and> P (intStateIRQTable (ksInterruptState s) irq) s) 1551 {s. \<forall>rv. index (intStateIRQTable_' (globals s)) (unat irq) = irqstate_to_C rv \<longrightarrow> s \<in> P' rv } 1552 hs (getIRQState irq >>= (\<lambda>rv. f rv)) c" 1553 apply (rule ccorres_guard_imp) 1554 apply (rule ccorres_symb_exec_l) 1555 defer 1556 apply (simp add: getIRQState_def getInterruptState_def) 1557 apply wp 1558 apply simp 1559 apply (rule getIRQState_sp) 1560 apply (simp add: getIRQState_def getInterruptState_def) 1561 apply assumption 1562 prefer 2 1563 apply (rule ccorres_guard_imp) 1564 apply (rule cc) 1565 apply simp 1566 apply assumption 1567 apply clarsimp 1568 apply (erule allE) 1569 apply (erule impE) 1570 prefer 2 1571 apply assumption 1572 apply (clarsimp simp: rf_sr_def cstate_relation_def 1573 Let_def cinterrupt_relation_def) 1574 done 1575 1576(* FIXME: move *) 1577lemma ccorres_ntfn_cases: 1578 assumes P: "\<And>p b send d. cap = NotificationCap p b send d \<Longrightarrow> ccorres r xf (P p b send d) (P' p b send d) hs (a cap) (c cap)" 1579 assumes Q: "\<not>isNotificationCap cap \<Longrightarrow> ccorres r xf (Q cap) (Q' cap) hs (a cap) (c cap)" 1580 shows 1581 "ccorres r xf (\<lambda>s. (\<forall>p b send d. cap = NotificationCap p b send d \<longrightarrow> P p b send d s) \<and> 1582 (\<not>isNotificationCap cap \<longrightarrow> Q cap s)) 1583 ({s. \<forall>p b send d. cap = NotificationCap p b send d \<longrightarrow> s \<in> P' p b send d} \<inter> 1584 {s. \<not>isNotificationCap cap \<longrightarrow> s \<in> Q' cap}) 1585 hs (a cap) (c cap)" 1586 apply (cases "isNotificationCap cap") 1587 apply (simp add: isCap_simps) 1588 apply (elim exE) 1589 apply (rule ccorres_guard_imp) 1590 apply (erule P) 1591 apply simp 1592 apply simp 1593 apply (rule ccorres_guard_imp) 1594 apply (erule Q) 1595 apply clarsimp 1596 apply clarsimp 1597 done 1598 1599(* FIXME: generalise the one in Interrupt_C *) 1600lemma getIRQSlot_ccorres2: 1601 "ccorres ((=) \<circ> Ptr) slot_' 1602 \<top> UNIV hs 1603 (getIRQSlot irq) (\<acute>slot :== CTypesDefs.ptr_add \<acute>intStateIRQNode (uint (ucast irq :: word32)))" 1604 apply (rule ccorres_from_vcg[where P=\<top> and P'=UNIV]) 1605 apply (rule allI, rule conseqPre, vcg) 1606 apply (clarsimp simp: getIRQSlot_def liftM_def getInterruptState_def 1607 locateSlot_conv) 1608 apply (simp add: simpler_gets_def bind_def return_def) 1609 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def 1610 cinterrupt_relation_def size_of_def 1611 cte_level_bits_def mult.commute mult.left_commute ucast_nat_def) 1612 done 1613 1614lemma getIRQSlot_ccorres3: 1615 "(\<And>rv. ccorresG rf_sr \<Gamma> r xf (P rv) (P' rv) hs (f rv) c) \<Longrightarrow> 1616 ccorresG rf_sr \<Gamma> r xf 1617 (\<lambda>s. P (intStateIRQNode (ksInterruptState s) + 2 ^ cte_level_bits * of_nat (unat irq)) s) 1618 {s. s \<in> P' (ptr_val (CTypesDefs.ptr_add (intStateIRQNode_' (globals s)) (uint (ucast irq :: word32))))} hs 1619 (getIRQSlot irq >>= f) c" 1620 apply (simp add: getIRQSlot_def locateSlot_conv liftM_def getInterruptState_def) 1621 apply (rule ccorres_symb_exec_l'[OF _ _ gets_sp]) 1622 apply (rule ccorres_guard_imp2, assumption) 1623 apply (clarsimp simp: getIRQSlot_ccorres_stuff 1624 objBits_simps cte_level_bits_def 1625 ucast_nat_def uint_ucast uint_up_ucast is_up) 1626 apply wp+ 1627 done 1628 1629 1630lemma scast_maxIRQ_is_less: 1631 fixes uc :: "irq \<Rightarrow> 16 word" 1632 and uc' :: "16 word\<Rightarrow> 32 sword" 1633 and b :: irq 1634 shows 1635 "(Kernel_C.maxIRQ) <s (ucast \<circ> (ucast :: irq \<Rightarrow> 16 word)) b \<Longrightarrow> scast Kernel_C.maxIRQ < b" 1636 apply (simp add: Kernel_C.maxIRQ_def word_sless_def word_sle_def, uint_arith, clarify,simp) 1637 apply (subgoal_tac "sint (ucast Kernel_C.maxIRQ :: 32 sword) \<le> uint b"; (simp only: Kernel_C.maxIRQ_def)?) 1638 apply (subgoal_tac "sint (ucast Kernel_C.maxIRQ :: 32 sword) \<noteq> uint b"; (simp only: Kernel_C.maxIRQ_def)?) 1639 apply (simp ) 1640 apply (subst uint_is_up_compose[where uc="(ucast :: irq \<Rightarrow> 16 word)" and uc' = "(ucast :: 16 word \<Rightarrow> 32 sword)",symmetric]; 1641 (simp add: is_up_def target_size source_size )?) 1642 apply fastforce 1643 apply (subst sint_ucast_uint_pred[where uc="(ucast :: irq \<Rightarrow> 16 word)" and uc' = "(ucast :: 16 word \<Rightarrow> 32 sword)"]; 1644 (simp add: is_up_def target_size source_size )?) 1645 apply fastforce 1646done 1647 1648lemma validIRQcastingLess: 1649 "Kernel_C.maxIRQ <s (ucast((ucast (b :: irq))::word16)) \<Longrightarrow> ARM_HYP.maxIRQ < b" 1650 by (simp add: Platform_maxIRQ scast_maxIRQ_is_less is_up_def target_size source_size) 1651 1652lemma scast_maxIRQ_is_not_less: 1653 "(\<not> (Kernel_C.maxIRQ) <s (ucast \<circ> (ucast :: irq \<Rightarrow> 16 word)) b) \<Longrightarrow> \<not> (scast Kernel_C.maxIRQ < b)" 1654 apply (subgoal_tac "sint (ucast Kernel_C.maxIRQ :: 32 sword) \<ge> sint (ucast (ucast b))"; 1655 simp only: Kernel_C.maxIRQ_def word_sless_def word_sle_def) 1656 apply (uint_arith) 1657 apply (subst (asm) sint_ucast_uint[where b=b and 'c=32 and 'b=16 and uc=ucast and uc'=ucast and uuc="ucast \<circ> ucast", simplified]; 1658 simp add: is_up_def target_size source_size) 1659 apply (cases "sint maxIRQ \<le> sint (UCAST(10 \<rightarrow> 32 signed) b)"; simp add: maxIRQ_def sint_uint) 1660 done 1661 1662(* FIXME ARMHYP: move *) 1663lemma ctzl_spec: 1664 "\<forall>s. \<Gamma> \<turnstile> {\<sigma>. s = \<sigma> \<and> x_' s \<noteq> 0} Call ctzl_'proc 1665 \<lbrace>\<acute>ret__long = of_nat (word_ctz (x_' s)) \<rbrace>" 1666 apply (rule allI, rule conseqPre, vcg) 1667 apply clarsimp 1668 apply (rule_tac x="ret__long_'_update f x" for f in exI) 1669 apply (simp add: mex_def meq_def) 1670 done 1671 1672lemma get_gic_vcpu_ctrl_misr_invs'[wp]: 1673 "valid invs' (doMachineOp get_gic_vcpu_ctrl_misr) (\<lambda>_. invs')" 1674 by (simp add: get_gic_vcpu_ctrl_misr_def doMachineOp_def split_def select_f_returns | wp)+ 1675 1676lemma get_gic_vcpu_ctrl_eisr1_invs'[wp]: 1677 "valid invs' (doMachineOp get_gic_vcpu_ctrl_eisr1) (\<lambda>_. invs')" 1678 by (simp add: get_gic_vcpu_ctrl_eisr1_def doMachineOp_def split_def select_f_returns | wp)+ 1679 1680lemma get_gic_vcpu_ctrl_eisr0_invs'[wp]: 1681 "valid invs' (doMachineOp get_gic_vcpu_ctrl_eisr0) (\<lambda>_. invs')" 1682 by (simp add: get_gic_vcpu_ctrl_eisr0_def doMachineOp_def split_def select_f_returns | wp)+ 1683 1684crunch obj_at'_s[wp]: armv_contextSwitch "\<lambda>s. obj_at' P (ksCurThread s) s" 1685 1686lemma dmo_machine_valid_lift: 1687 "(\<And>s f. P s = P (ksMachineState_update f s)) \<Longrightarrow> \<lbrace>P\<rbrace> doMachineOp f' \<lbrace>\<lambda>rv. P\<rbrace>" 1688 apply (wpsimp simp: split_def doMachineOp_def machine_op_lift_def machine_rest_lift_def in_monad) 1689 done 1690 1691lemma tcb_runnable_imp_simple: 1692 "obj_at' (\<lambda>s. runnable' (tcbState s)) t s \<Longrightarrow> obj_at' (\<lambda>s. simple' (tcbState s)) t s" 1693 apply (clarsimp simp: obj_at'_def) 1694 apply (case_tac "tcbState obj" ; clarsimp) 1695 done 1696 1697lemma ccorres_return_void_C_Seq: 1698 "ccorres_underlying sr \<Gamma> r rvxf arrel xf P P' hs X (return_void_C) \<Longrightarrow> 1699 ccorres_underlying sr \<Gamma> r rvxf arrel xf P P' hs X (return_void_C ;; Z)" 1700 apply (clarsimp simp: return_void_C_def) 1701 apply (erule ccorres_semantic_equiv0[rotated]) 1702 apply (rule semantic_equivI) 1703 apply (clarsimp simp: exec_assoc[symmetric]) 1704 apply (rule exec_Seq_cong, simp) 1705 apply (rule iffI) 1706 apply (auto elim!:exec_Normal_elim_cases intro: exec.Throw exec.Seq)[1] 1707 apply (auto elim!:exec_Normal_elim_cases intro: exec.Throw) 1708 done 1709 1710 1711lemma virq_to_H_arrayp[simp]: 1712 "virq_to_H (virq_C (ARRAY _. v)) = v" 1713 by (simp add: virq_to_H_def) 1714 1715lemma virq_virq_active_set_virqEOIIRQEN_spec': 1716 "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. virq_get_tag \<acute>virq = scast virq_virq_active\<rbrace> 1717 Call virq_virq_active_set_virqEOIIRQEN_'proc 1718 \<lbrace> \<acute>ret__struct_virq_C = virq_C (ARRAY _. virqSetEOIIRQEN (virq_to_H \<^bsup>s\<^esup>virq) \<^bsup>s\<^esup>v32) \<rbrace>" 1719 apply (hoare_rule HoarePartial.ProcNoRec1) (* force vcg to unfold non-recursive procedure *) 1720 apply vcg 1721 apply (clarsimp simp: virq_to_H_def virqSetEOIIRQEN_def o_def) 1722 apply (case_tac virq) 1723 apply clarsimp 1724 apply (rule array_ext) 1725 apply (clarsimp simp: virq_get_tag_def virq_tag_defs mask_def split: if_split) 1726 done 1727 1728lemma virq_virq_invalid_set_virqEOIIRQEN_spec': 1729 "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. virq_get_tag \<acute>virq = scast virq_virq_invalid\<rbrace> 1730 Call virq_virq_invalid_set_virqEOIIRQEN_'proc 1731 \<lbrace> \<acute>ret__struct_virq_C = virq_C (ARRAY _. virqSetEOIIRQEN (virq_to_H \<^bsup>s\<^esup>virq) \<^bsup>s\<^esup>v32) \<rbrace>" 1732 apply (hoare_rule HoarePartial.ProcNoRec1) (* force vcg to unfold non-recursive procedure *) 1733 apply vcg 1734 apply (clarsimp simp: virq_to_H_def virqSetEOIIRQEN_def o_def) 1735 apply (case_tac virq) 1736 apply clarsimp 1737 apply (rule array_ext) 1738 apply (clarsimp simp: virq_get_tag_def virq_tag_defs mask_def split: if_split) 1739 done 1740 1741lemma virq_virq_pending_set_virqEOIIRQEN_spec': 1742 "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. virq_get_tag \<acute>virq = scast virq_virq_pending\<rbrace> 1743 Call virq_virq_pending_set_virqEOIIRQEN_'proc 1744 \<lbrace> \<acute>ret__struct_virq_C = virq_C (ARRAY _. virqSetEOIIRQEN (virq_to_H \<^bsup>s\<^esup>virq) \<^bsup>s\<^esup>v32) \<rbrace>" 1745 apply (hoare_rule HoarePartial.ProcNoRec1) (* force vcg to unfold non-recursive procedure *) 1746 apply vcg 1747 apply (clarsimp simp: virq_to_H_def virqSetEOIIRQEN_def o_def) 1748 apply (case_tac virq) 1749 apply clarsimp 1750 apply (rule array_ext) 1751 apply (clarsimp simp: virq_get_tag_def virq_tag_defs mask_def split: if_split) 1752 done 1753 1754 1755lemma gic_vcpu_num_list_regs_cross_over: 1756 "\<lbrakk> of_nat (armKSGICVCPUNumListRegs (ksArchState s)) = gic_vcpu_num_list_regs_' t; 1757 valid_arch_state' s \<rbrakk> 1758 \<Longrightarrow> gic_vcpu_num_list_regs_' t \<le> 0x3F" 1759 apply (drule sym, simp) 1760 apply (clarsimp simp: valid_arch_state'_def max_armKSGICVCPUNumListRegs_def) 1761 apply (clarsimp simp: word_le_nat_alt unat_of_nat) 1762 done 1763 1764lemma virqSetEOIIRQEN_id: 1765 "\<lbrakk> virq_get_tag (virq_C (ARRAY _. idx)) \<noteq> scast virq_virq_active; 1766 virq_get_tag (virq_C (ARRAY _. idx)) \<noteq> scast virq_virq_pending; 1767 virq_get_tag (virq_C (ARRAY _. idx)) \<noteq> scast virq_virq_invalid \<rbrakk> 1768 \<Longrightarrow> virqSetEOIIRQEN idx 0 = idx" 1769 apply (clarsimp simp: virqSetEOIIRQEN_def virq_get_tag_def virq_tag_defs mask_def split: if_split) 1770 apply (rule_tac x="idx >> 28" in two_bits_cases; simp) 1771 done 1772 1773lemma vgicUpdateLR_ccorres_armHSCurVCPU: 1774 "\<lbrakk> v' = v ; n' = n ; n \<le> 63 \<rbrakk> \<Longrightarrow> 1775 ccorres dc xfdc 1776 (\<lambda>s. (armHSCurVCPU (ksArchState s) \<noteq> None) \<and> 1777 vcpu_at' (fst (the (armHSCurVCPU (ksArchState s)))) s) 1778 (UNIV \<inter> \<lbrace>\<acute>armHSCurVCPU = vcpu_Ptr vcpuptr\<rbrace>) hs 1779 (vgicUpdateLR vcpuptr n v) 1780 (Guard C_Guard {s. s \<Turnstile>\<^sub>c armHSCurVCPU_' (globals s)} 1781 (Basic_heap_update 1782 (\<lambda>s. vgic_lr_C_Ptr &(vgic_C_Ptr &((armHSCurVCPU_' (globals s))\<rightarrow>[''vgic_C''])\<rightarrow>[''lr_C''])) 1783 (\<lambda>s. Arrays.update 1784 (h_val (hrs_mem (t_hrs_' (globals s))) 1785 (vgic_lr_C_Ptr &(vgic_C_Ptr &((armHSCurVCPU_' (globals s))\<rightarrow>[''vgic_C''])\<rightarrow>[''lr_C'']))) 1786 n' (virq_C (ARRAY _. v')))))" 1787 supply from_bool_eq_if[simp] from_bool_eq_if'[simp] from_bool_0[simp] 1788 apply (rule ccorres_guard_imp) 1789 apply (rule_tac P="\<lambda>s. armHSCurVCPU (ksArchState s) \<noteq> None 1790 \<and> vcpu_at' (fst (the (armHSCurVCPU (ksArchState s)))) s" 1791 and P'=\<top> in ccorres_move_Guard) 1792 apply clarsimp 1793 apply (frule rf_sr_ksArchState_armHSCurVCPU) 1794 apply (clarsimp simp: cur_vcpu_relation_def split: option.splits) 1795 apply (fastforce simp: move_c_guard_vcpu[rule_format, simplified]) 1796 apply (simp add: vgicUpdate_def vcpuUpdate_def vgicUpdateLR_def) 1797 apply (rule ccorres_pre_getObject_vcpu, rename_tac vcpu) 1798 apply (rule_tac P="ko_at' vcpu vcpuptr" 1799 and P'="{s. armHSCurVCPU_' (globals s) = vcpu_Ptr vcpuptr }" in setObject_ccorres_helper 1800 , rule conseqPre, vcg) 1801 apply clarsimp 1802 apply (rule cmap_relationE1[OF cmap_relation_vcpu] 1803 ; (clarsimp simp: objBits_simps archObjSize_def machine_bits_defs)?) 1804 apply (assumption, erule ko_at_projectKO_opt) 1805 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def carch_state_relation_def 1806 cmachine_state_relation_def update_vcpu_map_to_vcpu 1807 typ_heap_simps' cpspace_relation_def update_vcpu_map_tos) 1808 apply (erule (1) cmap_relation_updI 1809 ; clarsimp simp: cvcpu_relation_regs_def cvgic_relation_def ; (rule refl)?) 1810 apply (fastforce simp: virq_to_H_def split: if_split) 1811 apply (simp add: objBits_simps archObjSize_def machine_bits_defs)+ 1812 done 1813 1814(* folded calculation of eisr used in vgicMaintenance *) 1815definition 1816 eisr_calc :: "machine_word \<Rightarrow> machine_word \<Rightarrow> nat" 1817where 1818 "eisr_calc eisr0 eisr1 \<equiv> if eisr0 \<noteq> 0 then word_ctz eisr0 else word_ctz eisr1 + 32" 1819 1820lemma ccorres_vgicMaintenance: 1821 notes dc_simp[simp del] Collect_const[simp del] 1822 notes scast_specific_plus32[simp] scast_specific_plus32_signed[simp] 1823 notes virq_virq_active_set_virqEOIIRQEN_spec = virq_virq_active_set_virqEOIIRQEN_spec' 1824 notes virq_virq_invalid_set_virqEOIIRQEN_spec = virq_virq_invalid_set_virqEOIIRQEN_spec' 1825 notes virq_virq_pending_set_virqEOIIRQEN_spec = virq_virq_pending_set_virqEOIIRQEN_spec' 1826 shows 1827 "ccorres dc xfdc 1828 (\<lambda>s. invs' s \<and> sch_act_not (ksCurThread s) s 1829 \<and> (\<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))) 1830 UNIV hs 1831 vgicMaintenance (Call VGICMaintenance_'proc)" 1832proof - 1833 1834 have unat_of_nat_ctz_plus_32s[simp]: 1835 "unat (of_nat (word_ctz w) + (0x20 :: int_sword)) = word_ctz w + 32" for w :: machine_word 1836 apply (subst unat_add_lem' ; clarsimp simp: unat_of_nat_ctz_smw) 1837 using word_ctz_le[where w=w, simplified] by (auto simp: unat_of_nat_eq) 1838 1839 have unat_of_nat_ctz_plus_32[simp]: 1840 "unat (of_nat (word_ctz w) + (0x20 :: machine_word)) = word_ctz w + 32" for w :: machine_word 1841 apply (subst unat_add_lem' ; clarsimp simp: unat_of_nat_ctz_mw) 1842 using word_ctz_le[where w=w, simplified] by (auto simp: unat_of_nat_eq) 1843 1844 have eisr_calc_signed_limits: 1845 "eisr0 = 0 \<longrightarrow> eisr1 \<noteq> 0 1846 \<Longrightarrow> (0 :: int_sword) <=s of_nat (eisr_calc eisr0 eisr1) 1847 \<and> of_nat (eisr_calc eisr0 eisr1) <s (0x40 :: int_sword)" 1848 for eisr0 :: machine_word and eisr1 1849 supply int_unat[simp del] 1850 using word_ctz_le[where w=eisr0] word_ctz_less[where w=eisr1] 1851 apply (clarsimp simp: eisr_calc_def sint_word_ariths sbintrunc_If word_sint_msb_eq 1852 word_sless_alt word_sle_def word_size uint_nat 1853 split: if_splits) 1854 apply (cut_tac not_msb_from_less[where v="of_nat (word_ctz eisr0) :: int_sword"]) 1855 apply (clarsimp simp: word_less_alt unat_of_nat_ctz_mw unat_of_nat_ctz_smw 1856 uint_nat) 1857 apply (cut_tac not_msb_from_less[where v="of_nat (word_ctz eisr1 + 32) :: int_sword"]) 1858 apply (clarsimp simp: word_less_alt unat_of_nat_ctz_mw unat_of_nat_ctz_smw 1859 uint_nat)+ 1860 done 1861 1862 have eisr_calc_le: 1863 "eisr0 = 0 \<longrightarrow> eisr1 \<noteq> 0 1864 \<Longrightarrow> eisr_calc eisr0 eisr1 \<le> 63" 1865 for eisr0 :: machine_word and eisr1 1866 using word_ctz_le[where w=eisr0] word_ctz_less[where w=eisr1] 1867 by (clarsimp simp: eisr_calc_def split: if_splits) 1868 1869 have of_nat_word_ctz_0x21helper[simp]: 1870 "0x21 + of_nat (word_ctz w) \<noteq> (0 :: int_sword)" for w :: machine_word 1871 apply (subst unat_arith_simps, simp) 1872 apply (subst unat_add_lem' ; clarsimp simp: unat_of_nat_ctz_smw) 1873 using word_ctz_le[where w=w, simplified] by (auto simp: unat_of_nat_eq) 1874 1875 show ?thesis 1876 apply (cinit) 1877 apply (rule ccorres_pre_getCurThread[unfolded getCurThread_def], rename_tac cthread) 1878 apply (ctac (no_vcg) add: isRunnable_ccorres, rename_tac runnable crunnable) 1879 apply (drule sym) 1880 apply (simp add: to_bool_def) 1881 apply (rule_tac P=runnable in ccorres_cases; clarsimp) 1882 prefer 2 1883 apply ccorres_rewrite 1884 apply (rule ccorres_return_void_C) 1885 apply ccorres_rewrite 1886 apply (ctac (no_vcg) add: get_gic_vcpu_ctrl_eisr0_ccorres) 1887 apply (ctac (no_vcg) add: get_gic_vcpu_ctrl_eisr1_ccorres) 1888 apply (ctac (no_vcg) add: get_gic_vcpu_ctrl_misr_ccorres) 1889 apply (rule ccorres_pre_gets_armKSGICVCPUNumListRegs_ksArchState, rename_tac num_list_regs) 1890 apply clarsimp 1891 apply (rule ccorres_Cond_rhs_Seq ; clarsimp) 1892 apply (rule ccorres_rhs_assoc)+ 1893 apply csymbr 1894 apply (fold eisr_calc_def) 1895 apply (rule_tac xf'=irq_idx_' 1896 and val="if eisr0 \<noteq> 0 1897 then of_nat (word_ctz eisr0) 1898 else (if eisr1 \<noteq> 0 then of_nat (word_ctz eisr1 + 32) else -1)" 1899 and R=\<top> and R'=UNIV 1900 in ccorres_symb_exec_r_known_rv) 1901 apply clarsimp 1902 apply (rule conseqPre, vcg) 1903 apply clarsimp 1904 subgoal for _ _ eisr1 using sint_ctz_32[where x=eisr1] by clarsimp 1905 apply ceqv 1906 apply clarsimp 1907 apply (simp add: if_to_top_of_bind) 1908 apply (rule_tac C'="{s. eisr0 = 0 \<and> eisr1 = 0 1909 \<or> num_list_regs \<le> eisr_calc eisr0 eisr1}" 1910 and Q="\<lambda>s. num_list_regs \<le> 63" 1911 and Q'="{s. gic_vcpu_num_list_regs_' (globals s) = of_nat num_list_regs}" 1912 in ccorres_rewrite_cond_sr_Seq) 1913 apply clarsimp 1914 subgoal for _ _ eisr0 eisr1 1915 using word_ctz_not_minus_1[where w=eisr1] word_ctz_not_minus_1[where w=eisr0] 1916 by (clarsimp split: if_splits simp: eisr_calc_def word_le_nat_alt unat_of_nat_eq 1917 unat_of_nat_ctz_mw of_nat_eq_signed_scast) 1918 1919 apply (rule ccorres_Cond_rhs_Seq) 1920 (* handle fault branch *) 1921 apply clarsimp 1922 apply (rule ccorres_pre_getCurThread, rename_tac cthread) 1923 apply (rule_tac R'="{s. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr cthread}" 1924 in ccorres_symb_exec_r) 1925 apply (ctac add: handleFault_ccorres) 1926 apply (rule conseqPre, vcg) 1927 apply (fastforce simp: cfault_rel_def seL4_Fault_VGICMaintenance_lift_def 1928 seL4_Fault_lift_def seL4_Fault_tag_defs is_cap_fault_def) 1929 apply (rule conseqPre, vcg, fastforce) 1930 apply (simp only:) (* rewrite if condition to False *) 1931 apply (clarsimp simp: bind_assoc) 1932 apply (rule ccorres_rhs_assoc)+ 1933 apply (ctac add: get_gic_vcpu_ctrl_lr_ccorres) 1934 apply (rename_tac virq virq') 1935 apply clarsimp 1936 1937 apply (subgoal_tac "(if eisr0 \<noteq> 0 then of_nat (word_ctz eisr0) 1938 else if eisr1 \<noteq> 0 then of_nat (word_ctz eisr1) + 32 else - 1) 1939 = (of_nat (eisr_calc eisr0 eisr1) :: (machine_word_len sword))") 1940 prefer 2 1941 apply (fastforce split: if_splits simp: eisr_calc_def) 1942 1943 (* getting type and setting EOIIRQEN for valid virq types is captured by virqSetEOIIRQEN *) 1944 apply (rule ccorres_rhs_assoc2) 1945 apply (rule_tac xf'=virq_' 1946 and val="virq_C (ARRAY _. ARM_HYP_H.virqSetEOIIRQEN virq 0)" 1947 and R=\<top> and R'="{s. virq_' s = virq_C (ARRAY _. virq)}" 1948 in ccorres_symb_exec_r_known_rv) 1949 apply (rule conseqPre, vcg) 1950 apply (fastforce simp: virqSetEOIIRQEN_id) 1951 apply ceqv 1952 apply (ctac add: set_gic_vcpu_ctrl_lr_ccorres) 1953 apply clarsimp 1954 apply (rule ccorres_pre_getCurVCPU[simplified comp_def], rename_tac vcpuopt) 1955 apply (rule ccorres_split_nothrow) (* updating vgic LR of current vcpu *) 1956 apply (wpc ; clarsimp) 1957 1958 (* no current vcpu *) 1959 apply (rule_tac C'="{_. False }" 1960 and Q="\<lambda>s. armHSCurVCPU (ksArchState s) = None" 1961 and Q'=UNIV 1962 in ccorres_rewrite_cond_sr) 1963 apply (fastforce dest!: rf_sr_ksArchState_armHSCurVCPU simp: cur_vcpu_relation_def split: option.splits) 1964 apply ccorres_rewrite 1965 apply (rule ccorres_return_Skip) 1966 1967 (* current vcpu *) 1968 apply (rename_tac vcpuptr active) 1969 apply (rule_tac C'="{_. active }" 1970 and Q="\<lambda>s. armHSCurVCPU (ksArchState s) = Some (vcpuptr, active)" 1971 and Q'=UNIV 1972 in ccorres_rewrite_cond_sr) 1973 apply (fastforce dest!: rf_sr_ksArchState_armHSCurVCPU simp: cur_vcpu_relation_def split: option.splits) 1974 1975 (* we unfortunately split an option and product, so we can't unify directly *) 1976 apply (rule_tac A="\<lambda>s. vcpu_at' (fst (the (armHSCurVCPU (ksArchState s)))) s 1977 \<and> armHSCurVCPU (ksArchState s) \<noteq> None" 1978 and A'="{s. armHSCurVCPU_' (globals s) = vcpu_Ptr (fst (vcpuptr, active))}" 1979 in ccorres_guard_imp) 1980 apply (rule_tac P=active in ccorres_cases ; clarsimp ; ccorres_rewrite) 1981 1982 (* active *) 1983 apply (rule ccorres_move_const_guards)+ 1984 apply (rule vgicUpdateLR_ccorres_armHSCurVCPU ; clarsimp simp: word_ctz_le) 1985 apply (fastforce dest: word_ctz_less 1986 simp: eisr_calc_def unat_of_nat_ctz_smw) 1987 apply (erule eisr_calc_le) 1988 apply (rule ccorres_return_Skip) 1989 apply clarsimp 1990 apply (erule eisr_calc_signed_limits) 1991 apply fastforce 1992 apply ceqv 1993 apply clarsimp 1994 apply (rule ccorres_pre_getCurThread, rename_tac cthread) 1995 apply (rule_tac R'="{s. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr cthread}" 1996 in ccorres_symb_exec_r) 1997 apply (ctac add: handleFault_ccorres) 1998 apply (rule conseqPre, vcg) 1999 2000 subgoal for _ _ _ eisr0 eisr1 2001 apply (clarsimp simp: cfault_rel_def seL4_Fault_VGICMaintenance_lift_def 2002 seL4_Fault_lift_def seL4_Fault_tag_defs is_cap_fault_def Let_def 2003 eisr_calc_def mask_eq_iff 2004 split: if_splits) 2005 apply (fastforce simp: uint_nat unat_of_nat_ctz_mw 2006 dest: word_ctz_less[where w=eisr1] word_ctz_less[where w=eisr0])+ 2007 done 2008 2009 apply (rule conseqPre, vcg, fastforce) 2010 apply clarsimp 2011 apply (simp only: split_def) 2012 apply (rule hoare_lift_Pf[where f=ksCurThread]) 2013 apply (wpsimp wp: hoare_vcg_const_imp_lift hoare_vcg_all_lift)+ 2014 apply vcg 2015 apply (wpsimp wp: hoare_vcg_const_imp_lift hoare_vcg_all_lift hoare_vcg_imp_lift' 2016 | assumption (* schematic asm *) 2017 | clarsimp simp: conj_comms cong: conj_cong)+ 2018 apply (vcg exspec=set_gic_vcpu_ctrl_lr_modifies) 2019 apply clarsimp 2020 apply (vcg exspec=set_gic_vcpu_ctrl_lr_modifies) 2021 apply (wpsimp wp: hoare_vcg_const_imp_lift hoare_vcg_all_lift hoare_vcg_imp_lift') 2022 apply (clarsimp) 2023 apply (vcg exspec=get_gic_vcpu_ctrl_lr_modifies) 2024 apply vcg 2025 apply (rule ccorres_pre_getCurThread, rename_tac cthread) 2026 apply (rule_tac R'="{s. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr cthread}" 2027 in ccorres_symb_exec_r) 2028 apply (ctac (no_vcg) add: handleFault_ccorres) 2029 apply (rule conseqPre, vcg) 2030 apply (fastforce simp: cfault_rel_def seL4_Fault_VGICMaintenance_lift_def 2031 seL4_Fault_lift_def seL4_Fault_tag_defs is_cap_fault_def) 2032 apply (rule conseqPre, vcg) 2033 apply (fastforce simp: cfault_rel_def seL4_Fault_VGICMaintenance_lift_def 2034 seL4_Fault_lift_def seL4_Fault_tag_defs is_cap_fault_def) 2035 (* we only care about lifting state-related imps, nothing rv-related is relevant *) 2036 apply (wpsimp wp: hoare_vcg_const_imp_lift hoare_vcg_all_lift 2037 hoare_vcg_imp_lift'[where P="\<lambda>_ s. P s" for P] 2038 | wp_once hoare_drop_imp)+ 2039 2040 apply (clarsimp cong: conj_cong simp: dc_def tcb_at_invs') 2041 apply (frule invs_arch_state') 2042 apply (clarsimp simp: valid_arch_state'_def max_armKSGICVCPUNumListRegs_def) 2043 apply (rule conjI, clarsimp) 2044 apply (rule conjI) 2045 apply (clarsimp simp: pred_tcb_at'_def) 2046 apply (erule obj_at'_weakenE) 2047 apply (case_tac "tcbState k"; fastforce) 2048 apply clarsimp 2049 apply (erule (1) invs'_HScurVCPU_vcpu_at') 2050 apply clarsimp 2051 apply (rule conjI; clarsimp simp: eisr_calc_def cur_vcpu_relation_def split: option.splits) 2052 done 2053qed 2054 2055lemma ccorres_handleReservedIRQ: 2056 "ccorres dc xfdc 2057 (invs' and (\<lambda>s. irq \<in> non_kernel_IRQs \<longrightarrow> sch_act_not (ksCurThread s) s \<and> 2058 (\<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)))) 2059 (UNIV \<inter> {s. irq_' s = ucast irq}) hs 2060 (handleReservedIRQ irq) (Call handleReservedIRQ_'proc)" 2061 supply dc_simp[simp del] 2062 apply (cinit lift: irq_') 2063 apply (rule ccorres_when[where R=\<top>]) 2064 apply (clarsimp simp: irqVGICMaintenance_def INTERRUPT_PPI_9_def ucast_up_ucast is_up) 2065 apply (rule iffI, simp) 2066 apply (rule upcast_ucast_id[where 'b="32 signed"]; simp) 2067 apply (rule ccorres_add_return2) 2068 apply (ctac (no_vcg) add: ccorres_vgicMaintenance) 2069 apply (rule ccorres_return_void_C) 2070 apply wp 2071 apply (simp add: non_kernel_IRQs_def) 2072 done 2073 2074lemma handleInterrupt_ccorres: 2075 "ccorres dc xfdc 2076 (invs' and (\<lambda>s. irq \<in> non_kernel_IRQs \<longrightarrow> sch_act_not (ksCurThread s) s \<and> 2077 (\<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)))) 2078 (UNIV \<inter> \<lbrace>\<acute>irq = ucast irq\<rbrace>) 2079 hs 2080 (handleInterrupt irq) 2081 (Call handleInterrupt_'proc)" 2082 apply (cinit lift: irq_' cong: call_ignore_cong) 2083 apply (rule ccorres_Cond_rhs_Seq) 2084 apply (simp add: Platform_maxIRQ del: Collect_const) 2085 apply (drule scast_maxIRQ_is_less[simplified]) 2086 apply (simp del: Collect_const) 2087 apply (rule ccorres_rhs_assoc)+ 2088 apply (subst doMachineOp_bind) 2089 apply (rule maskInterrupt_empty_fail) 2090 apply (rule ackInterrupt_empty_fail) 2091 apply (ctac add: maskInterrupt_ccorres[unfolded dc_def]) 2092 apply (subst bind_return_unit[where f="doMachineOp (ackInterrupt irq)"]) 2093 apply (ctac add: ackInterrupt_ccorres[unfolded dc_def]) 2094 apply (rule ccorres_split_throws) 2095 apply (rule ccorres_return_void_C[unfolded dc_def]) 2096 apply vcg 2097 apply wp 2098 apply (vcg exspec=ackInterrupt_modifies) 2099 apply wp 2100 apply (vcg exspec=maskInterrupt_modifies) 2101 apply (simp add: scast_maxIRQ_is_not_less Platform_maxIRQ del: Collect_const) 2102 apply (rule ccorres_pre_getIRQState) 2103 apply wpc 2104 apply simp 2105 apply (rule ccorres_fail) 2106 apply (simp add: bind_assoc cong: call_ignore_cong) 2107 apply (rule ccorres_move_const_guards)+ 2108 apply (rule ccorres_cond_true_seq) 2109 apply (rule ccorres_rhs_assoc)+ 2110 apply csymbr 2111 apply (rule getIRQSlot_ccorres3) 2112 apply (rule ccorres_getSlotCap_cte_at) 2113 apply (rule_tac P="cte_at' rv" in ccorres_cross_over_guard) 2114 apply ctac 2115 apply csymbr 2116 apply csymbr 2117 apply (rule ccorres_ntfn_cases) 2118 apply (clarsimp cong: call_ignore_cong simp del: Collect_const) 2119 apply (rule_tac b=send in ccorres_case_bools) 2120 apply simp 2121 apply (rule ccorres_cond_true_seq) 2122 apply (rule ccorres_rhs_assoc)+ 2123 apply csymbr 2124 apply csymbr 2125 apply (rule ccorres_cond_true_seq) 2126 apply (rule ccorres_rhs_assoc)+ 2127 apply csymbr 2128 apply csymbr 2129 apply (ctac (no_vcg) add: sendSignal_ccorres) 2130 apply (ctac (no_vcg) add: maskInterrupt_ccorres) 2131 apply (ctac add: ackInterrupt_ccorres [unfolded dc_def]) 2132 apply wp+ 2133 apply (simp del: Collect_const) 2134 apply (rule ccorres_cond_true_seq) 2135 apply (rule ccorres_rhs_assoc)+ 2136 apply csymbr+ 2137 apply (rule ccorres_cond_false_seq) 2138 apply simp 2139 apply (ctac (no_vcg) add: maskInterrupt_ccorres) 2140 apply (ctac add: ackInterrupt_ccorres [unfolded dc_def]) 2141 apply wp 2142 apply (rule_tac P=\<top> and P'="{s. ret__int_' s = 0 \<and> cap_get_tag cap \<noteq> scast cap_notification_cap}" in ccorres_inst) 2143 apply (clarsimp simp: isCap_simps simp del: Collect_const) 2144 apply (case_tac rva, simp_all del: Collect_const)[1] 2145 prefer 3 2146 apply metis 2147 apply ((rule ccorres_guard_imp2, 2148 rule ccorres_cond_false_seq, simp, 2149 rule ccorres_cond_false_seq, simp, 2150 ctac (no_vcg) add: maskInterrupt_ccorres, 2151 ctac (no_vcg) add: ackInterrupt_ccorres [unfolded dc_def], 2152 wp, simp)+) 2153 apply (wp getSlotCap_wp) 2154 apply simp 2155 apply vcg 2156 apply (simp add: bind_assoc) 2157 apply (rule ccorres_move_const_guards)+ 2158 apply (rule ccorres_cond_false_seq) 2159 apply (rule ccorres_cond_true_seq) 2160 apply (fold dc_def)[1] 2161 apply (rule ccorres_rhs_assoc)+ 2162 apply (ctac (no_vcg) add: timerTick_ccorres) 2163 apply (ctac (no_vcg) add: resetTimer_ccorres) 2164 apply (ctac add: ackInterrupt_ccorres ) 2165 apply wp+ 2166 apply (simp add: Platform_maxIRQ maxIRQ_def del: Collect_const) 2167 apply (rule ccorres_move_const_guards)+ 2168 apply (rule ccorres_cond_false_seq) 2169 apply (rule ccorres_cond_false_seq) 2170 apply (rule ccorres_cond_true_seq) 2171 apply (ctac add: ccorres_handleReservedIRQ) 2172 apply (ctac (no_vcg) add: ackInterrupt_ccorres [unfolded dc_def]) 2173 apply wp 2174 apply (vcg exspec=handleReservedIRQ_modifies) 2175 apply (simp add: sint_ucast_eq_uint is_down uint_up_ucast is_up) 2176 apply (clarsimp simp: word_sless_alt word_less_alt word_le_def Kernel_C.maxIRQ_def 2177 uint_up_ucast is_up_def 2178 source_size_def target_size_def word_size 2179 sint_ucast_eq_uint is_down is_up word_0_sle_from_less) 2180 apply (rule conjI) 2181 apply (clarsimp simp: cte_wp_at_ctes_of) 2182 using un_ui_le[of irq maxIRQ] 2183 apply (clarsimp simp: IRQTimer_def IRQSignal_def maxIRQ_def 2184 cte_wp_at_ctes_of ucast_ucast_b is_up) 2185 apply (intro conjI impI) 2186 apply clarsimp 2187 apply (erule(1) cmap_relationE1[OF cmap_relation_cte]) 2188 apply (clarsimp simp: typ_heap_simps') 2189 apply (simp add: cap_get_tag_isCap) 2190 apply (clarsimp simp: isCap_simps) 2191 apply (frule cap_get_tag_isCap_unfolded_H_cap) 2192 apply (frule cap_get_tag_to_H, assumption) 2193 apply (clarsimp simp: to_bool_def) 2194 apply (fastforce simp: unat_gt_0 intro!: array_assertion_abs_irq[rule_format]) 2195 apply (erule exE conjE)+ 2196 apply (erule(1) rf_sr_cte_at_valid[OF ctes_of_cte_at]) 2197 apply (fastforce simp: unat_gt_0 intro!: array_assertion_abs_irq[rule_format]) 2198 apply (clarsimp simp: IRQReserved_def)+ 2199 done 2200end 2201end 2202 2203