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_longlong_' (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 < 23" 146 by (cases hr, simp_all add: "StrictC'_register_defs") 147 148lemma register_from_H_sless: 149 "register_from_H hr <s 23" 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 = "((user_regs o 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 cregs_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 is_aligned_tcb_ptr_to_ctcb_ptr: 264 "obj_at' (P :: tcb \<Rightarrow> bool) p s 265 \<Longrightarrow> is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr p)) ctcb_size_bits" 266 apply (clarsimp simp: obj_at'_def objBits_simps' projectKOs 267 tcb_ptr_to_ctcb_ptr_def ctcb_offset_defs) 268 apply (erule aligned_add_aligned, simp_all add: word_bits_conv) 269 apply (simp add: is_aligned_def) 270 done 271 272lemma sanitiseRegister_spec: 273 "\<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>) 274 Call sanitiseRegister_'proc 275 \<lbrace>\<acute>ret__unsigned_long = sanitiseRegister t r v\<rbrace>" 276 apply vcg 277 apply (case_tac r; simp add: C_register_defs sanitiseRegister_def sanitiseOrFlags_def sanitiseAndFlags_def) (* long *) 278 by word_bitwise 279 280lemma getObject_tcb_wp': 281 "\<lbrace>\<lambda>s. \<forall>t. ko_at' (t :: tcb) p s \<longrightarrow> Q t s\<rbrace> getObject p \<lbrace>Q\<rbrace>" 282 by (clarsimp simp: getObject_def valid_def in_monad 283 split_def objBits_simps' loadObject_default_def 284 projectKOs obj_at'_def in_magnitude_check) 285 286lemma ccorres_pre_getObject_tcb: 287 assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c" 288 shows "ccorres r xf 289 (\<lambda>s. (\<forall>tcb. ko_at' tcb p s \<longrightarrow> P tcb s)) 290 {s. \<forall> tcb tcb'. cslift s (tcb_ptr_to_ctcb_ptr p) = Some tcb' \<and> ctcb_relation tcb tcb' 291 \<longrightarrow> s \<in> P' tcb} 292 hs (getObject p >>= (\<lambda>rv :: tcb. f rv)) c" 293 apply (rule ccorres_guard_imp2) 294 apply (rule ccorres_symb_exec_l) 295 apply (rule ccorres_guard_imp2) 296 apply (rule cc) 297 apply (rule conjI) 298 apply (rule_tac Q="ko_at' rv p s" in conjunct1) 299 apply assumption 300 apply assumption 301 apply (wpsimp wp: empty_fail_getObject getObject_tcb_wp')+ 302 apply (erule cmap_relationE1[OF cmap_relation_tcb], 303 erule ko_at_projectKO_opt) 304 apply simp 305 done 306 307(* FIXME move to Invariants_H *) 308lemma invs_cicd_arch_state' [elim!]: 309 "all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> valid_arch_state' s" 310 by (simp add: all_invs_but_ct_idle_or_in_cur_domain'_def valid_state'_def) 311 312(* FIXME move to Invariants_H *) 313lemma invs_cicd_no_0_obj'[elim!]: 314 "all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> no_0_obj' s" 315 by (simp add: all_invs_but_ct_idle_or_in_cur_domain'_def valid_state'_def valid_pspace'_def) 316 317(* FIXME: MOVE, probably to CSpace_RAB *) 318lemma ccorres_gen_asm2_state: 319 assumes rl: "\<And>s. P s \<Longrightarrow> ccorres r xf G G' hs a c" 320 shows "ccorres r xf G (G' \<inter> {s. P s}) hs a c" 321proof (rule ccorres_guard_imp2) 322 show "ccorres r xf G (G' \<inter> {_. \<exists>s. P s}) hs a c" 323 apply (rule ccorres_gen_asm2) 324 apply (erule exE) 325 apply (erule rl) 326 done 327next 328 fix s s' 329 assume "(s, s') \<in> rf_sr" and "G s" and "s' \<in> G' \<inter> {s. P s}" 330 thus "G s \<and> s' \<in> (G' \<inter> {_. \<exists>s. P s})" 331 by (clarsimp elim!: exI simp: Collect_const_mem) 332qed 333 334lemma cap_case_TCBCap2: 335 "(case cap of ThreadCap pd 336 \<Rightarrow> f pd | _ \<Rightarrow> g) 337 = (if isThreadCap cap 338 then f (capTCBPtr cap) 339 else g)" 340 by (simp add: isCap_simps 341 split: capability.split arch_capability.split) 342 343lemma length_of_msgRegisters: 344 "length X64_H.msgRegisters = 4" 345 by (auto simp: msgRegisters_unfold) 346thm setMRs_def X64.msgRegisters_def 347lemma setMRs_single: 348 "setMRs thread buffer [val] = do y \<leftarrow> asUser thread (setRegister register.R10 val); 349 return 1 350 od" 351 apply (clarsimp simp: setMRs_def length_of_msgRegisters zipWithM_x_def zipWith_def split: option.splits) 352 apply (subst zip_commute, subst zip_singleton) 353 apply (simp add: length_of_msgRegisters length_0_conv[symmetric]) 354 apply (clarsimp simp: msgRegisters_unfold sequence_x_def) 355 done 356 357end 358end 359