Library mcertikos.proc.PCVIntroCSource

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 _i := 10%positive.
Definition _mbi_adr := 11%positive.

#define num_chan 16337

extern void init_sync_chan (unsigned int index);
extern void tdqueue_init (unsigned int mbi_adr);

void fifobbq_pool_init (unsigned int mbi_adr){
    unsigned int i;

    tdqueue_init(mbi_adr);

    i = 0;
    while (i < num_chan){
        init_sync_chan(i);
        i++;
    }   
}

Definition f_fifobbq_pool_init_while_condition :=
  (Ebinop Olt (Etempvar _i tuint) (Econst_int (Int.repr num_chan) tint) tint).

Definition f_fifobbq_pool_init_while_body :=
  (Ssequence
     (Scall None (Evar init_sync_chan (Tfunction (Tcons tuint Tnil) tvoid cc_default))
            ((Etempvar _i tuint) :: nil))
     (Sset _i (Ebinop Oadd (Etempvar _i tuint) (Econst_int (Int.repr 1) tint) tuint))).

Definition f_fifobbq_pool_init_body :=
  (Ssequence
     (Scall None
            (Evar tdqueue_init (Tfunction (Tcons tuint Tnil) tvoid cc_default))
            ((Etempvar _mbi_adr tuint) :: nil))
     (Ssequence
        (Sset _i (Econst_int (Int.repr 0) tint))
        (Swhile f_fifobbq_pool_init_while_condition
                f_fifobbq_pool_init_while_body))).

Definition f_fifobbq_pool_init :=
  {|
    fn_return := tvoid;
    fn_callconv := cc_default;
    fn_params := ((_mbi_adr, tuint) :: nil);
    fn_vars := nil;
    fn_temps := ((_i, tuint) :: nil);
    fn_body := f_fifobbq_pool_init_body
  |}.

    #define MAX_BUFFSIZE 1024

    unsigned int
    ipc_send_body(unsigned int chid, unsigned int sender_kpa, unsigned int scount)
    {
        //unsigned int myid = get_curid();
        //unsigned int sender_kpa = get_kernel_pa(myid, vaddr);

        //set_sync_chan_to(chid, myid);
        if (scount < MAX_BUFFSIZE) {
          //set_sync_chan_paddr(chid, sender_kpa);
          set_sync_chan_count(chid, scount);
          page_copy(chid, scount, vaddr);
          return scount;
        } else {
          //set_sync_chan_paddr(chid, sender_kpa);
          set_sync_chan_count(chid, MAX_BUFFSIZE);
          page_copy(chid, MAX_BUFFSIZE, sender_kpa);
          return MAX_BUFFSIZE;
        }
    }
Function parameters and local temporaries used in the function
Let _scount : ident := 40%positive.
Let _chid : ident := 38%positive.
Let _vaddr : ident := 39%positive.

