Library mcertikos.proc.PAbQueueAtomicCSource

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

Notation _ih := 65%positive.
Notation _in_head := 40%positive.
Notation _out_head := 38%positive.
Notation _to := 46%positive.
Notation _count := 44%positive.
Notation _cv := 49%positive.
Notation _va := 59%positive.
Notation _pid := 58%positive.
Notation _paddr := 45%positive.
Notation _kpa := 60%positive.
Notation _idq := 50%positive.
Notation _struct_cv_t := 43%positive.
Notation _chanid := 53%positive.
Notation _struct_chpool_t := 47%positive.
Notation _struct_idQ_t := 36%positive.
Notation _in_tail := 39%positive.
Notation _out_tail := 37%positive.
Notation _max := 42%positive.
Notation _front := 41%positive.
Notation _next := 34%positive.
Notation _prev := 35%positive.
Notation _struct_sync_chpool_t := 51%positive.
Notation _chpool := 48%positive.
Notation _kpa´ := 79%positive.
Notation _n_to := 100%positive.
Notation _n_paddr := 101%positive.
Notation _n_count := 101%positive.
Notation _busy := 111%positive.
Notation _n_busy := 112%positive.

Definition t_struct_chpool_t :=
  (Tstruct _struct_chpool_t
           (Fcons _to tuint (Fcons _paddr tuint (Fcons _count tuint (Fcons _busy tuint Fnil)))) noattr).

Definition syncchpool_loc_type : globvar type :=
  {|
    gvar_info := (tarray t_struct_chpool_t num_chan);
    gvar_init := (Init_space (num_chan × 16) :: nil);
    gvar_readonly := false;
    gvar_volatile := false
  |}.

unsigned int get_sync_chan_to(unsigned int chanid) { return SYNCCHPOOL_LOCchanid.to; }

Definition f_get_sync_chan_to_body :=
  (Sreturn (Some (Efield
                    (Ederef
                       (Ebinop Oadd
                               (Evar SYNCCHPOOL_LOC (tarray t_struct_chpool_t num_chan))
                               (Etempvar _chanid tuint) (tptr t_struct_chpool_t))
                       t_struct_chpool_t) _to tuint))).

Definition f_get_sync_chan_to :=
  {|
    fn_return := tuint;
    fn_callconv := cc_default;
    fn_params := ((_chanid, tuint) :: nil);
    fn_vars := nil;
    fn_temps := nil;
    fn_body := f_get_sync_chan_to_body
  |}.

unsigned int get_sync_chan_paddr(unsigned int chanid) { return SYNCCHPOOL_LOC.chpoolchanid.paddr; }

Definition f_get_sync_chan_paddr_body :=
  (Sreturn (Some (Efield
                    (Ederef
                       (Ebinop Oadd
                               (Evar SYNCCHPOOL_LOC (tarray t_struct_chpool_t num_chan))
                               (Etempvar _chanid tuint) (tptr t_struct_chpool_t))
                       t_struct_chpool_t) _paddr tuint))).

Definition f_get_sync_chan_paddr :=
  {|
    fn_return := tuint;
    fn_callconv := cc_default;
    fn_params := ((_chanid, tuint) :: nil);
    fn_vars := nil;
    fn_temps := nil;
  fn_body := f_get_sync_chan_paddr_body
  |}.

unsigned int get_sync_chan_count(unsigned int chanid) { return SYNCCHPOOL_LOCchanid.count; }

Definition f_get_sync_chan_count_body :=
  (Sreturn (Some (Efield
                    (Ederef
                       (Ebinop Oadd
                               (Evar SYNCCHPOOL_LOC (tarray t_struct_chpool_t num_chan))
                               (Etempvar _chanid tuint) (tptr t_struct_chpool_t))
                       t_struct_chpool_t) _count tuint))).

Definition f_get_sync_chan_count :=
  {|
    fn_return := tuint;
    fn_callconv := cc_default;
    fn_params := ((_chanid, tuint) :: nil);
    fn_vars := nil;
    fn_temps := nil;
    fn_body := f_get_sync_chan_count_body
  |}.

unsigned int get_sync_chan_busy(unsigned int chanid) { return SYNCCHPOOL_LOCchanid.busy; }

Definition f_get_sync_chan_busy_body :=
  (Sreturn (Some (Efield
                    (Ederef
                       (Ebinop Oadd
                               (Evar SYNCCHPOOL_LOC (tarray t_struct_chpool_t num_chan))
                               (Etempvar _chanid tuint) (tptr t_struct_chpool_t))
                       t_struct_chpool_t) _busy tuint))).

Definition f_get_sync_chan_busy :=
  {|
    fn_return := tuint;
    fn_callconv := cc_default;
    fn_params := ((_chanid, tuint) :: nil);
    fn_vars := nil;
    fn_temps := nil;
    fn_body := f_get_sync_chan_busy_body
  |}.

void set_sync_chan_to(unsigned int chanid, unsigned int n_to) { SYNCCHPOOL_LOCchanid.to = n_to; }

Definition f_set_sync_chan_to_body :=
(Sassign
  (Efield
    (Ederef
      (Ebinop Oadd
        (Evar SYNCCHPOOL_LOC (tarray t_struct_chpool_t num_chan)) (Etempvar _chanid tuint)
        (tptr t_struct_chpool_t)) t_struct_chpool_t) _to tuint)
  (Etempvar _n_to tuint)).

