1(* 2 * Copyright 2014, General Dynamics C4 Systems 3 * 4 * SPDX-License-Identifier: GPL-2.0-only 5 *) 6 7(* 8The main architecture independent data types and type definitions in 9the abstract model. 10*) 11 12chapter "Basic Data Structures" 13 14theory Structures_A 15imports 16 Arch_Structs_A 17 "ExecSpec.MachineExports" 18begin 19 20context begin interpretation Arch . 21 22requalify_types 23 aobject_type 24 arch_cap 25 vm_rights 26 arch_kernel_obj 27 arch_state 28 arch_tcb 29 aa_type 30 31requalify_consts 32 acap_rights 33 acap_rights_update 34 arch_kobj_size 35 arch_obj_size 36 aobj_ref 37 asid_high_bits 38 asid_low_bits 39 arch_is_frame_type 40 badge_bits 41 default_arch_tcb 42 arch_tcb_context_get 43 arch_tcb_context_set 44 arch_tcb_set_registers 45 arch_tcb_get_registers 46 cte_level_bits 47 tcb_bits 48 endpoint_bits 49 ntfn_bits 50 aa_type 51 untyped_min_bits 52 untyped_max_bits 53 msg_label_bits 54end 55 56text \<open> 57 User mode can request these objects to be created by retype: 58\<close> 59datatype apiobject_type = 60 Untyped 61 | TCBObject 62 | EndpointObject 63 | NotificationObject 64 | CapTableObject 65 | ArchObject aobject_type 66 67definition 68 is_frame_type :: "apiobject_type \<Rightarrow> bool" 69where 70 "is_frame_type obj \<equiv> case obj of 71 ArchObject aobj \<Rightarrow> arch_is_frame_type aobj 72 | _ \<Rightarrow> False" 73 74 75text \<open>These allow more informative type signatures for IPC operations.\<close> 76type_synonym badge = data 77type_synonym msg_label = data 78type_synonym message = data 79 80 81text \<open>This type models refences to capability slots. The first element 82 of the tuple points to the object the capability is contained in. The second 83 element is the index of the slot inside a slot-containing object. The default 84 slot-containing object is a cnode, thus the name @{text cnode_index}. 85\<close> 86type_synonym cnode_index = "bool list" 87type_synonym cslot_ptr = "obj_ref \<times> cnode_index" 88 89 90text \<open>Capabilities. Capabilities represent explicit authority to perform some 91action and are required for all system calls. Capabilities to Endpoint, 92Notification, Thread and CNode objects allow manipulation of standard kernel 93objects. Untyped capabilities allow the creation and removal of kernel objects 94from a memory region. Reply capabilities allow sending a one-off message to 95a thread waiting for a reply. IRQHandler and IRQControl caps allow a user to 96configure the way interrupts on one or all IRQs are handled. Capabilities to 97architecture-specific facilities are provided through the @{text arch_cap} type. 98Null capabilities are the contents of empty capability slots; they confer no 99authority and can be freely replaced. Zombie capabilities are stored when 100the deletion of CNode and Thread objects is partially completed; they confer no 101authority but cannot be replaced until the deletion is finished. 102\<close> 103 104datatype cap 105 = NullCap 106 | UntypedCap bool obj_ref nat nat 107 \<comment> \<open>device flag, pointer, size in bits (i.e. @{text "size = 2^bits"}) and freeIndex (i.e. @{text "freeRef = obj_ref + (freeIndex * 2^4)"})\<close> 108 | EndpointCap obj_ref badge cap_rights 109 | NotificationCap obj_ref badge cap_rights 110 | ReplyCap obj_ref bool cap_rights 111 | CNodeCap obj_ref nat "bool list" 112 \<comment> \<open>CNode ptr, number of bits translated, guard\<close> 113 | ThreadCap obj_ref 114 | DomainCap 115 | IRQControlCap 116 | IRQHandlerCap irq 117 | Zombie obj_ref "nat option" nat 118 \<comment> \<open>@{text "cnode ptr * nat + tcb or cspace ptr"}\<close> 119 | ArchObjectCap (the_arch_cap: arch_cap) 120 121lemmas cap_cases = 122 cap.induct[where cap=cap and P="\<lambda>cap'. cap' = cap \<longrightarrow> P cap'" for cap P, simplified, rule_format] 123 124lemmas cap_cases_asm = 125cap.induct[where cap=cap and P="\<lambda>cap'. cap = cap' \<longrightarrow> P cap' \<longrightarrow> R" for P R cap, 126 simplified, rule_format, rotated -1] 127 128text \<open>The CNode object is an array of capability slots. The domain of the 129function will always be the set of boolean lists of some specific length. 130Empty slots contain a Null capability. 131\<close> 132type_synonym cnode_contents = "cnode_index \<Rightarrow> cap option" 133 134text \<open>Various access functions for the cap type are defined for 135convenience.\<close> 136definition 137 the_cnode_cap :: "cap \<Rightarrow> obj_ref \<times> nat \<times> bool list" where 138 "the_cnode_cap cap \<equiv> 139 case cap of 140 CNodeCap oref bits guard \<Rightarrow> (oref, bits, guard)" 141 142definition 143 the_arch_cap :: "cap \<Rightarrow> arch_cap" where 144 "the_arch_cap cap \<equiv> case cap of ArchObjectCap a \<Rightarrow> a" 145 146primrec (nonexhaustive) 147 cap_ep_badge :: "cap \<Rightarrow> badge" 148where 149 "cap_ep_badge (EndpointCap _ badge _) = badge" 150| "cap_ep_badge (NotificationCap _ badge _) = badge" 151 152primrec (nonexhaustive) 153 cap_ep_ptr :: "cap \<Rightarrow> badge" 154where 155 "cap_ep_ptr (EndpointCap obj_ref _ _) = obj_ref" 156| "cap_ep_ptr (NotificationCap obj_ref _ _) = obj_ref" 157 158definition 159 bits_of :: "cap \<Rightarrow> nat" where 160 "bits_of cap \<equiv> case cap of 161 UntypedCap _ _ bits _ \<Rightarrow> bits 162 | CNodeCap _ radix_bits _ \<Rightarrow> radix_bits" 163 164definition 165 free_index_of :: "cap \<Rightarrow> nat" where 166 "free_index_of cap \<equiv> case cap of 167 UntypedCap _ _ _ free_index \<Rightarrow> free_index" 168 169definition 170 is_reply_cap :: "cap \<Rightarrow> bool" where 171 "is_reply_cap cap \<equiv> case cap of ReplyCap _ m _ \<Rightarrow> \<not> m | _ \<Rightarrow> False" 172definition 173 is_master_reply_cap :: "cap \<Rightarrow> bool" where 174 "is_master_reply_cap cap \<equiv> case cap of ReplyCap _ m _ \<Rightarrow> m | _ \<Rightarrow> False" 175definition 176 is_zombie :: "cap \<Rightarrow> bool" where 177 "is_zombie cap \<equiv> case cap of Zombie _ _ _ \<Rightarrow> True | _ \<Rightarrow> False" 178definition 179 is_arch_cap :: "cap \<Rightarrow> bool" where 180 "is_arch_cap cap \<equiv> case cap of ArchObjectCap _ \<Rightarrow> True | _ \<Rightarrow> False" 181 182context 183notes [[function_internals =true]] 184begin 185 186fun is_cnode_cap :: "cap \<Rightarrow> bool" 187where 188 "is_cnode_cap (CNodeCap _ _ _) = True" 189| "is_cnode_cap _ = False" 190 191fun is_thread_cap :: "cap \<Rightarrow> bool" 192where 193 "is_thread_cap (ThreadCap _) = True" 194| "is_thread_cap _ = False" 195 196fun is_domain_cap :: "cap \<Rightarrow> bool" 197where 198 "is_domain_cap DomainCap = True" 199| "is_domain_cap _ = False" 200 201fun is_untyped_cap :: "cap \<Rightarrow> bool" 202where 203 "is_untyped_cap (UntypedCap _ _ _ _) = True" 204| "is_untyped_cap _ = False" 205 206fun is_ep_cap :: "cap \<Rightarrow> bool" 207where 208 "is_ep_cap (EndpointCap _ _ _) = True" 209| "is_ep_cap _ = False" 210 211fun is_ntfn_cap :: "cap \<Rightarrow> bool" 212where 213 "is_ntfn_cap (NotificationCap _ _ _) = True" 214| "is_ntfn_cap _ = False" 215 216primrec (nonexhaustive) 217 cap_rights :: "cap \<Rightarrow> cap_rights" 218where 219 "cap_rights (EndpointCap _ _ cr) = cr" 220| "cap_rights (NotificationCap _ _ cr) = cr" 221| "cap_rights (ReplyCap _ _ cr) = cr" 222| "cap_rights (ArchObjectCap acap) = acap_rights acap" 223end 224 225text \<open>Various update functions for cap data common to various kinds of 226cap are defined here.\<close> 227definition 228 cap_rights_update :: "cap_rights \<Rightarrow> cap \<Rightarrow> cap" where 229 "cap_rights_update cr' cap \<equiv> 230 case cap of 231 EndpointCap oref badge cr \<Rightarrow> EndpointCap oref badge cr' 232 | NotificationCap oref badge cr 233 \<Rightarrow> NotificationCap oref badge (cr' - {AllowGrant, AllowGrantReply}) 234 | ReplyCap t m cr \<Rightarrow> ReplyCap t m (cr' - {AllowRead, AllowGrantReply} \<union> {AllowWrite}) 235 | ArchObjectCap acap \<Rightarrow> ArchObjectCap (acap_rights_update cr' acap) 236 | _ \<Rightarrow> cap" 237 238definition 239 badge_update :: "badge \<Rightarrow> cap \<Rightarrow> cap" where 240 "badge_update data cap \<equiv> 241 case cap of 242 EndpointCap oref badge cr \<Rightarrow> EndpointCap oref (data && mask badge_bits) cr 243 | NotificationCap oref badge cr \<Rightarrow> NotificationCap oref (data && mask badge_bits) cr 244 | _ \<Rightarrow> cap" 245 246 247definition 248 mask_cap :: "cap_rights \<Rightarrow> cap \<Rightarrow> cap" where 249 "mask_cap rights cap \<equiv> cap_rights_update (cap_rights cap \<inter> rights) cap" 250 251section \<open>Message Info\<close> 252 253text \<open>The message info is the first thing interpreted on a user system call 254and determines the structure of the message the user thread is sending either to 255another user or to a system service. It is also passed to user threads receiving 256a message to indicate the structure of the message they have received. The 257@{text mi_length} parameter is the number of data words in the body of the 258message. The @{text mi_extra_caps} parameter is the number of caps to be passed 259together with the message. The @{text mi_caps_unwrapped} parameter is a bitmask 260allowing threads receiving a message to determine how extra capabilities were 261transferred. The @{text mi_label} parameter is transferred directly from sender 262to receiver as part of the message. 263\<close> 264 265datatype message_info = 266 MI (mi_length: length_type) 267 (mi_extra_caps: length_type) 268 (mi_caps_unwrapped: data) 269 (mi_label: msg_label) 270 271text \<open>Message infos are encoded to or decoded from a data word.\<close> 272primrec 273 message_info_to_data :: "message_info \<Rightarrow> data" 274where 275 "message_info_to_data (MI len exc unw mlabel) = 276 (let 277 extra = exc << 7; 278 unwrapped = unw << 9; 279 label = mlabel << 12 280 in 281 label || extra || unwrapped || len)" 282 283definition 284 data_to_message_info :: "data \<Rightarrow> message_info" 285where 286 "data_to_message_info w \<equiv> 287 MI (let v = w && mask 7 in if v > 120 then 120 else v) 288 ((w >> 7) && mask 2) 289 ((w >> 9) && mask 3) 290 ((w >> 12) && mask msg_label_bits)" 291 292section \<open>Kernel Objects\<close> 293 294text \<open>Endpoints are synchronous points of communication for threads. At any 295time an endpoint may contain a queue of threads waiting to send, a queue of 296threads waiting to receive or be idle. Whenever threads would be waiting to 297send and receive simultaneously messages are transferred immediately. 298\<close> 299 300datatype endpoint 301 = IdleEP 302 | SendEP "obj_ref list" 303 | RecvEP "obj_ref list" 304 305text \<open>Notifications are sets of binary semaphores (stored in the 306\emph{badge word}). Unlike endpoints, threads may choose to block waiting to 307receive, but not to send.\<close> 308 309datatype ntfn 310 = IdleNtfn 311 | WaitingNtfn "obj_ref list" 312 | ActiveNtfn badge 313 314record notification = 315 ntfn_obj :: ntfn 316 ntfn_bound_tcb :: "obj_ref option" 317 318 319definition 320 default_ep :: endpoint where 321 "default_ep \<equiv> IdleEP" 322 323definition 324 default_ntfn :: ntfn where 325 "default_ntfn \<equiv> IdleNtfn" 326 327definition 328 default_notification :: notification where 329 "default_notification \<equiv> \<lparr> 330 ntfn_obj = default_ntfn, 331 ntfn_bound_tcb = None \<rparr>" 332 333 334text \<open>Thread Control Blocks are the in-kernel representation of a thread. 335 336Threads which can execute are either in the Running state for normal execution, 337in the Restart state if their last operation has not completed yet or in the 338IdleThreadState for the unique system idle thread. Threads can also be blocked 339waiting for any of the different kinds of system messages. The Inactive state 340indicates that the TCB is not currently used by a running thread. 341 342TCBs also contain some special-purpose capability slots. The CTable slot is a 343capability to a CNode through which the thread accesses capabilities with which 344to perform system calls. The VTable slot is a capability to a virtual address 345space (an architecture-specific capability type) in which the thread runs. If 346the thread has issued a Reply cap to another thread and is awaiting a reply, 347that cap will have a "master" Reply cap as its parent in the Reply slot. The 348Caller slot is used to initially store any Reply cap issued to this thread. The 349IPCFrame slot stores a capability to a memory frame (an architecture-specific 350capability type) through which messages will be sent and received. 351 352If the thread has encountered a fault and is waiting to send it to its 353supervisor the fault is stored in @{text tcb_fault}. The user register file is 354stored in @{text tcb_context}, the pointer to the cap in the IPCFrame slot in 355@{text tcb_ipc_buffer} and the identity of the Endpoint cap through which faults 356are to be sent in @{text tcb_fault_handler}. 357\<close> 358 359record sender_payload = 360 sender_badge :: badge 361 sender_can_grant :: bool 362 sender_can_grant_reply :: bool 363 sender_is_call :: bool 364 365record receiver_payload = 366 receiver_can_grant :: bool 367 368datatype thread_state 369 = Running 370 | Inactive 371 | Restart 372 | BlockedOnReceive obj_ref receiver_payload 373 | BlockedOnSend obj_ref sender_payload 374 | BlockedOnReply 375 | BlockedOnNotification obj_ref 376 | IdleThreadState 377 378type_synonym priority = word8 379 380record tcb = 381 tcb_ctable :: cap 382 tcb_vtable :: cap 383 tcb_reply :: cap 384 tcb_caller :: cap 385 tcb_ipcframe :: cap 386 tcb_state :: thread_state 387 tcb_fault_handler :: cap_ref 388 tcb_ipc_buffer :: vspace_ref 389 tcb_fault :: "fault option" 390 tcb_bound_notification :: "obj_ref option" 391 tcb_mcpriority :: priority 392 tcb_arch :: arch_tcb (* arch_tcb must have a field for user context *) 393 394 395text \<open>Determines whether a thread in a given state may be scheduled.\<close> 396primrec 397 runnable :: "Structures_A.thread_state \<Rightarrow> bool" 398where 399 "runnable (Running) = True" 400| "runnable (Inactive) = False" 401| "runnable (Restart) = True" 402| "runnable (BlockedOnReceive x y) = False" 403| "runnable (BlockedOnSend x y) = False" 404| "runnable (BlockedOnNotification x) = False" 405| "runnable (IdleThreadState) = False" 406| "runnable (BlockedOnReply) = False" 407 408 409definition 410 default_tcb :: tcb where 411 "default_tcb \<equiv> \<lparr> 412 tcb_ctable = NullCap, 413 tcb_vtable = NullCap, 414 tcb_reply = NullCap, 415 tcb_caller = NullCap, 416 tcb_ipcframe = NullCap, 417 tcb_state = Inactive, 418 tcb_fault_handler = to_bl (0::machine_word), 419 tcb_ipc_buffer = 0, 420 tcb_fault = None, 421 tcb_bound_notification = None, 422 tcb_mcpriority = minBound, 423 tcb_arch = default_arch_tcb\<rparr>" 424 425text \<open> 426All kernel objects are CNodes, TCBs, Endpoints, Notifications or architecture 427specific. 428\<close> 429datatype kernel_object 430 = CNode nat cnode_contents \<comment> \<open>size in bits, and contents\<close> 431 | TCB tcb 432 | Endpoint endpoint 433 | Notification notification 434 | ArchObj (the_arch_obj: arch_kernel_obj) 435 436lemmas kernel_object_cases = 437 kernel_object.induct[where kernel_object=x and P="\<lambda>x'. x = x' \<longrightarrow> P x'" for x P, simplified, rule_format] 438 439lemmas kernel_object_cases_asm = 440kernel_object.induct[where kernel_object=x and P="\<lambda>x'. x = x' \<longrightarrow> P x' \<longrightarrow> R" for P R x, 441 simplified, rule_format, rotated -1] 442 443definition aobj_of :: "kernel_object \<Rightarrow> arch_kernel_obj option" 444 where 445 "aobj_of ko \<equiv> case ko of ArchObj aobj \<Rightarrow> Some aobj | _ \<Rightarrow> None" 446 447text \<open>Checks whether a cnode's contents are well-formed.\<close> 448 449definition 450 well_formed_cnode_n :: "nat \<Rightarrow> cnode_contents \<Rightarrow> bool" where 451 "well_formed_cnode_n n \<equiv> \<lambda>cs. dom cs = {x. length x = n}" 452 453primrec 454 obj_bits :: "kernel_object \<Rightarrow> nat" 455where 456 "obj_bits (CNode sz cs) = cte_level_bits + sz" 457| "obj_bits (TCB t) = tcb_bits" 458| "obj_bits (Endpoint ep) = endpoint_bits" 459| "obj_bits (Notification ntfn) = ntfn_bits" 460| "obj_bits (ArchObj ao) = arch_kobj_size ao" 461 462primrec (nonexhaustive) 463 obj_size :: "cap \<Rightarrow> machine_word" 464where 465 "obj_size NullCap = 0" 466| "obj_size (UntypedCap dev r bits f) = 1 << bits" 467| "obj_size (EndpointCap r b R) = 1 << obj_bits (Endpoint undefined)" 468| "obj_size (NotificationCap r b R) = 1 << obj_bits (Notification undefined)" 469| "obj_size (CNodeCap r bits g) = 1 << (cte_level_bits + bits)" 470| "obj_size (ThreadCap r) = 1 << obj_bits (TCB undefined)" 471| "obj_size (Zombie r zb n) = (case zb of None \<Rightarrow> 1 << obj_bits (TCB undefined) 472 | Some n \<Rightarrow> 1 << (cte_level_bits + n))" 473| "obj_size (ArchObjectCap a) = 1 << arch_obj_size a" 474 475 476text \<open>Object types:\<close> 477 478datatype a_type = 479 ATCB 480 | AEndpoint 481 | ANTFN 482 | ACapTable nat 483 | AGarbage nat \<comment> \<open>number of bytes of garbage\<close> 484 | AArch aa_type 485 486definition 487 a_type :: "kernel_object \<Rightarrow> a_type" 488where 489 "a_type ob \<equiv> case ob of 490 CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace 491 then ACapTable sz else AGarbage (cte_level_bits + sz) 492 | TCB tcb \<Rightarrow> ATCB 493 | Endpoint endpoint \<Rightarrow> AEndpoint 494 | Notification notification \<Rightarrow> ANTFN 495 | ArchObj ao \<Rightarrow> AArch (aa_type ao)" 496 497 498section \<open>Kernel State\<close> 499 500text \<open>The kernel's heap is a partial function containing kernel objects.\<close> 501type_synonym kheap = "obj_ref \<Rightarrow> kernel_object option" 502 503text \<open> 504Capabilities are created either by cloning an existing capability or by creating 505a subordinate capability from it. This results in a capability derivation tree 506or CDT. The kernel provides a Revoke operation which deletes all capabilities 507derived from one particular capability. To support this, the kernel stores the 508CDT explicitly. It is here stored as a tree, a partial mapping from 509capability slots to parent capability slots. 510\<close> 511type_synonym cdt = "cslot_ptr \<Rightarrow> cslot_ptr option" 512 513datatype irq_state = 514 IRQInactive 515 | IRQSignal 516 | IRQTimer 517 | IRQReserved 518 519text \<open>The kernel state includes a heap, a capability derivation tree 520(CDT), a bitmap used to determine if a capability is the original 521capability to that object, a pointer to the current thread, a pointer 522to the system idle thread, the state of the underlying machine, 523per-irq pointers to cnodes (each containing one notification through which 524interrupts are delivered), an array recording which 525interrupts are used for which purpose, and the state of the 526architecture-specific kernel module. 527 528Note: for each irq, @{text "interrupt_irq_node irq"} points to a cnode which 529can contain the notification cap through which interrupts are delivered. In 530C, this all lives in a single array. In the abstract spec though, to prove 531security, we can't have a single object accessible by everyone. Hence the need 532to separate irq handlers. 533\<close> 534record abstract_state = 535 kheap :: kheap 536 cdt :: cdt 537 is_original_cap :: "cslot_ptr \<Rightarrow> bool" 538 cur_thread :: obj_ref 539 idle_thread :: obj_ref 540 machine_state :: machine_state 541 interrupt_irq_node :: "irq \<Rightarrow> obj_ref" 542 interrupt_states :: "irq \<Rightarrow> irq_state" 543 arch_state :: arch_state 544 545text \<open>The following record extends the abstract kernel state with extra 546state of type @{typ "'a"}. The specification operates over states of 547this extended type. By choosing an appropriate concrete type for @{typ "'a"} 548we may obtain different \emph{instantiations} of the kernel specifications 549at differing levels of abstraction. See \autoref{c:ext-spec} for further 550information. 551\<close> 552record 'a state = abstract_state + exst :: 'a 553 554section \<open>Helper functions\<close> 555 556text \<open>This wrapper lifts monadic operations on the underlying machine state to 557monadic operations on the kernel state.\<close> 558definition 559 do_machine_op :: "(machine_state, 'a) nondet_monad \<Rightarrow> ('z state, 'a) nondet_monad" 560where 561 "do_machine_op mop \<equiv> do 562 ms \<leftarrow> gets machine_state; 563 (r, ms') \<leftarrow> select_f (mop ms); 564 modify (\<lambda>state. state \<lparr> machine_state := ms' \<rparr>); 565 return r 566 od" 567 568text \<open>This function generates the cnode indices used when addressing the 569capability slots within a TCB. 570\<close> 571definition 572 tcb_cnode_index :: "nat \<Rightarrow> cnode_index" where 573 "tcb_cnode_index n \<equiv> to_bl (of_nat n :: 3 word)" 574 575text \<open>Zombie capabilities store the bit size of the CNode cap they were 576created from or None if they were created from a TCB cap. This function 577decodes the bit-length of cnode indices into the relevant kernel objects. 578\<close> 579definition 580 zombie_cte_bits :: "nat option \<Rightarrow> nat" where 581 "zombie_cte_bits N \<equiv> case N of Some n \<Rightarrow> n | None \<Rightarrow> 3" 582 583lemma zombie_cte_bits_simps[simp]: 584 "zombie_cte_bits (Some n) = n" 585 "zombie_cte_bits None = 3" 586 by (simp add: zombie_cte_bits_def)+ 587 588text \<open>The first capability slot of the relevant kernel object.\<close> 589primrec (nonexhaustive) 590 first_cslot_of :: "cap \<Rightarrow> cslot_ptr" 591where 592 "first_cslot_of (ThreadCap oref) = (oref, tcb_cnode_index 0)" 593| "first_cslot_of (CNodeCap oref bits g) = (oref, replicate bits False)" 594| "first_cslot_of (Zombie oref bits n) = (oref, replicate (zombie_cte_bits bits) False)" 595 596text \<open>The set of all objects referenced by a capability.\<close> 597primrec 598 obj_refs :: "cap \<Rightarrow> obj_ref set" 599where 600 "obj_refs NullCap = {}" 601| "obj_refs (ReplyCap r m cr) = {}" 602| "obj_refs IRQControlCap = {}" 603| "obj_refs (IRQHandlerCap irq) = {}" 604| "obj_refs (UntypedCap dev r s f) = {}" 605| "obj_refs (CNodeCap r bits guard) = {r}" 606| "obj_refs (EndpointCap r b cr) = {r}" 607| "obj_refs (NotificationCap r b cr) = {r}" 608| "obj_refs (ThreadCap r) = {r}" 609| "obj_refs DomainCap = {}" 610| "obj_refs (Zombie ptr b n) = {ptr}" 611| "obj_refs (ArchObjectCap x) = set_option (aobj_ref x)" 612 613text \<open> 614 The partial definition below is sometimes easier to work with. 615 It also provides cases for UntypedCap and ReplyCap which are not 616 true object references in the sense of the other caps. 617\<close> 618primrec (nonexhaustive) 619 obj_ref_of :: "cap \<Rightarrow> obj_ref" 620where 621 "obj_ref_of (UntypedCap dev r s f) = r" 622| "obj_ref_of (ReplyCap r m cr) = r" 623| "obj_ref_of (CNodeCap r bits guard) = r" 624| "obj_ref_of (EndpointCap r b cr) = r" 625| "obj_ref_of (NotificationCap r b cr) = r" 626| "obj_ref_of (ThreadCap r) = r" 627| "obj_ref_of (Zombie ptr b n) = ptr" 628| "obj_ref_of (ArchObjectCap x) = the (aobj_ref x)" 629 630primrec (nonexhaustive) 631 cap_bits_untyped :: "cap \<Rightarrow> nat" 632where 633 "cap_bits_untyped (UntypedCap dev r s f) = s" 634 635definition tcb_cnode_map :: "tcb \<Rightarrow> cnode_index \<Rightarrow> cap option" 636 where 637 "tcb_cnode_map tcb \<equiv> 638 [tcb_cnode_index 0 \<mapsto> tcb_ctable tcb, 639 tcb_cnode_index 1 \<mapsto> tcb_vtable tcb, 640 tcb_cnode_index 2 \<mapsto> tcb_reply tcb, 641 tcb_cnode_index 3 \<mapsto> tcb_caller tcb, 642 tcb_cnode_index 4 \<mapsto> tcb_ipcframe tcb]" 643 644definition cap_of :: "kernel_object \<Rightarrow> cnode_index \<Rightarrow> cap option" 645 where 646 "cap_of kobj \<equiv> case kobj of CNode _ cs \<Rightarrow> cs | TCB tcb \<Rightarrow> tcb_cnode_map tcb | _ \<Rightarrow> Map.empty" 647 648text \<open>The set of all caps contained in a kernel object.\<close> 649 650definition 651 caps_of :: "kernel_object \<Rightarrow> cap set" where 652 "caps_of kobj \<equiv> ran (cap_of kobj)" 653 654section "Cap transfers" 655 656record captransfer = 657 ct_receive_root :: cap_ref 658 ct_receive_index :: cap_ref 659 ct_receive_depth :: data 660 661text \<open>A thread's IPC buffer capability must be to a page that is capable of 662containing the IPC buffer without the end of the buffer spilling into another 663page.\<close> 664definition cap_transfer_data_size :: nat 665 where 666 "cap_transfer_data_size \<equiv> 3" 667 668definition msg_max_length :: nat 669 where 670 "msg_max_length \<equiv> 120" 671 672definition msg_max_extra_caps :: nat 673 where 674 "msg_max_extra_caps \<equiv> 3" 675 676definition max_ipc_length :: nat 677 where 678 "max_ipc_length \<equiv> cap_transfer_data_size + msg_max_length + msg_max_extra_caps + 2" 679 680definition msg_align_bits :: nat 681 where 682 "msg_align_bits \<equiv> word_size_bits + (LEAST n. max_ipc_length \<le> 2 ^ n)" 683 684lemma msg_align_bits': 685 "msg_align_bits = word_size_bits + 7" 686proof - 687 have "(LEAST n. (cap_transfer_data_size + msg_max_length + msg_max_extra_caps + 2) \<le> 2 ^ n) = 7" 688 proof (rule Least_equality) 689 show "(cap_transfer_data_size + msg_max_length + msg_max_extra_caps + 2) \<le> 2 ^ 7" 690 by (simp add: cap_transfer_data_size_def msg_max_length_def msg_max_extra_caps_def) 691 next 692 fix y 693 assume "(cap_transfer_data_size + msg_max_length + msg_max_extra_caps + 2) \<le> 2 ^ y" 694 hence "(2 :: nat) ^ 7 \<le> 2 ^ y" 695 by (simp add: cap_transfer_data_size_def msg_max_length_def msg_max_extra_caps_def) 696 thus "7 \<le> y" 697 by (rule power_le_imp_le_exp [rotated], simp) 698 qed 699 thus ?thesis unfolding msg_align_bits_def max_ipc_length_def by simp 700qed 701 702end 703