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 TcbAcc_C 12imports Ctac_lemmas_C 13begin 14 15context kernel 16begin 17 18lemma ccorres_pre_threadGet: 19 assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (g rv) c" 20 shows "ccorres r xf 21 (\<lambda>s. \<forall>tcb. ko_at' tcb p s \<longrightarrow> P (f tcb) s) 22 ({s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr p) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> P' (f tcb)}) 23 hs (threadGet f p >>= (\<lambda>rv. g rv)) c" 24 apply (rule ccorres_guard_imp) 25 apply (rule ccorres_symb_exec_l) 26 defer 27 apply wp[1] 28 apply (rule tg_sp') 29 apply simp 30 apply assumption 31 defer 32 apply (rule ccorres_guard_imp) 33 apply (rule cc) 34 apply clarsimp 35 apply (frule obj_at_ko_at') 36 apply clarsimp 37 apply assumption 38 apply clarsimp 39 apply (frule (1) obj_at_cslift_tcb) 40 apply clarsimp 41 done 42 43 44(* FIXME MOVE *) 45crunch inv'[wp]: archThreadGet P 46 (ignore: getObject) 47 48(* FIXME MOVE near thm tg_sp' *) 49lemma atg_sp': 50 "\<lbrace>P\<rbrace> archThreadGet f p \<lbrace>\<lambda>t. obj_at' (\<lambda>t'. f (tcbArch t') = t) p and P\<rbrace>" 51 including no_pre 52 apply (simp add: archThreadGet_def) 53 apply wp 54 apply (rule hoare_strengthen_post) 55 apply (rule getObject_tcb_sp) 56 apply clarsimp 57 apply (erule obj_at'_weakenE) 58 apply simp 59 done 60 61(* FIXME: MOVE to EmptyFail *) 62lemma empty_fail_archThreadGet [intro!, wp, simp]: 63 "empty_fail (archThreadGet f p)" 64 by (simp add: archThreadGet_def getObject_def split_def) 65 66lemma ccorres_pre_archThreadGet: 67 assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (g rv) c" 68 shows "ccorres r xf 69 (\<lambda>s. \<forall>tcb. ko_at' tcb p s \<longrightarrow> P (f (tcbArch tcb)) s) 70 ({s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr p) = Some ctcb 71 \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> P' (f (tcbArch tcb))}) 72 hs (archThreadGet f p >>= (\<lambda>rv. g rv)) c" 73 apply (rule ccorres_guard_imp) 74 apply (rule ccorres_symb_exec_l) 75 defer 76 apply wp[1] 77 apply (rule atg_sp') 78 apply simp 79 apply assumption 80 defer 81 apply (rule ccorres_guard_imp) 82 apply (rule cc) 83 apply clarsimp 84 apply (frule obj_at_ko_at') 85 apply clarsimp 86 apply assumption 87 apply clarsimp 88 apply (frule (1) obj_at_cslift_tcb) 89 apply clarsimp 90 done 91 92lemma threadGet_eq: 93 "ko_at' tcb thread s \<Longrightarrow> (f tcb, s) \<in> fst (threadGet f thread s)" 94 unfolding threadGet_def 95 apply (simp add: liftM_def in_monad) 96 apply (rule exI [where x = tcb]) 97 apply simp 98 apply (subst getObject_eq) 99 apply simp 100 apply (simp add: objBits_simps') 101 apply assumption 102 apply simp 103 done 104 105lemma archThreadGet_eq: 106 "ko_at' tcb thread s \<Longrightarrow> (f (tcbArch tcb), s) \<in> fst (archThreadGet f thread s)" 107 unfolding archThreadGet_def 108 apply (simp add: liftM_def in_monad) 109 apply (rule exI [where x = tcb]) 110 apply simp 111 apply (subst getObject_eq) 112 apply simp 113 apply (simp add: objBits_simps') 114 apply assumption 115 apply simp 116 done 117 118lemma get_tsType_ccorres [corres]: 119 "ccorres (\<lambda>r r'. r' = thread_state_to_tsType r) ret__unsigned_' (tcb_at' thread) 120 (UNIV \<inter> {s. thread_state_ptr_' s = Ptr &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])}) [] 121 (getThreadState thread) (Call thread_state_ptr_get_tsType_'proc)" 122 unfolding getThreadState_def 123 apply (rule ccorres_from_spec_modifies) 124 apply (rule thread_state_ptr_get_tsType_spec) 125 apply (rule thread_state_ptr_get_tsType_modifies) 126 apply simp 127 apply (frule (1) obj_at_cslift_tcb) 128 apply (clarsimp simp: typ_heap_simps) 129 apply (frule (1) obj_at_cslift_tcb) 130 apply (clarsimp simp: typ_heap_simps) 131 apply (rule bexI [rotated, OF threadGet_eq], assumption) 132 apply simp 133 apply (erule ctcb_relation_thread_state_to_tsType) 134 done 135 136lemma threadGet_obj_at2: 137 "\<lbrace>\<top>\<rbrace> threadGet f thread \<lbrace>\<lambda>v. obj_at' (\<lambda>t. f t = v) thread\<rbrace>" 138 apply (rule hoare_post_imp) 139 prefer 2 140 apply (rule tg_sp') 141 apply simp 142 done 143 144lemma register_from_H_less: 145 "register_from_H hr < 20" 146 by (cases hr, simp_all add: "StrictC'_register_defs") 147 148lemma register_from_H_sless: 149 "register_from_H hr <s 20" 150 by (cases hr, simp_all add: "StrictC'_register_defs" word_sless_def word_sle_def) 151 152lemma register_from_H_0_sle[simp]: 153 "0 <=s register_from_H hr" 154 using word_0_sle_from_less[OF order_less_le_trans] register_from_H_less 155 by fastforce 156 157lemma getRegister_ccorres [corres]: 158 "ccorres (=) ret__unsigned_long_' \<top> 159 ({s. thread_' s = tcb_ptr_to_ctcb_ptr thread} \<inter> {s. reg_' s = register_from_H reg}) [] 160 (asUser thread (getRegister reg)) (Call getRegister_'proc)" 161 apply (unfold asUser_def) 162 apply (rule ccorres_guard_imp) 163 apply (rule ccorres_symb_exec_l [where Q="\<lambda>u. obj_at' (\<lambda>t. (atcbContextGet o tcbArch) t = u) thread" and 164 Q'="\<lambda>rv. {s. thread_' s = tcb_ptr_to_ctcb_ptr thread} \<inter> {s. reg_' s = register_from_H reg}"]) 165 apply (rule ccorres_from_vcg) 166 apply (rule allI, rule conseqPre) 167 apply vcg 168 apply clarsimp 169 apply (drule (1) obj_at_cslift_tcb) 170 apply (clarsimp simp: typ_heap_simps register_from_H_less register_from_H_sless) 171 apply (clarsimp simp: getRegister_def typ_heap_simps) 172 apply (rule_tac x = "((atcbContextGet o tcbArch) ko reg, \<sigma>)" in bexI [rotated]) 173 apply (simp add: in_monad' asUser_def select_f_def split_def) 174 apply (subst arg_cong2 [where f = "(\<in>)"]) 175 defer 176 apply (rule refl) 177 apply (erule threadSet_eq) 178 apply (clarsimp simp: ctcb_relation_def ccontext_relation_def carch_tcb_relation_def) 179 apply (wp threadGet_obj_at2)+ 180 apply simp 181 apply simp 182 apply (erule obj_atE') 183 apply (clarsimp simp: projectKOs ) 184 apply (subst fun_upd_idem) 185 apply (case_tac ko) 186 apply clarsimp 187 apply simp 188 done 189 190lemma getRestartPC_ccorres [corres]: 191 "ccorres (=) ret__unsigned_long_' \<top> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> [] 192 (asUser thread getRestartPC) (Call getRestartPC_'proc)" 193 unfolding getRestartPC_def 194 apply (cinit') 195 apply (rule ccorres_add_return2, ctac) 196 apply (rule ccorres_return_C, simp+)[1] 197 apply wp 198 apply vcg 199 apply (simp add: scast_id) 200 done 201 202lemma threadSet_corres_lemma: 203 assumes spec: "\<forall>s. \<Gamma>\<turnstile> \<lbrace>s. P s\<rbrace> Call f {t. Q s t}" 204 and mod: "modifies_heap_spec f" 205 and rl: "\<And>\<sigma> x t ko. \<lbrakk>(\<sigma>, x) \<in> rf_sr; Q x t; x \<in> P'; ko_at' ko thread \<sigma>\<rbrakk> 206 \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := ksPSpace \<sigma>(thread \<mapsto> KOTCB (g ko))\<rparr>, 207 t\<lparr>globals := globals x\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>) \<in> rf_sr" 208 and g: "\<And>s x. \<lbrakk>tcb_at' thread s; x \<in> P'; (s, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> P x" 209 shows "ccorres dc xfdc (tcb_at' thread) P' [] (threadSet g thread) (Call f)" 210 apply (rule ccorres_Call_call_for_vcg) 211 apply (rule ccorres_from_vcg) 212 apply (rule allI, rule conseqPre) 213 apply (rule HoarePartial.ProcModifyReturnNoAbr [where return' = "\<lambda>s t. t\<lparr> globals := globals s\<lparr>t_hrs_' := t_hrs_' (globals t) \<rparr>\<rparr>"]) 214 apply (rule HoarePartial.ProcSpecNoAbrupt [OF _ _ spec]) 215 apply (rule subset_refl) 216 apply vcg 217 prefer 2 218 apply (rule mod) 219 apply (clarsimp simp: mex_def meq_def) 220 apply clarsimp 221 apply (rule conjI) 222 apply (erule (2) g) 223 apply clarsimp 224 apply (frule obj_at_ko_at') 225 apply clarsimp 226 apply (rule bexI [rotated]) 227 apply (erule threadSet_eq) 228 apply simp 229 apply (rule_tac x1 = "t\<lparr>globals := globals x\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>" in iffD1 [OF rf_sr_upd], simp_all)[1] 230 apply (erule (3) rl) 231 done 232 233 234lemma threadSet_ccorres_lemma4: 235 "\<lbrakk> \<And>s tcb. \<Gamma> \<turnstile> (Q s tcb) c {s'. (s \<lparr>ksPSpace := ksPSpace s(thread \<mapsto> injectKOS (F tcb))\<rparr>, s') \<in> rf_sr}; 236 \<And>s s' tcb tcb'. \<lbrakk> (s, s') \<in> rf_sr; P tcb; ko_at' tcb thread s; 237 cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; 238 ctcb_relation tcb tcb'; P' s ; s' \<in> R\<rbrakk> \<Longrightarrow> s' \<in> Q s tcb \<rbrakk> 239 \<Longrightarrow> ccorres dc xfdc (obj_at' (P :: tcb \<Rightarrow> bool) thread and P') R hs (threadSet F thread) c" 240 apply (rule ccorres_from_vcg) 241 apply (rule allI) 242 apply (case_tac "obj_at' P thread \<sigma>") 243 apply (drule obj_at_ko_at', clarsimp) 244 apply (rule conseqPre, rule conseqPost) 245 apply assumption 246 apply clarsimp 247 apply (rule rev_bexI, rule threadSet_eq) 248 apply assumption 249 apply simp 250 apply simp 251 apply clarsimp 252 apply (drule(1) obj_at_cslift_tcb, clarsimp) 253 apply simp 254 apply (rule hoare_complete') 255 apply (simp add: cnvalid_def nvalid_def) (* pretty *) 256 done 257 258lemmas threadSet_ccorres_lemma3 = threadSet_ccorres_lemma4[where R=UNIV] 259 260lemmas threadSet_ccorres_lemma2 261 = threadSet_ccorres_lemma3[where P'=\<top>] 262 263lemma ctcb_relation_tcbVCPU: 264 "ctcb_relation t ko' \<Longrightarrow> tcbVCPU_C (tcbArch_C ko') = option_to_ptr (atcbVCPUPtr (tcbArch t))" 265 unfolding ctcb_relation_def carch_tcb_relation_def ccontext_relation_def 266 by clarsimp 267 268lemma is_aligned_tcb_ptr_to_ctcb_ptr: 269 "obj_at' (P :: tcb \<Rightarrow> bool) p s 270 \<Longrightarrow> is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr p)) ctcb_size_bits" 271 apply (clarsimp simp: obj_at'_def objBits_simps' projectKOs 272 tcb_ptr_to_ctcb_ptr_def ctcb_offset_defs) 273 apply (erule aligned_add_aligned, simp_all add: word_bits_conv) 274 apply (simp add: is_aligned_def) 275 done 276 277lemma valid_tcb'_vcpuE [elim_format]: 278 "valid_tcb' t s \<Longrightarrow> atcbVCPUPtr (tcbArch t) = Some v \<Longrightarrow> vcpu_at' v s" 279 unfolding valid_tcb'_def valid_arch_tcb'_def 280 by auto 281 282lemma sanitiseRegister_spec: 283 "\<forall>s t v r. \<Gamma> \<turnstile> ({s} \<inter> \<lbrace>\<acute>v = v\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H r\<rbrace> \<inter> \<lbrace>\<acute>archInfo = from_bool t\<rbrace>) 284 Call sanitiseRegister_'proc 285 \<lbrace>\<acute>ret__unsigned_long = sanitiseRegister t r v\<rbrace>" 286 apply vcg 287 apply (auto simp: C_register_defs sanitiseRegister_def word_0_sle_from_less 288 split: register.split) 289 done 290 291lemma rf_sr_ksArchState_armHSCurVCPU: 292 "(s, s') \<in> rf_sr \<Longrightarrow> cur_vcpu_relation (armHSCurVCPU (ksArchState s)) (armHSCurVCPU_' (globals s')) (armHSVCPUActive_' (globals s'))" 293 by (clarsimp simp: rf_sr_def cstate_relation_def carch_state_relation_def Let_def) 294 295lemma ccorres_pre_getCurVCPU: 296 assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c" 297 shows "ccorres r xf 298 (\<lambda>s. (\<forall>rv. (armHSCurVCPU \<circ> ksArchState) s = rv \<longrightarrow> P rv s)) 299 {s. \<forall>rv vcpu' act'. armHSCurVCPU_' (globals s) = vcpu' \<and> 300 armHSVCPUActive_' (globals s) = act' \<and> 301 cur_vcpu_relation rv vcpu' act' 302 \<longrightarrow> s \<in> P' rv } 303 hs (gets (armHSCurVCPU \<circ> ksArchState) >>= (\<lambda>rv. f rv)) c" 304 apply (rule ccorres_guard_imp) 305 apply (rule ccorres_symb_exec_l) 306 defer 307 apply wp 308 apply (rule hoare_gets_sp) 309 apply (clarsimp simp: empty_fail_def getCurThread_def simpler_gets_def) 310 apply assumption 311 apply clarsimp 312 defer 313 apply (rule ccorres_guard_imp) 314 apply (rule cc) 315 apply clarsimp 316 apply assumption 317 apply (clarsimp simp: rf_sr_ksArchState_armHSCurVCPU) 318 done 319 320lemma getObject_tcb_wp': 321 "\<lbrace>\<lambda>s. \<forall>t. ko_at' (t :: tcb) p s \<longrightarrow> Q t s\<rbrace> getObject p \<lbrace>Q\<rbrace>" 322 by (clarsimp simp: getObject_def valid_def in_monad 323 split_def objBits_simps' loadObject_default_def 324 projectKOs obj_at'_def in_magnitude_check) 325 326lemma ccorres_pre_getObject_tcb: 327 assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c" 328 shows "ccorres r xf 329 (\<lambda>s. (\<forall>tcb. ko_at' tcb p s \<longrightarrow> P tcb s)) 330 {s. \<forall> tcb tcb'. cslift s (tcb_ptr_to_ctcb_ptr p) = Some tcb' \<and> ctcb_relation tcb tcb' 331 \<longrightarrow> s \<in> P' tcb} 332 hs (getObject p >>= (\<lambda>rv :: tcb. f rv)) c" 333 apply (rule ccorres_guard_imp2) 334 apply (rule ccorres_symb_exec_l) 335 apply (rule ccorres_guard_imp2) 336 apply (rule cc) 337 apply (rule conjI) 338 apply (rule_tac Q="ko_at' rv p s" in conjunct1) 339 apply assumption 340 apply assumption 341 apply (wpsimp wp: empty_fail_getObject getObject_tcb_wp')+ 342 apply (erule cmap_relationE1[OF cmap_relation_tcb], 343 erule ko_at_projectKO_opt) 344 apply simp 345 done 346 347lemma ccorres_pre_getObject_vcpu: 348 assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c" 349 shows "ccorres r xf 350 (\<lambda>s. (\<forall>vcpu. ko_at' vcpu p s \<longrightarrow> P vcpu s)) 351 {s. \<forall> vcpu vcpu'. cslift s (vcpu_Ptr p) = Some vcpu' \<and> cvcpu_relation vcpu vcpu' 352 \<longrightarrow> s \<in> P' vcpu} 353 hs (getObject p >>= (\<lambda>rv :: vcpu. f rv)) c" 354 apply (rule ccorres_guard_imp2) 355 apply (rule ccorres_symb_exec_l) 356 apply (rule ccorres_guard_imp2) 357 apply (rule cc) 358 apply (rule conjI) 359 apply (rule_tac Q="ko_at' rv p s" in conjunct1) 360 apply assumption 361 apply assumption 362 apply (wpsimp wp: getVCPU_wp empty_fail_getObject)+ 363 apply (erule cmap_relationE1 [OF cmap_relation_vcpu], 364 erule ko_at_projectKO_opt) 365 apply simp 366 done 367 368lemma armHSCurVCPU_update_active_ccorres: 369 "b' = from_bool b \<Longrightarrow> v' = fst v \<Longrightarrow> 370 ccorres dc xfdc (\<lambda>s. armHSCurVCPU (ksArchState s) = Some v) UNIV hs 371 (modifyArchState (armHSCurVCPU_update (\<lambda>_. Some (v', b)))) 372 (Basic (\<lambda>s. globals_update (armHSVCPUActive_'_update (\<lambda>_. b')) s))" 373 apply (clarsimp simp: modifyArchState_def) 374 apply (rule ccorres_from_vcg) 375 apply (rule allI, rule conseqPre, vcg) 376 apply (clarsimp simp: bind_def simpler_gets_def from_bool_def simpler_modify_def) 377 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def) 378 by (clarsimp simp: carch_state_relation_def carch_globals_def cur_vcpu_relation_def 379 cmachine_state_relation_def from_bool_def 380 split: bool.split) 381 382lemma armHSCurVCPU_update_curv_ccorres: 383 "ccorres dc xfdc (\<lambda>s. ((armHSCurVCPU (ksArchState s)) = Some (v, a)) \<and> v \<noteq> 0 \<and> new \<noteq> 0) UNIV hs 384 (modifyArchState (armHSCurVCPU_update (\<lambda>_. Some (new, a)))) 385 (Basic (\<lambda>s. globals_update (armHSCurVCPU_'_update (\<lambda>_. Ptr new)) s))" 386 apply (clarsimp simp: modifyArchState_def) 387 apply (rule ccorres_from_vcg) 388 apply (rule allI, rule conseqPre, vcg) 389 apply (clarsimp simp: bind_def simpler_gets_def simpler_modify_def) 390 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def) 391 by (clarsimp simp: carch_state_relation_def carch_globals_def cur_vcpu_relation_def 392 cmachine_state_relation_def from_bool_def true_def false_def 393 split: bool.split) 394 395lemma armHSCurVCPU_update_ccorres: 396 "ccorres dc xfdc (\<lambda>_. cur_vcpu_relation curv vcpu act) UNIV hs 397 (modifyArchState (armHSCurVCPU_update (\<lambda>_. curv))) 398 (Basic (\<lambda>s. globals_update (armHSCurVCPU_'_update (\<lambda>_. vcpu)) s);; 399 Basic (\<lambda>s. globals_update (armHSVCPUActive_'_update (\<lambda>_. act)) s))" 400 apply (clarsimp simp: modifyArchState_def) 401 apply (rule ccorres_from_vcg) 402 apply (rule allI, rule conseqPre, vcg) 403 apply (clarsimp simp: bind_def simpler_gets_def simpler_modify_def) 404 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def) 405 by (clarsimp simp: carch_state_relation_def carch_globals_def cur_vcpu_relation_def 406 cmachine_state_relation_def from_bool_def true_def false_def 407 split: bool.split) 408 409lemmas armHSCurVCPU_update_active_ccorres2 = armHSCurVCPU_update_ccorres[where curv="Some (v, b)" for v b] 410 411lemma invs'_HScurVCPU_vcpu_at': 412 "\<lbrakk>invs' s; armHSCurVCPU (ksArchState s) = Some (a, b) \<rbrakk> \<Longrightarrow> vcpu_at' a s" 413by (fastforce dest: invs_arch_state' simp: valid_arch_state'_def vcpu_at_is_vcpu' ko_wp_at'_def split: option.splits) 414 415crunch ksArch[wp]: vcpuDisable, vcpuRestore, vcpuSave, vcpuEnable "\<lambda>s. P (ksArchState s)" 416 (ignore: getObject setObject wp: crunch_wps) 417 418(* FIXME move to Invariants_H *) 419lemma invs_cicd_arch_state' [elim!]: 420 "all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> valid_arch_state' s" 421 by (simp add: all_invs_but_ct_idle_or_in_cur_domain'_def valid_state'_def) 422 423(* FIXME move to Invariants_H *) 424lemma invs_cicd_no_0_obj'[elim!]: 425 "all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> no_0_obj' s" 426 by (simp add: all_invs_but_ct_idle_or_in_cur_domain'_def valid_state'_def valid_pspace'_def) 427 428(* FIXME: move *) 429lemma vcpu_at_ko: 430 "vcpu_at' p s \<Longrightarrow> \<exists>vcpu. ko_at' (vcpu::vcpu) p s" 431 apply (clarsimp simp: typ_at'_def obj_at'_def ko_wp_at'_def projectKOs) 432 apply (case_tac ko; simp) 433 apply (rename_tac arch_kernel_object) 434 apply (case_tac arch_kernel_object, auto)[1] 435 done 436 437(* FIXME: move *) 438lemma vcpu_at_c_guard: 439 "\<lbrakk>vcpu_at' p s; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> c_guard (vcpu_Ptr p)" 440 by (fastforce intro: typ_heap_simps dest!: vcpu_at_ko vcpu_at_rf_sr) 441 442(* FIXME: MOVE, probably to CSpace_RAB *) 443lemma ccorres_gen_asm2_state: 444 assumes rl: "\<And>s. P s \<Longrightarrow> ccorres r xf G G' hs a c" 445 shows "ccorres r xf G (G' \<inter> {s. P s}) hs a c" 446proof (rule ccorres_guard_imp2) 447 show "ccorres r xf G (G' \<inter> {_. \<exists>s. P s}) hs a c" 448 apply (rule ccorres_gen_asm2) 449 apply (erule exE) 450 apply (erule rl) 451 done 452next 453 fix s s' 454 assume "(s, s') \<in> rf_sr" and "G s" and "s' \<in> G' \<inter> {s. P s}" 455 thus "G s \<and> s' \<in> (G' \<inter> {_. \<exists>s. P s})" 456 by (clarsimp elim!: exI simp: Collect_const_mem) 457qed 458 459lemma cap_case_TCBCap2: 460 "(case cap of ThreadCap pd 461 \<Rightarrow> f pd | _ \<Rightarrow> g) 462 = (if isThreadCap cap 463 then f (capTCBPtr cap) 464 else g)" 465 by (simp add: isCap_simps 466 split: capability.split arch_capability.split) 467 468(* FIXME move *) 469lemma ccorres_pre_gets_armKSGICVCPUNumListRegs_ksArchState: 470 assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c" 471 shows "ccorres r xf 472 (\<lambda>s. (\<forall>rv. (armKSGICVCPUNumListRegs \<circ> ksArchState) s = rv \<longrightarrow> P rv s)) 473 {s. \<forall>rv vcpu' act'. of_nat rv = gic_vcpu_num_list_regs_' (globals s) 474 \<longrightarrow> s \<in> P' rv } 475 hs (gets (armKSGICVCPUNumListRegs \<circ> ksArchState) >>= (\<lambda>rv. f rv)) c" 476 apply (rule ccorres_guard_imp) 477 apply (rule ccorres_symb_exec_l) 478 defer 479 apply wp[1] 480 apply (rule gets_sp) 481 apply (clarsimp simp: empty_fail_def simpler_gets_def) 482 apply assumption 483 apply clarsimp 484 defer 485 apply (rule ccorres_guard_imp) 486 apply (rule cc) 487 apply clarsimp 488 apply assumption 489 apply (simp add: rf_sr_armKSGICVCPUNumListRegs) 490 done 491 492 493lemma length_of_msgRegisters: 494 "length ARM_HYP_H.msgRegisters = 4" 495 by (auto simp: msgRegisters_unfold) 496 497lemma setMRs_single: 498 "setMRs thread buffer [val] = do y \<leftarrow> asUser thread (setRegister register.R2 val); 499 return 1 500 od" 501 apply (clarsimp simp: setMRs_def length_of_msgRegisters zipWithM_x_def zipWith_def split: option.splits) 502 apply (subst zip_commute, subst zip_singleton) 503 apply (simp add: length_of_msgRegisters length_0_conv[symmetric]) 504 apply (clarsimp simp: msgRegisters_unfold sequence_x_def) 505 done 506 507end 508end 509