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