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