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