1(* 2 * Copyright 2014, General Dynamics C4 Systems 3 * 4 * SPDX-License-Identifier: GPL-2.0-only 5 *) 6 7(* 8Arch specific object invocations 9*) 10 11chapter "ARM Object Invocations" 12 13theory ArchInvocation_A 14imports Structures_A 15begin 16 17context Arch begin global_naming ARM_A 18 19text \<open>These datatypes encode the arguments to the various possible 20ARM-specific system calls. Selectors are defined for various fields 21for convenience elsewhere.\<close> 22 23datatype flush_type = Clean | Invalidate | CleanInvalidate | Unify 24 25datatype page_directory_invocation = 26 PageDirectoryFlush (pd_flush_type: flush_type) (pd_flush_start: vspace_ref) 27 (pd_flush_end: vspace_ref) (pd_flush_pstart: word32) 28 (pd_flush_pd: obj_ref) (pd_flush_asid: asid) 29 | PageDirectoryNothing 30 31datatype page_table_invocation = 32 PageTableMap cap cslot_ptr pde obj_ref 33 | PageTableUnmap cap cslot_ptr 34 35datatype asid_control_invocation = 36 MakePool obj_ref cslot_ptr cslot_ptr asid 37 38datatype asid_pool_invocation = 39 Assign asid obj_ref cslot_ptr 40 41datatype page_invocation 42 = PageMap 43 (page_map_asid: asid) 44 (page_map_cap: cap) 45 (page_map_ct_slot: cslot_ptr) 46 (page_map_entries: "pte \<times> (obj_ref list) + pde \<times> (obj_ref list)") 47 | PageUnmap 48 (page_unmap_cap: arch_cap) 49 (page_unmap_cap_slot: cslot_ptr) 50 | PageFlush 51 (page_flush_type: flush_type) 52 (page_flush_start: vspace_ref) 53 (page_flush_end: vspace_ref) 54 (page_flush_pstart: word32) 55 (page_flush_pd: obj_ref) 56 (page_flush_asid: asid) 57 | PageGetAddr 58 (page_get_paddr: obj_ref) 59 60datatype arch_invocation 61 = InvokePageTable page_table_invocation 62 | InvokePageDirectory page_directory_invocation 63 | InvokePage page_invocation 64 | InvokeASIDControl asid_control_invocation 65 | InvokeASIDPool asid_pool_invocation 66 67datatype arch_copy_register_sets = ARMNoExtraRegisters 68 69definition "ArchDefaultExtraRegisters \<equiv> ARMNoExtraRegisters" 70 71datatype arch_irq_control_invocation = 72 ArchIRQControlIssue irq cslot_ptr cslot_ptr bool 73 74end 75 76end 77