1/* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: GPL-2.0-only 5 */ 6 7#include <config.h> 8#include <types.h> 9#include <api/failures.h> 10#include <kernel/vspace.h> 11#include <object/structures.h> 12#include <arch/machine.h> 13#include <arch/model/statedata.h> 14#include <arch/object/objecttype.h> 15 16bool_t Arch_isFrameType(word_t type) 17{ 18 switch (type) { 19 case seL4_ARM_SmallPageObject: 20 return true; 21 case seL4_ARM_LargePageObject: 22 return true; 23 case seL4_ARM_HugePageObject: 24 return true; 25 default: 26 return false; 27 } 28} 29 30deriveCap_ret_t Arch_deriveCap(cte_t *slot, cap_t cap) 31{ 32 deriveCap_ret_t ret; 33 34 switch (cap_get_capType(cap)) { 35 case cap_page_global_directory_cap: 36 if (cap_page_global_directory_cap_get_capPGDIsMapped(cap)) { 37 ret.cap = cap; 38 ret.status = EXCEPTION_NONE; 39 } else { 40 userError("Deriving a PDG cap without an assigned ASID"); 41 current_syscall_error.type = seL4_IllegalOperation; 42 ret.cap = cap_null_cap_new(); 43 ret.status = EXCEPTION_SYSCALL_ERROR; 44 } 45 return ret; 46 47 case cap_page_upper_directory_cap: 48 if (cap_page_upper_directory_cap_get_capPUDIsMapped(cap)) { 49 ret.cap = cap; 50 ret.status = EXCEPTION_NONE; 51 } else { 52 userError("Deriving a PUD cap without an assigned ASID"); 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 case cap_page_table_cap: 72 if (cap_page_table_cap_get_capPTIsMapped(cap)) { 73 ret.cap = cap; 74 ret.status = EXCEPTION_NONE; 75 } else { 76 userError("Deriving a PT cap without an assigned ASID"); 77 current_syscall_error.type = seL4_IllegalOperation; 78 ret.cap = cap_null_cap_new(); 79 ret.status = EXCEPTION_SYSCALL_ERROR; 80 } 81 return ret; 82 83 case cap_frame_cap: 84 ret.cap = cap_frame_cap_set_capFMappedASID(cap, asidInvalid); 85 ret.status = EXCEPTION_NONE; 86 return ret; 87 88 case cap_asid_control_cap: 89 case cap_asid_pool_cap: 90 ret.cap = cap; 91 ret.status = EXCEPTION_NONE; 92 return ret; 93 94#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT 95 case cap_vcpu_cap: 96 ret.cap = cap; 97 ret.status = EXCEPTION_NONE; 98 return ret; 99#endif 100#ifdef CONFIG_ARM_SMMU 101 case cap_sid_control_cap: 102 case cap_cb_control_cap: 103 ret.cap = cap_null_cap_new(); 104 ret.status = EXCEPTION_NONE; 105 return ret; 106 case cap_sid_cap: 107 case cap_cb_cap: 108 ret.cap = cap; 109 ret.status = EXCEPTION_NONE; 110 return ret; 111#endif 112 default: 113 /* This assert has no equivalent in haskell, 114 * as the options are restricted by type */ 115 fail("Invalid arch cap"); 116 } 117} 118 119cap_t CONST Arch_updateCapData(bool_t preserve, word_t data, cap_t cap) 120{ 121 return cap; 122} 123 124cap_t CONST Arch_maskCapRights(seL4_CapRights_t cap_rights_mask, cap_t cap) 125{ 126 if (cap_get_capType(cap) == cap_frame_cap) { 127 vm_rights_t vm_rights; 128 129 vm_rights = vmRightsFromWord(cap_frame_cap_get_capFVMRights(cap)); 130 vm_rights = maskVMRights(vm_rights, cap_rights_mask); 131 132 return cap_frame_cap_set_capFVMRights(cap, wordFromVMRights(vm_rights)); 133 } else { 134 return cap; 135 } 136} 137 138finaliseCap_ret_t Arch_finaliseCap(cap_t cap, bool_t final) 139{ 140 finaliseCap_ret_t fc_ret; 141 142 switch (cap_get_capType(cap)) { 143 case cap_asid_pool_cap: 144 if (final) { 145 deleteASIDPool(cap_asid_pool_cap_get_capASIDBase(cap), 146 ASID_POOL_PTR(cap_asid_pool_cap_get_capASIDPool(cap))); 147 } 148 break; 149 150 case cap_page_global_directory_cap: 151#ifdef CONFIG_ARM_SMMU 152 if (cap_page_global_directory_cap_get_capPGDMappedCB(cap) != CB_INVALID) { 153 smmu_cb_delete_vspace(cap_page_global_directory_cap_get_capPGDMappedCB(cap), 154 cap_page_global_directory_cap_get_capPGDMappedASID(cap)); 155 } 156#endif 157 if (final && cap_page_global_directory_cap_get_capPGDIsMapped(cap)) { 158 deleteASID(cap_page_global_directory_cap_get_capPGDMappedASID(cap), 159 VSPACE_PTR(cap_page_global_directory_cap_get_capPGDBasePtr(cap))); 160 } 161 break; 162 163 case cap_page_upper_directory_cap: 164#ifdef AARCH64_VSPACE_S2_START_L1 165#ifdef CONFIG_ARM_SMMU 166 if (cap_page_upper_directory_cap_get_capPGDMappedCB(cap) != CB_INVALID) { 167 smmu_cb_delete_vspace(cap_page_upper_directory_cap_get_capPUDMappedCB(cap), 168 cap_page_upper_directory_cap_get_capPUDMappedASID(cap)); 169 } 170#endif 171 if (final && cap_page_upper_directory_cap_get_capPUDIsMapped(cap)) { 172 deleteASID(cap_page_upper_directory_cap_get_capPUDMappedASID(cap), 173 PUDE_PTR(cap_page_upper_directory_cap_get_capPUDBasePtr(cap))); 174 } 175#else 176 if (final && cap_page_upper_directory_cap_get_capPUDIsMapped(cap)) { 177 unmapPageUpperDirectory(cap_page_upper_directory_cap_get_capPUDMappedASID(cap), 178 cap_page_upper_directory_cap_get_capPUDMappedAddress(cap), 179 PUDE_PTR(cap_page_upper_directory_cap_get_capPUDBasePtr(cap))); 180 } 181 182#endif 183 break; 184 185 case cap_page_directory_cap: 186 if (final && cap_page_directory_cap_get_capPDIsMapped(cap)) { 187 unmapPageDirectory(cap_page_directory_cap_get_capPDMappedASID(cap), 188 cap_page_directory_cap_get_capPDMappedAddress(cap), 189 PDE_PTR(cap_page_directory_cap_get_capPDBasePtr(cap))); 190 } 191 break; 192 193 case cap_page_table_cap: 194 if (final && cap_page_table_cap_get_capPTIsMapped(cap)) { 195 unmapPageTable(cap_page_table_cap_get_capPTMappedASID(cap), 196 cap_page_table_cap_get_capPTMappedAddress(cap), 197 PTE_PTR(cap_page_table_cap_get_capPTBasePtr(cap))); 198 } 199 break; 200 201 case cap_frame_cap: 202 if (cap_frame_cap_get_capFMappedASID(cap)) { 203 unmapPage(cap_frame_cap_get_capFSize(cap), 204 cap_frame_cap_get_capFMappedASID(cap), 205 cap_frame_cap_get_capFMappedAddress(cap), 206 cap_frame_cap_get_capFBasePtr(cap)); 207 } 208 break; 209#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT 210 case cap_vcpu_cap: 211 if (final) { 212 vcpu_finalise(VCPU_PTR(cap_vcpu_cap_get_capVCPUPtr(cap))); 213 } 214 break; 215#endif 216#ifdef CONFIG_ARM_SMMU 217 case cap_cb_cap: 218 if (cap_cb_cap_get_capBindSID(cap) != SID_INVALID) { 219 smmu_sid_unbind(cap_cb_cap_get_capBindSID(cap)); 220 } 221 if (final) { 222 smmu_delete_cb(cap); 223 } 224 break; 225 case cap_sid_cap: 226 if (final) { 227 smmu_delete_sid(cap); 228 } 229 break; 230#endif 231 } 232 233 fc_ret.remainder = cap_null_cap_new(); 234 fc_ret.cleanupInfo = cap_null_cap_new(); 235 return fc_ret; 236} 237 238bool_t CONST Arch_sameRegionAs(cap_t cap_a, cap_t cap_b) 239{ 240 switch (cap_get_capType(cap_a)) { 241 case cap_frame_cap: 242 if (cap_get_capType(cap_b) == cap_frame_cap) { 243 244 word_t botA, botB, topA, topB; 245 botA = cap_frame_cap_get_capFBasePtr(cap_a); 246 botB = cap_frame_cap_get_capFBasePtr(cap_b); 247 topA = botA + MASK(pageBitsForSize(cap_frame_cap_get_capFSize(cap_a))); 248 topB = botB + MASK(pageBitsForSize(cap_frame_cap_get_capFSize(cap_b))) ; 249 return ((botA <= botB) && (topA >= topB) && (botB <= topB)); 250 } 251 break; 252 253 case cap_page_table_cap: 254 if (cap_get_capType(cap_b) == cap_page_table_cap) { 255 return cap_page_table_cap_get_capPTBasePtr(cap_a) == 256 cap_page_table_cap_get_capPTBasePtr(cap_b); 257 } 258 break; 259 260 case cap_page_directory_cap: 261 if (cap_get_capType(cap_b) == cap_page_directory_cap) { 262 return cap_page_directory_cap_get_capPDBasePtr(cap_a) == 263 cap_page_directory_cap_get_capPDBasePtr(cap_b); 264 } 265 break; 266 267 case cap_page_upper_directory_cap: 268 if (cap_get_capType(cap_b) == cap_page_upper_directory_cap) { 269 return cap_page_upper_directory_cap_get_capPUDBasePtr(cap_a) == 270 cap_page_upper_directory_cap_get_capPUDBasePtr(cap_b); 271 } 272 break; 273 274 case cap_page_global_directory_cap: 275 if (cap_get_capType(cap_b) == cap_page_global_directory_cap) { 276 return cap_page_global_directory_cap_get_capPGDBasePtr(cap_a) == 277 cap_page_global_directory_cap_get_capPGDBasePtr(cap_b); 278 } 279 break; 280 281 case cap_asid_control_cap: 282 if (cap_get_capType(cap_b) == cap_asid_control_cap) { 283 return true; 284 } 285 break; 286 287 case cap_asid_pool_cap: 288 if (cap_get_capType(cap_b) == cap_asid_pool_cap) { 289 return cap_asid_pool_cap_get_capASIDPool(cap_a) == 290 cap_asid_pool_cap_get_capASIDPool(cap_b); 291 } 292 break; 293 294#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT 295 case cap_vcpu_cap: 296 if (cap_get_capType(cap_b) == cap_vcpu_cap) { 297 return cap_vcpu_cap_get_capVCPUPtr(cap_a) == 298 cap_vcpu_cap_get_capVCPUPtr(cap_b); 299 } 300 break; 301#endif 302#ifdef CONFIG_ARM_SMMU 303 case cap_sid_control_cap: 304 if (cap_get_capType(cap_b) == cap_sid_control_cap || 305 cap_get_capType(cap_b) == cap_sid_cap) { 306 return true; 307 } 308 break; 309 case cap_cb_control_cap: 310 if (cap_get_capType(cap_b) == cap_cb_control_cap || 311 cap_get_capType(cap_b) == cap_cb_cap) { 312 return true; 313 } 314 break; 315 case cap_sid_cap: 316 if (cap_get_capType(cap_b) == cap_sid_cap) { 317 return cap_sid_cap_get_capSID(cap_a) == 318 cap_sid_cap_get_capSID(cap_b); 319 } 320 break; 321 case cap_cb_cap: 322 if (cap_get_capType(cap_b) == cap_cb_cap) { 323 return cap_cb_cap_get_capCB(cap_a) == 324 cap_cb_cap_get_capCB(cap_b); 325 } 326 break; 327#endif 328 } 329 return false; 330} 331 332bool_t CONST Arch_sameObjectAs(cap_t cap_a, cap_t cap_b) 333{ 334 if (cap_get_capType(cap_a) == cap_frame_cap) { 335 if (cap_get_capType(cap_b) == cap_frame_cap) { 336 return ((cap_frame_cap_get_capFBasePtr(cap_a) == 337 cap_frame_cap_get_capFBasePtr(cap_b)) && 338 (cap_frame_cap_get_capFSize(cap_a) == 339 cap_frame_cap_get_capFSize(cap_b)) && 340 ((cap_frame_cap_get_capFIsDevice(cap_a) == 0) == 341 (cap_frame_cap_get_capFIsDevice(cap_b) == 0))); 342 } 343 } 344#ifdef CONFIG_ARM_SMMU 345 if (cap_get_capType(cap_a) == cap_sid_control_cap && 346 cap_get_capType(cap_b) == cap_sid_cap) { 347 return false; 348 } 349 if (cap_get_capType(cap_a) == cap_cb_control_cap && 350 cap_get_capType(cap_b) == cap_cb_cap) { 351 return false; 352 } 353#endif 354 return Arch_sameRegionAs(cap_a, cap_b); 355} 356 357word_t Arch_getObjectSize(word_t t) 358{ 359 switch (t) { 360 case seL4_ARM_SmallPageObject: 361 return ARMSmallPageBits; 362 case seL4_ARM_LargePageObject: 363 return ARMLargePageBits; 364 case seL4_ARM_HugePageObject: 365 return ARMHugePageBits; 366 case seL4_ARM_PageTableObject: 367 return seL4_PageTableBits; 368 case seL4_ARM_PageDirectoryObject: 369 return seL4_PageDirBits; 370 case seL4_ARM_PageUpperDirectoryObject: 371 return seL4_PUDBits; 372#ifndef AARCH64_VSPACE_S2_START_L1 373 case seL4_ARM_PageGlobalDirectoryObject: 374 return seL4_PGDBits; 375#endif 376#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT 377 case seL4_ARM_VCPUObject: 378 return VCPU_SIZE_BITS; 379#endif 380 default: 381 fail("Invalid object type"); 382 return 0; 383 } 384} 385 386cap_t Arch_createObject(object_t t, void *regionBase, word_t userSize, bool_t deviceMemory) 387{ 388 switch (t) { 389 case seL4_ARM_SmallPageObject: 390 return cap_frame_cap_new( 391 asidInvalid, /* capFMappedASID */ 392 (word_t)regionBase, /* capFBasePtr */ 393 ARMSmallPage, /* capFSize */ 394 0, /* capFMappedAddress */ 395 VMReadWrite, /* capFVMRights */ 396 !!deviceMemory /* capFIsDevice */ 397 ); 398 399 case seL4_ARM_LargePageObject: 400 return cap_frame_cap_new( 401 asidInvalid, /* capFMappedASID */ 402 (word_t)regionBase, /* capFBasePtr */ 403 ARMLargePage, /* capFSize */ 404 0, /* capFMappedAddress */ 405 VMReadWrite, /* capFVMRights */ 406 !!deviceMemory /* capFIsDevice */ 407 ); 408 409 case seL4_ARM_HugePageObject: 410 return cap_frame_cap_new( 411 asidInvalid, /* capFMappedASID */ 412 (word_t)regionBase, /* capFBasePtr */ 413 ARMHugePage, /* capFSize */ 414 0, /* capFMappedAddress */ 415 VMReadWrite, /* capFVMRights */ 416 !!deviceMemory /* capFIsDevice */ 417 ); 418#ifndef AARCH64_VSPACE_S2_START_L1 419 case seL4_ARM_PageGlobalDirectoryObject: 420#ifdef CONFIG_ARM_SMMU 421 422 return cap_page_global_directory_cap_new( 423 asidInvalid, /* capPGDMappedASID */ 424 (word_t)regionBase, /* capPGDBasePtr */ 425 0, /* capPGDIsMapped */ 426 CB_INVALID /* capPGDMappedCB */ 427 ); 428#else 429 430 return cap_page_global_directory_cap_new( 431 asidInvalid, /* capPGDMappedASID */ 432 (word_t)regionBase, /* capPGDBasePtr */ 433 0 /* capPGDIsMapped */ 434 ); 435#endif /*!CONFIG_ARM_SMMU*/ 436#endif /*!AARCH64_VSPACE_S2_START_L1*/ 437 case seL4_ARM_PageUpperDirectoryObject: 438 return cap_page_upper_directory_cap_new( 439 asidInvalid, /* capPUDMappedASID */ 440 (word_t)regionBase, /* capPUDBasePtr */ 441 0, /* capPUDIsMapped */ 442 0 /* capPUDMappedAddress */ 443 ); 444 445 case seL4_ARM_PageDirectoryObject: 446 return cap_page_directory_cap_new( 447 asidInvalid, /* capPDMappedASID */ 448 (word_t)regionBase, /* capPDBasePtr */ 449 0, /* capPDIsMapped */ 450 0 /* capPDMappedAddress */ 451 ); 452 453 case seL4_ARM_PageTableObject: 454 return cap_page_table_cap_new( 455 asidInvalid, /* capPTMappedASID */ 456 (word_t)regionBase, /* capPTBasePtr */ 457 0, /* capPTIsMapped */ 458 0 /* capPTMappedAddress */ 459 ); 460 461#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT 462 case seL4_ARM_VCPUObject: 463 /** AUXUPD: "(True, ptr_retyp 464 (Ptr (ptr_val \<acute>regionBase) :: vcpu_C ptr))" */ 465 vcpu_init(VCPU_PTR(regionBase)); 466 return cap_vcpu_cap_new(VCPU_REF(regionBase)); 467#endif 468 469 default: 470 fail("Arch_createObject got an API type or invalid object type"); 471 } 472} 473 474exception_t Arch_decodeInvocation(word_t label, word_t length, cptr_t cptr, 475 cte_t *slot, cap_t cap, extra_caps_t extraCaps, 476 bool_t call, word_t *buffer) 477{ 478 479 /* The C parser cannot handle a switch statement with only a default 480 * case. So we need to do some gymnastics to remove the switch if 481 * there are no other cases */ 482#if defined(CONFIG_ARM_HYPERVISOR_SUPPORT) || defined(CONFIG_ARM_SMMU) 483 switch (cap_get_capType(cap)) { 484#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT 485 case cap_vcpu_cap: 486 return decodeARMVCPUInvocation(label, length, cptr, slot, cap, extraCaps, call, buffer); 487#endif /* end of CONFIG_ARM_HYPERVISOR_SUPPORT */ 488#ifdef CONFIG_ARM_SMMU 489 case cap_sid_control_cap: 490 return decodeARMSIDControlInvocation(label, length, cptr, slot, cap, extraCaps, call, buffer); 491 case cap_sid_cap: 492 return decodeARMSIDInvocation(label, length, cptr, slot, cap, extraCaps, call, buffer); 493 case cap_cb_control_cap: 494 return decodeARMCBControlInvocation(label, length, cptr, slot, cap, extraCaps, call, buffer); 495 case cap_cb_cap: 496 return decodeARMCBInvocation(label, length, cptr, slot, cap, extraCaps, call, buffer); 497#endif /*CONFIG_ARM_SMMU*/ 498 default: 499#else 500{ 501#endif 502 return decodeARMMMUInvocation(label, length, cptr, slot, cap, extraCaps, buffer); 503} 504} 505 506void 507Arch_prepareThreadDelete(tcb_t * thread) { 508#ifdef CONFIG_HAVE_FPU 509 fpuThreadDelete(thread); 510#endif 511 512#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT 513 if (thread->tcbArch.tcbVCPU) { 514 dissociateVCPUTCB(thread->tcbArch.tcbVCPU, thread); 515 } 516#endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */ 517} 518