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 ArchEmptyFail_AI
12imports "../EmptyFail_AI"
13begin
14
15context Arch begin global_naming ARM
16
17named_theorems EmptyFail_AI_assms
18
19crunch_ignore (empty_fail)
20  (add: invalidateLocalTLB_ASID_impl invalidateLocalTLB_VAASID_impl cleanByVA_impl
21        cleanByVA_PoU_impl invalidateByVA_impl invalidateByVA_I_impl
22        invalidate_I_PoU_impl cleanInvalByVA_impl branchFlush_impl
23        clean_D_PoU_impl cleanInvalidate_D_PoC_impl cleanInvalidateL2Range_impl
24        invalidateL2Range_impl cleanL2Range_impl flushBTAC_impl
25        writeContextID_impl isb_impl dsb_impl dmb_impl setHardwareASID_impl
26        writeTTBR0_impl cacheRangeOp setIRQTrigger_impl)
27
28crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]:
29  loadWord, load_word_offs, storeWord, getRestartPC, get_mrs
30
31end
32
33global_interpretation EmptyFail_AI_load_word?: EmptyFail_AI_load_word
34  proof goal_cases
35  interpret Arch .
36  case 1 show ?case by (unfold_locales; (fact EmptyFail_AI_assms)?)
37  qed
38
39context Arch begin global_naming ARM
40
41crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]: handle_fault
42  (simp: kernel_object.splits option.splits arch_cap.splits cap.splits endpoint.splits
43         bool.splits list.splits thread_state.splits split_def catch_def sum.splits
44         Let_def wp: zipWithM_x_empty_fail)
45
46crunch (empty_fail) empty_fail[wp]:
47  decode_tcb_configure, decode_bind_notification, decode_unbind_notification,
48  decode_set_priority, decode_set_mcpriority, decode_set_sched_params,
49  decode_set_tls_base
50  (simp: cap.splits arch_cap.splits split_def)
51
52lemma decode_tcb_invocation_empty_fail[wp]:
53  "empty_fail (decode_tcb_invocation a b (ThreadCap p) d e)"
54  by (simp add: decode_tcb_invocation_def split: invocation_label.splits | wp | intro conjI impI)+
55
56crunch (empty_fail) empty_fail[wp]: find_pd_for_asid, get_master_pde, check_vp_alignment,
57                   create_mapping_entries, ensure_safe_mapping, get_asid_pool, resolve_vaddr
58  (simp: kernel_object.splits arch_kernel_obj.splits option.splits pde.splits pte.splits)
59
60lemma arch_decode_ARMASIDControlMakePool_empty_fail:
61  "invocation_type label = ArchInvocationLabel ARMASIDControlMakePool
62    \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)"
63  apply (simp add: arch_decode_invocation_def Let_def)
64  apply (intro impI conjI allI)
65   apply (simp add: isPageFlushLabel_def isPDFlushLabel_def split: arch_cap.splits)+
66   apply (rule impI)
67   apply (simp add: split_def)
68   apply wp
69    apply simp
70   apply (subst bindE_assoc[symmetric])
71   apply (rule empty_fail_bindE)
72    subgoal by (fastforce simp: empty_fail_def whenE_def throwError_def select_ext_def bindE_def bind_def return_def returnOk_def lift_def liftE_def fail_def gets_def get_def assert_def select_def split: if_split_asm)
73   by (simp add: Let_def split: cap.splits arch_cap.splits option.splits bool.splits | wp | intro conjI impI allI)+
74
75lemma arch_decode_ARMASIDPoolAssign_empty_fail:
76  "invocation_type label = ArchInvocationLabel ARMASIDPoolAssign
77    \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)"
78  apply (simp add: arch_decode_invocation_def split_def Let_def isPageFlushLabel_def isPDFlushLabel_def
79            split: arch_cap.splits cap.splits option.splits | intro impI allI)+
80  apply (rule empty_fail_bindE)
81   apply simp
82  apply (rule empty_fail_bindE)
83   apply ((simp | wp)+)[1]
84  apply (rule empty_fail_bindE)
85   apply ((simp | wp)+)[1]
86  apply (rule empty_fail_bindE)
87   apply ((simp | wp)+)[1]
88  apply (subst bindE_assoc[symmetric])
89  apply (rule empty_fail_bindE)
90   subgoal by (fastforce simp: empty_fail_def whenE_def throwError_def select_def bindE_def
91                               bind_def return_def returnOk_def lift_def liftE_def select_ext_def
92                               gets_def get_def assert_def fail_def)
93  apply wp
94  done
95
96lemma arch_decode_invocation_empty_fail[wp]:
97  "empty_fail (arch_decode_invocation label b c d e f)"
98  apply (case_tac "invocation_type label")
99  apply (find_goal \<open>match premises in "_ = ArchInvocationLabel _" \<Rightarrow> \<open>-\<close>\<close>)
100  apply (rename_tac alabel)
101  apply (case_tac alabel; simp)
102  apply (find_goal \<open>succeeds \<open>erule arch_decode_ARMASIDControlMakePool_empty_fail\<close>\<close>)
103  apply (find_goal \<open>succeeds \<open>erule arch_decode_ARMASIDPoolAssign_empty_fail\<close>\<close>)
104  apply ((simp add: arch_decode_ARMASIDControlMakePool_empty_fail arch_decode_ARMASIDPoolAssign_empty_fail)+)[2]
105  including no_pre
106  by ((simp add: arch_decode_invocation_def Let_def split: arch_cap.splits cap.splits option.splits | (wp+) | intro conjI impI allI)+)
107
108end
109
110global_interpretation EmptyFail_AI_derive_cap?: EmptyFail_AI_derive_cap
111  proof goal_cases
112  interpret Arch .
113  case 1 show ?case by (unfold_locales; (fact EmptyFail_AI_assms)?)
114  qed
115
116context Arch begin global_naming ARM
117
118crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]: maskInterrupt, empty_slot,
119    setHardwareASID, set_current_pd, finalise_cap, preemption_point,
120    cap_swap_for_delete, decode_invocation
121  (simp: Let_def catch_def split_def OR_choiceE_def mk_ef_def option.splits endpoint.splits
122         notification.splits thread_state.splits sum.splits cap.splits arch_cap.splits
123         kernel_object.splits vmpage_size.splits pde.splits bool.splits list.splits)
124
125crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]: setRegister, setNextPC
126
127end
128
129global_interpretation EmptyFail_AI_rec_del?: EmptyFail_AI_rec_del
130  proof goal_cases
131  interpret Arch .
132  case 1 show ?case by (unfold_locales; (fact EmptyFail_AI_assms)?)
133  qed
134
135context Arch begin global_naming ARM
136crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]:
137  cap_delete, choose_thread
138end
139
140global_interpretation EmptyFail_AI_schedule_unit?: EmptyFail_AI_schedule_unit
141  proof goal_cases
142  interpret Arch .
143  case 1 show ?case by (unfold_locales; (fact EmptyFail_AI_assms)?)
144  qed
145
146global_interpretation EmptyFail_AI_schedule_det?: EmptyFail_AI_schedule_det
147  proof goal_cases
148  interpret Arch .
149  case 1 show ?case by (unfold_locales; (fact EmptyFail_AI_assms)?)
150  qed
151
152global_interpretation EmptyFail_AI_schedule?: EmptyFail_AI_schedule
153  proof goal_cases
154  interpret Arch .
155  case 1 show ?case by (unfold_locales; (fact EmptyFail_AI_assms)?)
156  qed
157
158context Arch begin global_naming ARM
159crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]: handle_event, activate_thread
160  (simp: cap.splits arch_cap.splits split_def invocation_label.splits Let_def
161         kernel_object.splits arch_kernel_obj.splits option.splits pde.splits pte.splits
162         bool.splits apiobject_type.splits aobject_type.splits notification.splits
163         thread_state.splits endpoint.splits catch_def sum.splits cnode_invocation.splits
164         page_table_invocation.splits page_invocation.splits asid_control_invocation.splits
165         asid_pool_invocation.splits arch_invocation.splits irq_state.splits syscall.splits
166         flush_type.splits page_directory_invocation.splits
167   ignore: resetTimer_impl ackInterrupt_impl)
168end
169
170global_interpretation EmptyFail_AI_call_kernel_unit?: EmptyFail_AI_call_kernel_unit
171  proof goal_cases
172  interpret Arch .
173  case 1 show ?case by (unfold_locales; (fact EmptyFail_AI_assms)?)
174  qed
175
176global_interpretation EmptyFail_AI_call_kernel_det?: EmptyFail_AI_call_kernel_det
177  proof goal_cases
178  interpret Arch .
179  case 1 show ?case by (unfold_locales; (fact EmptyFail_AI_assms)?)
180  qed
181
182global_interpretation EmptyFail_AI_call_kernel?: EmptyFail_AI_call_kernel
183  proof goal_cases
184  interpret Arch .
185  case 1 show ?case by (unfold_locales; (fact EmptyFail_AI_assms)?)
186  qed
187
188end
189