Library mcertikos.mcslock.MCSLockIntroGenAsmSource

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 atomic_mcs_log_sig:= mksignature (Tint::Tint::nil) None cc_default.
  Definition atomic_mcs_SWAP_sig:= mksignature (Tint::Tint::Tint::nil) (Some Tint) cc_default.
  Definition atomic_mcs_CAS_sig:= mksignature (Tint::Tint::nil) (Some Tint) cc_default.
  Definition mcs_log_sig:= mksignature (Tint::Tint::nil) None cc_default.
  Definition mcs_SWAP_TAIL_sig:= mksignature (Tint::Tint::Tint::nil) (Some Tint) cc_default.
  Definition mcs_CAS_TAIL_sig:= mksignature (Tint::Tint::nil) (Some Tint) cc_default.

  Definition AddrMakeArg (ofs:int) :=
    Addrmode (Some EDX) None (inl ofs).

  Definition AddrMakeArg2 (ofs:int) :=
    Addrmode (Some ESP) None (inl ofs).

  Definition Im_mcs_log : list instruction :=
    asm_instruction (Pallocframe 16 (Int.repr 12) (Int.repr 8))::
                    asm_instruction (Pmov_rm EAX (AddrMakeArg (Int.repr 0))) ::
                    asm_instruction (Pmov_mr (AddrMakeArg2 Int.zero) EAX) ::
                    asm_instruction (Pmov_rm EAX (AddrMakeArg (Int.repr 4))) ::
                    asm_instruction (Pmov_mr (AddrMakeArg2 (Int.repr 4)) EAX) ::
                    asm_instruction (Pcall_s atomic_mcs_log atomic_mcs_log_sig) ::
                    asm_instruction (Pfreeframe 16 (Int.repr 12) (Int.repr 8)) ::
                    asm_instruction (Pret) ::
                    nil.

  Definition mcs_log_function: function := mkfunction mcs_log_sig Im_mcs_log.

  Definition Im_mcs_SWAP_TAIL : list instruction :=
    asm_instruction (Pallocframe 20 (Int.repr 16) (Int.repr 12))::
                    asm_instruction (Pmov_rm EAX (AddrMakeArg (Int.repr 0))) ::
                    asm_instruction (Pmov_mr (AddrMakeArg2 Int.zero) EAX) ::
                    asm_instruction (Pmov_rm EAX (AddrMakeArg (Int.repr 4))) ::
                    asm_instruction (Pmov_mr (AddrMakeArg2 (Int.repr 4)) EAX) ::
                    asm_instruction (Pmov_rm EAX (AddrMakeArg (Int.repr 8))) ::
                    asm_instruction (Pmov_mr (AddrMakeArg2 (Int.repr 8)) EAX) ::
                    asm_instruction (Pcall_s atomic_mcs_SWAP atomic_mcs_SWAP_sig) ::
                    asm_instruction (Pfreeframe 20 (Int.repr 16) (Int.repr 12)) ::
                    asm_instruction (Pret) ::
                    nil.

  Definition mcs_SWAP_TAIL_function: function := mkfunction mcs_SWAP_TAIL_sig Im_mcs_SWAP_TAIL.

  Definition Im_mcs_CAS_TAIL : list instruction :=
    asm_instruction (Pallocframe 16 (Int.repr 12) (Int.repr 8))::
                    asm_instruction (Pmov_rm EAX (AddrMakeArg (Int.repr 0))) ::
                    asm_instruction (Pmov_mr (AddrMakeArg2 Int.zero) EAX) ::
                    asm_instruction (Pmov_rm EAX (AddrMakeArg (Int.repr 4))) ::
                    asm_instruction (Pmov_mr (AddrMakeArg2 (Int.repr 4)) EAX) ::
                    asm_instruction (Pcall_s atomic_mcs_CAS atomic_mcs_CAS_sig) ::
                    asm_instruction (Pfreeframe 16 (Int.repr 12) (Int.repr 8)) ::
                    asm_instruction (Pret) ::
                    nil.

  Definition mcs_CAS_TAIL_function: function := mkfunction mcs_CAS_TAIL_sig Im_mcs_CAS_TAIL.

End ASM_CODE.