1(*
2 * Copyright 2014, NICTA
3 *
4 * This software may be distributed and modified according to the terms of
5 * the GNU General Public License version 2. Note that NO WARRANTY is provided.
6 * See "LICENSE_GPLv2.txt" for details.
7 *
8 * @TAG(NICTA_GPL)
9 *)
10
11(*
12 * System calls
13 *)
14
15theory Syscall_D
16imports
17  Schedule_D
18  Decode_D
19  "ExecSpec.Event_H"
20begin
21
22(*
23 * Perform system calls.
24 *
25 * Each system call is broken into three stages:
26 *
27 *   (1) Cap validation, where we ensure that all caps passed
28 *       into the system call are valid;
29 *
30 *   (2) Argument validation, where we ensure that the requested
31 *       operation is valid and permitted; and
32 *
33 *   (3) Syscall execution, where we carry out the actual
34 *       operation.
35 *
36 * For this function, the user passes us in 5 functions:
37 *
38 *   (1, 2) A cap validation function, and an error handler;
39 *   (3, 4) A argument validation function, and an error handler;
40 *   (5)    A syscall execution function.
41 *
42 * This function returns an item of type "'c", and may also
43 * return an exception if operation (3) above was preempted
44 * by an interrupt.
45 *)
46
47definition
48syscall :: "
49  ('a fault_monad) \<Rightarrow> (unit k_monad) \<Rightarrow>
50  ('a \<Rightarrow> 'b except_monad) \<Rightarrow> (unit k_monad) \<Rightarrow>
51  ('b \<Rightarrow> unit preempt_monad) \<Rightarrow> unit preempt_monad"
52where
53  "syscall
54      cap_decoder_fn decode_error_handler_fn
55      arg_decode_fn arg_error_handler_fn
56      perform_syscall_fn \<equiv>
57    cap_decoder_fn
58    <handle>
59      (\<lambda> _. liftE $ decode_error_handler_fn)
60    <else>
61      (\<lambda> a. ((arg_decode_fn a)
62        <handle>
63          (\<lambda> _. liftE $ arg_error_handler_fn)
64        <else>
65          perform_syscall_fn))
66  "
67
68fun
69  perform_invocation :: "bool \<Rightarrow> bool \<Rightarrow> cdl_invocation \<Rightarrow> unit preempt_monad"
70where
71    "perform_invocation is_call can_block (InvokeUntyped untyped_params) = (invoke_untyped untyped_params)"
72  | "perform_invocation is_call can_block (InvokeEndpoint endpoint_params) = liftE (invoke_endpoint is_call can_block endpoint_params)"
73  | "perform_invocation is_call can_block (InvokeNotification ntfn_params) = liftE (invoke_notification ntfn_params)"
74  | "perform_invocation is_call can_block (InvokeReply reply_params) = liftE (invoke_reply reply_params)"
75  | "perform_invocation is_call can_block (InvokeTcb tcb_params) = (invoke_tcb tcb_params)"
76  | "perform_invocation is_call can_block (InvokeDomain domain_params) = (invoke_domain domain_params)"
77  | "perform_invocation is_call can_block (InvokeCNode cnode_params) = invoke_cnode cnode_params"
78  | "perform_invocation is_call can_block (InvokeIrqControl irq_params) = liftE (invoke_irq_control irq_params)"
79  | "perform_invocation is_call can_block (InvokeIrqHandler handler_params) = liftE (invoke_irq_handler handler_params)"
80  | "perform_invocation is_call can_block (InvokePageTable page_table_params) = liftE (invoke_page_table page_table_params)"
81  | "perform_invocation is_call can_block (InvokePage page_params) = liftE (invoke_page page_params)"
82  | "perform_invocation is_call can_block (InvokeAsidControl asid_control_params) = liftE (invoke_asid_control asid_control_params)"
83  | "perform_invocation is_call can_block (InvokeAsidPool asid_pool_params) = liftE (invoke_asid_pool asid_pool_params)"
84  | "perform_invocation is_call can_block (InvokePageDirectory page_dir_params) = liftE (invoke_page_directory page_dir_params) "
85
86definition ep_related_cap :: "cdl_cap \<Rightarrow> bool"
87where "ep_related_cap cap \<equiv> case cap of
88 cdl_cap.EndpointCap o_id badge rights \<Rightarrow> True
89| cdl_cap.NotificationCap o_id badge rights \<Rightarrow> True
90| cdl_cap.ReplyCap o_id \<Rightarrow> True
91| _ \<Rightarrow> False"
92
93definition "has_restart_cap \<equiv> \<lambda>tcb_id. do
94  t \<leftarrow> get_thread tcb_id;
95  return ((cdl_tcb_caps t) tcb_pending_op_slot = Some cdl_cap.RestartCap)
96  od"
97
98definition
99  handle_invocation :: "bool \<Rightarrow> bool \<Rightarrow> unit preempt_monad"
100where
101  "handle_invocation is_call can_block \<equiv>
102    doE
103      thread_ptr \<leftarrow> liftE $ gets_the cdl_current_thread;
104      thread \<leftarrow> liftE $ get_thread thread_ptr;
105      full_intent \<leftarrow> returnOk $ cdl_tcb_intent thread;
106
107      intent \<leftarrow> returnOk $ cdl_intent_op full_intent;
108      invoked_cptr \<leftarrow> returnOk $ cdl_intent_cap full_intent;
109      extra_cap_cptrs \<leftarrow> returnOk $ cdl_intent_extras full_intent;
110
111      syscall
112        (* Lookup all caps presented. *)
113        (doE
114          (cap, cap_ref) \<leftarrow> lookup_cap_and_slot thread_ptr invoked_cptr;
115          extra_caps \<leftarrow> lookup_extra_caps thread_ptr extra_cap_cptrs;
116          returnOk (cap, cap_ref, extra_caps)
117        odE)
118        (* If that failed, send off a fault IPC (if we did a blocking operation). *)
119        (when can_block $ handle_fault)
120
121        (* Decode the user's intent. *)
122        (\<lambda> (cap, cap_ref, extra_caps).
123          case intent of
124              None \<Rightarrow> (if ep_related_cap cap then
125                decode_invocation cap cap_ref extra_caps undefined
126                else throw)
127            | Some intent' \<Rightarrow>
128                decode_invocation cap cap_ref extra_caps intent')
129
130        (* If that stuffed up, we do nothing more than corrupt the frames. *)
131        (do corrupt_ipc_buffer thread_ptr True;
132            when is_call (mark_tcb_intent_error thread_ptr True)
133         od)
134
135        (* Invoke the system call. *)
136        (\<lambda> inv. doE
137            liftE $ set_cap (thread_ptr,tcb_pending_op_slot) RestartCap;
138            perform_invocation is_call can_block inv;
139            restart \<leftarrow> liftE $ has_restart_cap thread_ptr;
140            whenE restart $ liftE (do
141                       corrupt_ipc_buffer thread_ptr True;
142                       when (is_call) (mark_tcb_intent_error thread_ptr False);
143                       set_cap (thread_ptr,tcb_pending_op_slot) RunningCap
144            od)
145            odE)
146  odE
147  "
148
149definition
150  handle_recv :: "unit k_monad"
151where
152  "handle_recv \<equiv>
153    do
154      (* Get the current thread. *)
155      tcb_id \<leftarrow> gets_the cdl_current_thread;
156      tcb \<leftarrow> get_thread tcb_id;
157      (* Get the endpoint it is trying to receive from. *)
158      (doE
159        ep_cptr \<leftarrow> returnOk $ cdl_intent_cap (cdl_tcb_intent tcb);
160        ep_cap \<leftarrow> lookup_cap tcb_id ep_cptr;
161        (case ep_cap of
162          EndpointCap o_id badge rights \<Rightarrow>
163            if Read \<in> rights then
164              (liftE $ do
165                   delete_cap_simple (tcb_id, tcb_caller_slot);
166                   receive_ipc tcb_id (cap_object ep_cap)
167                od) \<sqinter> throw
168            else
169              throw
170        | NotificationCap o_id badge rights \<Rightarrow>
171            if Read \<in> rights then
172              (liftE $ recv_signal tcb_id ep_cap) \<sqinter> throw
173            else
174              throw
175        | _ \<Rightarrow>
176            throw)
177      odE)
178      <catch>
179        (\<lambda> _. handle_fault)
180    od
181  "
182
183definition
184  handle_reply :: "unit k_monad"
185where
186  "handle_reply \<equiv>
187    do
188      tcb_id \<leftarrow> gets_the cdl_current_thread;
189      caller_cap \<leftarrow> get_cap (tcb_id, tcb_caller_slot);
190
191      case caller_cap of
192          ReplyCap target \<Rightarrow> do_reply_transfer tcb_id target (tcb_id, tcb_caller_slot)
193        | NullCap \<Rightarrow> return ()
194        | _ \<Rightarrow> fail
195    od
196  "
197
198definition handle_hypervisor_fault :: "unit k_monad"
199where "handle_hypervisor_fault \<equiv> return ()"
200
201definition
202  handle_syscall :: "syscall \<Rightarrow> unit preempt_monad"
203where
204  "handle_syscall sys \<equiv>
205    case sys of
206      SysSend  \<Rightarrow> handle_invocation False True
207    | SysNBSend \<Rightarrow> handle_invocation False False
208    | SysCall \<Rightarrow> handle_invocation True True
209    | SysRecv \<Rightarrow> liftE $ handle_recv
210    | SysYield \<Rightarrow> returnOk ()
211    | SysReply \<Rightarrow> liftE $ handle_reply
212    | SysReplyRecv \<Rightarrow> liftE $ do
213        handle_reply;
214        handle_recv
215      od
216    | SysNBRecv \<Rightarrow> liftE $ handle_recv"
217
218definition
219  handle_event :: "event \<Rightarrow> unit preempt_monad"
220where
221  "handle_event ev \<equiv> case ev of
222      SyscallEvent sys \<Rightarrow> handle_syscall sys
223    | UnknownSyscall n \<Rightarrow> liftE $ handle_fault
224    | UserLevelFault a b \<Rightarrow> liftE $ handle_fault
225    | VMFaultEvent c \<Rightarrow> liftE $ handle_fault
226    | Interrupt \<Rightarrow> liftE $ handle_pending_interrupts
227    | HypervisorEvent w \<Rightarrow> liftE $ handle_hypervisor_fault
228    "
229
230definition
231  call_kernel :: "event \<Rightarrow> unit k_monad"
232where
233  "call_kernel ev \<equiv>
234    do
235      (* Deal with the event. *)
236      handle_event ev
237        <handle> (\<lambda> _. liftE handle_pending_interrupts);
238      schedule;
239      t \<leftarrow> gets cdl_current_thread;
240      case t of Some thread \<Rightarrow> do
241       restart \<leftarrow> has_restart_cap thread;
242       when restart $ set_cap (thread, tcb_pending_op_slot) RunningCap
243      od | None \<Rightarrow> return ()
244    od"
245
246end
247