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