Definition f_set_sync_chan_to :=
  {|
    fn_return := tvoid;
    fn_callconv := cc_default;
    fn_params := ((_chanid, tuint) :: (_n_to, tuint) :: nil);
    fn_vars := nil;
    fn_temps := nil;
    fn_body := f_set_sync_chan_to_body
  |}.

void set_sync_chan_paddr(unsigned int chanid, unsigned int n_paddr) { SYNCCHPOOL_LOCchanid.paddr = n_paddr; }

Definition f_set_sync_chan_paddr_body :=
  (Sassign
     (Efield
        (Ederef
           (Ebinop Oadd
                   (Evar SYNCCHPOOL_LOC (tarray t_struct_chpool_t num_chan)) (Etempvar _chanid tuint)
                   (tptr t_struct_chpool_t)) t_struct_chpool_t) _paddr tuint)
     (Etempvar _n_paddr tuint)).

Definition f_set_sync_chan_paddr :=
  {|
    fn_return := tvoid;
    fn_callconv := cc_default;
    fn_params := ((_chanid, tuint) :: (_n_paddr, tuint) :: nil);
    fn_vars := nil;
    fn_temps := nil;
    fn_body := f_set_sync_chan_paddr_body
  |}.

void set_sync_chan_count(unsigned int chanid, unsigned int n_count) { SYNCCHPOOL_LOCchanid.count = n_count; }

Definition f_set_sync_chan_count_body :=
(Sassign
  (Efield
    (Ederef
      (Ebinop Oadd
        (Evar SYNCCHPOOL_LOC (tarray t_struct_chpool_t num_chan)) (Etempvar _chanid tuint)
        (tptr t_struct_chpool_t)) t_struct_chpool_t) _count tuint)
  (Etempvar _n_count tuint)).

Definition f_set_sync_chan_count :=
  {|
    fn_return := tvoid;
    fn_callconv := cc_default;
    fn_params := ((_chanid, tuint) :: (_n_count, tuint) :: nil);
    fn_vars := nil;
    fn_temps := nil;
    fn_body := f_set_sync_chan_count_body
  |}.

void set_sync_chan_busy(unsigned int chanid, unsigned int n_busy) { SYNCCHPOOL_LOCchanid.busy = n_busy; }

Definition f_set_sync_chan_busy_body :=
  (Sassign
     (Efield
        (Ederef
           (Ebinop Oadd
                   (Evar SYNCCHPOOL_LOC (tarray t_struct_chpool_t num_chan)) (Etempvar _chanid tuint)
                   (tptr t_struct_chpool_t)) t_struct_chpool_t) _busy tuint)
     (Etempvar _n_busy tuint)).

Definition f_set_sync_chan_busy :=
  {|
    fn_return := tvoid;
    fn_callconv := cc_default;
    fn_params := ((_chanid, tuint) :: (_n_busy, tuint) :: nil);
    fn_vars := nil;
    fn_temps := nil;
    fn_body := f_set_sync_chan_busy_body
  |}.

void init_sync_chan(unsigned int chanid) { SYNCCHPOOL_LOCchanid.to = num_chan; SYNCCHPOOL_LOCchanid.paddr = 0; SYNCCHPOOL_LOCchanid.count = 0; SYNCCHPOOL_LOCchanid.busy = 0; }

Definition f_init_sync_chan_body :=
  (Ssequence
     (Sassign
        (Efield
           (Ederef
              (Ebinop Oadd (Evar SYNCCHPOOL_LOC (tarray t_struct_chpool_t num_chan))
                      (Etempvar _chanid tuint) (tptr t_struct_chpool_t))
              t_struct_chpool_t) _to tuint) (Econst_int (Int.repr num_chan) tint))
     (Ssequence
        (Sassign
           (Efield
              (Ederef
                 (Ebinop Oadd
                         (Evar SYNCCHPOOL_LOC (tarray t_struct_chpool_t num_chan))
                         (Etempvar _chanid tuint) (tptr t_struct_chpool_t))
                 t_struct_chpool_t) _paddr tuint) (Econst_int (Int.repr 0) tint))
        (Ssequence
           (Sassign
              (Efield
                 (Ederef
                    (Ebinop Oadd
                            (Evar SYNCCHPOOL_LOC (tarray t_struct_chpool_t num_chan))
                            (Etempvar _chanid tuint) (tptr t_struct_chpool_t))
                    t_struct_chpool_t) _count tuint) (Econst_int (Int.repr 0) tint))
           (Sassign
              (Efield
                 (Ederef
                    (Ebinop Oadd
                            (Evar SYNCCHPOOL_LOC (tarray t_struct_chpool_t num_chan))
                            (Etempvar _chanid tuint) (tptr t_struct_chpool_t))
                    t_struct_chpool_t) _busy tuint) (Econst_int (Int.repr 0) tint))))).

Definition f_init_sync_chan :=
  {|
    fn_return := tvoid;
    fn_callconv := cc_default;
    fn_params := ((_chanid, tuint) :: nil);
    fn_vars := nil;
    fn_temps := nil;
    fn_body := f_init_sync_chan_body
  |}.

extern unsigned int pt_read(unsigned int pid, unsigned int vaddr);

unsigned int get_kernel_pa(unsigned int pid, unsigned int va) { unsigned int kpa = pt_read(pid, va); kpa = kpa / PAGESIZE * PAGESIZE + va