Library mcertikos.virt.intel.VMXInitGenAsmSource
*********************************************************************** * * * 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 (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 null_signature) ::
asm_instruction (Pcall_s vmx_exit_post null_signature) ::
asm_instruction (Pcall_s proc_start_user null_signature) ::
nil.
Definition vmx_return_from_guest_function: function := mkfunction null_signature Im_vmx_return_from_guest.
End RETURN_GUEST.
End ASM_CODE.