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 EmptyFail_H 12imports Refine 13begin 14 15crunch_ignore (empty_fail) 16 (add: handleE' getCTE getObject updateObject 17 CSpaceDecls_H.resolveAddressBits 18 doMachineOp suspend restart schedule) 19 20context begin interpretation Arch . (*FIXME: arch_split*) 21 22lemmas forM_empty_fail[intro!, wp, simp] = empty_fail_mapM[simplified forM_def[symmetric]] 23lemmas forM_x_empty_fail[intro!, wp, simp] = empty_fail_mapM_x[simplified forM_x_def[symmetric]] 24lemmas forME_x_empty_fail[intro!, wp, simp] = mapME_x_empty_fail[simplified forME_x_def[symmetric]] 25 26lemma withoutPreemption_empty_fail[intro!, wp, simp]: 27 "empty_fail m \<Longrightarrow> empty_fail (withoutPreemption m)" 28 by (simp add: withoutPreemption_def) 29 30lemma withoutFailure_empty_fail[intro!, wp, simp]: 31 "empty_fail m \<Longrightarrow> empty_fail (withoutFailure m)" 32 by (simp add: withoutFailure_def) 33 34lemma catchFailure_empty_fail[intro!, wp, simp]: 35 "\<lbrakk> empty_fail f; \<And>x. empty_fail (g x) \<rbrakk> \<Longrightarrow> empty_fail (catchFailure f g)" 36 by (simp add: catchFailure_def empty_fail_catch) 37 38lemma emptyOnFailure_empty_fail[intro!, wp, simp]: 39 "empty_fail m \<Longrightarrow> empty_fail (emptyOnFailure m)" 40 by (simp add: emptyOnFailure_def empty_fail_catch) 41 42lemma rethrowFailure_empty_fail [intro!, wp, simp]: 43 "empty_fail m \<Longrightarrow> empty_fail (rethrowFailure f m)" 44 apply (simp add:rethrowFailure_def o_def) 45 apply (wp | simp)+ 46 done 47 48lemma unifyFailure_empty_fail [intro!, wp, simp]: 49 "empty_fail f \<Longrightarrow> empty_fail (unifyFailure f)" 50 by (simp add: unifyFailure_def) 51 52lemma lookupErrorOnFailure_empty_fail [intro!, wp, simp]: 53 "empty_fail f \<Longrightarrow> empty_fail (lookupErrorOnFailure isSource f)" 54 by (simp add: lookupErrorOnFailure_def) 55 56lemma setObject_empty_fail [intro!, wp, simp]: 57 assumes x: "(\<And>a b c. empty_fail (updateObject v a x b c))" 58 shows "empty_fail (setObject x v)" 59 apply (simp add: setObject_def split_def) 60 apply (wp x | simp)+ 61 done 62 63lemma asUser_empty_fail [intro!, wp, simp]: 64 "empty_fail f \<Longrightarrow> empty_fail (asUser t f)" 65 apply (simp add:asUser_def) 66 apply (wp | wpc | simp | simp add: empty_fail_def)+ 67 done 68 69lemma capFaultOnFailure_empty_fail [intro!, wp, simp]: 70 "empty_fail m \<Longrightarrow> empty_fail (capFaultOnFailure cptr rp m)" 71 apply (simp add: capFaultOnFailure_def) 72 done 73 74crunch (empty_fail) empty_fail[intro!, wp, simp]: locateSlotCap 75 76lemma resolveAddressBits_spec_empty_fail: 77 notes spec_empty_fail_bindE'[wp_split] 78 shows 79 "spec_empty_fail (CSpace_H.resolveAddressBits a b c) s" 80proof (induct arbitrary: s rule: resolveAddressBits.induct) 81 case (1 a b c s) 82 show ?case 83 apply (simp add: resolveAddressBits.simps) 84 apply (wp | simp | wpc | intro impI conjI | rule drop_spec_empty_fail)+ 85 apply (rule use_spec_empty_fail) 86 apply (rule 1 | simp add: in_monad | rule drop_spec_empty_fail | force)+ 87 done 88 qed 89 90lemmas resolveAddressBits_empty_fail[intro!, wp, simp] = 91 resolveAddressBits_spec_empty_fail[THEN use_spec_empty_fail] 92 93crunch (empty_fail) empty_fail[intro!, wp, simp]: lookupIPCBuffer 94(simp:Let_def) 95 96declare ef_dmo'[intro!, wp, simp] 97 98lemma empty_fail_getObject_ep [intro!, wp, simp]: 99 "empty_fail (getObject p :: endpoint kernel)" 100 by (simp add: empty_fail_getObject) 101 102lemma getEndpoint_empty_fail [intro!, wp, simp]: 103 "empty_fail (getEndpoint ep)" 104 by (simp add: getEndpoint_def) 105 106lemma constOnFailure_empty_fail[intro!, wp, simp]: 107 "empty_fail m \<Longrightarrow> empty_fail (constOnFailure x m)" 108 by (simp add: constOnFailure_def const_def empty_fail_catch) 109 110lemma ArchRetypeDecls_H_deriveCap_empty_fail[intro!, wp, simp]: 111 "isPageTableCap y \<or> isPageDirectoryCap y \<or> isPageCap y 112 \<or> isASIDControlCap y \<or> isASIDPoolCap y 113 \<Longrightarrow> empty_fail (Arch.deriveCap x y)" 114 apply (simp add: ARM_H.deriveCap_def) 115 by auto 116 117crunch (empty_fail) empty_fail[intro!, wp, simp]: ensureNoChildren 118 119lemma deriveCap_empty_fail[intro!, wp, simp]: 120 "empty_fail (RetypeDecls_H.deriveCap slot y)" 121 apply (simp add: Retype_H.deriveCap_def) 122 apply (clarsimp simp: empty_fail_bindE) 123 apply (case_tac "capCap y") 124 apply (simp_all add: isPageTableCap_def isPageDirectoryCap_def 125 isPageCap_def isASIDPoolCap_def isASIDControlCap_def) 126 done 127 128crunch (empty_fail) empty_fail[intro!, wp, simp]: setExtraBadge, cteInsert 129 130lemma transferCapsToSlots_empty_fail[intro!, wp, simp]: 131 "empty_fail (transferCapsToSlots ep buffer n caps slots mi)" 132 apply (induct caps arbitrary: slots n mi) 133 apply simp 134 apply (simp add: Let_def split_def 135 split del: if_split) 136 apply (simp | wp | wpc | safe)+ 137 done 138 139crunch (empty_fail) empty_fail[intro!, wp, simp]: lookupTargetSlot, ensureEmptySlot, lookupSourceSlot, lookupPivotSlot 140 141lemma decodeCNodeInvocation_empty_fail[intro!, wp, simp]: 142 "empty_fail (decodeCNodeInvocation label args cap exs)" 143 apply (rule_tac label=label and args=args and exs=exs in decode_cnode_cases2) 144 apply (simp_all add: decodeCNodeInvocation_def 145 split_def cnode_invok_case_cleanup unlessE_whenE 146 cong: if_cong bool.case_cong list.case_cong) 147 apply (simp | wp | wpc | safe)+ 148 done 149 150lemma empty_fail_getObject_ap [intro!, wp, simp]: 151 "empty_fail (getObject p :: asidpool kernel)" 152 by (simp add: empty_fail_getObject) 153 154lemma empty_fail_getObject_pde [intro!, wp, simp]: 155 "empty_fail (getObject p :: pde kernel)" 156 by (simp add: empty_fail_getObject) 157 158lemma empty_fail_getObject_pte [intro!, wp, simp]: 159 "empty_fail (getObject p :: pte kernel)" 160 by (simp add: empty_fail_getObject) 161 162crunch (empty_fail) empty_fail[intro!, wp, simp]: decodeARMMMUInvocation 163(simp: Let_def ARMMMU_improve_cases) 164 165lemma ignoreFailure_empty_fail[intro!, wp, simp]: 166 "empty_fail x \<Longrightarrow> empty_fail (ignoreFailure x)" 167 by (simp add: ignoreFailure_def empty_fail_catch) 168 169crunch (empty_fail) empty_fail[intro!, wp, simp]: cancelIPC, setThreadState, tcbSchedDequeue, setupReplyMaster, isBlocked, possibleSwitchTo, tcbSchedAppend 170(simp: Let_def) 171 172crunch (empty_fail) "_H_empty_fail": "ThreadDecls_H.suspend" 173lemma ThreadDecls_H_suspend_empty_fail[intro!, wp, simp]: 174 "empty_fail (ThreadDecls_H.suspend target)" 175 by (simp add:suspend_def) 176 177lemma ThreadDecls_H_restart_empty_fail[intro!, wp, simp]: 178 "empty_fail (ThreadDecls_H.restart target)" 179 by (simp add:restart_def) 180 181crunch (empty_fail) empty_fail[intro!, wp, simp]: finaliseCap, preemptionPoint, capSwapForDelete 182 (wp: empty_fail_catch simp: Let_def) 183 184lemmas finalise_spec_empty_fail_induct = finaliseSlot'.induct[where P= 185 "\<lambda>sl exp s. spec_empty_fail (finaliseSlot' sl exp) s"] 186 187lemma spec_empty_fail_If: 188 "\<lbrakk> P \<Longrightarrow> spec_empty_fail f s; \<not> P \<Longrightarrow> spec_empty_fail g s \<rbrakk> 189 \<Longrightarrow> spec_empty_fail (if P then f else g) s" 190 by (simp split: if_split) 191 192lemma spec_empty_whenE': 193 "\<lbrakk> P \<Longrightarrow> spec_empty_fail f s \<rbrakk> \<Longrightarrow> spec_empty_fail (whenE P f) s" 194 by (simp add: whenE_def spec_empty_returnOk) 195 196lemma finaliseSlot_spec_empty_fail: 197 notes spec_empty_fail_bindE'[rotated, wp_split] 198 shows "spec_empty_fail (finaliseSlot x b) s" 199unfolding finaliseSlot_def 200proof (induct rule: finalise_spec_empty_fail_induct) 201 case (1 x b s) 202 show ?case 203 apply (subst finaliseSlot'_simps_ext) 204 apply (simp only: split_def Let_def K_bind_def fun_app_def) 205 apply (wp spec_empty_whenE' spec_empty_fail_If | wpc 206 | rule 1[unfolded Let_def K_bind_def split_def fun_app_def, 207 simplified], (simp | intro conjI)+ 208 | rule drop_spec_empty_fail | simp)+ 209 done 210qed 211 212lemmas finaliseSlot_empty_fail[intro!, wp, simp] = 213 finaliseSlot_spec_empty_fail[THEN use_spec_empty_fail] 214 215lemma checkCapAt_empty_fail[intro!, wp, simp]: 216 "empty_fail action \<Longrightarrow> empty_fail (checkCapAt cap ptr action)" 217 by (simp add: checkCapAt_def) 218 219lemma assertDerived_empty_fail[intro!, wp, simp]: 220 "empty_fail f \<Longrightarrow> empty_fail (assertDerived src cap f)" 221 by (simp add: assertDerived_def) 222 223crunch (empty_fail) empty_fail[intro!, wp, simp]: cteDelete 224 225lemma liftE_empty_fail[intro!, wp, simp]: 226 "empty_fail f \<Longrightarrow> empty_fail (liftE f)" 227 by simp 228 229lemma spec_empty_fail_unlessE': 230 "\<lbrakk> \<not> P \<Longrightarrow> spec_empty_fail f s \<rbrakk> \<Longrightarrow> spec_empty_fail (unlessE P f) s" 231 by (simp add:unlessE_def spec_empty_returnOk) 232 233lemma cteRevoke_spec_empty_fail: 234 notes spec_empty_fail_bindE'[wp_split] 235 shows "spec_empty_fail (cteRevoke p) s" 236proof (induct rule: cteRevoke.induct) 237 case (1 p s) 238 show ?case 239 apply (simp add: cteRevoke.simps) 240 apply (wp spec_empty_whenE' spec_empty_fail_unlessE' | rule drop_spec_empty_fail, wp)+ 241 apply (rule 1, auto simp add: in_monad) 242 done 243qed 244 245lemmas cteRevoke_empty_fail[intro!, wp, simp] = 246 cteRevoke_spec_empty_fail[THEN use_spec_empty_fail] 247 248lemma Syscall_H_syscall_empty_fail[intro!, wp, simp]: 249 "\<lbrakk>empty_fail a; \<And>x. empty_fail (b x); \<And>x. empty_fail (c x); 250 \<And>x. empty_fail (d x); \<And>x. empty_fail (e x)\<rbrakk> 251 \<Longrightarrow> empty_fail (syscall a b c d e)" 252 apply (simp add:syscall_def) 253 apply (wp | wpc | simp)+ 254 done 255 256lemma catchError_empty_fail[intro!, wp, simp]: 257 "\<lbrakk> empty_fail f; \<And>x. empty_fail (g x) \<rbrakk> \<Longrightarrow> empty_fail (catchError f g)" 258 by (simp add: catchError_def handle_empty_fail) 259 260lemma findM_empty_fail [intro!, wp, simp]: 261 assumes m: "\<And>x. empty_fail (f x)" 262 shows "empty_fail (findM f xs)" 263proof (induct xs) 264 case Nil 265 thus ?case by (simp add: findM_def) 266next 267 case Cons 268 from Cons 269 show ?case by (simp add: m) 270qed 271 272crunch (empty_fail) empty_fail[intro!, wp, simp]: 273 chooseThread, getDomainTime, nextDomain, isHighestPrio 274 (wp: empty_fail_catch) 275 276lemma ThreadDecls_H_schedule_empty_fail[intro!, wp, simp]: 277 "empty_fail schedule" 278 apply (simp add: schedule_def) 279 apply (clarsimp simp: scheduleChooseNewThread_def split: if_split | wp | wpc)+ 280 done 281 282crunch (empty_fail) empty_fail: callKernel 283 (wp: empty_fail_catch) 284 285lemma call_kernel_serial: 286 "\<lbrakk> (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and 287 (\<lambda>s. scheduler_action s = resume_cur_thread)) s; 288 \<exists>s'. (s, s') \<in> state_relation \<and> 289 (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and 290 (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and 291 (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s' \<rbrakk> 292 \<Longrightarrow> fst (call_kernel event s) \<noteq> {}" 293 apply (cut_tac m = "call_kernel event" in corres_underlying_serial) 294 apply (rule kernel_corres) 295 apply (rule callKernel_empty_fail) 296 apply auto 297 done 298 299end 300 301end 302