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
11chapter "x64-Specific Data Types"
12
13theory Arch_Structs_A
14imports
15  "ExecSpec.Arch_Structs_B"
16  "../ExceptionTypes_A"
17  "../VMRights_A"
18begin
19
20context Arch begin global_naming X64_A
21
22text {*
23This theory provides architecture-specific definitions and datatypes
24including architecture-specific capabilities and objects.
25*}
26
27section {* Architecture-specific virtual memory *}
28
29type_synonym io_port = "16 word"
30type_synonym io_asid = "16 word"
31
32section {* Architecture-specific capabilities *}
33
34text {*  The x64 kernel supports capabilities for ASID pools and an ASID controller capability,
35along with capabilities for IO ports and spaces, as well as virtual memory mappings. *}
36
37datatype arch_cap =
38   ASIDPoolCap (acap_asid_pool : obj_ref) (acap_asid_base : asid)
39 | ASIDControlCap
40 | IOPortCap (acap_io_port_first_port : io_port) (acap_io_port_last_port : io_port)
41 | IOPortControlCap
42(* FIXME x64-vtd:
43 | IOSpaceCap (cap_io_domain_id : "16 word") (cap_io_pci_device : "io_asid option")
44 | IOPageTableCap (cap_iopt_base_ptr : obj_ref) (cap_io_pt_level : nat) (cap_iopt_mapped_address : "(io_asid * vspace_ref) option")
45*)
46 | PageCap bool obj_ref (acap_rights : cap_rights) vmmap_type vmpage_size "(asid * vspace_ref) option"
47 | PageTableCap obj_ref "(asid * vspace_ref) option"
48 | PageDirectoryCap obj_ref "(asid * vspace_ref) option"
49 | PDPointerTableCap obj_ref "(asid * vspace_ref) option"
50 | PML4Cap obj_ref "asid option"
51
52(* cr3 Stuff *)
53datatype cr3 = cr3 obj_ref asid
54
55primrec
56  cr3_base_address :: "cr3 \<Rightarrow> obj_ref"
57where
58  "cr3_base_address (cr3 addr _) = addr"
59
60primrec
61  cr3_pcid :: "cr3 \<Rightarrow> asid"
62where
63  "cr3_pcid (cr3 _ pcid) = pcid"
64
65section {* Architecture-specific objects *}
66
67datatype table_attr = Accessed | CacheDisabled | WriteThrough | ExecuteDisable
68type_synonym table_attrs = "table_attr set"
69
70datatype frame_attr = PTAttr table_attr | Global | PAT | Dirty
71type_synonym frame_attrs = "frame_attr set"
72
73datatype pml4e
74     = InvalidPML4E
75     | PDPointerTablePML4E
76         (pml4_table : obj_ref)
77         (pml4e_attrs : table_attrs)
78         (pml4e_rights : vm_rights)
79
80datatype pdpte
81     = InvalidPDPTE
82     | PageDirectoryPDPTE
83         (pdpt_table : obj_ref)
84         (pdpt_table_attrs : table_attrs)
85         (pdpt_rights : vm_rights)
86     | HugePagePDPTE
87         (pdpt_frame : obj_ref)
88         (pdpt_frame_attrs : frame_attrs)
89         (pdpt_rights : vm_rights)
90
91datatype pde
92      = InvalidPDE
93      | PageTablePDE
94         obj_ref
95         (pt_attrs : table_attrs)
96         (pde_rights : cap_rights)
97      | LargePagePDE
98         obj_ref
99         (pde_page_attrs : frame_attrs)
100         (pde_rights: cap_rights)
101
102datatype pte
103      = InvalidPTE
104      | SmallPagePTE
105         (pte_frame: obj_ref)
106         (pte_frame_attrs : frame_attrs)
107         (pte_rights : cap_rights)
108
109
110datatype vm_page_entry = VMPTE pte | VMPDE pde | VMPDPTE pdpte
111
112datatype translation_type = NotTranslated | Translated
113
114datatype iocte =
115   InvalidIOCTE
116 | VTDCTE
117   (domain_id : word16)
118   (res_mem_reg: bool)
119   (address_width: nat)
120   (next_level_ptr: obj_ref)
121   (translation_type: translation_type)
122   (iocte_present : bool)
123
124datatype iopte =
125   InvalidIOPTE
126 | VTDPTE
127   (frame_ptr : obj_ref)
128   (io_pte_rights  : vm_rights)
129
130datatype iorte =
131   InvalidIORTE
132 | VTDRTE
133   (context_table : obj_ref)
134   (iorte_present : bool)
135
136datatype arch_kernel_obj =
137   ASIDPool "9 word \<rightharpoonup> obj_ref"
138 | PageTable "9 word \<Rightarrow> pte"
139 | PageDirectory "9 word \<Rightarrow> pde"
140 | PDPointerTable "9 word \<Rightarrow> pdpte"
141 | PageMapL4 "9 word \<Rightarrow> pml4e"
142 | DataPage bool vmpage_size
143(* FIXME x64-vtd:
144 | IORootTable "16 word \<Rightarrow> iorte"
145 | IOContextTable "16 word \<Rightarrow> iocte"
146 | IOPageTable "16 word \<Rightarrow> iopte" *)
147
148definition table_size :: nat where
149  "table_size = ptTranslationBits + word_size_bits"
150
151definition iotable_size :: nat where
152  "iotable_size = ptTranslationBits + 2*word_size_bits"
153
154definition cte_level_bits :: nat where
155  "cte_level_bits \<equiv> 5"
156
157primrec
158  arch_obj_size :: "arch_cap \<Rightarrow> nat"
159where
160  "arch_obj_size (ASIDPoolCap _ _) = pageBits"
161| "arch_obj_size ASIDControlCap = 0"
162| "arch_obj_size (IOPortCap _ _) = 0"
163| "arch_obj_size IOPortControlCap = 0"
164(* FIXME x64-vtd:
165| "arch_obj_size (IOSpaceCap _ _) = 0"
166| "arch_obj_size (IOPageTableCap _ _ _) = iotable_size" *)
167| "arch_obj_size (PageCap _ _ _ _ sz _) = pageBitsForSize sz"
168| "arch_obj_size (PageTableCap _ _) = table_size"
169| "arch_obj_size (PageDirectoryCap _ _) = table_size"
170| "arch_obj_size (PDPointerTableCap _ _) = table_size"
171| "arch_obj_size (PML4Cap _ _) = table_size"
172
173primrec
174  arch_cap_is_device :: "arch_cap \<Rightarrow> bool"
175where
176  "arch_cap_is_device (ASIDPoolCap _ _) = False"
177| "arch_cap_is_device ASIDControlCap = False"
178| "arch_cap_is_device (IOPortCap _ _) = False"
179| "arch_cap_is_device IOPortControlCap = False"
180(* FIXME x64-vtd:
181| "arch_cap_is_device (IOSpaceCap _ _) = False"
182| "arch_cap_is_device (IOPageTableCap _ _ _) = False" *)
183| "arch_cap_is_device (PageCap is_dev _ _ _ _ _) = is_dev"
184| "arch_cap_is_device (PageTableCap _ _) = False"
185| "arch_cap_is_device (PageDirectoryCap _ _) = False"
186| "arch_cap_is_device (PDPointerTableCap _ _) = False"
187| "arch_cap_is_device (PML4Cap _ _) = False"
188
189definition tcb_bits :: nat where
190  "tcb_bits \<equiv> 11"
191
192definition endpoint_bits :: nat where
193  "endpoint_bits \<equiv> 4"
194
195definition ntfn_bits :: nat where
196  "ntfn_bits \<equiv> 5"
197
198definition untyped_min_bits :: nat where
199  "untyped_min_bits \<equiv> 4"
200
201definition untyped_max_bits :: nat where
202  "untyped_max_bits \<equiv> 47"
203
204primrec
205  arch_kobj_size :: "arch_kernel_obj \<Rightarrow> nat"
206where
207  "arch_kobj_size (ASIDPool _) = pageBits"
208| "arch_kobj_size (PageTable _) = table_size"
209| "arch_kobj_size (PageDirectory _) = table_size"
210| "arch_kobj_size (PDPointerTable _) = table_size"
211| "arch_kobj_size (PageMapL4 _) = table_size"
212| "arch_kobj_size (DataPage _ sz) = pageBitsForSize sz"
213
214primrec
215  aobj_ref :: "arch_cap \<rightharpoonup> obj_ref"
216where
217  "aobj_ref (ASIDPoolCap x _) = Some x"
218| "aobj_ref ASIDControlCap = None"
219| "aobj_ref (IOPortCap _ _) = None"
220| "aobj_ref IOPortControlCap = None"
221(* FIXME x64-vtd:
222| "aobj_ref (IOSpaceCap _ _) = None"
223| "aobj_ref (IOPageTableCap x _ _) = Some x" *)
224| "aobj_ref (PageCap _ x _ _ _ _) = Some x"
225| "aobj_ref (PageDirectoryCap x _) = Some x"
226| "aobj_ref (PageTableCap x _) = Some x"
227| "aobj_ref (PDPointerTableCap x _) = Some x"
228| "aobj_ref (PML4Cap x _) = Some x"
229
230
231definition
232  acap_rights_update :: "cap_rights \<Rightarrow> arch_cap \<Rightarrow> arch_cap" where
233 "acap_rights_update rs ac \<equiv> case ac of
234    PageCap dev x rs' m sz as \<Rightarrow> PageCap dev x (validate_vm_rights rs) m sz as
235  | _                   \<Rightarrow> ac"
236
237section {* Architecture-specific object types and default objects *}
238
239datatype
240  aobject_type =
241    SmallPageObj
242  | LargePageObj
243  | HugePageObj
244  | PageTableObj
245  | PageDirectoryObj
246  | PDPTObj
247  | PML4Obj
248  | ASIDPoolObj
249
250datatype X64IRQState =
251   IRQFree
252 | IRQReserved
253 | IRQMSI
254      (MSIBus : machine_word)
255      (MSIDev : machine_word)
256      (MSIFunc : machine_word)
257      (MSIHandle : machine_word)
258 | IRQIOAPIC
259      (IRQioapic : machine_word)
260      (IRQPin : machine_word)
261      (IRQLevel : machine_word)
262      (IRQPolarity : machine_word)
263      (IRQMasked : bool)
264
265definition
266  arch_is_frame_type :: "aobject_type \<Rightarrow> bool"
267where
268  "arch_is_frame_type aobj \<equiv> case aobj of
269         SmallPageObj \<Rightarrow> True
270       | LargePageObj \<Rightarrow> True
271       | HugePageObj \<Rightarrow> True
272       | _ \<Rightarrow> False"
273
274definition
275  arch_default_cap :: "aobject_type \<Rightarrow> obj_ref \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> arch_cap" where
276 "arch_default_cap tp r n dev \<equiv> case tp of
277    SmallPageObj \<Rightarrow> PageCap dev r vm_read_write VMNoMap X64SmallPage None
278  | LargePageObj \<Rightarrow> PageCap dev r vm_read_write VMNoMap X64LargePage None
279  | HugePageObj \<Rightarrow> PageCap dev r vm_read_write VMNoMap X64HugePage None
280  | PageTableObj \<Rightarrow> PageTableCap r None
281  | PageDirectoryObj \<Rightarrow> PageDirectoryCap r None
282  | PDPTObj \<Rightarrow> PDPointerTableCap r None
283  | PML4Obj \<Rightarrow> PML4Cap r None
284  | ASIDPoolObj \<Rightarrow> ASIDPoolCap r 0" (* unused *)
285
286definition
287  default_arch_object :: "aobject_type \<Rightarrow> bool \<Rightarrow> nat \<Rightarrow> arch_kernel_obj" where
288 "default_arch_object tp dev n \<equiv> case tp of
289    SmallPageObj \<Rightarrow> DataPage dev X64SmallPage
290  | LargePageObj \<Rightarrow> DataPage dev X64LargePage
291  | HugePageObj \<Rightarrow> DataPage dev X64HugePage
292  | PageTableObj \<Rightarrow> PageTable (\<lambda>x. InvalidPTE)
293  | PageDirectoryObj \<Rightarrow> PageDirectory (\<lambda>x. InvalidPDE)
294  | PDPTObj \<Rightarrow> PDPointerTable (\<lambda>x. InvalidPDPTE)
295  | PML4Obj \<Rightarrow> PageMapL4 (\<lambda>x. InvalidPML4E)
296  | ASIDPoolObj \<Rightarrow> ASIDPool (\<lambda>_. None)"
297
298type_synonym x64_vspace_region_uses = "vspace_ref \<Rightarrow> x64vspace_region_use"
299
300end
301
302qualify X64_A (in Arch)
303
304section {* Architecture-specific state *}
305
306record arch_state =
307  x64_asid_table            :: "3 word \<rightharpoonup> obj_ref"
308  x64_global_pml4           :: obj_ref
309  x64_kernel_vspace         :: X64_A.x64_vspace_region_uses
310  x64_global_pts            :: "obj_ref list"
311  x64_global_pdpts          :: "obj_ref list"
312  x64_global_pds            :: "obj_ref list"
313  x64_current_cr3           :: "X64_A.cr3"
314  x64_allocated_io_ports    :: "X64_A.io_port \<Rightarrow> bool"
315  x64_num_ioapics           :: "64 word"
316  x64_irq_state             :: "8 word \<Rightarrow> X64_A.X64IRQState"
317
318(* FIXME x64-vtd:
319  x64_num_io_domain_bits    :: "16 word"
320  x64_first_valid_io_domain :: "16 word"
321  x64_num_io_domain_id_bits :: "32 word"
322  x64_io_root_table         :: obj_ref *)
323
324end_qualify
325
326context Arch begin global_naming X64_A
327
328definition
329  pd_shift_bits :: "nat" where
330  "pd_shift_bits \<equiv> pageBits + ptTranslationBits"
331
332definition
333  pt_shift_bits :: "nat" where
334  "pt_shift_bits \<equiv> pageBits"
335
336definition
337  pdpt_shift_bits :: "nat" where
338  "pdpt_shift_bits \<equiv> pageBits + ptTranslationBits + ptTranslationBits"
339
340definition
341  pml4_shift_bits :: "nat" where
342  "pml4_shift_bits \<equiv> pageBits + ptTranslationBits + ptTranslationBits + ptTranslationBits"
343
344definition
345  pt_bits :: "nat" where
346  "pt_bits \<equiv> table_size"
347
348definition
349  pd_bits :: "nat" where
350  "pd_bits \<equiv> table_size"
351
352definition
353  pdpt_bits :: "nat" where
354  "pdpt_bits \<equiv> table_size"
355
356definition
357  pml4_bits :: "nat" where
358  "pml4_bits \<equiv> table_size"
359
360definition
361  iopt_bits :: "nat" where
362  "iopt_bits \<equiv> iotable_size"
363
364definition
365  vtd_cte_size_bits :: "nat" where
366  "vtd_cte_size_bits \<equiv> 8"
367
368definition
369  vtd_pt_bits :: "nat" where
370  "vtd_pt_bits \<equiv> iotable_size"
371
372definition
373  x64_num_io_pt_levels :: "nat" where
374  "x64_num_io_pt_levels \<equiv> 4"
375
376section "Type declarations for invariant definitions"
377
378(* FIXME x64-vtd: add *)
379datatype aa_type =
380    AASIDPool
381  | APageTable
382  | APageDirectory
383  | APDPointerTable
384  | APageMapL4
385  | AUserData vmpage_size
386  | ADeviceData vmpage_size
387
388(* FIXME x64-vtd: add *)
389definition aa_type :: "arch_kernel_obj \<Rightarrow> aa_type"
390where
391 "aa_type ao \<equiv> (case ao of
392           PageTable pt             \<Rightarrow> APageTable
393         | PageDirectory pd         \<Rightarrow> APageDirectory
394         | DataPage dev sz          \<Rightarrow> if dev then ADeviceData sz else AUserData sz
395         | ASIDPool f               \<Rightarrow> AASIDPool
396         | PDPointerTable pdpt      \<Rightarrow> APDPointerTable
397         | PageMapL4 pm             \<Rightarrow> APageMapL4)"
398
399text {* For implementation reasons the badge word has differing amounts of bits *}
400definition
401  badge_bits :: nat where
402  "badge_bits \<equiv> 64"
403
404end
405
406section "Arch-specific TCB"
407
408qualify X64_A (in Arch)
409
410text \<open> Arch-specific part of a TCB: this must have at least a field for user context. \<close>
411record arch_tcb =
412  tcb_context :: user_context
413
414end_qualify
415
416context Arch begin global_naming X64_A
417
418definition
419  default_arch_tcb :: arch_tcb where
420  "default_arch_tcb \<equiv> \<lparr>tcb_context = new_context\<rparr>"
421
422text \<open> Accessors for @{text "tcb_context"} inside @{text "arch_tcb"}.
423  These are later used to implement @{text as_user}, i.e.\ need to be
424  compatible with @{text user_monad}.\<close>
425definition
426  arch_tcb_context_set :: "user_context \<Rightarrow> arch_tcb \<Rightarrow> arch_tcb"
427where
428  "arch_tcb_context_set uc a_tcb \<equiv> a_tcb \<lparr> tcb_context := uc \<rparr>"
429
430definition
431  arch_tcb_context_get :: "arch_tcb \<Rightarrow> user_context"
432where
433  "arch_tcb_context_get a_tcb \<equiv> tcb_context a_tcb"
434
435(* FIXME: the following means that we break the set/getRegister abstraction
436          and should move some of this into the machine interface *)
437text \<open>
438 Accessors for the user register part of the @{text "arch_tcb"}.
439 (Because @{typ "register \<Rightarrow> machine_word"} may not be equal to @{typ user_context}).
440\<close>
441definition
442  arch_tcb_set_registers :: "(register \<Rightarrow> machine_word) \<Rightarrow> arch_tcb \<Rightarrow> arch_tcb"
443where
444  "arch_tcb_set_registers regs a_tcb \<equiv>
445    a_tcb \<lparr> tcb_context := UserContext (fpu_state (tcb_context a_tcb)) regs \<rparr>"
446
447definition
448  arch_tcb_get_registers :: "arch_tcb \<Rightarrow> register \<Rightarrow> machine_word"
449where
450  "arch_tcb_get_registers a_tcb \<equiv> user_regs (tcb_context a_tcb)"
451
452end
453
454end
455