Library mcertikos.devdrivers.DSerialCSource
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 _maxintr := 1%positive.
Definition _j := 2%positive.
Definition ioapic_init_loop_body :=
(Ssequence
(Scall None
(Evar ioapic_write (Tfunction (Tcons tuint (Tcons tuint Tnil))
tvoid cc_default))
((Ebinop Oadd (Econst_int (Int.repr 16) tint)
(Ebinop Omul (Econst_int (Int.repr 2) tint) (Etempvar _j tint)
tint) tint) ::
(Ebinop Oadd
(Ebinop Oadd (Econst_int (Int.repr 65536) tint)
(Econst_int (Int.repr 32) tint) tint) (Etempvar _j tint) tint) ::
nil))
(Ssequence
(Scall None
(Evar ioapic_write (Tfunction (Tcons tuint (Tcons tuint Tnil))
tvoid cc_default))
((Ebinop Oadd
(Ebinop Oadd (Econst_int (Int.repr 16) tint)
(Ebinop Omul (Econst_int (Int.repr 2) tint)
(Etempvar _j tint) tint) tint)
(Econst_int (Int.repr 1) tint) tint) ::
(Econst_int (Int.repr 0) tint) :: nil))
(Sset _j
(Ebinop Oadd (Etempvar _j tint) (Econst_int (Int.repr 1) tint)
tint))
)).
Definition ioapic_init_loop_condition :=
(Ebinop Ole (Etempvar _j tint) (Etempvar _maxintr tint) tint).
Definition ioapic_init_body :=
(Ssequence
(Ssequence
(Scall (Some 39%positive)
(Evar ioapic_read (Tfunction (Tcons tuint Tnil) tuint cc_default))
((Econst_int (Int.repr 1) tint) :: nil))
(Sset _maxintr
(Ebinop Omod
(Ebinop Odiv (Etempvar 39%positive tuint)
(Econst_int (Int.repr 65536) tint) tuint)
(Ebinop Oadd (Econst_int (Int.repr 255) tint)
(Econst_int (Int.repr 1) tint) tint) tuint)))
(Ssequence
(Sset _j (Econst_int (Int.repr 0) tint))
(Swhile ioapic_init_loop_condition ioapic_init_loop_body)
)).
Definition f_ioapic_init := {|
fn_return := tvoid;
fn_callconv := cc_default;
fn_params := nil;
fn_vars := nil;
fn_temps := ((_maxintr, tint) :: (_j, tint) :: (39%positive, tuint) :: nil);
fn_body := ioapic_init_body
|}.
Definition _irq := 3%positive.
Definition _lapicid := 4%positive.
Definition _polarity := 5%positive.
Definition _trigger_mode := 6%positive.
Definition ioapic_enable_body :=
(Ssequence
(Ssequence
(Scall (Some 42%positive)
(Evar ioapic_read (Tfunction (Tcons tuint Tnil) tuint cc_default))
((Econst_int (Int.repr 1) tint) :: nil))
(Sset _maxintr
(Ebinop Omod
(Ebinop Odiv (Etempvar 42%positive tuint)
(Econst_int (Int.repr 65536) tint) tuint)
(Ebinop Oadd (Econst_int (Int.repr 255) tint)
(Econst_int (Int.repr 1) tint) tint) tuint)))
(Ssequence
(Sifthenelse (Ebinop Oge (Etempvar _irq tuint)
(Econst_int (Int.repr 0) tint) tint)
(Ssequence
(Sset 43%positive
(Ecast
(Ebinop Ole (Etempvar _irq tuint)
(Ebinop Oadd (Econst_int (Int.repr 0) tint)
(Etempvar _maxintr tint) tint) tint) tbool))
(Sset 43%positive (Ecast (Etempvar 43%positive tbool) tint)))
(Sset 43%positive (Econst_int (Int.repr 0) tint)))
(Sifthenelse (Etempvar 43%positive tint)
(Ssequence
(Scall None
(Evar ioapic_write (Tfunction (Tcons tuint (Tcons tuint Tnil))
tvoid cc_default))
((Ebinop Oadd (Econst_int (Int.repr 16) tint)
(Ebinop Omul (Econst_int (Int.repr 2) tint)
(Ebinop Osub (Etempvar _irq tuint)
(Econst_int (Int.repr 0) tint) tuint) tuint) tuint) ::
(Ebinop Oadd
(Ebinop Oadd
(Ebinop Omul (Etempvar _trigger_mode tuint)
(Econst_int (Int.repr 32768) tint) tuint)
(Ebinop Omul (Etempvar _polarity tuint)
(Econst_int (Int.repr 8192) tint) tuint) tuint)
(Ebinop Oadd (Econst_int (Int.repr 32) tint)
(Etempvar _irq tuint) tuint) tuint) :: nil))
(Scall None
(Evar ioapic_write (Tfunction (Tcons tuint (Tcons tuint Tnil))
tvoid cc_default))
((Ebinop Oadd
(Ebinop Oadd (Econst_int (Int.repr 16) tint)
(Ebinop Omul (Econst_int (Int.repr 2) tint)
(Ebinop Osub (Etempvar _irq tuint)
(Econst_int (Int.repr 0) tint) tuint) tuint) tuint)
(Econst_int (Int.repr 1) tint) tuint) ::
(Ebinop Omul (Etempvar _lapicid tuint)
(Econst_int (Int.repr 16777216) tint) tuint) :: nil)))
Sskip))).
Definition f_ioapic_enable := {|
fn_return := tvoid;
fn_callconv := cc_default;
fn_params := ((_irq, tuint) :: (_lapicid, tuint) ::
(_trigger_mode, tuint) :: (_polarity, tuint) :: nil);
fn_vars := nil;
fn_temps := ((_maxintr, tint) :: (43%positive, tint) ::
(42%positive, tuint) :: nil);
fn_body := ioapic_enable_body
|}.
Definition _redlo := 7%positive.
Definition ioapic_mask_body :=
(Ssequence
(Scall None (Evar local_irq_save (Tfunction Tnil tvoid cc_default)) nil)
(Ssequence
(Scall (Some _redlo)
(Evar ioapic_read (Tfunction (Tcons tuint Tnil) tuint cc_default))
((Ebinop Oadd (Econst_int (Int.repr 16) tint)
(Ebinop Omul (Econst_int (Int.repr 2) tint)
(Ebinop Osub (Etempvar _irq tuint)
(Econst_int (Int.repr 0) tint) tuint) tuint) tuint) :: nil))
(Ssequence
(Sset _redlo
(Ebinop Oor (Etempvar _redlo tuint)
(Econst_int (Int.repr 65536) tint) tuint))
(Ssequence
(Scall None
(Evar ioapic_write (Tfunction (Tcons tuint (Tcons tuint Tnil))
tvoid cc_default))
((Ebinop Oadd (Econst_int (Int.repr 16) tint)
(Ebinop Omul (Econst_int (Int.repr 2) tint)
(Ebinop Osub (Etempvar _irq tuint)
(Econst_int (Int.repr 0) tint) tuint) tuint) tuint) ::
(Etempvar _redlo tuint) :: nil))
(Scall None (Evar local_irq_restore (Tfunction Tnil tvoid cc_default)) nil))))).
Definition f_ioapic_mask := {|
fn_return := tvoid;
fn_callconv := cc_default;
fn_params := ((_irq, tuint) :: nil);
fn_vars := nil;
fn_temps := ((_redlo, tuint) :: nil);
fn_body := ioapic_mask_body
|}.
Definition ioapic_unmask_body :=
(Ssequence
(Scall None (Evar local_irq_save (Tfunction Tnil tvoid cc_default)) nil)
(Ssequence
(Scall (Some _redlo)
(Evar ioapic_read (Tfunction (Tcons tuint Tnil) tuint cc_default))
((Ebinop Oadd (Econst_int (Int.repr 16) tint)
(Ebinop Omul (Econst_int (Int.repr 2) tint)
(Ebinop Osub (Etempvar _irq tuint)
(Econst_int (Int.repr 0) tint) tuint) tuint) tuint) :: nil))
(Ssequence
(Sset _redlo
(Ebinop Oand (Etempvar _redlo tuint)
(Eunop Onotint (Econst_int (Int.repr 65536) tint) tint) tuint))
(Ssequence
(Scall None
(Evar ioapic_write (Tfunction (Tcons tuint (Tcons tuint Tnil))
tvoid cc_default))
((Ebinop Oadd (Econst_int (Int.repr 16) tint)
(Ebinop Omul (Econst_int (Int.repr 2) tint)
(Ebinop Osub (Etempvar _irq tuint)
(Econst_int (Int.repr 0) tint) tuint) tuint) tuint) ::
(Etempvar _redlo tuint) :: nil))
(Scall None (Evar local_irq_restore (Tfunction Tnil tvoid cc_default)) nil))))).
Definition f_ioapic_unmask := {|
fn_return := tvoid;
fn_callconv := cc_default;
fn_params := ((_irq, tuint) :: nil);
fn_vars := nil;
fn_temps := ((_redlo, tuint) :: nil);
fn_body := ioapic_unmask_body
|}.
Require Import AST.
Require Import Integers.
Require Import Values.
Require Import Cop.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Definition _maxintr := 1%positive.
Definition _j := 2%positive.
Definition ioapic_init_loop_body :=
(Ssequence
(Scall None
(Evar ioapic_write (Tfunction (Tcons tuint (Tcons tuint Tnil))
tvoid cc_default))
((Ebinop Oadd (Econst_int (Int.repr 16) tint)
(Ebinop Omul (Econst_int (Int.repr 2) tint) (Etempvar _j tint)
tint) tint) ::
(Ebinop Oadd
(Ebinop Oadd (Econst_int (Int.repr 65536) tint)
(Econst_int (Int.repr 32) tint) tint) (Etempvar _j tint) tint) ::
nil))
(Ssequence
(Scall None
(Evar ioapic_write (Tfunction (Tcons tuint (Tcons tuint Tnil))
tvoid cc_default))
((Ebinop Oadd
(Ebinop Oadd (Econst_int (Int.repr 16) tint)
(Ebinop Omul (Econst_int (Int.repr 2) tint)
(Etempvar _j tint) tint) tint)
(Econst_int (Int.repr 1) tint) tint) ::
(Econst_int (Int.repr 0) tint) :: nil))
(Sset _j
(Ebinop Oadd (Etempvar _j tint) (Econst_int (Int.repr 1) tint)
tint))
)).
Definition ioapic_init_loop_condition :=
(Ebinop Ole (Etempvar _j tint) (Etempvar _maxintr tint) tint).
Definition ioapic_init_body :=
(Ssequence
(Ssequence
(Scall (Some 39%positive)
(Evar ioapic_read (Tfunction (Tcons tuint Tnil) tuint cc_default))
((Econst_int (Int.repr 1) tint) :: nil))
(Sset _maxintr
(Ebinop Omod
(Ebinop Odiv (Etempvar 39%positive tuint)
(Econst_int (Int.repr 65536) tint) tuint)
(Ebinop Oadd (Econst_int (Int.repr 255) tint)
(Econst_int (Int.repr 1) tint) tint) tuint)))
(Ssequence
(Sset _j (Econst_int (Int.repr 0) tint))
(Swhile ioapic_init_loop_condition ioapic_init_loop_body)
)).
Definition f_ioapic_init := {|
fn_return := tvoid;
fn_callconv := cc_default;
fn_params := nil;
fn_vars := nil;
fn_temps := ((_maxintr, tint) :: (_j, tint) :: (39%positive, tuint) :: nil);
fn_body := ioapic_init_body
|}.
Definition _irq := 3%positive.
Definition _lapicid := 4%positive.
Definition _polarity := 5%positive.
Definition _trigger_mode := 6%positive.
Definition ioapic_enable_body :=
(Ssequence
(Ssequence
(Scall (Some 42%positive)
(Evar ioapic_read (Tfunction (Tcons tuint Tnil) tuint cc_default))
((Econst_int (Int.repr 1) tint) :: nil))
(Sset _maxintr
(Ebinop Omod
(Ebinop Odiv (Etempvar 42%positive tuint)
(Econst_int (Int.repr 65536) tint) tuint)
(Ebinop Oadd (Econst_int (Int.repr 255) tint)
(Econst_int (Int.repr 1) tint) tint) tuint)))
(Ssequence
(Sifthenelse (Ebinop Oge (Etempvar _irq tuint)
(Econst_int (Int.repr 0) tint) tint)
(Ssequence
(Sset 43%positive
(Ecast
(Ebinop Ole (Etempvar _irq tuint)
(Ebinop Oadd (Econst_int (Int.repr 0) tint)
(Etempvar _maxintr tint) tint) tint) tbool))
(Sset 43%positive (Ecast (Etempvar 43%positive tbool) tint)))
(Sset 43%positive (Econst_int (Int.repr 0) tint)))
(Sifthenelse (Etempvar 43%positive tint)
(Ssequence
(Scall None
(Evar ioapic_write (Tfunction (Tcons tuint (Tcons tuint Tnil))
tvoid cc_default))
((Ebinop Oadd (Econst_int (Int.repr 16) tint)
(Ebinop Omul (Econst_int (Int.repr 2) tint)
(Ebinop Osub (Etempvar _irq tuint)
(Econst_int (Int.repr 0) tint) tuint) tuint) tuint) ::
(Ebinop Oadd
(Ebinop Oadd
(Ebinop Omul (Etempvar _trigger_mode tuint)
(Econst_int (Int.repr 32768) tint) tuint)
(Ebinop Omul (Etempvar _polarity tuint)
(Econst_int (Int.repr 8192) tint) tuint) tuint)
(Ebinop Oadd (Econst_int (Int.repr 32) tint)
(Etempvar _irq tuint) tuint) tuint) :: nil))
(Scall None
(Evar ioapic_write (Tfunction (Tcons tuint (Tcons tuint Tnil))
tvoid cc_default))
((Ebinop Oadd
(Ebinop Oadd (Econst_int (Int.repr 16) tint)
(Ebinop Omul (Econst_int (Int.repr 2) tint)
(Ebinop Osub (Etempvar _irq tuint)
(Econst_int (Int.repr 0) tint) tuint) tuint) tuint)
(Econst_int (Int.repr 1) tint) tuint) ::
(Ebinop Omul (Etempvar _lapicid tuint)
(Econst_int (Int.repr 16777216) tint) tuint) :: nil)))
Sskip))).
Definition f_ioapic_enable := {|
fn_return := tvoid;
fn_callconv := cc_default;
fn_params := ((_irq, tuint) :: (_lapicid, tuint) ::
(_trigger_mode, tuint) :: (_polarity, tuint) :: nil);
fn_vars := nil;
fn_temps := ((_maxintr, tint) :: (43%positive, tint) ::
(42%positive, tuint) :: nil);
fn_body := ioapic_enable_body
|}.
Definition _redlo := 7%positive.
Definition ioapic_mask_body :=
(Ssequence
(Scall None (Evar local_irq_save (Tfunction Tnil tvoid cc_default)) nil)
(Ssequence
(Scall (Some _redlo)
(Evar ioapic_read (Tfunction (Tcons tuint Tnil) tuint cc_default))
((Ebinop Oadd (Econst_int (Int.repr 16) tint)
(Ebinop Omul (Econst_int (Int.repr 2) tint)
(Ebinop Osub (Etempvar _irq tuint)
(Econst_int (Int.repr 0) tint) tuint) tuint) tuint) :: nil))
(Ssequence
(Sset _redlo
(Ebinop Oor (Etempvar _redlo tuint)
(Econst_int (Int.repr 65536) tint) tuint))
(Ssequence
(Scall None
(Evar ioapic_write (Tfunction (Tcons tuint (Tcons tuint Tnil))
tvoid cc_default))
((Ebinop Oadd (Econst_int (Int.repr 16) tint)
(Ebinop Omul (Econst_int (Int.repr 2) tint)
(Ebinop Osub (Etempvar _irq tuint)
(Econst_int (Int.repr 0) tint) tuint) tuint) tuint) ::
(Etempvar _redlo tuint) :: nil))
(Scall None (Evar local_irq_restore (Tfunction Tnil tvoid cc_default)) nil))))).
Definition f_ioapic_mask := {|
fn_return := tvoid;
fn_callconv := cc_default;
fn_params := ((_irq, tuint) :: nil);
fn_vars := nil;
fn_temps := ((_redlo, tuint) :: nil);
fn_body := ioapic_mask_body
|}.
Definition ioapic_unmask_body :=
(Ssequence
(Scall None (Evar local_irq_save (Tfunction Tnil tvoid cc_default)) nil)
(Ssequence
(Scall (Some _redlo)
(Evar ioapic_read (Tfunction (Tcons tuint Tnil) tuint cc_default))
((Ebinop Oadd (Econst_int (Int.repr 16) tint)
(Ebinop Omul (Econst_int (Int.repr 2) tint)
(Ebinop Osub (Etempvar _irq tuint)
(Econst_int (Int.repr 0) tint) tuint) tuint) tuint) :: nil))
(Ssequence
(Sset _redlo
(Ebinop Oand (Etempvar _redlo tuint)
(Eunop Onotint (Econst_int (Int.repr 65536) tint) tint) tuint))
(Ssequence
(Scall None
(Evar ioapic_write (Tfunction (Tcons tuint (Tcons tuint Tnil))
tvoid cc_default))
((Ebinop Oadd (Econst_int (Int.repr 16) tint)
(Ebinop Omul (Econst_int (Int.repr 2) tint)
(Ebinop Osub (Etempvar _irq tuint)
(Econst_int (Int.repr 0) tint) tuint) tuint) tuint) ::
(Etempvar _redlo tuint) :: nil))
(Scall None (Evar local_irq_restore (Tfunction Tnil tvoid cc_default)) nil))))).
Definition f_ioapic_unmask := {|
fn_return := tvoid;
fn_callconv := cc_default;
fn_params := ((_irq, tuint) :: nil);
fn_vars := nil;
fn_temps := ((_redlo, tuint) :: nil);
fn_body := ioapic_unmask_body
|}.