1(* 2 * Copyright 2014, General Dynamics C4 Systems 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(GD_GPL) 9 *) 10 11(* 12Higher level functions for manipulating virtual address spaces 13*) 14 15chapter "x64 VSpace Functions" 16 17theory ArchVSpace_A 18imports "../Retype_A" 19begin 20 21context Arch begin global_naming X64_A 22text {* 23 These attributes are always set to @{const False} when pages are mapped. 24*} 25definition 26 "attr_mask = {Global,Dirty,PTAttr Accessed,PTAttr ExecuteDisable}" 27 28definition 29 "attr_mask' = attr_mask \<union> {PAT}" 30 31text {* Save the set of entries that would be inserted into a page table or 32page directory to map various different sizes of frame at a given virtual 33address. *} 34primrec create_mapping_entries :: 35 "paddr \<Rightarrow> vspace_ref \<Rightarrow> vmpage_size \<Rightarrow> vm_rights \<Rightarrow> frame_attrs \<Rightarrow> obj_ref \<Rightarrow> 36 (vm_page_entry * obj_ref,'z::state_ext) se_monad" 37where 38 "create_mapping_entries base vptr X64SmallPage vm_rights attrib pd = 39 doE 40 p \<leftarrow> lookup_error_on_failure False $ lookup_pt_slot pd vptr; 41 returnOk $ (VMPTE (SmallPagePTE base (attrib - attr_mask) vm_rights), p) 42 odE" 43 44| "create_mapping_entries base vptr X64LargePage vm_rights attrib pdpt = 45 doE 46 p \<leftarrow> lookup_error_on_failure False $ lookup_pd_slot pdpt vptr; 47 returnOk $ (VMPDE (LargePagePDE base (attrib - attr_mask) vm_rights), p) 48 odE" 49 50| "create_mapping_entries base vptr X64HugePage vm_rights attrib pml4 = 51 doE 52 p \<leftarrow> lookup_error_on_failure False $ lookup_pdpt_slot pml4 vptr; 53 returnOk $ (VMPDPTE (HugePagePDPTE base (attrib - attr_mask') vm_rights), p) 54 odE" 55 56 57text {* This function checks that given entries are either invalid entries (for unmapping) 58or replace invalid entries (for mapping). *} 59fun ensure_safe_mapping :: 60 "(vm_page_entry * obj_ref) \<Rightarrow> (unit,'z::state_ext) se_monad" 61where 62"ensure_safe_mapping (VMPTE InvalidPTE, _) = returnOk ()" 63| 64"ensure_safe_mapping (VMPDE InvalidPDE, _) = returnOk ()" 65| 66"ensure_safe_mapping (VMPDPTE InvalidPDPTE, _) = returnOk ()" 67| 68"ensure_safe_mapping (VMPTE (SmallPagePTE _ _ _), pt_slot) = returnOk ()" 69| 70"ensure_safe_mapping (VMPDE (LargePagePDE _ _ _), pd_slot) = 71 doE 72 pde \<leftarrow> liftE $ get_pde pd_slot; 73 (case pde of 74 InvalidPDE \<Rightarrow> returnOk () 75 | LargePagePDE _ _ _ \<Rightarrow> returnOk () 76 | _ \<Rightarrow> throwError DeleteFirst) 77 odE" 78| 79"ensure_safe_mapping (VMPDPTE (HugePagePDPTE _ _ _), pdpt_slot) = 80 doE 81 pdpt \<leftarrow> liftE $ get_pdpte pdpt_slot; 82 (case pdpt of 83 InvalidPDPTE \<Rightarrow> returnOk () 84 | HugePagePDPTE _ _ _ \<Rightarrow> returnOk () 85 | _ \<Rightarrow> throwError DeleteFirst) 86 odE" 87| 88"ensure_safe_mapping (VMPDE (PageTablePDE _ _ _), _) = fail" 89| 90"ensure_safe_mapping (VMPDPTE (PageDirectoryPDPTE _ _ _), _) = fail" 91 92text {* Look up a thread's IPC buffer and check that the thread has the right 93authority to read or (in the receiver case) write to it. *} 94definition 95lookup_ipc_buffer :: "bool \<Rightarrow> obj_ref \<Rightarrow> (obj_ref option,'z::state_ext) s_monad" where 96"lookup_ipc_buffer is_receiver thread \<equiv> do 97 buffer_ptr \<leftarrow> thread_get tcb_ipc_buffer thread; 98 buffer_frame_slot \<leftarrow> return (thread, tcb_cnode_index 4); 99 buffer_cap \<leftarrow> get_cap buffer_frame_slot; 100 (case buffer_cap of 101 ArchObjectCap (PageCap _ p R _ vms _) \<Rightarrow> 102 if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not>is_receiver 103 then return $ Some $ p + (buffer_ptr && mask (pageBitsForSize vms)) 104 else return None 105 | _ \<Rightarrow> return None) 106od" 107 108text {* Locate the page directory associated with a given virtual ASID. *} 109definition 110find_vspace_for_asid :: "asid \<Rightarrow> (obj_ref,'z::state_ext) lf_monad" where 111"find_vspace_for_asid asid \<equiv> doE 112 assertE (asid > 0); 113 asid_table \<leftarrow> liftE $ gets (x64_asid_table \<circ> arch_state); 114 pool_ptr \<leftarrow> returnOk (asid_table (asid_high_bits_of asid)); 115 pool \<leftarrow> (case pool_ptr of 116 Some ptr \<Rightarrow> liftE $ get_asid_pool ptr 117 | None \<Rightarrow> throwError InvalidRoot); 118 pml4 \<leftarrow> returnOk (pool (asid_low_bits_of asid)); 119 (case pml4 of 120 Some ptr \<Rightarrow> returnOk ptr 121 | None \<Rightarrow> throwError InvalidRoot) 122odE" 123 124 125text {* Locate the page directory and check that this process succeeds and 126returns a pointer to a real page directory. *} 127definition 128find_vspace_for_asid_assert :: "asid \<Rightarrow> (obj_ref,'z::state_ext) s_monad" where 129"find_vspace_for_asid_assert asid \<equiv> do 130 pml4 \<leftarrow> find_vspace_for_asid asid <catch> K fail; 131 get_pml4 pml4; 132 return pml4 133 od" 134 135text {* Format a VM fault message to be passed to a thread's supervisor after 136it encounters a page fault. *} 137fun 138handle_vm_fault :: "obj_ref \<Rightarrow> vmfault_type \<Rightarrow> (unit,'z::state_ext) f_monad" 139where 140"handle_vm_fault thread fault_type = doE 141 addr \<leftarrow> liftE $ do_machine_op getFaultAddress; 142 fault \<leftarrow> liftE $ as_user thread $ getRegister ErrorRegister; 143 case fault_type of 144 X64DataFault \<Rightarrow> throwError $ ArchFault $ VMFault addr [0, fault && mask 5] 145 | X64InstructionFault \<Rightarrow> throwError $ ArchFault $ VMFault addr [1, fault && mask 5] 146odE" 147 148definition 149 get_current_cr3 :: "(cr3, 'z::state_ext) s_monad" 150where 151 "get_current_cr3 \<equiv> gets (x64_current_cr3 \<circ> arch_state)" 152 153definition 154 set_current_cr3 :: "cr3 \<Rightarrow> (unit,'z::state_ext) s_monad" 155where 156 "set_current_cr3 c \<equiv> 157 modify (\<lambda>s. s \<lparr>arch_state := (arch_state s) \<lparr>x64_current_cr3 := c\<rparr>\<rparr>)" 158 159definition 160 invalidate_page_structure_cache_asid :: "obj_ref \<Rightarrow> asid \<Rightarrow> (unit, 'z::state_ext) s_monad" 161where 162 "invalidate_page_structure_cache_asid vspace asid \<equiv> 163 do_machine_op $ invalidateLocalPageStructureCacheASID vspace (ucast asid)" 164 165definition 166 getCurrentVSpaceRoot :: "(obj_ref, 'z::state_ext) s_monad" 167where 168 "getCurrentVSpaceRoot \<equiv> do 169 cur \<leftarrow> get_current_cr3; 170 return $ cr3_base_address cur 171 od" 172 173definition 174 "cr3_addr_mask \<equiv> mask pml4_shift_bits << asid_bits" 175 176definition 177 make_cr3 :: "obj_ref \<Rightarrow> asid \<Rightarrow> cr3" 178where 179 "make_cr3 vspace asid \<equiv> cr3 (vspace && cr3_addr_mask) asid" 180 181definition 182 set_current_vspace_root :: "obj_ref \<Rightarrow> asid \<Rightarrow> (unit, 'z::state_ext) s_monad" 183where 184 "set_current_vspace_root vspace asid \<equiv> set_current_cr3 $ make_cr3 vspace asid" 185 186text {* Switch into the address space of a given thread or the global address 187space if none is correctly configured. *} 188definition 189 set_vm_root :: "obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad" where 190"set_vm_root tcb \<equiv> do 191 thread_root_slot \<leftarrow> return (tcb, tcb_cnode_index 1); 192 thread_root \<leftarrow> get_cap thread_root_slot; 193 (case thread_root of 194 ArchObjectCap (PML4Cap pml4 (Some asid)) \<Rightarrow> doE 195 pml4' \<leftarrow> find_vspace_for_asid asid; 196 whenE (pml4 \<noteq> pml4') $ throwError InvalidRoot; 197 cur_cr3 \<leftarrow> liftE $ get_current_cr3; 198 whenE (cur_cr3 \<noteq> make_cr3 (addrFromPPtr pml4) asid) $ 199 liftE $ set_current_cr3 $ make_cr3 (addrFromPPtr pml4) asid 200 odE 201 | _ \<Rightarrow> throwError InvalidRoot) <catch> 202 (\<lambda>_. do 203 global_pml4 \<leftarrow> gets (x64_global_pml4 \<circ> arch_state); 204 set_current_vspace_root (addrFromKPPtr global_pml4) 0 205 od) 206od" 207 208text {* Remove virtual to physical mappings in either direction involving this 209virtual ASID. *} 210definition 211hw_asid_invalidate :: "asid \<Rightarrow> obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad" where 212"hw_asid_invalidate asid vspace \<equiv> 213 do_machine_op $ invalidateASID vspace (ucast asid)" 214 215definition 216delete_asid_pool :: "asid \<Rightarrow> obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad" where 217"delete_asid_pool base ptr \<equiv> do 218 assert (asid_low_bits_of base = 0); 219 asid_table \<leftarrow> gets (x64_asid_table \<circ> arch_state); 220 when (asid_table (asid_high_bits_of base) = Some ptr) $ do 221 pool \<leftarrow> get_asid_pool ptr; 222 mapM (\<lambda>offset. (when (pool (ucast offset) \<noteq> None) $ 223 hw_asid_invalidate (base + offset) (the (pool (ucast offset))))) 224 [0 .e. (1 << asid_low_bits) - 1]; 225 asid_table' \<leftarrow> return (asid_table (asid_high_bits_of base:= None)); 226 modify (\<lambda>s. s \<lparr> arch_state := (arch_state s) \<lparr> x64_asid_table := asid_table' \<rparr>\<rparr>); 227 tcb \<leftarrow> gets cur_thread; 228 set_vm_root tcb 229 od 230od" 231 232text {* When deleting a page map level 4 from an ASID pool we must deactivate 233it. *} 234definition 235delete_asid :: "asid \<Rightarrow> obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad" where 236"delete_asid asid pml4 \<equiv> do 237 asid_table \<leftarrow> gets (x64_asid_table \<circ> arch_state); 238 case asid_table (asid_high_bits_of asid) of 239 None \<Rightarrow> return () 240 | Some pool_ptr \<Rightarrow> do 241 pool \<leftarrow> get_asid_pool pool_ptr; 242 when (pool (asid_low_bits_of asid) = Some pml4) $ do 243 hw_asid_invalidate asid pml4; 244 pool' \<leftarrow> return (pool (asid_low_bits_of asid := None)); 245 set_asid_pool pool_ptr pool'; 246 tcb \<leftarrow> gets cur_thread; 247 set_vm_root tcb 248 od 249 od 250od" 251 252definition 253 flush_all :: "obj_ref \<Rightarrow> asid \<Rightarrow> (unit,'z::state_ext) s_monad" where 254 "flush_all vspace asid \<equiv> do_machine_op $ invalidateASID vspace (ucast asid)" 255 256abbreviation 257 flush_pdpt :: "obj_ref \<Rightarrow> asid \<Rightarrow> (unit,'z::state_ext) s_monad" where 258 "flush_pdpt \<equiv> flush_all" 259 260abbreviation 261 flush_pd :: "obj_ref \<Rightarrow> asid \<Rightarrow> (unit,'z::state_ext) s_monad" where 262 "flush_pd \<equiv> flush_all" 263 264text {* Flush mappings associated with a page table. *} 265definition 266flush_table :: "obj_ref \<Rightarrow> vspace_ref \<Rightarrow> obj_ref \<Rightarrow> asid \<Rightarrow> (unit,'z::state_ext) s_monad" where 267"flush_table pml4_ref vptr pt_ref asid \<equiv> do 268 assert (vptr && mask (ptTranslationBits + pageBits) = 0); 269 pt \<leftarrow> get_pt pt_ref; 270 forM_x [0 .e. (-1::9 word)] (\<lambda>index. do 271 pte \<leftarrow> return $ pt index; 272 case pte of 273 InvalidPTE \<Rightarrow> return () 274 | _ \<Rightarrow> do_machine_op $ invalidateTranslationSingleASID (vptr + (ucast index << pageBits)) (ucast asid) 275 od) 276od" 277 278 279text {* Unmap a Page Directory Pointer Table from a PML4. *} 280definition 281unmap_pdpt :: "asid \<Rightarrow> vspace_ref \<Rightarrow> obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad" where 282"unmap_pdpt asid vaddr pdpt \<equiv> doE 283 vspace \<leftarrow> find_vspace_for_asid asid; 284 pm_slot \<leftarrow> returnOk $ lookup_pml4_slot vspace vaddr; 285 pml4e \<leftarrow> liftE $ get_pml4e pm_slot; 286 case pml4e of 287 PDPointerTablePML4E pt' _ _ \<Rightarrow> 288 if pt' = addrFromPPtr pdpt then returnOk () else throwError InvalidRoot 289 | _ \<Rightarrow> throwError InvalidRoot; 290 liftE $ do 291 flush_pdpt vspace asid; 292 store_pml4e pm_slot InvalidPML4E 293 od 294odE <catch> (K $ return ())" 295 296text {* Unmap a Page Directory from a Page Directory Pointer Table. *} 297definition 298unmap_pd :: "asid \<Rightarrow> vspace_ref \<Rightarrow> obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad" where 299"unmap_pd asid vaddr pd \<equiv> doE 300 vspace \<leftarrow> find_vspace_for_asid asid; 301 pdpt_slot \<leftarrow> lookup_pdpt_slot vspace vaddr; 302 pdpte \<leftarrow> liftE $ get_pdpte pdpt_slot; 303 case pdpte of 304 PageDirectoryPDPTE pd' _ _ \<Rightarrow> 305 if pd' = addrFromPPtr pd then returnOk () else throwError InvalidRoot 306 | _ \<Rightarrow> throwError InvalidRoot; 307 liftE $ do 308 flush_pd vspace asid; 309 store_pdpte pdpt_slot InvalidPDPTE; 310 invalidate_page_structure_cache_asid (addrFromPPtr vspace) asid 311 od 312odE <catch> (K $ return ())" 313 314text {* Unmap a page table from its page directory. *} 315definition 316unmap_page_table :: "asid \<Rightarrow> vspace_ref \<Rightarrow> obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad" where 317"unmap_page_table asid vaddr pt \<equiv> doE 318 vspace \<leftarrow> find_vspace_for_asid asid; 319 pd_slot \<leftarrow> lookup_pd_slot vspace vaddr; 320 pde \<leftarrow> liftE $ get_pde pd_slot; 321 case pde of 322 PageTablePDE addr _ _ \<Rightarrow> 323 if addrFromPPtr pt = addr then returnOk () else throwError InvalidRoot 324 | _ \<Rightarrow> throwError InvalidRoot; 325 liftE $ do 326 flush_table vspace vaddr pt asid; 327 store_pde pd_slot InvalidPDE; 328 invalidate_page_structure_cache_asid (addrFromPPtr vspace) asid 329 od 330odE <catch> (K $ return ())" 331 332text {* Check that a given frame is mapped by a given mapping entry. *} 333definition 334check_mapping_pptr :: "machine_word \<Rightarrow> vm_page_entry \<Rightarrow> bool" where 335"check_mapping_pptr pptr entry \<equiv> case entry of 336 VMPTE (SmallPagePTE base _ _) \<Rightarrow> base = addrFromPPtr pptr 337 | VMPDE (LargePagePDE base _ _) \<Rightarrow> base = addrFromPPtr pptr 338 | VMPDPTE (HugePagePDPTE base _ _) \<Rightarrow> base = addrFromPPtr pptr 339 | _ \<Rightarrow> False" 340 341 342text {* Unmap a mapped page if the given mapping details are still current. *} 343definition 344unmap_page :: "vmpage_size \<Rightarrow> asid \<Rightarrow> vspace_ref \<Rightarrow> obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad" where 345"unmap_page pgsz asid vptr pptr \<equiv> doE 346 vspace \<leftarrow> find_vspace_for_asid asid; 347 case pgsz of 348 X64SmallPage \<Rightarrow> doE 349 pt_slot \<leftarrow> lookup_pt_slot vspace vptr; 350 pte \<leftarrow> liftE $ get_pte pt_slot; 351 unlessE (check_mapping_pptr pptr (VMPTE pte)) $ throwError InvalidRoot; 352 liftE $ store_pte pt_slot InvalidPTE 353 odE 354 | X64LargePage \<Rightarrow> doE 355 pd_slot \<leftarrow> lookup_pd_slot vspace vptr; 356 pde \<leftarrow> liftE $ get_pde pd_slot; 357 unlessE (check_mapping_pptr pptr (VMPDE pde)) $ throwError InvalidRoot; 358 liftE $ store_pde pd_slot InvalidPDE 359 odE 360 | X64HugePage \<Rightarrow> doE 361 pdpt_slot \<leftarrow> lookup_pdpt_slot vspace vptr; 362 pdpte \<leftarrow> liftE $ get_pdpte pdpt_slot; 363 unlessE (check_mapping_pptr pptr (VMPDPTE pdpte)) $ throwError InvalidRoot; 364 liftE $ store_pdpte pdpt_slot InvalidPDPTE 365 odE; 366 liftE $ do_machine_op $ invalidateTranslationSingleASID vptr (ucast asid) 367odE <catch> (K $ return ())" 368 369 370text {* Page table structure capabilities cannot be copied until they 371have a virtual ASID and location assigned. This is because they 372cannot have multiple current virtual ASIDs and cannot be shared 373between address spaces or virtual locations. *} 374definition 375 arch_derive_cap :: "arch_cap \<Rightarrow> (cap,'z::state_ext) se_monad" 376where 377 "arch_derive_cap c \<equiv> case c of 378 PageTableCap _ (Some x) \<Rightarrow> returnOk (ArchObjectCap c) 379 | PageTableCap _ None \<Rightarrow> throwError IllegalOperation 380 | PageDirectoryCap _ (Some x) \<Rightarrow> returnOk (ArchObjectCap c) 381 | PageDirectoryCap _ None \<Rightarrow> throwError IllegalOperation 382 | PDPointerTableCap _ (Some x) \<Rightarrow> returnOk (ArchObjectCap c) 383 | PDPointerTableCap _ None \<Rightarrow> throwError IllegalOperation 384 | PML4Cap _ (Some x) \<Rightarrow> returnOk (ArchObjectCap c) 385 | PML4Cap _ None \<Rightarrow> throwError IllegalOperation 386 | PageCap dev r R mt pgs x \<Rightarrow> returnOk $ ArchObjectCap (PageCap dev r R VMNoMap pgs None) 387 | ASIDControlCap \<Rightarrow> returnOk (ArchObjectCap c) 388 | ASIDPoolCap _ _ \<Rightarrow> returnOk (ArchObjectCap c) 389(* FIXME x64-vtd: *) 390(* 391 | IOSpaceCap _ _ \<Rightarrow> returnOk c 392 | IOPageTableCap _ _ _ \<Rightarrow> returnOk c 393*) 394 | IOPortCap _ _ \<Rightarrow> returnOk (ArchObjectCap c) 395 | IOPortControlCap \<Rightarrow> returnOk NullCap" 396 397text {* No user-modifiable data is stored in x64-specific capabilities. *} 398definition 399 arch_update_cap_data :: "bool \<Rightarrow> data \<Rightarrow> arch_cap \<Rightarrow> cap" 400where 401 "arch_update_cap_data preserve data c \<equiv> ArchObjectCap c" 402 403 404text {* Actions that must be taken on finalisation of x64-specific 405capabilities. *} 406definition 407 arch_finalise_cap :: "arch_cap \<Rightarrow> bool \<Rightarrow> (cap \<times> cap,'z::state_ext) s_monad" 408where 409 "arch_finalise_cap c x \<equiv> case (c, x) of 410 (ASIDPoolCap ptr b, True) \<Rightarrow> do 411 delete_asid_pool b ptr; 412 return (NullCap, NullCap) 413 od 414 | (PML4Cap ptr (Some a), True) \<Rightarrow> do 415 delete_asid a ptr; 416 return (NullCap, NullCap) 417 od 418 | (PDPointerTableCap ptr (Some (a,v)), True) \<Rightarrow> do 419 unmap_pdpt a v ptr; 420 return (NullCap, NullCap) 421 od 422 | (PageDirectoryCap ptr (Some (a,v)), True) \<Rightarrow> do 423 unmap_pd a v ptr; 424 return (NullCap, NullCap) 425 od 426 | (PageTableCap ptr (Some (a, v)), True) \<Rightarrow> do 427 unmap_page_table a v ptr; 428 return (NullCap, NullCap) 429 od 430 | (PageCap _ ptr _ _ s (Some (a, v)), _) \<Rightarrow> do 431 unmap_page s a v ptr; 432 return (NullCap, NullCap) 433 od 434 | (IOPortCap f l, True) \<Rightarrow> return (NullCap, (ArchObjectCap (IOPortCap f l))) 435 (* FIXME x64-vtd: IOSpaceCap and IOPageTableCap for arch_finalise_cap *) 436 | _ \<Rightarrow> return (NullCap, NullCap)" 437 438 439 440text {* A thread's virtual address space capability must be to a mapped PML4 (page map level 4) 441to be valid on the x64 architecture. *} 442definition 443 is_valid_vtable_root :: "cap \<Rightarrow> bool" where 444 "is_valid_vtable_root c \<equiv> \<exists>r a. c = ArchObjectCap (PML4Cap r (Some a))" 445 446definition 447check_valid_ipc_buffer :: "vspace_ref \<Rightarrow> cap \<Rightarrow> (unit,'z::state_ext) se_monad" where 448"check_valid_ipc_buffer vptr c \<equiv> case c of 449 (ArchObjectCap (PageCap False _ _ _ _ _)) \<Rightarrow> doE 450 whenE (\<not> is_aligned vptr msg_align_bits) $ throwError AlignmentError; 451 returnOk () 452 odE 453| _ \<Rightarrow> throwError IllegalOperation" 454 455text {* Decode a user argument word describing the kind of VM attributes a 456mapping is to have. *} 457definition 458attribs_from_word :: "machine_word \<Rightarrow> frame_attrs" where 459"attribs_from_word w \<equiv> 460 let V = (if w !!0 then {PTAttr WriteThrough} else {}); 461 V' = (if w!!1 then insert (PTAttr CacheDisabled) V else V) 462 in if w!!2 then insert PAT V' else V'" 463 464 465text {* Update the mapping data saved in a page or page table capability. *} 466definition 467 update_map_data :: "arch_cap \<Rightarrow> (asid \<times> vspace_ref) option \<Rightarrow> vmmap_type option \<Rightarrow> arch_cap" where 468 "update_map_data cap m mt \<equiv> case cap of 469 PageCap dev p R _ sz _ \<Rightarrow> PageCap dev p R (the mt) sz m 470 | PageTableCap p _ \<Rightarrow> PageTableCap p m 471 | PageDirectoryCap p _ \<Rightarrow> PageDirectoryCap p m 472 | PDPointerTableCap p _ \<Rightarrow> PDPointerTableCap p m" 473 474text {* 475 A pointer is inside a user frame if its top bits point to a @{text DataPage}. 476*} 477definition 478 in_user_frame :: "obj_ref \<Rightarrow> 'z::state_ext state \<Rightarrow> bool" where 479 "in_user_frame p s \<equiv> 480 \<exists>sz. kheap s (p && ~~ mask (pageBitsForSize sz)) = 481 Some (ArchObj (DataPage False sz))" 482 483definition 484 fpu_thread_delete :: "obj_ref \<Rightarrow> (unit, 'z::state_ext) s_monad" 485where 486 "fpu_thread_delete thread_ptr \<equiv> do 487 using_fpu \<leftarrow> do_machine_op (nativeThreadUsingFPU thread_ptr); 488 when using_fpu $ do_machine_op (switchFpuOwner 0 0) 489 od" 490 491definition 492 prepare_thread_delete :: "obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad" 493where 494 "prepare_thread_delete thread_ptr \<equiv> fpu_thread_delete thread_ptr" 495 496text {* Make numeric value of @{const msg_align_bits} visible. *} 497lemmas msg_align_bits = msg_align_bits'[unfolded word_size_bits_def, simplified] 498 499end 500end 501