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