Library mcertikos.proc.VMXIntroGenAsmSource

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 get_CPU_ID_sig := mksignature nil (Some Tint) cc_default.

  Definition AddrMake (ofs:int) :=
    Addrmode None (Some (Asm.ECX, Int.one)) (inr (VMX_LOC, ofs)).

  Definition AddrMake2 (r: ireg) (ofs:int) :=
    Addrmode (Some r) None (inl ofs).

  Section VMX_ENTER.


    Definition Im_vmx_enter : list instruction :=
      asm_instruction (Pcall_s get_CPU_ID get_CPU_ID_sig) ::
      asm_instruction (Pmov_rr Asm.ECX Asm.EAX) ::
      asm_instruction (Pimul_ri ECX (Int.repr (VMX_Size´ × 4))) ::
      asm_instruction (Pmov_mr (AddrMake (Int.repr VMX_HOST_EBP)) Asm.EBP) ::
                      asm_instruction (Pmov_mr (AddrMake (Int.repr VMX_HOST_EDI)) Asm.EDI) ::
                      Pvmx_load_guest ::
                      Pgloballabel vmx_enter_bottom_half ::
                      asm_instruction (Pmov_rm Asm.EAX (AddrMake (Int.repr VMX_G_RAX))) ::
                      asm_instruction (Pmov_rm Asm.EBX (AddrMake (Int.repr VMX_G_RBX))) ::
                      asm_instruction (Pmov_rm Asm.EDX (AddrMake (Int.repr VMX_G_RDX))) ::
                      asm_instruction (Pmov_rm Asm.ESI (AddrMake (Int.repr VMX_G_RSI))) ::
                      asm_instruction (Pmov_rm Asm.EDI (AddrMake (Int.repr VMX_G_RDI))) ::
                      asm_instruction (Pmov_rm Asm.EBP (AddrMake (Int.repr VMX_G_RBP))) ::
                      Pmov_rm_nop_RA (AddrMake (Int.repr VMX_G_RIP)) ::
                      asm_instruction (Pjmp_s host_out null_signature) ::
                      
                      nil.

    Definition vmx_enter_function: function := mkfunction (mksignature nil None cc_default) Im_vmx_enter.

  End VMX_ENTER.

  Section VMX_EXIT.


    Definition Im_vmx_exit : list instruction :=

      asm_instruction (Pmov_mr (AddrMake (Int.repr VMX_G_RDI)) Asm.EDI) ::
                      Pvmx_store_guest ::
                      Pgloballabel vmx_exit_bottom_half ::
                      asm_instruction (Pmov_mr (AddrMake (Int.repr VMX_G_RAX)) Asm.EAX) ::
                      asm_instruction (Pmov_mr (AddrMake (Int.repr VMX_G_RBX)) Asm.EBX) ::
                      asm_instruction (Pmov_mr (AddrMake (Int.repr VMX_G_RDX)) Asm.EDX) ::
                      asm_instruction (Pmov_mr (AddrMake (Int.repr VMX_G_RSI)) Asm.ESI) ::
                      asm_instruction (Pmov_mr (AddrMake (Int.repr VMX_G_RBP)) Asm.EBP) ::
                      asm_instruction (Pmov_rm Asm.EBP (AddrMake (Int.repr VMX_HOST_EBP))) ::
                      asm_instruction (Pmov_rm Asm.EDI (AddrMake (Int.repr VMX_HOST_EDI))) ::
                      

                      asm_instruction (Pret)::
                      nil.

    Definition vmx_exit_function: function := mkfunction (mksignature nil None cc_default) Im_vmx_exit.

  End VMX_EXIT.

End ASM_CODE.