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