• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Community
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
    • X86isa
      • Program-execution
      • Sdm-instruction-set-summary
      • Tlb
      • Running-linux
      • Introduction
      • Asmtest
      • X86isa-build-instructions
      • Publications
      • Contributors
      • Machine
      • Implemented-opcodes
      • To-do
      • Proof-utilities
      • Peripherals
      • Model-validation
        • Virtualization-for-validation
          • Virtualization-for-validation-debugging
          • Virtualization-for-validation-limitations
          • Dump-virtualizable-state
          • Write-virtualizable-mem
          • Validate-insts
          • Run-until-rip-or-n
          • Validate-inst
          • Write-val1
          • Write-bytes
        • Dynamic-instrumentation
      • Modelcalls
      • Concrete-simulation-examples
      • Utils
      • Debugging-code-proofs
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Virtualization-for-validation

Virtualization-for-validation-debugging

Some tips on debugging the virtualization based validation tool.

The virtualization based validation tool is pretty rough, and it isn't uncommon to run into issues. Here we document some debugging tips.

Segfault or other issue immediately after starting the C program

This is likely either because you don't have permissions to open /dev/kvm or state.virt doesn't exist. I recommend running the C program with strace and check the return value for the open syscalls. If they are -1, you need to resolve why those files can't be opened.

VMEXIT with exit_reason = KVM_EXIT_FAIL_ENTRY and (on VMX, SVM has a different error code for a similar thing) hardware_entry_failure_reason = 0x80000021

This is probably the most difficult to debug issue you can come across. Essentially what has happened is that the state of the virtual machine is invalid. KVM can't give you more information because this is all the information the processor gave it. The SDM says that this error code (see SDM Volume 3 Chapter 27.8) means that the state failed one of the check in Chapter 27.3.1.

This part of the manual has a ton of different checks which may have failed, so it is basically useless. Here's a couple of suggestions on how to debug this. The first thing you should do is enable tracing of the KVM subsystem in Linux, enable dump invalid state, and then attempt to run the VM and look at the kernel log. Depending on the issue, you may notice something off in the log. Otherwise, move on to the following. It's pretty involved, but I have yet to find a better way.

Build a copy of QEMU's qemu-system-x86_64 with -ggdb. Then, launch it with the tiny code generator TCG backend (this is important, it won't work otherwise) in gdb, set a breakpoint on the cpu_vmexit function, and boot some Linux distro. Inside the VM, I run the validation C program (compiling it without -DVALIDATE is useful for this) and it will likely VMEXIT and trigger the breakpoint. Then, you can look at the backtrace to determine why it happened.

Note: due to differences between VMX and SVM, it's possible that the behavior in QEMU doesn't match the behavior on an Intel processor. In my experience, it usually still fails, but in some other way. For example, in QEMU I had the VM triple fault instead. If you're getting some sort of exception, try setting breakpoints on some of the functions used to raise exceptions.