Library mcertikos.proc.QueueIntroGenAsmSource

Require Import Coqlib.
Require Import Integers.
Require Import Constant.
Require Import GlobIdent.
Require Import AST.

Require Import liblayers.compat.CompatLayers.
Require Import LAsm.
Require Import GlobalOracle.

Section ASM_CODE.

  Definition AddrMake (ofs:int) :=
    Addrmode (Some ESP) None (inl ofs).
  Definition AddrMakeArg (ofs:int) := Addrmode (Some EDX) None (inl ofs).
  Definition AddrAbID :=
    Addrmode (Some EAX) None (inl (Int.repr lock_TCB_range)).

  Definition acquire_lock_sig := mksignature (Tint::Tint::Tint::nil) None cc_default.
  Definition acquire_lock_TCB_sig := mksignature (Tint::nil) None cc_default.

  Section AcqLOCK.


    Definition Im_acquire_lock_TCB : list instruction :=
      asm_instruction (Pallocframe 20 (Int.repr 16) (Int.repr 12)) ::
                      asm_instruction (Pmov_ri EAX (Int.repr (Z.of_nat local_lock_bound))) ::
                      asm_instruction (Pmov_mr (AddrMake (Int.zero)) EAX) ::
                      asm_instruction (Pmov_ri EAX (Int.repr ID_TCB)) ::
                      asm_instruction (Pmov_mr (AddrMake (Int.repr 4)) EAX) ::
                      asm_instruction (Pmov_rm EAX (AddrMakeArg (Int.repr 0))) ::
                      asm_instruction (Pmov_mr (AddrMake (Int.repr 8)) EAX) ::
                      asm_instruction (Pcall_s acquire_lock acquire_lock_sig) ::
                      asm_instruction (Pfreeframe 20 (Int.repr 16) (Int.repr 12)) ::
                      asm_instruction (Pret) ::
                      nil.

    Definition acquire_lock_TCB_function: function := mkfunction acquire_lock_TCB_sig Im_acquire_lock_TCB.

    Definition release_lock_sig := mksignature (Tint::Tint::nil) None cc_default.
    Definition release_lock_TCB_sig := mksignature (Tint::nil) None cc_default.


    Definition Im_release_lock_TCB : list instruction :=
      asm_instruction (Pallocframe 16 (Int.repr 12) (Int.repr 8)) ::
                      asm_instruction (Pmov_ri EAX (Int.repr ID_TCB)) ::
                      asm_instruction (Pmov_mr (AddrMake (Int.zero)) EAX) ::
                      asm_instruction (Pmov_rm EAX (AddrMakeArg (Int.repr 0))) ::
                      asm_instruction (Pmov_mr (AddrMake (Int.repr 4)) EAX) ::
                      asm_instruction (Pcall_s release_lock release_lock_sig) ::
                      asm_instruction (Pfreeframe 16 (Int.repr 12) (Int.repr 8)) ::
                      asm_instruction (Pret) ::
                      nil.

    Definition release_lock_TCB_function: function := mkfunction release_lock_TCB_sig Im_release_lock_TCB.

  End AcqLOCK.

End ASM_CODE.