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/* Currently MSIs do not go through a vt-d translation by
10 * the kernel, therefore when the user programs an MSI they
11 * need to know how the 'vector' they allocated relates to
12 * the actual vector table. In this case if they allocate
13 * vector X they need to program their MSI to interrupt
14 * vector X + IRQ_OFFSET */
15#define IRQ_OFFSET (0x20 + 16)
16
17/* When allocating vectors for IOAPIC or MSI interrupts,
18 * this represent the valid range */
19#define VECTOR_MIN (0)
20#define VECTOR_MAX (109)
21
22/* Legacy definitions */
23#define MSI_MIN VECTOR_MIN
24#define MSI_MAX VECTOR_MAX
25
26#define seL4_VCPUBits 14
27#define seL4_X86_VCPUBits    seL4_VCPUBits
28
29#define seL4_X86_EPTPML4EntryBits 3
30#define seL4_X86_EPTPML4IndexBits 9
31#define seL4_X86_EPTPML4Bits (seL4_X86_EPTPML4EntryBits + seL4_X86_EPTPML4IndexBits)
32
33#define seL4_X86_EPTPDPTEntryBits 3
34#define seL4_X86_EPTPDPTIndexBits 9
35#define seL4_X86_EPTPDPTBits (seL4_X86_EPTPDPTEntryBits + seL4_X86_EPTPDPTIndexBits)
36
37#define seL4_X86_EPTPDEntryBits   3
38#define seL4_X86_EPTPDIndexBits   9
39#define seL4_X86_EPTPDBits   (seL4_X86_EPTPDEntryBits + seL4_X86_EPTPDIndexBits)
40
41#define seL4_X86_EPTPTEntryBits   3
42#define seL4_X86_EPTPTIndexBits   9
43#define seL4_X86_EPTPTBits   (seL4_X86_EPTPTEntryBits + seL4_X86_EPTPTIndexBits)