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 IsolatedThreadAction 12imports "CLib.MonadicRewrite_C" Finalise_C CSpace_All SyscallArgs_C 13begin 14 15context begin interpretation Arch . 16 17datatype tcb_state_regs = TCBStateRegs "thread_state" "MachineTypes.register \<Rightarrow> machine_word" 18 19definition 20 "tsrContext tsr \<equiv> case tsr of TCBStateRegs ts regs \<Rightarrow> regs" 21 22definition 23 "tsrState tsr \<equiv> case tsr of TCBStateRegs ts regs \<Rightarrow> ts" 24 25lemma accessors_TCBStateRegs[simp]: 26 "TCBStateRegs (tsrState v) (tsrContext v) = v" 27 by (cases v, simp add: tsrState_def tsrContext_def) 28 29lemma tsrContext_simp[simp]: 30 "tsrContext (TCBStateRegs st con) = con" 31 by (simp add: tsrContext_def) 32 33lemma tsrState_simp[simp]: 34 "tsrState (TCBStateRegs st con) = st" 35 by (simp add: tsrState_def) 36 37definition 38 get_tcb_state_regs :: "kernel_object option \<Rightarrow> tcb_state_regs" 39where 40 "get_tcb_state_regs oko \<equiv> case oko of 41 Some (KOTCB tcb) \<Rightarrow> TCBStateRegs (tcbState tcb) ((user_regs o atcbContextGet o tcbArch) tcb)" 42 43definition 44 put_tcb_state_regs_tcb :: "tcb_state_regs \<Rightarrow> tcb \<Rightarrow> tcb" 45where 46 "put_tcb_state_regs_tcb tsr tcb \<equiv> case tsr of 47 TCBStateRegs st regs \<Rightarrow> 48 tcb \<lparr> tcbState := st, 49 tcbArch := atcbContextSet (UserContext (fpu_state (atcbContext (tcbArch tcb))) regs) 50 (tcbArch tcb) \<rparr>" 51 52definition 53 put_tcb_state_regs :: "tcb_state_regs \<Rightarrow> kernel_object option \<Rightarrow> kernel_object option" 54where 55 "put_tcb_state_regs tsr oko = Some (KOTCB (put_tcb_state_regs_tcb tsr 56 (case oko of 57 Some (KOTCB tcb) \<Rightarrow> tcb | _ \<Rightarrow> makeObject)))" 58 59definition 60 "partial_overwrite idx tcbs ps \<equiv> 61 \<lambda>x. if x \<in> range idx 62 then put_tcb_state_regs (tcbs (inv idx x)) (ps x) 63 else ps x" 64 65definition 66 isolate_thread_actions :: "('x \<Rightarrow> machine_word) \<Rightarrow> 'a kernel 67 \<Rightarrow> (('x \<Rightarrow> tcb_state_regs) \<Rightarrow> ('x \<Rightarrow> tcb_state_regs)) 68 \<Rightarrow> (scheduler_action \<Rightarrow> scheduler_action) 69 \<Rightarrow> 'a kernel" 70 where 71 "isolate_thread_actions idx m t f \<equiv> do 72 s \<leftarrow> gets (ksSchedulerAction_update (\<lambda>_. ResumeCurrentThread) 73 o ksPSpace_update (partial_overwrite idx (K undefined))); 74 tcbs \<leftarrow> gets (\<lambda>s. get_tcb_state_regs o ksPSpace s o idx); 75 sa \<leftarrow> getSchedulerAction; 76 (rv, s') \<leftarrow> select_f (m s); 77 modify (\<lambda>s. ksPSpace_update (partial_overwrite idx (t tcbs)) 78 (s' \<lparr> ksSchedulerAction := f sa \<rparr>)); 79 return rv 80 od" 81 82lemma UserContextGet[simp]: 83 "UserContext (fpu_state (atcbContext t)) (user_regs (atcbContextGet t)) = atcbContextGet t" 84 by (cases t, simp add: atcbContextGet_def) 85 86lemma put_tcb_state_regs_twice[simp]: 87 "put_tcb_state_regs tsr (put_tcb_state_regs tsr' tcb) 88 = put_tcb_state_regs tsr tcb" 89 apply (simp add: put_tcb_state_regs_def put_tcb_state_regs_tcb_def 90 atcbContextSet_def 91 makeObject_tcb newArchTCB_def newContext_def initContext_def 92 split: tcb_state_regs.split option.split 93 Structures_H.kernel_object.split) 94 apply (intro all_tcbI impI allI) 95 apply (case_tac q, simp) 96 done 97 98lemma partial_overwrite_twice[simp]: 99 "partial_overwrite idx f (partial_overwrite idx g ps) 100 = partial_overwrite idx f ps" 101 by (rule ext, simp add: partial_overwrite_def) 102 103lemma get_tcb_state_regs_partial_overwrite[simp]: 104 "inj idx \<Longrightarrow> 105 get_tcb_state_regs (partial_overwrite idx tcbs f (idx x)) 106 = tcbs x" 107 apply (simp add: partial_overwrite_def) 108 apply (simp add: put_tcb_state_regs_def 109 get_tcb_state_regs_def 110 put_tcb_state_regs_tcb_def 111 split: tcb_state_regs.split) 112 done 113 114lemma isolate_thread_actions_bind: 115 "inj idx \<Longrightarrow> 116 isolate_thread_actions idx a b c >>= 117 (\<lambda>x. isolate_thread_actions idx (d x) e f) 118 = isolate_thread_actions idx a id id 119 >>= (\<lambda>x. isolate_thread_actions idx (d x) (e o b) (f o c))" 120 apply (rule ext) 121 apply (clarsimp simp: isolate_thread_actions_def bind_assoc split_def 122 bind_select_f_bind[symmetric]) 123 apply (clarsimp simp: exec_gets getSchedulerAction_def) 124 apply (rule select_bind_eq) 125 apply (simp add: exec_gets exec_modify o_def) 126 apply (rule select_bind_eq) 127 apply (simp add: exec_gets exec_modify) 128 done 129 130lemmas setEndpoint_obj_at_tcb' = setEndpoint_obj_at'_tcb 131 132lemma tcbSchedEnqueue_obj_at_unchangedT: 133 assumes y: "\<And>f. \<forall>tcb. P (tcbQueued_update f tcb) = P tcb" 134 shows "\<lbrace>obj_at' P t\<rbrace> tcbSchedEnqueue t' \<lbrace>\<lambda>rv. obj_at' P t\<rbrace>" 135 apply (simp add: tcbSchedEnqueue_def unless_def) 136 apply (wp | simp add: y)+ 137 done 138 139lemma asUser_obj_at_notQ: 140 "\<lbrace>obj_at' (Not \<circ> tcbQueued) t\<rbrace> 141 asUser t (setRegister r v) 142 \<lbrace>\<lambda>rv. obj_at' (Not \<circ> tcbQueued) t\<rbrace>" 143 apply (simp add: asUser_def) 144 apply (rule hoare_seq_ext)+ 145 apply (simp add: split_def) 146 apply (rule threadSet_obj_at'_really_strongest) 147 apply (wp threadGet_wp |rule gets_inv|wpc|clarsimp)+ 148 apply (clarsimp simp: obj_at'_def) 149 done 150 151(* FIXME: Move to Schedule_R.thy. Make Arch_switchToThread_obj_at a specialisation of this *) 152lemma Arch_switchToThread_obj_at_pre: 153 "\<lbrace>obj_at' (Not \<circ> tcbQueued) t\<rbrace> 154 Arch.switchToThread t 155 \<lbrace>\<lambda>rv. obj_at' (Not \<circ> tcbQueued) t\<rbrace>" 156 apply (simp add: X64_H.switchToThread_def) 157 apply (wp asUser_obj_at_notQ doMachineOp_obj_at hoare_drop_imps|wpc)+ 158 done 159 160lemma rescheduleRequired_obj_at_unchangedT: 161 assumes y: "\<And>f. \<forall>tcb. P (tcbQueued_update f tcb) = P tcb" 162 shows "\<lbrace>obj_at' P t\<rbrace> rescheduleRequired \<lbrace>\<lambda>rv. obj_at' P t\<rbrace>" 163 apply (simp add: rescheduleRequired_def) 164 apply (wp tcbSchedEnqueue_obj_at_unchangedT[OF y] | wpc)+ 165 apply simp 166 done 167 168lemma setThreadState_obj_at_unchangedT: 169 assumes x: "\<And>f. \<forall>tcb. P (tcbState_update f tcb) = P tcb" 170 assumes y: "\<And>f. \<forall>tcb. P (tcbQueued_update f tcb) = P tcb" 171 shows "\<lbrace>obj_at' P t\<rbrace> setThreadState t' ts \<lbrace>\<lambda>rv. obj_at' P t\<rbrace>" 172 apply (simp add: setThreadState_def) 173 apply (wp rescheduleRequired_obj_at_unchangedT[OF y], simp) 174 apply (wp threadSet_obj_at'_strongish) 175 apply (clarsimp simp: obj_at'_def projectKOs x cong: if_cong) 176 done 177 178lemma setBoundNotification_obj_at_unchangedT: 179 assumes x: "\<And>f. \<forall>tcb. P (tcbBoundNotification_update f tcb) = P tcb" 180 shows "\<lbrace>obj_at' P t\<rbrace> setBoundNotification t' ts \<lbrace>\<lambda>rv. obj_at' P t\<rbrace>" 181 apply (simp add: setBoundNotification_def) 182 apply (wp threadSet_obj_at'_strongish) 183 apply (clarsimp simp: obj_at'_def projectKOs x cong: if_cong) 184 done 185 186lemmas setThreadState_obj_at_unchanged 187 = setThreadState_obj_at_unchangedT[OF all_tcbI all_tcbI] 188 189lemmas setBoundNotification_obj_at_unchanged 190 = setBoundNotification_obj_at_unchangedT[OF all_tcbI] 191 192lemmas setNotification_tcb = set_ntfn_tcb_obj_at' 193 194(* FIXME: move *) 195lemmas threadSet_obj_at' = threadSet_obj_at'_strongish 196 197end 198 199context kernel_m begin 200 201context begin interpretation Arch . (*FIXME: arch_split*) 202 203lemma getObject_return: 204 fixes v :: "'a :: pspace_storable" shows 205 "\<lbrakk> \<And>a b c d. (loadObject a b c d :: 'a kernel) = loadObject_default a b c d; 206 ko_at' v p s; (1 :: machine_word) < 2 ^ objBits v \<rbrakk> \<Longrightarrow> getObject p s = return v s" 207 apply (clarsimp simp: getObject_def split_def exec_gets 208 obj_at'_def projectKOs lookupAround2_known1 209 assert_opt_def loadObject_default_def) 210 apply (simp add: projectKO_def alignCheck_assert) 211 apply (simp add: project_inject objBits_def) 212 apply (frule(2) in_magnitude_check[where s'=s]) 213 apply (simp add: magnitudeCheck_assert in_monad) 214 done 215 216end 217 218lemmas getObject_return_tcb 219 = getObject_return[OF meta_eq_to_obj_eq, OF loadObject_tcb, 220 unfolded objBits_simps, simplified] 221 222lemmas setObject_modify_tcb 223 = setObject_modify[OF _ meta_eq_to_obj_eq, OF _ updateObject_tcb, 224 unfolded objBits_simps, simplified] 225 226lemma partial_overwrite_fun_upd: 227 "inj idx \<Longrightarrow> 228 partial_overwrite idx (tsrs (x := y)) 229 = (\<lambda>ps. (partial_overwrite idx tsrs ps) (idx x := put_tcb_state_regs y (ps (idx x))))" 230 apply (intro ext, simp add: partial_overwrite_def) 231 apply (clarsimp split: if_split) 232 done 233 234lemma get_tcb_state_regs_ko_at': 235 "ko_at' ko p s \<Longrightarrow> get_tcb_state_regs (ksPSpace s p) 236 = TCBStateRegs (tcbState ko) ((user_regs o atcbContextGet o tcbArch) ko)" 237 by (clarsimp simp: obj_at'_def projectKOs get_tcb_state_regs_def) 238 239lemma put_tcb_state_regs_ko_at': 240 "ko_at' ko p s \<Longrightarrow> put_tcb_state_regs tsr (ksPSpace s p) 241 = Some (KOTCB (ko \<lparr> tcbState := tsrState tsr 242 , tcbArch := atcbContextSet (UserContext (fpu_state (atcbContext (tcbArch ko))) (tsrContext tsr)) (tcbArch ko)\<rparr>))" 243 by (clarsimp simp: obj_at'_def projectKOs put_tcb_state_regs_def 244 put_tcb_state_regs_tcb_def 245 split: tcb_state_regs.split) 246 247lemma partial_overwrite_get_tcb_state_regs: 248 "\<lbrakk> \<forall>x. tcb_at' (idx x) s; inj idx \<rbrakk> \<Longrightarrow> 249 partial_overwrite idx (\<lambda>x. get_tcb_state_regs (ksPSpace s (idx x))) 250 (ksPSpace s) = ksPSpace s" 251 apply (rule ext, simp add: partial_overwrite_def 252 split: if_split) 253 apply clarsimp 254 apply (drule_tac x=xa in spec) 255 apply (clarsimp simp: obj_at'_def projectKOs put_tcb_state_regs_def 256 get_tcb_state_regs_def put_tcb_state_regs_tcb_def) 257 apply (case_tac obj, simp) 258 done 259 260lemma ksPSpace_update_partial_id: 261 "\<lbrakk> \<And>ps x. f ps x = ps (idx x) \<or> f ps x = ksPSpace s (idx x); 262 \<forall>x. tcb_at' (idx x) s; inj idx \<rbrakk> \<Longrightarrow> 263 ksPSpace_update (\<lambda>ps. partial_overwrite idx (\<lambda>x. get_tcb_state_regs (f ps x)) ps) s 264 = s" 265 apply (rule trans, rule kernel_state.fold_congs[OF refl refl]) 266 apply (erule_tac x="ksPSpace s" in meta_allE) 267 apply (clarsimp simp: partial_overwrite_get_tcb_state_regs) 268 apply (rule refl) 269 apply simp 270 done 271 272lemma isolate_thread_actions_asUser: 273 "\<lbrakk> idx t' = t; inj idx; f = (\<lambda>s. ({(v, modify_registers g s)}, False)) \<rbrakk> \<Longrightarrow> 274 monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) 275 (asUser t f) 276 (isolate_thread_actions idx (return v) 277 (\<lambda>tsrs. (tsrs (t' := TCBStateRegs (tsrState (tsrs t')) 278 (g (tsrContext (tsrs t')))))) 279 id)" 280 apply (simp add: asUser_def liftM_def isolate_thread_actions_def split_def 281 select_f_returns bind_assoc select_f_singleton_return 282 threadGet_def threadSet_def) 283 apply (clarsimp simp: monadic_rewrite_def) 284 apply (frule_tac x=t' in spec) 285 apply (drule obj_at_ko_at', clarsimp) 286 apply (simp add: exec_gets getSchedulerAction_def exec_modify objBits_defs 287 getObject_return_tcb setObject_modify_tcb o_def 288 cong: bind_apply_cong)+ 289 apply (simp add: partial_overwrite_fun_upd return_def get_tcb_state_regs_ko_at') 290 apply (rule kernel_state.fold_congs[OF refl refl]) 291 apply (clarsimp simp: partial_overwrite_get_tcb_state_regs 292 put_tcb_state_regs_ko_at') 293 apply (case_tac ko, simp) 294 apply (rename_tac uc) 295 apply (case_tac uc, simp add: modify_registers_def atcbContextGet_def atcbContextSet_def) 296 done 297 298lemma getRegister_simple: 299 "getRegister r = (\<lambda>con. ({(user_regs con r, con)}, False))" 300 by (simp add: getRegister_def simpler_gets_def) 301 302lemma mapM_getRegister_simple: 303 "mapM getRegister rs = (\<lambda>con. ({(map (user_regs con) rs, con)}, False))" 304 apply (induct rs) 305 apply (simp add: mapM_Nil return_def) 306 apply (simp add: mapM_Cons getRegister_def simpler_gets_def 307 bind_def return_def) 308 done 309 310lemma setRegister_simple: 311 "setRegister r v = (\<lambda>con. ({((), UserContext (fpu_state con) ((user_regs con)(r := v)))}, False))" 312 by (simp add: setRegister_def simpler_modify_def) 313 314lemma zipWithM_setRegister_simple: 315 "zipWithM_x setRegister rs vs 316 = (\<lambda>con. ({((), foldl (\<lambda>con (r, v). UserContext (fpu_state con) ((user_regs con)(r := v))) con (zip rs vs))}, False))" 317 apply (simp add: zipWithM_x_mapM_x) 318 apply (induct ("zip rs vs")) 319 apply (simp add: mapM_x_Nil return_def) 320 apply (clarsimp simp add: mapM_x_Cons bind_def setRegister_def 321 simpler_modify_def fun_upd_def[symmetric]) 322 done 323 324lemma dom_partial_overwrite: 325 "\<forall>x. tcb_at' (idx x) s \<Longrightarrow> dom (partial_overwrite idx tsrs (ksPSpace s)) 326 = dom (ksPSpace s)" 327 apply (rule set_eqI) 328 apply (clarsimp simp: dom_def partial_overwrite_def put_tcb_state_regs_def 329 split: if_split) 330 apply (fastforce elim!: obj_atE') 331 done 332 333lemma map_to_ctes_partial_overwrite: 334 "\<forall>x. tcb_at' (idx x) s \<Longrightarrow> 335 map_to_ctes (partial_overwrite idx tsrs (ksPSpace s)) 336 = ctes_of s" 337 apply (rule ext) 338 apply (frule dom_partial_overwrite[where tsrs=tsrs]) 339 apply (simp add: map_to_ctes_def partial_overwrite_def 340 Let_def) 341 apply (case_tac "x \<in> range idx") 342 apply (clarsimp simp: put_tcb_state_regs_def) 343 apply (drule_tac x=xa in spec) 344 apply (clarsimp simp: obj_at'_def projectKOs objBits_simps' 345 cong: if_cong) 346 apply (simp add: put_tcb_state_regs_def put_tcb_state_regs_tcb_def 347 objBits_simps' 348 cong: if_cong option.case_cong) 349 apply (case_tac obj, simp split: tcb_state_regs.split if_split) 350 apply simp 351 apply (rule if_cong[OF refl]) 352 apply simp 353 apply (case_tac "x && ~~ mask (objBitsKO (KOTCB undefined)) \<in> range idx") 354 apply (clarsimp simp: put_tcb_state_regs_def) 355 apply (drule_tac x=xa in spec) 356 apply (clarsimp simp: obj_at'_def projectKOs objBits_simps' 357 cong: if_cong) 358 apply (simp add: put_tcb_state_regs_def put_tcb_state_regs_tcb_def 359 objBits_simps' 360 cong: if_cong option.case_cong) 361 apply (case_tac obj, simp split: tcb_state_regs.split if_split) 362 apply (intro impI allI) 363 apply (subgoal_tac "x - idx xa = x && mask tcbBlockSizeBits") 364 apply (clarsimp simp: tcb_cte_cases_def objBits_defs split: if_split) 365 apply (drule_tac t = "idx xa" in sym) 366 apply (simp add: objBits_defs) 367 apply (simp cong: if_cong) 368 done 369 370definition 371 "thread_actions_isolatable idx f = 372 (inj idx \<longrightarrow> monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) 373 f (isolate_thread_actions idx f id id))" 374 375lemma getCTE_assert_opt: 376 "getCTE p = gets (\<lambda>s. ctes_of s p) >>= assert_opt" 377 apply (intro ext) 378 apply (simp add: exec_gets assert_opt_def prod_eq_iff 379 fail_def return_def 380 split: option.split) 381 apply (rule conjI) 382 apply clarsimp 383 apply (rule context_conjI) 384 apply (rule ccontr, clarsimp elim!: nonemptyE) 385 apply (frule use_valid[OF _ getCTE_sp], rule TrueI) 386 apply (frule in_inv_by_hoareD[OF getCTE_inv]) 387 apply (clarsimp simp: cte_wp_at_ctes_of) 388 apply (simp add: empty_failD[OF empty_fail_getCTE]) 389 apply clarsimp 390 apply (simp add: no_failD[OF no_fail_getCTE, OF ctes_of_cte_at]) 391 apply (subgoal_tac "cte_wp_at' ((=) x2) p x") 392 apply (clarsimp simp: cte_wp_at'_def getCTE_def) 393 apply (simp add: cte_wp_at_ctes_of) 394 done 395 396lemma getCTE_isolatable: 397 "thread_actions_isolatable idx (getCTE p)" 398 apply (clarsimp simp: thread_actions_isolatable_def) 399 apply (simp add: isolate_thread_actions_def bind_assoc split_def) 400 apply (simp add: getCTE_assert_opt bind_select_f_bind[symmetric] 401 bind_assoc select_f_returns) 402 apply (clarsimp simp: monadic_rewrite_def exec_gets getSchedulerAction_def 403 map_to_ctes_partial_overwrite) 404 apply (simp add: assert_opt_def select_f_returns select_f_asserts 405 split: option.split) 406 apply (clarsimp simp: exec_modify o_def return_def) 407 apply (simp add: ksPSpace_update_partial_id) 408 done 409 410lemma obj_at_partial_overwrite_If: 411 "\<lbrakk> \<forall>x. tcb_at' (idx x) s \<rbrakk> 412 \<Longrightarrow> obj_at' P p (ksPSpace_update (partial_overwrite idx f) s) 413 = (if p \<in> range idx 414 then obj_at' (\<lambda>tcb. P (put_tcb_state_regs_tcb (f (inv idx p)) tcb)) p s 415 else obj_at' P p s)" 416 apply (frule dom_partial_overwrite[where tsrs=f]) 417 apply (simp add: obj_at'_def ps_clear_def partial_overwrite_def 418 projectKOs split: if_split) 419 apply clarsimp 420 apply (drule_tac x=x in spec) 421 apply (clarsimp simp: put_tcb_state_regs_def objBits_simps) 422 done 423 424lemma obj_at_partial_overwrite_id1: 425 "\<lbrakk> p \<notin> range idx; \<forall>x. tcb_at' (idx x) s \<rbrakk> 426 \<Longrightarrow> obj_at' P p (ksPSpace_update (partial_overwrite idx f) s) 427 = obj_at' P p s" 428 apply (drule dom_partial_overwrite[where tsrs=f]) 429 apply (simp add: obj_at'_def ps_clear_def partial_overwrite_def 430 projectKOs) 431 done 432 433lemma obj_at_partial_overwrite_id2: 434 "\<lbrakk> \<forall>x. tcb_at' (idx x) s; \<And>v tcb. P v \<or> True \<Longrightarrow> injectKO v \<noteq> KOTCB tcb \<rbrakk> 435 \<Longrightarrow> obj_at' P p (ksPSpace_update (partial_overwrite idx f) s) 436 = obj_at' P p s" 437 apply (frule dom_partial_overwrite[where tsrs=f]) 438 apply (simp add: obj_at'_def ps_clear_def partial_overwrite_def 439 projectKOs split: if_split) 440 apply clarsimp 441 apply (drule_tac x=x in spec) 442 apply (clarsimp simp: put_tcb_state_regs_def objBits_simps 443 project_inject) 444 done 445 446lemma objBits_2n: 447 "(1 :: machine_word) < 2 ^ objBits obj" 448 by (simp add: objBits_def objBitsKO_def archObjSize_def pageBits_def objBits_simps' 449 split: kernel_object.split arch_kernel_object.split) 450 451lemma magnitudeCheck_assert2: 452 "\<lbrakk> is_aligned x n; (1 :: machine_word) < 2 ^ n; ksPSpace s x = Some v \<rbrakk> \<Longrightarrow> 453 magnitudeCheck x (snd (lookupAround2 x (ksPSpace (s :: kernel_state)))) n 454 = assert (ps_clear x n s)" 455 using in_magnitude_check[where x=x and n=n and s=s and s'=s and v="()"] 456 by (simp add: magnitudeCheck_assert in_monad) 457 458 459lemma getObject_get_assert: 460 assumes deflt: "\<And>a b c d. (loadObject a b c d :: ('a :: pspace_storable) kernel) 461 = loadObject_default a b c d" 462 shows 463 "(getObject p :: ('a :: pspace_storable) kernel) 464 = do v \<leftarrow> gets (obj_at' (\<lambda>x :: 'a. True) p); 465 assert v; 466 gets (the o projectKO_opt o the o swp fun_app p o ksPSpace) 467 od" 468 apply (rule ext) 469 apply (simp add: exec_get getObject_def split_def exec_gets 470 deflt loadObject_default_def projectKO_def2 471 alignCheck_assert) 472 apply (case_tac "ksPSpace x p") 473 apply (simp add: obj_at'_def assert_opt_def assert_def 474 split: option.split if_split) 475 apply (simp add: lookupAround2_known1 assert_opt_def 476 obj_at'_def projectKO_def2 477 split: option.split) 478 apply (clarsimp simp: fail_def fst_return conj_comms project_inject 479 objBits_def) 480 apply (simp only: assert2[symmetric], 481 rule bind_apply_cong[OF refl]) 482 apply (clarsimp simp: in_monad) 483 apply (fold objBits_def) 484 apply (simp add: magnitudeCheck_assert2[OF _ objBits_2n]) 485 apply (rule bind_apply_cong[OF refl]) 486 apply (clarsimp simp: in_monad return_def simpler_gets_def) 487 apply (simp add: iffD2[OF project_inject refl]) 488 done 489 490 491lemma getObject_isolatable: 492 "\<lbrakk> \<And>a b c d. (loadObject a b c d :: 'a kernel) = loadObject_default a b c d; 493 \<And>tcb. projectKO_opt (KOTCB tcb) = (None :: 'a option) \<rbrakk> \<Longrightarrow> 494 thread_actions_isolatable idx (getObject p :: ('a :: pspace_storable) kernel)" 495 apply (clarsimp simp: thread_actions_isolatable_def) 496 apply (simp add: getObject_get_assert split_def 497 isolate_thread_actions_def bind_select_f_bind[symmetric] 498 bind_assoc select_f_asserts select_f_returns) 499 apply (clarsimp simp: monadic_rewrite_def exec_gets getSchedulerAction_def) 500 apply (case_tac "p \<in> range idx") 501 apply clarsimp 502 apply (drule_tac x=x in spec) 503 apply (clarsimp simp: obj_at'_def projectKOs partial_overwrite_def 504 put_tcb_state_regs_def) 505 apply (simp add: obj_at_partial_overwrite_id1) 506 apply (simp add: partial_overwrite_def) 507 apply (rule bind_apply_cong[OF refl]) 508 apply (simp add: exec_modify return_def o_def simpler_gets_def 509 ksPSpace_update_partial_id in_monad) 510 done 511 512lemma gets_isolatable: 513 "\<lbrakk>\<And>g s. \<forall>x. tcb_at' (idx x) s \<Longrightarrow> 514 f (ksSchedulerAction_update g 515 (ksPSpace_update (partial_overwrite idx (\<lambda>_. undefined)) s)) = f s \<rbrakk> \<Longrightarrow> 516 thread_actions_isolatable idx (gets f)" 517 apply (clarsimp simp: thread_actions_isolatable_def) 518 apply (simp add: isolate_thread_actions_def select_f_returns 519 liftM_def bind_assoc) 520 apply (clarsimp simp: monadic_rewrite_def exec_gets 521 getSchedulerAction_def exec_modify) 522 apply (simp add: simpler_gets_def return_def 523 ksPSpace_update_partial_id o_def) 524 done 525 526lemma modify_isolatable: 527 assumes swap:"\<And>tsrs act s. \<forall>x. tcb_at' (idx x) s \<Longrightarrow> 528 (ksPSpace_update (partial_overwrite idx tsrs) ((f s)\<lparr> ksSchedulerAction := act \<rparr>)) 529 = f (ksPSpace_update (partial_overwrite idx tsrs) 530 (s \<lparr> ksSchedulerAction := act\<rparr>))" 531 shows 532 "thread_actions_isolatable idx (modify f)" 533 apply (clarsimp simp: thread_actions_isolatable_def) 534 apply (simp add: isolate_thread_actions_def select_f_returns 535 liftM_def bind_assoc) 536 apply (clarsimp simp: monadic_rewrite_def exec_gets 537 getSchedulerAction_def) 538 apply (simp add: simpler_modify_def o_def) 539 apply (subst swap) 540 apply (simp add: obj_at_partial_overwrite_If) 541 apply (simp add: ksPSpace_update_partial_id o_def) 542 done 543 544lemma isolate_thread_actions_wrap_bind: 545 "inj idx \<Longrightarrow> 546 do x \<leftarrow> isolate_thread_actions idx a b c; 547 isolate_thread_actions idx (d x) e f 548 od = 549 isolate_thread_actions idx 550 (do x \<leftarrow> isolate_thread_actions idx a id id; 551 isolate_thread_actions idx (d x) id id 552 od) (e o b) (f o c) 553 " 554 apply (rule ext) 555 apply (clarsimp simp: isolate_thread_actions_def bind_assoc split_def 556 bind_select_f_bind[symmetric] liftM_def 557 select_f_returns select_f_selects 558 getSchedulerAction_def) 559 apply (clarsimp simp: exec_gets getSchedulerAction_def o_def) 560 apply (rule select_bind_eq) 561 apply (simp add: exec_gets exec_modify o_def) 562 apply (rule select_bind_eq) 563 apply (simp add: exec_modify) 564 done 565 566lemma monadic_rewrite_in_isolate_thread_actions: 567 "\<lbrakk> inj idx; monadic_rewrite F True P a d \<rbrakk> \<Longrightarrow> 568 monadic_rewrite F True (\<lambda>s. P (ksSchedulerAction_update (\<lambda>_. ResumeCurrentThread) 569 (ksPSpace_update (partial_overwrite idx (\<lambda>_. undefined)) s))) 570 (isolate_thread_actions idx a b c) (isolate_thread_actions idx d b c)" 571 apply (clarsimp simp: isolate_thread_actions_def split_def) 572 apply (rule monadic_rewrite_bind_tail)+ 573 apply (rule_tac P="\<lambda>_. P s" in monadic_rewrite_bind_head) 574 apply (simp add: monadic_rewrite_def select_f_def) 575 apply wp+ 576 apply simp 577 done 578 579lemma thread_actions_isolatable_bind: 580 "\<lbrakk> thread_actions_isolatable idx f; \<And>x. thread_actions_isolatable idx (g x); 581 \<And>t. \<lbrace>tcb_at' t\<rbrace> f \<lbrace>\<lambda>rv. tcb_at' t\<rbrace> \<rbrakk> 582 \<Longrightarrow> thread_actions_isolatable idx (f >>= g)" 583 apply (clarsimp simp: thread_actions_isolatable_def) 584 apply (rule monadic_rewrite_imp) 585 apply (rule monadic_rewrite_trans) 586 apply (erule monadic_rewrite_bind2, assumption) 587 apply (rule hoare_vcg_all_lift, assumption) 588 apply (subst isolate_thread_actions_wrap_bind, simp) 589 apply simp 590 apply (rule monadic_rewrite_in_isolate_thread_actions, assumption) 591 apply (rule monadic_rewrite_transverse) 592 apply (erule monadic_rewrite_bind2, assumption) 593 apply (rule hoare_vcg_all_lift, assumption) 594 apply (simp add: bind_assoc id_def) 595 apply (rule monadic_rewrite_refl) 596 apply (simp add: obj_at_partial_overwrite_If) 597 done 598 599lemma thread_actions_isolatable_return: 600 "thread_actions_isolatable idx (return v)" 601 apply (clarsimp simp: thread_actions_isolatable_def 602 monadic_rewrite_def liftM_def 603 isolate_thread_actions_def 604 split_def bind_assoc select_f_returns 605 exec_gets getSchedulerAction_def) 606 apply (simp add: exec_modify return_def o_def 607 ksPSpace_update_partial_id) 608 done 609 610lemma thread_actions_isolatable_fail: 611 "thread_actions_isolatable idx fail" 612 by (simp add: thread_actions_isolatable_def 613 isolate_thread_actions_def select_f_asserts 614 liftM_def bind_assoc getSchedulerAction_def 615 monadic_rewrite_def exec_gets) 616 617lemma thread_actions_isolatable_returns: 618 "thread_actions_isolatable idx (return v)" 619 "thread_actions_isolatable idx (returnOk v)" 620 "thread_actions_isolatable idx (throwError v)" 621 by (simp add: returnOk_def throwError_def 622 thread_actions_isolatable_return)+ 623 624lemma thread_actions_isolatable_bindE: 625 "\<lbrakk> thread_actions_isolatable idx f; \<And>x. thread_actions_isolatable idx (g x); 626 \<And>t. \<lbrace>tcb_at' t\<rbrace> f \<lbrace>\<lambda>rv. tcb_at' t\<rbrace> \<rbrakk> 627 \<Longrightarrow> thread_actions_isolatable idx (f >>=E g)" 628 apply (simp add: bindE_def) 629 apply (erule thread_actions_isolatable_bind) 630 apply (simp add: lift_def thread_actions_isolatable_returns 631 split: sum.split) 632 apply assumption 633 done 634 635lemma thread_actions_isolatable_catch: 636 "\<lbrakk> thread_actions_isolatable idx f; \<And>x. thread_actions_isolatable idx (g x); 637 \<And>t. \<lbrace>tcb_at' t\<rbrace> f \<lbrace>\<lambda>rv. tcb_at' t\<rbrace> \<rbrakk> 638 \<Longrightarrow> thread_actions_isolatable idx (f <catch> g)" 639 apply (simp add: catch_def) 640 apply (erule thread_actions_isolatable_bind) 641 apply (simp add: thread_actions_isolatable_returns 642 split: sum.split) 643 apply assumption 644 done 645 646lemma thread_actions_isolatable_if: 647 "\<lbrakk> P \<Longrightarrow> thread_actions_isolatable idx a; 648 \<not> P \<Longrightarrow> thread_actions_isolatable idx b \<rbrakk> 649 \<Longrightarrow> thread_actions_isolatable idx (if P then a else b)" 650 by (cases P, simp_all) 651 652lemma select_f_isolatable: 653 "thread_actions_isolatable idx (select_f v)" 654 apply (clarsimp simp: thread_actions_isolatable_def 655 isolate_thread_actions_def 656 split_def select_f_selects liftM_def bind_assoc) 657 apply (rule monadic_rewrite_imp, rule monadic_rewrite_transverse) 658 apply (rule monadic_rewrite_drop_modify monadic_rewrite_bind_tail)+ 659 apply wp+ 660 apply (simp add: gets_bind_ign getSchedulerAction_def) 661 apply (rule monadic_rewrite_refl) 662 apply (simp add: ksPSpace_update_partial_id o_def) 663 done 664 665lemma doMachineOp_isolatable: 666 "thread_actions_isolatable idx (doMachineOp m)" 667 apply (simp add: doMachineOp_def split_def) 668 apply (intro thread_actions_isolatable_bind[OF _ _ hoare_pre(1)] 669 gets_isolatable thread_actions_isolatable_returns 670 modify_isolatable select_f_isolatable) 671 apply (simp | wp)+ 672 done 673 674lemma page_map_l4_at_partial_overwrite: 675 "\<forall>x. tcb_at' (idx x) s \<Longrightarrow> 676 page_map_l4_at' p (ksPSpace_update (partial_overwrite idx f) s) 677 = page_map_l4_at' p s" 678 by (simp add: page_map_l4_at'_def typ_at_to_obj_at_arches 679 obj_at_partial_overwrite_id2) 680 681lemma findVSpaceForASID_isolatable: 682 "thread_actions_isolatable idx (findVSpaceForASID asid)" 683 apply (simp add: findVSpaceForASID_def liftE_bindE liftME_def bindE_assoc 684 case_option_If2 assertE_def liftE_def checkPML4At_def 685 stateAssert_def2 686 cong: if_cong) 687 apply (intro thread_actions_isolatable_bind[OF _ _ hoare_pre(1)] 688 thread_actions_isolatable_bindE[OF _ _ hoare_pre(1)] 689 thread_actions_isolatable_if thread_actions_isolatable_returns 690 thread_actions_isolatable_fail 691 gets_isolatable getObject_isolatable) 692 apply (simp add: projectKO_opt_asidpool page_map_l4_at_partial_overwrite 693 | wp getASID_wp)+ 694 done 695 696lemma modifyArchState_isolatable: 697 "thread_actions_isolatable idx (modifyArchState f)" 698 by (clarsimp simp: modifyArchState_def modify_isolatable) 699 700lemma modify_not_fail[simp]: 701 "modify f s \<noteq> fail s" 702 by (simp add: simpler_modify_def fail_def) 703 704lemma setObject_assert_modify: 705 "\<lbrakk> updateObject v = updateObject_default v; (1::machine_word) < 2 ^ objBits v; 706 \<And>ko v'. projectKO_opt ko = Some (v'::'a) \<Longrightarrow> objBitsKO ko = objBits v \<rbrakk> \<Longrightarrow> 707 setObject p (v::'a::pspace_storable) s = (do 708 assert (obj_at' (\<lambda>_::'a. True) p s); 709 modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> injectKOS v))) 710 od) s" 711 apply (clarsimp simp: assert_def setObject_modify split: if_split) 712 apply (clarsimp simp: setObject_def updateObject_default_def exec_gets split_def bind_assoc) 713 apply (clarsimp simp: assert_opt_def assert_def alignCheck_assert projectKO_def 714 split: option.splits if_splits) 715 apply (clarsimp simp: magnitudeCheck_assert2 assert_def split: if_splits) 716 apply (clarsimp simp: obj_at'_def projectKOs) 717 done 718 719lemma thread_actions_isolatable_mapM_x: 720 "\<lbrakk> \<And>x. thread_actions_isolatable idx (f x); 721 \<And>x t. f x \<lbrace>tcb_at' t\<rbrace> \<rbrakk> \<Longrightarrow> thread_actions_isolatable idx (mapM_x f xs)" 722 apply (induct xs; clarsimp simp: mapM_x_Nil mapM_x_Cons thread_actions_isolatable_returns) 723 apply (rule thread_actions_isolatable_bind[OF _ _ hoare_pre(1)]; clarsimp?) 724 apply assumption+ 725 done 726 727lemma liftM_getObject_return_tcb: 728 "ko_at' v p s \<Longrightarrow> liftM f (getObject p) s = return (f (v::tcb)) s" 729 by (simp add: liftM_def bind_def getObject_return_tcb return_def objBits_defs) 730 731lemma getCurrentUserCR3_isolatable: 732 "thread_actions_isolatable idx (getCurrentUserCR3)" 733 by (clarsimp simp: getCurrentUserCR3_def gets_isolatable) 734 735lemma setCurrentUserCR3_isolatable: 736 "thread_actions_isolatable idx (setCurrentUserCR3 f)" 737 apply (clarsimp simp: setCurrentUserCR3_def) 738 apply (intro modify_isolatable doMachineOp_isolatable 739 thread_actions_isolatable_bind[OF _ _ hoare_pre(1)]) 740 apply wpsimp+ 741 done 742 743lemma setCurrentUserVSpaceRoot_isolatable: 744 "thread_actions_isolatable idx (setCurrentUserVSpaceRoot a f)" 745 by (clarsimp simp: setCurrentUserVSpaceRoot_def setCurrentUserCR3_isolatable) 746 747lemma setVMRoot_isolatable: 748 "thread_actions_isolatable idx (setVMRoot t)" 749 apply (simp add: setVMRoot_def getThreadVSpaceRoot_def 750 locateSlot_conv getSlotCap_def 751 cap_case_isPML4Cap if_bool_simps 752 whenE_def liftE_def 753 stateAssert_def2 754 cong: if_cong) 755 apply (intro thread_actions_isolatable_bind[OF _ _ hoare_pre(1)] 756 thread_actions_isolatable_bindE[OF _ _ hoare_pre(1)] 757 thread_actions_isolatable_catch[OF _ _ hoare_pre(1)] 758 thread_actions_isolatable_if thread_actions_isolatable_returns 759 thread_actions_isolatable_fail 760 getCurrentUserCR3_isolatable setCurrentUserCR3_isolatable 761 gets_isolatable getCTE_isolatable 762 setCurrentUserVSpaceRoot_isolatable 763 findVSpaceForASID_isolatable doMachineOp_isolatable 764 | simp add: projectKO_opt_asidpool 765 | wp getASID_wp typ_at_lifts)+ 766 done 767 768lemma transferCaps_simple: 769 "transferCaps mi [] ep receiver rcvrBuf = 770 do 771 getReceiveSlots receiver rcvrBuf; 772 return (mi\<lparr>msgExtraCaps := 0, msgCapsUnwrapped := 0\<rparr>) 773 od" 774 apply (cases mi) 775 apply (clarsimp simp: transferCaps_def getThreadCSpaceRoot_def locateSlot_conv) 776 done 777 778lemma transferCaps_simple_rewrite: 779 "monadic_rewrite True True ((\<lambda>_. caps = []) and \<top>) 780 (transferCaps mi caps ep r rBuf) 781 (return (mi \<lparr> msgExtraCaps := 0, msgCapsUnwrapped := 0 \<rparr>))" 782 including no_pre 783 apply (rule monadic_rewrite_gen_asm) 784 apply (rule monadic_rewrite_imp) 785 apply (rule monadic_rewrite_trans) 786 apply (simp add: transferCaps_simple, rule monadic_rewrite_refl) 787 apply (rule monadic_rewrite_symb_exec2, (wp empty_fail_getReceiveSlots)+) 788 apply (rule monadic_rewrite_refl) 789 apply simp 790 done 791 792lemma lookupExtraCaps_simple_rewrite: 793 "msgExtraCaps mi = 0 \<Longrightarrow> 794 (lookupExtraCaps thread rcvBuf mi = returnOk [])" 795 by (cases mi, simp add: lookupExtraCaps_def getExtraCPtrs_def 796 liftE_bindE upto_enum_step_def mapM_Nil 797 split: option.split) 798 799lemma lookupIPC_inv: "\<lbrace>P\<rbrace> lookupIPCBuffer f t \<lbrace>\<lambda>rv. P\<rbrace>" 800 by wp 801 802lemmas empty_fail_user_getreg = empty_fail_asUser[OF empty_fail_getRegister] 803 804lemma user_getreg_rv: 805 "\<lbrace>obj_at' (\<lambda>tcb. P ((user_regs o atcbContextGet o tcbArch) tcb r)) t\<rbrace> asUser t (getRegister r) \<lbrace>\<lambda>rv s. P rv\<rbrace>" 806 apply (simp add: asUser_def split_def) 807 apply (wp threadGet_wp) 808 apply (clarsimp simp: obj_at'_def projectKOs getRegister_def in_monad atcbContextGet_def) 809 done 810 811lemma copyMRs_simple: 812 "msglen \<le> of_nat (length X64_H.msgRegisters) \<longrightarrow> 813 copyMRs sender sbuf receiver rbuf msglen 814 = forM_x (take (unat msglen) X64_H.msgRegisters) 815 (\<lambda>r. do v \<leftarrow> asUser sender (getRegister r); 816 asUser receiver (setRegister r v) od) 817 >>= (\<lambda>rv. return msglen)" 818 apply (clarsimp simp: copyMRs_def mapM_discarded) 819 apply (rule bind_cong[OF refl]) 820 apply (simp add: length_msgRegisters n_msgRegisters_def min_def 821 word_le_nat_alt 822 split: option.split) 823 apply (simp add: upto_enum_def mapM_Nil) 824 done 825 826lemma doIPCTransfer_simple_rewrite: 827 "monadic_rewrite True True 828 ((\<lambda>_. msgExtraCaps (messageInfoFromWord msgInfo) = 0 829 \<and> msgLength (messageInfoFromWord msgInfo) 830 \<le> of_nat (length X64_H.msgRegisters)) 831 and obj_at' (\<lambda>tcb. tcbFault tcb = None 832 \<and> (user_regs o atcbContextGet o tcbArch) tcb msgInfoRegister = msgInfo) sender) 833 (doIPCTransfer sender ep badge True rcvr) 834 (do rv \<leftarrow> mapM_x (\<lambda>r. do v \<leftarrow> asUser sender (getRegister r); 835 asUser rcvr (setRegister r v) 836 od) 837 (take (unat (msgLength (messageInfoFromWord msgInfo))) X64_H.msgRegisters); 838 y \<leftarrow> setMessageInfo rcvr ((messageInfoFromWord msgInfo) \<lparr>msgCapsUnwrapped := 0\<rparr>); 839 asUser rcvr (setRegister X64_H.badgeRegister badge) 840 od)" 841 apply (rule monadic_rewrite_gen_asm) 842 apply (simp add: doIPCTransfer_def bind_assoc doNormalTransfer_def 843 getMessageInfo_def 844 cong: option.case_cong) 845 apply (rule monadic_rewrite_imp) 846 apply (rule monadic_rewrite_trans) 847 apply (rule monadic_rewrite_bind_tail)+ 848 apply (rule_tac P="fault = None" in monadic_rewrite_gen_asm, simp) 849 apply (rule monadic_rewrite_bind_tail) 850 apply (rule_tac x=msgInfo in monadic_rewrite_symb_exec, 851 (wp empty_fail_user_getreg user_getreg_rv)+) 852 apply (simp add: lookupExtraCaps_simple_rewrite returnOk_catch_bind) 853 apply (rule monadic_rewrite_bind) 854 apply (rule monadic_rewrite_from_simple, rule copyMRs_simple) 855 apply (rule monadic_rewrite_bind_head) 856 apply (rule transferCaps_simple_rewrite) 857 apply (wp threadGet_const)+ 858 apply (simp add: bind_assoc) 859 apply (rule monadic_rewrite_symb_exec2[OF lookupIPC_inv empty_fail_lookupIPCBuffer] 860 monadic_rewrite_symb_exec2[OF threadGet_inv empty_fail_threadGet] 861 monadic_rewrite_symb_exec2[OF user_getreg_inv' empty_fail_user_getreg] 862 monadic_rewrite_bind_head monadic_rewrite_bind_tail 863 | wp)+ 864 apply (case_tac "messageInfoFromWord msgInfo") 865 apply simp 866 apply (rule monadic_rewrite_refl) 867 apply wp 868 apply clarsimp 869 apply (auto elim!: obj_at'_weakenE) 870 done 871 872lemma monadic_rewrite_setSchedulerAction_noop: 873 "monadic_rewrite F E (\<lambda>s. ksSchedulerAction s = act) (setSchedulerAction act) (return ())" 874 unfolding setSchedulerAction_def 875 apply (rule monadic_rewrite_imp, rule monadic_rewrite_modify_noop) 876 apply simp 877 done 878 879lemma rescheduleRequired_simple_rewrite: 880 "monadic_rewrite F E 881 (sch_act_simple) 882 rescheduleRequired 883 (setSchedulerAction ChooseNewThread)" 884 apply (simp add: rescheduleRequired_def getSchedulerAction_def) 885 apply (simp add: monadic_rewrite_def exec_gets sch_act_simple_def) 886 apply auto 887 done 888 889lemma empty_fail_isRunnable: 890 "empty_fail (isRunnable t)" 891 by (simp add: isRunnable_def isBlocked_def) 892 893lemma setupCallerCap_rewrite: 894 "monadic_rewrite True True (\<lambda>s. reply_masters_rvk_fb (ctes_of s)) 895 (setupCallerCap send rcv) 896 (do setThreadState BlockedOnReply send; 897 replySlot \<leftarrow> getThreadReplySlot send; 898 callerSlot \<leftarrow> getThreadCallerSlot rcv; 899 replySlotCTE \<leftarrow> getCTE replySlot; 900 assert (mdbNext (cteMDBNode replySlotCTE) = 0 901 \<and> isReplyCap (cteCap replySlotCTE) 902 \<and> capReplyMaster (cteCap replySlotCTE) 903 \<and> mdbFirstBadged (cteMDBNode replySlotCTE) 904 \<and> mdbRevocable (cteMDBNode replySlotCTE)); 905 cteInsert (ReplyCap send False) replySlot callerSlot 906 od)" 907 apply (simp add: setupCallerCap_def getThreadCallerSlot_def 908 getThreadReplySlot_def locateSlot_conv 909 getSlotCap_def) 910 apply (rule monadic_rewrite_imp) 911 apply (rule monadic_rewrite_bind_tail)+ 912 apply (rule monadic_rewrite_assert)+ 913 apply (rule_tac P="mdbFirstBadged (cteMDBNode masterCTE) 914 \<and> mdbRevocable (cteMDBNode masterCTE)" 915 in monadic_rewrite_gen_asm) 916 apply simp 917 apply (rule monadic_rewrite_trans) 918 apply (rule monadic_rewrite_bind_tail) 919 apply (rule monadic_rewrite_symb_exec2, (wp | simp)+)+ 920 apply (rule monadic_rewrite_refl) 921 apply wp+ 922 apply (rule monadic_rewrite_symb_exec2, (wp empty_fail_getCTE)+)+ 923 apply (rule monadic_rewrite_refl) 924 apply (wp getCTE_wp' | simp add: cte_wp_at_ctes_of)+ 925 apply (clarsimp simp: reply_masters_rvk_fb_def) 926 apply fastforce 927 done 928 929lemma oblivious_getObject_ksPSpace_default: 930 "\<lbrakk> \<forall>s. ksPSpace (f s) = ksPSpace s; 931 \<And>a b c ko. (loadObject a b c ko :: 'a kernel) \<equiv> loadObject_default a b c ko \<rbrakk> \<Longrightarrow> 932 oblivious f (getObject p :: ('a :: pspace_storable) kernel)" 933 apply (simp add: getObject_def split_def loadObject_default_def 934 projectKO_def2 alignCheck_assert magnitudeCheck_assert) 935 apply (intro oblivious_bind, simp_all) 936 done 937 938lemmas oblivious_getObject_ksPSpace_tcb[simp] 939 = oblivious_getObject_ksPSpace_default[OF _ loadObject_tcb] 940 941lemma oblivious_setObject_ksPSpace_tcb[simp]: 942 "\<lbrakk> \<forall>s. ksPSpace (f s) = ksPSpace s; 943 \<forall>s g. ksPSpace_update g (f s) = f (ksPSpace_update g s) \<rbrakk> \<Longrightarrow> 944 oblivious f (setObject p (v :: tcb))" 945 apply (simp add: setObject_def split_def updateObject_default_def 946 projectKO_def2 alignCheck_assert magnitudeCheck_assert) 947 apply (intro oblivious_bind, simp_all) 948 done 949 950lemma oblivious_getObject_ksPSpace_cte[simp]: 951 "\<lbrakk> \<forall>s. ksPSpace (f s) = ksPSpace s \<rbrakk> \<Longrightarrow> 952 oblivious f (getObject p :: cte kernel)" 953 apply (simp add: getObject_def split_def loadObject_cte 954 projectKO_def2 alignCheck_assert magnitudeCheck_assert 955 typeError_def unless_when 956 cong: Structures_H.kernel_object.case_cong) 957 apply (intro oblivious_bind, 958 simp_all split: Structures_H.kernel_object.split if_split) 959 by (safe intro!: oblivious_bind, simp_all) 960 961lemma oblivious_doMachineOp[simp]: 962 "\<lbrakk> \<forall>s. ksMachineState (f s) = ksMachineState s; 963 \<forall>g s. ksMachineState_update g (f s) = f (ksMachineState_update g s) \<rbrakk> 964 \<Longrightarrow> oblivious f (doMachineOp oper)" 965 apply (simp add: doMachineOp_def split_def) 966 apply (intro oblivious_bind, simp_all) 967 done 968 969lemmas oblivious_getObject_ksPSpace_asidpool[simp] 970 = oblivious_getObject_ksPSpace_default[OF _ loadObject_asidpool] 971 972lemma oblivious_modifyArchState_schact[simp]: 973 "oblivious (ksSchedulerAction_update f) (modifyArchState f')" 974 by (simp add: oblivious_def modifyArchState_def simpler_modify_def) 975 976lemma oblivious_setVMRoot_schact: 977 "oblivious (ksSchedulerAction_update f) (setVMRoot t)" 978 apply (simp add: setVMRoot_def getThreadVSpaceRoot_def locateSlot_conv 979 getSlotCap_def getCTE_def) 980 by (safe intro!: oblivious_bind oblivious_bindE oblivious_catch oblivious_mapM_x 981 | simp_all add: liftE_def 982 findVSpaceForASID_def liftME_def 983 findVSpaceForASIDAssert_def checkPML4At_def 984 getCurrentUserCR3_def setCurrentUserCR3_def 985 invalidateASID_def setCurrentUserVSpaceRoot_def 986 split: if_split capability.split arch_capability.split option.split)+ 987 988 989lemma oblivious_switchToThread_schact: 990 "oblivious (ksSchedulerAction_update f) (ThreadDecls_H.switchToThread t)" 991 apply (simp add: Thread_H.switchToThread_def X64_H.switchToThread_def bind_assoc 992 getCurThread_def setCurThread_def threadGet_def liftM_def 993 threadSet_def tcbSchedEnqueue_def unless_when asUser_def 994 getQueue_def setQueue_def storeWordUser_def setRegister_def 995 pointerInUserData_def isRunnable_def isBlocked_def 996 getThreadState_def tcbSchedDequeue_def bitmap_fun_defs) 997 by (safe intro!: oblivious_bind 998 | simp_all add: oblivious_setVMRoot_schact)+ 999 1000lemma empty_fail_getCurThread[iff]: 1001 "empty_fail getCurThread" by (simp add: getCurThread_def) 1002lemma activateThread_simple_rewrite: 1003 "monadic_rewrite True True (ct_in_state' ((=) Running)) 1004 (activateThread) (return ())" 1005 apply (simp add: activateThread_def) 1006 apply (rule monadic_rewrite_imp) 1007 apply (rule monadic_rewrite_trans, rule monadic_rewrite_bind_tail)+ 1008 apply (rule_tac P="state = Running" in monadic_rewrite_gen_asm) 1009 apply simp 1010 apply (rule monadic_rewrite_refl) 1011 apply wp 1012 apply (rule monadic_rewrite_symb_exec2, (wp empty_fail_getThreadState)+) 1013 apply (rule monadic_rewrite_refl) 1014 apply wp 1015 apply (rule monadic_rewrite_symb_exec2, 1016 simp_all add: getCurThread_def) 1017 apply (rule monadic_rewrite_refl) 1018 apply (clarsimp simp: ct_in_state'_def elim!: pred_tcb'_weakenE) 1019 done 1020 1021end 1022 1023lemma setCTE_obj_at_prio[wp]: 1024 "\<lbrace>obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t\<rbrace> setCTE p v \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t\<rbrace>" 1025 unfolding setCTE_def 1026 by (rule setObject_cte_obj_at_tcb', simp+) 1027 1028crunch obj_at_prio[wp]: cteInsert "obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t" 1029 (wp: crunch_wps) 1030 1031crunch ctes_of[wp]: asUser "\<lambda>s. P (ctes_of s)" 1032 (wp: crunch_wps) 1033 1034lemma tcbSchedEnqueue_tcbPriority[wp]: 1035 "\<lbrace>obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t\<rbrace> 1036 tcbSchedEnqueue t' 1037 \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t\<rbrace>" 1038 apply (simp add: tcbSchedEnqueue_def unless_def) 1039 apply (wp | simp cong: if_cong)+ 1040 done 1041 1042crunch obj_at_prio[wp]: cteDeleteOne "obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t" 1043 (wp: crunch_wps setEndpoint_obj_at_tcb' 1044 setThreadState_obj_at_unchanged setNotification_tcb setBoundNotification_obj_at_unchanged 1045 simp: crunch_simps unless_def) 1046 1047context kernel_m begin 1048 1049lemma setThreadState_no_sch_change: 1050 "\<lbrace>\<lambda>s. P (ksSchedulerAction s) \<and> (runnable' st \<or> t \<noteq> ksCurThread s)\<rbrace> 1051 setThreadState st t 1052 \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>" 1053 (is "NonDetMonad.valid ?P ?f ?Q") 1054 apply (simp add: setThreadState_def setSchedulerAction_def) 1055 apply (wp hoare_pre_cont[where a=rescheduleRequired]) 1056 apply (rule_tac Q="\<lambda>_. ?P and st_tcb_at' ((=) st) t" in hoare_post_imp) 1057 apply (clarsimp split: if_split) 1058 apply (clarsimp simp: obj_at'_def st_tcb_at'_def projectKOs) 1059 apply (wp threadSet_pred_tcb_at_state) 1060 apply simp 1061 done 1062 1063lemma asUser_obj_at_unchangedT: 1064 assumes x: "\<forall>tcb con con'. con' \<in> fst (m con) 1065 \<longrightarrow> P (tcbArch_update (\<lambda>_. atcbContextSet (snd con') (tcbArch tcb)) tcb) = P tcb" shows 1066 "\<lbrace>obj_at' P t\<rbrace> asUser t' m \<lbrace>\<lambda>rv. obj_at' P t\<rbrace>" 1067 apply (simp add: asUser_def split_def) 1068 apply (wp threadSet_obj_at' threadGet_wp) 1069 apply (clarsimp simp: obj_at'_def projectKOs x cong: if_cong) 1070 done 1071 1072lemmas asUser_obj_at_unchanged 1073 = asUser_obj_at_unchangedT[OF all_tcbI, rule_format] 1074 1075lemma bind_assoc: 1076 "do y \<leftarrow> do x \<leftarrow> m; f x od; g y od 1077 = do x \<leftarrow> m; y \<leftarrow> f x; g y od" 1078 by (rule bind_assoc) 1079 1080lemma setObject_modify_assert: 1081 "\<lbrakk> updateObject v = updateObject_default v \<rbrakk> 1082 \<Longrightarrow> setObject p v = do f \<leftarrow> gets (obj_at' (\<lambda>v'. v = v' \<or> True) p); 1083 assert f; modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> injectKO v))) od" 1084 using objBits_2n[where obj=v] 1085 apply (simp add: setObject_def split_def updateObject_default_def 1086 bind_assoc projectKO_def2 alignCheck_assert) 1087 apply (rule ext, simp add: exec_gets) 1088 apply (case_tac "obj_at' (\<lambda>v'. v = v' \<or> True) p x") 1089 apply (clarsimp simp: obj_at'_def projectKOs lookupAround2_known1 1090 assert_opt_def) 1091 apply (clarsimp simp: project_inject) 1092 apply (simp only: objBits_def objBitsT_koTypeOf[symmetric] koTypeOf_injectKO) 1093 apply (simp add: magnitudeCheck_assert2 simpler_modify_def) 1094 apply (clarsimp simp: assert_opt_def assert_def magnitudeCheck_assert2 1095 split: option.split if_split) 1096 apply (clarsimp simp: obj_at'_def projectKOs) 1097 apply (clarsimp simp: project_inject) 1098 apply (simp only: objBits_def objBitsT_koTypeOf[symmetric] 1099 koTypeOf_injectKO simp_thms) 1100 done 1101 1102lemma setEndpoint_isolatable: 1103 "thread_actions_isolatable idx (setEndpoint p e)" 1104 apply (simp add: setEndpoint_def setObject_modify_assert 1105 assert_def) 1106 apply (case_tac "p \<in> range idx") 1107 apply (clarsimp simp: thread_actions_isolatable_def 1108 monadic_rewrite_def fun_eq_iff 1109 liftM_def isolate_thread_actions_def 1110 bind_assoc exec_gets getSchedulerAction_def 1111 bind_select_f_bind[symmetric]) 1112 apply (simp add: obj_at_partial_overwrite_id2) 1113 apply (drule_tac x=x in spec) 1114 apply (clarsimp simp: obj_at'_def projectKOs select_f_asserts) 1115 apply (intro thread_actions_isolatable_bind[OF _ _ hoare_pre(1)] 1116 thread_actions_isolatable_if 1117 thread_actions_isolatable_return 1118 thread_actions_isolatable_fail) 1119 apply (rule gets_isolatable) 1120 apply (simp add: obj_at_partial_overwrite_id2) 1121 apply (rule modify_isolatable) 1122 apply (clarsimp simp: o_def partial_overwrite_def) 1123 apply (rule kernel_state.fold_congs[OF refl refl]) 1124 apply (clarsimp simp: fun_eq_iff 1125 split: if_split) 1126 apply (wp | simp)+ 1127 done 1128 1129(* FIXME x64: tcb bits *) 1130lemma setCTE_assert_modify: 1131 "setCTE p v = do c \<leftarrow> gets (real_cte_at' p); 1132 t \<leftarrow> gets (tcb_at' (p && ~~ mask tcbBlockSizeBits) 1133 and K ((p && mask tcbBlockSizeBits) \<in> dom tcb_cte_cases)); 1134 if c then modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOCTE v))) 1135 else if t then 1136 modify (ksPSpace_update 1137 (\<lambda>ps. ps (p && ~~ mask tcbBlockSizeBits \<mapsto> 1138 KOTCB (snd (the (tcb_cte_cases (p && mask tcbBlockSizeBits))) (K v) 1139 (the (projectKO_opt (the (ps (p && ~~ mask tcbBlockSizeBits))))))))) 1140 else fail od" 1141 apply (clarsimp simp: setCTE_def setObject_def split_def 1142 fun_eq_iff exec_gets) 1143 apply (case_tac "real_cte_at' p x") 1144 apply (clarsimp simp: obj_at'_def projectKOs lookupAround2_known1 1145 assert_opt_def alignCheck_assert objBits_simps' 1146 magnitudeCheck_assert2 updateObject_cte) 1147 apply (simp add: simpler_modify_def) 1148 apply (simp split: if_split, intro conjI impI) 1149 apply (clarsimp simp: obj_at'_def projectKOs) 1150 apply (subgoal_tac "p \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1") 1151 apply (subgoal_tac "fst (lookupAround2 p (ksPSpace x)) 1152 = Some (p && ~~ mask tcbBlockSizeBits, KOTCB obj)") 1153 apply (simp add: assert_opt_def) 1154 apply (subst updateObject_cte_tcb) 1155 apply (fastforce simp add: subtract_mask) 1156 apply (simp add: assert_opt_def alignCheck_assert bind_assoc 1157 magnitudeCheck_assert 1158 is_aligned_neg_mask2 objBits_def) 1159 apply (rule ps_clear_lookupAround2, assumption+) 1160 apply (rule word_and_le2) 1161 apply (simp add: objBits_simps mask_def field_simps) 1162 apply (simp add: simpler_modify_def cong: option.case_cong if_cong) 1163 apply (rule kernel_state.fold_congs[OF refl refl]) 1164 apply (clarsimp simp: projectKO_opt_tcb cong: if_cong) 1165 apply (clarsimp simp: lookupAround2_char1 word_and_le2) 1166 apply (rule ccontr, clarsimp) 1167 apply (erule(2) ps_clearD) 1168 apply (simp add: objBits_simps mask_def field_simps) 1169 apply (rule tcb_cte_cases_in_range2) 1170 apply (simp add: subtract_mask) 1171 apply simp 1172 apply (clarsimp simp: assert_opt_def split: option.split) 1173 apply (rule trans [OF bind_apply_cong[OF _ refl] fun_cong[OF fail_bind]]) 1174 apply (simp add: fail_def prod_eq_iff) 1175 apply (rule context_conjI) 1176 apply (rule ccontr, clarsimp elim!: nonemptyE) 1177 apply (frule(1) updateObject_cte_is_tcb_or_cte[OF _ refl]) 1178 apply (erule disjE) 1179 apply clarsimp 1180 apply (frule(1) tcb_cte_cases_aligned_helpers) 1181 apply (clarsimp simp: domI[where m = cte_cte_cases] field_simps) 1182 apply (clarsimp simp: lookupAround2_char1 obj_at'_def projectKOs 1183 objBits_simps) 1184 apply (clarsimp simp: obj_at'_def lookupAround2_char1 1185 objBits_simps' projectKOs cte_level_bits_def) 1186 apply (erule empty_failD[OF empty_fail_updateObject_cte]) 1187 done 1188 1189lemma partial_overwrite_fun_upd2: 1190 "partial_overwrite idx tsrs (f (x := y)) 1191 = (partial_overwrite idx tsrs f) 1192 (x := if x \<in> range idx then put_tcb_state_regs (tsrs (inv idx x)) y 1193 else y)" 1194 by (simp add: fun_eq_iff partial_overwrite_def split: if_split) 1195 1196lemma atcbContextSetSetGet_eq[simp]: 1197 "atcbContextSet (UserContext (fpu_state (atcbContext 1198 (atcbContextSet (UserContext (fpu_state (atcbContext t)) r) t))) 1199 (user_regs (atcbContextGet t))) t = t" 1200 by (cases t, simp add: atcbContextSet_def atcbContextGet_def) 1201 1202lemma setCTE_isolatable: 1203 "thread_actions_isolatable idx (setCTE p v)" 1204 apply (simp add: setCTE_assert_modify) 1205 apply (clarsimp simp: thread_actions_isolatable_def 1206 monadic_rewrite_def fun_eq_iff 1207 liftM_def exec_gets 1208 isolate_thread_actions_def 1209 bind_assoc exec_gets getSchedulerAction_def 1210 bind_select_f_bind[symmetric] 1211 obj_at_partial_overwrite_If 1212 obj_at_partial_overwrite_id2 1213 cong: if_cong) 1214 apply (case_tac "p && ~~ mask tcbBlockSizeBits \<in> range idx \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases") 1215 apply clarsimp 1216 apply (frule_tac x=x in spec, erule obj_atE') 1217 apply (subgoal_tac "\<not> real_cte_at' p s") 1218 apply (clarsimp simp: select_f_returns select_f_asserts split: if_split) 1219 apply (clarsimp simp: o_def simpler_modify_def partial_overwrite_fun_upd2) 1220 apply (rule kernel_state.fold_congs[OF refl refl]) 1221 apply (rule ext) 1222 apply (clarsimp simp: partial_overwrite_get_tcb_state_regs 1223 split: if_split) 1224 apply (clarsimp simp: projectKOs get_tcb_state_regs_def 1225 put_tcb_state_regs_def put_tcb_state_regs_tcb_def 1226 partial_overwrite_def 1227 split: tcb_state_regs.split) 1228 apply (case_tac obj, simp add: projectKO_opt_tcb) 1229 apply (simp add: tcb_cte_cases_def split: if_split_asm) 1230 apply (drule_tac x=x in spec) 1231 apply (clarsimp simp: obj_at'_def projectKOs objBits_simps subtract_mask(2) [symmetric]) 1232 apply (erule notE[rotated], erule (3) tcb_ctes_clear[rotated]) 1233 apply (simp add: select_f_returns select_f_asserts split: if_split) 1234 apply (intro conjI impI) 1235 apply (clarsimp simp: simpler_modify_def fun_eq_iff 1236 partial_overwrite_fun_upd2 o_def 1237 intro!: kernel_state.fold_congs[OF refl refl]) 1238 apply (clarsimp simp: obj_at'_def projectKOs objBits_simps) 1239 apply (erule notE[rotated], rule tcb_ctes_clear[rotated 2], assumption+) 1240 apply (fastforce simp add: subtract_mask) 1241 apply simp 1242 apply (clarsimp simp: simpler_modify_def 1243 partial_overwrite_fun_upd2 o_def 1244 partial_overwrite_get_tcb_state_regs 1245 intro!: kernel_state.fold_congs[OF refl refl] 1246 split: if_split) 1247 apply (simp add: partial_overwrite_def) 1248 apply (subgoal_tac "p \<notin> range idx") 1249 apply (clarsimp simp: simpler_modify_def 1250 partial_overwrite_fun_upd2 o_def 1251 partial_overwrite_get_tcb_state_regs 1252 intro!: kernel_state.fold_congs[OF refl refl]) 1253 apply clarsimp 1254 apply (drule_tac x=x in spec) 1255 apply (clarsimp simp: obj_at'_def projectKOs) 1256 done 1257 1258lemma assert_isolatable: 1259 "thread_actions_isolatable idx (assert P)" 1260 by (simp add: assert_def thread_actions_isolatable_if 1261 thread_actions_isolatable_returns 1262 thread_actions_isolatable_fail) 1263 1264lemma cteInsert_isolatable: 1265 "thread_actions_isolatable idx (cteInsert cap src dest)" 1266 apply (simp add: cteInsert_def updateCap_def updateMDB_def 1267 Let_def setUntypedCapAsFull_def) 1268 apply (intro thread_actions_isolatable_bind[OF _ _ hoare_pre(1)] 1269 thread_actions_isolatable_if 1270 thread_actions_isolatable_returns assert_isolatable 1271 getCTE_isolatable setCTE_isolatable) 1272 apply (wp | simp)+ 1273 done 1274 1275lemma isolate_thread_actions_threadSet_tcbState: 1276 "\<lbrakk> inj idx; idx t' = t \<rbrakk> \<Longrightarrow> 1277 monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) 1278 (threadSet (tcbState_update (\<lambda>_. st)) t) 1279 (isolate_thread_actions idx (return ()) 1280 (\<lambda>tsrs. (tsrs (t' := TCBStateRegs st (tsrContext (tsrs t'))))) 1281 id)" 1282 apply (simp add: isolate_thread_actions_def bind_assoc split_def 1283 select_f_returns getSchedulerAction_def) 1284 apply (clarsimp simp: monadic_rewrite_def exec_gets threadSet_def 1285 getObject_get_assert bind_assoc liftM_def 1286 setObject_modify_assert) 1287 apply (frule_tac x=t' in spec, drule obj_at_ko_at') 1288 apply (clarsimp simp: exec_gets simpler_modify_def o_def 1289 intro!: kernel_state.fold_congs[OF refl refl]) 1290 apply (simp add: partial_overwrite_fun_upd 1291 partial_overwrite_get_tcb_state_regs) 1292 apply (clarsimp simp: put_tcb_state_regs_def put_tcb_state_regs_tcb_def 1293 projectKOs get_tcb_state_regs_def 1294 elim!: obj_atE') 1295 apply (case_tac ko) 1296 apply (simp add: projectKO_opt_tcb) 1297 done 1298 1299lemma thread_actions_isolatableD: 1300 "\<lbrakk> thread_actions_isolatable idx f; inj idx \<rbrakk> 1301 \<Longrightarrow> monadic_rewrite False True (\<lambda>s. (\<forall>x. tcb_at' (idx x) s)) 1302 f (isolate_thread_actions idx f id id)" 1303 by (clarsimp simp: thread_actions_isolatable_def) 1304 1305lemma tcbSchedDequeue_rewrite: 1306 "monadic_rewrite True True (obj_at' (Not \<circ> tcbQueued) t) (tcbSchedDequeue t) (return ())" 1307 apply (simp add: tcbSchedDequeue_def) 1308 apply (rule monadic_rewrite_imp) 1309 apply (rule monadic_rewrite_trans) 1310 apply (rule monadic_rewrite_bind_tail) 1311 apply (rule_tac P="\<not> queued" in monadic_rewrite_gen_asm) 1312 apply (simp add: when_def) 1313 apply (rule monadic_rewrite_refl) 1314 apply (wp threadGet_const) 1315 apply (rule monadic_rewrite_symb_exec2) 1316 apply wp+ 1317 apply (rule monadic_rewrite_refl) 1318 apply (clarsimp) 1319 done 1320 1321lemma switchToThread_rewrite: 1322 "monadic_rewrite True True 1323 (ct_in_state' (Not \<circ> runnable') and cur_tcb' and obj_at' (Not \<circ> tcbQueued) t) 1324 (switchToThread t) 1325 (do Arch.switchToThread t; setCurThread t od)" 1326 apply (simp add: switchToThread_def Thread_H.switchToThread_def) 1327 apply (rule monadic_rewrite_imp) 1328 apply (rule monadic_rewrite_trans) 1329 apply (rule monadic_rewrite_bind_tail) 1330 apply (rule monadic_rewrite_bind) 1331 apply (rule tcbSchedDequeue_rewrite) 1332 apply (rule monadic_rewrite_refl) 1333 apply (wp Arch_switchToThread_obj_at_pre)+ 1334 apply (rule monadic_rewrite_bind_tail) 1335 apply (rule monadic_rewrite_symb_exec) 1336 apply (wp+, simp) 1337 apply (rule monadic_rewrite_refl) 1338 apply (wp) 1339 apply (clarsimp simp: comp_def) 1340 done 1341 1342lemma threadGet_isolatable: 1343 assumes v: "\<And>tsr. \<forall>tcb. f (put_tcb_state_regs_tcb tsr tcb) = f tcb" 1344 shows "thread_actions_isolatable idx (threadGet f t)" 1345 apply (clarsimp simp: threadGet_def thread_actions_isolatable_def 1346 isolate_thread_actions_def split_def 1347 getObject_get_assert liftM_def 1348 bind_select_f_bind[symmetric] 1349 select_f_returns select_f_asserts bind_assoc) 1350 apply (clarsimp simp: monadic_rewrite_def exec_gets 1351 getSchedulerAction_def) 1352 apply (simp add: obj_at_partial_overwrite_If) 1353 apply (rule bind_apply_cong[OF refl]) 1354 apply (clarsimp simp: exec_gets exec_modify o_def 1355 ksPSpace_update_partial_id in_monad) 1356 apply (erule obj_atE') 1357 apply (clarsimp simp: projectKOs 1358 partial_overwrite_def put_tcb_state_regs_def 1359 cong: if_cong) 1360 apply (simp add: projectKO_opt_tcb v split: if_split) 1361 done 1362 1363 lemma switchToThread_isolatable: 1364 "thread_actions_isolatable idx (Arch.switchToThread t)" 1365 apply (simp add: X64_H.switchToThread_def 1366 storeWordUser_def stateAssert_def2) 1367 apply (intro thread_actions_isolatable_bind[OF _ _ hoare_pre(1)] 1368 gets_isolatable setVMRoot_isolatable 1369 thread_actions_isolatable_if 1370 doMachineOp_isolatable 1371 threadGet_isolatable [OF all_tcbI] 1372 thread_actions_isolatable_returns 1373 thread_actions_isolatable_fail) 1374 done 1375 1376lemma monadic_rewrite_trans_dup: 1377 "\<lbrakk> monadic_rewrite F E P f g; monadic_rewrite F E P g h \<rbrakk> 1378 \<Longrightarrow> monadic_rewrite F E P f h" 1379 by (auto simp add: monadic_rewrite_def) 1380 1381 1382lemma setCurThread_isolatable: 1383 "thread_actions_isolatable idx (setCurThread t)" 1384 by (simp add: setCurThread_def modify_isolatable) 1385 1386lemma isolate_thread_actions_tcbs_at: 1387 assumes f: "\<And>x. \<lbrace>tcb_at' (idx x)\<rbrace> f \<lbrace>\<lambda>rv. tcb_at' (idx x)\<rbrace>" shows 1388 "\<lbrace>\<lambda>s. \<forall>x. tcb_at' (idx x) s\<rbrace> 1389 isolate_thread_actions idx f f' f'' \<lbrace>\<lambda>p s. \<forall>x. tcb_at' (idx x) s\<rbrace>" 1390 apply (simp add: isolate_thread_actions_def split_def) 1391 apply wp 1392 apply clarsimp 1393 apply (simp add: obj_at_partial_overwrite_If use_valid[OF _ f]) 1394 done 1395 1396lemma isolate_thread_actions_rewrite_bind: 1397 "\<lbrakk> inj idx; monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) 1398 f (isolate_thread_actions idx f' f'' f'''); 1399 \<And>x. monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) 1400 (g x) 1401 (isolate_thread_actions idx (g' x) g'' g'''); 1402 thread_actions_isolatable idx f'; \<And>x. thread_actions_isolatable idx (g' x); 1403 \<And>x. \<lbrace>tcb_at' (idx x)\<rbrace> f' \<lbrace>\<lambda>rv. tcb_at' (idx x)\<rbrace> \<rbrakk> 1404 \<Longrightarrow> monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) 1405 (f >>= g) (isolate_thread_actions idx 1406 (f' >>= g') (g'' o f'') (g''' o f'''))" 1407 apply (rule monadic_rewrite_imp) 1408 apply (rule monadic_rewrite_trans) 1409 apply (rule monadic_rewrite_bind, assumption+) 1410 apply (wp isolate_thread_actions_tcbs_at) 1411 apply simp 1412 apply (subst isolate_thread_actions_wrap_bind, assumption) 1413 apply (rule monadic_rewrite_in_isolate_thread_actions, assumption) 1414 apply (rule monadic_rewrite_transverse) 1415 apply (rule monadic_rewrite_bind2) 1416 apply (erule(1) thread_actions_isolatableD) 1417 apply (rule thread_actions_isolatableD, assumption+) 1418 apply (rule hoare_vcg_all_lift, assumption) 1419 apply (simp add: liftM_def id_def) 1420 apply (rule monadic_rewrite_refl) 1421 apply (simp add: obj_at_partial_overwrite_If) 1422 done 1423 1424definition 1425 "copy_register_tsrs src dest r r' rf tsrs 1426 = tsrs (dest := TCBStateRegs (tsrState (tsrs dest)) 1427 ((tsrContext (tsrs dest)) (r' := rf (tsrContext (tsrs src) r))))" 1428 1429lemma tcb_at_KOTCB_upd: 1430 "tcb_at' (idx x) s \<Longrightarrow> 1431 tcb_at' p (ksPSpace_update (\<lambda>ps. ps(idx x \<mapsto> KOTCB tcb)) s) 1432 = tcb_at' p s" 1433 apply (clarsimp simp: obj_at'_def projectKOs objBits_simps 1434 split: if_split) 1435 apply (simp add: ps_clear_def) 1436 done 1437 1438definition 1439 "set_register_tsrs dest r v tsrs 1440 = tsrs (dest := TCBStateRegs (tsrState (tsrs dest)) 1441 ((tsrContext (tsrs dest)) (r := v)))" 1442 1443 1444lemma set_register_isolate: 1445 "\<lbrakk> inj idx; idx y = dest \<rbrakk> \<Longrightarrow> 1446 monadic_rewrite False True 1447 (\<lambda>s. \<forall>x. tcb_at' (idx x) s) 1448 (asUser dest (setRegister r v)) 1449 (isolate_thread_actions idx (return ()) 1450 (set_register_tsrs y r v) id)" 1451 apply (simp add: asUser_def split_def bind_assoc 1452 getRegister_def setRegister_def 1453 select_f_returns isolate_thread_actions_def 1454 getSchedulerAction_def) 1455 apply (simp add: threadGet_def liftM_def getObject_get_assert 1456 bind_assoc threadSet_def 1457 setObject_modify_assert) 1458 apply (clarsimp simp: monadic_rewrite_def exec_gets 1459 exec_modify tcb_at_KOTCB_upd) 1460 apply (clarsimp simp: simpler_modify_def 1461 intro!: kernel_state.fold_congs[OF refl refl]) 1462 apply (clarsimp simp: set_register_tsrs_def o_def 1463 partial_overwrite_fun_upd 1464 partial_overwrite_get_tcb_state_regs) 1465 apply (drule_tac x=y in spec) 1466 apply (clarsimp simp: obj_at'_def projectKOs objBits_simps 1467 cong: if_cong) 1468 apply (case_tac obj) 1469 apply (simp add: projectKO_opt_tcb put_tcb_state_regs_def 1470 put_tcb_state_regs_tcb_def get_tcb_state_regs_def 1471 atcbContextGet_def 1472 cong: if_cong) 1473 done 1474 1475lemma copy_register_isolate: 1476 "\<lbrakk> inj idx; idx x = src; idx y = dest \<rbrakk> \<Longrightarrow> 1477 monadic_rewrite False True 1478 (\<lambda>s. \<forall>x. tcb_at' (idx x) s) 1479 (do v \<leftarrow> asUser src (getRegister r); 1480 asUser dest (setRegister r' (rf v)) od) 1481 (isolate_thread_actions idx (return ()) 1482 (copy_register_tsrs x y r r' rf) id)" 1483 apply (simp add: asUser_def split_def bind_assoc 1484 getRegister_def setRegister_def 1485 select_f_returns isolate_thread_actions_def 1486 getSchedulerAction_def) 1487 apply (simp add: threadGet_def liftM_def getObject_get_assert 1488 bind_assoc threadSet_def 1489 setObject_modify_assert) 1490 apply (clarsimp simp: monadic_rewrite_def exec_gets 1491 exec_modify tcb_at_KOTCB_upd) 1492 apply (clarsimp simp: simpler_modify_def 1493 intro!: kernel_state.fold_congs[OF refl refl]) 1494 apply (clarsimp simp: copy_register_tsrs_def o_def 1495 partial_overwrite_fun_upd 1496 partial_overwrite_get_tcb_state_regs) 1497 apply (frule_tac x=x in spec, drule_tac x=y in spec) 1498 apply (clarsimp simp: obj_at'_def projectKOs objBits_simps 1499 cong: if_cong) 1500 apply (case_tac obj, case_tac obja) 1501 apply (simp add: projectKO_opt_tcb put_tcb_state_regs_def 1502 put_tcb_state_regs_tcb_def get_tcb_state_regs_def 1503 atcbContextGet_def 1504 cong: if_cong) 1505 apply (auto simp: fun_eq_iff split: if_split) 1506 done 1507 1508lemmas monadic_rewrite_bind_alt 1509 = monadic_rewrite_trans[OF monadic_rewrite_bind_tail monadic_rewrite_bind_head, rotated -1] 1510 1511 1512lemma monadic_rewrite_isolate_final2: 1513 assumes mr: "monadic_rewrite F E Q f g" 1514 and eqs: "\<And>s tsrs. \<lbrakk> P s; tsrs = get_tcb_state_regs o ksPSpace s o idx \<rbrakk> 1515 \<Longrightarrow> f' tsrs = g' tsrs" 1516 "\<And>s. P s \<Longrightarrow> f'' (ksSchedulerAction s) = g'' (ksSchedulerAction s)" 1517 "\<And>s tsrs sa. R s \<Longrightarrow> 1518 Q ((ksPSpace_update (partial_overwrite idx tsrs) 1519 s) (| ksSchedulerAction := sa |))" 1520 shows 1521 "monadic_rewrite F E (P and R) 1522 (isolate_thread_actions idx f f' f'') 1523 (isolate_thread_actions idx g g' g'')" 1524 apply (simp add: isolate_thread_actions_def split_def) 1525 apply (rule monadic_rewrite_imp) 1526 apply (rule monadic_rewrite_bind_tail)+ 1527 apply (rule_tac P="\<lambda> s'. Q s" in monadic_rewrite_bind) 1528 apply (insert mr)[1] 1529 apply (simp add: monadic_rewrite_def select_f_def) 1530 apply auto[1] 1531 apply (rule_tac P="P and (\<lambda>s. tcbs = get_tcb_state_regs o ksPSpace s o idx 1532 \<and> sa = ksSchedulerAction s)" 1533 in monadic_rewrite_refl3) 1534 apply (clarsimp simp: exec_modify eqs return_def) 1535 apply wp+ 1536 apply (clarsimp simp: o_def eqs) 1537 done 1538 1539lemmas monadic_rewrite_isolate_final 1540 = monadic_rewrite_isolate_final2[where R=\<top>, OF monadic_rewrite_refl2, simplified] 1541 1542lemma copy_registers_isolate_general: 1543 "\<lbrakk> inj idx; idx x = t; idx y = t' \<rbrakk> \<Longrightarrow> 1544 monadic_rewrite False True 1545 (\<lambda>s. \<forall>x. tcb_at' (idx x) s) 1546 (mapM_x (\<lambda>r. do v \<leftarrow> asUser t (getRegister (f r)); 1547 asUser t' (setRegister (f' r) (rf r v)) 1548 od) 1549 regs) 1550 (isolate_thread_actions idx 1551 (return ()) (foldr (\<lambda>r. copy_register_tsrs x y (f r) (f' r) (rf r)) (rev regs)) id)" 1552 apply (induct regs) 1553 apply (simp add: mapM_x_Nil) 1554 apply (clarsimp simp: monadic_rewrite_def liftM_def bind_assoc 1555 isolate_thread_actions_def 1556 split_def exec_gets getSchedulerAction_def 1557 select_f_returns o_def ksPSpace_update_partial_id) 1558 apply (simp add: return_def simpler_modify_def) 1559 apply (simp add: mapM_x_Cons) 1560 apply (rule monadic_rewrite_imp) 1561 apply (rule monadic_rewrite_trans) 1562 apply (rule isolate_thread_actions_rewrite_bind, assumption) 1563 apply (rule copy_register_isolate, assumption+) 1564 apply (rule thread_actions_isolatable_returns)+ 1565 apply wp 1566 apply (rule monadic_rewrite_isolate_final[where P=\<top>], simp+) 1567 done 1568 1569lemmas copy_registers_isolate = copy_registers_isolate_general[where f="\<lambda>x. x" and f'="\<lambda>x. x" and rf="\<lambda>_ x. x"] 1570 1571lemma setSchedulerAction_isolate: 1572 "inj idx \<Longrightarrow> 1573 monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) 1574 (setSchedulerAction sa) 1575 (isolate_thread_actions idx (return ()) id (\<lambda>_. sa))" 1576 apply (clarsimp simp: monadic_rewrite_def liftM_def bind_assoc 1577 isolate_thread_actions_def select_f_returns 1578 exec_gets getSchedulerAction_def o_def 1579 ksPSpace_update_partial_id setSchedulerAction_def) 1580 apply (simp add: simpler_modify_def) 1581 done 1582 1583lemma updateMDB_isolatable: 1584 "thread_actions_isolatable idx (updateMDB slot f)" 1585 apply (simp add: updateMDB_def thread_actions_isolatable_return 1586 split: if_split) 1587 apply (intro impI thread_actions_isolatable_bind[OF _ _ hoare_pre(1)] 1588 getCTE_isolatable setCTE_isolatable, 1589 (wp | simp)+) 1590 done 1591 1592lemma clearUntypedFreeIndex_isolatable: 1593 "thread_actions_isolatable idx (clearUntypedFreeIndex slot)" 1594 apply (simp add: clearUntypedFreeIndex_def getSlotCap_def) 1595 apply (rule thread_actions_isolatable_bind) 1596 apply (rule getCTE_isolatable) 1597 apply (simp split: capability.split, safe intro!: thread_actions_isolatable_return) 1598 apply (simp add: updateTrackedFreeIndex_def getSlotCap_def) 1599 apply (intro thread_actions_isolatable_bind getCTE_isolatable 1600 modify_isolatable) 1601 apply (wp | simp)+ 1602 done 1603 1604lemma emptySlot_isolatable: 1605 "thread_actions_isolatable idx (emptySlot slot NullCap)" 1606 apply (simp add: emptySlot_def updateCap_def case_Null_If Retype_H.postCapDeletion_def 1607 cong: if_cong) 1608 apply (intro thread_actions_isolatable_bind[OF _ _ hoare_pre(1)] 1609 clearUntypedFreeIndex_isolatable 1610 thread_actions_isolatable_if 1611 getCTE_isolatable setCTE_isolatable 1612 thread_actions_isolatable_return 1613 updateMDB_isolatable, 1614 (wp | simp)+) 1615 done 1616 1617lemmas fastpath_isolatables 1618 = setEndpoint_isolatable getCTE_isolatable 1619 assert_isolatable cteInsert_isolatable 1620 switchToThread_isolatable setCurThread_isolatable 1621 emptySlot_isolatable updateMDB_isolatable 1622 thread_actions_isolatable_returns 1623 1624lemmas fastpath_isolate_rewrites 1625 = isolate_thread_actions_threadSet_tcbState isolate_thread_actions_asUser 1626 copy_registers_isolate setSchedulerAction_isolate 1627 fastpath_isolatables[THEN thread_actions_isolatableD] 1628 1629lemma lookupIPCBuffer_isolatable: 1630 "thread_actions_isolatable idx (lookupIPCBuffer w t)" 1631 apply (simp add: lookupIPCBuffer_def) 1632 apply (rule thread_actions_isolatable_bind) 1633 apply (clarsimp simp: put_tcb_state_regs_tcb_def threadGet_isolatable 1634 getThreadBufferSlot_def locateSlot_conv getSlotCap_def 1635 split: tcb_state_regs.split)+ 1636 apply (rule thread_actions_isolatable_bind) 1637 apply (clarsimp simp: thread_actions_isolatable_return 1638 getCTE_isolatable 1639 assert_isolatable 1640 split: capability.split arch_capability.split bool.split)+ 1641 apply (rule thread_actions_isolatable_if) 1642 apply (rule thread_actions_isolatable_bind) 1643 apply (simp add: assert_isolatable thread_actions_isolatable_return | wp)+ 1644 done 1645 1646lemma setThreadState_rewrite_simple: 1647 "monadic_rewrite True True 1648 (\<lambda>s. (runnable' st \<or> ksSchedulerAction s \<noteq> ResumeCurrentThread \<or> t \<noteq> ksCurThread s) \<and> tcb_at' t s) 1649 (setThreadState st t) 1650 (threadSet (tcbState_update (\<lambda>_. st)) t)" 1651 apply (simp add: setThreadState_def) 1652 apply (rule monadic_rewrite_imp) 1653 apply (rule monadic_rewrite_trans) 1654 apply (rule monadic_rewrite_bind_tail) 1655 apply (rule monadic_rewrite_trans) 1656 apply (rule monadic_rewrite_bind_tail)+ 1657 apply (simp add: when_def) 1658 apply (rule monadic_rewrite_gen_asm) 1659 apply (subst if_not_P) 1660 apply assumption 1661 apply (rule monadic_rewrite_refl) 1662 apply wp+ 1663 apply (rule monadic_rewrite_symb_exec2, 1664 (wp empty_fail_isRunnable 1665 | (simp only: getCurThread_def getSchedulerAction_def 1666 , rule empty_fail_gets))+)+ 1667 apply (rule monadic_rewrite_refl) 1668 apply (simp add: conj_comms, wp hoare_vcg_imp_lift threadSet_tcbState_st_tcb_at') 1669 apply (clarsimp simp: obj_at'_def sch_act_simple_def st_tcb_at'_def) 1670 apply (rule monadic_rewrite_refl) 1671 apply clarsimp 1672 done 1673 1674end 1675 1676end 1677