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