Library mcertikos.proc.ThreadSchedGenAsmSource

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 dequeue_sig:= mksignature (Tint::nil) (Some Tint) cc_default.
  Definition set_state_sig := mksignature (Tint::Tint::nil) None cc_default.
  Definition get_curid_sig := mksignature nil (Some Tint) cc_default.
  Definition set_curid_sig := mksignature (Tint::nil) None cc_default.
  Definition get_CPU_ID_sig := mksignature nil (Some Tint) cc_default.

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

  Definition Im_thread_sched : list instruction :=
    asm_instruction (Pallocframe 16 (Int.repr 12) (Int.repr 8)) ::
                    asm_instruction (Pcall_s get_CPU_ID get_CPU_ID_sig) ::
                    asm_instruction (Pmov_mr (AddrMake Int.zero) EAX) ::
                    asm_instruction (Pcall_s dequeue dequeue_sig) ::

                    asm_instruction (Pmov_mr (AddrMake (Int.zero)) EAX) ::
                    asm_instruction (Pmov_ri EAX Int.one) ::
                    asm_instruction (Pmov_mr (AddrMake (Int.repr 4)) EAX) ::
                    asm_instruction (Pcall_s set_state set_state_sig) ::

                    asm_instruction (Pcall_s get_curid get_curid_sig) ::
                    asm_instruction (Pmov_mr (AddrMake (Int.repr 4)) EAX) ::

                    asm_instruction (Pcall_s set_curid set_curid_sig) ::

                    asm_instruction (Pmov_rm EDX (AddrMake (Int.repr 0))) ::
                    asm_instruction (Pmov_rm EAX (AddrMake (Int.repr 4))) ::

                    asm_instruction (Pfreeframe 16 (Int.repr 12) (Int.repr 8)) ::
                    asm_instruction (Pjmp_s kctxt_switch null_signature) ::
                    nil.

  Definition threadsched_function: function := mkfunction null_signature Im_thread_sched.

End ASM_CODE.