-
Notifications
You must be signed in to change notification settings - Fork 0
/
Invocations_D.thy
109 lines (88 loc) · 3.51 KB
/
Invocations_D.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
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
(*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: GPL-2.0-only
*)
theory Invocations_D
imports Types_D
begin
datatype cdl_cnode_invocation =
InsertCall cdl_cap cdl_cap_ref cdl_cap_ref
| MoveCall cdl_cap cdl_cap_ref cdl_cap_ref
| RevokeCall cdl_cap_ref
| DeleteCall cdl_cap_ref
| RotateCall cdl_cap cdl_cap cdl_cap_ref cdl_cap_ref cdl_cap_ref
| SaveCall cdl_cap_ref
| CancelBadgedSendsCall cdl_cap
datatype cdl_untyped_invocation =
Retype cdl_cap_ref
cdl_object_type cdl_size_bits "cdl_cap_ref list" bool nat
datatype cdl_tcb_invocation =
WriteRegisters cdl_object_id bool "word32 list" nat
| ReadRegisters cdl_object_id bool word32 nat
| CopyRegisters cdl_object_id cdl_object_id bool bool bool bool nat
| ThreadControl cdl_object_id cdl_cap_ref
"cdl_cptr option"
"(cdl_cap \<times> cdl_cap_ref) option"
"(cdl_cap \<times> cdl_cap_ref) option"
"(cdl_cap \<times> cdl_cap_ref) option"
| Suspend cdl_object_id
| Resume cdl_object_id
| NotificationControl cdl_object_id "cdl_object_id option"
| SetTLSBase cdl_object_id
datatype arch_cdl_irq_control_invocation =
ARMIssueIrqHandler cdl_irq cdl_cap_ref cdl_cap_ref bool
datatype cdl_irq_control_invocation =
IssueIrqHandler cdl_irq cdl_cap_ref cdl_cap_ref
| ArchIssueIrqHandler arch_cdl_irq_control_invocation
datatype cdl_irq_handler_invocation =
AckIrq cdl_irq
| SetIrqHandler cdl_irq cdl_cap cdl_cap_ref
| ClearIrqHandler cdl_irq
datatype cdl_endpoint_invocation =
(* We need not track the "block" or "call" bits because they
are handled separately in the top-level syscall interface. *)
(* badge, grant, grant reply, ep *)
SyncMessage cdl_badge bool bool cdl_object_id
datatype cdl_notification_invocation =
(* badge (notification word) and notification object *)
Signal cdl_badge cdl_object_id
datatype cdl_reply_invocation =
ReplyMessage cdl_object_id cdl_cap_ref bool (* can grant *)
datatype cdl_page_table_invocation =
(* PageTableMap <real_pt_cap> <pt_cap> <pt_cap_ref> <pd_target_slot> *)
PageTableMap cdl_cap cdl_cap cdl_cap_ref cdl_cap_ref
(* PageTableUnmap <mapped_addr option> <pt_obj_id> <pt_cap_ref> *)
| PageTableUnmap "cdl_mapped_addr option" cdl_object_id cdl_cap_ref
datatype cdl_asid_control_invocation =
MakePool cdl_cap cdl_cap_ref "cdl_object_id set" cdl_cap_ref nat
datatype cdl_asid_pool_invocation =
Assign cdl_asid cdl_cap_ref cdl_cap_ref
datatype flush =
Clean | Invalidate | CleanInvalidate | Unify
datatype cdl_page_invocation =
PageMap cdl_cap cdl_cap cdl_cap_ref "cdl_cap_ref list"
| PageUnmap "cdl_mapped_addr option" cdl_object_id "cdl_cap_ref" nat
| PageFlushCaches flush
| PageGetAddress
datatype cdl_page_directory_invocation =
PageDirectoryFlush flush
| PageDirectoryNothing
datatype cdl_domain_invocation =
SetDomain cdl_object_id word8
datatype cdl_invocation =
InvokeUntyped cdl_untyped_invocation
| InvokeEndpoint cdl_endpoint_invocation
| InvokeNotification cdl_notification_invocation
| InvokeReply cdl_reply_invocation
| InvokeTcb cdl_tcb_invocation
| InvokeDomain cdl_domain_invocation
| InvokeCNode cdl_cnode_invocation
| InvokeIrqControl cdl_irq_control_invocation
| InvokeIrqHandler cdl_irq_handler_invocation
| InvokePageTable cdl_page_table_invocation
| InvokePage cdl_page_invocation
| InvokePageDirectory cdl_page_directory_invocation
| InvokeAsidControl cdl_asid_control_invocation
| InvokeAsidPool cdl_asid_pool_invocation
end