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 ARM */ 21#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT 22static inline int vka_alloc_vcpu(vka_t *vka, vka_object_t *result) 23{ 24 return vka_alloc_object(vka, seL4_ARM_VCPUObject, seL4_ARM_VCPUBits, result); 25} 26 27LEAKY(vcpu) 28#endif 29 30#ifdef CONFIG_TK1_SMMU 31static inline int vka_alloc_io_page_table(vka_t *vka, vka_object_t *result) 32{ 33 return vka_alloc_object(vka, seL4_ARM_IOPageTableObject, seL4_IOPageTableBits, result); 34} 35 36LEAKY(io_page_table) 37#endif 38 39/* 40 * Get the size (in bits) of the untyped memory required to create an object of 41 * the given size. 42 */ 43static inline unsigned long 44vka_arch_get_object_size(seL4_Word objectType) 45{ 46 switch (objectType) { 47 case seL4_ARM_SmallPageObject: 48 return seL4_PageBits; 49 case seL4_ARM_LargePageObject: 50 return seL4_LargePageBits; 51 case seL4_ARM_PageTableObject: 52 return seL4_PageTableBits; 53 case seL4_ARM_PageDirectoryObject: 54 return seL4_PageDirBits; 55 case seL4_ARM_VCPUObject: 56 return seL4_ARM_VCPUBits; 57#ifdef CONFIG_TK1_SMMU 58 case seL4_ARM_IOPageTableObject: 59 return seL4_IOPageTableBits; 60#endif 61 default: 62 return vka_arm_mode_get_object_size(objectType);; 63 } 64} 65 66