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