Definition ipc_send_body_body :=
  (Sifthenelse (Ebinop Olt (Etempvar _scount tuint)
                       (Econst_int (Int.repr 1024) tint) tint)
               (Ssequence
                  (Scall None
                         (Evar set_sync_chan_count (Tfunction
                                                      (Tcons tuint (Tcons tuint Tnil))
                                                      tvoid cc_default))
                         ((Etempvar _chid tuint) :: (Etempvar _scount tuint) :: nil))
                  (Ssequence
                     (Scall None
                            (Evar page_copy (Tfunction
                                               (Tcons tuint
                                                      (Tcons tuint (Tcons tuint Tnil))) tvoid
                                               cc_default))
                            ((Etempvar _chid tuint) :: (Etempvar _scount tuint) ::
                                                    (Etempvar _vaddr tuint) :: nil))
                     (Sreturn (Some (Etempvar _scount tuint)))))
               (Ssequence
                  (Scall None
                         (Evar set_sync_chan_count (Tfunction
                                                      (Tcons tuint (Tcons tuint Tnil))
                                                      tvoid cc_default))
                         ((Etempvar _chid tuint) :: (Econst_int (Int.repr 1024) tint) ::
                                                 nil))
                  (Ssequence
                     (Scall None
                            (Evar page_copy (Tfunction
                                               (Tcons tuint
                                                      (Tcons tuint (Tcons tuint Tnil))) tvoid
                                               cc_default))
                            ((Etempvar _chid tuint) ::
                                                    (Econst_int (Int.repr 1024) tint) ::
                                                    (Etempvar _vaddr tuint) :: nil))
                     (Sreturn (Some (Econst_int (Int.repr 1024) tint)))))).

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

    #define NUM_PROC 1204

    unsigned int
    ipc_receive_body(unsigned int chid, unsigned int vaddr, unsigned int rcount)
    {
      //unsigned int myid = get_curid();
      unsigned int sender_count = get_sync_chan_count(chid);
      unsigned int arecvcount = (sender_count < rcount) ? sender_count : rcount;
      //unsigned int rbuffpa = get_kernel_pa(myid, vaddr);

      page_copy_back(chid, arecvcount, vaddr);

      //set_sync_chan_to(chid, NUM_PROC);
      //set_sync_chan_paddr(chid, 0);
      set_sync_chan_count(chid, 0);

      return arecvcount;
    }
Function parameters and local temporaries used in the function
Let _senderid : ident := 146%positive.
Let _rcount : ident := 143%positive.
Let _arecvcount : ident := 147%positive.
Let _sender_count : ident := 15%positive.

Definition ipc_receive_body_body :=
  (Ssequence
     (Scall (Some _sender_count)
            (Evar get_sync_chan_count (Tfunction (Tcons tuint Tnil) tuint
                                                 cc_default))
            ((Etempvar _chid tuint) :: nil))
     (Ssequence
        (Sifthenelse (Ebinop Olt (Etempvar _sender_count tuint)
                             (Etempvar _rcount tuint) tint)
                     (Sset _arecvcount (Ecast (Etempvar _sender_count tuint) tuint))
                     (Sset _arecvcount (Ecast (Etempvar _rcount tuint) tuint)))
        (Ssequence
           (Scall None
                  (Evar page_copy_back (Tfunction
                                          (Tcons tuint
                                                 (Tcons tuint (Tcons tuint Tnil))) tvoid
                                          cc_default))
                  ((Etempvar _chid tuint) :: (Etempvar _arecvcount tuint) ::
                                          (Etempvar _vaddr tuint) :: nil))
           (Ssequence
              (Scall None
                     (Evar set_sync_chan_count (Tfunction
                                                  (Tcons tuint
                                                         (Tcons tuint Tnil)) tvoid
                                                  cc_default))
                     ((Etempvar _chid tuint) ::
                                             (Econst_int (Int.repr 0) tint) :: nil))
              (Sreturn (Some (Etempvar _arecvcount tuint))))))).

Definition f_ipc_receive_body :=
  {|
    fn_return := tuint;
    fn_callconv := cc_default;
    fn_params := ((_chid, tuint) :: (_vaddr, tuint) :: (_rcount, tuint) :: nil);
    fn_vars := nil;
    fn_temps := ((_sender_count, tuint) ::
                                        (_arecvcount, tuint) :: nil);
    fn_body := ipc_receive_body_body
  |}.

    #define num_cv 255
    #define num_proc 1024

    void
    idq_push(unsigned int chid, unsigned int qid, unsigned int tid)
    {
      unsigned int h;
      unsigned int t;

      h = fifobbq_get_head(chid, qid);
      if (h == num_proc)
      {
        fifobbq_set_head(chid, qid, tid);
        fifobbq_set_tail(chid, qid, tid);
      }
      else
      {
        t = fifobbq_get_tail(chid, qid);
        fifobbq_set_head(chid, qid, h);
        fifobbq_set_tail(chid, qid, tid);
        idq_set_next(t, tid);
        idq_set_prev(tid, t);
        idq_set_next(tid, num_proc);
      }
    }


