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 12imports Bits_R 13begin 14 15(* Collect empty_fail lemmas here. naming convention is emtpy_fail_NAME. 16 Unless there is a good reason, they should all be [intro!, wp, simp] *) 17 18lemma empty_fail_projectKO [simp, intro!]: 19 "empty_fail (projectKO v)" 20 unfolding empty_fail_def projectKO_def 21 by (simp add: return_def fail_def split: option.splits) 22 23lemma empty_fail_alignCheck [intro!, wp, simp]: 24 "empty_fail (alignCheck a b)" 25 unfolding alignCheck_def 26 by (simp add: alignError_def) 27 28lemma empty_fail_magnitudeCheck [intro!, wp, simp]: 29 "empty_fail (magnitudeCheck a b c)" 30 unfolding magnitudeCheck_def 31 by (simp split: option.splits) 32 33lemma empty_fail_loadObject_default [intro!, wp, simp]: 34 shows "empty_fail (loadObject_default x b c d)" 35 by (auto simp: loadObject_default_def 36 split: option.splits) 37 38lemma empty_fail_threadGet [intro!, wp, simp]: 39 "empty_fail (threadGet f p)" 40 by (simp add: threadGet_def getObject_def split_def) 41 42lemma empty_fail_getCTE [intro!, wp, simp]: 43 "empty_fail (getCTE slot)" 44 apply (simp add: getCTE_def getObject_def split_def) 45 apply (intro empty_fail_bind, simp_all) 46 apply (simp add: loadObject_cte typeError_def alignCheck_def alignError_def 47 magnitudeCheck_def 48 split: Structures_H.kernel_object.split) 49 apply (auto split: option.split) 50 done 51 52lemma empty_fail_updateObject_cte [intro!, wp, simp]: 53 "empty_fail (updateObject (v :: cte) ko a b c)" 54 by (simp add: updateObject_cte typeError_def unless_def split: kernel_object.splits ) 55 56lemma empty_fail_setCTE [intro!, wp, simp]: 57 "empty_fail (setCTE p cte)" 58 unfolding setCTE_def 59 by (simp add: setObject_def split_def) 60 61lemma empty_fail_updateMDB [intro!, wp, simp]: 62 "empty_fail (updateMDB a b)" 63 unfolding updateMDB_def Let_def by auto 64 65lemma empty_fail_getSlotCap [intro!, wp, simp]: 66 "empty_fail (getSlotCap a)" 67 unfolding getSlotCap_def by simp 68 69context begin interpretation Arch . (*FIXME: arch_split*) 70 71lemma empty_fail_getObject: 72 assumes x: "(\<And>b c d. empty_fail (loadObject x b c d::'a :: pspace_storable kernel))" 73 shows "empty_fail (getObject x :: 'a :: pspace_storable kernel)" 74 apply (simp add: getObject_def split_def) 75 apply (safe intro!: empty_fail_bind empty_fail_gets empty_fail_assert_opt) 76 apply (rule x) 77 done 78 79lemma empty_fail_getObject_tcb [intro!, wp, simp]: 80 shows "empty_fail (getObject x :: tcb kernel)" 81 by (auto intro: empty_fail_getObject) 82 83lemma empty_fail_updateTrackedFreeIndex [intro!, wp, simp]: 84 shows "empty_fail (updateTrackedFreeIndex p idx)" 85 by (simp add: updateTrackedFreeIndex_def) 86 87lemma empty_fail_updateNewFreeIndex [intro!, wp, simp]: 88 shows "empty_fail (updateNewFreeIndex p)" 89 apply (simp add: updateNewFreeIndex_def) 90 apply (safe intro!: empty_fail_bind) 91 apply (simp split: capability.split) 92 done 93 94lemma empty_fail_insertNewCap [intro!, wp, simp]: 95 "empty_fail (insertNewCap p p' cap)" 96 unfolding insertNewCap_def by simp 97 98lemma empty_fail_getIRQSlot [intro!, wp, simp]: 99 "empty_fail (getIRQSlot irq)" 100 by (simp add: getIRQSlot_def getInterruptState_def locateSlot_conv) 101 102lemma empty_fail_getObject_ntfn [intro!, wp, simp]: 103 "empty_fail (getObject p :: Structures_H.notification kernel)" 104 by (simp add: empty_fail_getObject) 105 106lemma empty_fail_getNotification [intro!, wp, simp]: 107 "empty_fail (getNotification ep)" 108 by (simp add: getNotification_def) 109 110lemma empty_fail_lookupIPCBuffer [intro!, wp, simp]: 111 "empty_fail (lookupIPCBuffer a b)" 112 by (clarsimp simp: lookupIPCBuffer_def ARM_H.lookupIPCBuffer_def 113 Let_def getThreadBufferSlot_def locateSlot_conv 114 split: capability.splits arch_capability.splits | wp | wpc)+ 115 116lemma empty_fail_updateObject_default [intro!, wp, simp]: 117 "empty_fail (updateObject_default v ko a b c)" 118 by (simp add: updateObject_default_def typeError_def unless_def split: kernel_object.splits ) 119 120lemma empty_fail_threadSet [intro!, wp, simp]: 121 "empty_fail (threadSet f p)" 122 by (simp add: threadSet_def getObject_def setObject_def split_def) 123 124lemma empty_fail_getThreadState[iff]: 125 "empty_fail (getThreadState t)" 126 by (simp add: getThreadState_def) 127 128declare empty_fail_stateAssert [wp] 129declare setRegister_empty_fail [intro!, simp] 130 131lemma empty_fail_getSchedulerAction [intro!, wp, simp]: 132 "empty_fail getSchedulerAction" 133 by (simp add: getSchedulerAction_def getObject_def split_def) 134 135lemma empty_fail_scheduleSwitchThreadFastfail [intro!, wp, simp]: 136 "empty_fail (scheduleSwitchThreadFastfail a b c d)" 137 by (simp add: scheduleSwitchThreadFastfail_def split: if_splits) 138 139lemma empty_fail_curDomain [intro!, wp, simp]: 140 "empty_fail curDomain" 141 by (simp add: curDomain_def) 142 143end 144end 145