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)