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 Arch Object Instances"
16
17theory ArchObjInsts_H
18imports
19  ArchTypes_H
20  "../PSpaceStorable_H"
21  "../ObjectInstances_H"
22begin
23qualify X64_H (in Arch)
24
25instantiation X64_H.pde :: pre_storable
26begin
27interpretation Arch .
28
29definition
30  projectKO_opt_pde:
31  "projectKO_opt e \<equiv> case e of KOArch (KOPDE e) \<Rightarrow> Some e | _ \<Rightarrow> None"
32
33definition
34  injectKO_pde [simp]:
35  "injectKO e \<equiv> KOArch (KOPDE e)"
36
37definition
38  koType_pde [simp]:
39  "koType (t::pde itself) \<equiv> ArchT PDET"
40
41instance
42  by (intro_classes,
43      auto simp: projectKO_opt_pde split: kernel_object.splits arch_kernel_object.splits)
44
45end
46
47
48instantiation X64_H.pte :: pre_storable
49begin
50interpretation Arch .
51
52definition
53  projectKO_opt_pte:
54  "projectKO_opt e \<equiv> case e of (KOArch (KOPTE e)) \<Rightarrow> Some e | _ \<Rightarrow> None"
55
56definition
57  injectKO_pte [simp]:
58  "injectKO e \<equiv> KOArch (KOPTE e)"
59
60definition
61  koType_pte [simp]:
62  "koType (t::pte itself) \<equiv> ArchT PTET"
63
64instance
65  by (intro_classes,
66      auto simp: projectKO_opt_pte split: kernel_object.splits arch_kernel_object.splits)
67
68end
69
70instantiation X64_H.pdpte :: pre_storable
71begin
72interpretation Arch .
73
74definition
75  projectKO_opt_pdpte:
76  "projectKO_opt e \<equiv> case e of (KOArch (KOPDPTE e)) \<Rightarrow> Some e | _ \<Rightarrow> None"
77
78definition
79  injectKO_pdpte [simp]:
80  "injectKO e \<equiv> KOArch (KOPDPTE e)"
81
82definition
83  koType_pdpte [simp]:
84  "koType (t::pdpte itself) \<equiv> ArchT PDPTET"
85
86instance
87  by (intro_classes,
88      auto simp: projectKO_opt_pdpte split: kernel_object.splits arch_kernel_object.splits)
89
90end
91
92instantiation X64_H.pml4e :: pre_storable
93begin
94interpretation Arch .
95
96definition
97  projectKO_opt_pml4e:
98  "projectKO_opt e \<equiv> case e of (KOArch (KOPML4E e)) \<Rightarrow> Some e | _ \<Rightarrow> None"
99
100definition
101  injectKO_pml4e [simp]:
102  "injectKO e \<equiv> KOArch (KOPML4E e)"
103
104definition
105  koType_pml4e [simp]:
106  "koType (t::pml4e itself) \<equiv> ArchT PML4ET"
107
108instance
109  by (intro_classes,
110      auto simp: projectKO_opt_pml4e split: kernel_object.splits arch_kernel_object.splits)
111
112end
113
114instantiation X64_H.asidpool :: pre_storable
115begin
116interpretation Arch .
117
118definition
119  injectKO_asidpool [simp]:
120  "injectKO e \<equiv> KOArch (KOASIDPool e)"
121
122definition
123  koType_asidpool [simp]:
124  "koType (t::asidpool itself) \<equiv> ArchT ASIDPoolT"
125
126definition
127  projectKO_opt_asidpool:
128  "projectKO_opt e \<equiv> case e of (KOArch (KOASIDPool e)) \<Rightarrow> Some e | _ \<Rightarrow> None"
129
130instance
131  by (intro_classes,
132      auto simp: projectKO_opt_asidpool split: kernel_object.splits arch_kernel_object.splits)
133
134end
135
136lemmas (in Arch) projectKO_opts_defs =
137  projectKO_opt_pte projectKO_opt_pde
138  projectKO_opt_pdpte projectKO_opt_pml4e
139  projectKO_opt_asidpool
140  ObjectInstances_H.projectKO_opts_defs
141
142lemmas (in Arch) [simp] =
143  injectKO_pte koType_pte
144  injectKO_pde koType_pde
145  injectKO_pdpte koType_pdpte
146  injectKO_pml4e koType_pml4e
147  injectKO_asidpool koType_asidpool
148
149
150\<comment> \<open>--------------------------------------\<close>
151
152#INCLUDE_SETTINGS keep_constructor = asidpool
153
154#INCLUDE_HASKELL_PREPARSE SEL4/Object/Structures/X64.lhs
155#INCLUDE_HASKELL_PREPARSE SEL4/Machine/Hardware/X64.lhs
156
157
158instantiation X64_H.pde :: pspace_storable
159begin
160interpretation Arch .
161
162#INCLUDE_HASKELL SEL4/Object/Instances/X64.lhs instanceproofs bodies_only ONLY PDE
163
164instance
165  apply (intro_classes)
166  apply (clarsimp simp add: updateObject_default_def in_monad projectKO_opts_defs
167                            projectKO_eq2
168                     split: kernel_object.splits arch_kernel_object.splits)
169  done
170
171end
172
173instantiation X64_H.pte :: pspace_storable
174begin
175interpretation Arch .
176
177#INCLUDE_HASKELL SEL4/Object/Instances/X64.lhs instanceproofs bodies_only ONLY PTE
178
179instance
180  apply (intro_classes)
181  apply (clarsimp simp add: updateObject_default_def in_monad projectKO_opts_defs
182                            projectKO_eq2
183                     split: kernel_object.splits arch_kernel_object.splits)
184  done
185
186end
187
188
189instantiation X64_H.pdpte :: pspace_storable
190begin
191interpretation Arch .
192
193#INCLUDE_HASKELL SEL4/Object/Instances/X64.lhs instanceproofs bodies_only ONLY PDPTE
194
195instance
196  apply (intro_classes)
197  apply (clarsimp simp add: updateObject_default_def in_monad projectKO_opts_defs
198                            projectKO_eq2
199                     split: kernel_object.splits arch_kernel_object.splits)
200  done
201
202end
203
204instantiation X64_H.pml4e :: pspace_storable
205begin
206interpretation Arch .
207
208#INCLUDE_HASKELL SEL4/Object/Instances/X64.lhs instanceproofs bodies_only ONLY PML4E
209
210instance
211  apply (intro_classes)
212  apply (clarsimp simp add: updateObject_default_def in_monad projectKO_opts_defs
213                            projectKO_eq2
214                     split: kernel_object.splits arch_kernel_object.splits)
215  done
216
217end
218
219(* This is hard coded since using funArray in haskell for 2^32 bound is risky *)
220
221instantiation X64_H.asidpool :: pspace_storable
222begin
223interpretation Arch .
224
225definition
226  makeObject_asidpool: "(makeObject :: asidpool)  \<equiv> ASIDPool $
227        funArray (const Nothing)"
228
229definition
230  loadObject_asidpool[simp]:
231 "(loadObject p q n obj) :: asidpool kernel \<equiv>
232    loadObject_default p q n obj"
233
234definition
235  updateObject_asidpool[simp]:
236 "updateObject (val :: asidpool) \<equiv>
237    updateObject_default val"
238
239instance
240  apply (intro_classes)
241  apply (clarsimp simp add: updateObject_default_def in_monad projectKO_opts_defs
242                            projectKO_eq2
243                     split: kernel_object.splits arch_kernel_object.splits)
244  done
245
246end
247
248lemmas load_update_defs =
249  loadObject_pte updateObject_pte
250  loadObject_pde updateObject_pde
251  loadObject_pdpte updateObject_pdpte
252  loadObject_pml4e updateObject_pml4e
253  loadObject_asidpool updateObject_asidpool
254
255declare load_update_defs[simp del]
256
257end_qualify
258
259declare (in Arch) load_update_defs[simp]
260
261end
262