Library mcertikos.proc.UCtxtIntroGenAsmSource

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 EAX) None (inl ofs).

  Section RestoreUCtxt.


    Definition Im_restore_uctx : list instruction :=
      
      asm_instruction (Pmov_rm EAX (Addrmode (Some Asm.ESP) None (inl Int.zero))) ::

                      asm_instruction (Psal_ri EAX (Int.repr 2)) ::
                      asm_instruction (Pmov_rr EDX EAX) ::
                      asm_instruction (Psal_ri EAX (Int.repr 4)) ::
                      asm_instruction (Plea EAX (Addrmode (Some EDX) (Some (EAX, Int.one)) (inr (UCTX_LOC, Int.zero)))) ::

                      asm_instruction (Plea Asm.ESP (AddrMake (Int.repr (U_ES × 4)))) ::

                      
                      asm_instruction (Pmov_rm Asm.EDI (AddrMake (Int.repr (U_EDI × 4)))) ::
                      asm_instruction (Pmov_rm Asm.ESI (AddrMake (Int.repr (U_ESI × 4)))) ::
                      asm_instruction (Pmov_rm Asm.EBP (AddrMake (Int.repr (U_EBP × 4)))) ::
                      asm_instruction (Pmov_rm Asm.EBX (AddrMake (Int.repr (U_EBX × 4)))) ::
                      asm_instruction (Pmov_rm EDX (AddrMake (Int.repr (U_EDX × 4)))) ::
                      asm_instruction (Pmov_rm ECX (AddrMake (Int.repr (U_ECX × 4)))) ::
                      
                      Pmov_rm_nop Asm.ESP (AddrMake (Int.repr (U_ESP × 4))) ::
                      Pmov_rm_nop_RA (AddrMake (Int.repr (U_EIP × 4))) ::
                      
                      asm_instruction (Pmov_rm Asm.EAX (AddrMake (Int.repr (U_EAX × 4)))) ::
                      asm_instruction (Pjmp_s trap_out null_signature) ::
                      nil.

    Definition restoreuctx_function: function := mkfunction (mksignature (AST.Tint::nil) None cc_default) Im_restore_uctx.

  End RestoreUCtxt.

  Section ELFLoad.


    Definition Im_elf_load : list instruction :=
      
      PELFLOAD ::
               nil.

    Definition elf_load_sig := mksignature (Tint::Tint::nil) None cc_default.

    Definition elfload_function: function := mkfunction elf_load_sig Im_elf_load.

  End ELFLoad.

End ASM_CODE.

Notation MCode_Asm :=
  (restore_uctx ↦ restoreuctx_function
                ⊕ elf_load ↦ elfload_function).