2014-07-14 19:32:44 +00:00
|
|
|
(*
|
|
|
|
|
* Copyright 2014, General Dynamics C4 Systems
|
|
|
|
|
*
|
|
|
|
|
* This software may be distributed and modified according to the terms of
|
|
|
|
|
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
|
|
|
|
|
* See "LICENSE_GPLv2.txt" for details.
|
|
|
|
|
*
|
|
|
|
|
* @TAG(GD_GPL)
|
|
|
|
|
*)
|
|
|
|
|
|
|
|
|
|
(*
|
|
|
|
|
Data types for syscall invocations
|
|
|
|
|
*)
|
|
|
|
|
|
2015-05-16 09:52:49 +00:00
|
|
|
chapter "Kernel Object Invocations"
|
2014-07-14 19:32:44 +00:00
|
|
|
|
|
|
|
|
theory Invocations_A
|
2016-01-12 05:39:35 +00:00
|
|
|
imports "./$L4V_ARCH/ArchInvocation_A"
|
2014-07-14 19:32:44 +00:00
|
|
|
begin
|
|
|
|
|
|
2016-05-04 03:28:20 +00:00
|
|
|
context begin interpretation Arch .
|
|
|
|
|
|
|
|
|
|
requalify_types
|
2016-02-04 08:17:47 +00:00
|
|
|
arch_copy_register_sets
|
|
|
|
|
arch_irq_control_invocation
|
|
|
|
|
arch_invocation
|
|
|
|
|
|
2016-06-27 07:19:11 +00:00
|
|
|
requalify_consts
|
|
|
|
|
message_info_to_data
|
|
|
|
|
data_to_message_info
|
|
|
|
|
|
2016-05-04 03:28:20 +00:00
|
|
|
end
|
|
|
|
|
|
2014-07-14 19:32:44 +00:00
|
|
|
text {* These datatypes encode the arguments to the available system calls. *}
|
|
|
|
|
|
|
|
|
|
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
|
|
|
|
|
| RecycleCall cslot_ptr
|
|
|
|
|
|
|
|
|
|
datatype untyped_invocation =
|
2016-02-11 06:02:13 +00:00
|
|
|
Retype cslot_ptr obj_ref obj_ref apiobject_type nat "cslot_ptr list" bool
|
2014-07-14 19:32:44 +00:00
|
|
|
|
2016-02-04 08:17:47 +00:00
|
|
|
datatype tcb_invocation =
|
2016-01-12 05:39:35 +00:00
|
|
|
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
|
2016-07-08 04:31:51 +00:00
|
|
|
(tc_new_fault_ep: "cap_ref option") (tc_new_mcpriority: "word8 option") (tc_new_priority: "word8 option")
|
2015-05-16 09:52:49 +00:00
|
|
|
(tc_new_croot: "(cap * cslot_ptr) option") (tc_new_vroot: "(cap * cslot_ptr) option")
|
|
|
|
|
(tc_new_buffer: "(vspace_ref * (cap * cslot_ptr) option) option")
|
2016-01-12 05:39:35 +00:00
|
|
|
| Suspend "obj_ref"
|
|
|
|
|
| Resume "obj_ref"
|
2015-11-02 00:00:32 +00:00
|
|
|
| NotificationControl "obj_ref" "obj_ref option"
|
2014-07-14 19:32:44 +00:00
|
|
|
|
|
|
|
|
datatype irq_control_invocation =
|
|
|
|
|
IRQControl irq cslot_ptr cslot_ptr
|
2016-01-14 04:01:46 +00:00
|
|
|
| ArchIRQControl arch_irq_control_invocation
|
2014-07-14 19:32:44 +00:00
|
|
|
|
|
|
|
|
datatype irq_handler_invocation =
|
|
|
|
|
ACKIrq irq
|
|
|
|
|
| SetIRQHandler irq cap cslot_ptr
|
|
|
|
|
| ClearIRQHandler irq
|
|
|
|
|
|
|
|
|
|
datatype invocation =
|
|
|
|
|
InvokeUntyped untyped_invocation
|
2016-01-12 05:39:35 +00:00
|
|
|
| InvokeEndpoint obj_ref machine_word bool
|
|
|
|
|
| InvokeNotification obj_ref machine_word
|
2014-07-14 19:32:44 +00:00
|
|
|
| InvokeReply obj_ref cslot_ptr
|
|
|
|
|
| InvokeTCB tcb_invocation
|
|
|
|
|
| InvokeDomain obj_ref word8
|
|
|
|
|
| InvokeCNode cnode_invocation
|
|
|
|
|
| InvokeIRQControl irq_control_invocation
|
|
|
|
|
| InvokeIRQHandler irq_handler_invocation
|
|
|
|
|
| InvokeArchObject arch_invocation
|
|
|
|
|
|
|
|
|
|
end
|
