Library mcertikos.virt.intel.VMCSIntroGenAsmSource

***********************************************************************
*                                                                     *
*            The CertiKOS Certified Kit Operating System              *
*                                                                     *
*                   The FLINT Group, Yale University                  *
*                                                                     *
*  Copyright The FLINT Group, Yale University.  All rights reserved.  *
*  This file is distributed under the terms of the Yale University    *
*  Non-Commercial License Agreement.                                  *
*                                                                     *
*********************************************************************** 


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 (r: ireg) (ofs:int) :=
    Addrmode (Some r) None (inl ofs).

  Section RCR0.

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

    Definition rcr0_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 8 (Int.repr 4) (Int.repr 0)) ::
                      asm_instruction (Pmov_rm ECX (AddrMake EDX (Int.repr 0))) ::
                      Pvmread VMCS_LOC EAX ECX::
                      asm_instruction (Pfreeframe 8 (Int.repr 4) (Int.repr 0)) ::
                      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 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))) ::
                      Pvmwrite VMCS_LOC EAX ECX::
                      asm_instruction (Pfreeframe 8 (Int.repr 4) (Int.repr 0)) ::
                      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 8 (Int.repr 4) (Int.repr 0)) ::
                      asm_instruction (Pmov_rm ECX (AddrMake EDX (Int.repr 0))) ::
                      Pvmread VMCS_LOC EAX ECX::
                      asm_instruction (Plea ECX (Addrmode (Some ECX) None (inl Int.one))) ::
                      Pvmread VMCS_LOC EDX ECX::
                      asm_instruction (Pfreeframe 8 (Int.repr 4) (Int.repr 0)) ::
                      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 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))) ::
                      Pvmwrite VMCS_LOC EAX ECX::
                      asm_instruction (Plea ECX (Addrmode (Some ECX) None (inl Int.one))) ::
                      Pvmwrite VMCS_LOC EDX ECX::
                      asm_instruction (Pfreeframe 8 (Int.repr 4) (Int.repr 0)) ::
                      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 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))) ::
                      Pvmwrite VMCS_LOC EAX ECX::
                      asm_instruction (Pfreeframe 8 (Int.repr 4) (Int.repr 0)) ::
                      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 (Pmov_ra EAX VMCS_LOC) ::
                      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.