Let _qid := 1001 % positive.
Let _tid := 1002 % positive.
Let _h := 1003 % positive.
Let _t := 1004 % positive.

Definition idq_push_body :=
  (Ssequence
    (Scall (Some _h)
      (Evar fifobbq_get_head (Tfunction (Tcons tuint (Tcons tuint Tnil))
                                tuint cc_default))
      ((Etempvar _chid tuint) :: (Etempvar _qid tuint) :: nil))
  (Sifthenelse (Ebinop Oeq (Etempvar _h tuint)
                 (Econst_int (Int.repr num_proc) tint) tint)
    (Ssequence
      (Scall None
        (Evar fifobbq_set_head (Tfunction
                                  (Tcons tuint
                                    (Tcons tuint (Tcons tuint Tnil))) tvoid
                                  cc_default))
        ((Etempvar _chid tuint) :: (Etempvar _qid tuint) ::
         (Etempvar _tid tuint) :: nil))
      (Scall None
        (Evar fifobbq_set_tail (Tfunction
                                  (Tcons tuint
                                    (Tcons tuint (Tcons tuint Tnil))) tvoid
                                  cc_default))
        ((Etempvar _chid tuint) :: (Etempvar _qid tuint) ::
         (Etempvar _tid tuint) :: nil)))
    (Ssequence
        (Scall (Some _t)
          (Evar fifobbq_get_tail (Tfunction (Tcons tuint (Tcons tuint Tnil))
                                    tuint cc_default))
          ((Etempvar _chid tuint) :: (Etempvar _qid tuint) :: nil))
      (Ssequence
        (Scall None
          (Evar fifobbq_set_head (Tfunction
                                    (Tcons tuint
                                      (Tcons tuint (Tcons tuint Tnil))) tvoid
                                    cc_default))
          ((Etempvar _chid tuint) :: (Etempvar _qid tuint) ::
           (Etempvar _h tuint) :: nil))
        (Ssequence
          (Scall None
            (Evar fifobbq_set_tail (Tfunction
                                      (Tcons tuint
                                        (Tcons tuint (Tcons tuint Tnil)))
                                      tvoid cc_default))
            ((Etempvar _chid tuint) :: (Etempvar _qid tuint) ::
             (Etempvar _tid tuint) :: nil))
          (Ssequence
            (Scall None
              (Evar idq_set_next (Tfunction (Tcons tuint (Tcons tuint Tnil))
                                    tvoid cc_default))
              ((Etempvar _t tuint) :: (Etempvar _tid tuint) :: nil))
            (Ssequence
              (Scall None
                (Evar idq_set_prev (Tfunction
                                      (Tcons tuint (Tcons tuint Tnil)) tvoid
                                      cc_default))
                ((Etempvar _tid tuint) :: (Etempvar _t tuint) :: nil))
              (Scall None
                (Evar idq_set_next (Tfunction
                                      (Tcons tuint (Tcons tuint Tnil)) tvoid
                                      cc_default))
                ((Etempvar _tid tuint) :: (Econst_int (Int.repr num_proc) tint) ::
                 nil))))))))).

Definition f_idq_push := {|
  fn_return := tvoid;
  fn_callconv := cc_default;
  fn_params := ((_chid, tuint) :: (_qid, tuint) :: (_tid, tuint) :: nil);
  fn_vars := nil;
  fn_temps := ((_h, tuint) :: (_t, tuint) :: nil);
  fn_body := idq_push_body
|}.

    #define num_cv 255
    #define num_proc 1024

    unsigned int
    idq_pull(unsigned int chid, unsigned int qid)
    {
      unsigned int h;
      unsigned int t;
      unsigned int n;

      h = fifobbq_get_head(chid, qid);
      t = fifobbq_get_tail(chid, qid);
      if (h == t)
      {
        fifobbq_set_head(chid, qid, num_proc);
        fifobbq_set_tail(chid, qid, num_proc);
      }
      else
      {
        n = idq_get_next(h);
        fifobbq_set_head(chid, qid, n);
        fifobbq_set_tail(chid, qid, t);
      }
      return h;
    }


