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