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#include <config.h> 12#include <types.h> 13#include <api/failures.h> 14#include <kernel/vspace.h> 15#include <object/structures.h> 16#include <arch/machine.h> 17#include <arch/model/statedata.h> 18#include <arch/object/objecttype.h> 19#include <arch/machine/tlb.h> 20#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT 21#include <arch/object/vcpu.h> 22#endif 23 24bool_t 25Arch_isFrameType(word_t type) 26{ 27 switch (type) { 28 case seL4_ARM_SmallPageObject: 29 return true; 30 case seL4_ARM_LargePageObject: 31 return true; 32 case seL4_ARM_SectionObject: 33 return true; 34 case seL4_ARM_SuperSectionObject: 35 return true; 36 default: 37 return false; 38 } 39} 40 41deriveCap_ret_t 42Arch_deriveCap(cte_t *slot, cap_t cap) 43{ 44 deriveCap_ret_t ret; 45 46 switch (cap_get_capType(cap)) { 47 case cap_page_table_cap: 48 if (cap_page_table_cap_get_capPTIsMapped(cap)) { 49 ret.cap = cap; 50 ret.status = EXCEPTION_NONE; 51 } else { 52 userError("Deriving an unmapped PT cap"); 53 current_syscall_error.type = seL4_IllegalOperation; 54 ret.cap = cap_null_cap_new(); 55 ret.status = EXCEPTION_SYSCALL_ERROR; 56 } 57 return ret; 58 59 case cap_page_directory_cap: 60 if (cap_page_directory_cap_get_capPDIsMapped(cap)) { 61 ret.cap = cap; 62 ret.status = EXCEPTION_NONE; 63 } else { 64 userError("Deriving a PD cap without an assigned ASID"); 65 current_syscall_error.type = seL4_IllegalOperation; 66 ret.cap = cap_null_cap_new(); 67 ret.status = EXCEPTION_SYSCALL_ERROR; 68 } 69 return ret; 70 71 /* This is a deviation from haskell, which has only 72 * one frame cap type on ARM */ 73 case cap_small_frame_cap: 74 ret.cap = cap_small_frame_cap_set_capFMappedASID(cap, asidInvalid); 75 ret.status = EXCEPTION_NONE; 76 return ret; 77 78 case cap_frame_cap: 79 ret.cap = cap_frame_cap_set_capFMappedASID(cap, asidInvalid); 80 ret.status = EXCEPTION_NONE; 81 return ret; 82 83 case cap_asid_control_cap: 84 case cap_asid_pool_cap: 85 ret.cap = cap; 86 ret.status = EXCEPTION_NONE; 87 return ret; 88 89#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT 90 case cap_vcpu_cap: 91 ret.cap = cap; 92 ret.status = EXCEPTION_NONE; 93 return ret; 94#endif 95 96#ifdef CONFIG_ARM_SMMU 97 case cap_io_space_cap: 98 ret.cap = cap; 99 ret.status = EXCEPTION_NONE; 100 return ret; 101 102 case cap_io_page_table_cap: 103 if (cap_io_page_table_cap_get_capIOPTIsMapped(cap)) { 104 ret.cap = cap; 105 ret.status = EXCEPTION_NONE; 106 } else { 107 userError("Deriving a IOPT cap without an assigned IOASID"); 108 current_syscall_error.type = seL4_IllegalOperation; 109 ret.cap = cap_null_cap_new(); 110 ret.status = EXCEPTION_SYSCALL_ERROR; 111 } 112 return ret; 113#endif 114 default: 115 /* This assert has no equivalent in haskell, 116 * as the options are restricted by type */ 117 fail("Invalid arch cap"); 118 } 119} 120 121cap_t CONST 122Arch_updateCapData(bool_t preserve, word_t data, cap_t cap) 123{ 124 return cap; 125} 126 127cap_t CONST 128Arch_maskCapRights(seL4_CapRights_t cap_rights_mask, cap_t cap) 129{ 130 if (cap_get_capType(cap) == cap_small_frame_cap) { 131 vm_rights_t vm_rights; 132 133 vm_rights = vmRightsFromWord( 134 cap_small_frame_cap_get_capFVMRights(cap)); 135 vm_rights = maskVMRights(vm_rights, cap_rights_mask); 136 return cap_small_frame_cap_set_capFVMRights(cap, 137 wordFromVMRights(vm_rights)); 138 } else if (cap_get_capType(cap) == cap_frame_cap) { 139 vm_rights_t vm_rights; 140 141 vm_rights = vmRightsFromWord( 142 cap_frame_cap_get_capFVMRights(cap)); 143 vm_rights = maskVMRights(vm_rights, cap_rights_mask); 144 return cap_frame_cap_set_capFVMRights(cap, 145 wordFromVMRights(vm_rights)); 146 } else { 147 return cap; 148 } 149} 150 151finaliseCap_ret_t 152Arch_finaliseCap(cap_t cap, bool_t final) 153{ 154 finaliseCap_ret_t fc_ret; 155 156 switch (cap_get_capType(cap)) { 157 case cap_asid_pool_cap: 158 if (final) { 159 deleteASIDPool(cap_asid_pool_cap_get_capASIDBase(cap), 160 ASID_POOL_PTR(cap_asid_pool_cap_get_capASIDPool(cap))); 161 } 162 break; 163 164 case cap_page_directory_cap: 165 if (final && cap_page_directory_cap_get_capPDIsMapped(cap)) { 166 deleteASID(cap_page_directory_cap_get_capPDMappedASID(cap), 167 PDE_PTR(cap_page_directory_cap_get_capPDBasePtr(cap))); 168 } 169 break; 170 171 case cap_page_table_cap: 172 if (final && cap_page_table_cap_get_capPTIsMapped(cap)) { 173 unmapPageTable( 174 cap_page_table_cap_get_capPTMappedASID(cap), 175 cap_page_table_cap_get_capPTMappedAddress(cap), 176 PTE_PTR(cap_page_table_cap_get_capPTBasePtr(cap))); 177 } 178 break; 179 180 case cap_small_frame_cap: 181 if (cap_small_frame_cap_get_capFMappedASID(cap)) { 182#ifdef CONFIG_ARM_SMMU 183 if (isIOSpaceFrameCap(cap)) { 184 unmapIOPage(cap); 185 break; 186 } 187#endif 188 189 unmapPage(ARMSmallPage, 190 cap_small_frame_cap_get_capFMappedASID(cap), 191 cap_small_frame_cap_get_capFMappedAddress(cap), 192 (void *)cap_small_frame_cap_get_capFBasePtr(cap)); 193 } 194 break; 195 196 case cap_frame_cap: 197 if (cap_frame_cap_get_capFMappedASID(cap)) { 198#ifdef CONFIG_BENCHMARK_USE_KERNEL_LOG_BUFFER 199 /* If the last cap to the user-level log buffer frame is being revoked, 200 * reset the ksLog so that the kernel doesn't log anymore 201 */ 202 if (unlikely(cap_frame_cap_get_capFSize(cap) == ARMSection)) { 203 if (pptr_to_paddr((void *)cap_frame_cap_get_capFBasePtr(cap)) == ksUserLogBuffer) { 204 ksUserLogBuffer = 0; 205 206 /* Invalidate log page table entries */ 207 clearMemory((void *) armKSGlobalLogPT, BIT(seL4_PageTableBits)); 208 209 cleanCacheRange_PoU((pptr_t) &armKSGlobalLogPT[0], 210 (pptr_t) &armKSGlobalLogPT[0] + BIT(seL4_PageTableBits), 211 addrFromPPtr((void *)&armKSGlobalLogPT[0])); 212 213 for (int idx = 0; idx < BIT(PT_INDEX_BITS); idx++) { 214 invalidateTranslationSingle(KS_LOG_PPTR + (idx << seL4_PageBits)); 215 } 216 217 userError("Log buffer frame is invalidated, kernel can't benchmark anymore"); 218 } 219 } 220#endif /* CONFIG_BENCHMARK_USE_KERNEL_LOG_BUFFER */ 221 222 unmapPage(cap_frame_cap_get_capFSize(cap), 223 cap_frame_cap_get_capFMappedASID(cap), 224 cap_frame_cap_get_capFMappedAddress(cap), 225 (void *)cap_frame_cap_get_capFBasePtr(cap)); 226 } 227 break; 228 229#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT 230 case cap_vcpu_cap: 231 if (final) { 232 vcpu_finalise(VCPU_PTR(cap_vcpu_cap_get_capVCPUPtr(cap))); 233 } 234 break; 235#endif 236 237#ifdef CONFIG_ARM_SMMU 238 case cap_io_space_cap: 239 if (final) { 240 clearIOPageDirectory(cap); 241 } 242 break; 243 244 case cap_io_page_table_cap: 245 if (final && cap_io_page_table_cap_get_capIOPTIsMapped(cap)) { 246 deleteIOPageTable(cap); 247 } 248 break; 249#endif 250 251 default: 252 break; 253 } 254 255 fc_ret.remainder = cap_null_cap_new(); 256 fc_ret.cleanupInfo = cap_null_cap_new(); 257 return fc_ret; 258} 259 260bool_t CONST 261Arch_sameRegionAs(cap_t cap_a, cap_t cap_b) 262{ 263 switch (cap_get_capType(cap_a)) { 264 case cap_small_frame_cap: 265 case cap_frame_cap: 266 if (cap_get_capType(cap_b) == cap_small_frame_cap || 267 cap_get_capType(cap_b) == cap_frame_cap) { 268 word_t botA, botB, topA, topB; 269 botA = generic_frame_cap_get_capFBasePtr(cap_a); 270 botB = generic_frame_cap_get_capFBasePtr(cap_b); 271 topA = botA + MASK (pageBitsForSize(generic_frame_cap_get_capFSize(cap_a))); 272 topB = botB + MASK (pageBitsForSize(generic_frame_cap_get_capFSize(cap_b))) ; 273 return ((botA <= botB) && (topA >= topB) && (botB <= topB)); 274 } 275 break; 276 277 case cap_page_table_cap: 278 if (cap_get_capType(cap_b) == cap_page_table_cap) { 279 return cap_page_table_cap_get_capPTBasePtr(cap_a) == 280 cap_page_table_cap_get_capPTBasePtr(cap_b); 281 } 282 break; 283 284 case cap_page_directory_cap: 285 if (cap_get_capType(cap_b) == cap_page_directory_cap) { 286 return cap_page_directory_cap_get_capPDBasePtr(cap_a) == 287 cap_page_directory_cap_get_capPDBasePtr(cap_b); 288 } 289 break; 290 291 case cap_asid_control_cap: 292 if (cap_get_capType(cap_b) == cap_asid_control_cap) { 293 return true; 294 } 295 break; 296 297 case cap_asid_pool_cap: 298 if (cap_get_capType(cap_b) == cap_asid_pool_cap) { 299 return cap_asid_pool_cap_get_capASIDPool(cap_a) == 300 cap_asid_pool_cap_get_capASIDPool(cap_b); 301 } 302 break; 303 304#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT 305 case cap_vcpu_cap: 306 if (cap_get_capType(cap_b) == cap_vcpu_cap) { 307 return cap_vcpu_cap_get_capVCPUPtr(cap_a) == 308 cap_vcpu_cap_get_capVCPUPtr(cap_b); 309 } 310 break; 311#endif 312 313#ifdef CONFIG_ARM_SMMU 314 case cap_io_space_cap: 315 if (cap_get_capType(cap_b) == cap_io_space_cap) { 316 return cap_io_space_cap_get_capModuleID(cap_a) == 317 cap_io_space_cap_get_capModuleID(cap_b); 318 } 319 break; 320 321 case cap_io_page_table_cap: 322 if (cap_get_capType(cap_b) == cap_io_page_table_cap) { 323 return cap_io_page_table_cap_get_capIOPTBasePtr(cap_a) == 324 cap_io_page_table_cap_get_capIOPTBasePtr(cap_b); 325 } 326 break; 327#endif 328 } 329 330 return false; 331} 332 333bool_t CONST 334Arch_sameObjectAs(cap_t cap_a, cap_t cap_b) 335{ 336 if (cap_get_capType(cap_a) == cap_small_frame_cap) { 337 if (cap_get_capType(cap_b) == cap_small_frame_cap) { 338 return ((cap_small_frame_cap_get_capFBasePtr(cap_a) == 339 cap_small_frame_cap_get_capFBasePtr(cap_b)) && 340 ((cap_small_frame_cap_get_capFIsDevice(cap_a) == 0) == 341 (cap_small_frame_cap_get_capFIsDevice(cap_b) == 0))); 342 } else if (cap_get_capType(cap_b) == cap_frame_cap) { 343 return false; 344 } 345 } 346 if (cap_get_capType(cap_a) == cap_frame_cap) { 347 if (cap_get_capType(cap_b) == cap_frame_cap) { 348 return ((cap_frame_cap_get_capFBasePtr(cap_a) == 349 cap_frame_cap_get_capFBasePtr(cap_b)) && 350 (cap_frame_cap_get_capFSize(cap_a) == 351 cap_frame_cap_get_capFSize(cap_b)) && 352 ((cap_frame_cap_get_capFIsDevice(cap_a) == 0) == 353 (cap_frame_cap_get_capFIsDevice(cap_b) == 0))); 354 } else if (cap_get_capType(cap_b) == cap_small_frame_cap) { 355 return false; 356 } 357 } 358 return Arch_sameRegionAs(cap_a, cap_b); 359} 360 361word_t 362Arch_getObjectSize(word_t t) 363{ 364 switch (t) { 365 case seL4_ARM_SmallPageObject: 366 return ARMSmallPageBits; 367 case seL4_ARM_LargePageObject: 368 return ARMLargePageBits; 369 case seL4_ARM_SectionObject: 370 return ARMSectionBits; 371 case seL4_ARM_SuperSectionObject: 372 return ARMSuperSectionBits; 373 case seL4_ARM_PageTableObject: 374 return PTE_SIZE_BITS + PT_INDEX_BITS; 375 case seL4_ARM_PageDirectoryObject: 376 return PDE_SIZE_BITS + PD_INDEX_BITS; 377#ifdef CONFIG_ARM_SMMU 378 case seL4_ARM_IOPageTableObject: 379 return seL4_IOPageTableBits; 380#endif 381#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT 382 case seL4_ARM_VCPUObject: 383 return VCPU_SIZE_BITS; 384#endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */ 385 default: 386 fail("Invalid object type"); 387 return 0; 388 } 389} 390 391cap_t 392Arch_createObject(object_t t, void *regionBase, word_t userSize, bool_t deviceMemory) 393{ 394 switch (t) { 395 case seL4_ARM_SmallPageObject: 396 if (deviceMemory) { 397 /** AUXUPD: "(True, ptr_retyps 1 398 (Ptr (ptr_val \<acute>regionBase) :: user_data_device_C ptr))" */ 399 /** GHOSTUPD: "(True, gs_new_frames vmpage_size.ARMSmallPage 400 (ptr_val \<acute>regionBase) 401 (unat ARMSmallPageBits))" */ 402 } else { 403 /** AUXUPD: "(True, ptr_retyps 1 404 (Ptr (ptr_val \<acute>regionBase) :: user_data_C ptr))" */ 405 /** GHOSTUPD: "(True, gs_new_frames vmpage_size.ARMSmallPage 406 (ptr_val \<acute>regionBase) 407 (unat ARMSmallPageBits))" */ 408 } 409 return cap_small_frame_cap_new( 410 ASID_LOW(asidInvalid), VMReadWrite, 411 0, !!deviceMemory, 412#ifdef CONFIG_ARM_SMMU 413 0, 414#endif 415 ASID_HIGH(asidInvalid), 416 (word_t)regionBase); 417 418 case seL4_ARM_LargePageObject: 419 if (deviceMemory) { 420 /** AUXUPD: "(True, ptr_retyps 16 421 (Ptr (ptr_val \<acute>regionBase) :: user_data_device_C ptr))" */ 422 /** GHOSTUPD: "(True, gs_new_frames vmpage_size.ARMLargePage 423 (ptr_val \<acute>regionBase) 424 (unat ARMLargePageBits))" */ 425 } else { 426 /** AUXUPD: "(True, ptr_retyps 16 427 (Ptr (ptr_val \<acute>regionBase) :: user_data_C ptr))" */ 428 /** GHOSTUPD: "(True, gs_new_frames vmpage_size.ARMLargePage 429 (ptr_val \<acute>regionBase) 430 (unat ARMLargePageBits))" */ 431 } 432 return cap_frame_cap_new( 433 ARMLargePage, ASID_LOW(asidInvalid), VMReadWrite, 434 0, !!deviceMemory, ASID_HIGH(asidInvalid), 435 (word_t)regionBase); 436 437 case seL4_ARM_SectionObject: 438 if (deviceMemory) { 439#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT 440 /** AUXUPD: "(True, ptr_retyps 512 441 (Ptr (ptr_val \<acute>regionBase) :: user_data_device_C ptr))" */ 442#else /* CONFIG_ARM_HYPERVISOR_SUPPORT */ 443 /** AUXUPD: "(True, ptr_retyps 256 444 (Ptr (ptr_val \<acute>regionBase) :: user_data_device_C ptr))" */ 445#endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */ 446 /** GHOSTUPD: "(True, gs_new_frames vmpage_size.ARMSection 447 (ptr_val \<acute>regionBase) 448 (unat ARMSectionBits))" */ 449 } else { 450#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT 451 /** AUXUPD: "(True, ptr_retyps 512 452 (Ptr (ptr_val \<acute>regionBase) :: user_data_C ptr))" */ 453#else /* CONFIG_ARM_HYPERVISOR_SUPPORT */ 454 /** AUXUPD: "(True, ptr_retyps 256 455 (Ptr (ptr_val \<acute>regionBase) :: user_data_C ptr))" */ 456#endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */ 457 /** GHOSTUPD: "(True, gs_new_frames vmpage_size.ARMSection 458 (ptr_val \<acute>regionBase) 459 (unat ARMSectionBits))" */ 460 } 461 return cap_frame_cap_new( 462 ARMSection, ASID_LOW(asidInvalid), VMReadWrite, 463 0, !!deviceMemory, ASID_HIGH(asidInvalid), 464 (word_t)regionBase); 465 466 case seL4_ARM_SuperSectionObject: 467 if (deviceMemory) { 468#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT 469 /** AUXUPD: "(True, ptr_retyps 8192 470 (Ptr (ptr_val \<acute>regionBase) :: user_data_device_C ptr))" */ 471#else /* CONFIG_ARM_HYPERVISOR_SUPPORT */ 472 /** AUXUPD: "(True, ptr_retyps 4096 473 (Ptr (ptr_val \<acute>regionBase) :: user_data_device_C ptr))" */ 474#endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */ 475 /** GHOSTUPD: "(True, gs_new_frames vmpage_size.ARMSuperSection 476 (ptr_val \<acute>regionBase) 477 (unat ARMSuperSectionBits))" */ 478 } else { 479#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT 480 /** AUXUPD: "(True, ptr_retyps 8192 481 (Ptr (ptr_val \<acute>regionBase) :: user_data_C ptr))" */ 482#else /* CONFIG_ARM_HYPERVISOR_SUPPORT */ 483 /** AUXUPD: "(True, ptr_retyps 4096 484 (Ptr (ptr_val \<acute>regionBase) :: user_data_C ptr))" */ 485#endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */ 486 /** GHOSTUPD: "(True, gs_new_frames vmpage_size.ARMSuperSection 487 (ptr_val \<acute>regionBase) 488 (unat ARMSuperSectionBits))" */ 489 } 490 return cap_frame_cap_new( 491 ARMSuperSection, ASID_LOW(asidInvalid), VMReadWrite, 492 0, !!deviceMemory, ASID_HIGH(asidInvalid), 493 (word_t)regionBase); 494 495 case seL4_ARM_PageTableObject: 496#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT 497 /** AUXUPD: "(True, ptr_retyps 1 498 (Ptr (ptr_val \<acute>regionBase) :: (pte_C[512]) ptr))" */ 499#else /* CONFIG_ARM_HYPERVISOR_SUPPORT */ 500 /** AUXUPD: "(True, ptr_retyps 1 501 (Ptr (ptr_val \<acute>regionBase) :: (pte_C[256]) ptr))" */ 502#endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */ 503 504 return cap_page_table_cap_new(false, asidInvalid, 0, 505 (word_t)regionBase); 506 507 case seL4_ARM_PageDirectoryObject: 508#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT 509 /** AUXUPD: "(True, ptr_retyps 1 510 (Ptr (ptr_val \<acute>regionBase) :: (pde_C[2048]) ptr))" */ 511#else /* CONFIG_ARM_HYPERVISOR_SUPPORT */ 512 /** AUXUPD: "(True, ptr_retyps 1 513 (Ptr (ptr_val \<acute>regionBase) :: (pde_C[4096]) ptr))" */ 514#endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */ 515 copyGlobalMappings((pde_t *)regionBase); 516 cleanCacheRange_PoU((word_t)regionBase, 517 (word_t)regionBase + (1 << (PD_INDEX_BITS + PDE_SIZE_BITS)) - 1, 518 addrFromPPtr(regionBase)); 519 520 return cap_page_directory_cap_new(false, asidInvalid, 521 (word_t)regionBase); 522#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT 523 case seL4_ARM_VCPUObject: 524 /** AUXUPD: "(True, ptr_retyp 525 (Ptr (ptr_val \<acute>regionBase) :: vcpu_C ptr))" */ 526 vcpu_init(VCPU_PTR(regionBase)); 527 return cap_vcpu_cap_new(VCPU_REF(regionBase)); 528#endif 529 530#ifdef CONFIG_ARM_SMMU 531 case seL4_ARM_IOPageTableObject: 532 /* When the untyped was zeroed it was cleaned to the PoU, but the SMMUs 533 * typically pull directly from RAM, so we do a futher clean to RAM here */ 534 cleanCacheRange_RAM((word_t)regionBase, 535 (word_t)regionBase + (1 << seL4_IOPageTableBits) - 1, 536 addrFromPPtr(regionBase)); 537 return cap_io_page_table_cap_new(0, asidInvalid, (word_t)regionBase, 0); 538#endif 539 default: 540 /* 541 * This is a conflation of the haskell error: "Arch.createNewCaps 542 * got an API type" and the case where an invalid object type is 543 * passed (which is impossible in haskell). 544 */ 545 fail("Arch_createObject got an API type or invalid object type"); 546 } 547} 548 549exception_t 550Arch_decodeInvocation(word_t invLabel, word_t length, cptr_t cptr, 551 cte_t *slot, cap_t cap, extra_caps_t excaps, 552 bool_t call, word_t *buffer) 553{ 554 /* The C parser cannot handle a switch statement with only a default 555 * case. So we need to do some gymnastics to remove the switch if 556 * there are no other cases */ 557#if defined(CONFIG_ARM_SMMU) || defined(CONFIG_ARM_HYPERVISOR_SUPPORT) 558 switch (cap_get_capType(cap)) { 559#ifdef CONFIG_ARM_SMMU 560 case cap_io_space_cap: 561 return decodeARMIOSpaceInvocation(invLabel, cap); 562 case cap_io_page_table_cap: 563 return decodeARMIOPTInvocation(invLabel, length, slot, cap, excaps, buffer); 564#endif 565#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT 566 case cap_vcpu_cap: 567 return decodeARMVCPUInvocation(invLabel, length, cptr, slot, cap, excaps, call, buffer); 568#endif /* end of CONFIG_ARM_HYPERVISOR_SUPPORT */ 569 default: 570#else 571{ 572#endif 573 return decodeARMMMUInvocation(invLabel, length, cptr, slot, cap, excaps, buffer); 574} 575} 576 577void 578Arch_prepareThreadDelete(tcb_t * thread) { 579#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT 580 if (thread->tcbArch.tcbVCPU) { 581 dissociateVCPUTCB(thread->tcbArch.tcbVCPU, thread); 582 } 583#else /* CONFIG_ARM_HYPERVISOR_SUPPORT */ 584 /* No action required on ARM. */ 585#endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */ 586} 587 588