Indan Zupancic

For some reason `if (config_set(CONFIG_HAVE_FPU))` doesn't work to hide things. Easily fixed by creating an empty `fpuRelease`, but I wouldn't expect that would be necessary. Any suggestions? Edit: I fixed...

@chrisguikema If you have time, could you review and test the x86 VCPU changes on your VmMs? Would be good to know whether there is a performance degradation too. I...

Okay, done. Let me know if this is fine.

> Sorry, I thought that the new `invokeDomainSetSet` function would be fine but it returning an exception causes a surprising amount of pain in the proofs. Do you have any...

XSAVES works with VCPU too now, we were missing proper FPU state init for VCPUs on x86. All code paths in `vcpu_fpu_to_guest()` are now tested (verified with printfs). For `vcpu_fpu_to_host()`,...

> You mean x86 32-bit virtualisation? I guess we should better double-check, but I wasn't even aware that we support that. Yes. And we do. In CI it's e.g. PC99_debug_hyp_gcc_32....

The rebase madness should be done now. Multiple commits combined with previous ones, mistakes made with previous rebase fixed, and last tweaks after a per-commit review.

I reverted the `set` optimisation and removed the `setThreadState ThreadState_Running`, as it doesn't seem to be necessary. If it gives problems for verification I'll add it back, but correctly this...

> Okay, I've finally gotten back to this and updated the proofs for the last round of improvements. This did need one additional change however, to do with making it...

It seems that commit 407484d causes things to break on the HiFive P550. Which seems to be the only RISCV with SMP enabled. Anyway, the reason why the commit breaks...