libsel4: fix incorrect seL4_VMEnter() description

SEL4_VMENTER_CALL_CONTROL_ENTRY_MR refers to the
VM Entry Interruption-Information Field of the VMCS [1].
Not the VM-Entry Controls, which are two different things.

[1]: src/arch/x86/object/vcpu.c: vcpu_update_state_sysvmenter()

Signed-off-by: Bill Nguyen <bill.nguyen@student.unsw.edu.au>
This commit is contained in:
Bill Nguyen
2025-12-02 19:34:28 +11:00
committed by Indan Zupancic
parent b0567c4d1c
commit 704f80b9be
3 changed files with 6 additions and 2 deletions

View File

@@ -16,7 +16,7 @@ typedef enum kernel_fault_context {
*/
SEL4_VMENTER_CALL_EIP_MR,
SEL4_VMENTER_CALL_CONTROL_PPC_MR,
SEL4_VMENTER_CALL_CONTROL_ENTRY_MR,
SEL4_VMENTER_CALL_INTERRUPT_INFO_MR,
/*
* In addition to the above message registers, if a VMEnter results in

View File

@@ -30,6 +30,10 @@
#define SEL4_VCPU_FAULT_LABEL SEL4_DEPRECATE_MACRO(seL4_Fault_VCPUFault)
#endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */
#ifdef CONFIG_VTX
#define SEL4_VMENTER_CALL_CONTROL_ENTRY_MR SEL4_DEPRECATE_MACRO(SEL4_VMENTER_CALL_INTERRUPT_INFO_MR)
#endif /* CONFIG_VTX */
typedef seL4_CapRights_t seL4_CapRights SEL4_DEPRECATED("use seL4_CapRights_t");
typedef union {

View File

@@ -335,7 +335,7 @@ seL4_BenchmarkResetAllThreadsUtilisation(void);
* The mapping of hardware register to message register is
* - `SEL4_VMENTER_CALL_EIP_MR` Address to start executing instructions at in the guest mode
* - `SEL4_VMENTER_CALL_CONTROL_PPC_MR` New value for the Primary Processor Based VM Execution Controls
* - `SEL4_VMENTER_CALL_CONTROL_ENTRY_MR` New value for the VM Entry Controls
* - `SEL4_VMENTER_CALL_INTERRUPT_INFO_MR` New value for the VM Entry Interruption-Information
*
* On return these same three message registers will be filled with the values at the point
* that the privileged mode ceased executing. If this function returns with `SEL4_VMENTER_RESULT_FAULT`