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
11(*
12    Defines the instances of pspace_storable objects.
13*)
14
15chapter "Storable Object Instances"
16
17theory ObjectInstances_H
18imports
19  Structures_H
20  "./$L4V_ARCH/State_H"
21  PSpaceStorable_H
22  Config_H
23begin
24
25context begin interpretation Arch .
26requalify_consts
27  VPtr
28  newContext
29end
30
31lemma projectKO_eq2:
32  "((obj,s') \<in> fst (projectKO ko s)) = (projectKO_opt ko = Some obj \<and> s' = s)"
33  by (auto simp: projectKO_def fail_def return_def split: option.splits)
34
35
36\<comment> \<open>-----------------------------------\<close>
37
38instantiation endpoint :: pre_storable
39begin
40
41definition
42  projectKO_opt_ep:
43  "projectKO_opt e \<equiv> case e of KOEndpoint e \<Rightarrow> Some e | _ \<Rightarrow> None"
44
45definition
46  injectKO_ep [simp]:
47  "injectKO e \<equiv> KOEndpoint e"
48
49definition
50  koType_ep [simp]:
51  "koType (t::endpoint itself) \<equiv> EndpointT"
52
53instance
54  by (intro_classes,
55      auto simp: projectKO_opt_ep split: kernel_object.splits)
56
57end
58
59instantiation notification :: pre_storable
60begin
61
62definition
63  projectKO_opt_ntfn:
64  "projectKO_opt e \<equiv> case e of KONotification e \<Rightarrow> Some e | _ \<Rightarrow> None"
65
66definition
67  injectKO_ntfn [simp]:
68  "injectKO e \<equiv> KONotification e"
69
70definition
71  koType_ntfn [simp]:
72  "koType (t::notification itself) \<equiv> NotificationT"
73
74instance
75  by (intro_classes,
76      auto simp: projectKO_opt_ntfn split: kernel_object.splits)
77
78end
79
80
81instantiation cte :: pre_storable
82begin
83
84definition
85  projectKO_opt_cte:
86  "projectKO_opt e \<equiv> case e of KOCTE e \<Rightarrow> Some e | _ \<Rightarrow> None"
87
88definition
89  injectKO_cte [simp]:
90  "injectKO c \<equiv> KOCTE c"
91
92definition
93  koType_cte [simp]:
94  "koType (t::cte itself) \<equiv> CTET"
95
96instance
97  by (intro_classes,
98      auto simp: projectKO_opt_cte split: kernel_object.splits)
99
100end
101
102instantiation user_data_device :: pre_storable
103begin
104
105definition
106  projectKO_opt_user_data_device:
107  "projectKO_opt e \<equiv> case e of KOUserDataDevice \<Rightarrow> Some UserDataDevice | _ \<Rightarrow> None"
108
109definition
110  injectKO_user_data_device [simp]:
111  "injectKO (t :: user_data_device) \<equiv> KOUserDataDevice"
112
113definition
114  koType_user_data_device [simp]:
115  "koType (t::user_data_device itself) \<equiv> UserDataDeviceT"
116
117instance
118  by (intro_classes,
119      auto simp: projectKO_opt_user_data_device split: kernel_object.splits)
120end
121
122instantiation user_data :: pre_storable
123begin
124
125definition
126  projectKO_opt_user_data:
127  "projectKO_opt e \<equiv> case e of KOUserData \<Rightarrow> Some UserData | _ \<Rightarrow> None"
128
129definition
130  injectKO_user_data [simp]:
131  "injectKO (t :: user_data) \<equiv> KOUserData"
132
133definition
134  koType_user_data [simp]:
135  "koType (t::user_data itself) \<equiv> UserDataT"
136
137instance
138  by (intro_classes,
139      auto simp: projectKO_opt_user_data split: kernel_object.splits)
140
141end
142
143
144instantiation tcb :: pre_storable
145begin
146
147definition
148  projectKO_opt_tcb:
149  "projectKO_opt e \<equiv> case e of KOTCB e \<Rightarrow> Some e | _ \<Rightarrow> None"
150
151definition
152  injectKO_tcb [simp]:
153  "injectKO t \<equiv> KOTCB t"
154
155definition
156  koType_tcb [simp]:
157  "koType (t::tcb itself) \<equiv> TCBT"
158
159instance
160  by (intro_classes,
161      auto simp: projectKO_opt_tcb split: kernel_object.splits)
162
163end
164
165
166lemmas projectKO_opts_defs =
167  projectKO_opt_tcb projectKO_opt_cte projectKO_opt_ntfn projectKO_opt_ep
168  projectKO_opt_user_data projectKO_opt_user_data_device
169
170lemmas injectKO_defs =
171  injectKO_tcb injectKO_cte injectKO_ntfn injectKO_ep injectKO_user_data injectKO_user_data_device
172
173lemmas koType_defs =
174  koType_tcb koType_cte koType_ntfn koType_ep koType_user_data koType_user_data_device
175
176\<comment> \<open>-----------------------------------\<close>
177
178instantiation endpoint :: pspace_storable
179begin
180
181#INCLUDE_HASKELL SEL4/Object/Instances.lhs instanceproofs bodies_only ONLY Endpoint
182
183instance
184  apply (intro_classes)
185  apply simp
186  apply (case_tac ko, auto simp: projectKO_opt_ep updateObject_default_def
187                                 in_monad projectKO_eq2
188                           split: kernel_object.splits)
189  done
190
191end
192
193
194instantiation notification :: pspace_storable
195begin
196
197#INCLUDE_HASKELL SEL4/Object/Instances.lhs instanceproofs bodies_only ONLY Notification
198
199instance
200  apply (intro_classes)
201  apply (case_tac ko, auto simp: projectKO_opt_ntfn updateObject_default_def
202                                 in_monad projectKO_eq2
203                           split: kernel_object.splits)
204  done
205
206end
207
208
209instantiation cte :: pspace_storable
210begin
211
212#INCLUDE_HASKELL SEL4/Object/Instances.lhs instanceproofs bodies_only ONLY CTE
213
214instance
215  apply (intro_classes)
216  apply (case_tac ko, auto simp: projectKO_opt_cte updateObject_cte
217                                 in_monad projectKO_eq2 typeError_def alignError_def
218                           split: kernel_object.splits if_split_asm)
219  done
220
221end
222
223
224instantiation user_data :: pspace_storable
225begin
226
227#INCLUDE_HASKELL SEL4/Object/Instances.lhs instanceproofs bodies_only ONLY UserData
228
229instance
230  apply (intro_classes)
231  apply (case_tac ko, auto simp: projectKO_opt_user_data updateObject_default_def
232                                 in_monad projectKO_eq2
233                           split: kernel_object.splits)
234  done
235
236end
237
238
239instantiation user_data_device :: pspace_storable
240begin
241
242#INCLUDE_HASKELL SEL4/Object/Instances.lhs instanceproofs bodies_only ONLY UserDataDevice
243
244instance
245  apply (intro_classes)
246  apply (case_tac ko, auto simp: projectKO_opt_user_data_device updateObject_default_def
247                                 in_monad projectKO_eq2
248                           split: kernel_object.splits)
249  done
250
251end
252
253
254instantiation tcb :: pspace_storable
255begin
256
257#INCLUDE_HASKELL SEL4/Object/Instances.lhs instanceproofs bodies_only ONLY TCB
258
259instance
260  apply (intro_classes)
261  apply (case_tac ko, auto simp: projectKO_opt_tcb updateObject_default_def
262                                 in_monad projectKO_eq2
263                           split: kernel_object.splits)
264  done
265
266end
267
268
269end
270