1(*
2 * Copyright 2014, General Dynamics C4 Systems
3 *
4 * SPDX-License-Identifier: GPL-2.0-only
5 *)
6
7(*
8Data types for syscall invocations
9*)
10
11chapter "Kernel Object Invocations"
12
13theory Invocations_A
14imports ArchInvocation_A
15begin
16
17context begin interpretation Arch .
18
19requalify_types
20  arch_copy_register_sets
21  arch_irq_control_invocation
22  arch_invocation
23
24end
25
26text \<open>These datatypes encode the arguments to the available system calls.\<close>
27
28datatype cnode_invocation =
29    InsertCall cap cslot_ptr cslot_ptr
30  | MoveCall cap cslot_ptr cslot_ptr
31  | RevokeCall cslot_ptr
32  | DeleteCall cslot_ptr
33  | RotateCall cap cap cslot_ptr cslot_ptr cslot_ptr
34  | SaveCall cslot_ptr
35  | CancelBadgedSendsCall cap
36
37datatype untyped_invocation =
38    Retype cslot_ptr bool obj_ref obj_ref apiobject_type nat "cslot_ptr list" bool
39
40datatype tcb_invocation =
41    WriteRegisters machine_word bool "machine_word list" arch_copy_register_sets
42  | ReadRegisters machine_word bool machine_word arch_copy_register_sets
43  | CopyRegisters machine_word machine_word bool bool bool bool arch_copy_register_sets
44  | ThreadControl machine_word cslot_ptr
45                  (tc_new_fault_ep: "cap_ref option")
46                  (tc_new_mcpriority: "(word8 * obj_ref) option")
47                  (tc_new_priority: "(word8 * obj_ref) option")
48                  (tc_new_croot: "(cap * cslot_ptr) option")
49                  (tc_new_vroot: "(cap * cslot_ptr) option")
50                  (tc_new_buffer: "(vspace_ref * (cap * cslot_ptr) option) option")
51  | Suspend "obj_ref"
52  | Resume "obj_ref"
53  | NotificationControl "obj_ref" "obj_ref option"
54  | SetTLSBase obj_ref machine_word
55
56datatype irq_control_invocation =
57    IRQControl irq cslot_ptr cslot_ptr
58  | ArchIRQControl arch_irq_control_invocation
59
60datatype irq_handler_invocation =
61    ACKIrq irq
62  | SetIRQHandler irq cap cslot_ptr
63  | ClearIRQHandler irq
64
65datatype invocation =
66    InvokeUntyped untyped_invocation
67  | InvokeEndpoint obj_ref machine_word bool bool
68  | InvokeNotification obj_ref machine_word
69  | InvokeReply obj_ref cslot_ptr bool
70  | InvokeTCB tcb_invocation
71  | InvokeDomain obj_ref word8
72  | InvokeCNode cnode_invocation
73  | InvokeIRQControl irq_control_invocation
74  | InvokeIRQHandler irq_handler_invocation
75  | InvokeArchObject arch_invocation
76
77end
78