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 CSpace_All 12imports CSpace_RAB_C CSpace_C 13begin 14 15context kernel_m 16begin 17 18 19 20 21abbreviation 22 "lookupCapAndSlot_xf \<equiv> liftxf errstate lookupCapAndSlot_ret_C.status_C 23 (\<lambda> x . (lookupCapAndSlot_ret_C.cap_C x, lookupCapAndSlot_ret_C.slot_C x)) 24 ret__struct_lookupCapAndSlot_ret_C_'" 25 26 27 28 29(* FIXME: move *) 30lemma ccorres_return_into_rel: 31 "ccorres (\<lambda>rv rv'. r (f rv) rv') xf G G' hs a c 32 \<Longrightarrow> ccorres r xf G G' hs (a >>= (\<lambda>rv. return (f rv))) c" 33 by (simp add: liftM_def[symmetric] o_def) 34 35lemma lookupCap_ccorres': 36 "ccorres (lookup_failure_rel \<currency> ccap_relation) lookupCap_xf 37 (valid_pspace' and tcb_at' a) 38 (UNIV \<inter> {s. cPtr_' s = b} \<inter> {s. thread_' s = tcb_ptr_to_ctcb_ptr a}) [] 39 (lookupCap a b) (Call lookupCap_'proc)" 40 apply (cinit lift: cPtr_' thread_' simp: lookupCapAndSlot_def liftME_def bindE_assoc) 41 42 apply (ctac (no_vcg) add: lookupSlotForThread_ccorres') 43 \<comment> \<open>case where lu_ret.status is EXCEPTION_NONE\<close> 44 apply (simp add: split_beta cong:call_ignore_cong) 45 apply csymbr \<comment> \<open>call status_C_update\<close> 46 apply (simp add: Collect_const[symmetric] lookupSlot_raw_rel_def liftE_def 47 del: Collect_const) 48 apply (rule ccorres_move_c_guard_cte) 49 apply (ctac ) 50 apply (rule ccorres_return_CE [unfolded returnOk_def, simplified], simp+)[1] 51 apply wp 52 apply vcg 53 \<comment> \<open>case where lu_ret.status is *not* EXCEPTION_NONE\<close> 54 apply simp 55 apply (rule ccorres_split_throws) 56 apply (rule ccorres_rhs_assoc)+ 57 apply csymbr 58 apply csymbr \<comment> \<open>call cap_null_cap_new_'proc\<close> 59 apply csymbr 60 apply (rule ccorres_return_C_errorE, simp+)[1] 61 apply vcg 62 apply (wp | simp)+ 63 64 \<comment> \<open>last subgoal\<close> 65 apply (clarsimp simp: valid_pspace_valid_objs') 66 apply (intro impI conjI allI) 67 apply (simp add: lookupSlot_raw_rel_def) 68 apply (rule_tac y="ret___struct_lookupCap_ret_C_' s" for s 69 in arg_cong, fastforce) 70 apply simp 71 apply (case_tac err, simp+) [1] 72done 73 74lemma lookupCap_ccorres: 75 "ccorres (lookup_failure_rel \<currency> ccap_relation) lookupCap_xf 76 (\<lambda>s. invs' s \<and> (tcb_at' a s)) 77 (UNIV \<inter> {s. cPtr_' s = b} \<inter> {s. thread_' s = tcb_ptr_to_ctcb_ptr a}) [] 78 (lookupCap a b) (Call lookupCap_'proc)" 79 apply (rule ccorres_guard_imp2, rule lookupCap_ccorres') 80 apply fastforce 81 done 82 83 84lemma lookupCapAndSlot_ccorres : 85 "ccorres 86 (lookup_failure_rel \<currency> (\<lambda>(c,s) (c',s'). ccap_relation c c' \<and> s'= Ptr s)) lookupCapAndSlot_xf 87 (\<lambda>s. invs' s \<and> tcb_at' thread s) 88 (UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>cPtr = cPtr\<rbrace> ) [] 89 (lookupCapAndSlot thread cPtr) 90 (Call lookupCapAndSlot_'proc)" 91 apply (cinit lift: thread_' cPtr_') 92 93 apply (ctac (no_vcg)) 94 \<comment> \<open>case where lu_ret.status is EXCEPTION_NONE\<close> 95 apply (simp add: split_beta cong:call_ignore_cong) 96 apply csymbr \<comment> \<open>call status_C_update\<close> 97 apply csymbr \<comment> \<open>call slot_C_update\<close> 98 apply (simp add: Collect_const[symmetric] lookupSlot_raw_rel_def liftE_bindE 99 del: Collect_const) 100 apply (rule ccorres_move_c_guard_cte) 101 apply (rule_tac P="cte_at' rv" and P'=UNIV in ccorres_from_vcg_throws) 102 apply (rule allI, rule conseqPre, vcg) 103 apply (clarsimp simp: Bex_def in_monad getSlotCap_def in_getCTE2 cte_wp_at_ctes_of) 104 apply (erule(1) cmap_relationE1[OF cmap_relation_cte]) 105 apply (simp add: ccte_relation_ccap_relation typ_heap_simps') 106 \<comment> \<open>case where lu_ret.status is *not* EXCEPTION_NONE\<close> 107 apply simp 108 apply (rule ccorres_split_throws) 109 apply (rule ccorres_rhs_assoc)+ 110 apply csymbr+ 111 apply (rule ccorres_return_C_errorE, simp+)[1] 112 113 apply vcg 114 apply (wp | simp)+ 115 116 \<comment> \<open>last subgoal\<close> 117 apply clarsimp 118 apply (rule conjI, fastforce) 119 apply clarsimp 120 apply (case_tac err, simp+) [1] 121done 122 123 124(* FIXME: move *) 125lemma injection_handler_liftM: 126 "injection_handler f 127 = liftM (\<lambda>v. case v of Inl ex \<Rightarrow> Inl (f ex) | Inr rv \<Rightarrow> Inr rv)" 128 apply (intro ext, simp add: injection_handler_def liftM_def 129 handleE'_def) 130 apply (rule bind_apply_cong, rule refl) 131 apply (simp add: throwError_def split: sum.split) 132 done 133 134lemma lookupErrorOnFailure_ccorres: 135 "ccorres (f \<currency> r) xf P P' hs a c 136 \<Longrightarrow> ccorres ((\<lambda>x y z. \<exists>w. x = FailedLookup isSource w \<and> f w y z) \<currency> r) 137 xf P P' hs 138 (lookupErrorOnFailure isSource a) c" 139 apply (simp add: lookupError_injection injection_handler_liftM) 140 apply (erule ccorres_rel_imp) 141 apply (auto split: sum.split) 142 done 143 144 145lemma lookup_failure_rel_fault_lift: 146 " \<lbrakk> st \<noteq> scast EXCEPTION_NONE; 147 lookup_failure_rel err st (errstate t)\<rbrakk> 148 \<Longrightarrow> \<exists>v. lookup_fault_lift (current_lookup_fault_' (globals t)) = Some v \<and> lookup_fault_to_H v = err" 149 apply (case_tac err, clarsimp+) 150 done 151 152lemma le_64_mask_eq: 153 "(bits::machine_word) \<le> 64 \<Longrightarrow> bits && mask 7 = bits" 154 apply (rule less_mask_eq, simp) 155 apply (erule le_less_trans, simp) 156 done 157 158lemma lookupSlotForCNodeOp_ccorres': 159 "ccorres 160 (syscall_error_rel \<currency> (\<lambda>w w'. w'= Ptr w \<and> depth \<le> word_bits)) lookupSlot_xf 161 (\<lambda>s. valid_pspace' s \<and> s \<turnstile>' croot \<and> depth < 2 ^ word_bits) 162 (UNIV \<inter> {s. capptr_' s = capptr} \<inter> 163 {s. to_bool (isSource_' s) = isSource} \<inter> 164 {s. ccap_relation croot (root___struct_cap_C_' s)} \<inter> 165 {s. depth_' s = of_nat depth} ) [] 166 (lookupSlotForCNodeOp isSource croot capptr depth) 167 (Call lookupSlotForCNodeOp_'proc)" 168 apply (cinit lift: capptr_' isSource_' root___struct_cap_C_' depth_') 169 apply csymbr \<comment> \<open>slot_C_update\<close> 170 apply csymbr \<comment> \<open>cap_get_capType\<close> 171 172 apply (rule_tac Q=\<top> and Q'=\<top> in ccorres_if_cond_throws2) 173 \<comment> \<open>correspondance of Haskell and C conditions\<close> 174 apply (clarsimp simp: Collect_const_mem cap_get_tag_isCap) 175 176 \<comment> \<open>case where root is *not* a CNode => throw InvalidRoot\<close> 177 apply simp 178 apply (rule_tac P=\<top> and P' =UNIV in ccorres_from_vcg_throws) 179 apply (rule allI, rule conseqPre, vcg) 180 apply (clarsimp simp: throwError_def return_def syscall_error_rel_def) 181 apply (clarsimp simp: EXCEPTION_NONE_def EXCEPTION_SYSCALL_ERROR_def) 182 apply (drule_tac lookup_fault_lift_invalid_root) 183 apply clarsimp 184 apply (subst syscall_error_to_H_cases(6), simp+)[1] 185 186 \<comment> \<open>case where root is a CNode\<close> 187 apply (simp add: rangeCheck_def) 188 apply csymbr 189 apply (rule ccorres_Cond_rhs_Seq) 190 apply (rule_tac P="depth < 2 ^ word_bits" in ccorres_gen_asm) 191 apply (drule unat_of_nat64) 192 apply (simp add: unlessE_def fromIntegral_def integral_inv) 193 apply (rule ccorres_cond_true_seq) 194 apply (rule ccorres_split_throws) 195 apply (rule_tac P= \<top> and P' =UNIV in ccorres_from_vcg_throws) 196 apply (rule allI, rule conseqPre, vcg) 197 apply (clarsimp simp: throwError_def return_def syscall_error_rel_def 198 word_sle_def syscall_error_to_H_cases 199 word_size exception_defs) 200 apply vcg 201 apply csymbr 202 apply (rule_tac Q="\<lambda>s. depth < 2 ^ word_bits" and Q'=\<top> in ccorres_split_unless_throwError_cond) 203 \<comment> \<open>correspondance of Haskell and C conditions\<close> 204 apply (clarsimp simp: Collect_const_mem fromIntegral_def integral_inv) 205 apply (simp add: word_size unat_of_nat64 word_less_nat_alt 206 word_less_1[symmetric] linorder_not_le) 207 208 \<comment> \<open>case of RangeError\<close> 209 apply (rule_tac P= \<top> and P' =UNIV in ccorres_from_vcg_throws) 210 apply (rule allI, rule conseqPre, vcg) 211 apply (clarsimp simp: throwError_def return_def syscall_error_rel_def) 212 apply (clarsimp simp: EXCEPTION_NONE_def EXCEPTION_SYSCALL_ERROR_def) 213 apply (subst syscall_error_to_H_cases(4), simp+)[1] 214 apply (simp add: word_size word_sle_def) 215 216 \<comment> \<open>case where there is *no* RangeError\<close> 217 apply (rule_tac xf'=lookupSlot_xf in ccorres_rel_imp) 218 apply (rule_tac r="\<lambda>w w'. w'= Ptr w" 219 and f="\<lambda> st fl es. fl = scast EXCEPTION_SYSCALL_ERROR \<and> 220 syscall_error_to_H (errsyscall es) (errlookup_fault es) = Some (FailedLookup isSource st)" 221 in lookupErrorOnFailure_ccorres) 222 apply (ctac (no_vcg)) \<comment> \<open>resolveAddressBits\<close> 223 \<comment> \<open>case where resolveAddressBits results in EXCEPTION_NONE\<close> 224 apply clarsimp 225 apply (rule_tac A=\<top> and A'=UNIV in ccorres_guard_imp2) 226 apply (rule_tac Q=\<top> and Q'=\<top> in ccorres_if_cond_throws2) 227 \<comment> \<open>correspondance of Haskell and C conditions\<close> 228 apply (clarsimp simp: Collect_const_mem unat_gt_0) 229 \<comment> \<open>case where bits are remaining\<close> 230 apply (rule_tac P= \<top> and P' =UNIV in ccorres_from_vcg_throws) 231 apply (rule allI, rule conseqPre, vcg) 232 apply (clarsimp simp: throwError_def return_def) 233 apply (clarsimp simp: EXCEPTION_NONE_def EXCEPTION_SYSCALL_ERROR_def) 234 apply (subst syscall_error_to_H_cases(6), simp+)[1] 235 apply (simp add: lookup_fault_depth_mismatch_lift) 236 apply (erule le_64_mask_eq) 237 238 \<comment> \<open>case where *no* bits are remaining\<close> 239 apply csymbr \<comment> \<open>slot_C_update\<close> 240 apply csymbr \<comment> \<open>status_C_update\<close> 241 apply (rule ccorres_return_CE, simp+)[1] 242 243 apply vcg 244 245 \<comment> \<open>guard_imp subgoal\<close> 246 apply clarsimp 247 248 \<comment> \<open>case where resolveAddressBits does *not* results in EXCEPTION_NONE\<close> 249 apply clarsimp 250 apply (rule_tac P= \<top> and P' ="\<lbrace>\<exists>v. (lookup_fault_lift (\<acute>current_lookup_fault)) = Some v 251 \<and> lookup_fault_to_H v = err \<rbrace>" 252 in ccorres_from_vcg_throws) 253 apply (rule allI, rule conseqPre, vcg) 254 apply (clarsimp simp: throwError_def return_def) 255 apply (clarsimp simp: EXCEPTION_NONE_def EXCEPTION_SYSCALL_ERROR_def) 256 apply (subst syscall_error_to_H_cases(6), simp+)[1] 257 apply wp 258 259 \<comment> \<open>rel_imp\<close> 260 apply clarsimp 261 apply (case_tac x, clarsimp) 262 apply (simp add: syscall_error_rel_def errstate_def) 263 apply (clarsimp simp: word_bits_def word_size fromIntegral_def 264 integral_inv) 265 266 apply vcg 267 apply vcg 268 269 \<comment> \<open>last subgoal\<close> 270 apply (clarsimp simp: if_1_0_0 to_bool_def true_def word_size 271 fromIntegral_def integral_inv) 272 apply (case_tac "cap_get_tag root___struct_cap_C = scast cap_cnode_cap") 273 prefer 2 apply clarsimp 274 apply (clarsimp simp: unat_of_nat64 word_sle_def) 275 apply (simp add: Collect_const_mem lookup_failure_rel_fault_lift) 276 done 277 278 279lemma lookupSlotForCNodeOp_ccorres: 280 "ccorres 281 (syscall_error_rel \<currency> (\<lambda>w w'. w'= Ptr w \<and> depth \<le> word_bits)) lookupSlot_xf 282 (\<lambda>s. invs' s \<and> s \<turnstile>' croot \<and> depth < 2 ^ word_bits) 283 (UNIV \<inter> {s. capptr_' s = capptr} \<inter> 284 {s. to_bool (isSource_' s) = isSource} \<inter> 285 {s. ccap_relation croot (root___struct_cap_C_' s)} \<inter> 286 {s. depth_' s = of_nat depth} ) [] 287 (lookupSlotForCNodeOp isSource croot capptr depth) 288 (Call lookupSlotForCNodeOp_'proc)" 289 apply (rule ccorres_guard_imp2, rule lookupSlotForCNodeOp_ccorres') 290 apply fastforce 291 done 292 293lemma lookupSourceSlot_ccorres': 294 "ccorres 295 (syscall_error_rel \<currency> (\<lambda>w w'. w'= Ptr w \<and> depth \<le> word_bits)) lookupSlot_xf 296 (\<lambda>s. valid_pspace' s \<and> s \<turnstile>' croot \<and> depth < 2 ^ word_bits) 297 (UNIV \<inter> {s. capptr_' s = capptr} \<inter> 298 {s. ccap_relation croot (root___struct_cap_C_' s)} \<inter> 299 {s. depth_' s = of_nat depth} ) [] 300 (lookupSourceSlot croot capptr depth) 301 (Call lookupSourceSlot_'proc)" 302 apply (cinit lift: capptr_' root___struct_cap_C_' depth_') 303 apply (rule ccorres_trim_returnE) 304 apply simp 305 apply simp 306 apply (ctac add: lookupSlotForCNodeOp_ccorres') 307 apply (clarsimp simp: to_bool_def true_def false_def) 308 done 309 310lemma lookupSourceSlot_ccorres: 311 "ccorres 312 (syscall_error_rel \<currency> (\<lambda>w w'. w'= Ptr w \<and> depth \<le> word_bits)) lookupSlot_xf 313 (\<lambda>s. invs' s \<and> s \<turnstile>' croot \<and> depth < 2 ^ word_bits) 314 (UNIV \<inter> {s. capptr_' s = capptr} \<inter> 315 {s. ccap_relation croot (root___struct_cap_C_' s)} \<inter> 316 {s. depth_' s = of_nat depth} ) [] 317 (lookupSourceSlot croot capptr depth) 318 (Call lookupSourceSlot_'proc)" 319 apply (rule ccorres_guard_imp2, rule lookupSourceSlot_ccorres') 320 apply fastforce 321 done 322 323lemma lookupTargetSlot_ccorres': 324 "ccorres 325 (syscall_error_rel \<currency> (\<lambda>w w'. w'= Ptr w \<and> depth \<le> word_bits)) lookupSlot_xf 326 (\<lambda>s. valid_pspace' s \<and> s \<turnstile>' croot \<and> depth < 2 ^ word_bits) 327 (UNIV \<inter> {s. capptr_' s = capptr} \<inter> 328 {s. ccap_relation croot (root___struct_cap_C_' s)} \<inter> 329 {s. depth_' s = of_nat depth} ) [] 330 (lookupTargetSlot croot capptr depth) 331 (Call lookupTargetSlot_'proc)" 332 apply (cinit lift: capptr_' root___struct_cap_C_' depth_') 333 apply (rule ccorres_trim_returnE) 334 apply simp 335 apply simp 336 apply (ctac add: lookupSlotForCNodeOp_ccorres') 337 apply (clarsimp simp: to_bool_def true_def false_def) 338 done 339 340lemma lookupTargetSlot_ccorres: 341 "ccorres 342 (syscall_error_rel \<currency> (\<lambda>w w'. w'= Ptr w \<and> depth \<le> word_bits)) lookupSlot_xf 343 (\<lambda>s. invs' s \<and> s \<turnstile>' croot \<and> depth < 2 ^ word_bits) 344 (UNIV \<inter> {s. capptr_' s = capptr} \<inter> 345 {s. ccap_relation croot (root___struct_cap_C_' s)} \<inter> 346 {s. depth_' s = of_nat depth} ) [] 347 (lookupTargetSlot croot capptr depth) 348 (Call lookupTargetSlot_'proc)" 349 apply (rule ccorres_guard_imp2, rule lookupTargetSlot_ccorres') 350 apply fastforce 351 done 352 353lemma lookupPivotSlot_ccorres: 354 "ccorres 355 (syscall_error_rel \<currency> (\<lambda>w w'. w'= Ptr w \<and> depth \<le> word_bits)) lookupSlot_xf 356 (\<lambda>s. invs' s \<and> s \<turnstile>' croot \<and> depth < 2 ^ word_bits) 357 (UNIV \<inter> {s. capptr_' s = capptr} \<inter> 358 {s. ccap_relation croot (root___struct_cap_C_' s)} \<inter> 359 {s. depth_' s = of_nat depth} ) [] 360 (lookupPivotSlot croot capptr depth) 361 (Call lookupPivotSlot_'proc)" 362 apply (cinit lift: capptr_' root___struct_cap_C_' depth_') 363 apply (rule ccorres_trim_returnE) 364 apply simp 365 apply simp 366 apply (ctac add: lookupSlotForCNodeOp_ccorres) 367 apply (clarsimp simp: to_bool_def true_def false_def) 368 done 369 370end 371end 372