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(*
12Arch specific object invocations
13*)
14
15chapter "x64 Object Invocations"
16
17theory ArchInvocation_A
18imports "../Structures_A"
19begin
20
21context Arch begin global_naming X64_A
22
23text {* These datatypes encode the arguments to the various possible
24x64-specific system calls. Selectors are defined for various fields
25for convenience elsewhere. *}
26
27datatype pdpt_invocation =
28    PDPTMap cap cslot_ptr pml4e obj_ref obj_ref
29  | PDPTUnmap cap cslot_ptr
30
31datatype page_directory_invocation =
32    PageDirectoryMap cap cslot_ptr pdpte obj_ref obj_ref
33  | PageDirectoryUnmap cap cslot_ptr
34
35datatype page_table_invocation =
36    PageTableMap cap cslot_ptr pde obj_ref obj_ref
37  | PageTableUnmap cap cslot_ptr
38
39datatype asid_control_invocation =
40    MakePool obj_ref cslot_ptr cslot_ptr asid
41
42datatype asid_pool_invocation =
43    Assign asid obj_ref cslot_ptr
44
45datatype page_invocation
46     = PageMap
47         (page_map_cap: cap)
48         (page_map_ct_slot: cslot_ptr)
49         (page_map_entries: "vm_page_entry \<times> obj_ref")
50         (page_map_vspace: obj_ref)
51     | PageRemap
52         (page_remap_entries: "vm_page_entry \<times> obj_ref")
53         (page_remap_asid: asid)
54         (page_remap_vspace: obj_ref)
55     | PageUnmap
56         (page_unmap_cap: arch_cap)
57         (page_unmap_cap_slot: cslot_ptr)
58(*     | PageIOMap
59         (page_iomap_cap: cap)
60         (page_iomap_ct_clot: cslot_ptr)
61         (page_iomap_asid: iopte)
62         (page_iomap_entries: "obj_ref") *)
63     | PageGetAddr
64         (page_get_paddr: obj_ref)
65
66datatype io_port_invocation_data
67  = IOPortIn8 | IOPortIn16 | IOPortIn32
68  | IOPortOut8 "8 word" | IOPortOut16 "16 word" | IOPortOut32 "32 word"
69
70datatype io_port_invocation = IOPortInvocation io_port io_port_invocation_data
71
72datatype io_port_control_invocation = IOPortControlInvocation io_port io_port cslot_ptr cslot_ptr
73
74(*
75datatype io_pt_invocation
76     = IOPageTableMapContext cap cslot_ptr iocte obj_ref
77     | IOPageTableMap cap cslot_ptr iopte obj_ref
78     | IOPageTableUnmap cap cslot_ptr *)
79
80datatype arch_invocation
81     = InvokePageTable page_table_invocation
82     | InvokePageDirectory page_directory_invocation
83     | InvokePDPT pdpt_invocation
84     | InvokePage page_invocation
85     | InvokeASIDControl asid_control_invocation
86     | InvokeASIDPool asid_pool_invocation
87     | InvokeIOPort io_port_invocation
88     | InvokeIOPortControl io_port_control_invocation
89     (*| InvokeIOPT io_pt_invocation*)
90
91datatype arch_copy_register_sets = X64NoExtraRegisters
92
93definition "ArchDefaultExtraRegisters \<equiv> X64NoExtraRegisters"
94
95datatype arch_irq_control_invocation
96  = IssueIRQHandlerIOAPIC irq cslot_ptr cslot_ptr
97      machine_word machine_word machine_word machine_word machine_word
98  | IssueIRQHandlerMSI irq cslot_ptr cslot_ptr
99      machine_word machine_word machine_word machine_word
100
101end
102end
103