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 (liftE (sendIPC blocking do_call badge canGrant thread epptr)) 66 (Call performInvocation_Endpoint_'proc)" 67 apply cinit 68 apply (ctac add: sendIPC_ccorres) 69 apply (simp add: return_returnOk) 70 apply (rule ccorres_return_CE, simp+)[1] 71 apply wp 72 apply simp 73 apply (vcg exspec=sendIPC_modifies) 74 apply (clarsimp simp add: rf_sr_ksCurThread sch_act_sane_not) 75 done 76 77(* This lemma now assumes 'weak_sch_act_wf (ksSchedulerAction s) s' in place of 'sch_act_simple'. *) 78 79lemma performInvocation_Notification_ccorres: 80 "ccorres (K (K \<bottom>) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') 81 (invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) 82 (UNIV \<inter> {s. ntfn_' s = ntfn_Ptr ntfnptr} 83 \<inter> {s. badge_' s = badge} 84 \<inter> {s. message_' s = message}) [] 85 (liftE (sendSignal ntfnptr badge)) 86 (Call performInvocation_Notification_'proc)" 87 apply cinit 88 apply (ctac add: sendSignal_ccorres) 89 apply (simp add: return_returnOk) 90 apply (rule ccorres_return_CE, simp+)[1] 91 apply wp 92 apply simp 93 apply (vcg exspec=sendSignal_modifies) 94 apply simp 95 done 96 97lemma performInvocation_Reply_ccorres: 98 "ccorres (K (K \<bottom>) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') 99 (invs' and tcb_at' receiver and st_tcb_at' active' sender and sch_act_simple 100 and ((Not o real_cte_at' slot) or cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot) 101 and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte)) 102 slot and (\<lambda>s. ksCurThread s = sender)) 103 (UNIV \<inter> {s. thread_' s = tcb_ptr_to_ctcb_ptr receiver} 104 \<inter> {s. slot_' s = cte_Ptr slot}) [] 105 (liftE (doReplyTransfer sender receiver slot)) 106 (Call performInvocation_Reply_'proc)" 107 apply cinit 108 apply (ctac add: doReplyTransfer_ccorres) 109 apply (simp add: return_returnOk) 110 apply (rule ccorres_return_CE, simp+)[1] 111 apply wp 112 apply simp 113 apply (vcg exspec=doReplyTransfer_modifies) 114 apply (simp add: rf_sr_ksCurThread) 115 apply (auto simp: isReply_def elim!: pred_tcb'_weakenE) 116 done 117 118lemma decodeInvocation_ccorres: 119 "interpret_excaps extraCaps' = excaps_map extraCaps 120 \<Longrightarrow> 121 ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') 122 (invs' and (\<lambda>s. ksCurThread s = thread) and ct_active' and sch_act_simple 123 and valid_cap' cp and (\<lambda>s. \<forall>x \<in> zobj_refs' cp. ex_nonz_cap_to' x s) 124 and (excaps_in_mem extraCaps \<circ> ctes_of) 125 and cte_wp_at' (diminished' cp \<circ> cteCap) slot 126 and (\<lambda>s. \<forall>v \<in> set extraCaps. ex_cte_cap_wp_to' isCNodeCap (snd v) s) 127 and (\<lambda>s. \<forall>v \<in> set extraCaps. s \<turnstile>' fst v \<and> cte_at' (snd v) s) 128 and (\<lambda>s. \<forall>v \<in> set extraCaps. \<forall>y \<in> zobj_refs' (fst v). ex_nonz_cap_to' y s) 129 and (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)) 130 and sysargs_rel args buffer) 131 (UNIV \<inter> {s. call_' s = from_bool isCall} 132 \<inter> {s. block_' s = from_bool isBlocking} 133 \<inter> {s. call_' s = from_bool isCall} 134 \<inter> {s. block_' s = from_bool isBlocking} 135 \<inter> {s. invLabel_' s = label} 136 \<inter> {s. unat (length___unsigned_long_' s) = length args} 137 \<inter> {s. capIndex_' s = cptr} 138 \<inter> {s. slot_' s = cte_Ptr slot} 139 \<inter> {s. excaps_' s = extraCaps'} 140 \<inter> {s. ccap_relation cp (cap_' s)} 141 \<inter> {s. buffer_' s = option_to_ptr buffer}) [] 142 (decodeInvocation label args cptr slot cp extraCaps 143 >>= invocationCatch thread isBlocking isCall id) 144 (Call decodeInvocation_'proc)" 145 apply (cinit' lift: call_' block_' invLabel_' length___unsigned_long_' 146 capIndex_' slot_' excaps_' cap_' buffer_') 147 apply csymbr 148 apply (simp add: cap_get_tag_isCap decodeInvocation_def 149 cong: if_cong StateSpace.state.fold_congs 150 globals.fold_congs 151 del: Collect_const) 152 apply (cut_tac cap=cp in cap_cases_one_on_true_sum) 153 apply (rule ccorres_Cond_rhs_Seq) 154 apply (simp add: Let_def isArchCap_T_isArchObjectCap liftME_invocationCatch) 155 apply (rule ccorres_split_throws) 156 apply (rule ccorres_trim_returnE) 157 apply simp 158 apply simp 159 apply (rule ccorres_call, rule Arch_decodeInvocation_ccorres [where buffer=buffer]) 160 apply assumption 161 apply simp+ 162 apply (vcg exspec=Arch_decodeInvocation_modifies) 163 apply simp 164 apply csymbr 165 apply (simp add: cap_get_tag_isCap del: Collect_const) 166 apply (rule ccorres_Cond_rhs) 167 apply (simp add: invocationCatch_def throwError_bind) 168 apply (rule syscall_error_throwError_ccorres_n) 169 apply (simp add: syscall_error_to_H_cases) 170 apply (rule ccorres_Cond_rhs) 171 apply (simp add: invocationCatch_def throwError_bind) 172 apply (rule syscall_error_throwError_ccorres_n) 173 apply (simp add: syscall_error_to_H_cases) 174 apply (rule ccorres_Cond_rhs) 175 apply (simp add: if_to_top_of_bind) 176 apply (rule ccorres_rhs_assoc)+ 177 apply csymbr 178 apply (rule ccorres_if_cond_throws2[where Q=\<top> and Q'=\<top>]) 179 apply (clarsimp simp: isCap_simps) 180 apply (frule cap_get_tag_isCap_unfolded_H_cap) 181 apply (drule(1) cap_get_tag_to_H) 182 apply (clarsimp simp: to_bool_def) 183 apply (simp add: throwError_bind invocationCatch_def) 184 apply (rule syscall_error_throwError_ccorres_n) 185 apply (simp add: syscall_error_to_H_cases) 186 apply (simp add: returnOk_bind ccorres_invocationCatch_Inr 187 performInvocation_def bind_assoc liftE_bindE) 188 apply (ctac add: setThreadState_ccorres) 189 apply csymbr 190 apply csymbr 191 apply csymbr 192 apply (rule ccorres_pre_getCurThread) 193 apply (simp only: liftE_bindE[symmetric]) 194 apply (ctac add: performInvocation_Endpoint_ccorres) 195 apply (rule ccorres_alternative2) 196 apply (rule ccorres_return_CE, simp+)[1] 197 apply (rule ccorres_return_C_errorE, simp+)[1] 198 apply wp 199 apply simp 200 apply (vcg exspec=performInvocation_Endpoint_modifies) 201 apply simp 202 apply (rule hoare_use_eq[where f=ksCurThread]) 203 apply (wp sts_invs_minor' sts_st_tcb_at'_cases 204 setThreadState_ct' hoare_vcg_all_lift sts_ksQ')+ 205 apply simp 206 apply (vcg exspec=setThreadState_modifies) 207 apply vcg 208 apply (rule ccorres_Cond_rhs) 209 apply (rule ccorres_rhs_assoc)+ 210 apply (csymbr) 211 apply (simp add: if_to_top_of_bind Collect_const[symmetric] 212 del: Collect_const) 213 apply (rule ccorres_if_cond_throws2[where Q=\<top> and Q'=\<top>]) 214 apply (clarsimp simp: isCap_simps) 215 apply (frule cap_get_tag_isCap_unfolded_H_cap) 216 apply (drule(1) cap_get_tag_to_H) 217 apply (clarsimp simp: to_bool_def) 218 apply (simp add: throwError_bind invocationCatch_def) 219 apply (rule syscall_error_throwError_ccorres_n) 220 apply (simp add: syscall_error_to_H_cases) 221 apply (simp add: returnOk_bind ccorres_invocationCatch_Inr 222 performInvocation_def bindE_assoc) 223 apply (simp add: liftE_bindE) 224 apply (ctac add: setThreadState_ccorres) 225 apply csymbr 226 apply csymbr 227 apply (simp only: liftE_bindE[symmetric]) 228 apply (ctac(no_vcg) add: performInvocation_Notification_ccorres) 229 apply (rule ccorres_alternative2) 230 apply (rule ccorres_return_CE, simp+)[1] 231 apply (rule ccorres_return_C_errorE, simp+)[1] 232 apply wp 233 apply (wp sts_invs_minor') 234 apply simp 235 apply (vcg exspec=setThreadState_modifies) 236 apply vcg 237 apply (rule ccorres_Cond_rhs) 238 apply (simp add: if_to_top_of_bind) 239 apply (rule ccorres_rhs_assoc)+ 240 apply csymbr 241 apply (rule ccorres_if_cond_throws2[where Q=\<top> and Q'=\<top>]) 242 apply (clarsimp simp: isCap_simps) 243 apply (frule cap_get_tag_isCap_unfolded_H_cap) 244 apply (clarsimp simp: cap_get_tag_ReplyCap to_bool_def) 245 apply (simp add: throwError_bind invocationCatch_def) 246 apply (rule syscall_error_throwError_ccorres_n) 247 apply (simp add: syscall_error_to_H_cases) 248 apply (simp add: returnOk_bind ccorres_invocationCatch_Inr 249 performInvocation_def liftE_bindE 250 bind_assoc) 251 apply (ctac add: setThreadState_ccorres) 252 apply csymbr 253 apply (rule ccorres_pre_getCurThread) 254 apply (simp only: liftE_bindE[symmetric]) 255 apply (ctac add: performInvocation_Reply_ccorres) 256 apply (rule ccorres_alternative2) 257 apply (rule ccorres_return_CE, simp+)[1] 258 apply (rule ccorres_return_C_errorE, simp+)[1] 259 apply wp 260 apply simp 261 apply (vcg exspec=performInvocation_Reply_modifies) 262 apply (simp add: cur_tcb'_def[symmetric]) 263 apply (rule_tac R="\<lambda>rv s. ksCurThread s = thread" in hoare_post_add) 264 apply (simp cong: conj_cong) 265 apply (strengthen imp_consequent) 266 apply (wp sts_invs_minor' sts_st_tcb_at'_cases) 267 apply simp 268 apply (vcg exspec=setThreadState_modifies) 269 apply vcg 270 apply (rule ccorres_Cond_rhs) 271 apply (simp add: if_to_top_of_bind) 272 apply (rule ccorres_trim_returnE, simp+) 273 apply (simp add: liftME_invocationCatch o_def) 274 apply (rule ccorres_call, rule decodeTCBInvocation_ccorres) 275 apply assumption 276 apply (simp+)[3] 277 apply (rule ccorres_Cond_rhs) 278 apply (rule ccorres_trim_returnE, simp+) 279 apply (simp add: liftME_invocationCatch o_def) 280 apply (rule ccorres_call, 281 erule decodeDomainInvocation_ccorres[unfolded o_def], 282 simp+)[1] 283 apply (rule ccorres_Cond_rhs) 284 apply (simp add: if_to_top_of_bind) 285 apply (rule ccorres_trim_returnE, simp+) 286 apply (simp add: liftME_invocationCatch o_def) 287 apply (rule ccorres_call, 288 erule decodeCNodeInvocation_ccorres[unfolded o_def], 289 simp+)[1] 290 apply (rule ccorres_Cond_rhs) 291 apply simp 292 apply (rule ccorres_trim_returnE, simp+) 293 apply (simp add: liftME_invocationCatch) 294 apply (rule ccorres_call, 295 erule decodeUntypedInvocation_ccorres, simp+)[1] 296 apply (rule ccorres_Cond_rhs) 297 apply (simp add: liftME_invocationCatch) 298 apply (rule ccorres_trim_returnE, simp+) 299 apply (rule ccorres_call, erule decodeIRQControlInvocation_ccorres, 300 simp+)[1] 301 apply (rule ccorres_Cond_rhs) 302 apply (simp add: Let_def liftME_invocationCatch) 303 apply (rule ccorres_rhs_assoc)+ 304 apply csymbr 305 apply (rule ccorres_trim_returnE, simp+) 306 apply (rule ccorres_call, 307 erule decodeIRQHandlerInvocation_ccorres, simp+) 308 apply (rule ccorres_inst[where P=\<top> and P'=UNIV]) 309 apply (simp add: isArchCap_T_isArchObjectCap one_on_true_def from_bool_0) 310 apply (rule conjI) 311 apply (clarsimp simp: tcb_at_invs' ct_in_state'_def 312 simple_sane_strg) 313 apply (clarsimp simp: cte_wp_at_ctes_of valid_cap'_def isCap_simps 314 unat_eq_0 sysargs_rel_n_def n_msgRegisters_def valid_tcb_state'_def 315 | rule conjI | erule pred_tcb'_weakenE disjE 316 | drule st_tcb_at_idle_thread')+ 317 apply fastforce 318 apply (simp add: cap_lift_capEPBadge_mask_eq) 319 apply (clarsimp simp: rf_sr_ksCurThread cap_get_tag_isCap "StrictC'_thread_state_defs") 320 apply (frule word_unat.Rep_inverse') 321 apply (simp add: cap_get_tag_isCap[symmetric] cap_get_tag_ReplyCap) 322 apply (rule conjI) 323 apply (simp add: cap_get_tag_isCap) 324 apply (clarsimp simp: isCap_simps cap_get_tag_to_H) 325 apply (insert ccap_relation_IRQHandler_mask, elim meta_allE, drule(1) meta_mp) 326 apply (simp add: mask_def [of 4]) 327 apply (intro conjI impI; drule(1) cap_get_tag_to_H; clarsimp) 328 apply (simp add: cap_lift_endpoint_cap cap_endpoint_cap_lift_def word_size) 329 done 330 331lemma ccorres_Call_Seq: 332 "\<lbrakk> \<Gamma> f = Some v; ccorres r xf P P' hs a (v ;; c) \<rbrakk> 333 \<Longrightarrow> ccorres r xf P P' hs a (Call f ;; c)" 334 apply (erule ccorres_semantic_equivD1) 335 apply (rule semantic_equivI) 336 apply (auto elim!: exec_elim_cases intro: exec.intros) 337 done 338 339lemma wordFromRights_mask_0: 340 "wordFromRights rghts && ~~ mask 4 = 0" 341 apply (simp add: wordFromRights_def word_ao_dist word_or_zero 342 split: cap_rights.split) 343 apply (simp add: mask_def split: if_split) 344 done 345 346lemma wordFromRights_mask_eq: 347 "wordFromRights rghts && mask 4 = wordFromRights rghts" 348 apply (cut_tac x="wordFromRights rghts" and y="mask 4" and z="~~ mask 4" 349 in word_bool_alg.conj_disj_distrib) 350 apply (simp add: wordFromRights_mask_0) 351 done 352 353lemma loadWordUser_user_word_at: 354 "\<lbrace>\<lambda>s. \<forall>rv. user_word_at rv x s \<longrightarrow> Q rv s\<rbrace> loadWordUser x \<lbrace>Q\<rbrace>" 355 apply (simp add: loadWordUser_def user_word_at_def 356 doMachineOp_def split_def) 357 apply wp 358 apply (clarsimp simp: pointerInUserData_def 359 loadWord_def in_monad upto0_7_def 360 is_aligned_mask) 361 done 362 363lemma mapM_loadWordUser_user_words_at: 364 "\<lbrace>\<lambda>s. \<forall>rv. (\<forall>x < length xs. user_word_at (rv ! x) (xs ! x) s) 365 \<and> length rv = length xs \<longrightarrow> Q rv s\<rbrace> 366 mapM loadWordUser xs \<lbrace>Q\<rbrace>" 367 apply (induct xs arbitrary: Q) 368 apply (simp add: mapM_def sequence_def) 369 apply wp 370 apply (simp add: mapM_Cons) 371 apply wp 372 apply assumption 373 apply (wp loadWordUser_user_word_at) 374 apply clarsimp 375 apply (drule spec, erule mp) 376 apply clarsimp 377 apply (case_tac x) 378 apply simp 379 apply simp 380 done 381 382lemma getSlotCap_slotcap_in_mem: 383 "\<lbrace>\<top>\<rbrace> getSlotCap slot \<lbrace>\<lambda>cap s. slotcap_in_mem cap slot (ctes_of s)\<rbrace>" 384 apply (simp add: getSlotCap_def) 385 apply (wp getCTE_wp') 386 apply (clarsimp simp: cte_wp_at_ctes_of slotcap_in_mem_def) 387 done 388 389lemma lookupExtraCaps_excaps_in_mem[wp]: 390 "\<lbrace>\<top>\<rbrace> lookupExtraCaps thread buffer info \<lbrace>\<lambda>rv s. excaps_in_mem rv (ctes_of s)\<rbrace>,-" 391 apply (simp add: excaps_in_mem_def lookupExtraCaps_def lookupCapAndSlot_def 392 split_def) 393 apply (wp mapME_set) 394 apply (wp getSlotCap_slotcap_in_mem | simp)+ 395 done 396 397lemma getCurThread_ccorres: 398 "ccorres ((=) \<circ> tcb_ptr_to_ctcb_ptr) thread_' 399 \<top> UNIV hs getCurThread (\<acute>thread :== \<acute>ksCurThread)" 400 apply (rule ccorres_from_vcg) 401 apply (rule allI, rule conseqPre, vcg) 402 apply (clarsimp simp: getCurThread_def simpler_gets_def 403 rf_sr_ksCurThread) 404 done 405 406lemma getMessageInfo_ccorres: 407 "ccorres (\<lambda>rv rv'. rv = messageInfoFromWord rv') ret__unsigned_long_' \<top> 408 (UNIV \<inter> {s. thread_' s = tcb_ptr_to_ctcb_ptr thread} 409 \<inter> {s. reg_' s = register_from_H X64_H.msgInfoRegister}) [] 410 (getMessageInfo thread) (Call getRegister_'proc)" 411 apply (simp add: getMessageInfo_def liftM_def[symmetric]) 412 apply (rule ccorres_rel_imp, rule ccorres_guard_imp2, rule getRegister_ccorres) 413 apply simp 414 apply simp 415 done 416 417lemma messageInfoFromWord_spec: 418 "\<forall>s. \<Gamma> \<turnstile> {s} Call messageInfoFromWord_'proc 419 {s'. seL4_MessageInfo_lift (ret__struct_seL4_MessageInfo_C_' s') 420 = mi_from_H (messageInfoFromWord (w_' s))}" 421 apply (rule allI, rule conseqPost, rule messageInfoFromWord_spec[rule_format]) 422 apply simp_all 423 apply (clarsimp simp: seL4_MessageInfo_lift_def mi_from_H_def 424 messageInfoFromWord_def Let_def 425 msgLengthBits_def msgExtraCapBits_def 426 msgMaxExtraCaps_def msgLabelBits_def shiftL_nat) 427 done 428 429lemma threadGet_tcbIpcBuffer_ccorres [corres]: 430 "ccorres (=) w_bufferPtr_' (tcb_at' tptr) UNIV hs 431 (threadGet tcbIPCBuffer tptr) 432 (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t (Ptr &(tcb_ptr_to_ctcb_ptr tptr\<rightarrow> 433 [''tcbIPCBuffer_C''])::machine_word ptr)\<rbrace> 434 (\<acute>w_bufferPtr :== 435 h_val (hrs_mem \<acute>t_hrs) 436 (Ptr &(tcb_ptr_to_ctcb_ptr tptr\<rightarrow>[''tcbIPCBuffer_C''])::machine_word ptr)))" 437 apply (rule ccorres_guard_imp2) 438 apply (rule ccorres_add_return2) 439 apply (rule ccorres_pre_threadGet) 440 apply (rule_tac P = "obj_at' (\<lambda>tcb. tcbIPCBuffer tcb = x) tptr" and 441 P'="{s'. \<exists>ctcb. 442 cslift s' (tcb_ptr_to_ctcb_ptr tptr) = Some ctcb \<and> 443 tcbIPCBuffer_C ctcb = x }" in ccorres_from_vcg) 444 apply (rule allI, rule conseqPre, vcg) 445 apply clarsimp 446 apply (clarsimp simp: return_def typ_heap_simps') 447 apply (clarsimp simp: obj_at'_def ctcb_relation_def) 448 done 449 450lemma handleInvocation_def2: 451 "handleInvocation isCall isBlocking = 452 do thread \<leftarrow> getCurThread; 453 info \<leftarrow> getMessageInfo thread; 454 ptr \<leftarrow> asUser thread (getRegister X64_H.capRegister); 455 v \<leftarrow> (doE (cap, slot) \<leftarrow> capFaultOnFailure ptr False (lookupCapAndSlot thread ptr); 456 buffer \<leftarrow> withoutFailure (VSpace_H.lookupIPCBuffer False thread); 457 extracaps \<leftarrow> lookupExtraCaps thread buffer info; 458 returnOk (slot, cap, extracaps, buffer) 459 odE); 460 case v of Inl f \<Rightarrow> liftE (when isBlocking (handleFault thread f)) 461 | Inr (slot, cap, extracaps, buffer) \<Rightarrow> 462 do args \<leftarrow> getMRs thread buffer info; 463 v' \<leftarrow> do v \<leftarrow> RetypeDecls_H.decodeInvocation (msgLabel info) args ptr slot cap extracaps; 464 invocationCatch thread isBlocking isCall id v od; 465 case v' of Inr _ \<Rightarrow> liftE (replyOnRestart thread [] isCall) 466 | Inl (Inl syserr) \<Rightarrow> liftE (when isCall (replyFromKernel thread 467 (msgFromSyscallError syserr))) 468 | Inl (Inr preempt) \<Rightarrow> throwError preempt 469 od 470 od" 471 apply (simp add: handleInvocation_def Syscall_H.syscall_def runExceptT_def 472 liftE_bindE cong: sum.case_cong) 473 apply (rule ext, (rule bind_apply_cong [OF refl])+) 474 apply (clarsimp simp: bind_assoc split: sum.split) 475 apply (rule bind_apply_cong [OF refl])+ 476 apply (clarsimp simp: invocationCatch_def throwError_bind 477 liftE_bindE bind_assoc 478 split: sum.split) 479 apply (rule bind_apply_cong [OF refl])+ 480 apply (simp add: bindE_def bind_assoc) 481 apply (rule bind_apply_cong [OF refl])+ 482 apply (clarsimp simp: lift_def throwError_bind returnOk_bind split: sum.split) 483 apply (simp cong: bind_cong add: ts_Restart_case_helper') 484 apply (simp add: when_def[symmetric] replyOnRestart_def[symmetric]) 485 apply (simp add: liftE_def replyOnRestart_twice alternative_bind 486 alternative_refl split: if_split) 487 done 488 489lemma thread_state_to_tsType_eq_Restart: 490 "(thread_state_to_tsType ts = scast ThreadState_Restart) 491 = (ts = Restart)" 492 by (cases ts, simp_all add: "StrictC'_thread_state_defs") 493 494lemma wordFromMessageInfo_spec: 495 "\<forall>s. \<Gamma>\<turnstile> {s} Call wordFromMessageInfo_'proc 496 {s'. \<forall>mi. seL4_MessageInfo_lift (mi_' s) = mi_from_H mi 497 \<longrightarrow> ret__unsigned_long_' s' = wordFromMessageInfo mi}" 498 apply (rule allI, rule conseqPost[OF wordFromMessageInfo_spec[rule_format] _ subset_refl]) 499 apply (clarsimp simp: wordFromMessageInfo_def 500 msgLengthBits_def msgExtraCapBits_def msgMaxExtraCaps_def shiftL_nat) 501 apply (drule sym[where t="mi_from_H mi" for mi]) 502 apply (clarsimp simp: seL4_MessageInfo_lift_def mi_from_H_def mask_def) 503 apply (thin_tac _)+ 504 apply word_bitwise 505 done 506 507lemma handleDoubleFault_ccorres: 508 "ccorres dc xfdc (invs' and tcb_at' tptr and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and 509 sch_act_not tptr and (\<lambda>s. \<forall>p. tptr \<notin> set (ksReadyQueues s p))) 510 (UNIV \<inter> {s. tptr_' s = tcb_ptr_to_ctcb_ptr tptr}) 511 [] (handleDoubleFault tptr ex1 ex2) 512 (Call handleDoubleFault_'proc)" 513 apply (cinit lift: tptr_') 514 apply (subst ccorres_seq_skip'[symmetric]) 515 apply (ctac (no_vcg)) 516 apply (rule ccorres_symb_exec_l) 517 apply (rule ccorres_return_Skip) 518 apply (wp asUser_inv getRestartPC_inv)+ 519 apply (rule empty_fail_asUser) 520 apply (simp add: getRestartPC_def) 521 apply wp 522 apply clarsimp 523 apply (simp add: ThreadState_Inactive_def) 524 apply (fastforce simp: valid_tcb_state'_def) 525 done 526 527lemma cap_case_EndpointCap_CanSend_CanGrant: 528 "(case cap of EndpointCap v0 v1 True v3 True \<Rightarrow> f v0 v1 v3 529 | _ \<Rightarrow> g) 530 = (if (isEndpointCap cap \<and> capEPCanSend cap \<and> capEPCanGrant cap) 531 then f (capEPPtr cap) (capEPBadge cap) (capEPCanReceive cap) 532 else g)" 533 by (simp add: isCap_simps 534 split: capability.split bool.split) 535 536lemma threadGet_tcbFaultHandler_ccorres [corres]: 537 "ccorres (=) handlerCPtr_' (tcb_at' tptr) UNIV hs 538 (threadGet tcbFaultHandler tptr) 539 (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t (tcb_ptr_to_ctcb_ptr tptr)\<rbrace> 540 (\<acute>handlerCPtr :== 541 h_val (hrs_mem \<acute>t_hrs) 542 (Ptr &(tcb_ptr_to_ctcb_ptr tptr\<rightarrow>[''tcbFaultHandler_C''])::machine_word ptr)))" 543 apply (rule ccorres_guard_imp2) 544 apply (rule ccorres_add_return2) 545 apply (rule ccorres_pre_threadGet) 546 apply (rule_tac P = "obj_at' (\<lambda>tcb. tcbFaultHandler tcb = x) tptr" and 547 P'="{s'. \<exists> ctcb. 548 cslift s' (tcb_ptr_to_ctcb_ptr tptr) = Some ctcb \<and> 549 tcbFaultHandler_C ctcb = x }" in ccorres_from_vcg) 550 apply (rule allI, rule conseqPre, vcg) 551 apply clarsimp 552 apply (clarsimp simp: return_def typ_heap_simps') 553 apply (clarsimp simp: obj_at'_def ctcb_relation_def) 554done 555 556lemma hrs_mem_update_use_hrs_mem: 557 "hrs_mem_update f = (\<lambda>hrs. (hrs_mem_update $ (\<lambda>_. f (hrs_mem hrs))) hrs)" 558 by (simp add: hrs_mem_update_def hrs_mem_def fun_eq_iff) 559 560lemma sendFaultIPC_ccorres: 561 "ccorres (cfault_rel2 \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') 562 (invs' and st_tcb_at' simple' tptr and sch_act_not tptr and 563 (\<lambda>s. \<forall>p. tptr \<notin> set (ksReadyQueues s p))) 564 (UNIV \<inter> {s. (cfault_rel (Some fault) (seL4_Fault_lift(current_fault_' (globals s))) 565 (lookup_fault_lift(current_lookup_fault_' (globals s))))} 566 \<inter> {s. tptr_' s = tcb_ptr_to_ctcb_ptr tptr}) 567 [] (sendFaultIPC tptr fault) 568 (Call sendFaultIPC_'proc)" 569 apply (cinit lift: tptr_' cong: call_ignore_cong) 570 apply (simp add: liftE_bindE del:Collect_const cong:call_ignore_cong) 571 apply (rule ccorres_symb_exec_r) 572 apply (rule ccorres_split_nothrow) 573 apply (rule threadGet_tcbFaultHandler_ccorres) 574 apply ceqv 575 576 apply (rule_tac xf'=lu_ret___struct_lookupCap_ret_C_' 577 in ccorres_split_nothrow_callE) 578 apply (rule capFaultOnFailure_ccorres) 579 apply (rule lookupCap_ccorres) 580 apply simp 581 apply simp 582 apply simp 583 apply simp 584 apply ceqv 585 apply clarsimp 586 apply csymbr+ 587 588 apply (simp add: cap_case_EndpointCap_CanSend_CanGrant) 589 590 apply (rule ccorres_rhs_assoc2) 591 592 apply (rule ccorres_symb_exec_r) 593 apply (rule_tac Q=\<top> 594 and Q'="\<lambda>s'. 595 ( ret__int_' s' = 596 (if ( (cap_get_tag (lookupCap_ret_C.cap_C rv'a) = scast cap_endpoint_cap) \<and> 597 (capCanSend_CL (cap_endpoint_cap_lift (lookupCap_ret_C.cap_C rv'a)))\<noteq>0 \<and> 598 (capCanGrant_CL (cap_endpoint_cap_lift (lookupCap_ret_C.cap_C rv'a)))\<noteq>0) 599 then 1 else 0))" 600 in ccorres_cond_both') 601 apply clarsimp 602 apply (frule cap_get_tag_isCap(4)[symmetric], 603 clarsimp simp: cap_get_tag_EndpointCap to_bool_def 604 split:if_splits) 605 apply auto[1] 606 apply (rule ccorres_rhs_assoc) 607 apply (rule ccorres_rhs_assoc) 608 apply (rule ccorres_rhs_assoc) 609 apply (simp add: liftE_def bind_assoc) 610 611 apply (rule_tac ccorres_split_nothrow_novcg) 612 apply (rule_tac P=\<top> and P'=invs' 613 and R="{s. 614 (cfault_rel (Some fault) 615 (seL4_Fault_lift(current_fault_' (globals s))) 616 (lookup_fault_lift(original_lookup_fault_' s)))}" 617 in threadSet_ccorres_lemma4) 618 apply vcg 619 apply (clarsimp simp: typ_heap_simps' packed_heap_update_collapse_hrs) 620 621 apply (intro conjI allI impI) 622 apply (simp add: typ_heap_simps' rf_sr_def) 623 apply (rule rf_sr_tcb_update_no_queue2[unfolded rf_sr_def, simplified], 624 assumption+, (simp add: typ_heap_simps')+) 625 apply (rule ball_tcb_cte_casesI, simp+) 626 apply (simp add: ctcb_relation_def cthread_state_relation_def ) 627 apply (case_tac "tcbState tcb", simp+) 628 apply (simp add: rf_sr_def) 629 apply (rule rf_sr_tcb_update_no_queue2[unfolded rf_sr_def, simplified], 630 assumption+, (simp add: typ_heap_simps' | simp only: hrs_mem_update_use_hrs_mem)+) 631 apply (rule ball_tcb_cte_casesI, simp+) 632 apply (clarsimp simp: typ_heap_simps') 633 apply (simp add: ctcb_relation_def cthread_state_relation_def) 634 apply (rule conjI) 635 apply (case_tac "tcbState tcb", simp+) 636 apply (simp add: cfault_rel_def) 637 apply (clarsimp) 638 apply (clarsimp simp: seL4_Fault_lift_def Let_def is_cap_fault_def 639 split: if_split_asm) 640 apply ceqv 641 642 apply csymbr 643 apply csymbr 644 apply (ctac (no_vcg) add: sendIPC_ccorres) 645 apply (ctac (no_vcg) add: ccorres_return_CE [unfolded returnOk_def comp_def]) 646 apply wp 647 apply (wp threadSet_pred_tcb_no_state threadSet_invs_trivial threadSet_typ_at_lifts 648 | simp)+ 649 650 apply (clarsimp simp: guard_is_UNIV_def) 651 apply (frule cap_get_tag_isCap(4)[symmetric]) 652 apply (clarsimp simp: cap_get_tag_EndpointCap to_bool_def) 653 654 apply clarsimp 655 apply (rule_tac P=\<top> and P'=UNIV 656 in ccorres_from_vcg_throws) 657 apply clarsimp 658 apply (clarsimp simp add: throwError_def return_def) 659 apply (rule conseqPre, vcg) 660 apply (clarsimp simp: EXCEPTION_FAULT_def EXCEPTION_NONE_def) 661 apply (simp add: cfault_rel2_def cfault_rel_def EXCEPTION_FAULT_def) 662 apply (simp add: seL4_Fault_CapFault_lift) 663 apply (simp add: lookup_fault_missing_capability_lift is_cap_fault_def) 664 665 apply vcg 666 667 apply (clarsimp) 668 apply (rule conseqPre, vcg) 669 apply clarsimp 670 671 apply clarsimp 672 apply (rule ccorres_split_throws) 673 apply (rule_tac P=\<top> and P'="{x. errstate x= err'}" 674 in ccorres_from_vcg_throws) 675 apply clarsimp 676 apply (clarsimp simp add: throwError_def return_def) 677 apply (rule conseqPre, vcg) 678 apply (clarsimp simp: EXCEPTION_FAULT_def EXCEPTION_NONE_def) 679 apply (simp add: cfault_rel2_def cfault_rel_def EXCEPTION_FAULT_def) 680 apply (simp add: seL4_Fault_CapFault_lift is_cap_fault_def) 681 apply (erule lookup_failure_rel_fault_lift [rotated, unfolded EXCEPTION_NONE_def, simplified], 682 assumption) 683 684 apply vcg 685 apply (clarsimp simp: inQ_def) 686 apply (rule_tac Q="\<lambda>a b. invs' b \<and> st_tcb_at' simple' tptr b 687 \<and> sch_act_not tptr b \<and> valid_cap' a b 688 \<and> (\<forall>p. tptr \<notin> set (ksReadyQueues b p))" 689 and E="\<lambda> _. \<top>" 690 in hoare_post_impErr) 691 apply (wp) 692 apply (clarsimp simp: isCap_simps) 693 apply (clarsimp simp: valid_cap'_def pred_tcb_at') 694 apply simp 695 696 apply (clarsimp) 697 apply (vcg exspec=lookupCap_modifies) 698 apply clarsimp 699 apply wp 700 apply (clarsimp) 701 apply (vcg) 702 703 apply (clarsimp, vcg) 704 apply (rule conseqPre, vcg) 705 apply clarsimp 706 apply (clarsimp) 707 apply fastforce 708 done 709 710lemma handleFault_ccorres: 711 "ccorres dc xfdc (invs' and st_tcb_at' simple' t and 712 sch_act_not t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p))) 713 (UNIV \<inter> {s. (cfault_rel (Some flt) (seL4_Fault_lift(current_fault_' (globals s))) 714 (lookup_fault_lift(current_lookup_fault_' (globals s))) )} 715 \<inter> {s. tptr_' s = tcb_ptr_to_ctcb_ptr t}) 716 hs (handleFault t flt) 717 (Call handleFault_'proc)" 718 apply (cinit lift: tptr_') 719 apply (simp add: catch_def) 720 apply (rule ccorres_symb_exec_r) 721 apply (rule ccorres_split_nothrow_novcg_case_sum) 722 apply (ctac (no_vcg) add: sendFaultIPC_ccorres) 723 apply ceqv 724 apply clarsimp 725 apply (rule ccorres_cond_empty) 726 apply (rule ccorres_return_Skip') 727 apply clarsimp 728 apply (rule ccorres_cond_univ) 729 apply (ctac (no_vcg) add: handleDoubleFault_ccorres [unfolded dc_def]) 730 apply (simp add: sendFaultIPC_def) 731 apply wp 732 apply ((wp hoare_vcg_all_lift_R hoare_drop_impE_R |wpc |simp add: throw_def)+)[1] 733 apply clarsimp 734 apply ((wp hoare_vcg_all_lift_R hoare_drop_impE_R |wpc |simp add: throw_def)+)[1] 735 apply (wp) 736 apply (simp add: guard_is_UNIV_def) 737 apply (simp add: guard_is_UNIV_def) 738 apply clarsimp 739 apply vcg 740 apply clarsimp 741 apply (rule conseqPre, vcg) 742 apply clarsimp 743 apply (clarsimp simp: pred_tcb_at') 744 done 745 746lemma getMessageInfo_less_4: 747 "\<lbrace>\<top>\<rbrace> getMessageInfo t \<lbrace>\<lambda>rv s. msgExtraCaps rv < 4\<rbrace>" 748 including no_pre 749 apply (simp add: getMessageInfo_def) 750 apply wp 751 apply (rule hoare_strengthen_post, rule hoare_vcg_prop) 752 apply (simp add: messageInfoFromWord_def Let_def 753 Types_H.msgExtraCapBits_def) 754 apply (rule minus_one_helper5, simp) 755 apply simp 756 apply (rule word_and_le1) 757 done 758 759lemma invs_queues_imp: 760 "invs' s \<longrightarrow> valid_queues s" 761 by clarsimp 762 763(* FIXME: move *) 764lemma length_CL_from_H [simp]: 765 "length_CL (mi_from_H mi) = msgLength mi" 766 by (simp add: mi_from_H_def) 767 768lemma getMRs_length: 769 "\<lbrace>\<lambda>s. msgLength mi \<le> 120\<rbrace> getMRs thread buffer mi 770 \<lbrace>\<lambda>args s. if buffer = None then length args = min (unat n_msgRegisters) (unat (msgLength mi)) 771 else length args = unat (msgLength mi)\<rbrace>" 772 apply (cases buffer) 773 apply (simp add: getMRs_def) 774 apply (rule hoare_pre, wp) 775 apply (rule asUser_const_rv) 776 apply simp 777 apply (wp mapM_length) 778 apply (simp add: min_def length_msgRegisters) 779 apply (clarsimp simp: n_msgRegisters_def) 780 apply (simp add: getMRs_def) 781 apply (rule hoare_pre, wp) 782 apply simp 783 apply (wp mapM_length asUser_const_rv mapM_length)+ 784 apply (clarsimp simp: length_msgRegisters) 785 apply (simp add: min_def split: if_splits) 786 apply (clarsimp simp: word_le_nat_alt) 787 apply (simp add: msgMaxLength_def msgLengthBits_def n_msgRegisters_def) 788 done 789 790lemma getMessageInfo_msgLength': 791 "\<lbrace>\<top>\<rbrace> getMessageInfo t \<lbrace>\<lambda>rv s. msgLength rv \<le> 0x78\<rbrace>" 792 including no_pre 793 apply (simp add: getMessageInfo_def) 794 apply wp 795 apply (rule hoare_strengthen_post, rule hoare_vcg_prop) 796 apply (simp add: messageInfoFromWord_def Let_def msgMaxLength_def not_less 797 Types_H.msgExtraCapBits_def split: if_split ) 798 done 799 800lemma handleInvocation_ccorres: 801 "ccorres (K dc \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') 802 (invs' and 803 ct_active' and sch_act_simple and 804 (\<lambda>s. \<forall>x. ksCurThread s \<notin> set (ksReadyQueues s x))) 805 (UNIV \<inter> {s. isCall_' s = from_bool isCall} 806 \<inter> {s. isBlocking_' s = from_bool isBlocking}) [] 807 (handleInvocation isCall isBlocking) (Call handleInvocation_'proc)" 808 apply (cinit' lift: isCall_' isBlocking_' 809 simp: whileAnno_def handleInvocation_def2) 810 apply (simp add: liftE_bindE del: Collect_const cong: call_ignore_cong) 811 apply (ctac(no_vcg) add: getCurThread_ccorres) 812 apply (ctac(no_vcg) add: getMessageInfo_ccorres) 813 apply (simp del: Collect_const cong: call_ignore_cong) 814 apply csymbr 815 apply (ctac(no_vcg) add: getRegister_ccorres) 816 apply (simp add: Syscall_H.syscall_def 817 liftE_bindE split_def bindE_bind_linearise 818 cong: call_ignore_cong 819 del: Collect_const) 820 apply (rule_tac ccorres_split_nothrow_case_sum) 821 apply (ctac add: capFaultOnFailure_ccorres 822 [OF lookupCapAndSlot_ccorres]) 823 apply ceqv 824 apply (simp add: ccorres_cond_iffs Collect_False 825 cong: call_ignore_cong 826 del: Collect_const) 827 apply (simp only: bind_assoc) 828 apply (ctac(no_vcg) add: lookupIPCBuffer_ccorres) 829 apply (simp add: liftME_def bindE_assoc del: Collect_const) 830 apply (simp add: bindE_bind_linearise del: Collect_const) 831 apply (rule_tac xf'="\<lambda>s. (status_' s, 832 current_extra_caps_' (globals s))" 833 and ef'=fst and vf'=snd and es=errstate 834 in ccorres_split_nothrow_novcg_case_sum) 835 apply (rule ccorres_call, rule lookupExtraCaps_ccorres, simp+) 836 apply (rule ceqv_tuple2, ceqv, ceqv) 837 apply (simp add: returnOk_bind liftE_bindE 838 Collect_False 839 ccorres_cond_iffs ts_Restart_case_helper' 840 del: Collect_const cong: bind_cong) 841 apply (rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2, 842 rule_tac xf'="length___unsigned_long_'" 843 and r'="\<lambda>rv rv'. unat rv' = length rv" 844 in ccorres_split_nothrow) 845 apply (rule ccorres_add_return2) 846 apply (rule ccorres_symb_exec_l) 847 apply (rule_tac P="\<lambda>s. rvd \<noteq> Some 0 \<and> (if rvd = None then 848 length x = min (unat (n_msgRegisters)) 849 (unat (msgLength (messageInfoFromWord ret__unsigned_long))) 850 else 851 length x = (unat (msgLength (messageInfoFromWord ret__unsigned_long))))" 852 and P'=UNIV 853 in ccorres_from_vcg) 854 apply (clarsimp simp: return_def) 855 apply (rule conseqPre, vcg) 856 apply (clarsimp simp: word_less_nat_alt) 857 apply (rule conjI) 858 apply clarsimp 859 apply (case_tac rvd, clarsimp simp: option_to_ptr_def option_to_0_def min_def n_msgRegisters_def) 860 apply (clarsimp simp: option_to_0_def option_to_ptr_def) 861 apply clarsimp 862 apply (case_tac rvd, 863 clarsimp simp: option_to_0_def min_def option_to_ptr_def 864 n_msgRegisters_def 865 split: if_splits) 866 apply (clarsimp simp: option_to_0_def option_to_ptr_def) 867 apply wp 868 apply (wp getMRs_length) 869 apply simp 870 apply ceqv 871 apply csymbr 872 apply (simp only: bind_assoc[symmetric]) 873 apply (rule ccorres_split_nothrow_novcg_case_sum) 874 apply (ctac add: decodeInvocation_ccorres) 875 apply ceqv 876 apply (simp add: Collect_False exception_defs 877 replyOnRestart_def liftE_def bind_assoc 878 del: Collect_const) 879 apply (rule ccorres_move_c_guard_tcb) 880 apply (rule getThreadState_ccorres_foo) 881 apply csymbr 882 apply (rule ccorres_abstract_cleanup) 883 apply (rule_tac P="ret__unsigned_longlong = thread_state_to_tsType rvg" 884 in ccorres_gen_asm2) 885 apply (simp add: thread_state_to_tsType_eq_Restart from_bool_0 886 del: Collect_const add: Collect_const[symmetric]) 887 apply (rule ccorres_Cond_rhs_Seq) 888 apply (rule ccorres_rhs_assoc)+ 889 apply (rule ccorres_Cond_rhs_Seq) 890 apply (simp add: bind_assoc) 891 apply (ctac(no_vcg) add: replyFromKernel_success_empty_ccorres) 892 apply (ctac(no_vcg) add: setThreadState_ccorres) 893 apply (rule ccorres_return_CE[folded return_returnOk], simp+)[1] 894 apply wp+ 895 apply (rule hoare_strengthen_post, rule rfk_invs') 896 apply auto[1] 897 apply simp 898 apply (ctac(no_vcg) add: setThreadState_ccorres) 899 apply (rule ccorres_return_CE[folded return_returnOk], simp+)[1] 900 apply wp 901 apply simp 902 apply (rule ccorres_return_CE[folded return_returnOk], simp+)[1] 903 apply wpc 904 apply (simp add: syscall_error_rel_def from_bool_0 exception_defs 905 Collect_False ccorres_cond_iffs Collect_True 906 del: Collect_const) 907 apply (rule ccorres_rhs_assoc)+ 908 apply (simp add: liftE_def Collect_const[symmetric] 909 del: Collect_const) 910 apply (rule ccorres_Cond_rhs_Seq) 911 apply simp 912 apply (ctac(no_vcg) add: replyFromKernel_error_ccorres) 913 apply (rule ccorres_split_throws) 914 apply (rule ccorres_return_CE[folded return_returnOk], simp+)[1] 915 apply vcg 916 apply wp 917 apply simp 918 apply (rule ccorres_split_throws) 919 apply (rule ccorres_return_CE[folded return_returnOk], simp+)[1] 920 apply vcg 921 apply (simp add: cintr_def) 922 apply (rule ccorres_split_throws) 923 apply (rule ccorres_return_C_errorE, simp+)[1] 924 apply vcg 925 apply (simp add: invocationCatch_def o_def) 926 apply (rule_tac Q="\<lambda>rv'. invs' and tcb_at' rv" 927 and E="\<lambda>ft. invs' and tcb_at' rv" 928 in hoare_post_impErr) 929 apply (wp hoare_split_bind_case_sumE 930 alternative_wp hoare_drop_imps 931 setThreadState_nonqueued_state_update 932 ct_in_state'_set setThreadState_st_tcb 933 hoare_vcg_all_lift sts_ksQ' 934 | wpc | wps)+ 935 apply auto[1] 936 apply clarsimp 937 apply (clarsimp simp: guard_is_UNIV_def Collect_const_mem) 938 apply (simp add: "StrictC'_thread_state_defs" mask_def) 939 apply (simp add: typ_heap_simps) 940 apply (case_tac ts, simp_all add: cthread_state_relation_def)[1] 941 apply (clarsimp simp: guard_is_UNIV_def Collect_const_mem) 942 apply (clarsimp simp add: intr_and_se_rel_def exception_defs 943 syscall_error_rel_def cintr_def 944 split: sum.split_asm) 945 apply (simp add: conj_comms) 946 apply (wp getMRs_sysargs_rel) 947 apply (simp add: ) 948 apply vcg 949 apply (simp add: ccorres_cond_iffs ccorres_seq_cond_raise 950 Collect_True Collect_False 951 del: Collect_const) 952 apply (rule ccorres_rhs_assoc)+ 953 apply (simp add: ccorres_cond_iffs Collect_const[symmetric] 954 del: Collect_const) 955 apply (rule ccorres_Cond_rhs_Seq) 956 apply (simp add: from_bool_0 liftE_def) 957 apply (ctac(no_vcg) add: handleFault_ccorres) 958 apply (rule ccorres_split_throws) 959 apply (rule ccorres_return_CE[folded return_returnOk], simp+)[1] 960 apply vcg 961 apply wp 962 apply (simp add: from_bool_0 liftE_def) 963 apply (rule ccorres_split_throws) 964 apply (rule ccorres_return_CE[folded return_returnOk], simp+)[1] 965 apply vcg 966 apply (simp add: ball_conj_distrib) 967 apply (wp lookupExtraCaps_excaps_in_mem 968 lec_dimished'[unfolded o_def] 969 lec_derived'[unfolded o_def]) 970 apply (clarsimp simp: guard_is_UNIV_def option_to_ptr_def 971 mi_from_H_def) 972 apply (clarsimp simp: guard_is_UNIV_def) 973 apply simp 974 apply (wp lookupIPCBuffer_Some_0) 975 apply (simp add: Collect_True liftE_def return_returnOk 976 del: Collect_const) 977 apply (rule ccorres_rhs_assoc)+ 978 apply (rule_tac P=\<top> in ccorres_cross_over_guard) 979 apply (rule ccorres_symb_exec_r) 980 apply (rule ccorres_split_nothrow_novcg_dc) 981 apply (rule ccorres_when[where R=\<top>]) 982 apply (simp add: from_bool_0 Collect_const_mem) 983 apply (ctac add: handleFault_ccorres) 984 apply (rule ccorres_split_throws) 985 apply (rule ccorres_return_CE, simp+)[1] 986 apply vcg 987 apply wp 988 apply (simp add: guard_is_UNIV_def) 989 apply vcg 990 apply (rule conseqPre, vcg) 991 apply clarsimp 992 apply (simp, wp lcs_diminished'[unfolded o_def]) 993 apply clarsimp 994 apply (vcg exspec= lookupCapAndSlot_modifies) 995 apply simp 996 apply (wp getMessageInfo_less_4 getMessageInfo_le3 getMessageInfo_msgLength')+ 997 apply (simp add: msgMaxLength_def, wp getMessageInfo_msgLength')[1] 998 apply simp 999 apply wp 1000 apply (clarsimp simp: Collect_const_mem) 1001 apply (simp add: Kernel_C.msgInfoRegister_def X64_H.msgInfoRegister_def 1002 X64.msgInfoRegister_def Kernel_C.RSI_def Kernel_C.RDI_def 1003 Kernel_C.capRegister_def X64_H.capRegister_def 1004 X64.capRegister_def) 1005 apply (clarsimp simp: cfault_rel_def option_to_ptr_def) 1006 apply (simp add: seL4_Fault_CapFault_lift is_cap_fault_def) 1007 apply (frule lookup_failure_rel_fault_lift, assumption) 1008 apply clarsimp 1009 apply (clarsimp simp: ct_in_state'_def pred_tcb_at') 1010 apply (auto simp: ct_in_state'_def sch_act_simple_def intro!: active_ex_cap' 1011 elim!: pred_tcb'_weakenE dest!: st_tcb_at_idle_thread')[1] 1012 done 1013 1014lemma ccorres_return_void_catchbrk: 1015 "ccorres_underlying sr G r xf ar axf P P' hs 1016 f return_void_C 1017 \<Longrightarrow> ccorres_underlying sr G r xf ar axf P P' (catchbrk_C # hs) 1018 f return_void_C" 1019 apply (simp add: return_void_C_def catchbrk_C_def) 1020 apply (rule ccorresI') 1021 apply clarsimp 1022 apply (erule exec_handlers_Seq_cases') 1023 prefer 2 1024 apply (clarsimp elim!: exec_Normal_elim_cases) 1025 apply (clarsimp elim!: exec_Normal_elim_cases) 1026 apply (erule exec_handlers.cases, simp_all) 1027 prefer 2 1028 apply (auto elim!: exec_Normal_elim_cases)[1] 1029 apply (clarsimp elim!: exec_Normal_elim_cases) 1030 apply (erule exec_Normal_elim_cases, simp_all) 1031 apply (clarsimp elim!: exec_Normal_elim_cases) 1032 apply (erule(4) ccorresE) 1033 apply (rule EHAbrupt) 1034 apply (fastforce intro: exec.intros) 1035 apply assumption 1036 apply clarsimp 1037 apply (frule exec_handlers_less) 1038 apply clarsimp 1039 apply fastforce 1040 done 1041 1042lemma real_cte_tcbCallerSlot: 1043 "tcb_at' t s \<Longrightarrow> \<not> real_cte_at' (t + 2 ^ cte_level_bits * tcbCallerSlot) s" 1044 apply (clarsimp simp: obj_at'_def projectKOs objBits_simps' 1045 cte_level_bits_def tcbCallerSlot_def) 1046 apply (drule_tac x=t and y="t + a" for a in ps_clearD, assumption) 1047 apply (rule le_neq_trans, simp_all)[1] 1048 apply (erule is_aligned_no_wrap') 1049 apply simp 1050 apply (subst field_simps[symmetric], rule is_aligned_no_overflow3, assumption, simp_all) 1051 done 1052 1053lemma handleReply_ccorres: 1054 "ccorres dc xfdc 1055 (\<lambda>s. invs' s \<and> st_tcb_at' (\<lambda>a. \<not> isReply a) (ksCurThread s) s \<and> sch_act_simple s) 1056 UNIV 1057 [] 1058 (handleReply) 1059 (Call handleReply_'proc)" 1060 apply cinit 1061 apply (rule ccorres_pre_getCurThread) 1062 1063 apply (simp only: getThreadCallerSlot_def locateSlot_conv) 1064 1065 1066 apply (rule_tac P="\<lambda>s. thread=ksCurThread s \<and> invs' s \<and> is_aligned thread tcbBlockSizeBits" 1067 and r'="\<lambda> a c. c = cte_Ptr a" 1068 and xf'="callerSlot_'" and P'=UNIV in ccorres_split_nothrow) 1069 apply (rule ccorres_from_vcg) 1070 apply (rule allI, rule conseqPre, vcg) 1071 apply (clarsimp simp: return_def word_sle_def) 1072 apply (frule is_aligned_neg_mask_eq) 1073 apply (frule tcb_at_invs') 1074 apply (simp add: mask_def tcbCallerSlot_def 1075 cte_level_bits_def size_of_def 1076 ptr_add_assertion_positive 1077 tcb_cnode_index_defs rf_sr_ksCurThread 1078 rf_sr_tcb_ctes_array_assertion2[THEN array_assertion_shrink_right]) 1079 apply ceqv 1080 1081 apply (simp del: Collect_const) 1082 apply (rule ccorres_getSlotCap_cte_at) 1083 apply (rule ccorres_move_c_guard_cte) 1084 apply ctac 1085 apply (wpc, simp_all) 1086 apply (rule ccorres_fail) 1087 apply (simp add: ccap_relation_NullCap_iff cap_tag_defs) 1088 apply (rule ccorres_split_throws) 1089 apply (rule ccorres_Catch) 1090 apply csymbr 1091 apply (rule ccorres_cond_false) 1092 apply (rule ccorres_cond_true) 1093 apply simp 1094 apply (rule ccorres_return_void_catchbrk) 1095 apply (rule ccorres_return_void_C[unfolded dc_def]) 1096 apply (vcg exspec=doReplyTransfer_modifies) 1097 apply (rule ccorres_fail)+ 1098 apply (wpc, simp_all) 1099 apply (rule ccorres_fail) 1100 apply (rule ccorres_split_throws) 1101 apply (rule ccorres_Catch) 1102 apply csymbr 1103 apply (rule ccorres_cond_true) 1104 apply (frule cap_get_tag_isCap_unfolded_H_cap(8)) 1105 apply simp 1106 apply (rule ccorres_rhs_assoc)+ 1107 apply csymbr+ 1108 apply (frule cap_get_tag_ReplyCap) 1109 apply (clarsimp simp: to_bool_def) 1110 apply (csymbr, csymbr) 1111 apply simp 1112 apply (rule ccorres_assert2) 1113 apply (fold dc_def) 1114 apply (rule ccorres_add_return2) 1115 apply (ctac (no_vcg)) 1116 apply (rule ccorres_return_void_catchbrk) 1117 apply (rule ccorres_return_void_C) 1118 apply wp 1119 apply (vcg exspec=doReplyTransfer_modifies) 1120 apply (rule ccorres_fail)+ 1121 apply simp_all 1122 apply (simp add: getSlotCap_def) 1123 apply (wp getCTE_wp')[1] 1124 apply vcg 1125 apply wp 1126 apply vcg 1127 apply clarsimp 1128 apply (intro allI conjI impI, 1129 simp_all add: cap_get_tag_isCap_unfolded_H_cap cap_tag_defs) 1130 apply (rule tcb_aligned', rule tcb_at_invs', simp) 1131 apply (auto simp: cte_wp_at_ctes_of valid_cap'_def 1132 dest!: ctes_of_valid')[1] 1133 apply (clarsimp simp: cte_wp_at_ctes_of isCap_simps) 1134 apply (simp add: real_cte_tcbCallerSlot[OF pred_tcb_at']) 1135 apply (clarsimp simp: cte_wp_at_ctes_of isCap_simps) 1136 apply clarsimp 1137 apply (frule cap_get_tag_isCap_unfolded_H_cap) 1138 apply (simp add: cap_get_tag_ReplyCap) 1139 apply clarsimp 1140 apply (frule cap_get_tag_isCap_unfolded_H_cap) 1141 apply (simp add: cap_get_tag_ReplyCap to_bool_def) 1142 done 1143 1144lemma deleteCallerCap_ccorres [corres]: 1145 "ccorres dc xfdc 1146 (\<lambda>s. invs' s \<and> tcb_at' receiver s) 1147 (UNIV \<inter> {s. receiver_' s = tcb_ptr_to_ctcb_ptr receiver}) 1148 [] 1149 (deleteCallerCap receiver) 1150 (Call deleteCallerCap_'proc)" 1151 apply (cinit lift: receiver_') 1152 apply (simp only: getThreadCallerSlot_def locateSlot_conv) 1153 apply (rule ccorres_move_array_assertion_tcb_ctes ccorres_Guard_Seq)+ 1154 apply (rule_tac P="\<lambda>_. is_aligned receiver tcbBlockSizeBits" and r'="\<lambda> a c. cte_Ptr a = c" 1155 and xf'="callerSlot_'" and P'=UNIV in ccorres_split_nothrow_novcg) 1156 apply (rule ccorres_from_vcg) 1157 apply (rule allI, rule conseqPre, vcg) 1158 apply (clarsimp simp: return_def word_sle_def) 1159 apply (frule is_aligned_neg_mask_eq) 1160 apply (simp add: mask_def tcbCallerSlot_def Kernel_C.tcbCaller_def 1161 cte_level_bits_def size_of_def) 1162 apply (drule ptr_val_tcb_ptr_mask2) 1163 apply (simp add: mask_def objBits_defs) 1164 apply ceqv 1165 apply (rule ccorres_symb_exec_l) 1166 apply (rule ccorres_symb_exec_l) 1167 apply (rule ccorres_symb_exec_r) 1168 apply (ctac add: cteDeleteOne_ccorres[where w="ucast cap_reply_cap"]) 1169 apply vcg 1170 apply (rule conseqPre, vcg, clarsimp simp: rf_sr_def 1171 gs_set_assn_Delete_cstate_relation[unfolded o_def]) 1172 apply (wp | simp)+ 1173 apply (simp add: getSlotCap_def) 1174 apply (wp getCTE_wp)+ 1175 apply clarsimp 1176 apply (simp add: guard_is_UNIV_def ghost_assertion_data_get_def 1177 ghost_assertion_data_set_def) 1178 apply (clarsimp simp: cte_wp_at_ctes_of cap_get_tag_isCap[symmetric] 1179 cap_tag_defs tcb_cnode_index_defs word_sle_def 1180 tcb_aligned') 1181 done 1182 1183 1184(* FIXME: MOVE *) 1185lemma cap_case_EndpointCap_NotificationCap: 1186 "(case cap of EndpointCap v0 v1 v2 v3 v4 \<Rightarrow> f v0 v1 v2 v3 v4 1187 | NotificationCap v0 v1 v2 v3 \<Rightarrow> g v0 v1 v2 v3 1188 | _ \<Rightarrow> h) 1189 = (if isEndpointCap cap 1190 then f (capEPPtr cap) (capEPBadge cap) (capEPCanSend cap) (capEPCanReceive cap) (capEPCanGrant cap) 1191 else if isNotificationCap cap 1192 then g (capNtfnPtr cap) (capNtfnBadge cap) (capNtfnCanSend cap) (capNtfnCanReceive cap) 1193 else h)" 1194 by (simp add: isCap_simps 1195 split: capability.split) 1196 1197 1198(* FIXME: MOVE *) 1199lemma capFaultOnFailure_if_case_sum: 1200 " (capFaultOnFailure epCPtr b (if c then f else g) >>= 1201 sum.case_sum (handleFault thread) return) = 1202 (if c then ((capFaultOnFailure epCPtr b f) 1203 >>= sum.case_sum (handleFault thread) return) 1204 else ((capFaultOnFailure epCPtr b g) 1205 >>= sum.case_sum (handleFault thread) return))" 1206 by (case_tac c, clarsimp, clarsimp) 1207 1208 1209 1210(* FIXME: MOVE to Corres_C.thy *) 1211lemma ccorres_trim_redundant_throw_break: 1212 "\<lbrakk>ccorres_underlying rf_sr \<Gamma> arrel axf arrel axf G G' (SKIP # hs) a c; 1213 \<And>s f. axf (global_exn_var_'_update f s) = axf s \<rbrakk> 1214 \<Longrightarrow> ccorres_underlying rf_sr \<Gamma> r xf arrel axf G G' (SKIP # hs) 1215 a (c;; Basic (global_exn_var_'_update (\<lambda>_. Break));; THROW)" 1216 apply - 1217 apply (rule ccorres_trim_redundant_throw') 1218 apply simp 1219 apply simp 1220 apply simp 1221 done 1222 1223lemma invs_valid_objs_strengthen: 1224 "invs' s \<longrightarrow> valid_objs' s" by fastforce 1225 1226lemma ct_not_ksQ_strengthen: 1227 "thread = ksCurThread s \<and> ksCurThread s \<notin> set (ksReadyQueues s p) \<longrightarrow> thread \<notin> set (ksReadyQueues s p)" by fastforce 1228 1229lemma option_to_ctcb_ptr_valid_ntfn: 1230 "valid_ntfn' ntfn s ==> (option_to_ctcb_ptr (ntfnBoundTCB ntfn) = NULL) = (ntfnBoundTCB ntfn = None)" 1231 apply (cases "ntfnBoundTCB ntfn", simp_all add: option_to_ctcb_ptr_def) 1232 apply (clarsimp simp: valid_ntfn'_def tcb_at_not_NULL) 1233 done 1234 1235 1236lemma deleteCallerCap_valid_ntfn'[wp]: 1237 "\<lbrace>\<lambda>s. valid_ntfn' x s\<rbrace> deleteCallerCap c \<lbrace>\<lambda>rv s. valid_ntfn' x s\<rbrace>" 1238 apply (wp hoare_vcg_ex_lift hoare_vcg_all_lift hoare_vcg_ball_lift hoare_vcg_imp_lift 1239 | simp add: valid_ntfn'_def split: ntfn.splits)+ 1240 apply auto 1241 done 1242 1243lemma hoare_vcg_imp_liftE: 1244 "\<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>" 1245 apply (simp add: validE_def valid_def split_def split: sum.splits) 1246 done 1247 1248 1249lemma not_obj_at'_ntfn: 1250 "(\<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)" 1251 apply (simp add: obj_at'_real_def projectKOs typ_at'_def ko_wp_at'_def objBits_simps) 1252 apply (rule iffI) 1253 apply (clarsimp) 1254 apply (case_tac ko) 1255 apply (clarsimp)+ 1256 done 1257 1258lemma handleRecv_ccorres: 1259 notes rf_sr_upd_safe[simp del] 1260 shows 1261 "ccorres dc xfdc 1262 (\<lambda>s. invs' s \<and> st_tcb_at' simple' (ksCurThread s) s 1263 \<and> sch_act_sane s \<and> (\<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))) 1264 {s. isBlocking_' s = from_bool isBlocking} 1265 [] 1266 (handleRecv isBlocking) 1267 (Call handleRecv_'proc)" 1268 apply (cinit lift: isBlocking_') 1269 apply (rule ccorres_pre_getCurThread) 1270 apply (ctac) 1271 apply (simp add: catch_def) 1272 apply (simp add: capFault_bindE) 1273 apply (simp add: bindE_bind_linearise) 1274 apply (rule_tac xf'=lu_ret___struct_lookupCap_ret_C_' 1275 in ccorres_split_nothrow_case_sum) 1276 apply (rule capFaultOnFailure_ccorres) 1277 apply (ctac add: lookupCap_ccorres) 1278 apply ceqv 1279 apply clarsimp 1280 apply (rule ccorres_Catch) 1281 apply csymbr 1282 apply (simp add: cap_get_tag_isCap del: Collect_const) 1283 apply (clarsimp simp: cap_case_EndpointCap_NotificationCap 1284 capFaultOnFailure_if_case_sum) 1285 apply (rule ccorres_cond_both' [where Q=\<top> and Q'=\<top>]) 1286 apply clarsimp 1287 apply (rule ccorres_rhs_assoc)+ 1288 apply csymbr 1289 apply (simp add: case_bool_If capFaultOnFailure_if_case_sum) 1290 apply (rule ccorres_if_cond_throws_break2 [where Q=\<top> and Q'=\<top>]) 1291 apply clarsimp 1292 apply (simp add: cap_get_tag_isCap[symmetric] cap_get_tag_EndpointCap 1293 del: Collect_const) 1294 apply (simp add: to_bool_def) 1295 apply (rule ccorres_rhs_assoc)+ 1296 apply (simp add: capFaultOnFailure_def rethrowFailure_def 1297 handleE'_def throwError_def) 1298 apply (rule ccorres_cross_over_guard[where P=\<top>]) 1299 apply (rule ccorres_symb_exec_r) 1300 apply (rule ccorres_cross_over_guard[where P=\<top>]) 1301 apply (rule ccorres_symb_exec_r) 1302 apply (rule ccorres_add_return2) 1303 apply (rule ccorres_split_nothrow_call[where xf'=xfdc and d'="\<lambda>_. break_C" 1304 and Q="\<lambda>_ _. True" and Q'="\<lambda>_ _. UNIV"]) 1305 apply (ctac add: handleFault_ccorres[unfolded dc_def]) 1306 apply simp+ 1307 apply ceqv 1308 apply (rule ccorres_break_return) 1309 apply simp+ 1310 apply wp 1311 apply (vcg exspec=handleFault_modifies) 1312 1313 apply vcg 1314 apply (rule conseqPre, vcg) 1315 apply (clarsimp simp: rf_sr_upd_safe) 1316 1317 apply vcg 1318 apply (rule conseqPre, vcg) 1319 apply (clarsimp simp: rf_sr_upd_safe) 1320 1321 apply (simp add: liftE_bind) 1322 apply (ctac) 1323 apply (rule_tac P="\<lambda>s. ksCurThread s = rv" in ccorres_cross_over_guard) 1324 apply (ctac add: receiveIPC_ccorres[unfolded dc_def]) 1325 1326 apply (wp deleteCallerCap_ksQ_ct' hoare_vcg_all_lift) 1327 apply (rule conseqPost[where Q'=UNIV and A'="{}"], vcg exspec=deleteCallerCap_modifies) 1328 apply (clarsimp dest!: rf_sr_ksCurThread) 1329 apply simp 1330 apply clarsimp 1331 apply (vcg exspec=handleFault_modifies) 1332 1333 apply (clarsimp simp: case_bool_If capFaultOnFailure_if_case_sum capFault_bindE) 1334 apply (simp add: liftE_bindE bind_bindE_assoc bind_assoc) 1335 apply (rule ccorres_cond_both' [where Q=\<top> and Q'=\<top>]) 1336 apply clarsimp 1337 1338 apply (rule ccorres_rhs_assoc)+ 1339 apply csymbr 1340 apply csymbr 1341 apply csymbr 1342 apply csymbr 1343 apply (rename_tac thread epCPtr rv rva ntfnptr) 1344 apply (rule_tac P="valid_cap' rv" in ccorres_cross_over_guard) 1345 apply (simp only: capFault_injection injection_handler_If injection_liftE 1346 injection_handler_throwError if_to_top_of_bind) 1347 apply csymbr 1348 apply (rule ccorres_abstract_cleanup) 1349 apply csymbr 1350 apply csymbr 1351 apply (rule ccorres_if_lhs) 1352 1353 apply (rule ccorres_pre_getNotification) 1354 apply (rename_tac ntfn) 1355 apply (rule_tac Q="valid_ntfn' ntfn and (\<lambda>s. thread = ksCurThread s)" 1356 and Q'="\<lambda>s. ret__unsigned_longlonga = ptr_val (option_to_ctcb_ptr (ntfnBoundTCB ntfn))" 1357 in ccorres_if_cond_throws_break2) 1358 apply (clarsimp simp: cap_get_tag_isCap[symmetric] cap_get_tag_NotificationCap 1359 option_to_ctcb_ptr_valid_ntfn rf_sr_ksCurThread) 1360 apply (auto simp: option_to_ctcb_ptr_def)[1] 1361 apply (rule ccorres_rhs_assoc)+ 1362 1363 apply (simp add: capFaultOnFailure_def rethrowFailure_def 1364 handleE'_def throwError_def) 1365 apply (rule ccorres_cross_over_guard[where P=\<top>]) 1366 apply (rule ccorres_symb_exec_r) 1367 apply (rule ccorres_cross_over_guard[where P=\<top>]) 1368 apply (rule ccorres_symb_exec_r) 1369 apply (rule ccorres_add_return2) 1370 apply (rule ccorres_split_nothrow_call[where xf'=xfdc and d'="\<lambda>_. break_C" 1371 and Q="\<lambda>_ _. True" and Q'="\<lambda>_ _. UNIV"]) 1372 apply (ctac add: handleFault_ccorres[unfolded dc_def]) 1373 apply simp+ 1374 apply ceqv 1375 apply (rule ccorres_break_return) 1376 apply simp+ 1377 apply wp 1378 apply (vcg exspec=handleFault_modifies) 1379 1380 apply vcg 1381 apply (rule conseqPre, vcg) 1382 apply (clarsimp simp: rf_sr_upd_safe) 1383 1384 apply vcg 1385 apply (rule conseqPre, vcg) 1386 apply (clarsimp simp: rf_sr_upd_safe) 1387 1388 apply (simp add: liftE_bind) 1389 apply (ctac add: receiveSignal_ccorres[unfolded dc_def]) 1390 apply clarsimp 1391 apply (vcg exspec=handleFault_modifies) 1392 apply (rule ccorres_cond_true_seq) 1393 apply (rule ccorres_split_throws) 1394 apply (rule ccorres_rhs_assoc)+ 1395 apply (simp add: capFaultOnFailure_def rethrowFailure_def 1396 handleE'_def throwError_def) 1397 apply (rule ccorres_cross_over_guard[where P=\<top>]) 1398 apply (rule ccorres_symb_exec_r) 1399 apply (rule ccorres_cross_over_guard[where P=\<top>]) 1400 apply (rule ccorres_symb_exec_r) 1401 apply (rule ccorres_add_return2) 1402 apply (ctac add: handleFault_ccorres[unfolded dc_def]) 1403 apply (rule ccorres_break_return[where P=\<top> and P'=UNIV]) 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 apply vcg 1412 apply (rule conseqPre, vcg) 1413 apply (clarsimp simp: rf_sr_upd_safe) 1414 apply (vcg exspec=handleFault_modifies) 1415 apply (simp add: capFaultOnFailure_def rethrowFailure_def 1416 handleE'_def throwError_def) 1417 1418 apply (rule ccorres_rhs_assoc)+ 1419 apply (rule ccorres_cross_over_guard[where P=\<top>]) 1420 apply (rule ccorres_symb_exec_r) 1421 apply (rule ccorres_cross_over_guard[where P=\<top>]) 1422 apply (rule ccorres_symb_exec_r) 1423 apply (ctac add: handleFault_ccorres[unfolded dc_def]) 1424 apply vcg 1425 apply (rule conseqPre, vcg) 1426 apply (clarsimp simp: rf_sr_upd_safe) 1427 apply vcg 1428 apply (rule conseqPre, vcg) 1429 apply (clarsimp simp: rf_sr_upd_safe) 1430 1431 apply clarsimp 1432 apply (rule ccorres_add_return2) 1433 apply (rule ccorres_rhs_assoc)+ 1434 apply (rule ccorres_cross_over_guard[where P=\<top>]) 1435 apply (rule ccorres_symb_exec_r) 1436 apply (ctac add: handleFault_ccorres[unfolded dc_def]) 1437 apply (rule ccorres_split_throws) 1438 apply (rule ccorres_return_void_C [unfolded dc_def]) 1439 apply vcg 1440 apply wp 1441 apply (vcg exspec=handleFault_modifies) 1442 apply vcg 1443 apply (rule conseqPre, vcg) 1444 apply (clarsimp simp: rf_sr_upd_safe) 1445 apply (wp) 1446 apply clarsimp 1447 apply (rename_tac thread epCPtr) 1448 apply (rule_tac Q'="(\<lambda>rv s. invs' s \<and> st_tcb_at' simple' thread s 1449 \<and> sch_act_sane s \<and> (\<forall>p. thread \<notin> set (ksReadyQueues s p)) \<and> thread = ksCurThread s 1450 \<and> valid_cap' rv s)" in hoare_post_imp_R[rotated]) 1451 apply (clarsimp simp: sch_act_sane_def) 1452 apply (auto dest!: obj_at_valid_objs'[OF _ invs_valid_objs'] 1453 simp: projectKOs valid_obj'_def, 1454 auto simp: pred_tcb_at'_def obj_at'_def objBits_simps projectKOs ct_in_state'_def)[1] 1455 apply wp 1456 apply clarsimp 1457 apply (vcg exspec=isBlocked_modifies exspec=lookupCap_modifies) 1458 1459 apply wp 1460 apply clarsimp 1461 apply vcg 1462 1463 apply (clarsimp simp add: sch_act_sane_def) 1464 apply (simp add: cap_get_tag_isCap[symmetric] del: rf_sr_upd_safe) 1465 apply (simp add: Kernel_C.capRegister_def X64_H.capRegister_def ct_in_state'_def 1466 X64.capRegister_def Kernel_C.RDI_def 1467 tcb_at_invs') 1468 apply (frule invs_valid_objs') 1469 apply (frule tcb_aligned'[OF tcb_at_invs']) 1470 apply clarsimp 1471 apply (intro conjI impI allI) 1472 apply (clarsimp simp: cfault_rel_def seL4_Fault_CapFault_lift 1473 lookup_fault_missing_capability_lift is_cap_fault_def)+ 1474 apply (clarsimp simp: cap_get_tag_NotificationCap) 1475 apply (rule cmap_relationE1[OF cmap_relation_ntfn], assumption, erule ko_at_projectKO_opt) 1476 apply (clarsimp simp: cnotification_relation_def Let_def) 1477 apply (clarsimp simp: cfault_rel_def seL4_Fault_CapFault_lift 1478 lookup_fault_missing_capability_lift is_cap_fault_def)+ 1479 apply (clarsimp simp: cap_get_tag_NotificationCap) 1480 apply (simp add: ccap_relation_def to_bool_def) 1481 apply (clarsimp simp: cap_get_tag_NotificationCap valid_cap'_def) 1482 apply (drule obj_at_ko_at', clarsimp) 1483 apply (rule cmap_relationE1[OF cmap_relation_ntfn], assumption, erule ko_at_projectKO_opt) 1484 apply (clarsimp simp: typ_heap_simps) 1485 apply (clarsimp simp: cfault_rel_def seL4_Fault_CapFault_lift 1486 lookup_fault_missing_capability_lift is_cap_fault_def)+ 1487 apply (case_tac w, clarsimp+) 1488 done 1489 1490lemma handleYield_ccorres: 1491 "ccorres dc xfdc 1492 (invs' and ct_active') 1493 UNIV 1494 [] 1495 (handleYield) 1496 (Call handleYield_'proc)" 1497 apply cinit 1498 apply (rule ccorres_pre_getCurThread) 1499 apply (ctac add: tcbSchedDequeue_ccorres) 1500 apply (ctac add: tcbSchedAppend_ccorres) 1501 apply (ctac add: rescheduleRequired_ccorres) 1502 apply (wp weak_sch_act_wf_lift_linear tcbSchedAppend_valid_objs') 1503 apply (vcg exspec= tcbSchedAppend_modifies) 1504 apply (wp weak_sch_act_wf_lift_linear tcbSchedDequeue_valid_queues) 1505 apply (vcg exspec= tcbSchedDequeue_modifies) 1506 apply (clarsimp simp: tcb_at_invs' invs_valid_objs' 1507 valid_objs'_maxPriority valid_objs'_maxDomain) 1508 apply (auto simp: obj_at'_def st_tcb_at'_def ct_in_state'_def valid_objs'_maxDomain) 1509 done 1510 1511 1512lemma getIRQState_sp: 1513 "\<lbrace>P\<rbrace> getIRQState irq \<lbrace>\<lambda>rv s. rv = intStateIRQTable (ksInterruptState s) irq \<and> P s\<rbrace>" 1514 apply (simp add: getIRQState_def getInterruptState_def) 1515 apply wp 1516 apply simp 1517 done 1518 1519lemma ccorres_pre_getIRQState: 1520 assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c" 1521 shows "ccorres r xf 1522 (\<lambda>s. irq \<le> ucast Kernel_C.maxIRQ \<and> P (intStateIRQTable (ksInterruptState s) irq) s) 1523 {s. \<forall>rv. index (intStateIRQTable_' (globals s)) (unat irq) = irqstate_to_C rv \<longrightarrow> s \<in> P' rv } 1524 hs (getIRQState irq >>= (\<lambda>rv. f rv)) c" 1525 apply (rule ccorres_guard_imp) 1526 apply (rule ccorres_symb_exec_l) 1527 defer 1528 apply (simp add: getIRQState_def getInterruptState_def) 1529 apply wp 1530 apply simp 1531 apply (rule getIRQState_sp) 1532 apply (simp add: getIRQState_def getInterruptState_def) 1533 apply assumption 1534 prefer 2 1535 apply (rule ccorres_guard_imp) 1536 apply (rule cc) 1537 apply simp 1538 apply assumption 1539 apply clarsimp 1540 apply (erule allE) 1541 apply (erule impE) 1542 prefer 2 1543 apply assumption 1544 apply (clarsimp simp: rf_sr_def cstate_relation_def 1545 Let_def cinterrupt_relation_def) 1546 done 1547 1548(* FIXME: move *) 1549lemma ccorres_ntfn_cases: 1550 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)" 1551 assumes Q: "\<not>isNotificationCap cap \<Longrightarrow> ccorres r xf (Q cap) (Q' cap) hs (a cap) (c cap)" 1552 shows 1553 "ccorres r xf (\<lambda>s. (\<forall>p b send d. cap = NotificationCap p b send d \<longrightarrow> P p b send d s) \<and> 1554 (\<not>isNotificationCap cap \<longrightarrow> Q cap s)) 1555 ({s. \<forall>p b send d. cap = NotificationCap p b send d \<longrightarrow> s \<in> P' p b send d} \<inter> 1556 {s. \<not>isNotificationCap cap \<longrightarrow> s \<in> Q' cap}) 1557 hs (a cap) (c cap)" 1558 apply (cases "isNotificationCap cap") 1559 apply (simp add: isCap_simps) 1560 apply (elim exE) 1561 apply (rule ccorres_guard_imp) 1562 apply (erule P) 1563 apply simp 1564 apply simp 1565 apply (rule ccorres_guard_imp) 1566 apply (erule Q) 1567 apply clarsimp 1568 apply clarsimp 1569 done 1570 1571(* FIXME: generalise the one in Interrupt_C *) 1572lemma getIRQSlot_ccorres2: 1573 "ccorres ((=) \<circ> Ptr) slot_' 1574 \<top> UNIV hs 1575 (getIRQSlot irq) (\<acute>slot :== CTypesDefs.ptr_add \<acute>intStateIRQNode (uint (ucast irq :: machine_word)))" 1576 apply (rule ccorres_from_vcg[where P=\<top> and P'=UNIV]) 1577 apply (rule allI, rule conseqPre, vcg) 1578 apply (clarsimp simp: getIRQSlot_def liftM_def getInterruptState_def 1579 locateSlot_conv) 1580 apply (simp add: simpler_gets_def bind_def return_def) 1581 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def 1582 cinterrupt_relation_def size_of_def 1583 cte_level_bits_def mult.commute mult.left_commute ucast_nat_def) 1584 done 1585 1586lemma getIRQSlot_ccorres3: 1587 "(\<And>rv. ccorresG rf_sr \<Gamma> r xf (P rv) (P' rv) hs (f rv) c) \<Longrightarrow> 1588 ccorresG rf_sr \<Gamma> r xf 1589 (\<lambda>s. P (intStateIRQNode (ksInterruptState s) + 2 ^ cte_level_bits * of_nat (unat irq)) s) 1590 {s. s \<in> P' (ptr_val (CTypesDefs.ptr_add (intStateIRQNode_' (globals s)) (uint (ucast irq :: machine_word))))} hs 1591 (getIRQSlot irq >>= f) c" 1592 apply (simp add: getIRQSlot_def locateSlot_conv liftM_def getInterruptState_def) 1593 apply (rule ccorres_symb_exec_l'[OF _ _ gets_sp]) 1594 apply (rule ccorres_guard_imp2, assumption) 1595 apply (clarsimp simp: getIRQSlot_ccorres_stuff 1596 objBits_simps cte_level_bits_def 1597 ucast_nat_def uint_ucast uint_up_ucast is_up) 1598 apply wp+ 1599 done 1600 1601lemma scast_maxIRQ_less_eq: 1602 fixes b :: irq 1603 shows "(Kernel_C.maxIRQ <s ucast b) = (scast Kernel_C.maxIRQ < b)" 1604 apply (clarsimp simp: Kernel_C.maxIRQ_def word_sless_def word_sle_def) 1605 apply (simp add: sint_ucast_eq_uint is_down_def target_size_def source_size_def word_size) 1606 apply uint_arith 1607 apply (auto simp: uint_up_ucast is_up_def target_size_def source_size_def word_size) 1608 done 1609 1610lemmas scast_maxIRQ_is_less = scast_maxIRQ_less_eq [THEN iffD1] 1611 1612lemma validIRQcastingLess: 1613 "Kernel_C.maxIRQ <s ucast b \<Longrightarrow> X64.maxIRQ < b" 1614 by (simp add: Platform_maxIRQ scast_maxIRQ_is_less is_up_def target_size source_size) 1615 1616lemma scast_maxIRQ_is_not_less: 1617 fixes b :: irq 1618 shows "\<not> Kernel_C.maxIRQ <s ucast b \<Longrightarrow> \<not> (scast Kernel_C.maxIRQ < b)" 1619 by (simp add: scast_maxIRQ_less_eq) 1620 1621(* FIXME ARMHYP: move *) 1622lemma ctzl_spec: 1623 "\<forall>s. \<Gamma> \<turnstile> {\<sigma>. s = \<sigma> \<and> x_' s \<noteq> 0} Call ctzl_'proc 1624 \<lbrace>\<acute>ret__long = of_nat (word_ctz (x_' s)) \<rbrace>" 1625 apply (rule allI, rule conseqPre, vcg) 1626 apply clarsimp 1627 apply (rule_tac x="ret__long_'_update f x" for f in exI) 1628 apply (simp add: mex_def meq_def) 1629 done 1630 1631lemma dmo_machine_valid_lift: 1632 "(\<And>s f m. P s = P (ksMachineState_update f s)) \<Longrightarrow> \<lbrace>P\<rbrace> doMachineOp f' \<lbrace>\<lambda>rv. P\<rbrace>" 1633 apply (wpsimp simp: split_def doMachineOp_def machine_op_lift_def machine_rest_lift_def in_monad) 1634 done 1635 1636lemma tcb_runnable_imp_simple: 1637 "obj_at' (\<lambda>s. runnable' (tcbState s)) t s \<Longrightarrow> obj_at' (\<lambda>s. simple' (tcbState s)) t s" 1638 apply (clarsimp simp: obj_at'_def) 1639 apply (case_tac "tcbState obj" ; clarsimp) 1640 done 1641 1642lemma ccorres_return_void_C_Seq: 1643 "ccorres_underlying sr \<Gamma> r rvxf arrel xf P P' hs X (return_void_C) \<Longrightarrow> 1644 ccorres_underlying sr \<Gamma> r rvxf arrel xf P P' hs X (return_void_C ;; Z)" 1645 apply (clarsimp simp: return_void_C_def) 1646 apply (erule ccorres_semantic_equiv0[rotated]) 1647 apply (rule semantic_equivI) 1648 apply (clarsimp simp: exec_assoc[symmetric]) 1649 apply (rule exec_Seq_cong, simp) 1650 apply (rule iffI) 1651 apply (auto elim!:exec_Normal_elim_cases intro: exec.Throw exec.Seq)[1] 1652 apply (auto elim!:exec_Normal_elim_cases intro: exec.Throw) 1653 done 1654 1655 1656lemma scast_specific_plus64: 1657 "scast (of_nat (word_ctz x) + 0x20 :: 64 signed word) = of_nat (word_ctz x) + (0x20 :: machine_word)" 1658 by (simp add: scast_down_add is_down_def target_size_def source_size_def word_size) 1659 1660lemma scast_specific_plus64_signed: 1661 "scast (of_nat (word_ctz x) + 0x20 :: machine_word) = of_nat (word_ctz x) + (0x20 :: 64 signed word)" 1662 by (simp add: scast_down_add is_down_def target_size_def source_size_def word_size) 1663 1664lemma ccorres_handleReservedIRQ: 1665 "ccorres dc xfdc 1666 (invs' and (\<lambda>s. irq \<in> non_kernel_IRQs \<longrightarrow> sch_act_not (ksCurThread s) s \<and> 1667 (\<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)))) 1668 (UNIV \<inter> {s. irq_' s = ucast irq}) hs 1669 (handleReservedIRQ irq) (Call handleReservedIRQ_'proc)" 1670 supply dc_simp[simp del] 1671 apply (cinit lift: irq_') 1672 apply (rule ccorres_return_Skip) 1673 apply clarsimp 1674 done 1675 1676lemma handleInterrupt_ccorres: 1677 "ccorres dc xfdc 1678 (invs' and (\<lambda>s. irq \<in> non_kernel_IRQs \<longrightarrow> sch_act_not (ksCurThread s) s \<and> 1679 (\<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)))) 1680 (UNIV \<inter> \<lbrace>\<acute>irq = ucast irq\<rbrace>) 1681 hs 1682 (handleInterrupt irq) 1683 (Call handleInterrupt_'proc)" 1684 apply (cinit lift: irq_' cong: call_ignore_cong) 1685 apply (rule ccorres_Cond_rhs_Seq) 1686 apply (simp add: Platform_maxIRQ del: Collect_const) 1687 apply (drule scast_maxIRQ_is_less[simplified]) 1688 apply (simp del: Collect_const) 1689 apply (rule ccorres_rhs_assoc)+ 1690 apply (subst doMachineOp_bind) 1691 apply (rule maskInterrupt_empty_fail) 1692 apply (rule ackInterrupt_empty_fail) 1693 apply (ctac add: maskInterrupt_ccorres[unfolded dc_def]) 1694 apply (subst bind_return_unit[where f="doMachineOp (ackInterrupt irq)"]) 1695 apply (ctac add: ackInterrupt_ccorres[unfolded dc_def]) 1696 apply (rule ccorres_split_throws) 1697 apply (rule ccorres_return_void_C[unfolded dc_def]) 1698 apply vcg 1699 apply wp 1700 apply (vcg exspec=ackInterrupt_modifies) 1701 apply wp 1702 apply (vcg exspec=maskInterrupt_modifies) 1703 apply (simp add: scast_maxIRQ_is_not_less Platform_maxIRQ del: Collect_const) 1704 apply (rule ccorres_pre_getIRQState) 1705 apply wpc 1706 apply simp 1707 apply (rule ccorres_fail) 1708 apply (simp add: bind_assoc cong: call_ignore_cong) 1709 apply (rule ccorres_move_const_guards)+ 1710 apply (rule ccorres_cond_true_seq) 1711 apply (rule ccorres_rhs_assoc)+ 1712 apply csymbr 1713 apply (rule getIRQSlot_ccorres3) 1714 apply (rule ccorres_getSlotCap_cte_at) 1715 apply (rule_tac P="cte_at' rv" in ccorres_cross_over_guard) 1716 apply (rule ptr_add_assertion_irq_guard[unfolded dc_def]) 1717 apply (rule ccorres_move_array_assertion_irq ccorres_move_c_guard_cte)+ 1718 apply ctac 1719 apply csymbr 1720 apply csymbr 1721 apply (rule ccorres_ntfn_cases) 1722 apply (clarsimp cong: call_ignore_cong simp del: Collect_const) 1723 apply (rule_tac b=send in ccorres_case_bools) 1724 apply simp 1725 apply (rule ccorres_cond_true_seq) 1726 apply (rule ccorres_rhs_assoc)+ 1727 apply csymbr 1728 apply csymbr 1729 apply (rule ccorres_cond_true_seq) 1730 apply (rule ccorres_rhs_assoc)+ 1731 apply csymbr 1732 apply csymbr 1733 apply (ctac (no_vcg) add: sendSignal_ccorres) 1734 apply (ctac (no_vcg) add: maskInterrupt_ccorres) 1735 apply (ctac add: ackInterrupt_ccorres [unfolded dc_def]) 1736 apply wp+ 1737 apply (simp del: Collect_const) 1738 apply (rule ccorres_cond_true_seq) 1739 apply (rule ccorres_rhs_assoc)+ 1740 apply csymbr+ 1741 apply (rule ccorres_cond_false_seq) 1742 apply simp 1743 apply (ctac (no_vcg) add: maskInterrupt_ccorres) 1744 apply (ctac add: ackInterrupt_ccorres [unfolded dc_def]) 1745 apply wp 1746 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) 1747 apply (clarsimp simp: isCap_simps simp del: Collect_const) 1748 apply (case_tac rva, simp_all del: Collect_const)[1] 1749 prefer 3 1750 apply metis 1751 apply ((rule ccorres_guard_imp2, 1752 rule ccorres_cond_false_seq, simp, 1753 rule ccorres_cond_false_seq, simp, 1754 ctac (no_vcg) add: maskInterrupt_ccorres, 1755 ctac (no_vcg) add: ackInterrupt_ccorres [unfolded dc_def], 1756 wp, simp)+) 1757 apply (wp getSlotCap_wp) 1758 apply simp 1759 apply vcg 1760 apply (simp add: bind_assoc) 1761 apply (rule ccorres_move_const_guards)+ 1762 apply (rule ccorres_cond_false_seq) 1763 apply (rule ccorres_cond_true_seq) 1764 apply (fold dc_def)[1] 1765 apply (rule ccorres_rhs_assoc)+ 1766 apply (ctac (no_vcg) add: timerTick_ccorres) 1767 apply (ctac (no_vcg) add: resetTimer_ccorres) 1768 apply (ctac add: ackInterrupt_ccorres ) 1769 apply wp+ 1770 apply (simp add: Platform_maxIRQ maxIRQ_def del: Collect_const) 1771 apply (rule ccorres_move_const_guards)+ 1772 apply (rule ccorres_cond_false_seq) 1773 apply (rule ccorres_cond_false_seq) 1774 apply (rule ccorres_cond_true_seq) 1775 apply (ctac add: ccorres_handleReservedIRQ) 1776 apply (ctac (no_vcg) add: ackInterrupt_ccorres [unfolded dc_def]) 1777 apply wp 1778 apply (vcg exspec=handleReservedIRQ_modifies) 1779 apply (simp add: sint_ucast_eq_uint is_down uint_up_ucast is_up ) 1780 apply (clarsimp simp: word_sless_alt word_less_alt word_le_def Kernel_C.maxIRQ_def 1781 uint_up_ucast is_up_def 1782 source_size_def target_size_def word_size 1783 sint_ucast_eq_uint is_down is_up word_0_sle_from_less) 1784 apply (rule conjI) 1785 apply (clarsimp simp: cte_wp_at_ctes_of non_kernel_IRQs_def) 1786 apply (clarsimp) 1787 apply (clarsimp simp: Kernel_C.IRQTimer_def Kernel_C.IRQSignal_def 1788 cte_wp_at_ctes_of ucast_ucast_b is_up) 1789 apply (intro conjI impI) 1790 apply clarsimp 1791 apply (erule(1) cmap_relationE1[OF cmap_relation_cte]) 1792 apply (clarsimp simp: typ_heap_simps') 1793 apply (simp add: cap_get_tag_isCap) 1794 apply (clarsimp simp: isCap_simps) 1795 apply (frule cap_get_tag_isCap_unfolded_H_cap) 1796 apply (frule cap_get_tag_to_H, assumption) 1797 apply (clarsimp simp: to_bool_def) 1798 apply (cut_tac un_ui_le[where b = 191 and a = irq, 1799 simplified word_size]) 1800 apply (simp add: ucast_eq_0 is_up_def source_size_def 1801 target_size_def word_size unat_gt_0 1802 | subst array_assertion_abs_irq[rule_format, OF conjI])+ 1803 apply (erule exE conjE)+ 1804 apply (erule(1) rf_sr_cte_at_valid[OF ctes_of_cte_at]) 1805 apply (clarsimp simp:nat_le_iff) 1806 apply (clarsimp simp: IRQReserved_def)+ 1807 done 1808end 1809 1810end 1811