Library mcertikos.trap.SysCallGenAsmSource

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

  Definition syscall_c_dispatch_sig := null_signature.

  Definition trap_get_sig := null_signature.
  Definition proc_start_user_sig := null_signature.


  Definition thread_yield_sig := null_signature.
  Definition ptfault_resv_sig := mksignature (Tint::nil) None cc_default.
  Definition thread_sleep_sig :=
    mksignature (Tint::nil) None cc_default.

  Definition trap_sendtochan_pre_sig :=
    mksignature nil (Some Tint) cc_default.

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

  Section SysDispatch.


    Definition Im_sys_dispatch : list instruction :=
      asm_instruction (Pcall_s proc_exit_user2 proc_exit_user_sig) ::
                      asm_instruction (Pcall_s syscall_dispatch_C syscall_c_dispatch_sig) ::
                      asm_instruction (Pcall_s proc_start_user2 proc_start_user_sig) ::
                      nil.

    Definition sys_dispatch_function: function := mkfunction null_signature Im_sys_dispatch.

  End SysDispatch.


  Section SysYield.


    Definition Im_sys_yield : list instruction :=
      asm_instruction (Pcall_s proc_exit_user proc_exit_user_sig) ::
                      Pmov_ra_RA proc_start_user ::
                      asm_instruction (Pjmp_s thread_yield thread_yield_sig) ::
                      nil.

    Definition sys_yield_function: function := mkfunction null_signature Im_sys_yield.

  End SysYield.


  Section PgfHandler.


    Definition Im_pgf_handler : list instruction :=
      asm_instruction (Pcall_s proc_exit_user proc_exit_user_sig) ::
                      asm_instruction (Pallocframe 12 (Int.repr 8) (Int.repr 4)) ::
                      asm_instruction (Pcall_s trap_get trap_get_sig) ::
                      asm_instruction (Pmov_mr (AddrMake (Int.zero)) EAX) ::
                      asm_instruction (Pcall_s ptfault_resv ptfault_resv_sig) ::
                      asm_instruction (Pfreeframe 12 (Int.repr 8) (Int.repr 4)) ::
                      asm_instruction (Pcall_s proc_start_user proc_start_user_sig) ::
                      nil.

    Definition pgf_handler_function: function := mkfunction null_signature Im_pgf_handler.

  End PgfHandler.

  Section SysSendPre.


    Definition Im_sys_sendtochan_pre : list instruction :=
      asm_instruction (Pcall_s proc_exit_user proc_exit_user_sig) ::
                      asm_instruction (Pcall_s trap_sendtochan_pre trap_sendtochan_pre_sig) ::
                      Pmov_ra_RA sys_sendtochan_post ::
                      asm_instruction (Plea ESP (AddrMake (Int.repr 28))) ::
                      asm_instruction (Pjmp_s thread_sleep thread_sleep_sig) ::
                      nil.

    Definition sys_sendtochan_pre_function: function := mkfunction null_signature Im_sys_sendtochan_pre.

  End SysSendPre.

  Section SysSendPost.


    Definition Im_sys_sendtochan_post : list instruction :=
      asm_instruction (Pcall_s trap_sendtochan_post null_signature) ::
                      asm_instruction (Pcall_s proc_start_user proc_start_user_sig) ::
                      nil.

    Definition sys_sendtochan_post_function: function := mkfunction null_signature Im_sys_sendtochan_post.

  End SysSendPost.

  Section SysRunVM.


    Definition Im_sys_run_vm : list instruction :=
      asm_instruction (Pcall_s proc_exit_user proc_exit_user_sig) ::
                      asm_instruction (Pjmp_s vmx_run_vm null_signature) ::
                      nil.

    Definition sys_run_vm_function: function := mkfunction null_signature Im_sys_run_vm.

  End SysRunVM.

End ASM_CODE.