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