Library mcertikos.devdrivers.DSerialIntroCSource
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 ex: ident := 1 % positive.
Definition serial_init_body :=
(Ssequence
(Scall None
(Evar serial_out (Tfunction (Tcons tint (Tcons tuint Tnil)) tvoid
cc_default))
((Ebinop Oadd (Econst_int (Int.repr 1016) tint)
(Econst_int (Int.repr 3) tint) tint) ::
(Econst_int (Int.repr 0) tint) :: nil))
(Ssequence
(Scall None
(Evar serial_out (Tfunction (Tcons tint (Tcons tuint Tnil)) tvoid
cc_default))
((Ebinop Oadd (Econst_int (Int.repr 1016) tint)
(Econst_int (Int.repr 1) tint) tint) ::
(Econst_int (Int.repr 0) tint) :: nil))
(Ssequence
(Scall None
(Evar serial_out (Tfunction (Tcons tint (Tcons tuint Tnil)) tvoid
cc_default))
((Ebinop Oadd (Econst_int (Int.repr 1016) tint)
(Econst_int (Int.repr 3) tint) tint) ::
(Econst_int (Int.repr 128) tint) :: nil))
(Ssequence
(Scall None
(Evar serial_out (Tfunction (Tcons tint (Tcons tuint Tnil)) tvoid
cc_default))
((Ebinop Oadd (Econst_int (Int.repr 1016) tint)
(Econst_int (Int.repr 0) tint) tint) ::
(Econst_int (Int.repr 1) tuint) :: nil))
(Ssequence
(Scall None
(Evar serial_out (Tfunction (Tcons tint (Tcons tuint Tnil))
tvoid cc_default))
((Ebinop Oadd (Econst_int (Int.repr 1016) tint)
(Econst_int (Int.repr 1) tint) tint) ::
(Econst_int (Int.repr 0) tuint) :: nil))
(Ssequence
(Scall None
(Evar serial_out (Tfunction (Tcons tint (Tcons tuint Tnil))
tvoid cc_default))
((Ebinop Oadd (Econst_int (Int.repr 1016) tint)
(Econst_int (Int.repr 3) tint) tint) ::
(Econst_int (Int.repr 3) tint) :: nil))
(Ssequence
(Scall None
(Evar serial_out (Tfunction (Tcons tint (Tcons tuint Tnil))
tvoid cc_default))
((Ebinop Oadd (Econst_int (Int.repr 1016) tint)
(Econst_int (Int.repr 2) tint) tint) ::
(Econst_int (Int.repr 199) tint) :: nil))
(Ssequence
(Scall None
(Evar serial_out (Tfunction
(Tcons tint (Tcons tuint Tnil)) tvoid
cc_default))
((Ebinop Oadd (Econst_int (Int.repr 1016) tint)
(Econst_int (Int.repr 4) tint) tint) ::
(Econst_int (Int.repr 11) tint) :: nil))
(Ssequence
(Ssequence
(Scall (Some ex)
(Evar serial_in (Tfunction
(Tcons tint (Tcons tuint Tnil))
tuint cc_default))
((Ebinop Oadd (Econst_int (Int.repr 1016) tint)
(Econst_int (Int.repr 5) tint) tint) ::
(Econst_int (Int.repr 0) tint) :: nil))
(Scall None
(Evar set_serial_exists (Tfunction (Tcons tuint Tnil)
tvoid cc_default))
((Ebinop One (Etempvar ex tuint)
(Econst_int (Int.repr 255) tint) tint) :: nil)))
(Ssequence
(Scall None
(Evar serial_in (Tfunction
(Tcons tint (Tcons tuint Tnil))
tuint cc_default))
((Ebinop Oadd (Econst_int (Int.repr 1016) tint)
(Econst_int (Int.repr 2) tint) tint) ::
(Econst_int (Int.repr 255) tint) :: nil))
(Scall None
(Evar serial_in (Tfunction
(Tcons tint (Tcons tuint Tnil))
tuint cc_default))
((Ebinop Oadd (Econst_int (Int.repr 1016) tint)
(Econst_int (Int.repr 0) tint) tint) ::
(Econst_int (Int.repr 255) tint) :: nil)))))))))))).
Definition f_serial_init := {|
fn_return := tvoid;
fn_callconv := cc_default;
fn_params := nil;
fn_vars := nil;
fn_temps := ((ex, tuchar) :: nil);
fn_body := serial_init_body
|}.
Definition _rv: ident := 4 % positive.
Definition _rx: ident := 5 % positive.
Definition serial_getc_body :=
(Ssequence
(Sset _rv (Econst_int (Int.repr 0) tint))
(Ssequence
(Ssequence
(Scall (Some 42%positive)
(Evar get_serial_exists (Tfunction Tnil tuint cc_default)) nil)
(Sifthenelse (Etempvar 42%positive tuint)
(Ssequence
(Scall (Some 41%positive)
(Evar serial_in (Tfunction (Tcons tint (Tcons tuint Tnil)) tuint
cc_default))
((Ebinop Oadd (Econst_int (Int.repr 1016) tint)
(Econst_int (Int.repr 5) tint) tint) ::
(Econst_int (Int.repr 1) tint) :: nil))
(Sifthenelse (Ebinop Oeq
(Ebinop Omod (Etempvar 41%positive tuint)
(Econst_int (Int.repr 2) tint) tuint)
(Econst_int (Int.repr 1) tint) tint)
(Ssequence
(Scall (Some _rx)
(Evar serial_in (Tfunction (Tcons tint (Tcons tuint Tnil))
tuint cc_default))
((Ebinop Oadd (Econst_int (Int.repr 1016) tint)
(Econst_int (Int.repr 0) tint) tint) ::
(Econst_int (Int.repr 255) tint) :: nil))
(Ssequence
(Scall None
(Evar cons_buf_write (Tfunction (Tcons tuint Tnil) tvoid
cc_default))
((Etempvar _rx tuint) :: nil))
(Sset _rv (Econst_int (Int.repr 1) tint))))
Sskip))
Sskip))
(Sreturn (Some (Etempvar _rv tuint))))).
Definition f_serial_getc := {|
fn_return := tuint;
fn_callconv := cc_default;
fn_params := nil;
fn_vars := nil;
fn_temps := ((_rv, tuint) :: (_rx, tuchar) ::
(42%positive, tuint) :: (41%positive, tuint) :: nil);
fn_body := serial_getc_body
|}.
Definition _lsr: ident := 6 % positive.
Definition _i: ident := 9 % positive.
Definition _c: ident := 10 % positive.
Definition serial_putc_loop_body :=
(Ssequence
(Sset _i
(Ebinop Oadd (Etempvar _i tuint)
(Econst_int (Int.repr 1) tuint) tuint))
(Ssequence
(Scall (Some 43%positive)
(Evar serial_in (Tfunction
(Tcons tint (Tcons tuint Tnil))
tuint cc_default))
((Ebinop Oadd (Econst_int (Int.repr 1016) tint)
(Econst_int (Int.repr 5) tint) tint) ::
(Econst_int (Int.repr 32) tint) :: nil))
(Sset _lsr
(Ebinop Omod
(Ebinop Odiv (Etempvar 43%positive tuint)
(Econst_int (Int.repr 32) tuint) tuint)
(Econst_int (Int.repr 2) tuint) tuint)))).
Definition serial_putc_loop_condition : expr :=
Ebinop Oand
(Ebinop Olt (Etempvar _i tuint) (Econst_int (Int.repr 12800) tuint) tint)
(Ebinop Oeq (Etempvar _lsr tuint) (Econst_int (Int.repr 0) tuint) tint)
tint.
Definition serial_putc_body :=
(Ssequence
(Scall (Some 44%positive)
(Evar get_serial_exists (Tfunction Tnil tuint cc_default)) nil)
(Sifthenelse (Etempvar 44%positive tuint)
(Ssequence
(Ssequence
(Scall (Some 41%positive)
(Evar serial_in (Tfunction (Tcons tint (Tcons tuint Tnil)) tuint
cc_default))
((Ebinop Oadd (Econst_int (Int.repr 1016) tint)
(Econst_int (Int.repr 5) tint) tint) ::
(Econst_int (Int.repr 32) tint) :: nil))
(Sset _lsr
(Ebinop Omod
(Ebinop Odiv (Etempvar 41%positive tuint)
(Econst_int (Int.repr 32) tuint) tuint)
(Econst_int (Int.repr 2) tuint) tuint)))
(Ssequence
(Sifthenelse (Ebinop Oeq (Etempvar _lsr tuint)
(Econst_int (Int.repr 0) tuint) tint)
(Ssequence
(Sset _i (Econst_int (Int.repr 0) tuint))
(Swhile serial_putc_loop_condition serial_putc_loop_body))
Sskip)
(Sifthenelse (Ebinop Oeq (Etempvar _c tuint)
(Econst_int (Int.repr 10) tint) tint)
(Ssequence
(Scall None
(Evar serial_out (Tfunction (Tcons tint (Tcons tuint Tnil))
tvoid cc_default))
((Ebinop Oadd (Econst_int (Int.repr 1016) tint)
(Econst_int (Int.repr 0) tint) tint) ::
(Econst_int (Int.repr 13) tint) :: nil))
(Scall None
(Evar serial_out (Tfunction (Tcons tint (Tcons tuint Tnil))
tvoid cc_default))
((Ebinop Oadd (Econst_int (Int.repr 1016) tint)
(Econst_int (Int.repr 0) tint) tint) ::
(Econst_int (Int.repr 10) tint) :: nil)))
(Scall None
(Evar serial_out (Tfunction (Tcons tint (Tcons tuint Tnil))
tvoid cc_default))
((Ebinop Oadd (Econst_int (Int.repr 1016) tint)
(Econst_int (Int.repr 0) tint) tint) :: (Etempvar _c tuint) ::
nil)))))
Sskip)).
Definition f_serial_putc :=
{|
fn_return := tvoid;
fn_callconv := cc_default;
fn_params := ((_c, tuint) :: nil);
fn_vars := nil;
fn_temps := ((_lsr, tuint) :: (_i, tuint) :: (44%positive, tuint) ::
(43%positive, tuint) :: (42%positive, tint) ::
(41%positive, tuint) :: nil);
fn_body := serial_putc_body
|}.
Require Import AST.
Require Import Integers.
Require Import Values.
Require Import Cop.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Definition ex: ident := 1 % positive.
Definition serial_init_body :=
(Ssequence
(Scall None
(Evar serial_out (Tfunction (Tcons tint (Tcons tuint Tnil)) tvoid
cc_default))
((Ebinop Oadd (Econst_int (Int.repr 1016) tint)
(Econst_int (Int.repr 3) tint) tint) ::
(Econst_int (Int.repr 0) tint) :: nil))
(Ssequence
(Scall None
(Evar serial_out (Tfunction (Tcons tint (Tcons tuint Tnil)) tvoid
cc_default))
((Ebinop Oadd (Econst_int (Int.repr 1016) tint)
(Econst_int (Int.repr 1) tint) tint) ::
(Econst_int (Int.repr 0) tint) :: nil))
(Ssequence
(Scall None
(Evar serial_out (Tfunction (Tcons tint (Tcons tuint Tnil)) tvoid
cc_default))
((Ebinop Oadd (Econst_int (Int.repr 1016) tint)
(Econst_int (Int.repr 3) tint) tint) ::
(Econst_int (Int.repr 128) tint) :: nil))
(Ssequence
(Scall None
(Evar serial_out (Tfunction (Tcons tint (Tcons tuint Tnil)) tvoid
cc_default))
((Ebinop Oadd (Econst_int (Int.repr 1016) tint)
(Econst_int (Int.repr 0) tint) tint) ::
(Econst_int (Int.repr 1) tuint) :: nil))
(Ssequence
(Scall None
(Evar serial_out (Tfunction (Tcons tint (Tcons tuint Tnil))
tvoid cc_default))
((Ebinop Oadd (Econst_int (Int.repr 1016) tint)
(Econst_int (Int.repr 1) tint) tint) ::
(Econst_int (Int.repr 0) tuint) :: nil))
(Ssequence
(Scall None
(Evar serial_out (Tfunction (Tcons tint (Tcons tuint Tnil))
tvoid cc_default))
((Ebinop Oadd (Econst_int (Int.repr 1016) tint)
(Econst_int (Int.repr 3) tint) tint) ::
(Econst_int (Int.repr 3) tint) :: nil))
(Ssequence
(Scall None
(Evar serial_out (Tfunction (Tcons tint (Tcons tuint Tnil))
tvoid cc_default))
((Ebinop Oadd (Econst_int (Int.repr 1016) tint)
(Econst_int (Int.repr 2) tint) tint) ::
(Econst_int (Int.repr 199) tint) :: nil))
(Ssequence
(Scall None
(Evar serial_out (Tfunction
(Tcons tint (Tcons tuint Tnil)) tvoid
cc_default))
((Ebinop Oadd (Econst_int (Int.repr 1016) tint)
(Econst_int (Int.repr 4) tint) tint) ::
(Econst_int (Int.repr 11) tint) :: nil))
(Ssequence
(Ssequence
(Scall (Some ex)
(Evar serial_in (Tfunction
(Tcons tint (Tcons tuint Tnil))
tuint cc_default))
((Ebinop Oadd (Econst_int (Int.repr 1016) tint)
(Econst_int (Int.repr 5) tint) tint) ::
(Econst_int (Int.repr 0) tint) :: nil))
(Scall None
(Evar set_serial_exists (Tfunction (Tcons tuint Tnil)
tvoid cc_default))
((Ebinop One (Etempvar ex tuint)
(Econst_int (Int.repr 255) tint) tint) :: nil)))
(Ssequence
(Scall None
(Evar serial_in (Tfunction
(Tcons tint (Tcons tuint Tnil))
tuint cc_default))
((Ebinop Oadd (Econst_int (Int.repr 1016) tint)
(Econst_int (Int.repr 2) tint) tint) ::
(Econst_int (Int.repr 255) tint) :: nil))
(Scall None
(Evar serial_in (Tfunction
(Tcons tint (Tcons tuint Tnil))
tuint cc_default))
((Ebinop Oadd (Econst_int (Int.repr 1016) tint)
(Econst_int (Int.repr 0) tint) tint) ::
(Econst_int (Int.repr 255) tint) :: nil)))))))))))).
Definition f_serial_init := {|
fn_return := tvoid;
fn_callconv := cc_default;
fn_params := nil;
fn_vars := nil;
fn_temps := ((ex, tuchar) :: nil);
fn_body := serial_init_body
|}.
Definition _rv: ident := 4 % positive.
Definition _rx: ident := 5 % positive.
Definition serial_getc_body :=
(Ssequence
(Sset _rv (Econst_int (Int.repr 0) tint))
(Ssequence
(Ssequence
(Scall (Some 42%positive)
(Evar get_serial_exists (Tfunction Tnil tuint cc_default)) nil)
(Sifthenelse (Etempvar 42%positive tuint)
(Ssequence
(Scall (Some 41%positive)
(Evar serial_in (Tfunction (Tcons tint (Tcons tuint Tnil)) tuint
cc_default))
((Ebinop Oadd (Econst_int (Int.repr 1016) tint)
(Econst_int (Int.repr 5) tint) tint) ::
(Econst_int (Int.repr 1) tint) :: nil))
(Sifthenelse (Ebinop Oeq
(Ebinop Omod (Etempvar 41%positive tuint)
(Econst_int (Int.repr 2) tint) tuint)
(Econst_int (Int.repr 1) tint) tint)
(Ssequence
(Scall (Some _rx)
(Evar serial_in (Tfunction (Tcons tint (Tcons tuint Tnil))
tuint cc_default))
((Ebinop Oadd (Econst_int (Int.repr 1016) tint)
(Econst_int (Int.repr 0) tint) tint) ::
(Econst_int (Int.repr 255) tint) :: nil))
(Ssequence
(Scall None
(Evar cons_buf_write (Tfunction (Tcons tuint Tnil) tvoid
cc_default))
((Etempvar _rx tuint) :: nil))
(Sset _rv (Econst_int (Int.repr 1) tint))))
Sskip))
Sskip))
(Sreturn (Some (Etempvar _rv tuint))))).
Definition f_serial_getc := {|
fn_return := tuint;
fn_callconv := cc_default;
fn_params := nil;
fn_vars := nil;
fn_temps := ((_rv, tuint) :: (_rx, tuchar) ::
(42%positive, tuint) :: (41%positive, tuint) :: nil);
fn_body := serial_getc_body
|}.
Definition _lsr: ident := 6 % positive.
Definition _i: ident := 9 % positive.
Definition _c: ident := 10 % positive.
Definition serial_putc_loop_body :=
(Ssequence
(Sset _i
(Ebinop Oadd (Etempvar _i tuint)
(Econst_int (Int.repr 1) tuint) tuint))
(Ssequence
(Scall (Some 43%positive)
(Evar serial_in (Tfunction
(Tcons tint (Tcons tuint Tnil))
tuint cc_default))
((Ebinop Oadd (Econst_int (Int.repr 1016) tint)
(Econst_int (Int.repr 5) tint) tint) ::
(Econst_int (Int.repr 32) tint) :: nil))
(Sset _lsr
(Ebinop Omod
(Ebinop Odiv (Etempvar 43%positive tuint)
(Econst_int (Int.repr 32) tuint) tuint)
(Econst_int (Int.repr 2) tuint) tuint)))).
Definition serial_putc_loop_condition : expr :=
Ebinop Oand
(Ebinop Olt (Etempvar _i tuint) (Econst_int (Int.repr 12800) tuint) tint)
(Ebinop Oeq (Etempvar _lsr tuint) (Econst_int (Int.repr 0) tuint) tint)
tint.
Definition serial_putc_body :=
(Ssequence
(Scall (Some 44%positive)
(Evar get_serial_exists (Tfunction Tnil tuint cc_default)) nil)
(Sifthenelse (Etempvar 44%positive tuint)
(Ssequence
(Ssequence
(Scall (Some 41%positive)
(Evar serial_in (Tfunction (Tcons tint (Tcons tuint Tnil)) tuint
cc_default))
((Ebinop Oadd (Econst_int (Int.repr 1016) tint)
(Econst_int (Int.repr 5) tint) tint) ::
(Econst_int (Int.repr 32) tint) :: nil))
(Sset _lsr
(Ebinop Omod
(Ebinop Odiv (Etempvar 41%positive tuint)
(Econst_int (Int.repr 32) tuint) tuint)
(Econst_int (Int.repr 2) tuint) tuint)))
(Ssequence
(Sifthenelse (Ebinop Oeq (Etempvar _lsr tuint)
(Econst_int (Int.repr 0) tuint) tint)
(Ssequence
(Sset _i (Econst_int (Int.repr 0) tuint))
(Swhile serial_putc_loop_condition serial_putc_loop_body))
Sskip)
(Sifthenelse (Ebinop Oeq (Etempvar _c tuint)
(Econst_int (Int.repr 10) tint) tint)
(Ssequence
(Scall None
(Evar serial_out (Tfunction (Tcons tint (Tcons tuint Tnil))
tvoid cc_default))
((Ebinop Oadd (Econst_int (Int.repr 1016) tint)
(Econst_int (Int.repr 0) tint) tint) ::
(Econst_int (Int.repr 13) tint) :: nil))
(Scall None
(Evar serial_out (Tfunction (Tcons tint (Tcons tuint Tnil))
tvoid cc_default))
((Ebinop Oadd (Econst_int (Int.repr 1016) tint)
(Econst_int (Int.repr 0) tint) tint) ::
(Econst_int (Int.repr 10) tint) :: nil)))
(Scall None
(Evar serial_out (Tfunction (Tcons tint (Tcons tuint Tnil))
tvoid cc_default))
((Ebinop Oadd (Econst_int (Int.repr 1016) tint)
(Econst_int (Int.repr 0) tint) tint) :: (Etempvar _c tuint) ::
nil)))))
Sskip)).
Definition f_serial_putc :=
{|
fn_return := tvoid;
fn_callconv := cc_default;
fn_params := ((_c, tuint) :: nil);
fn_vars := nil;
fn_temps := ((_lsr, tuint) :: (_i, tuint) :: (44%positive, tuint) ::
(43%positive, tuint) :: (42%positive, tint) ::
(41%positive, tuint) :: nil);
fn_body := serial_putc_body
|}.