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 SyscallArgs_C 12imports 13 TcbQueue_C 14 CSpace_RAB_C 15 StoreWord_C DetWP 16begin 17 18(*FIXME: arch_split: C kernel names hidden by Haskell names *) 19context kernel_m begin 20abbreviation "msgRegistersC \<equiv> kernel_all_substitute.msgRegisters" 21lemmas msgRegistersC_def = kernel_all_substitute.msgRegisters_def 22end 23 24context begin interpretation Arch . (*FIXME: arch_split*) 25 26declare word_neq_0_conv[simp del] 27 28definition 29 cintr :: "irq \<Rightarrow> machine_word \<Rightarrow> errtype \<Rightarrow> bool" 30where 31 "cintr a x err \<equiv> x = scast EXCEPTION_PREEMPTED" 32 33definition 34 replyOnRestart :: "machine_word \<Rightarrow> machine_word list \<Rightarrow> bool \<Rightarrow> unit kernel" 35where 36 "replyOnRestart thread reply isCall \<equiv> 37 do state \<leftarrow> getThreadState thread; 38 when (state = Restart) (do 39 _ \<leftarrow> when isCall (replyFromKernel thread (0, reply)); 40 setThreadState Running thread 41 od) 42 od" 43 44crunch typ_at'[wp]: replyOnRestart "\<lambda>s. P (typ_at' T p s)" 45 (wp: crunch_wps simp: crunch_simps) 46 47lemmas replyOnRestart_typ_ats[wp] = typ_at_lifts [OF replyOnRestart_typ_at'] 48 49lemma replyOnRestart_invs'[wp]: 50 "\<lbrace>invs'\<rbrace> replyOnRestart thread reply isCall \<lbrace>\<lambda>rv. invs'\<rbrace>" 51 including no_pre 52 apply (simp add: replyOnRestart_def) 53 apply (wp setThreadState_nonqueued_state_update rfk_invs' static_imp_wp) 54 apply (rule hoare_vcg_all_lift) 55 apply (wp setThreadState_nonqueued_state_update rfk_invs' hoare_vcg_all_lift rfk_ksQ) 56 apply (rule hoare_strengthen_post, rule gts_sp') 57 apply (clarsimp simp: pred_tcb_at') 58 apply (auto elim!: pred_tcb'_weakenE st_tcb_ex_cap'' 59 dest: st_tcb_at_idle_thread') 60 done 61 62 63declare psubset_singleton[simp] 64 65lemma gts_eq: 66 "st_tcb_at' (\<lambda>st. st = state) t s 67 \<Longrightarrow> (getThreadState t s = return state s)" 68 apply (simp add: prod_eq_iff return_def) 69 apply (subst conj_commute, rule context_conjI) 70 apply (rule no_failD[OF no_fail_getThreadState]) 71 apply (erule pred_tcb_at') 72 apply (rule not_psubset_eq) 73 apply clarsimp 74 apply (drule empty_failD [OF empty_fail_getThreadState]) 75 apply simp 76 apply clarsimp 77 apply (frule in_inv_by_hoareD[OF gts_inv']) 78 apply (drule use_valid [OF _ gts_sp', OF _ TrueI]) 79 apply (clarsimp simp: st_tcb_at'_def obj_at'_def projectKOs objBits_simps) 80 done 81 82lemma replyOnRestart_twice': 83 "((), s') \<in> fst (replyOnRestart t reply isCall s) 84 \<Longrightarrow> replyOnRestart t reply' isCall' s' 85 = return () s'" 86 apply (clarsimp simp add: replyOnRestart_def in_monad) 87 apply (drule use_valid [OF _ gts_sp', OF _ TrueI]) 88 apply (case_tac "state = Restart") 89 apply clarsimp 90 apply (drule use_valid [OF _ setThreadState_st_tcb'], simp) 91 apply (simp add: gts_eq when_def cong: bind_apply_cong) 92 apply (simp add: gts_eq when_def cong: bind_apply_cong) 93 done 94 95lemma replyOnRestart_twice[simplified]: 96 "do replyOnRestart t reply isCall; replyOnRestart t reply' isCall'; m od 97 = do replyOnRestart t reply isCall; m od" 98 apply (rule ext) 99 apply (rule bind_apply_cong[OF refl]) 100 apply simp 101 apply (subst bind_apply_cong [OF _ refl]) 102 apply (erule replyOnRestart_twice') 103 apply simp 104 done 105 106end 107 108context kernel_m begin 109 110lemma ccorres_pre_getWorkUnits: 111 assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c" 112 shows "ccorres r xf 113 (\<lambda>s. \<forall>rv. ksWorkUnitsCompleted s = rv \<longrightarrow> P rv s) 114 {s. \<forall>rv. s \<in> P' rv} hs (getWorkUnits >>= f) c" 115 apply (simp add: getWorkUnits_def) 116 apply (rule ccorres_guard_imp) 117 apply (rule ccorres_symb_exec_l) 118 defer 119 apply wp[1] 120 apply (rule gets_sp) 121 apply (clarsimp simp: empty_fail_def simpler_gets_def) 122 apply assumption 123 apply clarsimp 124 defer 125 apply (rule ccorres_guard_imp) 126 apply (rule cc) 127 apply clarsimp 128 apply assumption 129 apply clarsimp 130 done 131 132lemma preemptionPoint_ccorres: 133 "ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') 134 invs' UNIV [] 135 preemptionPoint (Call preemptionPoint_'proc)" 136 apply (cinit simp: workUnitsLimit_def whenE_def) 137 apply (rule ccorres_liftE_Seq) 138 apply (rule ccorres_split_nothrow 139 [where P=\<top> and P'=UNIV and r'=dc and xf'=xfdc]) 140 apply (rule ccorres_from_vcg) 141 apply (rule allI, rule conseqPre, vcg) 142 apply (clarsimp simp: modifyWorkUnits_def simpler_modify_def) 143 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def 144 carch_state_relation_def 145 cmachine_state_relation_def) 146 apply ceqv 147 apply (rule ccorres_liftE_Seq) 148 apply (rule ccorres_pre_getWorkUnits) 149 apply (rule ccorres_cond_seq) 150 apply (rule_tac R="\<lambda>s. rv = ksWorkUnitsCompleted s" in ccorres_cond2) 151 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def) 152 prefer 2 153 apply simp 154 apply (rule ccorres_from_vcg_throws [where P=\<top> and P'=UNIV]) 155 apply (rule allI, rule conseqPre, vcg) 156 apply (simp add: returnOk_def return_def) 157 apply (rule ccorres_liftE_Seq) 158 apply (rule ccorres_rhs_assoc)+ 159 apply (rule ccorres_split_nothrow 160 [where P=\<top> and P'=UNIV and r'=dc and xf'=xfdc]) 161 apply (rule ccorres_from_vcg) 162 apply (rule allI, rule conseqPre, vcg) 163 apply (thin_tac "P" for P)+ 164 apply (clarsimp simp: setWorkUnits_def simpler_modify_def) 165 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def 166 carch_state_relation_def 167 cmachine_state_relation_def) 168 apply ceqv 169 apply (rule ccorres_liftE_Seq) 170 apply (ctac (no_vcg) add: isIRQPending_ccorres) 171 apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV]) 172 apply (rule allI, rule conseqPre, vcg) 173 apply (simp add: from_bool_0 whenE_def returnOk_def throwError_def 174 return_def split: option.splits) 175 apply (clarsimp simp: cintr_def exception_defs) 176 apply wp+ 177 apply vcg 178 apply (unfold modifyWorkUnits_def)[1] 179 apply wp 180 apply vcg 181 apply simp 182 done 183 184definition 185 "invocationCatch thread isBlocking isCall inject 186 \<equiv> 187 sum.case_sum (throwError \<circ> Inl) 188 (\<lambda>oper. doE y \<leftarrow> liftE (setThreadState Structures_H.thread_state.Restart thread); 189 reply \<leftarrow> RetypeDecls_H.performInvocation isBlocking isCall (inject oper) 190 >>= sum.case_sum (throwError \<circ> Inr) returnOk; 191 liftE (if reply = [] then replyOnRestart thread [] isCall \<sqinter> return () 192 else replyOnRestart thread reply isCall) 193 odE)" 194 195definition 196 "intr_and_se_rel seOrIRQ status err 197 \<equiv> case seOrIRQ of Inl se \<Rightarrow> syscall_error_rel se status err 198 | Inr irq \<Rightarrow> cintr irq status err" 199 200lemma intr_and_se_rel_simps[simp]: 201 "intr_and_se_rel (Inl se) = syscall_error_rel se" 202 "intr_and_se_rel (Inr irq) = cintr irq" 203 by (rule ext | simp add: intr_and_se_rel_def)+ 204 205lemma errstate_globals_overwrite[simp]: 206 "errstate (s \<lparr> globals := globals t \<rparr>) = errstate t" 207 by (simp add: errstate_def) 208 209definition 210 array_to_list :: "('a['b :: finite]) \<Rightarrow> 'a list" 211where 212 "array_to_list arr \<equiv> map (index arr) ([0 ..< card (UNIV :: 'b set)])" 213 214definition 215 interpret_excaps :: "extra_caps_C \<Rightarrow> cte_C ptr list" 216where 217 "interpret_excaps excps \<equiv> 218 (takeWhile (\<lambda>x. ptr_val x \<noteq> 0) 219 (array_to_list (excaprefs_C excps)))" 220 221lemma interpret_excaps_test_null[unfolded array_to_list_def, simplified]: 222 "\<lbrakk> length (interpret_excaps excps) \<ge> n; 223 n < length (array_to_list (excaprefs_C excps)) \<rbrakk> 224 \<Longrightarrow> (index (excaprefs_C excps) n = NULL) = (length (interpret_excaps excps) = n)" 225 apply (simp add: interpret_excaps_def) 226 apply (rule iffI) 227 apply (erule order_antisym[rotated]) 228 apply (rule length_takeWhile_le) 229 apply (simp add: array_to_list_def) 230 apply simp 231 apply (drule length_takeWhile_ge) 232 apply (simp add: array_to_list_def NULL_ptr_val) 233 done 234 235definition 236 excaps_map :: "(capability \<times> machine_word) list 237 \<Rightarrow> cte_C ptr list" 238where 239 "excaps_map \<equiv> map (\<lambda>(cp, slot). cte_Ptr slot)" 240 241definition 242 slotcap_in_mem :: "capability \<Rightarrow> machine_word 243 \<Rightarrow> cte_heap \<Rightarrow> bool" 244where 245 "slotcap_in_mem cap slot 246 \<equiv> \<lambda>cte_heap. \<exists>cte. cte_heap slot = Some cte \<and> cap = cteCap cte" 247 248lemma slotcap_in_mem_def2: 249 "slotcap_in_mem cap slot (ctes_of s) 250 = cte_wp_at' (\<lambda>cte. cap = cteCap cte) slot s" 251 by (simp add: slotcap_in_mem_def cte_wp_at_ctes_of) 252 253definition 254 excaps_in_mem :: "(capability \<times> machine_word) list 255 \<Rightarrow> cte_heap \<Rightarrow> bool" 256where 257 "excaps_in_mem cps \<equiv> \<lambda>cte_heap. 258 \<forall>(cp, slot) \<in> set cps. slotcap_in_mem cp slot cte_heap" 259 260 261lemma ccorres_alternative1: 262 "ccorres rvr xf P P' hs f c 263 \<Longrightarrow> ccorres rvr xf P P' hs (f \<sqinter> g) c" 264 apply (simp add: ccorres_underlying_def) 265 apply (erule ballEI, clarsimp del: allI) 266 apply (simp add: alternative_def) 267 apply (elim allEI) 268 apply (auto simp: alternative_def split: xstate.split_asm) 269 done 270 271lemma ccorres_alternative2: 272 "ccorres rvr xf P P' hs g c 273 \<Longrightarrow> ccorres rvr xf P P' hs (f \<sqinter> g) c" 274 apply (simp add: ccorres_underlying_def) 275 apply (erule ballEI, clarsimp del: allI) 276 apply (simp add: alternative_def) 277 apply (elim allEI) 278 apply (auto simp: alternative_def split: xstate.split_asm) 279 done 280 281lemma o_xo_injector: 282 "((f o f') \<currency> r) = ((f \<currency> r) o case_sum (Inl o f') Inr)" 283 by (intro ext, simp split: sum.split) 284 285lemma ccorres_invocationCatch_Inr: 286 "ccorres (f \<currency> r) xf P P' hs 287 (invocationCatch thread isBlocking isCall injector (Inr v)) c 288 = 289 ccorres ((f \<circ> Inr) \<currency> r) xf P P' hs 290 (do _ \<leftarrow> setThreadState Restart thread; 291 doE reply \<leftarrow> performInvocation isBlocking isCall (injector v); 292 if reply = [] then liftE (replyOnRestart thread [] isCall) \<sqinter> returnOk () 293 else liftE (replyOnRestart thread reply isCall) 294 odE od) c" 295 apply (simp add: invocationCatch_def liftE_bindE o_xo_injector) 296 apply (subst ccorres_liftM_simp[symmetric]) 297 apply (simp add: liftM_def bind_assoc bindE_def) 298 apply (rule_tac f="\<lambda>f. ccorres rvr xs P P' hs f c" for rvr xs in arg_cong) 299 apply (rule ext) 300 apply (rule bind_apply_cong [OF refl])+ 301 apply (simp add: throwError_bind returnOk_bind lift_def liftE_def 302 alternative_bind 303 split: sum.split if_split) 304 apply (simp add: throwError_def) 305 done 306 307lemma getSlotCap_eq: 308 "slotcap_in_mem cap slot (ctes_of s) 309 \<Longrightarrow> getSlotCap slot s = return cap s" 310 apply (clarsimp simp: slotcap_in_mem_def2 getSlotCap_def) 311 apply (frule cte_wp_at_weakenE'[OF _ TrueI]) 312 apply (drule no_failD[OF no_fail_getCTE]) 313 apply (clarsimp simp: cte_wp_at'_def getCTE_def[symmetric] 314 bind_def return_def) 315 done 316 317lemma getSlotCap_ccorres_fudge: 318 "ccorres_underlying sr Gamm rvr xf ar axf P Q hs (do rv \<leftarrow> getSlotCap slot; _ \<leftarrow> assert (rv = cp); a rv od) c 319 \<Longrightarrow> ccorres_underlying sr Gamm rvr xf ar axf 320 (P and (slotcap_in_mem cp slot o ctes_of)) 321 Q hs (a cp) c" 322 apply (simp add: ccorres_underlying_def) 323 apply (erule ballEI, clarsimp del: allI) 324 apply (simp add: bind_apply_cong [OF getSlotCap_eq refl] 325 cong: xstate.case_cong) 326 done 327 328lemma getSlotCap_ccorres_fudge_n: 329 "ccorres_underlying sr Gamm rvr xf ar axf P Q hs 330 (do rv \<leftarrow> getSlotCap (snd (vals ! n)); 331 _ \<leftarrow> assert (rv = fst (vals ! n)); a od) c 332 \<Longrightarrow> ccorres_underlying sr Gamm rvr xf ar axf 333 ((\<lambda>s. cte_wp_at' (\<lambda>cte. cteCap cte = fst (vals ! n)) 334 (snd (vals ! n)) s \<longrightarrow> P s) 335 and (excaps_in_mem vals \<circ> ctes_of) and K (n < length vals)) Q 336 hs a c" 337 apply (rule ccorres_guard_imp2) 338 apply (erule getSlotCap_ccorres_fudge) 339 apply (clarsimp simp: excaps_in_mem_def) 340 apply (drule bspec, erule nth_mem) 341 apply (clarsimp simp: slotcap_in_mem_def cte_wp_at_ctes_of) 342 done 343 344definition 345 "is_syscall_error_code f code 346 = (\<forall>Q. (\<Gamma> \<turnstile> {s. global_exn_var_'_update (\<lambda>_. Return) 347 (ret__unsigned_long_'_update (\<lambda>_. scast EXCEPTION_SYSCALL_ERROR) 348 (globals_update (current_syscall_error_'_update f) s)) \<in> Q} 349 code {}, Q))" 350 351abbreviation(input) 352 (* no longer needed *) 353 "Basic_with_globals f == (Basic f)" 354 355lemma is_syscall_error_codes: 356 "is_syscall_error_code f 357 (Basic (globals_update (current_syscall_error_'_update f));; 358 return_C ret__unsigned_long_'_update (\<lambda>_. scast EXCEPTION_SYSCALL_ERROR))" 359 "is_syscall_error_code (f' o f) 360 (Basic (globals_update (current_syscall_error_'_update f));; 361 Basic (globals_update (current_syscall_error_'_update f'));; 362 return_C ret__unsigned_long_'_update (\<lambda>_. scast EXCEPTION_SYSCALL_ERROR))" 363 "is_syscall_error_code (f'' o f' o f) 364 (Basic (globals_update (current_syscall_error_'_update f));; 365 Basic (globals_update (current_syscall_error_'_update f'));; 366 Basic (globals_update (current_syscall_error_'_update f''));; 367 return_C ret__unsigned_long_'_update (\<lambda>_. scast EXCEPTION_SYSCALL_ERROR))" 368 "is_syscall_error_code f 369 (SKIP;; 370 Basic (globals_update (current_syscall_error_'_update f));; 371 return_C ret__unsigned_long_'_update (\<lambda>_. scast EXCEPTION_SYSCALL_ERROR))" 372 "is_syscall_error_code (f' o f) 373 (SKIP;; 374 Basic (globals_update (current_syscall_error_'_update f));; 375 Basic (globals_update (current_syscall_error_'_update f'));; 376 return_C ret__unsigned_long_'_update (\<lambda>_. scast EXCEPTION_SYSCALL_ERROR))" 377 "is_syscall_error_code (f'' o f' o f) 378 (SKIP;; 379 Basic (globals_update (current_syscall_error_'_update f));; 380 Basic (globals_update (current_syscall_error_'_update f'));; 381 Basic (globals_update (current_syscall_error_'_update f''));; 382 return_C ret__unsigned_long_'_update (\<lambda>_. scast EXCEPTION_SYSCALL_ERROR))" 383 "is_syscall_error_code f 384 (Basic_with_globals (globals_update (current_syscall_error_'_update f));; 385 return_C ret__unsigned_long_'_update (\<lambda>_. scast EXCEPTION_SYSCALL_ERROR))" 386 "is_syscall_error_code (f' o f) 387 (Basic_with_globals (globals_update (current_syscall_error_'_update f));; 388 Basic_with_globals (globals_update (current_syscall_error_'_update f'));; 389 return_C ret__unsigned_long_'_update (\<lambda>_. scast EXCEPTION_SYSCALL_ERROR))" 390 "is_syscall_error_code (f'' o f' o f) 391 (Basic_with_globals (globals_update (current_syscall_error_'_update f));; 392 Basic_with_globals (globals_update (current_syscall_error_'_update f'));; 393 Basic_with_globals (globals_update (current_syscall_error_'_update f''));; 394 return_C ret__unsigned_long_'_update (\<lambda>_. scast EXCEPTION_SYSCALL_ERROR))" 395 "is_syscall_error_code (f'''' \<circ> f''' \<circ> f'' o f' o f) 396 ( 397 Basic_with_globals (globals_update (current_syscall_error_'_update f));; 398 Basic_with_globals (globals_update (current_syscall_error_'_update f'));; 399 Basic_with_globals (globals_update (current_syscall_error_'_update f''));; 400 Basic_with_globals (globals_update (current_syscall_error_'_update f'''));; 401 Basic_with_globals (globals_update (current_syscall_error_'_update f''''));; 402 return_C ret__unsigned_long_'_update (\<lambda>_. scast EXCEPTION_SYSCALL_ERROR))" 403 "is_syscall_error_code f 404 (SKIP;; 405 Basic_with_globals (globals_update (current_syscall_error_'_update f));; 406 return_C ret__unsigned_long_'_update (\<lambda>_. scast EXCEPTION_SYSCALL_ERROR))" 407 "is_syscall_error_code (f' o f) 408 (SKIP;; 409 Basic_with_globals (globals_update (current_syscall_error_'_update f));; 410 Basic_with_globals (globals_update (current_syscall_error_'_update f'));; 411 return_C ret__unsigned_long_'_update (\<lambda>_. scast EXCEPTION_SYSCALL_ERROR))" 412 "is_syscall_error_code (f'' o f' o f) 413 (SKIP;; 414 Basic_with_globals (globals_update (current_syscall_error_'_update f));; 415 Basic_with_globals (globals_update (current_syscall_error_'_update f'));; 416 Basic_with_globals (globals_update (current_syscall_error_'_update f''));; 417 return_C ret__unsigned_long_'_update (\<lambda>_. scast EXCEPTION_SYSCALL_ERROR))" 418 by ((rule iffD2[OF is_syscall_error_code_def], intro allI, 419 rule conseqPre, vcg, safe, (simp_all add: o_def)?)+) 420 421lemma syscall_error_throwError_ccorres_direct: 422 "\<lbrakk> is_syscall_error_code f code; 423 \<And>err' ft'. syscall_error_to_H (f err') ft' = Some err \<rbrakk> 424 \<Longrightarrow> 425 ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id v' ret__unsigned_long_') 426 \<top> (UNIV) (SKIP # hs) 427 (throwError (Inl err)) code" 428 apply (rule ccorres_from_vcg_throws) 429 apply (rule allI, rule conseqPre) 430 apply (erule iffD1[OF is_syscall_error_code_def, THEN spec]) 431 apply (clarsimp simp: throwError_def return_def) 432 apply (simp add: syscall_error_rel_def exception_defs) 433 done 434 435lemma syscall_error_throwError_ccorres_succs: 436 "\<lbrakk> is_syscall_error_code f code; 437 \<And>err' ft'. syscall_error_to_H (f err') ft' = Some err \<rbrakk> 438 \<Longrightarrow> 439 ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id v' ret__unsigned_long_') 440 \<top> (UNIV) (SKIP # hs) 441 (throwError (Inl err)) (code ;; remainder)" 442 apply (rule ccorres_guard_imp2, 443 rule ccorres_split_throws) 444 apply (erule syscall_error_throwError_ccorres_direct) 445 apply simp 446 apply (rule HoarePartialProps.augment_Faults) 447 apply (erule iffD1[OF is_syscall_error_code_def, THEN spec]) 448 apply simp+ 449 done 450 451lemmas syscall_error_throwError_ccorres_n = 452 is_syscall_error_codes[THEN syscall_error_throwError_ccorres_direct, 453 simplified o_apply] 454 is_syscall_error_codes[THEN syscall_error_throwError_ccorres_succs, 455 simplified o_apply] 456 457definition idButNot :: "'a \<Rightarrow> 'a" 458where "idButNot x = x" 459 460lemma interpret_excaps_test_null2: 461 "n < 3 \<Longrightarrow> 462 (index (excaprefs_C excps) n = NULL) 463 = (length (interpret_excaps excps) \<le> n 464 \<and> index (idButNot excaprefs_C excps) n = NULL)" 465 unfolding idButNot_def 466 apply safe 467 apply (rule ccontr, simp only: linorder_not_le) 468 apply (frule(1) interpret_excaps_test_null [OF order_less_imp_le]) 469 apply simp 470 done 471 472lemma interpret_excaps_eq[unfolded array_to_list_def, simplified]: 473 "interpret_excaps excps = xs \<Longrightarrow> 474 \<forall>n < length xs. (index (excaprefs_C excps) n) = (xs ! n) 475 \<and> (length xs < length (array_to_list (excaprefs_C excps)) 476 \<longrightarrow> index (excaprefs_C excps) (length xs) = NULL)" 477 apply (clarsimp simp: interpret_excaps_def) 478 apply (drule length_takeWhile_gt) 479 apply (clarsimp simp: nth_append) 480 apply (clarsimp simp: array_to_list_def) 481 apply (frule_tac f=length in arg_cong, subst(asm) length_map, 482 simp(no_asm_use)) 483 apply (rule conjI) 484 apply (rule trans, erule map_upt_eq_vals_D, simp) 485 apply (simp add: nth_append) 486 apply clarsimp 487 apply (frule nth_length_takeWhile) 488 apply (rule trans, erule map_upt_eq_vals_D, simp) 489 apply (simp add: nth_append NULL_ptr_val) 490 done 491 492lemma ctes_of_0_contr[elim]: 493 "\<lbrakk> ctes_of s 0 = Some cte; valid_mdb' s \<rbrakk> \<Longrightarrow> P" 494 by (drule(1) ctes_of_not_0, simp) 495 496lemma invocationCatch_use_injection_handler: 497 "(v >>= invocationCatch thread isBlocking isCall injector) 498 = (injection_handler Inl v >>=E 499 (invocationCatch thread isBlocking isCall injector o Inr))" 500 apply (simp add: injection_handler_def handleE'_def 501 bind_bindE_assoc) 502 apply (rule ext, rule bind_apply_cong [OF refl]) 503 apply (simp add: invocationCatch_def return_returnOk 504 split: sum.split) 505 done 506 507lemma injection_handler_returnOk: 508 "injection_handler injector (returnOk v) = returnOk v" 509 by (simp add: returnOk_liftE injection_liftE) 510 511lemma injection_handler_If: 512 "injection_handler injector (If P a b) 513 = If P (injection_handler injector a) 514 (injection_handler injector b)" 515 by (simp split: if_split) 516 517(* FIXME: duplicated in CSpace_All *) 518lemma injection_handler_liftM: 519 "injection_handler f 520 = liftM (\<lambda>v. case v of Inl ex \<Rightarrow> Inl (f ex) | Inr rv \<Rightarrow> Inr rv)" 521 apply (intro ext, simp add: injection_handler_def liftM_def 522 handleE'_def) 523 apply (rule bind_apply_cong, rule refl) 524 apply (simp add: throwError_def split: sum.split) 525 done 526 527lemma injection_handler_throwError: 528 "injection_handler f (throwError v) = throwError (f v)" 529 by (simp add: injection_handler_def handleE'_def 530 throwError_bind) 531 532lemma injection_handler_whenE: 533 "injection_handler injf (whenE P f) 534 = whenE P (injection_handler injf f)" 535 by (simp add: whenE_def injection_handler_returnOk split: if_split) 536 537lemmas injection_handler_bindE = injection_bindE [OF refl refl] 538lemmas injection_handler_wp = injection_wp [OF refl] 539 540lemma ccorres_injection_handler_csum1: 541 "ccorres (f \<currency> r) xf P P' hs a c 542 \<Longrightarrow> ccorres 543 ((\<lambda>rv a b. \<exists>rv'. rv = injector rv' \<and> f rv' a b) \<currency> r) xf P P' hs 544 (injection_handler injector a) c" 545 apply (simp add: injection_handler_liftM) 546 apply (erule ccorres_rel_imp) 547 apply (auto split: sum.split) 548 done 549 550lemma ccorres_injection_handler_csum2: 551 "ccorres ((f o injector) \<currency> r) xf P P' hs a c 552 \<Longrightarrow> ccorres (f \<currency> r) xf P P' hs 553 (injection_handler injector a) c" 554 apply (simp add: injection_handler_liftM) 555 apply (erule ccorres_rel_imp) 556 apply (auto split: sum.split) 557 done 558 559definition 560 is_nondet_refinement :: "('a, 's) nondet_monad 561 \<Rightarrow> ('a, 's) nondet_monad \<Rightarrow> bool" 562where 563 "is_nondet_refinement f g \<equiv> \<forall>s. (snd (f s) \<longrightarrow> snd (g s)) \<and> fst (f s) \<subseteq> fst (g s)" 564 565lemma is_nondet_refinement_refl[simp]: 566 "is_nondet_refinement a a" 567 by (simp add: is_nondet_refinement_def) 568 569lemma is_nondet_refinement_bind: 570 "\<lbrakk> is_nondet_refinement a c; \<And>rv. is_nondet_refinement (b rv) (d rv) \<rbrakk> 571 \<Longrightarrow> is_nondet_refinement (a >>= b) (c >>= d)" 572 apply (clarsimp simp: is_nondet_refinement_def bind_def split_def) 573 apply fast 574 done 575 576lemma is_nondet_refinement_bindE: 577 "\<lbrakk> is_nondet_refinement a c; \<And>rv. is_nondet_refinement (b rv) (d rv) \<rbrakk> 578 \<Longrightarrow> is_nondet_refinement (a >>=E b) (c >>=E d)" 579 apply (simp add: bindE_def) 580 apply (erule is_nondet_refinement_bind) 581 apply (simp add: lift_def split: sum.split) 582 done 583 584lemma ccorres_nondet_refinement: 585 "\<lbrakk> is_nondet_refinement a b; 586 ccorres_underlying sr Gamm rvr xf arrel axf G G' hs a c \<rbrakk> 587 \<Longrightarrow> ccorres_underlying sr Gamm rvr xf arrel axf G G' hs b c" 588 apply (simp add: ccorres_underlying_def is_nondet_refinement_def 589 split_def) 590 apply (rule ballI, drule(1) bspec) 591 apply (intro impI) 592 apply (drule mp, blast) 593 apply (elim allEI) 594 apply (clarsimp split: xstate.split_asm) 595 apply blast 596 done 597 598lemma is_nondet_refinement_alternative1: 599 "is_nondet_refinement a (a \<sqinter> b)" 600 by (clarsimp simp add: is_nondet_refinement_def alternative_def) 601 602lemma ccorres_defer: 603 assumes c: "ccorres r xf P P' hs H C" 604 assumes f: "no_fail Q H" 605 shows "ccorres (\<lambda>_. r rv) xf (\<lambda>s. P s \<and> Q s \<and> (P s \<and> Q s \<longrightarrow> fst (H s) = {(rv,s)})) P' hs (return ()) C" 606 using c 607 apply (clarsimp simp: ccorres_underlying_def split: xstate.splits) 608 apply (drule (1) bspec) 609 apply clarsimp 610 apply (erule impE) 611 apply (insert f)[1] 612 apply (clarsimp simp: no_fail_def) 613 apply (clarsimp simp: return_def) 614 apply (rule conjI) 615 apply clarsimp 616 apply (rename_tac s) 617 apply (erule_tac x=n in allE) 618 apply (erule_tac x="Normal s" in allE) 619 apply (clarsimp simp: unif_rrel_def) 620 apply fastforce 621 done 622 623lemma no_fail_loadWordUser: 624 "no_fail (pointerInUserData x and K (is_aligned x 3)) (loadWordUser x)" 625 apply (simp add: loadWordUser_def) 626 apply (rule no_fail_pre, wp no_fail_stateAssert) 627 apply simp 628 done 629 630lemma no_fail_getMRs: 631 "no_fail (tcb_at' thread and case_option \<top> valid_ipc_buffer_ptr' buffer) 632 (getMRs thread buffer info)" 633 apply (rule det_wp_no_fail) 634 apply (rule det_wp_getMRs) 635 done 636 637lemma nat_less_4_cases: 638 "(x::nat) < 4 \<Longrightarrow> x=0 \<or> x=1 \<or> x=2 \<or> x=3" 639 by clarsimp 640 641lemma msgRegisters_scast: 642 "n < unat (scast n_msgRegisters :: machine_word) \<Longrightarrow> 643 unat (scast (index msgRegistersC n)::machine_word) = unat (index msgRegistersC n)" 644 apply (simp add: kernel_all_global_addresses.msgRegisters_def fupdate_def update_def n_msgRegisters_def fcp_beta 645 Kernel_C.R10_def Kernel_C.R8_def Kernel_C.R9_def Kernel_C.R15_def) 646 by (auto dest!: nat_less_4_cases) 647 648lemma asUser_cur_obj_at': 649 assumes f: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>" 650 shows "\<lbrace>\<lambda>s. obj_at' (\<lambda>tcb. P (atcbContextGet (tcbArch tcb))) (ksCurThread s) s \<and> t = ksCurThread s\<rbrace> 651 asUser t f \<lbrace>\<lambda>rv s. obj_at' (\<lambda>tcb. Q rv (atcbContextGet (tcbArch tcb))) (ksCurThread s) s\<rbrace>" 652 apply (simp add: asUser_def split_def) 653 apply (wp) 654 apply (rule hoare_lift_Pf2 [where f=ksCurThread]) 655 apply (wp threadSet_obj_at'_really_strongest)+ 656 apply (clarsimp simp: threadGet_def) 657 apply (wp getObject_tcb_wp) 658 apply clarsimp 659 apply (drule obj_at_ko_at') 660 apply clarsimp 661 apply (rename_tac tcb) 662 apply (rule_tac x=tcb in exI) 663 apply clarsimp 664 apply (drule use_valid, rule f, assumption) 665 apply clarsimp 666 done 667 668lemma asUser_const_rv: 669 assumes f: "\<lbrace>\<lambda>s. P\<rbrace> f \<lbrace>\<lambda>rv s. Q rv\<rbrace>" 670 shows "\<lbrace>\<lambda>s. P\<rbrace> asUser t f \<lbrace>\<lambda>rv s. Q rv\<rbrace>" 671 apply (simp add: asUser_def split_def) 672 apply (wp) 673 apply (clarsimp simp: threadGet_def) 674 apply (wp getObject_tcb_wp) 675 apply clarsimp 676 apply (drule obj_at_ko_at') 677 apply clarsimp 678 apply (rename_tac tcb) 679 apply (rule_tac x=tcb in exI) 680 apply clarsimp 681 apply (drule use_valid, rule f, assumption) 682 apply clarsimp 683 done 684 685lemma getMRs_tcbContext: 686 "\<lbrace>\<lambda>s. n < unat n_msgRegisters \<and> n < unat (msgLength info) \<and> thread = ksCurThread s \<and> cur_tcb' s\<rbrace> 687 getMRs thread buffer info 688 \<lbrace>\<lambda>rv s. obj_at' (\<lambda>tcb. user_regs (atcbContextGet (tcbArch tcb)) (X64_H.msgRegisters ! n) = rv ! n) (ksCurThread s) s\<rbrace>" 689 apply (rule hoare_assume_pre) 690 apply (elim conjE) 691 apply (thin_tac "thread = t" for t) 692 apply (clarsimp simp add: getMRs_def) 693 apply (wp|wpc)+ 694 apply (rule_tac P="n < length x" in hoare_gen_asm) 695 apply (clarsimp simp: nth_append) 696 apply (wp mapM_wp' static_imp_wp)+ 697 apply simp 698 apply (rule asUser_cur_obj_at') 699 apply (simp add: getRegister_def msgRegisters_unfold) 700 apply (simp add: mapM_Cons bind_assoc mapM_empty) 701 apply wp 702 apply (wp hoare_drop_imps hoare_vcg_all_lift) 703 apply (wp asUser_cur_obj_at') 704 apply (simp add: getRegister_def msgRegisters_unfold) 705 apply (simp add: mapM_Cons bind_assoc mapM_empty) 706 apply (wp asUser_const_rv) 707 apply clarsimp 708 apply (wp asUser_const_rv) 709 apply (clarsimp simp: n_msgRegisters_def msgRegisters_unfold) 710 apply (simp add: nth_Cons' cur_tcb'_def split: if_split) 711 done 712 713lemma threadGet_tcbIpcBuffer_ccorres [corres]: 714 "ccorres (=) w_bufferPtr_' (tcb_at' tptr) UNIV hs 715 (threadGet tcbIPCBuffer tptr) 716 (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t tcb_ptr_to_ctcb_ptr tptr\<rbrace> 717 (\<acute>w_bufferPtr :== 718 h_val (hrs_mem \<acute>t_hrs) 719 (Ptr &(tcb_ptr_to_ctcb_ptr tptr\<rightarrow>[''tcbIPCBuffer_C''])::machine_word ptr)))" 720 apply (rule ccorres_guard_imp2) 721 apply (rule ccorres_add_return2) 722 apply (rule ccorres_pre_threadGet) 723 apply (rule_tac P = "obj_at' (\<lambda>tcb. tcbIPCBuffer tcb = x) tptr" and 724 P'="{s'. \<exists>ctcb. 725 cslift s' (tcb_ptr_to_ctcb_ptr tptr) = Some ctcb \<and> 726 tcbIPCBuffer_C ctcb = x }" in ccorres_from_vcg) 727 apply (rule allI, rule conseqPre, vcg) 728 apply clarsimp 729 apply (clarsimp simp: return_def typ_heap_simps') 730 apply (clarsimp simp: obj_at'_def ctcb_relation_def) 731 done 732 733(* FIXME: move *) 734lemma ccorres_case_bools: 735 assumes P: "ccorres r xf P P' hs (a True) (c True)" 736 assumes Q: "ccorres r xf Q Q' hs (a False) (c False)" 737 shows "ccorres r xf (\<lambda>s. (b \<longrightarrow> P s) \<and> (\<not>b \<longrightarrow> Q s)) 738 ({s. b \<longrightarrow> s \<in> P'} \<inter> {s. \<not>b \<longrightarrow> s \<in> Q'}) 739 hs (a b) (c b)" 740 apply (cases b) 741 apply (auto simp: P Q) 742 done 743 744lemma ccorres_cond_both': 745 assumes abs: "\<forall>s s'. (s, s') \<in> sr \<and> Q s \<and> Q' s' \<longrightarrow> P = (s' \<in> P')" 746 and ac: "P \<Longrightarrow> ccorres_underlying sr G r xf arrel axf R R' hs a c" 747 and bd: "\<not> P \<Longrightarrow> ccorres_underlying sr G r xf arrel axf U U' hs b d" 748 shows "ccorres_underlying sr G r xf arrel axf 749 (Q and (\<lambda>s. P \<longrightarrow> R s) and (\<lambda>s. \<not> P \<longrightarrow> U s)) 750 (Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')}) 751 hs 752 (if P then a else b) (Cond P' c d)" 753 apply (rule ccorres_guard_imp2) 754 apply (rule ccorres_if_lhs) 755 apply (rule ccorres_cond_true) 756 apply (erule ac) 757 apply (rule ccorres_cond_false) 758 apply (erule bd) 759 apply clarsimp 760 apply (frule abs[rule_format, OF conjI], simp+) 761 done 762 763lemma pageBitsForSize_32 [simp]: 764 "pageBitsForSize sz < 64" 765 by (cases sz, auto simp: bit_simps) 766 767lemma ccap_relation_frame_tags: 768 "ccap_relation (ArchObjectCap (PageCap v0 v1 mt v2 dev v3)) cap \<Longrightarrow> 769 cap_get_tag cap = scast cap_frame_cap" 770 by (auto simp: cap_get_tag_isCap_unfolded_H_cap) 771 772(* FIXME: move *) 773lemma ccorres_case_bools': 774 assumes P: "b \<Longrightarrow> ccorres r xf P P' hs (a True) (c True)" 775 assumes Q: "\<not> b \<Longrightarrow> ccorres r xf Q Q' hs (a False) (c False)" 776 shows "ccorres r xf (\<lambda>s. (b \<longrightarrow> P s) \<and> (\<not>b \<longrightarrow> Q s)) 777 ({s. b \<longrightarrow> s \<in> P'} \<inter> {s. \<not>b \<longrightarrow> s \<in> Q'}) 778 hs (a b) (c b)" 779 apply (cases b) 780 apply (auto simp: P Q) 781 done 782 783(* FIXME x64: does this need vmrights \<noteq> 0 *) 784lemma capFVMRights_range: 785 "\<And>cap. cap_get_tag cap = scast cap_frame_cap \<Longrightarrow> 786 cap_frame_cap_CL.capFVMRights_CL (cap_frame_cap_lift cap) \<le> 3" 787 by (simp add: cap_frame_cap_lift_def 788 cap_lift_def cap_tag_defs word_and_le1 mask_def)+ 789 790lemma dumb_bool_for_all: "(\<forall>x. x) = False" 791 by auto 792 793lemma dumb_bool_split_for_vcg: 794 "\<lbrace>d \<longrightarrow> \<acute>ret__unsigned_long \<noteq> 0\<rbrace> \<inter> \<lbrace>\<not> d \<longrightarrow> \<acute>ret__unsigned_long = 0\<rbrace> 795 = \<lbrace>d = to_bool \<acute>ret__unsigned_long \<rbrace>" 796 by (auto simp: to_bool_def) 797 798lemma ccap_relation_page_is_device: 799 "ccap_relation (capability.ArchObjectCap (arch_capability.PageCap v0a v1 mt v2 d v3)) c 800 \<Longrightarrow> (cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift c) \<noteq> 0) = d" 801 apply (clarsimp simp: ccap_relation_def Let_def map_option_Some_eq2 cap_to_H_def) 802 apply (case_tac z) 803 apply (auto split: if_splits simp: to_bool_def Let_def cap_frame_cap_lift_def) 804 done 805 806lemma lookupIPCBuffer_ccorres[corres]: 807 "ccorres ((=) \<circ> option_to_ptr) ret__ptr_to_unsigned_long_' 808 (tcb_at' t) 809 (UNIV \<inter> {s. thread_' s = tcb_ptr_to_ctcb_ptr t} 810 \<inter> {s. isReceiver_' s = from_bool isReceiver}) [] 811 (lookupIPCBuffer isReceiver t) (Call lookupIPCBuffer_'proc)" 812 apply (cinit lift: thread_' isReceiver_') 813 apply (rule ccorres_split_nothrow) 814 apply simp 815 apply (rule threadGet_tcbIpcBuffer_ccorres) 816 apply ceqv 817 apply (simp add: getThreadBufferSlot_def locateSlot_conv 818 cte_C_size word_sle_def Collect_True 819 del: Collect_const) 820 apply ccorres_remove_UNIV_guard 821 apply (rule ccorres_getSlotCap_cte_at) 822 apply (rule ccorres_move_array_assertion_tcb_ctes) 823 apply (ctac (no_vcg)) 824 apply csymbr 825 apply (rule_tac b="isArchObjectCap rva \<and> isPageCap (capCap rva)" in ccorres_case_bools') 826 apply simp 827 apply (rule ccorres_cond_false_seq) 828 apply (simp(no_asm)) 829 apply csymbr 830 apply (rule_tac b="isDeviceCap rva" in ccorres_case_bools') 831 apply (rule ccorres_cond_true_seq) 832 apply (rule ccorres_from_vcg_split_throws[where P=\<top> and P'=UNIV]) 833 apply vcg 834 apply (rule conseqPre, vcg, 835 clarsimp simp: isCap_simps return_def option_to_ptr_def option_to_0_def) 836 apply (rule ccorres_cond_false_seq) 837 apply simp 838 apply csymbr 839 apply csymbr 840 apply (clarsimp simp: isCap_simps) 841 apply (rule ccorres_guard_imp[where A=\<top> and A'=UNIV], 842 rule ccorres_cond [where R=\<top>]) 843 apply (clarsimp simp: from_bool_0 isCap_simps) 844 apply (frule cap_get_tag_isCap_unfolded_H_cap) 845 apply (clarsimp simp: cap_frame_cap_lift cap_to_H_def elim!: ccap_relationE) 846 apply (clarsimp simp: vmrights_to_H_def) 847 apply (simp add: Kernel_C.VMReadOnly_def Kernel_C.VMKernelOnly_def 848 Kernel_C.VMReadWrite_def 849 split: if_split) 850 apply (frule cap_get_tag_isCap_unfolded_H_cap(18),simp) 851 apply (frule capFVMRights_range) thm pageBitsForSize_spec 852 apply (simp add: cap_frame_cap_lift) 853 apply (clarsimp simp: cap_to_H_def vmrights_to_H_def to_bool_def 854 word_le_make_less 855 Kernel_C.VMReadWrite_def Kernel_C.VMReadOnly_def 856 Kernel_C.VMKernelOnly_def 857 dest: word_less_cases) 858 apply (rule ccorres_rhs_assoc)+ 859 apply csymbr 860 apply csymbr 861 apply csymbr 862 apply csymbr 863 apply csymbr 864 apply csymbr 865 apply (rule ccorres_Guard) 866 apply simp 867 apply (rule ccorres_assert)+ 868 apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws) 869 apply (rule allI, rule conseqPre, vcg) 870 apply (clarsimp simp: return_def option_to_ptr_def option_to_0_def isCap_simps) 871 apply (frule cap_get_tag_isCap_unfolded_H_cap) 872 apply (clarsimp simp: cap_frame_cap_lift cap_to_H_def mask_def elim!: ccap_relationE) 873 apply (ctac add: ccorres_return_C) 874 apply clarsimp 875 apply (frule cap_get_tag_isCap_unfolded_H_cap) 876 apply (clarsimp simp: if_1_0_0 Collect_const_mem isCap_simps word_less_nat_alt 877 option_to_ptr_def from_bool_0 option_to_0_def ccap_relation_def 878 c_valid_cap_def cl_valid_cap_def cap_frame_cap_lift) 879 apply (rule ccorres_cond_true_seq) 880 apply simp 881 apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws) 882 apply (rule allI, rule conseqPre, vcg) 883 apply (clarsimp simp: return_def option_to_ptr_def option_to_0_def isCap_simps 884 dumb_bool_for_all 885 split: capability.splits arch_capability.splits bool.splits) 886 apply wpsimp 887 apply (clarsimp simp: if_1_0_0 Collect_const_mem) 888 apply (rule conjI) 889 apply (clarsimp simp: isCap_simps word_less_nat_alt ) 890 apply (frule ccap_relation_page_is_device) 891 apply (frule ccap_relation_frame_tags) 892 apply clarsimp 893 apply (rule ccontr) 894 apply clarsimp 895 apply (fastforce simp: cap_get_tag_PageCap_frame 896 isCap_simps) 897 apply wp 898 apply vcg 899 apply (simp add: word_sle_def Collect_const_mem 900 tcb_cnode_index_defs tcbSlots cte_level_bits_def 901 size_of_def) 902 done 903 904 905lemma doMachineOp_pointerInUserData: 906 "\<lbrace>pointerInUserData p\<rbrace> doMachineOp m \<lbrace>\<lambda>rv. pointerInUserData p\<rbrace>" 907 by (simp add: pointerInUserData_def) wp 908 909lemma loadWordUser_wp: 910 "\<lbrace>\<lambda>s. is_aligned p 3 \<and> (\<forall>v. user_word_at v p s \<longrightarrow> P v s)\<rbrace> 911 loadWordUser p 912 \<lbrace>P\<rbrace>" 913 apply (simp add: loadWordUser_def loadWord_def stateAssert_def 914 user_word_at_def valid_def upto0_7_def) 915 apply (clarsimp simp: in_monad in_doMachineOp) 916 done 917 918lemma ccorres_pre_loadWordUser: 919 "(\<And>rv. ccorres r xf (P rv) (Q rv) hs (a rv) c) \<Longrightarrow> 920 ccorres r xf (valid_pspace' and K (is_aligned ptr 3) and 921 (\<lambda>s. \<forall>v. user_word_at v ptr s \<longrightarrow> P v s)) 922 {s. \<forall>v. cslift s (Ptr ptr :: machine_word ptr) = Some v \<longrightarrow> 923 s \<in> Q v} hs 924 (loadWordUser ptr >>= a) c" 925 apply (rule ccorres_guard_imp) 926 apply (rule_tac Q="\<lambda>rv. P rv and user_word_at rv ptr" and Q'=Q in 927 ccorres_symb_exec_l [OF _ loadWordUser_inv loadWordUser_wp]) 928 apply (fastforce intro: ccorres_guard_imp) 929 apply simp 930 apply simp 931 apply clarsimp 932 apply (drule(1) user_word_at_cross_over, simp) 933 apply (clarsimp simp: typ_heap_simps h_t_valid_clift_Some_iff) 934 done 935 936lemma loadWordUser_user_word_at: 937 "\<lbrace>\<lambda>s. \<forall>rv. user_word_at rv x s \<longrightarrow> Q rv s\<rbrace> loadWordUser x \<lbrace>Q\<rbrace>" 938 apply (simp add: loadWordUser_def user_word_at_def 939 doMachineOp_def split_def) 940 apply wp 941 apply (clarsimp simp: pointerInUserData_def 942 loadWord_def in_monad 943 is_aligned_mask upto0_7_def) 944 done 945 946lemma mapM_loadWordUser_user_words_at: 947 "\<lbrace>\<lambda>s. \<forall>rv. (\<forall>x < length xs. user_word_at (rv ! x) (xs ! x) s) 948 \<and> length rv = length xs \<longrightarrow> Q rv s\<rbrace> 949 mapM loadWordUser xs \<lbrace>Q\<rbrace>" 950 apply (induct xs arbitrary: Q) 951 apply (simp add: mapM_def sequence_def) 952 apply wp 953 apply (simp add: mapM_Cons) 954 apply wp 955 apply assumption 956 apply (wp loadWordUser_user_word_at) 957 apply clarsimp 958 apply (drule spec, erule mp) 959 apply clarsimp 960 apply (case_tac x) 961 apply simp 962 apply simp 963 done 964 965 966lemma getMRs_user_word: 967 "\<lbrace>\<lambda>s. valid_ipc_buffer_ptr' buffer s \<and> i < msgLength info 968 \<and> msgLength info \<le> msgMaxLength \<and> i >= scast n_msgRegisters\<rbrace> 969 getMRs thread (Some buffer) info 970 \<lbrace>\<lambda>xs. user_word_at (xs ! unat i) (buffer + (i * 8 + 8))\<rbrace>" 971 apply (rule hoare_assume_pre) 972 apply (elim conjE) 973 apply (thin_tac "valid_ipc_buffer_ptr' x y" for x y) 974 apply (simp add: getMRs_def) 975 apply wp 976 apply (rule_tac P="length hardwareMRValues = unat n_msgRegisters" in hoare_gen_asm) 977 apply (clarsimp simp: nth_append word_le_nat_alt 978 word_less_nat_alt word_size 979 linorder_not_less [symmetric]) 980 apply (wp mapM_loadWordUser_user_words_at) 981 apply (wp hoare_vcg_all_lift) 982 apply (rule_tac Q="\<lambda>_. \<top>" in hoare_strengthen_post) 983 apply wp 984 apply clarsimp 985 defer 986 apply simp 987 apply (wp asUser_const_rv) 988 apply (simp add: msgRegisters_unfold n_msgRegisters_def) 989 apply (erule_tac x="unat i - unat n_msgRegisters" in allE) 990 apply (erule impE) 991 apply (simp add: msgRegisters_unfold 992 msgMaxLength_def msgLengthBits_def n_msgRegisters_def) 993 apply (drule (1) order_less_le_trans) 994 apply (simp add: word_less_nat_alt word_le_nat_alt) 995 apply (simp add: msgRegisters_unfold 996 msgMaxLength_def msgLengthBits_def n_msgRegisters_def) 997 apply (simp add: upto_enum_word del: upt_rec_numeral) 998 apply (subst (asm) nth_map) 999 apply (simp del: upt_rec_numeral) 1000 apply (drule (1) order_less_le_trans) 1001 apply (simp add: word_less_nat_alt word_le_nat_alt) 1002 apply (subst (asm) nth_upt) 1003 apply simp 1004 apply (drule (1) order_less_le_trans) 1005 apply (simp add: word_less_nat_alt word_le_nat_alt) 1006 apply (simp add: word_le_nat_alt add.commute add.left_commute mult.commute mult.left_commute 1007 wordSize_def') 1008 done 1009 1010declare if_split [split] 1011 1012definition 1013 "getMRs_rel args buffer \<equiv> \<lambda>s. \<exists>mi. msgLength mi \<le> msgMaxLength \<and> fst (getMRs (ksCurThread s) buffer mi s) = {(args, s)}" 1014 1015definition 1016 "sysargs_rel args buffer \<equiv> 1017 cur_tcb' 1018 and case_option \<top> valid_ipc_buffer_ptr' buffer 1019 and getMRs_rel args buffer 1020 and (\<lambda>_. length args > unat (scast n_msgRegisters :: machine_word) \<longrightarrow> buffer \<noteq> None)" 1021 1022definition 1023 "sysargs_rel_n args buffer n \<equiv> \<lambda>s. n < length args \<and> (unat (scast n_msgRegisters :: machine_word) \<le> n \<longrightarrow> buffer \<noteq> None)" 1024 1025lemma sysargs_rel_to_n: 1026 "sysargs_rel args buffer s \<Longrightarrow> sysargs_rel_n args buffer n s = (n < length args)" 1027 by (auto simp add: sysargs_rel_def sysargs_rel_n_def) 1028 1029lemma getMRs_rel: 1030 "\<lbrace>\<lambda>s. msgLength mi \<le> msgMaxLength \<and> thread = ksCurThread s \<and> 1031 case_option \<top> valid_ipc_buffer_ptr' buffer s \<and> 1032 cur_tcb' s\<rbrace> 1033 getMRs thread buffer mi \<lbrace>\<lambda>args. getMRs_rel args buffer\<rbrace>" 1034 apply (simp add: getMRs_rel_def) 1035 apply (rule hoare_pre) 1036 apply (rule_tac x=mi in hoare_vcg_exI) 1037 apply wp 1038 apply (rule_tac Q="\<lambda>rv s. thread = ksCurThread s \<and> fst (getMRs thread buffer mi s) = {(rv,s)}" in hoare_strengthen_post) 1039 apply (wp det_result det_wp_getMRs) 1040 apply clarsimp 1041 apply (clarsimp simp: cur_tcb'_def) 1042 done 1043 1044lemma length_msgRegisters: 1045 "length X64_H.msgRegisters = unat (scast n_msgRegisters :: machine_word)" 1046 by (simp add: msgRegisters_unfold n_msgRegisters_def) 1047 1048lemma getMRs_len[simplified]: 1049 "\<lbrace>\<top>\<rbrace> getMRs thread buffer mi \<lbrace>\<lambda>args s. length args > unat (scast n_msgRegisters :: machine_word) \<longrightarrow> buffer \<noteq> None\<rbrace>" 1050 apply (simp add: getMRs_def) 1051 apply (cases buffer, simp_all add:hoare_TrueI) 1052 apply (wp asUser_const_rv | simp)+ 1053 apply (simp add: length_msgRegisters) 1054 done 1055 1056lemma getMRs_sysargs_rel: 1057 "\<lbrace>(\<lambda>s. thread = ksCurThread s) and cur_tcb' and case_option \<top> valid_ipc_buffer_ptr' buffer and K (msgLength mi \<le> msgMaxLength)\<rbrace> 1058 getMRs thread buffer mi \<lbrace>\<lambda>args. sysargs_rel args buffer\<rbrace>" 1059 apply (simp add: sysargs_rel_def) 1060 apply (wp getMRs_rel getMRs_len|simp)+ 1061 done 1062 1063lemma ccorres_assume_pre: 1064 assumes "\<And>s. P s \<Longrightarrow> ccorres r xf (P and (\<lambda>s'. s' = s)) P' hs H C" 1065 shows "ccorres r xf P P' hs H C" 1066 apply (clarsimp simp: ccorres_underlying_def) 1067 apply (frule assms) 1068 apply (simp add: ccorres_underlying_def) 1069 apply blast 1070 done 1071 1072lemma getMRs_length: 1073 "\<lbrace>\<lambda>s. msgLength mi \<le> msgMaxLength\<rbrace> getMRs thread buffer mi 1074 \<lbrace>\<lambda>args s. if buffer = None then length args = min (unat (scast n_msgRegisters :: machine_word)) (unat (msgLength mi)) 1075 else length args = unat (msgLength mi)\<rbrace>" 1076 apply (cases buffer) 1077 apply (simp add: getMRs_def) 1078 apply (rule hoare_pre, wp) 1079 apply (rule asUser_const_rv) 1080 apply simp 1081 apply (wp mapM_length) 1082 apply (simp add: min_def length_msgRegisters) 1083 apply clarsimp 1084 apply (simp add: getMRs_def) 1085 apply (rule hoare_pre, wp) 1086 apply simp 1087 apply (wp mapM_length asUser_const_rv mapM_length)+ 1088 apply (clarsimp simp: length_msgRegisters) 1089 apply (simp add: min_def split: if_splits) 1090 apply (clarsimp simp: word_le_nat_alt) 1091 apply (simp add: msgMaxLength_def msgLengthBits_def n_msgRegisters_def) 1092 done 1093 1094lemma index_msgRegisters_less': 1095 "n < 4 \<Longrightarrow> index msgRegistersC n < 0x17" 1096 by (simp add: msgRegistersC_def fupdate_def Arrays.update_def 1097 fcp_beta "StrictC'_register_defs") 1098 1099lemma index_msgRegisters_less: 1100 "n < 4 \<Longrightarrow> index msgRegistersC n <s 0x17" 1101 "n < 4 \<Longrightarrow> index msgRegistersC n < 0x17" 1102 using index_msgRegisters_less' 1103 by (simp_all add: word_sless_msb_less) 1104 1105lemma valid_ipc_buffer_ptr_array: 1106 "valid_ipc_buffer_ptr' (ptr_val p) s \<Longrightarrow> (s, s') \<in> rf_sr 1107 \<Longrightarrow> n \<le> 2 ^ (msg_align_bits - 3) 1108 \<Longrightarrow> n \<noteq> 0 1109 \<Longrightarrow> array_assertion (p :: machine_word ptr) n (hrs_htd (t_hrs_' (globals s')))" 1110 apply (clarsimp simp: valid_ipc_buffer_ptr'_def typ_at_to_obj_at_arches) 1111 apply (drule obj_at_ko_at', clarsimp) 1112 apply (drule rf_sr_heap_user_data_relation) 1113 apply (erule cmap_relationE1) 1114 apply (clarsimp simp: heap_to_user_data_def Let_def) 1115 apply (rule conjI, rule exI, erule ko_at_projectKO_opt) 1116 apply (rule refl) 1117 apply (drule clift_field, rule user_data_C_words_C_fl_ti, simp) 1118 apply (erule clift_array_assertion_imp, simp+) 1119 apply (simp add: field_lvalue_def msg_align_bits) 1120 apply (rule_tac x="unat (ptr_val p && mask pageBits >> 3)" in exI, 1121 simp add: word_shift_by_3 shiftr_shiftl1 1122 is_aligned_andI1[OF is_aligned_weaken]) 1123 apply (simp add: add.commute word_plus_and_or_coroll2) 1124 apply (cut_tac a="(ptr_val p && mask pageBits ) >> 3" 1125 and b="2 ^ (pageBits - 3) - 2 ^ (msg_align_bits - 3)" in unat_le_helper) 1126 apply (simp add: pageBits_def msg_align_bits mask_def is_aligned_mask) 1127 apply word_bitwise 1128 apply simp 1129 apply (simp add: msg_align_bits pageBits_def) 1130 done 1131 1132lemma array_assertion_valid_ipc_buffer_ptr_abs: 1133 "\<forall>s s'. (s, s') \<in> rf_sr \<and> (valid_ipc_buffer_ptr' (ptr_val (p s)) s) 1134 \<and> (n s' \<le> 2 ^ (msg_align_bits - 3) \<and> (x s' \<noteq> 0 \<longrightarrow> n s' \<noteq> 0)) 1135 \<longrightarrow> (x s' = 0 \<or> array_assertion (p s :: machine_word ptr) (n s') (hrs_htd (t_hrs_' (globals s'))))" 1136 apply (intro allI impI disjCI2, clarsimp) 1137 apply (erule(1) valid_ipc_buffer_ptr_array, simp_all) 1138 done 1139 1140lemmas ccorres_move_array_assertion_ipc_buffer 1141 = ccorres_move_array_assertions [OF array_assertion_valid_ipc_buffer_ptr_abs] 1142 1143lemma getSyscallArg_ccorres_foo: 1144 "ccorres (\<lambda>a rv. rv = args ! n) ret__unsigned_long_' 1145 (sysargs_rel args buffer and sysargs_rel_n args buffer n) 1146 (UNIV \<inter> \<lbrace>unat \<acute>i = n\<rbrace> \<inter> \<lbrace>\<acute>ipc_buffer = option_to_ptr buffer\<rbrace>) [] 1147 (return ()) (Call getSyscallArg_'proc)" 1148 apply (rule ccorres_assume_pre) 1149 apply (subst (asm) sysargs_rel_def) 1150 apply (subst (asm) getMRs_rel_def) 1151 apply (subst (asm) pred_conj_def)+ 1152 apply (elim conjE exE) 1153 apply (cinit lift: i_' ipc_buffer_') 1154 apply (fold return_def) 1155 apply (rule_tac H="do thread \<leftarrow> gets ksCurThread; getMRs thread buffer mi od" in ccorres_defer) 1156 prefer 2 1157 apply (rule no_fail_pre, wp no_fail_getMRs) 1158 apply assumption 1159 apply (rule ccorres_cond_seq) 1160 apply (rule_tac R=\<top> and P="\<lambda>_. n < unat (scast n_msgRegisters :: machine_word)" in ccorres_cond_both) 1161 apply (simp add: word_less_nat_alt split: if_split) 1162 apply (rule ccorres_add_return2) 1163 apply (rule ccorres_symb_exec_l) 1164 apply (rule_tac P="\<lambda>s. n < unat (scast n_msgRegisters :: machine_word) \<and> 1165 obj_at' (\<lambda>tcb. user_regs (atcbContextGet (tcbArch tcb)) 1166 (X64_H.msgRegisters!n) = x!n) (ksCurThread s) s" 1167 and P' = UNIV 1168 in ccorres_from_vcg_split_throws) 1169 apply vcg 1170 apply (simp add: return_def del: Collect_const) 1171 apply (rule conseqPre, vcg) 1172 apply (clarsimp simp: rf_sr_ksCurThread) 1173 apply (drule (1) obj_at_cslift_tcb) 1174 apply (clarsimp simp: typ_heap_simps' msgRegisters_scast) 1175 apply (clarsimp simp: ctcb_relation_def ccontext_relation_def 1176 msgRegisters_ccorres atcbContextGet_def 1177 carch_tcb_relation_def cregs_relation_def) 1178 apply (subst (asm) msgRegisters_ccorres) 1179 apply (clarsimp simp: n_msgRegisters_def) 1180 apply (simp add: n_msgRegisters_def word_less_nat_alt) 1181 apply (simp add: index_msgRegisters_less unat_less_helper) 1182 apply wp[1] 1183 apply (wp getMRs_tcbContext) 1184 apply simp 1185 apply (rule ccorres_seq_skip [THEN iffD2]) 1186 apply (rule ccorres_add_return2) 1187 apply (rule ccorres_symb_exec_l) 1188 apply (rule_tac P="\<lambda>s. user_word_at (x!n) (ptr_val (CTypesDefs.ptr_add ipc_buffer (of_nat n + 1))) s 1189 \<and> valid_ipc_buffer_ptr' (ptr_val ipc_buffer) s \<and> n < msgMaxLength" 1190 and P'=UNIV 1191 in ccorres_from_vcg_throws) 1192 apply (simp add: return_def split del: if_split) 1193 apply (rule allI, rule conseqPre, vcg) 1194 apply (clarsimp split del: if_split) 1195 apply (frule(1) user_word_at_cross_over, rule refl) 1196 apply (clarsimp simp: ptr_add_def mult.commute 1197 msgMaxLength_def) 1198 apply (safe intro!: disjCI2 elim!: valid_ipc_buffer_ptr_array, 1199 simp_all add: unatSuc2 add.commute msg_align_bits)[1] 1200 apply wp[1] 1201 apply (rule_tac P="\<exists>b. buffer = Some b" in hoare_gen_asm) 1202 apply (clarsimp simp: option_to_ptr_def option_to_0_def) 1203 apply (rule_tac P="\<lambda>s. valid_ipc_buffer_ptr' (ptr_val (Ptr b)) s \<and> i < msgLength mi \<and> 1204 msgLength mi \<le> msgMaxLength \<and> scast n_msgRegisters \<le> i" 1205 in hoare_pre(1)) 1206 apply (wp getMRs_user_word) 1207 apply (clarsimp simp: msgMaxLength_def unat_less_helper) 1208 apply simp 1209 apply (clarsimp simp: sysargs_rel_def sysargs_rel_n_def) 1210 apply (rule conjI, clarsimp simp: unat_of_nat64 word_bits_def) 1211 apply (drule equalityD2) 1212 apply clarsimp 1213 apply (drule use_valid, rule getMRs_length, assumption) 1214 apply (simp add: n_msgRegisters_def split: if_split_asm) 1215 apply (rule conjI) 1216 apply (clarsimp simp: option_to_ptr_def option_to_0_def 1217 word_less_nat_alt word_le_nat_alt unat_of_nat64 word_bits_def 1218 n_msgRegisters_def not_less msgMaxLength_def) 1219 apply (drule equalityD2) 1220 apply clarsimp 1221 apply (drule use_valid, rule getMRs_length) 1222 apply (simp add: word_le_nat_alt msgMaxLength_def) 1223 apply (simp split: if_split_asm) 1224 apply (rule conjI, clarsimp simp: cur_tcb'_def) 1225 apply clarsimp 1226 apply (clarsimp simp: bind_def gets_def return_def split_def get_def) 1227 done 1228 1229end 1230 1231context begin interpretation Arch . (*FIXME: arch_split*) 1232 1233lemma invocation_eq_use_type: 1234 "\<lbrakk> value \<equiv> (value' :: 32 signed word); 1235 unat (scast value' :: machine_word) < length (enum :: invocation_label list); (scast value' :: machine_word) \<noteq> 0 \<rbrakk> 1236 \<Longrightarrow> (label = (scast value)) = (invocation_type label = enum ! unat (scast value' :: machine_word))" 1237 apply (fold invocation_type_eq, unfold invocationType_def) 1238 apply (simp add: maxBound_is_length Let_def toEnum_def 1239 nth_eq_iff_index_eq nat_le_Suc_less_imp 1240 split: if_split) 1241 apply (intro impI conjI) 1242 apply (simp add: enum_invocation_label) 1243 apply (subgoal_tac "InvalidInvocation = enum ! 0") 1244 apply (erule ssubst, subst nth_eq_iff_index_eq, simp+) 1245 apply (clarsimp simp add: unat_eq_0) 1246 apply (simp add: enum_invocation_label) 1247 done 1248 1249lemmas all_invocation_label_defs = invocation_label_defs arch_invocation_label_defs sel4_arch_invocation_label_defs 1250 1251lemmas invocation_eq_use_types 1252 = all_invocation_label_defs[THEN invocation_eq_use_type, simplified, 1253 unfolded enum_invocation_label enum_arch_invocation_label, simplified] 1254 1255lemma ccorres_equals_throwError: 1256 "\<lbrakk> f = throwError v; ccorres_underlying sr Gamm rr xf arr axf P P' hs (throwError v) c \<rbrakk> 1257 \<Longrightarrow> ccorres_underlying sr Gamm rr xf arr axf P P' hs f c" 1258 by simp 1259 1260end 1261 1262end 1263