1(*
2 * Copyright 2014, General Dynamics C4 Systems
3 *
4 * SPDX-License-Identifier: GPL-2.0-only
5 *)
6
7(*
8Decoding system calls
9*)
10
11chapter "Decoding System Calls"
12
13theory Decode_A
14imports
15  Interrupt_A
16  ArchDecode_A
17  "ExecSpec.InvocationLabels_H"
18begin
19
20context begin interpretation Arch .
21
22requalify_consts
23  ArchDefaultExtraRegisters
24  check_valid_ipc_buffer
25  is_valid_vtable_root
26  arch_decode_irq_control_invocation
27  arch_data_to_obj_type
28  arch_decode_invocation
29  arch_check_irq
30
31end
32
33
34text \<open>
35  This theory includes definitions describing how user arguments are
36decoded into invocation structures; these structures are then used
37to perform the actual system call (see @{text "perform_invocation"}).
38In addition, these definitions check the validity of these arguments,
39throwing an error if given an invalid request.
40
41  As such, this theory describes the binary interface between the
42user and the kernel, along with the preconditions on each argument.
43\<close>
44
45
46section "CNode"
47
48text \<open>This definition decodes CNode invocations.\<close>
49
50definition
51  decode_cnode_invocation ::
52  "data \<Rightarrow> data list \<Rightarrow> cap \<Rightarrow> cap list \<Rightarrow> (cnode_invocation,'z::state_ext) se_monad"
53where
54"decode_cnode_invocation label args cap excaps \<equiv> doE
55  unlessE (gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]) $
56    throwError IllegalOperation;
57  whenE (length args < 2) (throwError TruncatedMessage);
58  index \<leftarrow> returnOk $ data_to_cptr $ args ! 0;
59  bits \<leftarrow> returnOk $ data_to_nat $ args ! 1;
60  args \<leftarrow> returnOk $ drop 2 args;
61  dest_slot \<leftarrow> lookup_target_slot cap index bits;
62  if length args \<ge> 2 \<and> length excaps > 0
63        \<and> gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate] then
64  doE
65    src_index \<leftarrow> returnOk $ data_to_cptr $ args ! 0;
66    src_depth \<leftarrow> returnOk $ data_to_nat $ args ! 1;
67    args \<leftarrow> returnOk $ drop 2 args;
68    src_root_cap \<leftarrow> returnOk $ excaps ! 0;
69    ensure_empty dest_slot;
70    src_slot \<leftarrow>
71         lookup_source_slot src_root_cap src_index src_depth;
72    src_cap \<leftarrow> liftE $ get_cap src_slot;
73    whenE (src_cap = NullCap) $
74         throwError $ FailedLookup True $ MissingCapability src_depth;
75    (rights, cap_data, is_move) \<leftarrow> case (gen_invocation_type label, args) of
76      (CNodeCopy, rightsWord # _) \<Rightarrow> doE
77                    rights \<leftarrow> returnOk $ data_to_rights $ rightsWord;
78                    returnOk $ (rights, None, False)
79                odE
80     | (CNodeMint, rightsWord # capData # _) \<Rightarrow> doE
81                    rights \<leftarrow> returnOk $ data_to_rights $ rightsWord;
82                    returnOk $ (rights, Some capData, False)
83                odE
84     | (CNodeMove, _) \<Rightarrow> returnOk (all_rights, None, True)
85     | (CNodeMutate, capData # _) \<Rightarrow> returnOk (all_rights, Some capData, True)
86     | _ \<Rightarrow> throwError TruncatedMessage;
87    src_cap \<leftarrow> returnOk $ mask_cap rights src_cap;
88    new_cap \<leftarrow> (if is_move then returnOk else derive_cap src_slot) (case cap_data of
89                  Some w \<Rightarrow> update_cap_data is_move w src_cap
90                | None \<Rightarrow> src_cap);
91    whenE (new_cap = NullCap) $ throwError IllegalOperation;
92    returnOk $ (if is_move then MoveCall else InsertCall) new_cap src_slot dest_slot
93  odE
94  else if gen_invocation_type label = CNodeRevoke then returnOk $ RevokeCall dest_slot
95  else if gen_invocation_type label = CNodeDelete then returnOk $ DeleteCall dest_slot
96  else if gen_invocation_type label = CNodeSaveCaller then doE
97    ensure_empty dest_slot;
98    returnOk $ SaveCall dest_slot
99  odE
100  else if gen_invocation_type label = CNodeCancelBadgedSends then doE
101    cap \<leftarrow> liftE $ get_cap dest_slot;
102    unlessE (has_cancel_send_rights cap) $ throwError IllegalOperation;
103    returnOk $ CancelBadgedSendsCall cap
104  odE
105  else if gen_invocation_type label = CNodeRotate \<and> length args > 5
106          \<and> length excaps > 1 then
107  doE
108    pivot_new_data \<leftarrow> returnOk $ args ! 0;
109    pivot_index \<leftarrow> returnOk $ data_to_cptr $ args ! 1;
110    pivot_depth \<leftarrow> returnOk $ data_to_nat $ args ! 2;
111    src_new_data \<leftarrow> returnOk $ args ! 3;
112    src_index \<leftarrow> returnOk $ data_to_cptr $ args ! 4;
113    src_depth \<leftarrow> returnOk $ data_to_nat $ args ! 5;
114    pivot_root_cap <- returnOk $ excaps ! 0;
115    src_root_cap <- returnOk $ excaps ! 1;
116
117    src_slot <- lookup_source_slot src_root_cap src_index src_depth;
118    pivot_slot <- lookup_pivot_slot pivot_root_cap pivot_index pivot_depth;
119
120    whenE (pivot_slot = src_slot \<or> pivot_slot = dest_slot) $
121      throwError IllegalOperation;
122
123    unlessE (src_slot = dest_slot) $ ensure_empty dest_slot;
124
125    src_cap <- liftE $ get_cap src_slot;
126    whenE (src_cap = NullCap) $
127      throwError $ FailedLookup True $ MissingCapability src_depth;
128
129    pivot_cap <- liftE $ get_cap pivot_slot;
130    whenE (pivot_cap = NullCap) $
131      throwError $ FailedLookup False $ MissingCapability pivot_depth;
132
133    new_src_cap \<leftarrow> returnOk $ update_cap_data True src_new_data src_cap;
134    new_pivot_cap \<leftarrow> returnOk $ update_cap_data True pivot_new_data pivot_cap;
135
136    whenE (new_src_cap = NullCap) $ throwError IllegalOperation;
137    whenE (new_pivot_cap = NullCap) $ throwError IllegalOperation;
138
139    returnOk $ RotateCall new_src_cap new_pivot_cap src_slot pivot_slot dest_slot
140  odE
141  else
142    throwError TruncatedMessage
143odE"
144
145section "Threads"
146
147text \<open>The definitions in this section decode invocations
148on TCBs.
149\<close>
150
151text \<open>This definition checks whether the first argument is
152between the second and third.
153\<close>
154
155definition
156  decode_read_registers :: "data list \<Rightarrow> cap \<Rightarrow> (tcb_invocation,'z::state_ext) se_monad"
157where
158"decode_read_registers data cap \<equiv> case data of
159  flags#n#_ \<Rightarrow> doE
160    range_check n 1 $ of_nat (length frameRegisters + length gpRegisters);
161    p \<leftarrow> case cap of ThreadCap p \<Rightarrow> returnOk p;
162    self \<leftarrow> liftE $ gets cur_thread;
163    whenE (p = self) $ throwError IllegalOperation;
164    returnOk $ ReadRegisters p (flags !! 0) n ArchDefaultExtraRegisters
165  odE
166| _ \<Rightarrow> throwError TruncatedMessage"
167
168definition
169  decode_copy_registers :: "data list \<Rightarrow> cap \<Rightarrow> cap list \<Rightarrow> (tcb_invocation,'z::state_ext) se_monad"
170where
171"decode_copy_registers data cap extra_caps \<equiv> case data of
172  flags#_ \<Rightarrow>  doE
173    suspend_source \<leftarrow> returnOk (flags !! 0);
174    resume_target \<leftarrow> returnOk (flags !! 1);
175    transfer_frame \<leftarrow> returnOk (flags !! 2);
176    transfer_integer \<leftarrow> returnOk (flags !! 3);
177    whenE (extra_caps = []) $ throwError TruncatedMessage;
178    src_tcb \<leftarrow> (case extra_caps of
179      ThreadCap p # _ \<Rightarrow> returnOk p
180    | _ \<Rightarrow> throwError $ InvalidCapability 1);
181    p \<leftarrow> case cap of ThreadCap p \<Rightarrow> returnOk p;
182    returnOk $ CopyRegisters p src_tcb
183                             suspend_source resume_target
184                             transfer_frame transfer_integer
185                             ArchDefaultExtraRegisters
186  odE
187| _ \<Rightarrow>  throwError TruncatedMessage"
188
189
190definition
191  decode_write_registers :: "data list \<Rightarrow> cap \<Rightarrow> (tcb_invocation,'z::state_ext) se_monad"
192where
193"decode_write_registers data cap \<equiv> case data of
194  flags#n#values \<Rightarrow> doE
195    whenE (length values < unat n) $ throwError TruncatedMessage;
196    p \<leftarrow> case cap of ThreadCap p \<Rightarrow> returnOk p;
197    self \<leftarrow> liftE $ gets cur_thread;
198    whenE (p = self) $ throwError IllegalOperation;
199    returnOk $ WriteRegisters p (flags !! 0)
200               (take (unat n) values) ArchDefaultExtraRegisters
201  odE
202| _ \<Rightarrow> throwError TruncatedMessage"
203
204
205definition
206  check_prio :: "data \<Rightarrow> obj_ref \<Rightarrow> (unit,'z::state_ext) se_monad"
207where
208  "check_prio new_prio auth_tcb \<equiv>
209    doE
210      mcp \<leftarrow> liftE $ thread_get tcb_mcpriority auth_tcb;
211      whenE (new_prio > ucast mcp) $ throwError (RangeError 0 (ucast mcp))
212    odE"
213
214
215definition
216  decode_set_priority :: "data list \<Rightarrow> cap \<Rightarrow> cslot_ptr \<Rightarrow> (cap \<times> cslot_ptr) list \<Rightarrow> (tcb_invocation,'z::state_ext) se_monad"
217where
218  "decode_set_priority args cap slot extra_caps \<equiv> doE
219     whenE (length args = 0 \<or> length extra_caps = 0) $ throwError TruncatedMessage;
220     prio \<leftarrow> returnOk $ ucast (args ! 0);
221     auth_tcb \<leftarrow> case fst (extra_caps ! 0) of
222         ThreadCap tcb_ptr \<Rightarrow> returnOk tcb_ptr
223       | _ \<Rightarrow> throwError (InvalidCapability 1);
224     check_prio (args ! 0) auth_tcb;
225     returnOk (ThreadControl (obj_ref_of cap) slot None None
226                             (Some (prio, auth_tcb)) None None None)
227     odE"
228
229
230definition
231  decode_set_mcpriority :: "data list \<Rightarrow> cap \<Rightarrow> cslot_ptr \<Rightarrow> (cap \<times> cslot_ptr) list \<Rightarrow> (tcb_invocation,'z::state_ext) se_monad"
232where
233  "decode_set_mcpriority args cap slot extra_caps \<equiv> doE
234     whenE (length args = 0 \<or> length extra_caps = 0) $ throwError TruncatedMessage;
235     new_mcp \<leftarrow> returnOk $ ucast $ args ! 0;
236     auth_tcb \<leftarrow> case fst (extra_caps ! 0) of
237         ThreadCap tcb_ptr \<Rightarrow> returnOk tcb_ptr
238       | _ \<Rightarrow> throwError (InvalidCapability 1);
239     check_prio (args ! 0) auth_tcb;
240     returnOk (ThreadControl (obj_ref_of cap) slot None (Some (new_mcp, auth_tcb))
241                             None None None None)
242     odE"
243
244
245definition
246  decode_set_sched_params :: "data list \<Rightarrow> cap \<Rightarrow> cslot_ptr \<Rightarrow> (cap \<times> cslot_ptr) list \<Rightarrow> (tcb_invocation,'z::state_ext) se_monad"
247where
248  "decode_set_sched_params args cap slot extra_caps \<equiv> doE
249     whenE (length args < 2) $ throwError TruncatedMessage;
250     whenE (length extra_caps = 0) $ throwError TruncatedMessage;
251     new_mcp \<leftarrow> returnOk $ ucast $ args ! 0;
252     new_prio \<leftarrow> returnOk $ ucast $ args ! 1;
253     auth_tcb \<leftarrow> case fst (extra_caps ! 0) of
254         ThreadCap tcb_ptr \<Rightarrow> returnOk tcb_ptr
255       | _ \<Rightarrow> throwError (InvalidCapability 1);
256     check_prio (args ! 0) auth_tcb;
257     check_prio (args ! 1) auth_tcb;
258     returnOk (ThreadControl (obj_ref_of cap) slot None
259                             (Some (new_mcp, auth_tcb)) (Some (new_prio, auth_tcb)) None None None)
260     odE"
261
262
263definition
264  decode_set_ipc_buffer ::
265  "data list \<Rightarrow> cap \<Rightarrow> cslot_ptr \<Rightarrow> (cap \<times> cslot_ptr) list \<Rightarrow> (tcb_invocation,'z::state_ext) se_monad"
266where
267"decode_set_ipc_buffer args cap slot excs \<equiv> doE
268  whenE (length args = 0) $ throwError TruncatedMessage;
269  whenE (length excs = 0) $ throwError TruncatedMessage;
270  buffer \<leftarrow> returnOk $ data_to_vref $ args ! 0;
271  (bcap, bslot) \<leftarrow> returnOk $ excs ! 0;
272  newbuf \<leftarrow> if buffer = 0 then returnOk None
273           else doE
274      buffer_cap \<leftarrow> derive_cap bslot bcap;
275      check_valid_ipc_buffer buffer buffer_cap;
276      returnOk $ Some (buffer_cap, bslot)
277    odE;
278  returnOk $
279    ThreadControl (obj_ref_of cap) slot None None None None None (Some (buffer, newbuf))
280odE"
281
282
283definition
284  decode_set_space
285  :: "data list \<Rightarrow> cap \<Rightarrow> cslot_ptr \<Rightarrow> (cap \<times> cslot_ptr) list \<Rightarrow> (tcb_invocation,'z::state_ext) se_monad"
286where
287  "decode_set_space args cap slot excaps \<equiv> doE
288   whenE (length args < 3 \<or> length excaps < 2) $ throwError TruncatedMessage;
289   fault_ep \<leftarrow> returnOk $ args ! 0;
290   croot_data  \<leftarrow> returnOk $ args ! 1;
291   vroot_data  \<leftarrow> returnOk $ args ! 2;
292   croot_arg  \<leftarrow> returnOk $ excaps ! 0;
293   vroot_arg  \<leftarrow> returnOk $ excaps ! 1;
294   can_chg_cr \<leftarrow> liftE $ liftM Not $ slot_cap_long_running_delete
295                      $ get_tcb_ctable_ptr $ obj_ref_of cap;
296   can_chg_vr \<leftarrow> liftE $ liftM Not $ slot_cap_long_running_delete
297                      $ get_tcb_vtable_ptr $ obj_ref_of cap;
298   unlessE (can_chg_cr \<and> can_chg_vr) $ throwError IllegalOperation;
299
300   croot_cap  \<leftarrow> returnOk $ fst croot_arg;
301   croot_slot \<leftarrow> returnOk $ snd croot_arg;
302   croot_cap' \<leftarrow> derive_cap croot_slot $
303                   (if croot_data = 0 then id else update_cap_data False croot_data)
304                   croot_cap;
305   unlessE (is_cnode_cap croot_cap') $ throwError IllegalOperation;
306   croot \<leftarrow> returnOk (croot_cap', croot_slot);
307
308   vroot_cap  \<leftarrow> returnOk $ fst vroot_arg;
309   vroot_slot \<leftarrow> returnOk $ snd vroot_arg;
310   vroot_cap' \<leftarrow> derive_cap vroot_slot $
311                   (if vroot_data = 0 then id else update_cap_data False vroot_data)
312                   vroot_cap;
313   unlessE (is_valid_vtable_root vroot_cap') $ throwError IllegalOperation;
314   vroot \<leftarrow> returnOk (vroot_cap', vroot_slot);
315
316   returnOk $ ThreadControl (obj_ref_of cap) slot (Some (to_bl fault_ep)) None None
317                            (Some croot) (Some vroot) None
318 odE"
319
320
321definition
322  decode_tcb_configure ::
323  "data list \<Rightarrow> cap \<Rightarrow> cslot_ptr \<Rightarrow> (cap \<times> cslot_ptr) list \<Rightarrow> (tcb_invocation,'z::state_ext) se_monad"
324where
325  "decode_tcb_configure args cap slot extra_caps \<equiv> doE
326     whenE (length args < 4) $ throwError TruncatedMessage;
327     whenE (length extra_caps < 3) $ throwError TruncatedMessage;
328     fault_ep \<leftarrow> returnOk $ args ! 0;
329     croot_data \<leftarrow> returnOk $ args ! 1;
330     vroot_data \<leftarrow> returnOk $ args ! 2;
331     crootvroot \<leftarrow> returnOk $ take 2 extra_caps;
332     buffer_cap \<leftarrow> returnOk $ extra_caps ! 2;
333     buffer \<leftarrow> returnOk $ args ! 3;
334     set_params \<leftarrow> decode_set_ipc_buffer [buffer] cap slot [buffer_cap];
335     set_space \<leftarrow> decode_set_space [fault_ep, croot_data, vroot_data] cap slot crootvroot;
336     returnOk $ ThreadControl (obj_ref_of cap) slot (tc_new_fault_ep set_space)
337                              None None
338                              (tc_new_croot set_space) (tc_new_vroot set_space)
339                              (tc_new_buffer set_params)
340   odE"
341
342definition
343  decode_bind_notification ::
344  "cap \<Rightarrow> (cap \<times> cslot_ptr) list \<Rightarrow> (tcb_invocation,'z::state_ext) se_monad"
345where
346  "decode_bind_notification cap extra_caps \<equiv> case cap of
347    ThreadCap tcb \<Rightarrow> doE
348     whenE (length extra_caps = 0) $ throwError TruncatedMessage;
349     nTFN \<leftarrow> liftE $ get_bound_notification tcb;
350     case nTFN of
351         Some _ \<Rightarrow> throwError IllegalOperation
352       | None \<Rightarrow> returnOk ();
353     (ntfnptr, rights) \<leftarrow> case fst (hd extra_caps) of
354         NotificationCap ptr _ r \<Rightarrow> returnOk (ptr, r)
355       | _ \<Rightarrow> throwError IllegalOperation;
356     whenE (AllowRecv \<notin> rights) $ throwError IllegalOperation;
357     ntfn \<leftarrow> liftE  $ get_notification ntfnptr;
358     case (ntfn_obj ntfn, ntfn_bound_tcb ntfn) of
359         (IdleNtfn, None) \<Rightarrow> returnOk ()
360       | (ActiveNtfn _, None) \<Rightarrow> returnOk ()
361       | _ \<Rightarrow> throwError IllegalOperation;
362      returnOk $ NotificationControl tcb (Some ntfnptr)
363   odE
364 | _ \<Rightarrow> throwError IllegalOperation"
365
366
367definition
368  decode_unbind_notification :: "cap \<Rightarrow> (tcb_invocation,'z::state_ext) se_monad"
369where
370  "decode_unbind_notification cap \<equiv> case cap of
371     ThreadCap tcb \<Rightarrow> doE
372       nTFN \<leftarrow> liftE $ get_bound_notification tcb;
373       case nTFN of
374           None \<Rightarrow> throwError IllegalOperation
375         | Some _ \<Rightarrow> returnOk ();
376       returnOk $ NotificationControl tcb None
377    odE
378 | _ \<Rightarrow> throwError IllegalOperation"
379
380definition
381  decode_set_tls_base :: "data list \<Rightarrow> cap \<Rightarrow> (tcb_invocation,'z::state_ext) se_monad"
382where
383  "decode_set_tls_base args cap \<equiv> doE
384     whenE (length args = 0) $ throwError TruncatedMessage;
385     returnOk (SetTLSBase (obj_ref_of cap) (ucast (args ! 0)))
386   odE"
387
388definition
389  decode_tcb_invocation ::
390  "data \<Rightarrow> data list \<Rightarrow> cap \<Rightarrow> cslot_ptr \<Rightarrow> (cap \<times> cslot_ptr) list \<Rightarrow>
391  (tcb_invocation,'z::state_ext) se_monad"
392where
393 "decode_tcb_invocation label args cap slot excs \<equiv>
394  case gen_invocation_type label of
395      TCBReadRegisters \<Rightarrow> decode_read_registers args cap
396    | TCBWriteRegisters \<Rightarrow> decode_write_registers args cap
397    | TCBCopyRegisters \<Rightarrow> decode_copy_registers args cap $ map fst excs
398    | TCBSuspend \<Rightarrow> returnOk $ Suspend $ obj_ref_of cap
399    | TCBResume \<Rightarrow> returnOk $ Resume $ obj_ref_of cap
400    | TCBConfigure \<Rightarrow> decode_tcb_configure args cap slot excs
401    | TCBSetPriority \<Rightarrow> decode_set_priority args cap slot excs
402    | TCBSetMCPriority \<Rightarrow> decode_set_mcpriority args cap slot excs
403    | TCBSetSchedParams \<Rightarrow> decode_set_sched_params args cap slot excs
404    | TCBSetIPCBuffer \<Rightarrow> decode_set_ipc_buffer args cap slot excs
405    | TCBSetSpace \<Rightarrow> decode_set_space args cap slot excs
406    | TCBBindNotification \<Rightarrow> decode_bind_notification cap excs
407    | TCBUnbindNotification \<Rightarrow> decode_unbind_notification cap
408    | TCBSetTLSBase \<Rightarrow> decode_set_tls_base args cap
409    | _ \<Rightarrow> throwError IllegalOperation"
410
411definition
412  decode_domain_invocation ::
413  "data \<Rightarrow> data list \<Rightarrow> (cap \<times> cslot_ptr) list \<Rightarrow>
414    ((obj_ref \<times> domain), 'z::state_ext) se_monad"
415where
416  "decode_domain_invocation label args excs \<equiv> doE
417     whenE (gen_invocation_type label \<noteq> DomainSetSet) $ throwError IllegalOperation;
418     domain \<leftarrow> (case args of
419       x # xs \<Rightarrow> doE
420         whenE (unat x \<ge> num_domains) $ throwError $ InvalidArgument 0;
421         returnOk (ucast x)
422       odE
423       | _ \<Rightarrow> throwError TruncatedMessage);
424     whenE (length excs = 0) $ throwError TruncatedMessage;
425     case (fst (hd excs)) of ThreadCap ptr \<Rightarrow> returnOk $ (ptr, domain)
426       | _ \<Rightarrow> throwError $ InvalidArgument 1
427   odE"
428
429section "IRQ"
430
431text \<open>The following two definitions decode system calls for the
432interrupt controller and interrupt handlers\<close>
433
434definition
435  decode_irq_control_invocation :: "data \<Rightarrow> data list \<Rightarrow> cslot_ptr \<Rightarrow> cap list
436                                     \<Rightarrow> (irq_control_invocation,'z::state_ext) se_monad" where
437 "decode_irq_control_invocation label args src_slot cps \<equiv>
438  (if gen_invocation_type label = IRQIssueIRQHandler
439    then if length args \<ge> 3 \<and> length cps \<ge> 1
440      then let irq_word = args ! 0;
441               index = args ! 1;
442               depth = args ! 2;
443               cnode = cps ! 0;
444               irq = ucast irq_word
445      in doE
446        arch_check_irq irq_word;
447        irq_active \<leftarrow> liftE $ is_irq_active irq;
448        whenE irq_active $ throwError RevokeFirst;
449
450        dest_slot \<leftarrow> lookup_target_slot
451               cnode (data_to_cptr index) (unat depth);
452        ensure_empty dest_slot;
453
454        returnOk $ IRQControl irq dest_slot src_slot
455      odE
456    else throwError TruncatedMessage
457  else liftME ArchIRQControl $ arch_decode_irq_control_invocation label args src_slot cps)"
458
459definition
460  decode_irq_handler_invocation :: "data \<Rightarrow> irq \<Rightarrow> (cap \<times> cslot_ptr) list
461                                     \<Rightarrow> (irq_handler_invocation,'z::state_ext) se_monad" where
462 "decode_irq_handler_invocation label irq cps \<equiv>
463  if gen_invocation_type label = IRQAckIRQ
464    then returnOk $ ACKIrq irq
465  else if gen_invocation_type label = IRQSetIRQHandler
466    then if cps \<noteq> []
467      then let (cap, slot) = hd cps in
468      if is_ntfn_cap cap \<and> AllowSend \<in> cap_rights cap
469      then returnOk $ SetIRQHandler irq cap slot
470      else throwError $ InvalidCapability 0
471    else throwError TruncatedMessage
472  else if gen_invocation_type label = IRQClearIRQHandler
473    then returnOk $ ClearIRQHandler irq
474  else throwError IllegalOperation"
475
476section "Untyped"
477
478text \<open>The definitions in this section deal with decoding invocations
479of untyped memory capabilities.
480\<close>
481
482definition
483  data_to_obj_type :: "data \<Rightarrow> (apiobject_type,'z::state_ext) se_monad" where
484  "data_to_obj_type type \<equiv> doE
485    n \<leftarrow> returnOk $ data_to_nat type;
486    if n = 0 then
487      returnOk $ Untyped
488    else if n = 1 then
489      returnOk $ TCBObject
490    else if n = 2 then
491      returnOk $ EndpointObject
492    else if n = 3 then
493      returnOk $ NotificationObject
494    else if n = 4 then
495      returnOk $ CapTableObject
496    else (case arch_data_to_obj_type (n - 5)
497       of Some tp \<Rightarrow> returnOk (ArchObject tp)
498        | None \<Rightarrow> throwError (InvalidArgument 0))
499  odE"
500
501definition
502  decode_untyped_invocation ::
503  "data \<Rightarrow> data list \<Rightarrow> cslot_ptr \<Rightarrow> cap \<Rightarrow> cap list \<Rightarrow> (untyped_invocation,'z::state_ext) se_monad"
504where
505"decode_untyped_invocation label args slot cap excaps \<equiv> doE
506  unlessE (gen_invocation_type label = UntypedRetype) $ throwError IllegalOperation;
507  whenE (length args < 6) $ throwError TruncatedMessage;
508  whenE (length excaps = 0) $ throwError TruncatedMessage;
509  root_cap \<leftarrow> returnOk $ excaps ! 0;
510  new_type \<leftarrow> data_to_obj_type (args!0);
511
512  user_obj_size \<leftarrow> returnOk $ data_to_nat (args!1);
513  object_size \<leftarrow> returnOk (obj_bits_api new_type user_obj_size);
514  unlessE (user_obj_size < word_bits \<and> object_size \<le> untyped_max_bits)
515    $ throwError (RangeError 0 (of_nat untyped_max_bits));
516  whenE (new_type = CapTableObject \<and> user_obj_size = 0)
517    $ throwError (InvalidArgument 1);
518  whenE (new_type = Untyped \<and> user_obj_size < untyped_min_bits)
519    $ throwError (InvalidArgument 1);
520  node_index \<leftarrow> returnOk $ data_to_cptr (args!2);
521  node_depth \<leftarrow> returnOk $ data_to_nat (args!3);
522
523  node_cap \<leftarrow> if node_depth = 0
524        then returnOk root_cap
525        else doE
526            node_slot \<leftarrow> lookup_target_slot
527                root_cap node_index node_depth;
528            liftE $ get_cap node_slot
529        odE;
530
531  if is_cnode_cap node_cap
532        then  returnOk ()
533        else  throwError $ FailedLookup False $ MissingCapability node_depth;
534
535  node_offset \<leftarrow> returnOk $ data_to_nat (args ! 4);
536  node_window \<leftarrow> returnOk $ data_to_nat (args ! 5);
537  radix_bits \<leftarrow> returnOk $ bits_of node_cap;
538  node_size \<leftarrow> returnOk (2 ^ radix_bits);
539
540  whenE (node_offset < 0 \<or> node_offset > node_size - 1) $
541    throwError $ RangeError 0 (of_nat (node_size - 1));
542
543  whenE (node_window < 1 \<or> node_window > 256) $ throwError $ RangeError 1 256;
544
545  whenE (node_window < 1 \<or> node_window > node_size - node_offset) $
546    throwError $ RangeError 1 (of_nat (node_size - node_offset));
547
548  oref \<leftarrow> returnOk $ obj_ref_of node_cap;
549  offsets \<leftarrow> returnOk $ map (nat_to_cref radix_bits)
550                           [node_offset ..< node_offset + node_window];
551  slots \<leftarrow> returnOk $ map (\<lambda>cref. (oref, cref)) offsets;
552
553  mapME_x ensure_empty slots;
554
555  reset \<leftarrow> liftE $ const_on_failure False $ (doE
556    ensure_no_children slot;
557    returnOk True
558  odE);
559
560  free_index \<leftarrow> returnOk (if reset then 0 else free_index_of cap);
561  free_ref \<leftarrow> returnOk (get_free_ref (obj_ref_of cap) free_index);
562  aligned_free_ref \<leftarrow> returnOk (alignUp free_ref object_size);
563  untyped_free_bytes \<leftarrow> returnOk (obj_size cap - of_nat (free_index));
564
565  max_count \<leftarrow> returnOk ( untyped_free_bytes >> object_size);
566  whenE (unat max_count < node_window) $
567        throwError $ NotEnoughMemory $ untyped_free_bytes;
568
569  not_frame \<leftarrow> returnOk (\<not> is_frame_type new_type);
570  (ptr, is_device) \<leftarrow> case cap of
571                        UntypedCap dev p n f \<Rightarrow> returnOk (p,dev)
572                      | _ \<Rightarrow> fail;
573  whenE (is_device \<and> not_frame \<and> new_type \<noteq> Untyped) $
574           throwError $ InvalidArgument 1;
575  returnOk $ Retype slot reset ptr aligned_free_ref new_type user_obj_size slots is_device
576odE"
577
578section "Toplevel invocation decode."
579
580text \<open>This definition is the toplevel decoding definition; it dispatches
581to the above definitions, after checking, in some cases, whether the
582invocation is allowed.
583\<close>
584
585definition
586  decode_invocation ::
587  "data \<Rightarrow> data list \<Rightarrow> cap_ref \<Rightarrow> cslot_ptr \<Rightarrow> cap \<Rightarrow> (cap \<times> cslot_ptr) list \<Rightarrow> (invocation,'z::state_ext) se_monad"
588where
589  "decode_invocation label args cap_index slot cap excaps \<equiv>
590  case cap of
591    EndpointCap ptr badge rights \<Rightarrow>
592      if AllowSend \<in> rights then
593        returnOk $ InvokeEndpoint ptr badge (AllowGrant \<in> rights) (AllowGrantReply \<in> rights)
594      else throwError $ InvalidCapability 0
595  | NotificationCap ptr badge rights \<Rightarrow>
596      if AllowSend \<in> rights then
597        returnOk $ InvokeNotification ptr badge
598      else throwError $ InvalidCapability 0
599  | ReplyCap thread False rights \<Rightarrow>
600      returnOk $ InvokeReply thread slot (AllowGrant \<in> rights)
601  | IRQControlCap \<Rightarrow>
602      liftME InvokeIRQControl
603        $ decode_irq_control_invocation label args slot (map fst excaps)
604  | IRQHandlerCap irq \<Rightarrow>
605      liftME InvokeIRQHandler
606        $ decode_irq_handler_invocation label irq excaps
607  | ThreadCap ptr \<Rightarrow>
608      liftME InvokeTCB $ decode_tcb_invocation label args cap slot excaps
609  | DomainCap \<Rightarrow>
610      liftME (case_prod InvokeDomain) $ decode_domain_invocation label args excaps
611  | CNodeCap ptr bits _ \<Rightarrow>
612      liftME InvokeCNode $ decode_cnode_invocation label args cap (map fst excaps)
613  | UntypedCap dev ptr sz fi \<Rightarrow>
614      liftME InvokeUntyped $ decode_untyped_invocation label args slot cap (map fst excaps)
615  | ArchObjectCap arch_cap \<Rightarrow>
616      liftME InvokeArchObject $
617        arch_decode_invocation label args cap_index slot arch_cap excaps
618  | _ \<Rightarrow>
619      throwError $ InvalidCapability 0"
620
621end
622