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 11(* things that should be moved into first refinement *) 12 13theory Move 14imports "Refine.Refine" 15begin 16 17(* FIXME move: need a theory on top of CSpec that arches can share *) 18(* word size corresponding to a C int (e.g. 32 bit signed on x64 and ARM *) 19type_synonym int_sword = "machine_word_len signed word" 20 21lemma finaliseCap_Reply: 22 "\<lbrace>Q (NullCap,NullCap) and K (isReplyCap cap)\<rbrace> finaliseCapTrue_standin cap fin \<lbrace>Q\<rbrace>" 23 apply (rule NonDetMonadVCG.hoare_gen_asm) 24 apply (clarsimp simp: finaliseCapTrue_standin_def isCap_simps) 25 apply wp 26 done 27 28lemma cteDeleteOne_Reply: 29 "\<lbrace>st_tcb_at' P t and cte_wp_at' (isReplyCap o cteCap) slot\<rbrace> cteDeleteOne slot \<lbrace>\<lambda>_. st_tcb_at' P t\<rbrace>" 30 apply (simp add: cteDeleteOne_def unless_def split_def) 31 apply (wp finaliseCap_Reply isFinalCapability_inv getCTE_wp') 32 apply (clarsimp simp: cte_wp_at_ctes_of) 33 done 34 35lemma cancelSignal_st_tcb': 36 "\<lbrace>\<lambda>s. t\<noteq>t' \<and> st_tcb_at' P t' s\<rbrace> cancelSignal t ntfn \<lbrace>\<lambda>_. st_tcb_at' P t'\<rbrace>" 37 apply (simp add: cancelSignal_def Let_def) 38 apply (rule hoare_pre) 39 apply (wp sts_pred_tcb_neq' getNotification_wp|wpc)+ 40 apply clarsimp 41 done 42 43lemma cancelIPC_st_tcb_at': 44 "\<lbrace>\<lambda>s. t\<noteq>t' \<and> st_tcb_at' P t' s\<rbrace> cancelIPC t \<lbrace>\<lambda>_. st_tcb_at' P t'\<rbrace>" 45 apply (simp add: cancelIPC_def Let_def getThreadReplySlot_def locateSlot_conv) 46 apply (wp sts_pred_tcb_neq' getEndpoint_wp cteDeleteOne_Reply getCTE_wp'|wpc)+ 47 apply (rule hoare_strengthen_post [where Q="\<lambda>_. st_tcb_at' P t'"]) 48 apply (wp threadSet_st_tcb_at2) 49 apply simp 50 apply (clarsimp simp: cte_wp_at_ctes_of capHasProperty_def) 51 apply (wp cancelSignal_st_tcb' sts_pred_tcb_neq' getEndpoint_wp gts_wp'|wpc)+ 52 apply clarsimp 53 done 54 55lemma suspend_st_tcb_at': 56 "\<lbrace>\<lambda>s. (t\<noteq>t' \<longrightarrow> st_tcb_at' P t' s) \<and> (t=t' \<longrightarrow> P Inactive)\<rbrace> 57 suspend t 58 \<lbrace>\<lambda>_. st_tcb_at' P t'\<rbrace>" 59 apply (simp add: suspend_def unless_def) 60 apply (cases "t=t'") 61 apply (simp|wp cancelIPC_st_tcb_at' sts_st_tcb')+ 62 done 63 64lemma to_bool_if: 65 "(if w \<noteq> 0 then 1 else 0) = (if to_bool w then 1 else 0)" 66 by (auto simp: to_bool_def) 67 68(* FIXME MOVE *) 69lemma typ_at'_no_0_objD: 70 "typ_at' P p s \<Longrightarrow> no_0_obj' s \<Longrightarrow> p \<noteq> 0" 71 by (cases "p = 0" ; clarsimp) 72 73(* FIXME ARMHYP MOVE *) 74lemma ko_at'_not_NULL: 75 "\<lbrakk> ko_at' ko p s ; no_0_obj' s\<rbrakk> 76 \<Longrightarrow> p \<noteq> 0" 77 by (fastforce simp: word_gt_0 typ_at'_no_0_objD) 78 79context begin interpretation Arch . (*FIXME: arch_split*) 80 81lemma vcpu_at_ko'_eq: 82 "(\<exists>vcpu :: vcpu. ko_at' vcpu p s) = vcpu_at' p s" 83 apply (rule iffI) 84 apply (clarsimp simp: typ_at'_def obj_at'_def ko_wp_at'_def projectKOs) 85 apply (clarsimp simp: typ_at'_def obj_at'_def ko_wp_at'_def projectKOs) 86 apply (case_tac ko, auto) 87 apply (rename_tac arch_kernel_object) 88 apply (case_tac arch_kernel_object, auto)[1] 89 done 90 91lemmas vcpu_at_ko' = vcpu_at_ko'_eq[THEN iffD2] 92 93lemma sym_refs_tcb_vcpu': 94 "\<lbrakk> ko_at' (tcb::tcb) t s; atcbVCPUPtr (tcbArch tcb) = Some v; sym_refs (state_hyp_refs_of' s) \<rbrakk> \<Longrightarrow> 95 \<exists>vcpu. ko_at' vcpu v s \<and> vcpuTCBPtr vcpu = Some t" 96 apply (drule (1) hyp_sym_refs_obj_atD') 97 apply (clarsimp simp: obj_at'_real_def ko_wp_at'_def) 98 apply (case_tac ko; simp add: tcb_vcpu_refs'_def projectKOs) 99 apply (rename_tac koa) 100 apply (case_tac koa; clarsimp simp: refs_of_a_def vcpu_tcb_refs'_def) 101 done 102 103 104(* FIXME MOVE *) 105lemma ko_at'_tcb_vcpu_not_NULL: 106 "\<lbrakk> ko_at' (tcb::tcb) t s ; valid_objs' s ; no_0_obj' s ; atcbVCPUPtr (tcbArch tcb) = Some p \<rbrakk> 107 \<Longrightarrow> 0 < p" 108 \<comment> \<open>when C pointer is NULL, need this to show atcbVCPUPtr is None\<close> 109 unfolding valid_pspace'_def 110 by (fastforce simp: valid_tcb'_def valid_arch_tcb'_def word_gt_0 typ_at'_no_0_objD 111 dest: valid_objs_valid_tcb') 112 113 114(* FIXME move *) 115lemma setVMRoot_valid_queues': 116 "\<lbrace> valid_queues' \<rbrace> setVMRoot a \<lbrace> \<lambda>_. valid_queues' \<rbrace>" 117 by (rule valid_queues_lift'; wp) 118 119lemma vcpuEnable_valid_pspace' [wp]: 120 "\<lbrace> valid_pspace' \<rbrace> vcpuEnable a \<lbrace>\<lambda>_. valid_pspace' \<rbrace>" 121 by (wpsimp simp: valid_pspace'_def valid_mdb'_def) 122 123lemma vcpuSave_valid_pspace' [wp]: 124 "\<lbrace> valid_pspace' \<rbrace> vcpuSave a \<lbrace>\<lambda>_. valid_pspace' \<rbrace>" 125 by (wpsimp simp: valid_pspace'_def valid_mdb'_def) 126 127lemma vcpuRestore_valid_pspace' [wp]: 128 "\<lbrace> valid_pspace' \<rbrace> vcpuRestore a \<lbrace>\<lambda>_. valid_pspace' \<rbrace>" 129 by (wpsimp simp: valid_pspace'_def valid_mdb'_def) 130 131lemma vcpuSwitch_valid_pspace' [wp]: 132 "\<lbrace> valid_pspace' \<rbrace> vcpuSwitch a \<lbrace>\<lambda>_. valid_pspace' \<rbrace>" 133 by (wpsimp simp: valid_pspace'_def valid_mdb'_def) 134 135lemma ko_at_vcpu_at'D: 136 "ko_at' (vcpu :: vcpu) vcpuptr s \<Longrightarrow> vcpu_at' vcpuptr s" 137 by (fastforce simp: typ_at_to_obj_at_arches elim: obj_at'_weakenE) 138 139 140(* FIXME: change the original to be predicated! *) 141crunch ko_at'2[wp]: doMachineOp "\<lambda>s. P (ko_at' p t s)" 142 (simp: crunch_simps) 143 144(* FIXME: change the original to be predicated! *) 145crunch pred_tcb_at'2[wp]: doMachineOp "\<lambda>s. P (pred_tcb_at' a b p s)" 146 (simp: crunch_simps) 147 148crunch valid_queues'[wp]: readVCPUReg "\<lambda>s. valid_queues s" 149 (ignore: getObject) 150 151crunch valid_objs'[wp]: readVCPUReg "\<lambda>s. valid_objs' s" 152 (ignore: getObject) 153 154crunch sch_act_wf'[wp]: readVCPUReg "\<lambda>s. P (sch_act_wf (ksSchedulerAction s) s)" 155 (ignore: getObject) 156 157crunch ko_at'[wp]: readVCPUReg "\<lambda>s. P (ko_at' a p s)" 158 (ignore: getObject) 159 160crunch obj_at'[wp]: readVCPUReg "\<lambda>s. P (obj_at' a p s)" 161 (ignore: getObject) 162 163crunch pred_tcb_at'[wp]: readVCPUReg "\<lambda>s. P (pred_tcb_at' a b p s)" 164 (ignore: getObject) 165 166crunch ksCurThread[wp]: readVCPUReg "\<lambda>s. P (ksCurThread s)" 167 (ignore: getObject) 168 169lemma fromEnum_maxBound_vcpureg_def: 170 "fromEnum (maxBound :: vcpureg) = 38" 171 by (clarsimp simp: fromEnum_def maxBound_def enum_vcpureg) 172 173lemma unat_of_nat_mword_fromEnum_vcpureg[simp]: 174 "unat ((of_nat (fromEnum e)) :: machine_word) = fromEnum (e :: vcpureg)" 175 apply (subst unat_of_nat_eq, clarsimp) 176 apply (rule order_le_less_trans[OF maxBound_is_bound]) 177 apply (clarsimp simp: fromEnum_maxBound_vcpureg_def)+ 178 done 179 180lemma unat_of_nat_mword_length_upto_vcpureg[simp]: 181 "unat ((of_nat (length [(start :: vcpureg) .e. end])) :: machine_word) = length [start .e. end]" 182 apply (subst unat_of_nat_eq ; clarsimp) 183 apply (rule order_le_less_trans[OF length_upto_enum_le_maxBound]) 184 apply (simp add: fromEnum_maxBound_vcpureg_def) 185 done 186 187 188(* when creating a new object, the entire slot including starting address should be free *) 189(* FIXME move *) 190lemma ps_clear_entire_slotI: 191 "({p..p + 2 ^ n - 1}) \<inter> dom (ksPSpace s) = {} \<Longrightarrow> ps_clear p n s" 192 by (fastforce simp: ps_clear_def) 193 194(* FIXME move *) 195lemma ps_clear_ksPSpace_upd_same[simp]: 196 "ps_clear p n (s\<lparr>ksPSpace := ksPSpace s(p \<mapsto> v)\<rparr>) = ps_clear p n s" 197 by (fastforce simp: ps_clear_def) 198 199(* FIXME move *) 200lemma getObject_vcpu_prop: 201 "\<lbrace>obj_at' P t\<rbrace> getObject t \<lbrace>\<lambda>(vcpu :: vcpu) s. P vcpu\<rbrace>" 202 apply (rule obj_at_getObject) 203 apply (clarsimp simp: loadObject_default_def in_monad projectKOs) 204 done 205 206(* FIXME move *) 207(* FIXME would be interesting to generalise these kinds of lemmas to other KOs *) 208lemma setObject_sets_object_vcpu: 209 "\<lbrace> vcpu_at' v \<rbrace> setObject v (vcpu::vcpu) \<lbrace> \<lambda>_. ko_at' vcpu v \<rbrace>" 210 supply fun_upd_apply[simp del] 211 apply (clarsimp simp: setObject_def updateObject_default_def bind_assoc) 212 apply (wpsimp wp: hoare_vcg_imp_lift' hoare_vcg_ex_lift simp: alignError_def) 213 apply (clarsimp simp: obj_at'_def) 214 apply (clarsimp simp: obj_at'_def projectKOs objBitsKO_def archObjSize_def dest!: vcpu_at_ko') 215 apply (fastforce simp: fun_upd_apply) 216 done 217 218(* FIXME move *) 219(* FIXME would be interesting to generalise these kinds of lemmas to other KOs *) 220lemma placeNewObject_creates_object_vcpu: 221 "\<lbrace> \<top> \<rbrace> placeNewObject v (vcpu::vcpu) 0 \<lbrace> \<lambda>_. ko_at' vcpu v \<rbrace>" 222 supply fun_upd_apply[simp del] haskell_assert_inv[wp del] 223 apply (clarsimp simp: placeNewObject_def placeNewObject'_def split_def alignError_def) 224 apply (wpsimp wp: assert_wp hoare_vcg_imp_lift' hoare_vcg_ex_lift) 225 apply (clarsimp simp: is_aligned_mask[symmetric] objBitsKO_def archObjSize_def) 226 apply (case_tac "is_aligned v vcpuBits"; clarsimp) 227 apply (rule conjI; clarsimp) 228 apply (subst (asm) lookupAround2_None1) 229 apply (clarsimp simp: obj_at'_def projectKOs objBitsKO_def archObjSize_def fun_upd_apply) 230 apply (fastforce intro: ps_clear_entire_slotI simp add: field_simps fun_upd_apply) 231 apply (subst (asm) lookupAround2_char1) 232 apply (clarsimp simp: obj_at'_def projectKOs objBitsKO_def archObjSize_def fun_upd_apply) 233 apply (fastforce intro: ps_clear_entire_slotI simp add: field_simps) 234 done 235 236end 237 238 239(* FIXME: move *) 240lemma cond_throw_whenE: 241 "(if P then f else throwError e) = (whenE (\<not> P) (throwError e) >>=E (\<lambda>_. f))" 242 by (auto split: if_splits 243 simp: throwError_def bindE_def 244 whenE_def bind_def returnOk_def return_def) 245 246lemma ksPSpace_update_eq_ExD: 247 "s = t\<lparr> ksPSpace := ksPSpace s\<rparr> 248 \<Longrightarrow> \<exists>ps. s = t \<lparr> ksPSpace := ps \<rparr>" 249 by (erule exI) 250 251lemma threadGet_wp'': 252 "\<lbrace>\<lambda>s. \<forall>v. obj_at' (\<lambda>tcb. f tcb = v) thread s \<longrightarrow> P v s\<rbrace> threadGet f thread \<lbrace>P\<rbrace>" 253 apply (rule hoare_pre) 254 apply (rule threadGet_wp) 255 apply (clarsimp simp: obj_at'_def) 256 done 257 258lemma tcbSchedEnqueue_queued_queues_inv: 259 "\<lbrace>\<lambda>s. obj_at' tcbQueued t s \<and> P (ksReadyQueues s) \<rbrace> tcbSchedEnqueue t \<lbrace>\<lambda>_ s. P (ksReadyQueues s)\<rbrace>" 260 unfolding tcbSchedEnqueue_def unless_def 261 apply (wpsimp simp: if_apply_def2 wp: threadGet_wp) 262 apply normalise_obj_at' 263 done 264 265lemma addToBitmap_sets_L1Bitmap_same_dom: 266 "\<lbrace>\<lambda>s. p \<le> maxPriority \<and> d' = d \<rbrace> addToBitmap d' p 267 \<lbrace>\<lambda>rv s. ksReadyQueuesL1Bitmap s d \<noteq> 0 \<rbrace>" 268 unfolding addToBitmap_def bitmap_fun_defs 269 apply wpsimp 270 apply (clarsimp simp: maxPriority_def numPriorities_def word_or_zero le_def 271 prioToL1Index_max[simplified wordRadix_def, simplified]) 272 done 273 274crunch ksReadyQueuesL1Bitmap[wp]: setQueue "\<lambda>s. P (ksReadyQueuesL1Bitmap s)" 275 276lemma tcb_in_cur_domain'_def': 277 "tcb_in_cur_domain' t = (\<lambda>s. obj_at' (\<lambda>tcb. tcbDomain tcb = ksCurDomain s) t s)" 278 unfolding tcb_in_cur_domain'_def 279 by (auto simp: obj_at'_def) 280 281lemma sts_running_ksReadyQueuesL1Bitmap[wp]: 282 "\<lbrace>\<lambda>s. P (ksReadyQueuesL1Bitmap s)\<rbrace> 283 setThreadState Structures_H.thread_state.Running t 284 \<lbrace>\<lambda>_ s. P (ksReadyQueuesL1Bitmap s)\<rbrace>" 285 unfolding setThreadState_def 286 apply wp 287 apply (rule hoare_pre_cont) 288 apply (wpsimp simp: if_apply_def2 289 wp: hoare_drop_imps hoare_vcg_disj_lift threadSet_tcbState_st_tcb_at')+ 290 done 291 292lemma sts_running_ksReadyQueuesL2Bitmap[wp]: 293 "\<lbrace>\<lambda>s. P (ksReadyQueuesL2Bitmap s)\<rbrace> 294 setThreadState Structures_H.thread_state.Running t 295 \<lbrace>\<lambda>_ s. P (ksReadyQueuesL2Bitmap s)\<rbrace>" 296 unfolding setThreadState_def 297 apply wp 298 apply (rule hoare_pre_cont) 299 apply (wpsimp simp: if_apply_def2 300 wp: hoare_drop_imps hoare_vcg_disj_lift threadSet_tcbState_st_tcb_at')+ 301 done 302 303lemma asUser_obj_at_not_queued[wp]: 304 "\<lbrace>obj_at' (\<lambda>tcb. \<not> tcbQueued tcb) p\<rbrace> asUser t m \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. \<not> tcbQueued tcb) p\<rbrace>" 305 apply (simp add: asUser_def split_def) 306 apply (wp hoare_drop_imps | simp)+ 307 done 308 309lemma ko_at'_obj_at'_field: 310 "ko_at' ko (t s) s \<Longrightarrow> obj_at' (\<lambda>ko'. f ko' = f ko) (t s) s" 311 by (erule obj_at'_weakenE, simp) 312 313end 314