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