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 "ARM Object Invocations" 16 17theory ArchInvocation_A 18imports "../Structures_A" 19begin 20 21context Arch begin global_naming ARM_A 22 23text {* These datatypes encode the arguments to the various possible 24ARM-specific system calls. Selectors are defined for various fields 25for convenience elsewhere. *} 26 27datatype flush_type = Clean | Invalidate | CleanInvalidate | Unify 28 29datatype page_directory_invocation = 30 PageDirectoryFlush (pd_flush_type: flush_type) (pd_flush_start: vspace_ref) 31 (pd_flush_end: vspace_ref) (pd_flush_pstart: word32) 32 (pd_flush_pd: obj_ref) (pd_flush_asid: asid) 33 | PageDirectoryNothing 34 35datatype page_table_invocation = 36 PageTableMap cap cslot_ptr pde 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_asid: asid) 48 (page_map_cap: cap) 49 (page_map_ct_slot: cslot_ptr) 50 (page_map_entries: "pte \<times> (obj_ref list) + pde \<times> (obj_ref list)") 51 | PageRemap 52 (page_remap_asid: asid) 53 (page_remap_entries: "pte \<times> (obj_ref list) + pde \<times> (obj_ref list)") 54 | PageUnmap 55 (page_unmap_cap: arch_cap) 56 (page_unmap_cap_slot: cslot_ptr) 57 | PageFlush 58 (page_flush_type: flush_type) 59 (page_flush_start: vspace_ref) 60 (page_flush_end: vspace_ref) 61 (page_flush_pstart: word32) 62 (page_flush_pd: obj_ref) 63 (page_flush_asid: asid) 64 | PageGetAddr 65 (page_get_paddr: obj_ref) 66 67datatype vcpu_invocation = 68 VCPUSetTCB obj_ref (*vcpu*) obj_ref (*tcb*) 69 | VCPUInjectIRQ obj_ref nat virq 70 | VCPUReadRegister obj_ref vcpureg 71 | VCPUWriteRegister obj_ref vcpureg machine_word 72 73datatype arch_invocation 74 = InvokePageTable page_table_invocation 75 | InvokePageDirectory page_directory_invocation 76 | InvokePage page_invocation 77 | InvokeASIDControl asid_control_invocation 78 | InvokeASIDPool asid_pool_invocation 79 | InvokeVCPU vcpu_invocation 80 81(* The ARM platform currently does not define any additional register sets for 82the "CopyRegisters" operation. This may be changed in future to support a floating point unit. *) 83 84datatype arch_copy_register_sets = ARMNoExtraRegisters 85 86definition "ArchDefaultExtraRegisters \<equiv> ARMNoExtraRegisters" 87 88datatype arch_irq_control_invocation = 89 ArchIRQControlIssue irq cslot_ptr cslot_ptr bool 90 91end 92 93end 94