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.