Library mcertikos.proc.EPTIntroGenAsmSource

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 get_CPU_ID_sig := mksignature nil (Some Tint) cc_default.

    Definition Im_ept_invalidate_mappings : list instruction :=
      asm_instruction (Pallocframe 24 (Int.repr 20) (Int.repr 16)) ::
                      asm_instruction (Pcall_s get_CPU_ID get_CPU_ID_sig) ::
                      asm_instruction (Pimul_ri EAX (Int.repr 8413184)) ::
                      asm_instruction (Plea EAX (Addrmode None (Some (EAX, Int.one)) (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.