Library mcertikos.proc.VMCSIntroGenAsmSource

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.

  Notation v_vmcs_size := 4096 % Z.

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

  Definition AddrMakeBase (r: ireg) :=
    Addrmode None (Some (r, Int.one)) (inr (VMCS_LOC, Int.zero)).

  Section RCR0.

    Definition Im_rcr0 : list instruction :=
      Prcr0 EAX ::
            asm_instruction (Pret) ::
            nil.

    Definition rcr0_sig := mksignature nil (Some Tint) cc_default.

    Definition get_CPU_ID_sig := mksignature nil (Some Tint) cc_default.

    Definition rcr0_function: function := mkfunction rcr0_sig Im_rcr0.

  End RCR0.

  Section RCR3.

    Definition Im_rcr3 : list instruction :=
      Prcr3 EAX ::
            asm_instruction (Pret) ::
            nil.

    Definition rcr3_sig := mksignature nil (Some Tint) cc_default.

    Definition rcr3_function: function := mkfunction rcr3_sig Im_rcr3.

  End RCR3.

  Section RCR4.

    Definition Im_rcr4 : list instruction :=
      Prcr4 EAX ::
            asm_instruction (Pret) ::
            nil.

    Definition rcr4_sig := mksignature nil (Some Tint) cc_default.

    Definition rcr4_function: function := mkfunction rcr4_sig Im_rcr4.

  End RCR4.

  Section RDMSR.


    Definition Im_rdmsr : list instruction :=
    asm_instruction (Pallocframe 8 (Int.repr 4) (Int.repr 0)) ::
                    asm_instruction (Pmov_rm ECX (AddrMake EDX (Int.repr 0))) ::
                    Prdmsr ::
                    asm_instruction (Pfreeframe 8 (Int.repr 4) (Int.repr 0)) ::
                    asm_instruction (Pret) ::
                    nil.

    Definition rdmsr_sig := mksignature (Tint :: nil) (Some Tlong) cc_default.

    Definition rdmsr_function: function := mkfunction rdmsr_sig Im_rdmsr.

  End RDMSR.

  Section WRMSR.


    Definition Im_wrmsr : list instruction :=
      asm_instruction (Pallocframe 8 (Int.repr 4) (Int.repr 0)) ::
                      asm_instruction (Pmov_rm ECX (AddrMake EDX (Int.repr 0))) ::
                      asm_instruction (Pmov_rm EAX (AddrMake EDX (Int.repr 4))) ::
                      asm_instruction (Pmov_rm EDX (AddrMake EDX (Int.repr 8))) ::
                      
                      Pwrmsr ::
                      asm_instruction (Pmov_ri EAX Int.zero) ::
                      asm_instruction (Pfreeframe 8 (Int.repr 4) (Int.repr 0)) ::
                      asm_instruction (Pret) ::
                      nil.

    Definition wrmsr_sig := mksignature (Tint :: Tlong :: nil) (Some Tint) cc_default.

    Definition wrmsr_function: function := mkfunction wrmsr_sig Im_wrmsr.

  End WRMSR.

  Section VMCS_READZ.


    Definition Im_vmcs_readz : list instruction :=
      asm_instruction (Pallocframe 12 (Int.repr 8) (Int.repr 4)) ::
                      asm_instruction (Pmov_rm ECX (AddrMake EDX (Int.repr 0))) ::
                      asm_instruction (Pmov_mr (AddrMake ESP (Int.repr 0)) ECX) ::
                      asm_instruction (Pcall_s get_CPU_ID get_CPU_ID_sig) ::
                      asm_instruction (Pimul_ri EAX (Int.repr v_vmcs_size)) ::
                      asm_instruction (Pmov_rm ECX (AddrMake ESP (Int.repr 0))) ::
                      Pvmread VMCS_LOC EAX EAX ECX::
                      asm_instruction (Pfreeframe 12 (Int.repr 8) (Int.repr 4)) ::
                      asm_instruction (Pret) ::
                      nil.

    Definition vmcs_readz_sig := mksignature (Tint :: nil) (Some Tint) cc_default.

    Definition vmcs_readz_function: function := mkfunction vmcs_readz_sig Im_vmcs_readz.

  End VMCS_READZ.

  Section VMCS_WRITEZ.


    Definition Im_vmcs_writez : list instruction :=
      asm_instruction (Pallocframe 12 (Int.repr 8) (Int.repr 4)) ::
                      asm_instruction (Pmov_mr (AddrMake ESP (Int.repr 0)) EDX) ::
                      asm_instruction (Pcall_s get_CPU_ID get_CPU_ID_sig) ::
                      asm_instruction (Pimul_ri EAX (Int.repr v_vmcs_size)) ::
                      asm_instruction (Pmov_rm EDX (AddrMake ESP (Int.repr 0))) ::
                      asm_instruction (Pmov_rm ECX (AddrMake EDX (Int.repr 0))) ::
                      asm_instruction (Pmov_rm EDX (AddrMake EDX (Int.repr 4))) ::

                      Pvmwrite VMCS_LOC EAX EDX ECX::
                      asm_instruction (Pfreeframe 12 (Int.repr 8) (Int.repr 4)) ::
                      asm_instruction (Pret) ::
                      nil.

    Definition vmcs_writez_sig := mksignature (Tint :: Tint :: nil) None cc_default.

    Definition vmcs_writez_function: function := mkfunction vmcs_writez_sig Im_vmcs_writez.

  End VMCS_WRITEZ.

  Section VMCS_READZ64.


    Definition Im_vmcs_readz64 : list instruction :=
      asm_instruction (Pallocframe 12 (Int.repr 8) (Int.repr 4)) ::
                      asm_instruction (Pmov_rm ECX (AddrMake EDX (Int.repr 0))) ::
                      asm_instruction (Pmov_mr (AddrMake ESP (Int.repr 0)) ECX) ::
                      asm_instruction (Pcall_s get_CPU_ID get_CPU_ID_sig) ::
                      asm_instruction (Pimul_ri EAX (Int.repr v_vmcs_size)) ::
                      asm_instruction (Pmov_rm ECX (AddrMake ESP (Int.repr 0))) ::

                      asm_instruction (Pmov_mr (AddrMake ESP (Int.repr 0)) ESI) ::
                      asm_instruction (Pmov_rr ESI EAX) ::
                      Pvmread VMCS_LOC ESI EAX ECX ::
                      asm_instruction (Plea ECX (Addrmode (Some ECX) None (inl Int.one))) ::
                      Pvmread VMCS_LOC ESI EDX ECX ::
                      asm_instruction (Pmov_rm ESI (AddrMake ESP (Int.repr 0))) ::
                      asm_instruction (Pfreeframe 12 (Int.repr 8) (Int.repr 4)) ::
                      asm_instruction (Pret) ::
                      nil.

    Definition vmcs_readz64_sig := mksignature (Tint :: nil) (Some Tlong) cc_default.

    Definition vmcs_readz64_function: function := mkfunction vmcs_readz64_sig Im_vmcs_readz64.

  End VMCS_READZ64.

  Section VMCS_WRITEZ64.


    Definition Im_vmcs_writez64 : list instruction :=
      asm_instruction (Pallocframe 12 (Int.repr 8) (Int.repr 4)) ::
                      asm_instruction (Pmov_mr (AddrMake ESP (Int.repr 0)) EDX) ::
                      asm_instruction (Pcall_s get_CPU_ID get_CPU_ID_sig) ::
                      asm_instruction (Pimul_ri EAX (Int.repr v_vmcs_size)) ::
                      asm_instruction (Pmov_rm EDX (AddrMake ESP (Int.repr 0))) ::

                      asm_instruction (Pmov_mr (AddrMake ESP (Int.repr 0)) ESI) ::
                      asm_instruction (Pmov_rr ESI EAX) ::
                      asm_instruction (Pmov_rm ECX (AddrMake EDX (Int.repr 0))) ::
                      asm_instruction (Pmov_rm EAX (AddrMake EDX (Int.repr 4))) ::
                      asm_instruction (Pmov_rm EDX (AddrMake EDX (Int.repr 8))) ::
                      Pvmwrite VMCS_LOC ESI EAX ECX::
                      asm_instruction (Plea ECX (Addrmode (Some ECX) None (inl Int.one))) ::
                      Pvmwrite VMCS_LOC ESI EDX ECX::
                      asm_instruction (Pmov_rm ESI (AddrMake ESP (Int.repr 0))) ::
                      asm_instruction (Pfreeframe 12 (Int.repr 8) (Int.repr 4)) ::
                      asm_instruction (Pret) ::
                      nil.

    Definition vmcs_writez64_sig := mksignature (Tint :: Tlong :: nil) None cc_default.

    Definition vmcs_writez64_function: function := mkfunction vmcs_writez64_sig Im_vmcs_writez64.

  End VMCS_WRITEZ64.

  Section VMCS_WRITE_IDENT.


    Definition Im_vmcs_write_ident : list instruction :=
      asm_instruction (Pallocframe 12 (Int.repr 8) (Int.repr 4)) ::
                      asm_instruction (Pmov_mr (AddrMake ESP (Int.repr 0)) EDX) ::
                      asm_instruction (Pcall_s get_CPU_ID get_CPU_ID_sig) ::
                      asm_instruction (Pimul_ri EAX (Int.repr v_vmcs_size)) ::
                      asm_instruction (Pmov_rm EDX (AddrMake ESP (Int.repr 0))) ::
                      asm_instruction (Pmov_rm ECX (AddrMake EDX (Int.repr 0))) ::
                      asm_instruction (Pmov_rm EDX (AddrMake EDX (Int.repr 4))) ::

                      Pvmwrite VMCS_LOC EAX EDX ECX::
                      asm_instruction (Pfreeframe 12 (Int.repr 8) (Int.repr 4)) ::
                      asm_instruction (Pret) ::
                      nil.

    Definition vmcs_write_ident_sig := mksignature (Tint :: Tint :: nil) None cc_default.

    Definition vmcs_write_ident_function: function := mkfunction vmcs_write_ident_sig Im_vmcs_write_ident.

  End VMCS_WRITE_IDENT.

  Section VMX_ENABLE.

    Definition Im_vmx_enable : list instruction :=
      Pvmx_enable :: nil.

    Definition vmx_enable_sig := mksignature nil None cc_default.

    Definition vmx_enable_function: function := mkfunction vmx_enable_sig Im_vmx_enable.

  End VMX_ENABLE.

  Section VMPTRLD.


    Definition Im_vmptrld : list instruction :=
      asm_instruction (Pallocframe 16 (Int.repr 12) (Int.repr 8)) ::
                      asm_instruction (Pcall_s get_CPU_ID get_CPU_ID_sig) ::
                      asm_instruction (Pimul_ri EAX (Int.repr v_vmcs_size)) ::
                      asm_instruction (Plea EAX (AddrMakeBase EAX)) ::
                      asm_instruction (Pmov_mr (AddrMake ESP (Int.repr 0)) EAX) ::
                      asm_instruction (Pmov_ri EAX Int.zero) ::
                      asm_instruction (Pmov_mr (AddrMake ESP (Int.repr 4)) EAX) ::
                      Pvmptrld (AddrMake ESP (Int.repr 0)) ::
                      asm_instruction (Pfreeframe 16 (Int.repr 12) (Int.repr 8)) ::
                      asm_instruction (Pret) ::
                      nil.

    Definition vmptrld_sig := mksignature nil None cc_default.

    Definition vmptrld_function: function := mkfunction vmptrld_sig Im_vmptrld.

  End VMPTRLD.

End ASM_CODE.