Do you want a KASSERT(vmexit->exitcode == VM_EXITCODE_HLT) here or is that too silly? It seem from my reading that this is in fact true (and there's a comment at the start of this function saying it is true), but it is not trivially obvious from the code (e.g. the vlapic_pending_intr() in vmx_inject_interrupts() is called from a non-HLT exit, but only in the !virtual_interrupt_delivery case and this function is only used to implement vlapic_pending_intr() in the virtual_interrupt_delivery case).

I do think the idea is sound and prefer it to D14382.

I had one more question about this that I thought of after my first comment. Is there any chance that this VMCS field isn't valid to read such that vmcs_read() could fault in the !virtual_interrupt_delivery case? If the vmcs_read() will always succeed and just return zero in that case then this is fine. If it would fault on an old CPU that doesn't support virtual interrupts then it should be conditional. (I just can't recall if VMCS fields are always readable vs if some of them might fault if you try to read them for an unsupported feature.)

I've just tested this on system with hw.vmm.vmx.cap.virtual_interrupt_delivery = 0 and in this case vmcs_read(VMCS_GUEST_INTR_STATUS) simply returns zero.

I'm going to extrapolate that this is behavior on all generations of CPUs which don't support the 1-setting of the “virtual-interrupt delivery” VM-execution control :-)