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#ifndef __LIBSEL4_ARCH_TYPES_H
14#define __LIBSEL4_ARCH_TYPES_H
15
16#include <autoconf.h>
17#include <sel4/simple_types.h>
18#include <sel4/sel4_arch/types.h>
19
20typedef seL4_CPtr seL4_X86_ASIDControl;
21typedef seL4_CPtr seL4_X86_ASIDPool;
22typedef seL4_CPtr seL4_X86_IOSpace;
23typedef seL4_CPtr seL4_X86_IOPort;
24typedef seL4_CPtr seL4_X86_IOPortControl;
25typedef seL4_CPtr seL4_X86_Page;
26typedef seL4_CPtr seL4_X86_PDPT;
27typedef seL4_CPtr seL4_X86_PageDirectory;
28typedef seL4_CPtr seL4_X86_PageTable;
29typedef seL4_CPtr seL4_X86_IOPageTable;
30typedef seL4_CPtr seL4_X86_EPTPML4;
31typedef seL4_CPtr seL4_X86_EPTPDPT;
32typedef seL4_CPtr seL4_X86_EPTPD;
33typedef seL4_CPtr seL4_X86_EPTPT;
34typedef seL4_CPtr seL4_X86_VCPU;
35
36typedef enum {
37    seL4_X86_Default_VMAttributes = 0,
38    seL4_X86_WriteBack = 0,
39    seL4_X86_WriteThrough = 1,
40    seL4_X86_CacheDisabled = 2,
41    seL4_X86_Uncacheable = 3,
42    seL4_X86_WriteCombining = 4,
43    SEL4_FORCE_LONG_ENUM(seL4_X86_VMAttributes),
44} seL4_X86_VMAttributes;
45
46typedef struct seL4_VCPUContext_ {
47    seL4_Word eax, ebx, ecx, edx, esi, edi, ebp;
48} seL4_VCPUContext;
49
50#endif
51