1/* 2 * Copyright 2017, Data61 3 * Commonwealth Scientific and Industrial Research Organisation (CSIRO) 4 * ABN 41 687 119 230. 5 * 6 * This software may be distributed and modified according to the terms of 7 * the GNU General Public License version 2. Note that NO WARRANTY is provided. 8 * See "LICENSE_GPLv2.txt" for details. 9 * 10 * @TAG(DATA61_GPL) 11 */ 12 13#include <config.h> 14#include <types.h> 15#include <api/failures.h> 16#include <kernel/vspace.h> 17#include <object/structures.h> 18#include <arch/machine.h> 19#include <arch/model/statedata.h> 20#include <arch/object/objecttype.h> 21 22bool_t 23Arch_isFrameType(word_t type) 24{ 25 switch (type) { 26 case seL4_ARM_SmallPageObject: 27 return true; 28 case seL4_ARM_LargePageObject: 29 return true; 30 case seL4_ARM_HugePageObject: 31 return true; 32 default: 33 return false; 34 } 35} 36 37deriveCap_ret_t 38Arch_deriveCap(cte_t *slot, cap_t cap) 39{ 40 deriveCap_ret_t ret; 41 42 switch (cap_get_capType(cap)) { 43 case cap_page_global_directory_cap: 44 if (cap_page_global_directory_cap_get_capPGDIsMapped(cap)) { 45 ret.cap = cap; 46 ret.status = EXCEPTION_NONE; 47 } else { 48 userError("Deriving a PDG cap without an assigned ASID"); 49 current_syscall_error.type = seL4_IllegalOperation; 50 ret.cap = cap_null_cap_new(); 51 ret.status = EXCEPTION_SYSCALL_ERROR; 52 } 53 return ret; 54 55 case cap_page_upper_directory_cap: 56 if (cap_page_upper_directory_cap_get_capPUDIsMapped(cap)) { 57 ret.cap = cap; 58 ret.status = EXCEPTION_NONE; 59 } else { 60 userError("Deriving a PUD cap without an assigned ASID"); 61 current_syscall_error.type = seL4_IllegalOperation; 62 ret.cap = cap_null_cap_new(); 63 ret.status = EXCEPTION_SYSCALL_ERROR; 64 } 65 return ret; 66 67 case cap_page_directory_cap: 68 if (cap_page_directory_cap_get_capPDIsMapped(cap)) { 69 ret.cap = cap; 70 ret.status = EXCEPTION_NONE; 71 } else { 72 userError("Deriving a PD cap without an assigned ASID"); 73 current_syscall_error.type = seL4_IllegalOperation; 74 ret.cap = cap_null_cap_new(); 75 ret.status = EXCEPTION_SYSCALL_ERROR; 76 } 77 return ret; 78 79 case cap_page_table_cap: 80 if (cap_page_table_cap_get_capPTIsMapped(cap)) { 81 ret.cap = cap; 82 ret.status = EXCEPTION_NONE; 83 } else { 84 userError("Deriving a PT cap without an assigned ASID"); 85 current_syscall_error.type = seL4_IllegalOperation; 86 ret.cap = cap_null_cap_new(); 87 ret.status = EXCEPTION_SYSCALL_ERROR; 88 } 89 return ret; 90 91 case cap_frame_cap: 92 ret.cap = cap_frame_cap_set_capFMappedASID(cap, asidInvalid); 93 ret.status = EXCEPTION_NONE; 94 return ret; 95 96 case cap_asid_control_cap: 97 case cap_asid_pool_cap: 98 ret.cap = cap; 99 ret.status = EXCEPTION_NONE; 100 return ret; 101 102#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT 103 case cap_vcpu_cap: 104 ret.cap = cap; 105 ret.status = EXCEPTION_NONE; 106 return ret; 107#endif 108 default: 109 /* This assert has no equivalent in haskell, 110 * as the options are restricted by type */ 111 fail("Invalid arch cap"); 112 } 113} 114 115cap_t CONST 116Arch_updateCapData(bool_t preserve, word_t data, cap_t cap) 117{ 118 return cap; 119} 120 121cap_t CONST 122Arch_maskCapRights(seL4_CapRights_t cap_rights_mask, cap_t cap) 123{ 124 if (cap_get_capType(cap) == cap_frame_cap) { 125 vm_rights_t vm_rights; 126 127 vm_rights = vmRightsFromWord(cap_frame_cap_get_capFVMRights(cap)); 128 vm_rights = maskVMRights(vm_rights, cap_rights_mask); 129 130 return cap_frame_cap_set_capFVMRights(cap, wordFromVMRights(vm_rights)); 131 } else { 132 return cap; 133 } 134} 135 136finaliseCap_ret_t 137Arch_finaliseCap(cap_t cap, bool_t final) 138{ 139 finaliseCap_ret_t fc_ret; 140 141 switch (cap_get_capType(cap)) { 142 case cap_asid_pool_cap: 143 if (final) { 144 deleteASIDPool(cap_asid_pool_cap_get_capASIDBase(cap), 145 ASID_POOL_PTR(cap_asid_pool_cap_get_capASIDPool(cap))); 146 } 147 break; 148 149 case cap_page_global_directory_cap: 150 if (final && cap_page_global_directory_cap_get_capPGDIsMapped(cap)) { 151 deleteASID(cap_page_global_directory_cap_get_capPGDMappedASID(cap), 152 PGDE_PTR(cap_page_global_directory_cap_get_capPGDBasePtr(cap))); 153 } 154 break; 155 156 case cap_page_upper_directory_cap: 157 if (final && cap_page_upper_directory_cap_get_capPUDIsMapped(cap)) { 158 unmapPageUpperDirectory(cap_page_upper_directory_cap_get_capPUDMappedASID(cap), 159 cap_page_upper_directory_cap_get_capPUDMappedAddress(cap), 160 PUDE_PTR(cap_page_upper_directory_cap_get_capPUDBasePtr(cap))); 161 } 162 break; 163 164 case cap_page_directory_cap: 165 if (final && cap_page_directory_cap_get_capPDIsMapped(cap)) { 166 unmapPageDirectory(cap_page_directory_cap_get_capPDMappedASID(cap), 167 cap_page_directory_cap_get_capPDMappedAddress(cap), 168 PDE_PTR(cap_page_directory_cap_get_capPDBasePtr(cap))); 169 } 170 break; 171 172 case cap_page_table_cap: 173 if (final && cap_page_table_cap_get_capPTIsMapped(cap)) { 174 unmapPageTable(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_frame_cap: 181 if (cap_frame_cap_get_capFMappedASID(cap)) { 182 unmapPage(cap_frame_cap_get_capFSize(cap), 183 cap_frame_cap_get_capFMappedASID(cap), 184 cap_frame_cap_get_capFMappedAddress(cap), 185 cap_frame_cap_get_capFBasePtr(cap)); 186 } 187 break; 188#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT 189 case cap_vcpu_cap: 190 if (final) { 191 vcpu_finalise(VCPU_PTR(cap_vcpu_cap_get_capVCPUPtr(cap))); 192 } 193 break; 194#endif 195 } 196 197 fc_ret.remainder = cap_null_cap_new(); 198 fc_ret.cleanupInfo = cap_null_cap_new(); 199 return fc_ret; 200} 201 202bool_t CONST Arch_sameRegionAs(cap_t cap_a, cap_t cap_b) 203{ 204 switch (cap_get_capType(cap_a)) { 205 case cap_frame_cap: 206 if (cap_get_capType(cap_b) == cap_frame_cap) { 207 208 word_t botA, botB, topA, topB; 209 botA = cap_frame_cap_get_capFBasePtr(cap_a); 210 botB = cap_frame_cap_get_capFBasePtr(cap_b); 211 topA = botA + MASK(pageBitsForSize(cap_frame_cap_get_capFSize(cap_a))); 212 topB = botB + MASK(pageBitsForSize(cap_frame_cap_get_capFSize(cap_b))) ; 213 return ((botA <= botB) && (topA >= topB) && (botB <= topB)); 214 } 215 break; 216 217 case cap_page_table_cap: 218 if (cap_get_capType(cap_b) == cap_page_table_cap) { 219 return cap_page_table_cap_get_capPTBasePtr(cap_a) == 220 cap_page_table_cap_get_capPTBasePtr(cap_b); 221 } 222 break; 223 224 case cap_page_directory_cap: 225 if (cap_get_capType(cap_b) == cap_page_directory_cap) { 226 return cap_page_directory_cap_get_capPDBasePtr(cap_a) == 227 cap_page_directory_cap_get_capPDBasePtr(cap_b); 228 } 229 break; 230 231 case cap_page_upper_directory_cap: 232 if (cap_get_capType(cap_b) == cap_page_upper_directory_cap) { 233 return cap_page_upper_directory_cap_get_capPUDBasePtr(cap_a) == 234 cap_page_upper_directory_cap_get_capPUDBasePtr(cap_b); 235 } 236 break; 237 238 case cap_page_global_directory_cap: 239 if (cap_get_capType(cap_b) == cap_page_global_directory_cap) { 240 return cap_page_global_directory_cap_get_capPGDBasePtr(cap_a) == 241 cap_page_global_directory_cap_get_capPGDBasePtr(cap_b); 242 } 243 break; 244 245 case cap_asid_control_cap: 246 if (cap_get_capType(cap_b) == cap_asid_control_cap) { 247 return true; 248 } 249 break; 250 251 case cap_asid_pool_cap: 252 if (cap_get_capType(cap_b) == cap_asid_pool_cap) { 253 return cap_asid_pool_cap_get_capASIDPool(cap_a) == 254 cap_asid_pool_cap_get_capASIDPool(cap_b); 255 } 256 break; 257 258#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT 259 case cap_vcpu_cap: 260 if (cap_get_capType(cap_b) == cap_vcpu_cap) { 261 return cap_vcpu_cap_get_capVCPUPtr(cap_a) == 262 cap_vcpu_cap_get_capVCPUPtr(cap_b); 263 } 264#endif 265 } 266 267 return false; 268} 269 270bool_t CONST 271Arch_sameObjectAs(cap_t cap_a, cap_t cap_b) 272{ 273 if (cap_get_capType(cap_a) == cap_frame_cap) { 274 if (cap_get_capType(cap_b) == cap_frame_cap) { 275 return ((cap_frame_cap_get_capFBasePtr(cap_a) == 276 cap_frame_cap_get_capFBasePtr(cap_b)) && 277 (cap_frame_cap_get_capFSize(cap_a) == 278 cap_frame_cap_get_capFSize(cap_b)) && 279 ((cap_frame_cap_get_capFIsDevice(cap_a) == 0) == 280 (cap_frame_cap_get_capFIsDevice(cap_b) == 0))); 281 } 282 } 283 return Arch_sameRegionAs(cap_a, cap_b); 284} 285 286word_t 287Arch_getObjectSize(word_t t) 288{ 289 switch (t) { 290 case seL4_ARM_SmallPageObject: 291 return ARMSmallPageBits; 292 case seL4_ARM_LargePageObject: 293 return ARMLargePageBits; 294 case seL4_ARM_HugePageObject: 295 return ARMHugePageBits; 296 case seL4_ARM_PageTableObject: 297 return seL4_PageTableBits; 298 case seL4_ARM_PageDirectoryObject: 299 return seL4_PageDirBits; 300 case seL4_ARM_PageUpperDirectoryObject: 301 return seL4_PUDBits; 302 case seL4_ARM_PageGlobalDirectoryObject: 303 return seL4_PGDBits; 304#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT 305 case seL4_ARM_VCPUObject: 306 return VCPU_SIZE_BITS; 307#endif 308 default: 309 fail("Invalid object type"); 310 return 0; 311 } 312} 313 314cap_t 315Arch_createObject(object_t t, void *regionBase, word_t userSize, bool_t deviceMemory) 316{ 317 switch (t) { 318 case seL4_ARM_SmallPageObject: 319 return cap_frame_cap_new( 320 asidInvalid, /* capFMappedASID */ 321 (word_t)regionBase, /* capFBasePtr */ 322 ARMSmallPage, /* capFSize */ 323 0, /* capFMappedAddress */ 324 VMReadWrite, /* capFVMRights */ 325 !!deviceMemory /* capFIsDevice */ 326 ); 327 328 case seL4_ARM_LargePageObject: 329 return cap_frame_cap_new( 330 asidInvalid, /* capFMappedASID */ 331 (word_t)regionBase, /* capFBasePtr */ 332 ARMLargePage, /* capFSize */ 333 0, /* capFMappedAddress */ 334 VMReadWrite, /* capFVMRights */ 335 !!deviceMemory /* capFIsDevice */ 336 ); 337 338 case seL4_ARM_HugePageObject: 339 return cap_frame_cap_new( 340 asidInvalid, /* capFMappedASID */ 341 (word_t)regionBase, /* capFBasePtr */ 342 ARMHugePage, /* capFSize */ 343 0, /* capFMappedAddress */ 344 VMReadWrite, /* capFVMRights */ 345 !!deviceMemory /* capFIsDevice */ 346 ); 347 348 case seL4_ARM_PageGlobalDirectoryObject: 349 return cap_page_global_directory_cap_new( 350 asidInvalid, /* capPGDMappedASID */ 351 (word_t)regionBase, /* capPGDBasePtr */ 352 0 /* capPGDIsMapped */ 353 ); 354 355 case seL4_ARM_PageUpperDirectoryObject: 356 return cap_page_upper_directory_cap_new( 357 asidInvalid, /* capPUDMappedASID */ 358 (word_t)regionBase, /* capPUDBasePtr */ 359 0, /* capPUDIsMapped */ 360 0 /* capPUDMappedAddress */ 361 ); 362 363 case seL4_ARM_PageDirectoryObject: 364 return cap_page_directory_cap_new( 365 asidInvalid, /* capPDMappedASID */ 366 (word_t)regionBase, /* capPDBasePtr */ 367 0, /* capPDIsMapped */ 368 0 /* capPDMappedAddress */ 369 ); 370 371 case seL4_ARM_PageTableObject: 372 return cap_page_table_cap_new( 373 asidInvalid, /* capPTMappedASID */ 374 (word_t)regionBase, /* capPTBasePtr */ 375 0, /* capPTIsMapped */ 376 0 /* capPTMappedAddress */ 377 ); 378 379#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT 380 case seL4_ARM_VCPUObject: 381 /** AUXUPD: "(True, ptr_retyp 382 (Ptr (ptr_val \<acute>regionBase) :: vcpu_C ptr))" */ 383 vcpu_init(VCPU_PTR(regionBase)); 384 return cap_vcpu_cap_new(VCPU_REF(regionBase)); 385#endif 386 387 default: 388 fail("Arch_createObject got an API type or invalid object type"); 389 } 390} 391 392exception_t 393Arch_decodeInvocation(word_t label, word_t length, cptr_t cptr, 394 cte_t *slot, cap_t cap, extra_caps_t extraCaps, 395 bool_t call, word_t *buffer) 396{ 397 398 /* The C parser cannot handle a switch statement with only a default 399 * case. So we need to do some gymnastics to remove the switch if 400 * there are no other cases */ 401#if defined(CONFIG_ARM_HYPERVISOR_SUPPORT) 402 switch (cap_get_capType(cap)) { 403#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT 404 case cap_vcpu_cap: 405 return decodeARMVCPUInvocation(label, length, cptr, slot, cap, extraCaps, call, buffer); 406#endif /* end of CONFIG_ARM_HYPERVISOR_SUPPORT */ 407 default: 408#else 409{ 410#endif 411 return decodeARMMMUInvocation(label, length, cptr, slot, cap, extraCaps, buffer); 412} 413} 414 415void 416Arch_prepareThreadDelete(tcb_t * thread) { 417#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT 418 if (thread->tcbArch.tcbVCPU) { 419 dissociateVCPUTCB(thread->tcbArch.tcbVCPU, thread); 420 } 421#endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */ 422} 423