Library mcertikos.devdrivers.DHandlerSwAsmSource
*********************************************************************** * * * The CertiKOS Certified Kit Operating System * * * * The FLINT Group, Yale University * * * * Copyright The FLINT Group, Yale University. All rights reserved. * * This file is distributed under the terms of the Yale University * * Non-Commercial License Agreement. * * * ***********************************************************************
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.