diff --git a/xen/arch/x86/hvm/vmx/intr.c b/xen/arch/x86/hvm/vmx/intr.c
index 8431937f42..d8387e7215 100644
--- a/xen/arch/x86/hvm/vmx/intr.c
+++ b/xen/arch/x86/hvm/vmx/intr.c
@@ -38,6 +38,7 @@
 #include <asm/hvm/trace.h>
 #include <asm/vm_event.h>
 
+#include "vmcs.h"
 #include "vmx.h"
 #include "vvmx.h"
 
diff --git a/xen/arch/x86/hvm/vmx/vmcs.c b/xen/arch/x86/hvm/vmx/vmcs.c
index 3d0f6be5bb..57e19e8dad 100644
--- a/xen/arch/x86/hvm/vmx/vmcs.c
+++ b/xen/arch/x86/hvm/vmx/vmcs.c
@@ -42,6 +42,7 @@
 #include <asm/tboot.h>
 #include <asm/apic.h>
 
+#include "vmcs.h"
 #include "vmx.h"
 #include "vvmx.h"
 
diff --git a/xen/arch/x86/hvm/vmx/vmcs.h b/xen/arch/x86/hvm/vmx/vmcs.h
new file mode 100644
index 0000000000..c0cca0ce73
--- /dev/null
+++ b/xen/arch/x86/hvm/vmx/vmcs.h
@@ -0,0 +1,100 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+/*
+ * vmcs.h: VMCS related definitions
+ *
+ * Copyright (c) 2004, Intel Corporation.
+ */
+
+#ifndef __X86_HVM_VMX_VMCS_PRIV_H__
+#define __X86_HVM_VMX_VMCS_PRIV_H__
+
+#include <xen/sched.h>
+#include <xen/types.h>
+
+#include <asm/hvm/vmx/vmcs.h>
+
+struct vmcs_struct {
+    uint32_t vmcs_revision_id;
+    unsigned char data [0]; /* vmcs size is read from MSR */
+};
+
+#define _VMX_DOMAIN_PML_ENABLED    0
+#define VMX_DOMAIN_PML_ENABLED     (1ul << _VMX_DOMAIN_PML_ENABLED)
+
+/*
+ * Layout of the MSR bitmap, as interpreted by hardware:
+ *  - *_low  covers MSRs 0 to 0x1fff
+ *  - *_ligh covers MSRs 0xc0000000 to 0xc0001fff
+ */
+struct vmx_msr_bitmap {
+    unsigned long read_low  [0x2000 / BITS_PER_LONG];
+    unsigned long read_high [0x2000 / BITS_PER_LONG];
+    unsigned long write_low [0x2000 / BITS_PER_LONG];
+    unsigned long write_high[0x2000 / BITS_PER_LONG];
+};
+
+#define NR_PML_ENTRIES   512
+
+void vmcs_dump_vcpu(struct vcpu *v);
+int vmx_vmcs_init(void);
+int cf_check vmx_cpu_up_prepare(unsigned int cpu);
+void cf_check vmx_cpu_dead(unsigned int cpu);
+int cf_check vmx_cpu_up(void);
+void cf_check vmx_cpu_down(void);
+
+int vmx_create_vmcs(struct vcpu *v);
+void vmx_destroy_vmcs(struct vcpu *v);
+bool __must_check vmx_vmcs_try_enter(struct vcpu *v);
+void vmx_vmcs_reload(struct vcpu *v);
+
+void vmx_vmcs_switch(paddr_t from, paddr_t to);
+void vmx_set_eoi_exit_bitmap(struct vcpu *v, uint8_t vector);
+void vmx_clear_eoi_exit_bitmap(struct vcpu *v, uint8_t vector);
+bool vmx_msr_is_intercepted(struct vmx_msr_bitmap *msr_bitmap,
+                            unsigned int msr, bool is_write) __nonnull(1);
+void virtual_vmcs_enter(const struct vcpu *);
+void virtual_vmcs_exit(const struct vcpu *);
+u64 virtual_vmcs_vmread(const struct vcpu *, uint32_t encoding);
+enum vmx_insn_errno virtual_vmcs_vmread_safe(const struct vcpu *v,
+                                             uint32_t vmcs_encoding,
+                                             uint64_t *val);
+void virtual_vmcs_vmwrite(const struct vcpu *, uint32_t encoding, uint64_t val);
+enum vmx_insn_errno virtual_vmcs_vmwrite_safe(const struct vcpu *v,
+                                              uint32_t vmcs_encoding,
+                                              uint64_t val);
+
+DECLARE_PER_CPU(bool, vmxon);
+
+bool vmx_vcpu_pml_enabled(const struct vcpu *v);
+int vmx_vcpu_enable_pml(struct vcpu *v);
+void vmx_vcpu_disable_pml(struct vcpu *v);
+void vmx_vcpu_flush_pml_buffer(struct vcpu *v);
+
+static inline int vmx_read_guest_loadonly_msr(
+    const struct vcpu *v, uint32_t msr, uint64_t *val)
+{
+    const struct vmx_msr_entry *ent =
+        vmx_find_msr(v, msr, VMX_MSR_GUEST_LOADONLY);
+
+    if ( !ent )
+    {
+        *val = 0;
+        return -ESRCH;
+    }
+
+    *val = ent->data;
+
+    return 0;
+}
+
+#endif /* __X86_HVM_VMX_VMCS_PRIV_H__ */
+
+/*
+ * Local variables:
+ * mode: C
+ * c-file-style: "BSD"
+ * c-basic-offset: 4
+ * tab-width: 4
+ * indent-tabs-mode: nil
+ * End:
+ */
diff --git a/xen/arch/x86/hvm/vmx/vmx.c b/xen/arch/x86/hvm/vmx/vmx.c
index 73ab4e9816..c5f6902206 100644
--- a/xen/arch/x86/hvm/vmx/vmx.c
+++ b/xen/arch/x86/hvm/vmx/vmx.c
@@ -57,6 +57,7 @@
 #include <public/hvm/ioreq.h>
 
 #include "pi.h"
