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_VMENTER
14#define __LIBSEL4_ARCH_VMENTER
15
16/*
17 * When performing a seL4_SysVMEnter seL4 expects certain guest state to be
18 * placed in the message registers. These defines indicates which MRs hold
19 * which values. Whenever a VMEnter returns seL4 will also fill these registers
20 * with the corresponding guest state
21 */
22#define SEL4_VMENTER_CALL_EIP_MR 0
23#define SEL4_VMENTER_CALL_CONTROL_PPC_MR 1
24#define SEL4_VMENTER_CALL_CONTROL_ENTRY_MR 2
25
26/*
27 * In addition to the above message registers, if a VMEnter results in
28 * a fault the following constants describe the contents of the message
29 * registers that contain fault specific information
30 */
31#define SEL4_VMENTER_FAULT_REASON_MR 3
32#define SEL4_VMENTER_FAULT_QUALIFICATION_MR 4
33#define SEL4_VMENTER_FAULT_INSTRUCTION_LEN_MR 5
34#define SEL4_VMENTER_FAULT_GUEST_PHYSICAL_MR 6
35#define SEL4_VMENTER_FAULT_RFLAGS_MR 7
36#define SEL4_VMENTER_FAULT_GUEST_INT_MR 8
37#define SEL4_VMENTER_FAULT_CR3_MR 9
38#define SEL4_VMENTER_FAULT_EAX 10
39#define SEL4_VMENTER_FAULT_EBX 11
40#define SEL4_VMENTER_FAULT_ECX 12
41#define SEL4_VMENTER_FAULT_EDX 13
42#define SEL4_VMENTER_FAULT_ESI 14
43#define SEL4_VMENTER_FAULT_EDI 15
44#define SEL4_VMENTER_FAULT_EBP 16
45
46/*
47 * After performing a seL4_SysVMEnter the msgInfo register is set to indicate
48 * whether a return back to this thread happened due to a fault in the associated
49 * VCPU, or a notification was received on the bound notification object.
50 * If using the seL4_VMEnter wrapper function, then this is the return value
51 *
52 * In the case of a notification the badge register is the received notification
53 * and the message registers are set in the same format as we passed them to
54 * seL4_SysVMEnter
55 *
56 * If a fault is returned then the badge register is empty and the message
57 * format is a combination of the format we passed to seL4_SysVMEnter with
58 * additional registers described with the SEL4_VMENTER_FAULT_ constants
59 */
60#define SEL4_VMENTER_RESULT_FAULT 1
61#define SEL4_VMENTER_RESULT_NOTIF 0
62
63/*
64 * Constants describing the number of message registers returned by the
65 * kernel for each of the return cases of VMEnter
66 */
67#define SEL4_VMENTER_RESULT_FAULT_LEN 17
68#define SEL4_VMENTER_RESULT_NOTIF_LEN 3
69
70#endif /* __LIBSEL4_ARCH_VMENTER */
71