1/*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 */
6
7#pragma once
8
9#ifdef HAVE_AUTOCONF
10#include <autoconf.h>
11#endif /* HAVE_AUTOCONF */
12
13typedef enum _object {
14    seL4_X86_4K = seL4_ModeObjectTypeCount,
15    seL4_X86_LargePageObject,
16    seL4_X86_PageTableObject,
17    seL4_X86_PageDirectoryObject,
18#ifdef CONFIG_IOMMU
19    seL4_X86_IOPageTableObject,
20#endif
21#ifdef CONFIG_VTX
22    seL4_X86_VCPUObject,
23    seL4_X86_EPTPML4Object,
24    seL4_X86_EPTPDPTObject,
25    seL4_X86_EPTPDObject,
26    seL4_X86_EPTPTObject,
27#endif
28    seL4_ObjectTypeCount
29} seL4_ArchObjectType;
30typedef seL4_Word object_t;
31
32#ifndef CONFIG_IOMMU
33#define seL4_X86_IOPageTableObject 0xffffff
34#endif
35
36#ifndef CONFIG_VTX
37#define seL4_X86_VCPUObject 0xfffffe
38#define seL4_X86_EPTPML4Object 0xfffffd
39#define seL4_X86_EPTPDPTObject 0xfffffc
40#define seL4_X86_EPTPDObject 0xfffffb
41#define seL4_X86_EPTPTObject 0xfffffa
42#endif
43
44