Let _n := 1005 % positive.

Definition idq_pull_body :=
  (Ssequence
    (Scall (Some _h)
      (Evar fifobbq_get_head (Tfunction (Tcons tuint (Tcons tuint Tnil))
                                tuint cc_default))
      ((Etempvar _chid tuint) :: (Etempvar _qid tuint) :: nil))
  (Ssequence
      (Scall (Some _t)
        (Evar fifobbq_get_tail (Tfunction (Tcons tuint (Tcons tuint Tnil))
                                  tuint cc_default))
        ((Etempvar _chid tuint) :: (Etempvar _qid tuint) :: nil))
    (Ssequence
      (Sifthenelse (Ebinop Oeq (Etempvar _h tuint) (Etempvar _t tuint) tint)
        (Ssequence
          (Scall None
            (Evar fifobbq_set_head (Tfunction
                                      (Tcons tuint
                                        (Tcons tuint (Tcons tuint Tnil)))
                                      tvoid cc_default))
            ((Etempvar _chid tuint) :: (Etempvar _qid tuint) ::
             (Econst_int (Int.repr num_proc) tint) :: nil))
          (Scall None
            (Evar fifobbq_set_tail (Tfunction
                                      (Tcons tuint
                                        (Tcons tuint (Tcons tuint Tnil)))
                                      tvoid cc_default))
            ((Etempvar _chid tuint) :: (Etempvar _qid tuint) ::
             (Econst_int (Int.repr num_proc) tint) :: nil)))
        (Ssequence
            (Scall (Some _n)
              (Evar idq_get_next (Tfunction (Tcons tuint Tnil) tuint
                                    cc_default))
              ((Etempvar _h tuint) :: nil))
          (Ssequence
            (Scall None
              (Evar fifobbq_set_head (Tfunction
                                        (Tcons tuint
                                          (Tcons tuint (Tcons tuint Tnil)))
                                        tvoid cc_default))
              ((Etempvar _chid tuint) :: (Etempvar _qid tuint) ::
               (Etempvar _n tuint) :: nil))
            (Scall None
              (Evar fifobbq_set_tail (Tfunction
                                        (Tcons tuint
                                          (Tcons tuint (Tcons tuint Tnil)))
                                        tvoid cc_default))
              ((Etempvar _chid tuint) :: (Etempvar _qid tuint) ::
               (Etempvar _t tuint) :: nil)))))
      (Sreturn (Some (Etempvar _h tuint)))))).

Definition f_idq_pull := {|
  fn_return := tuint;
  fn_callconv := cc_default;
  fn_params := ((_chid, tuint) :: (_qid, tuint) :: nil);
  fn_vars := nil;
  fn_temps := ((_h, tuint) :: (_t, tuint) :: (_n, tuint) :: nil);
  fn_body := idq_pull_body
|}.

    unsigned int
    idq_peek(unsigned int chid, unsigned int qid)
    {
      unsigned int h;

      h = fifobbq_get_head(chid, qid);
      return h;
    }


Definition idq_peek_body :=
  (Ssequence
    (Scall (Some _h)
      (Evar fifobbq_get_head (Tfunction (Tcons tuint (Tcons tuint Tnil))
                                tuint cc_default))
      ((Etempvar _chid tuint) :: (Etempvar _qid tuint) :: nil))
  (Sreturn (Some (Etempvar _h tuint)))).

Definition f_idq_peek := {|
  fn_return := tuint;
  fn_callconv := cc_default;
  fn_params := ((_chid, tuint) :: (_qid, tuint) :: nil);
  fn_vars := nil;
  fn_temps := ((_h, tuint) :: nil);
  fn_body := idq_peek_body
|}.