+#include "vmcs.h"
 #include "vmx.h"
 #include "vvmx.h"
 
diff --git a/xen/arch/x86/hvm/vmx/vvmx.c b/xen/arch/x86/hvm/vmx/vvmx.c
index 0af5411076..d0a6fa2d20 100644
--- a/xen/arch/x86/hvm/vmx/vvmx.c
+++ b/xen/arch/x86/hvm/vmx/vvmx.c
@@ -29,6 +29,7 @@
 #include <asm/hvm/vmx/vvmx.h>
 #include <asm/hvm/nestedhvm.h>
 
+#include "vmcs.h"
 #include "vmx.h"
 #include "vvmx.h"
 
diff --git a/xen/arch/x86/include/asm/hvm/vmx/vmcs.h b/xen/arch/x86/include/asm/hvm/vmx/vmcs.h
index 0a84e74478..47206b1e9d 100644
--- a/xen/arch/x86/include/asm/hvm/vmx/vmcs.h
+++ b/xen/arch/x86/include/asm/hvm/vmx/vmcs.h
@@ -20,22 +20,10 @@
 
 #include <xen/mm.h>
 
-extern void vmcs_dump_vcpu(struct vcpu *v);
-extern int vmx_vmcs_init(void);
-int cf_check vmx_cpu_up_prepare(unsigned int cpu);
-void cf_check vmx_cpu_dead(unsigned int cpu);
-int cf_check vmx_cpu_up(void);
-void cf_check vmx_cpu_down(void);
-
-struct vmcs_struct {
-    u32 vmcs_revision_id;
-    unsigned char data [0]; /* vmcs size is read from MSR */
-};
-
 struct vmx_msr_entry {
-    u32 index;
-    u32 mbz;
-    u64 data;
+    uint32_t index;
+    uint32_t mbz;
+    uint64_t data;
 };
 
 #define EPT_DEFAULT_MT      X86_MT_WB
@@ -49,14 +37,12 @@ struct ept_data {
                      :5,     /* rsvd. */
                      mfn:52;
         };
-        u64 eptp;
+        uint64_t eptp;
     };
     /* Set of PCPUs needing an INVEPT before a VMENTER. */
     cpumask_var_t invalidate;
 };
 
