Library mcertikos.virt.intel.EPTOpGenAsmSource
*********************************************************************** * * * 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 EPT_INVALID.
Definition Im_ept_invalidate_mappings : list instruction :=
asm_instruction (Pallocframe 24 (Int.repr 20) (Int.repr 16)) ::
asm_instruction (Plea EAX (Addrmode None None (inr(EPT_LOC, Int.repr 30)))) ::
asm_instruction (Pmov_mr (AddrMake ESP (Int.repr 0)) EAX) ::
asm_instruction (Pxor_r EAX) ::
asm_instruction (Pmov_mr (AddrMake ESP (Int.repr 4)) EAX) ::
asm_instruction (Pmov_mr (AddrMake ESP (Int.repr 8)) EAX) ::
asm_instruction (Pmov_mr (AddrMake ESP (Int.repr 12)) EAX) ::
asm_instruction (Pmov_ri EAX (Int.repr 1)) ::
Pinvept EAX (AddrMake ESP (Int.repr 0)) ::
asm_instruction (Pfreeframe 24 (Int.repr 20) (Int.repr 16)) ::
asm_instruction (Pxor_r EAX) ::
asm_instruction (Pret) ::
nil.
Definition ept_invalidate_mappings_sig := mksignature nil (Some AST.Tint) cc_default.
Definition ept_invalidate_mappings_function: function := mkfunction ept_invalidate_mappings_sig Im_ept_invalidate_mappings.
End EPT_INVALID.
End ASM_CODE.