arm_hv_set_vreg
void arm_hv_set_vreg(u32 msr, u64 val);
#define WRMSR(msr, val) arm_hv_set_vreg(msr, val)