-#define _VMX_DOMAIN_PML_ENABLED    0
-#define VMX_DOMAIN_PML_ENABLED     (1ul << _VMX_DOMAIN_PML_ENABLED)
 struct vmx_domain {
     mfn_t apic_access_mfn;
     /* VMX_DOMAIN_* */
@@ -69,36 +55,22 @@ struct vmx_domain {
     bool exec_sp;
 };
 
-/*
- * Layout of the MSR bitmap, as interpreted by hardware:
- *  - *_low  covers MSRs 0 to 0x1fff
- *  - *_ligh covers MSRs 0xc0000000 to 0xc0001fff
- */
-struct vmx_msr_bitmap {
-    unsigned long read_low  [0x2000 / BITS_PER_LONG];
-    unsigned long read_high [0x2000 / BITS_PER_LONG];
-    unsigned long write_low [0x2000 / BITS_PER_LONG];
-    unsigned long write_high[0x2000 / BITS_PER_LONG];
-};
-
 struct pi_desc {
     DECLARE_BITMAP(pir, X86_NR_VECTORS);
     union {
         struct {
-            u16     on     : 1,  /* bit 256 - Outstanding Notification */
-                    sn     : 1,  /* bit 257 - Suppress Notification */
-                    rsvd_1 : 14; /* bit 271:258 - Reserved */
-            u8      nv;          /* bit 279:272 - Notification Vector */
-            u8      rsvd_2;      /* bit 287:280 - Reserved */
-            u32     ndst;        /* bit 319:288 - Notification Destination */
+            uint16_t   on     : 1,  /* bit 256 - Outstanding Notification */
+                       sn     : 1,  /* bit 257 - Suppress Notification */
+                       rsvd_1 : 14; /* bit 271:258 - Reserved */
+            uint8_t    nv;          /* bit 279:272 - Notification Vector */
+            uint8_t    rsvd_2;      /* bit 287:280 - Reserved */
+            uint32_t   ndst;        /* bit 319:288 - Notification Destination */
         };
-        u64 control;
+        uint64_t control;
     };
-    u32 rsvd[6];
+    uint32_t rsvd[6];
 } __attribute__ ((aligned (64)));
 
-#define NR_PML_ENTRIES   512
-
 struct pi_blocking_vcpu {
     struct list_head     list;
     spinlock_t           *lock;
@@ -123,9 +95,9 @@ struct vmx_vcpu {
     int                  launched;
 
     /* Cache of cpu execution control. */
-    u32                  exec_control;
-    u32                  secondary_exec_control;
-    u32                  exception_bitmap;
+    uint32_t             exec_control;
+    uint32_t             secondary_exec_control;
+    uint32_t             exception_bitmap;
 
     uint64_t             shadow_gs;
     uint64_t             star;
@@ -154,7 +126,7 @@ struct vmx_vcpu {
     unsigned long        host_cr0;
 
     /* Do we need to tolerate a spurious EPT_MISCONFIG VM exit? */
-    bool_t               ept_spurious_misconfig;
+    bool                 ept_spurious_misconfig;
 
     /* Processor Trace configured and enabled for the vcpu. */
     bool                 ipt_active;
@@ -191,12 +163,8 @@ struct vmx_vcpu {
     struct pi_blocking_vcpu pi_blocking;
 };
 
-int vmx_create_vmcs(struct vcpu *v);
-void vmx_destroy_vmcs(struct vcpu *v);
 void vmx_vmcs_enter(struct vcpu *v);
-bool_t __must_check vmx_vmcs_try_enter(struct vcpu *v);
 void vmx_vmcs_exit(struct vcpu *v);
-void vmx_vmcs_reload(struct vcpu *v);
 
 #define CPU_BASED_VIRTUAL_INTR_PENDING        0x00000004
 #define CPU_BASED_USE_TSC_OFFSETING           0x00000008
@@ -219,14 +187,14 @@ void vmx_vmcs_reload(struct vcpu *v);
 #define CPU_BASED_MONITOR_EXITING             0x20000000
 #define CPU_BASED_PAUSE_EXITING               0x40000000
 #define CPU_BASED_ACTIVATE_SECONDARY_CONTROLS 0x80000000
-extern u32 vmx_cpu_based_exec_control;
+extern uint32_t vmx_cpu_based_exec_control;
 
 #define PIN_BASED_EXT_INTR_MASK         0x00000001
 #define PIN_BASED_NMI_EXITING           0x00000008
 #define PIN_BASED_VIRTUAL_NMIS          0x00000020
 #define PIN_BASED_PREEMPT_TIMER         0x00000040
 #define PIN_BASED_POSTED_INTERRUPT      0x00000080
-extern u32 vmx_pin_based_exec_control;
+extern uint32_t vmx_pin_based_exec_control;
 
 #define VM_EXIT_SAVE_DEBUG_CNTRLS       0x00000004
 #define VM_EXIT_IA32E_MODE              0x00000200
@@ -238,7 +206,7 @@ extern u32 vmx_pin_based_exec_control;
 #define VM_EXIT_LOAD_HOST_EFER          0x00200000
 #define VM_EXIT_SAVE_PREEMPT_TIMER      0x00400000
 #define VM_EXIT_CLEAR_BNDCFGS           0x00800000
-extern u32 vmx_vmexit_control;
+extern uint32_t vmx_vmexit_control;
 
 #define VM_ENTRY_IA32E_MODE             0x00000200
 #define VM_ENTRY_SMM                    0x00000400
@@ -247,7 +215,7 @@ extern u32 vmx_vmexit_control;
 #define VM_ENTRY_LOAD_GUEST_PAT         0x00004000
 #define VM_ENTRY_LOAD_GUEST_EFER        0x00008000
 #define VM_ENTRY_LOAD_BNDCFGS           0x00010000
-extern u32 vmx_vmentry_control;
+extern uint32_t vmx_vmentry_control;
 
 #define SECONDARY_EXEC_VIRTUALIZE_APIC_ACCESSES 0x00000001
 #define SECONDARY_EXEC_ENABLE_EPT               0x00000002
@@ -269,7 +237,7 @@ extern u32 vmx_vmentry_control;
 #define SECONDARY_EXEC_TSC_SCALING              0x02000000
 #define SECONDARY_EXEC_BUS_LOCK_DETECTION       0x40000000
 #define SECONDARY_EXEC_NOTIFY_VM_EXITING        0x80000000
-extern u32 vmx_secondary_exec_control;
+extern uint32_t vmx_secondary_exec_control;
 
 #define VMX_EPT_EXEC_ONLY_SUPPORTED                         0x00000001
 #define VMX_EPT_WALK_LENGTH_4_SUPPORTED                     0x00000040
@@ -286,7 +254,7 @@ extern u32 vmx_secondary_exec_control;
 #define VMX_VPID_INVVPID_SINGLE_CONTEXT                  0x20000000000ULL
 #define VMX_VPID_INVVPID_ALL_CONTEXT                     0x40000000000ULL
 #define VMX_VPID_INVVPID_SINGLE_CONTEXT_RETAINING_GLOBAL 0x80000000000ULL
-extern u64 vmx_ept_vpid_cap;
+extern uint64_t vmx_ept_vpid_cap;
 
 #define VMX_MISC_PROC_TRACE                     0x00004000
 #define VMX_MISC_CR3_TARGET                     0x01ff0000
@@ -373,7 +341,7 @@ extern u64 vmx_ept_vpid_cap;
  */
 #define VMX_BASIC_DEFAULT1_ZERO		(1ULL << 55)
 
-extern u64 vmx_basic_msr;
+extern uint64_t vmx_basic_msr;
 #define cpu_has_vmx_ins_outs_instr_info \
     (!!(vmx_basic_msr & VMX_BASIC_INS_OUT_INFO))
 
@@ -614,23 +582,6 @@ static inline int vmx_read_guest_msr(const struct vcpu *v, uint32_t msr,
     return 0;
 }
 
-static inline int vmx_read_guest_loadonly_msr(
-    const struct vcpu *v, uint32_t msr, uint64_t *val)
-{
-    const struct vmx_msr_entry *ent =
-        vmx_find_msr(v, msr, VMX_MSR_GUEST_LOADONLY);
-
-    if ( !ent )
-    {
-        *val = 0;
-        return -ESRCH;
-    }
-
-    *val = ent->data;
-
-    return 0;
-}
-
 static inline int vmx_write_guest_msr(struct vcpu *v, uint32_t msr,
                                       uint64_t val)
 {
@@ -644,7 +595,6 @@ static inline int vmx_write_guest_msr(struct vcpu *v, uint32_t msr,
     return 0;
 }
 
-
 /* MSR intercept bitmap infrastructure. */
 enum vmx_msr_intercept_type {
     VMX_MSR_R  = 1,
@@ -656,27 +606,7 @@ void vmx_clear_msr_intercept(struct vcpu *v, unsigned int msr,
                              enum vmx_msr_intercept_type type);
 void vmx_set_msr_intercept(struct vcpu *v, unsigned int msr,
                            enum vmx_msr_intercept_type type);
-void vmx_vmcs_switch(paddr_t from, paddr_t to);
-void vmx_set_eoi_exit_bitmap(struct vcpu *v, u8 vector);
-void vmx_clear_eoi_exit_bitmap(struct vcpu *v, u8 vector);
-bool vmx_msr_is_intercepted(struct vmx_msr_bitmap *msr_bitmap,
-                            unsigned int msr, bool is_write) __nonnull(1);
-void virtual_vmcs_enter(const struct vcpu *);
-void virtual_vmcs_exit(const struct vcpu *);
-u64 virtual_vmcs_vmread(const struct vcpu *, u32 encoding);
-enum vmx_insn_errno virtual_vmcs_vmread_safe(const struct vcpu *v,
-                                             u32 vmcs_encoding, u64 *val);
-void virtual_vmcs_vmwrite(const struct vcpu *, u32 encoding, u64 val);
-enum vmx_insn_errno virtual_vmcs_vmwrite_safe(const struct vcpu *v,
-                                              u32 vmcs_encoding, u64 val);
-
-DECLARE_PER_CPU(bool_t, vmxon);
-
-bool_t vmx_vcpu_pml_enabled(const struct vcpu *v);
-int vmx_vcpu_enable_pml(struct vcpu *v);
-void vmx_vcpu_disable_pml(struct vcpu *v);
-void vmx_vcpu_flush_pml_buffer(struct vcpu *v);
-bool_t vmx_domain_pml_enabled(const struct domain *d);
+bool vmx_domain_pml_enabled(const struct domain *d);
 int vmx_domain_enable_pml(struct domain *d);
 void vmx_domain_disable_pml(struct domain *d);
 void vmx_domain_flush_pml_buffers(struct domain *d);
