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> word32 \<Rightarrow> errtype \<Rightarrow> bool" 30where 31 "cintr a x err \<equiv> x = scast EXCEPTION_PREEMPTED" 32 33definition 34 replyOnRestart :: "word32 \<Rightarrow> word32 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> word32) 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> word32 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> word32) 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 532lemmas injection_handler_bindE = injection_bindE [OF refl refl] 533lemmas injection_handler_wp = injection_wp [OF refl] 534 535lemma ccorres_injection_handler_csum1: 536 "ccorres (f \<currency> r) xf P P' hs a c 537 \<Longrightarrow> ccorres 538 ((\<lambda>rv a b. \<exists>rv'. rv = injector rv' \<and> f rv' a b) \<currency> r) xf P P' hs 539 (injection_handler injector a) c" 540 apply (simp add: injection_handler_liftM) 541 apply (erule ccorres_rel_imp) 542 apply (auto split: sum.split) 543 done 544 545lemma ccorres_injection_handler_csum2: 546 "ccorres ((f o injector) \<currency> r) xf P P' hs a c 547 \<Longrightarrow> ccorres (f \<currency> r) xf P P' hs 548 (injection_handler injector a) c" 549 apply (simp add: injection_handler_liftM) 550 apply (erule ccorres_rel_imp) 551 apply (auto split: sum.split) 552 done 553 554definition 555 is_nondet_refinement :: "('a, 's) nondet_monad 556 \<Rightarrow> ('a, 's) nondet_monad \<Rightarrow> bool" 557where 558 "is_nondet_refinement f g \<equiv> \<forall>s. (snd (f s) \<longrightarrow> snd (g s)) \<and> fst (f s) \<subseteq> fst (g s)" 559 560lemma is_nondet_refinement_refl[simp]: 561 "is_nondet_refinement a a" 562 by (simp add: is_nondet_refinement_def) 563 564lemma is_nondet_refinement_bind: 565 "\<lbrakk> is_nondet_refinement a c; \<And>rv. is_nondet_refinement (b rv) (d rv) \<rbrakk> 566 \<Longrightarrow> is_nondet_refinement (a >>= b) (c >>= d)" 567 apply (clarsimp simp: is_nondet_refinement_def bind_def split_def) 568 apply fast 569 done 570 571lemma is_nondet_refinement_bindE: 572 "\<lbrakk> is_nondet_refinement a c; \<And>rv. is_nondet_refinement (b rv) (d rv) \<rbrakk> 573 \<Longrightarrow> is_nondet_refinement (a >>=E b) (c >>=E d)" 574 apply (simp add: bindE_def) 575 apply (erule is_nondet_refinement_bind) 576 apply (simp add: lift_def split: sum.split) 577 done 578 579lemma ccorres_nondet_refinement: 580 "\<lbrakk> is_nondet_refinement a b; 581 ccorres_underlying sr Gamm rvr xf arrel axf G G' hs a c \<rbrakk> 582 \<Longrightarrow> ccorres_underlying sr Gamm rvr xf arrel axf G G' hs b c" 583 apply (simp add: ccorres_underlying_def is_nondet_refinement_def 584 split_def) 585 apply (rule ballI, drule(1) bspec) 586 apply (intro impI) 587 apply (drule mp, blast) 588 apply (elim allEI) 589 apply (clarsimp split: xstate.split_asm) 590 apply blast 591 done 592 593lemma is_nondet_refinement_alternative1: 594 "is_nondet_refinement a (a \<sqinter> b)" 595 by (clarsimp simp add: is_nondet_refinement_def alternative_def) 596 597lemma ccorres_defer: 598 assumes c: "ccorres r xf P P' hs H C" 599 assumes f: "no_fail Q H" 600 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" 601 using c 602 apply (clarsimp simp: ccorres_underlying_def split: xstate.splits) 603 apply (drule (1) bspec) 604 apply clarsimp 605 apply (erule impE) 606 apply (insert f)[1] 607 apply (clarsimp simp: no_fail_def) 608 apply (clarsimp simp: return_def) 609 apply (rule conjI) 610 apply clarsimp 611 apply (rename_tac s) 612 apply (erule_tac x=n in allE) 613 apply (erule_tac x="Normal s" in allE) 614 apply (clarsimp simp: unif_rrel_def) 615 apply fastforce 616 done 617 618lemma no_fail_loadWordUser: 619 "no_fail (pointerInUserData x and K (is_aligned x 2)) (loadWordUser x)" 620 apply (simp add: loadWordUser_def) 621 apply (rule no_fail_pre, wp no_fail_stateAssert) 622 apply simp 623 done 624 625lemma no_fail_getMRs: 626 "no_fail (tcb_at' thread and case_option \<top> valid_ipc_buffer_ptr' buffer) 627 (getMRs thread buffer info)" 628 apply (rule det_wp_no_fail) 629 apply (rule det_wp_getMRs) 630 done 631 632lemma msgRegisters_scast: 633 "n < unat (scast n_msgRegisters :: word32) \<Longrightarrow> 634 unat (scast (index msgRegistersC n)::word32) = unat (index msgRegistersC n)" 635 apply (simp add: msgRegisters_def fupdate_def update_def n_msgRegisters_def fcp_beta 636 Kernel_C.R2_def Kernel_C.R3_def Kernel_C.R4_def Kernel_C.R5_def 637 Kernel_C.R6_def Kernel_C.R7_def) 638 done 639 640lemma asUser_cur_obj_at': 641 assumes f: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>" 642 shows "\<lbrace>\<lambda>s. obj_at' (\<lambda>tcb. P (atcbContextGet (tcbArch tcb))) (ksCurThread s) s \<and> t = ksCurThread s\<rbrace> 643 asUser t f \<lbrace>\<lambda>rv s. obj_at' (\<lambda>tcb. Q rv (atcbContextGet (tcbArch tcb))) (ksCurThread s) s\<rbrace>" 644 apply (simp add: asUser_def split_def) 645 apply (wp) 646 apply (rule hoare_lift_Pf2 [where f=ksCurThread]) 647 apply (wp threadSet_obj_at'_really_strongest)+ 648 apply (clarsimp simp: threadGet_def) 649 apply (wp getObject_tcb_wp) 650 apply clarsimp 651 apply (drule obj_at_ko_at') 652 apply clarsimp 653 apply (rename_tac tcb) 654 apply (rule_tac x=tcb in exI) 655 apply clarsimp 656 apply (drule use_valid, rule f, assumption) 657 apply clarsimp 658 done 659 660lemma asUser_const_rv: 661 assumes f: "\<lbrace>\<lambda>s. P\<rbrace> f \<lbrace>\<lambda>rv s. Q rv\<rbrace>" 662 shows "\<lbrace>\<lambda>s. P\<rbrace> asUser t f \<lbrace>\<lambda>rv s. Q rv\<rbrace>" 663 apply (simp add: asUser_def split_def) 664 apply (wp) 665 apply (clarsimp simp: threadGet_def) 666 apply (wp getObject_tcb_wp) 667 apply clarsimp 668 apply (drule obj_at_ko_at') 669 apply clarsimp 670 apply (rename_tac tcb) 671 apply (rule_tac x=tcb in exI) 672 apply clarsimp 673 apply (drule use_valid, rule f, assumption) 674 apply clarsimp 675 done 676 677 678lemma getMRs_tcbContext: 679 "\<lbrace>\<lambda>s. n < unat n_msgRegisters \<and> n < unat (msgLength info) \<and> thread = ksCurThread s \<and> cur_tcb' s\<rbrace> 680 getMRs thread buffer info 681 \<lbrace>\<lambda>rv s. obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) (ARM_HYP_H.msgRegisters ! n) = rv ! n) (ksCurThread s) s\<rbrace>" 682 apply (rule hoare_assume_pre) 683 apply (elim conjE) 684 apply (thin_tac "thread = t" for t) 685 apply (clarsimp simp add: getMRs_def) 686 apply (wp|wpc)+ 687 apply (rule_tac P="n < length x" in hoare_gen_asm) 688 apply (clarsimp simp: nth_append) 689 apply (wp mapM_wp' static_imp_wp)+ 690 apply simp 691 apply (rule asUser_cur_obj_at') 692 apply (simp add: getRegister_def msgRegisters_unfold) 693 apply (simp add: mapM_Cons bind_assoc mapM_empty) 694 apply wp 695 apply (wp hoare_drop_imps hoare_vcg_all_lift) 696 apply (wp asUser_cur_obj_at') 697 apply (simp add: getRegister_def msgRegisters_unfold) 698 apply (simp add: mapM_Cons bind_assoc mapM_empty) 699 apply (wp asUser_const_rv) 700 apply clarsimp 701 apply (wp asUser_const_rv) 702 apply (clarsimp simp: n_msgRegisters_def msgRegisters_unfold) 703 apply (simp add: nth_Cons' cur_tcb'_def split: if_split) 704 done 705 706lemma threadGet_tcbIpcBuffer_ccorres [corres]: 707 "ccorres (=) w_bufferPtr_' (tcb_at' tptr) UNIV hs 708 (threadGet tcbIPCBuffer tptr) 709 (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t tcb_ptr_to_ctcb_ptr tptr\<rbrace> 710 (\<acute>w_bufferPtr :== 711 h_val (hrs_mem \<acute>t_hrs) 712 (Ptr &(tcb_ptr_to_ctcb_ptr tptr\<rightarrow>[''tcbIPCBuffer_C''])::word32 ptr)))" 713 apply (rule ccorres_guard_imp2) 714 apply (rule ccorres_add_return2) 715 apply (rule ccorres_pre_threadGet) 716 apply (rule_tac P = "obj_at' (\<lambda>tcb. tcbIPCBuffer tcb = x) tptr" and 717 P'="{s'. \<exists>ctcb. 718 cslift s' (tcb_ptr_to_ctcb_ptr tptr) = Some ctcb \<and> 719 tcbIPCBuffer_C ctcb = x }" in ccorres_from_vcg) 720 apply (rule allI, rule conseqPre, vcg) 721 apply clarsimp 722 apply (clarsimp simp: return_def typ_heap_simps') 723 apply (clarsimp simp: obj_at'_def ctcb_relation_def) 724 done 725 726(* FIXME: move *) 727lemma ccorres_case_bools: 728 assumes P: "ccorres r xf P P' hs (a True) (c True)" 729 assumes Q: "ccorres r xf Q Q' hs (a False) (c False)" 730 shows "ccorres r xf (\<lambda>s. (b \<longrightarrow> P s) \<and> (\<not>b \<longrightarrow> Q s)) 731 ({s. b \<longrightarrow> s \<in> P'} \<inter> {s. \<not>b \<longrightarrow> s \<in> Q'}) 732 hs (a b) (c b)" 733 apply (cases b) 734 apply (auto simp: P Q) 735 done 736 737lemma ccorres_cond_both': 738 assumes abs: "\<forall>s s'. (s, s') \<in> sr \<and> Q s \<and> Q' s' \<longrightarrow> P = (s' \<in> P')" 739 and ac: "P \<Longrightarrow> ccorres_underlying sr G r xf arrel axf R R' hs a c" 740 and bd: "\<not> P \<Longrightarrow> ccorres_underlying sr G r xf arrel axf U U' hs b d" 741 shows "ccorres_underlying sr G r xf arrel axf 742 (Q and (\<lambda>s. P \<longrightarrow> R s) and (\<lambda>s. \<not> P \<longrightarrow> U s)) 743 (Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')}) 744 hs 745 (if P then a else b) (Cond P' c d)" 746 apply (rule ccorres_guard_imp2) 747 apply (rule ccorres_if_lhs) 748 apply (rule ccorres_cond_true) 749 apply (erule ac) 750 apply (rule ccorres_cond_false) 751 apply (erule bd) 752 apply clarsimp 753 apply (frule abs[rule_format, OF conjI], simp+) 754 done 755 756lemma pageBitsForSize_32 [simp]: 757 "pageBitsForSize sz < 32" 758 by (cases sz, auto) 759 760lemma ccap_relation_frame_tags: 761 "ccap_relation (ArchObjectCap (PageCap dev v0 v1 v2 v3)) cap \<Longrightarrow> 762 cap_get_tag cap = scast cap_frame_cap \<or> cap_get_tag cap = scast cap_small_frame_cap" 763 apply (case_tac "v2 = ARMSmallPage") 764 apply (auto simp: cap_get_tag_isCap_unfolded_H_cap) 765 done 766 767(* FIXME: move *) 768lemma ccorres_case_bools': 769 assumes P: "b \<Longrightarrow> ccorres r xf P P' hs (a True) (c True)" 770 assumes Q: "\<not> b \<Longrightarrow> ccorres r xf Q Q' hs (a False) (c False)" 771 shows "ccorres r xf (\<lambda>s. (b \<longrightarrow> P s) \<and> (\<not>b \<longrightarrow> Q s)) 772 ({s. b \<longrightarrow> s \<in> P'} \<inter> {s. \<not>b \<longrightarrow> s \<in> Q'}) 773 hs (a b) (c b)" 774 apply (cases b) 775 apply (auto simp: P Q) 776 done 777 778lemma capFVMRights_range: 779 "\<And>cap. cap_get_tag cap = scast cap_frame_cap \<Longrightarrow> 780 cap_frame_cap_CL.capFVMRights_CL (cap_frame_cap_lift cap) \<le> 3" 781 "\<And>cap. cap_get_tag cap = scast cap_small_frame_cap \<Longrightarrow> 782 cap_small_frame_cap_CL.capFVMRights_CL (cap_small_frame_cap_lift cap) \<le> 3" 783 by (simp add: cap_frame_cap_lift_def cap_small_frame_cap_lift_def 784 cap_lift_def cap_tag_defs word_and_le1 mask_def)+ 785 786lemma dumb_bool_for_all: "(\<forall>x. x) = False" 787 by auto 788 789lemma dumb_bool_split_for_vcg: 790 "\<lbrace>d \<longrightarrow> \<acute>ret__unsigned_long \<noteq> 0\<rbrace> \<inter> \<lbrace>\<not> d \<longrightarrow> \<acute>ret__unsigned_long = 0\<rbrace> 791 = \<lbrace>d = to_bool \<acute>ret__unsigned_long \<rbrace>" 792 by (auto simp: to_bool_def) 793 794lemma ccap_relation_page_is_device: 795 "ccap_relation (capability.ArchObjectCap (arch_capability.PageCap d v0a v1 v2 v3)) c 796 \<Longrightarrow> (generic_frame_cap_get_capFIsDevice_CL (cap_lift c) \<noteq> 0) = d" 797 apply (clarsimp simp: ccap_relation_def Let_def map_option_Some_eq2 cap_to_H_def) 798 apply (case_tac z) 799 apply (auto split: if_splits simp: to_bool_def generic_frame_cap_get_capFIsDevice_CL_def Let_def) 800 done 801 802lemma lookupIPCBuffer_ccorres[corres]: 803 "ccorres ((=) \<circ> option_to_ptr) ret__ptr_to_unsigned_long_' 804 (tcb_at' t) 805 (UNIV \<inter> {s. thread_' s = tcb_ptr_to_ctcb_ptr t} 806 \<inter> {s. isReceiver_' s = from_bool isReceiver}) [] 807 (lookupIPCBuffer isReceiver t) (Call lookupIPCBuffer_'proc)" 808 apply (cinit lift: thread_' isReceiver_') 809 apply (rule ccorres_split_nothrow) 810 apply simp 811 apply (rule threadGet_tcbIpcBuffer_ccorres) 812 apply ceqv 813 apply (simp add: getThreadBufferSlot_def locateSlot_conv 814 cte_C_size word_sle_def Collect_True 815 del: Collect_const) 816 apply ccorres_remove_UNIV_guard 817 apply (rule ccorres_getSlotCap_cte_at) 818 apply (rule ccorres_move_array_assertion_tcb_ctes 819 ccorres_move_c_guard_tcb_ctes)+ 820 apply (ctac (no_vcg)) 821 apply csymbr 822 apply (rule_tac b="isArchObjectCap rva \<and> isPageCap (capCap rva)" in ccorres_case_bools') 823 apply simp 824 apply (rule ccorres_symb_exec_r) 825 apply (rule_tac b="capVPSize (capCap rva) \<noteq> ARMSmallPage" in ccorres_case_bools') 826 apply (rule ccorres_cond_true_seq) 827 apply (rule ccorres_rhs_assoc)+ 828 apply csymbr 829 apply csymbr 830 apply (rule ccorres_cond_false_seq) 831 apply (simp(no_asm)) 832 apply csymbr 833 apply (rule_tac b="isDeviceCap rva" in ccorres_case_bools') 834 apply (rule ccorres_cond_true_seq) 835 apply (rule ccorres_from_vcg_split_throws[where P=\<top> and P'=UNIV]) 836 apply vcg 837 apply (rule conseqPre, vcg, 838 clarsimp simp: isCap_simps return_def 839 option_to_ptr_def option_to_0_def) 840 apply (rule ccorres_cond_false_seq) 841 apply simp 842 apply csymbr 843 apply (clarsimp simp: isCap_simps) 844 apply (rule ccorres_guard_imp[where A=\<top> and A'=UNIV], 845 rule ccorres_cond [where R=\<top>]) 846 apply (clarsimp simp: from_bool_0 isCap_simps) 847 apply (frule ccap_relation_PageCap_generics) 848 apply clarsimp 849 apply (clarsimp simp: vmrights_to_H_def) 850 apply (simp add: Kernel_C.VMReadOnly_def Kernel_C.VMKernelOnly_def 851 Kernel_C.VMReadWrite_def Kernel_C.VMNoAccess_def 852 split: if_split) 853 apply clarsimp 854 apply (drule less_4_cases) 855 apply auto[1] 856 apply (frule cap_get_tag_isCap_unfolded_H_cap(17),simp) 857 apply (frule capFVMRights_range) 858 apply (simp add: cap_frame_cap_lift 859 generic_frame_cap_get_capFVMRights_CL_def) 860 apply (clarsimp simp: cap_to_H_def vmrights_to_H_def to_bool_def 861 word_le_make_less Kernel_C.VMNoAccess_def 862 Kernel_C.VMReadWrite_def Kernel_C.VMReadOnly_def 863 Kernel_C.VMKernelOnly_def 864 dest: word_less_cases) 865 apply (rule ccorres_rhs_assoc)+ 866 apply csymbr 867 apply csymbr 868 apply csymbr 869 apply csymbr 870 apply csymbr 871 apply csymbr 872 apply (rule ccorres_Guard) 873 apply simp 874 apply (rule ccorres_assert)+ 875 apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws) 876 apply (rule allI, rule conseqPre, vcg) 877 apply (clarsimp simp: return_def option_to_ptr_def option_to_0_def isCap_simps) 878 apply (clarsimp dest!: ccap_relation_PageCap_generics simp: mask_def) 879 apply (ctac add: ccorres_return_C) 880 apply clarsimp 881 apply (clarsimp simp: if_1_0_0 Collect_const_mem isCap_simps word_less_nat_alt 882 option_to_ptr_def from_bool_0 option_to_0_def dest!:ccap_relation_frame_tags) 883 apply (rule ccorres_cond_false_seq) 884 apply (simp(no_asm)) 885 apply (rule ccorres_cond_false_seq) 886 apply (simp(no_asm)) 887 apply csymbr 888 apply (rule_tac b="isDeviceCap rva" in ccorres_case_bools') 889 apply (rule ccorres_cond_true_seq) 890 apply (rule ccorres_from_vcg_split_throws[where P=\<top> and P'=UNIV]) 891 apply vcg 892 apply (rule conseqPre, vcg, 893 clarsimp simp: isCap_simps return_def 894 option_to_ptr_def option_to_0_def) 895 apply (rule ccorres_cond_false_seq) 896 apply simp 897 apply csymbr 898 apply (clarsimp simp: isCap_simps) 899 apply (rule ccorres_guard_imp[where A=\<top> and A'=UNIV], 900 rule ccorres_cond [where R=\<top>]) 901 apply (clarsimp simp: from_bool_0 isCap_simps) 902 apply (frule ccap_relation_PageCap_generics) 903 apply clarsimp 904 apply (clarsimp simp: vmrights_to_H_def) 905 apply (simp add: Kernel_C.VMReadOnly_def Kernel_C.VMKernelOnly_def 906 Kernel_C.VMReadWrite_def Kernel_C.VMNoAccess_def 907 split: if_split) 908 apply clarsimp 909 apply (drule less_4_cases) 910 apply auto[1] 911 apply (frule cap_get_tag_isCap_unfolded_H_cap(16),simp) 912 apply (frule capFVMRights_range) 913 apply (simp add: cap_frame_cap_lift 914 generic_frame_cap_get_capFVMRights_CL_def) 915 apply (clarsimp simp: cap_to_H_def vmrights_to_H_def to_bool_def 916 word_le_make_less Kernel_C.VMNoAccess_def 917 Kernel_C.VMReadWrite_def Kernel_C.VMReadOnly_def 918 Kernel_C.VMKernelOnly_def 919 dest: word_less_cases) 920 apply (rule ccorres_rhs_assoc)+ 921 apply csymbr 922 apply csymbr 923 apply csymbr 924 apply csymbr 925 apply csymbr 926 apply csymbr 927 apply (rule ccorres_Guard) 928 apply simp 929 apply (rule ccorres_assert)+ 930 apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws) 931 apply (rule allI, rule conseqPre, vcg) 932 apply (clarsimp simp: return_def option_to_ptr_def option_to_0_def isCap_simps) 933 apply (clarsimp dest!: ccap_relation_PageCap_generics simp: mask_def) 934 apply (ctac add: ccorres_return_C) 935 apply clarsimp 936 apply (clarsimp simp: if_1_0_0 Collect_const_mem isCap_simps word_less_nat_alt 937 option_to_ptr_def option_to_0_def dest!:ccap_relation_frame_tags) 938 apply (clarsimp simp: from_bool_0) 939 apply vcg 940 apply clarsimp 941 apply (rule conseqPre, vcg) 942 apply (clarsimp simp: from_bool_0 isCap_simps Collect_const_mem) 943 apply (simp (no_asm)) 944 apply (rule ccorres_symb_exec_r) 945 apply (rule ccorres_cond_true_seq) 946 apply (rule ccorres_rhs_assoc)+ 947 apply csymbr 948 apply csymbr 949 apply (rule ccorres_cond_true_seq) 950 apply simp 951 apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws) 952 apply (rule allI, rule conseqPre, vcg) 953 apply (clarsimp simp: return_def option_to_ptr_def option_to_0_def isCap_simps 954 dumb_bool_for_all 955 split: capability.splits arch_capability.splits bool.splits) 956 957 apply vcg 958 apply (rule conseqPre, vcg) 959 apply clarsimp 960 apply clarsimp 961 apply wp 962 apply (clarsimp simp: if_1_0_0 Collect_const_mem) 963 apply (rule conjI) 964 apply (clarsimp simp: isCap_simps word_less_nat_alt ) 965 apply (frule ccap_relation_page_is_device) 966 apply (frule ccap_relation_PageCap_generics) 967 apply (frule ccap_relation_frame_tags) 968 apply clarsimp 969 apply (rule conjI,clarsimp) 970 apply (simp add: to_bool_neq_0 cap_get_tag_PageCap_small_frame 971 cap_get_tag_PageCap_frame cap_frame_cap_lift 972 split: if_splits) 973 apply (erule disjE) 974 apply ((clarsimp simp: cap_small_frame_cap_lift cap_get_tag_PageCap_frame 975 to_bool_neq_0 cap_get_tag_PageCap_small_frame 976 split: if_splits)+)[2] 977 apply (rule ccontr) 978 apply clarsimp 979 apply (erule disjE) 980 apply ((fastforce simp: cap_get_tag_PageCap_frame 981 cap_get_tag_PageCap_small_frame isCap_simps)+)[2] 982 apply wp 983 apply vcg 984 apply (simp add: word_sle_def Collect_const_mem 985 tcb_cnode_index_defs tcbSlots cte_level_bits_def 986 size_of_def) 987 done 988 989 990lemma doMachineOp_pointerInUserData: 991 "\<lbrace>pointerInUserData p\<rbrace> doMachineOp m \<lbrace>\<lambda>rv. pointerInUserData p\<rbrace>" 992 by (simp add: pointerInUserData_def) wp 993 994lemma loadWordUser_wp: 995 "\<lbrace>\<lambda>s. is_aligned p 2 \<and> (\<forall>v. user_word_at v p s \<longrightarrow> P v s)\<rbrace> 996 loadWordUser p 997 \<lbrace>P\<rbrace>" 998 apply (simp add: loadWordUser_def loadWord_def stateAssert_def 999 user_word_at_def valid_def) 1000 apply (clarsimp simp: in_monad in_doMachineOp) 1001 done 1002 1003lemma ccorres_pre_loadWordUser: 1004 "(\<And>rv. ccorres r xf (P rv) (Q rv) hs (a rv) c) \<Longrightarrow> 1005 ccorres r xf (valid_pspace' and K (is_aligned ptr 2) and 1006 (\<lambda>s. \<forall>v. user_word_at v ptr s \<longrightarrow> P v s)) 1007 {s. \<forall>v. cslift s (Ptr ptr :: word32 ptr) = Some v \<longrightarrow> 1008 s \<in> Q v} hs 1009 (loadWordUser ptr >>= a) c" 1010 apply (rule ccorres_guard_imp) 1011 apply (rule_tac Q="\<lambda>rv. P rv and user_word_at rv ptr" and Q'=Q in 1012 ccorres_symb_exec_l [OF _ loadWordUser_inv loadWordUser_wp]) 1013 apply (fastforce intro: ccorres_guard_imp) 1014 apply simp 1015 apply simp 1016 apply clarsimp 1017 apply (drule(1) user_word_at_cross_over, simp) 1018 apply (clarsimp simp: typ_heap_simps h_t_valid_clift_Some_iff) 1019 done 1020 1021lemma loadWordUser_user_word_at: 1022 "\<lbrace>\<lambda>s. \<forall>rv. user_word_at rv x s \<longrightarrow> Q rv s\<rbrace> loadWordUser x \<lbrace>Q\<rbrace>" 1023 apply (simp add: loadWordUser_def user_word_at_def 1024 doMachineOp_def split_def) 1025 apply wp 1026 apply (clarsimp simp: pointerInUserData_def 1027 loadWord_def in_monad 1028 is_aligned_mask) 1029 done 1030 1031lemma mapM_loadWordUser_user_words_at: 1032 "\<lbrace>\<lambda>s. \<forall>rv. (\<forall>x < length xs. user_word_at (rv ! x) (xs ! x) s) 1033 \<and> length rv = length xs \<longrightarrow> Q rv s\<rbrace> 1034 mapM loadWordUser xs \<lbrace>Q\<rbrace>" 1035 apply (induct xs arbitrary: Q) 1036 apply (simp add: mapM_def sequence_def) 1037 apply wp 1038 apply (simp add: mapM_Cons) 1039 apply wp 1040 apply assumption 1041 apply (wp loadWordUser_user_word_at) 1042 apply clarsimp 1043 apply (drule spec, erule mp) 1044 apply clarsimp 1045 apply (case_tac x) 1046 apply simp 1047 apply simp 1048 done 1049 1050 1051lemma getMRs_user_word: 1052 "\<lbrace>\<lambda>s. valid_ipc_buffer_ptr' buffer s \<and> i < msgLength info 1053 \<and> msgLength info \<le> msgMaxLength \<and> i >= scast n_msgRegisters\<rbrace> 1054 getMRs thread (Some buffer) info 1055 \<lbrace>\<lambda>xs. user_word_at (xs ! unat i) (buffer + (i * 4 + 4))\<rbrace>" 1056 apply (rule hoare_assume_pre) 1057 apply (elim conjE) 1058 apply (thin_tac "valid_ipc_buffer_ptr' x y" for x y) 1059 apply (simp add: getMRs_def) 1060 apply wp 1061 apply (rule_tac P="length hardwareMRValues = unat n_msgRegisters" in hoare_gen_asm) 1062 apply (clarsimp simp: nth_append word_le_nat_alt 1063 word_less_nat_alt word_size 1064 linorder_not_less [symmetric]) 1065 apply (wp mapM_loadWordUser_user_words_at) 1066 apply (wp hoare_vcg_all_lift) 1067 apply (rule_tac Q="\<lambda>_. \<top>" in hoare_strengthen_post) 1068 apply wp 1069 apply clarsimp 1070 defer 1071 apply simp 1072 apply (wp asUser_const_rv) 1073 apply (simp add: msgRegisters_unfold n_msgRegisters_def) 1074 apply (erule_tac x="unat i - unat n_msgRegisters" in allE) 1075 apply (erule impE) 1076 apply (simp add: msgRegisters_unfold 1077 msgMaxLength_def msgLengthBits_def n_msgRegisters_def) 1078 apply (drule (1) order_less_le_trans) 1079 apply (simp add: word_less_nat_alt word_le_nat_alt) 1080 apply (simp add: msgRegisters_unfold 1081 msgMaxLength_def msgLengthBits_def n_msgRegisters_def) 1082 apply (simp add: upto_enum_word del: upt_rec_numeral) 1083 apply (subst (asm) nth_map) 1084 apply (simp del: upt_rec_numeral) 1085 apply (drule (1) order_less_le_trans) 1086 apply (simp add: word_less_nat_alt word_le_nat_alt) 1087 apply (subst (asm) nth_upt) 1088 apply simp 1089 apply (drule (1) order_less_le_trans) 1090 apply (simp add: word_less_nat_alt word_le_nat_alt) 1091 apply (simp add: word_le_nat_alt add.commute add.left_commute mult.commute mult.left_commute 1092 wordSize_def') 1093 done 1094 1095declare if_split [split] 1096 1097definition 1098 "getMRs_rel args buffer \<equiv> \<lambda>s. \<exists>mi. msgLength mi \<le> msgMaxLength \<and> fst (getMRs (ksCurThread s) buffer mi s) = {(args, s)}" 1099 1100definition 1101 "sysargs_rel args buffer \<equiv> 1102 cur_tcb' 1103 and case_option \<top> valid_ipc_buffer_ptr' buffer 1104 and getMRs_rel args buffer 1105 and (\<lambda>_. length args > unat (scast n_msgRegisters :: word32) \<longrightarrow> buffer \<noteq> None)" 1106 1107definition 1108 "sysargs_rel_n args buffer n \<equiv> \<lambda>s. n < length args \<and> (unat (scast n_msgRegisters :: word32) \<le> n \<longrightarrow> buffer \<noteq> None)" 1109 1110lemma sysargs_rel_to_n: 1111 "sysargs_rel args buffer s \<Longrightarrow> sysargs_rel_n args buffer n s = (n < length args)" 1112 by (auto simp add: sysargs_rel_def sysargs_rel_n_def) 1113 1114lemma getMRs_rel: 1115 "\<lbrace>\<lambda>s. msgLength mi \<le> msgMaxLength \<and> thread = ksCurThread s \<and> 1116 case_option \<top> valid_ipc_buffer_ptr' buffer s \<and> 1117 cur_tcb' s\<rbrace> 1118 getMRs thread buffer mi \<lbrace>\<lambda>args. getMRs_rel args buffer\<rbrace>" 1119 apply (simp add: getMRs_rel_def) 1120 apply (rule hoare_pre) 1121 apply (rule_tac x=mi in hoare_vcg_exI) 1122 apply wp 1123 apply (rule_tac Q="\<lambda>rv s. thread = ksCurThread s \<and> fst (getMRs thread buffer mi s) = {(rv,s)}" in hoare_strengthen_post) 1124 apply (wp det_result det_wp_getMRs) 1125 apply clarsimp 1126 apply (clarsimp simp: cur_tcb'_def) 1127 done 1128 1129lemma length_msgRegisters: 1130 "length ARM_HYP_H.msgRegisters = unat (scast n_msgRegisters :: word32)" 1131 by (simp add: msgRegisters_unfold n_msgRegisters_def) 1132 1133lemma getMRs_len[simplified]: 1134 "\<lbrace>\<top>\<rbrace> getMRs thread buffer mi \<lbrace>\<lambda>args s. length args > unat (scast n_msgRegisters :: word32) \<longrightarrow> buffer \<noteq> None\<rbrace>" 1135 apply (simp add: getMRs_def) 1136 apply (cases buffer, simp_all add:hoare_TrueI) 1137 apply (wp asUser_const_rv | simp)+ 1138 apply (simp add: length_msgRegisters) 1139 done 1140 1141lemma getMRs_sysargs_rel: 1142 "\<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> 1143 getMRs thread buffer mi \<lbrace>\<lambda>args. sysargs_rel args buffer\<rbrace>" 1144 apply (simp add: sysargs_rel_def) 1145 apply (wp getMRs_rel getMRs_len|simp)+ 1146 done 1147 1148lemma ccorres_assume_pre: 1149 assumes "\<And>s. P s \<Longrightarrow> ccorres r xf (P and (\<lambda>s'. s' = s)) P' hs H C" 1150 shows "ccorres r xf P P' hs H C" 1151 apply (clarsimp simp: ccorres_underlying_def) 1152 apply (frule assms) 1153 apply (simp add: ccorres_underlying_def) 1154 apply blast 1155 done 1156 1157lemma getMRs_length: 1158 "\<lbrace>\<lambda>s. msgLength mi \<le> msgMaxLength\<rbrace> getMRs thread buffer mi 1159 \<lbrace>\<lambda>args s. if buffer = None then length args = min (unat (scast n_msgRegisters :: word32)) (unat (msgLength mi)) 1160 else length args = unat (msgLength mi)\<rbrace>" 1161 apply (cases buffer) 1162 apply (simp add: getMRs_def) 1163 apply (rule hoare_pre, wp) 1164 apply (rule asUser_const_rv) 1165 apply simp 1166 apply (wp mapM_length) 1167 apply (simp add: min_def length_msgRegisters) 1168 apply clarsimp 1169 apply (simp add: getMRs_def) 1170 apply (rule hoare_pre, wp) 1171 apply simp 1172 apply (wp mapM_length asUser_const_rv mapM_length)+ 1173 apply (clarsimp simp: length_msgRegisters) 1174 apply (simp add: min_def split: if_splits) 1175 apply (clarsimp simp: word_le_nat_alt) 1176 apply (simp add: msgMaxLength_def msgLengthBits_def n_msgRegisters_def) 1177 done 1178 1179lemma index_msgRegisters_less': 1180 "n < 4 \<Longrightarrow> index msgRegistersC n < 0x14" 1181 by (simp add: msgRegistersC_def fupdate_def Arrays.update_def 1182 fcp_beta "StrictC'_register_defs") 1183 1184lemma index_msgRegisters_less: 1185 "n < 4 \<Longrightarrow> index msgRegistersC n <s 0x14" 1186 "n < 4 \<Longrightarrow> index msgRegistersC n < 0x14" 1187 using index_msgRegisters_less' 1188 by (simp_all add: word_sless_msb_less) 1189 1190lemma valid_ipc_buffer_ptr_array: 1191 "valid_ipc_buffer_ptr' (ptr_val p) s \<Longrightarrow> (s, s') \<in> rf_sr 1192 \<Longrightarrow> n \<le> 2 ^ (msg_align_bits - 2) 1193 \<Longrightarrow> n \<noteq> 0 1194 \<Longrightarrow> array_assertion (p :: word32 ptr) n (hrs_htd (t_hrs_' (globals s')))" 1195 apply (clarsimp simp: valid_ipc_buffer_ptr'_def typ_at_to_obj_at_arches) 1196 apply (drule obj_at_ko_at', clarsimp) 1197 apply (drule rf_sr_heap_user_data_relation) 1198 apply (erule cmap_relationE1) 1199 apply (clarsimp simp: heap_to_user_data_def Let_def) 1200 apply (rule conjI, rule exI, erule ko_at_projectKO_opt) 1201 apply (rule refl) 1202 apply (drule clift_field, rule user_data_C_words_C_fl_ti, simp) 1203 apply (erule clift_array_assertion_imp, simp+) 1204 apply (simp add: field_lvalue_def msg_align_bits) 1205 apply (rule_tac x="unat (ptr_val p && mask pageBits >> 2)" in exI, 1206 simp add: word_shift_by_2 shiftr_shiftl1 1207 is_aligned_andI1[OF is_aligned_weaken]) 1208 apply (simp add: add.commute word_plus_and_or_coroll2) 1209 apply (cut_tac a="(ptr_val p && mask pageBits ) >> 2" 1210 and b="2 ^ (pageBits - 2) - 2 ^ (msg_align_bits - 2)" in unat_le_helper) 1211 apply (simp add: pageBits_def msg_align_bits mask_def is_aligned_mask) 1212 apply word_bitwise 1213 apply simp 1214 apply (simp add: msg_align_bits pageBits_def multiple_mask_trivia) 1215 done 1216 1217lemma array_assertion_valid_ipc_buffer_ptr_abs: 1218 "\<forall>s s'. (s, s') \<in> rf_sr \<and> (valid_ipc_buffer_ptr' (ptr_val (p s)) s) 1219 \<and> (n s' \<le> 2 ^ (msg_align_bits - 2) \<and> (x s' \<noteq> 0 \<longrightarrow> n s' \<noteq> 0)) 1220 \<longrightarrow> (x s' = 0 \<or> array_assertion (p s :: word32 ptr) (n s') (hrs_htd (t_hrs_' (globals s'))))" 1221 apply (intro allI impI disjCI2, clarsimp) 1222 apply (erule(1) valid_ipc_buffer_ptr_array, simp_all) 1223 done 1224 1225lemmas ccorres_move_array_assertion_ipc_buffer 1226 = ccorres_move_array_assertions [OF array_assertion_valid_ipc_buffer_ptr_abs] 1227 1228lemma getSyscallArg_ccorres_foo: 1229 "ccorres (\<lambda>a rv. rv = args ! n) ret__unsigned_long_' 1230 (sysargs_rel args buffer and sysargs_rel_n args buffer n) 1231 (UNIV \<inter> \<lbrace>unat \<acute>i = n\<rbrace> \<inter> \<lbrace>\<acute>ipc_buffer = option_to_ptr buffer\<rbrace>) [] 1232 (return ()) (Call getSyscallArg_'proc)" 1233 apply (rule ccorres_assume_pre) 1234 apply (subst (asm) sysargs_rel_def) 1235 apply (subst (asm) getMRs_rel_def) 1236 apply (subst (asm) pred_conj_def)+ 1237 apply (elim conjE exE) 1238 apply (cinit lift: i_' ipc_buffer_') 1239 apply (fold return_def) 1240 apply (rule_tac H="do thread \<leftarrow> gets ksCurThread; getMRs thread buffer mi od" in ccorres_defer) 1241 prefer 2 1242 apply (rule no_fail_pre, wp no_fail_getMRs) 1243 apply assumption 1244 apply (rule ccorres_cond_seq) 1245 apply (rule_tac R=\<top> and P="\<lambda>_. n < unat (scast n_msgRegisters :: word32)" in ccorres_cond_both) 1246 apply (simp add: word_less_nat_alt split: if_split) 1247 apply (rule ccorres_add_return2) 1248 apply (rule ccorres_symb_exec_l) 1249 apply (rule_tac P="\<lambda>s. n < unat (scast n_msgRegisters :: word32) \<and> obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) (ARM_HYP_H.msgRegisters!n) = x!n) (ksCurThread s) s" 1250 and P' = UNIV 1251 in ccorres_from_vcg_split_throws) 1252 apply vcg 1253 apply (simp add: return_def del: Collect_const) 1254 apply (rule conseqPre, vcg) 1255 apply (clarsimp simp: rf_sr_ksCurThread) 1256 apply (drule (1) obj_at_cslift_tcb) 1257 apply (clarsimp simp: typ_heap_simps' msgRegisters_scast) 1258 apply (clarsimp simp: ctcb_relation_def ccontext_relation_def 1259 msgRegisters_ccorres atcbContextGet_def 1260 carch_tcb_relation_def) 1261 apply (subst (asm) msgRegisters_ccorres) 1262 apply (clarsimp simp: n_msgRegisters_def) 1263 apply (simp add: n_msgRegisters_def word_less_nat_alt) 1264 apply (simp add: index_msgRegisters_less unat_less_helper) 1265 apply wp[1] 1266 apply (wp getMRs_tcbContext) 1267 apply simp 1268 apply (rule ccorres_seq_skip [THEN iffD2]) 1269 apply (rule ccorres_add_return2) 1270 apply (rule ccorres_symb_exec_l) 1271 apply (rule_tac P="\<lambda>s. user_word_at (x!n) (ptr_val (CTypesDefs.ptr_add ipc_buffer (of_nat n + 1))) s 1272 \<and> valid_ipc_buffer_ptr' (ptr_val ipc_buffer) s \<and> n < msgMaxLength" 1273 and P'=UNIV 1274 in ccorres_from_vcg_throws) 1275 apply (simp add: return_def split del: if_split) 1276 apply (rule allI, rule conseqPre, vcg) 1277 apply (clarsimp split del: if_split) 1278 apply (frule(1) user_word_at_cross_over, rule refl) 1279 apply (clarsimp simp: ptr_add_def mult.commute 1280 msgMaxLength_def) 1281 apply (safe intro!: disjCI2 elim!: valid_ipc_buffer_ptr_array, 1282 simp_all add: unatSuc2 add.commute msg_align_bits)[1] 1283 apply wp[1] 1284 apply (rule_tac P="\<exists>b. buffer = Some b" in hoare_gen_asm) 1285 apply (clarsimp simp: option_to_ptr_def option_to_0_def) 1286 apply (rule_tac P="\<lambda>s. valid_ipc_buffer_ptr' (ptr_val (Ptr b)) s \<and> i < msgLength mi \<and> 1287 msgLength mi \<le> msgMaxLength \<and> scast n_msgRegisters \<le> i" 1288 in hoare_pre(1)) 1289 apply (wp getMRs_user_word) 1290 apply (clarsimp simp: msgMaxLength_def unat_less_helper) 1291 apply simp 1292 apply (clarsimp simp: sysargs_rel_def sysargs_rel_n_def) 1293 apply (rule conjI, clarsimp simp: unat_of_nat32 word_bits_def) 1294 apply (drule equalityD2) 1295 apply clarsimp 1296 apply (drule use_valid, rule getMRs_length, assumption) 1297 apply (simp add: n_msgRegisters_def split: if_split_asm) 1298 apply (rule conjI) 1299 apply (clarsimp simp: option_to_ptr_def option_to_0_def 1300 word_less_nat_alt word_le_nat_alt unat_of_nat32 word_bits_def 1301 n_msgRegisters_def not_less msgMaxLength_def) 1302 apply (drule equalityD2) 1303 apply clarsimp 1304 apply (drule use_valid, rule getMRs_length) 1305 apply (simp add: word_le_nat_alt msgMaxLength_def) 1306 apply (simp split: if_split_asm) 1307 apply (rule conjI, clarsimp simp: cur_tcb'_def) 1308 apply clarsimp 1309 apply (clarsimp simp: bind_def gets_def return_def split_def get_def) 1310 done 1311 1312end 1313 1314context begin interpretation Arch . (*FIXME: arch_split*) 1315 1316lemma invocation_eq_use_type: 1317 "\<lbrakk> value \<equiv> (value' :: 32 signed word); 1318 unat (scast value' :: word32) < length (enum :: invocation_label list); (scast value' :: word32) \<noteq> 0 \<rbrakk> 1319 \<Longrightarrow> (label = (scast value)) = (invocation_type label = enum ! unat (scast value' :: word32))" 1320 apply (fold invocation_type_eq, unfold invocationType_def) 1321 apply (simp add: maxBound_is_length Let_def toEnum_def 1322 nth_eq_iff_index_eq nat_le_Suc_less_imp 1323 split: if_split) 1324 apply (intro impI conjI) 1325 apply (simp add: enum_invocation_label) 1326 apply (subgoal_tac "InvalidInvocation = enum ! 0") 1327 apply (erule ssubst, subst nth_eq_iff_index_eq, simp+) 1328 apply (clarsimp simp add: unat_eq_0) 1329 apply (simp add: enum_invocation_label) 1330 done 1331 1332lemmas all_invocation_label_defs = invocation_label_defs arch_invocation_label_defs sel4_arch_invocation_label_defs 1333 1334lemmas invocation_eq_use_types 1335 = all_invocation_label_defs[THEN invocation_eq_use_type, simplified, 1336 unfolded enum_invocation_label enum_arch_invocation_label, simplified] 1337 1338lemma ccorres_equals_throwError: 1339 "\<lbrakk> f = throwError v; ccorres_underlying sr Gamm rr xf arr axf P P' hs (throwError v) c \<rbrakk> 1340 \<Longrightarrow> ccorres_underlying sr Gamm rr xf arr axf P P' hs f c" 1341 by simp 1342 1343end 1344 1345end 1346