Library mcertikos.proc.VMXInitGenAsmSource

Require Import Coqlib.
Require Import Integers.
Require Import Constant.
Require Import GlobIdent.
Require Import AST.

Require Import liblayers.compat.CompatLayers.
Require Import LAsm.

Section ASM_CODE.

  Definition AddrMake (ofs:int) :=
    Addrmode (Some ESP) None (inl ofs).

  Section VM_RUN.


    Definition Im_vm_run_user : list instruction :=
      asm_instruction (Pcall_s vmptrld null_signature) ::
                      asm_instruction (Pcall_s vmx_enter_pre null_signature) ::
                      asm_instruction (Pjmp_s vmx_enter null_signature) ::
                      nil.

    Definition vm_run_function: function := mkfunction null_signature Im_vm_run_user.

  End VM_RUN.

  Section RETURN_GUEST.


    Definition Im_vmx_return_from_guest : list instruction :=
      asm_instruction (Pcall_s host_in null_signature) ::
                      asm_instruction (Pcall_s vmx_exit_post null_signature) ::
                      Phost_in_post ::

                      nil.

    Definition vmx_return_from_guest_function: function := mkfunction null_signature Im_vmx_return_from_guest.

  End RETURN_GUEST.

End ASM_CODE.