Library mcertikos.devdrivers.DHandlerSwAsmSource

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 (id: ident) :=
    Addrmode None None (inr (id, Int.zero)).

  Definition Im_serial_intr_handler_asm : list instruction :=

                    asm_instruction (Pmov_mr (AddrMake set_tf) EDX) ::
                    asm_instruction (Pallocframe 8 (Int.repr 4) (Int.repr 0)) ::
                    asm_instruction (Pmov_rm EDX (AddrMake set_tf)) ::
    asm_instruction (Pcall_s save_context null_signature) ::

                    asm_instruction (Pcall_s serial_intr_handler_sw null_signature) ::
                    
                    asm_instruction (Pmov_ri EDX Int.zero) ::
                    asm_instruction (Pmov_mr (AddrMake set_tf) EDX) ::

                    asm_instruction (Pcall_s restore_context null_signature) ::
                    asm_instruction (Pfreeframe 8 (Int.repr 4) (Int.repr 0)) ::

                    asm_instruction (Pret) ::
                    nil.

  Definition serial_intr_handler_asm_function: function := mkfunction null_signature Im_serial_intr_handler_asm.

End ASM_CODE.