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 BSD 2-Clause license. Note that NO WARRANTY is provided. 8 * See "LICENSE_BSD2.txt" for details. 9 * 10 * @TAG(DATA61_BSD) 11 */ 12 13#pragma once 14 15#include <vka/vka.h> 16#include <vka/kobject_t.h> 17#include <utils/util.h> 18#include <vka/sel4_arch/object.h> 19 20/*resource allocation interfaces for virtual machine extensions on x86*/ 21#ifdef CONFIG_VTX 22static inline int vka_alloc_vcpu (vka_t *vka, vka_object_t *result) 23{ 24 return vka_alloc_object(vka, seL4_X86_VCPUObject, seL4_X86_VCPUBits, result); 25} 26 27static inline int vka_alloc_ept_page_directory_pointer_table (vka_t *vka, vka_object_t *result) 28{ 29 return vka_alloc_object(vka, seL4_X86_EPTPDPTObject, seL4_X86_EPTPDPTBits, result); 30} 31 32static inline int vka_alloc_ept_page_directory (vka_t *vka, vka_object_t *result) 33{ 34 return vka_alloc_object(vka, seL4_X86_EPTPDObject, seL4_X86_EPTPDBits, result); 35} 36 37static inline int vka_alloc_ept_page_table (vka_t *vka, vka_object_t *result) 38{ 39 return vka_alloc_object(vka, seL4_X86_EPTPTObject, seL4_X86_EPTPTBits, result); 40} 41static inline int vka_alloc_ept_pdpt(vka_t *vka, vka_object_t *result) 42{ 43 return vka_alloc_object(vka, seL4_X86_EPTPDPTObject, seL4_X86_EPTPDPTBits, result); 44} 45static inline int vka_alloc_ept_pml4(vka_t *vka, vka_object_t *result) 46{ 47 return vka_alloc_object(vka, seL4_X86_EPTPML4Object, seL4_X86_EPTPML4Bits, result); 48} 49#endif /* CONFIG_VTX */ 50 51static inline int vka_alloc_io_page_table(vka_t *vka, vka_object_t *result) 52{ 53 return vka_alloc_object(vka, seL4_X86_IOPageTableObject, seL4_IOPageTableBits, result); 54} 55 56LEAKY(io_page_table) 57 58#ifdef CONFIG_VTX 59LEAKY(vcpu) 60LEAKY(ept_page_directory_pointer_table) 61LEAKY(ept_page_directory) 62LEAKY(ept_page_table) 63LEAKY(ept_pdpt) 64LEAKY(ept_pml4) 65#endif /* CONFIG_VTX */ 66 67static inline unsigned long 68vka_arch_get_object_size(seL4_Word objectType) 69{ 70 switch (objectType) { 71 case seL4_X86_4K: 72 return seL4_PageBits; 73 case seL4_X86_LargePageObject: 74 return seL4_LargePageBits; 75 case seL4_X86_PageTableObject: 76 return seL4_PageTableBits; 77 case seL4_X86_PageDirectoryObject: 78 return seL4_PageDirBits; 79 80#ifdef CONFIG_VTX 81 case seL4_X86_VCPUObject: 82 return seL4_X86_VCPUBits; 83 case seL4_X86_EPTPDPTObject: 84 return seL4_X86_EPTPDPTBits; 85 case seL4_X86_EPTPDObject: 86 return seL4_X86_EPTPDBits; 87 case seL4_X86_EPTPTObject: 88 return seL4_X86_EPTPTBits; 89 case seL4_X86_EPTPML4Object: 90 return seL4_X86_EPTPML4Bits; 91#endif 92 93 case seL4_X86_IOPageTableObject: 94 return seL4_IOPageTableBits; 95 96 default: 97 return vka_x86_mode_get_object_size(objectType); 98 } 99} 100 101