Library mcertikos.ipc.PIPCIntroCSource

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

      extern void syncsendto_chan_pre(unsigned int);
      extern unsigned int ipc_send_body(unsigned int, unsigned int, unsigned int);
      extern void release_lock_CHAN(unsigned int);

      unsigned int
      syncsendto_chan(unsigned int chid, unsigned int vaddr, unsigned int scount)
      {
        unsigned int res;
        syncsendto_chan_pre(chid);
        chid = SLEEP_Q_START + chid;
        res = ipc_send_body(chid, vaddr, scount);
        release_lock_CHAN(chid);
        return res;
      }
Function parameters and local temporaries used in the function
Local Open Scope positive_scope.
Let _chid: ident := 1.
Let _vaddr: ident := 2.
Let _scount: ident := 3.
Let _res: ident := 4.

Local Open Scope Z_scope.

Definition syncsendto_chan_body : statement :=
  (Ssequence
  (Scall None
    (Evar syncsendto_chan_pre (Tfunction (Tcons tuint Tnil) tvoid
                                 cc_default))
    ((Etempvar _chid tuint) :: nil))
  (Ssequence
    (Sset _chid
      (Ebinop Oadd
        (Ebinop Oadd
          (Ebinop Oadd (Econst_int (Int.repr 0) tint)
            (Econst_int (Int.repr TOTAL_CPU) tint) tint)
        (Econst_int (Int.repr TOTAL_CPU) tint) tint) (Etempvar _chid tuint) tuint))
    (Ssequence
        (Scall (Some _res)
          (Evar ipc_send_body (Tfunction
                                 (Tcons tuint
                                   (Tcons tuint (Tcons tuint Tnil))) tuint
                                 cc_default))
          ((Etempvar _chid tuint) :: (Etempvar _vaddr tuint) ::
           (Etempvar _scount tuint) :: nil))
      (Ssequence
        (Scall None
          (Evar release_lock_CHAN (Tfunction (Tcons tuint Tnil) tvoid
                                     cc_default))
          ((Etempvar _chid tuint) :: nil))
        (Sreturn (Some (Etempvar _res tuint))))))).

Definition f_syncsendto_chan := {|
                                 fn_return := tuint;
                                 fn_callconv := cc_default;
                                 fn_params := ((_chid, tuint) :: (_vaddr, tuint) :: (_scount, tuint) :: nil);
                                 fn_vars := nil;
                                 fn_temps := ((_res, tuint) :: nil);
                                 fn_body := syncsendto_chan_body
                               |}.


extern unsigned int get_curid(void);
extern unsigned int tryreceive_chan(unsigned int, unsigned int);
extern void acquire_lock_CHAN(unsigned int);
extern void release_lock_CHAN(unsigned int);

unsigned int
syncreceive_chan(unsigned int chid, unsigned int vaddr, unsigned int rcount)
{
  unsigned int res, chanid;
  chanid = SLEEP_Q_START + chid;
  acquire_lock_CHAN(chanid);
  res = tryreceive_chan(chid, vaddr, rcount);
  release_lock_CHAN(chanid);
  return res;
}

Local Open Scope positive_scope.

Definition _rcount : ident := 8.
Definition _curid : ident := 11.
Definition _chanid : ident := 111.

Definition syncreceive_chan_body : statement :=
  (Ssequence
  (Sset _chanid
    (Ebinop Oadd
      (Ebinop Oadd
        (Ebinop Oadd (Econst_int (Int.repr 0) tint)
          (Econst_int (Int.repr 8) tint) tint) (Econst_int (Int.repr 8) tint)
        tint) (Etempvar _chid tuint) tuint))
  (Ssequence
    (Scall None
      (Evar acquire_lock_CHAN (Tfunction (Tcons tuint Tnil) tvoid
                                 cc_default))
      ((Etempvar _chanid tuint) :: nil))
    (Ssequence
        (Scall (Some _res)
          (Evar tryreceive_chan (Tfunction
                                   (Tcons tuint
                                     (Tcons tuint (Tcons tuint Tnil))) tuint
                                   cc_default))
          ((Etempvar _chid tuint) :: (Etempvar _vaddr tuint) ::
           (Etempvar _rcount tuint) :: nil))
      (Ssequence
        (Scall None
          (Evar release_lock_CHAN (Tfunction (Tcons tuint Tnil) tvoid
                                     cc_default))
          ((Etempvar _chanid tuint) :: nil))
        (Sreturn (Some (Etempvar _res tuint))))))).

Definition f_syncreceive_chan :=
  {|
    fn_return := tuint;
    fn_callconv := cc_default;
    fn_params := ((_chid, tuint) :: (_vaddr, tuint) :: (_rcount, tuint) :: nil);
    fn_vars := nil;
    fn_temps := ((_res, tuint) :: (_chanid, tuint) :: nil);
    fn_body := syncreceive_chan_body
  |}.