Library mcertikos.devdrivers.DHandlerCxtCSource

Require Import Coqlib.
Require Import AST.
Require Import Integers.
Require Import Values.
Require Import Cop.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.

Definition _has_irq := 1%positive.
Definition _n := 2%positive.
Definition _t := 3%positive.

Definition serial_intr_disable_handler_loop_condition :=
  Ebinop Oand
  (Ebinop Oeq (Etempvar _has_irq tuint) (Econst_int (Int.repr 1) tuint) tint)
  (Ebinop Ogt (Etempvar _t tuint) (Econst_int (Int.repr 0) tuint) tint)
  tint.

Notation serial_intr_disable_handler_loop_body :=
  (Ssequence
     (Scall (Some _n)
            (Evar serial_hw_intr (Tfunction Tnil tuint cc_default)) nil)
     (Ssequence
        (Sifthenelse (Ebinop Oeq (Etempvar _n tuint)
                             (Econst_int (Int.repr 36) tint) tint)
                     (Ssequence
                        (Scall None
                               (Evar serial_intr_handler_asm (Tfunction Tnil tvoid cc_default)) nil)
                        (Scall None (Evar iret (Tfunction Tnil tvoid cc_default))
                               nil))
                     Sskip)
        (Ssequence
           (Sset _t
                 (Ebinop Osub (Etempvar _t tuint)
                         (Econst_int (Int.repr 1) tuint) tuint))
           (Scall (Some _has_irq)
                  (Evar serial_irq_check (Tfunction Tnil tuint cc_default))
                  nil)
  ))).

Definition serial_intr_disable_handler_body :=
  (Ssequence
     (Sset _t (Econst_int (Int.repr 100) tuint))
     (Ssequence
        (Scall (Some _has_irq) (Evar serial_irq_check (Tfunction Tnil tuint cc_default)) nil)
        (Sifthenelse (Ebinop Oeq (Etempvar _has_irq tuint) (Econst_int (Int.repr 1) tint) tint)
                     (Swhile serial_intr_disable_handler_loop_condition serial_intr_disable_handler_loop_body)
                     Sskip))).

Definition f_serial_intr_disable_handler := {|
  fn_return := tvoid;
  fn_callconv := cc_default;
  fn_params := nil;
  fn_vars := nil;
  fn_temps := ((_n, tuint) :: (_has_irq, tuint) :: (_t, tuint) :: nil);
  fn_body := serial_intr_disable_handler_body
|}.

Notation serial_intr_enable_handler_loop_body :=
  (Ssequence
     (Scall (Some _n) (Evar ic_intr (Tfunction
                            (Tcons tuint Tnil) tuint cc_default))
            ((Econst_int (Int.repr 4) tuint) :: nil))
     (Ssequence
        (Sifthenelse (Ebinop Oeq (Etempvar _n tuint)
                             (Econst_int (Int.repr 36) tuint) tint)
                     (Ssequence
                        (Scall None (Evar serial_intr_handler_asm
                                          (Tfunction Tnil tvoid cc_default)) nil)
                        (Scall None (Evar iret (Tfunction Tnil tvoid cc_default))
                               nil))
                     Sskip)
        (Ssequence
           (Sset _t
                 (Ebinop Osub (Etempvar _t tuint) (Econst_int (Int.repr 1) tint) tuint))
           (Scall (Some _has_irq)
                  (Evar serial_irq_current (Tfunction Tnil tuint
                                                      cc_default)) nil)
  ))).

Definition serial_intr_enable_handler_loop_condition :=
  Ebinop Oand
         (Ebinop Oeq (Etempvar _has_irq tuint) (Econst_int (Int.repr 1) tuint) tint)
         (Ebinop Ogt (Etempvar _t tuint) (Econst_int (Int.repr 0) tuint) tint)
         tint.

Definition serial_intr_enable_handler_body :=
  (Ssequence
     (Sset _t (Econst_int (Int.repr 100) tuint))
     (Ssequence
        (Scall (Some _has_irq)
               (Evar serial_irq_current (Tfunction Tnil tuint cc_default)) nil)
        (Sifthenelse (Ebinop Oeq (Etempvar _has_irq tuint)
                             (Econst_int (Int.repr 1) tuint) tint)
                     (Swhile serial_intr_enable_handler_loop_condition serial_intr_enable_handler_loop_body)
                     Sskip))).

Definition f_serial_intr_enable_handler := {|
  fn_return := tvoid;
  fn_callconv := cc_default;
  fn_params := nil;
  fn_vars := nil;
  fn_temps := ((_n, tuint) :: (_has_irq, tuint) :: (_t, tuint) :: nil);
  fn_body := serial_intr_enable_handler_body
|}.