Library mcertikos.proc.PKContextNewCSource

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 _cpuid := 50%positive.
Notation _to := 60%positive.
Notation _sl := 70%positive.

#define TOTAL_CPU 8

extern unsigned int get_CPU_ID(void);

unsigned int SLEEPER_LOC[TOTAL_CPU];

unsigned int sleeper_zzz(void)
{
    unsigned int cpuid, to;

    cpuid = get_CPU_ID();
    to = SLEEPER_LOC[cpuid];

    if(to == 0){
        return 1;
    } else {
        return 0;
    }
}

Definition f_sleeper_zzz_body :=
(Ssequence
   (Scall (Some _cpuid) (Evar get_CPU_ID (Tfunction Tnil tuint cc_default)) nil)
  (Ssequence
    (Sset _to
      (Ederef
        (Ebinop Oadd (Evar SLEEPER_LOC (tarray tuint 8))
          (Etempvar _cpuid tuint) (tptr tuint)) tuint))
    (Sifthenelse (Ebinop Oeq (Etempvar _to tuint)
                   (Econst_int (Int.repr 0) tint) tint)
      (Sreturn (Some (Econst_int (Int.repr 1) tint)))
      (Sreturn (Some (Econst_int (Int.repr 0) tint)))))).

Definition f_sleeper_zzz := {|
  fn_return := tuint;
  fn_callconv := cc_default;
  fn_params := nil;
  fn_vars := nil;
  fn_temps := ((_cpuid, tuint) :: (_to, tuint) :: nil);
  fn_body := f_sleeper_zzz_body
|}.

#define TOTAL_CPU 8

extern unsigned int get_curid(void);

unsigned int SLEEPER_LOC[num_proc];

void sleeper_inc(void)
{
    unsigned int tid, sl;

    cpuid = get_CPU_ID();

    sl = SLEEPER_LOC[cpuid];
    SLEEPER_LOC[cpuid] = sl + 1;
}

Definition f_sleeper_inc_body :=
(Ssequence
   (Scall (Some _cpuid) (Evar get_CPU_ID (Tfunction Tnil tuint cc_default)) nil)
  (Ssequence
    (Sset _sl
      (Ederef
        (Ebinop Oadd (Evar SLEEPER_LOC (tarray tuint 8))
          (Etempvar _cpuid tuint) (tptr tuint)) tuint))
    (Sassign
      (Ederef
        (Ebinop Oadd (Evar SLEEPER_LOC (tarray tuint 8))
          (Etempvar _cpuid tuint) (tptr tuint)) tuint)
      (Ebinop Oadd (Etempvar _sl tuint) (Econst_int (Int.repr 1) tint) tuint)))).

Definition f_sleeper_inc := {|
  fn_return := tvoid;
  fn_callconv := cc_default;
  fn_params := nil;
  fn_vars := nil;
  fn_temps := ((_cpuid, tuint) :: (_sl, tuint) :: nil);
  fn_body := f_sleeper_inc_body
|}.

#define TOTAL_CPU 8

extern unsigned int get_curid(void);

unsigned int SLEEPER_LOC[TOTAL_CPU];


void sleeper_dec(void)
{
    unsigned int cpuid, sl;

    cpuid = get_curid();

    sl = SLEEPER_LOC[cpuid];
    SLEEPER_LOC[cpuid] = sl - 1;
}

Definition f_sleeper_dec_body :=
  (Ssequence
     (Scall (Some _cpuid) (Evar get_CPU_ID (Tfunction Tnil tuint cc_default)) nil)
     (Ssequence
        (Sset _sl
              (Ederef
                 (Ebinop Oadd (Evar SLEEPER_LOC (tarray tuint 8))
                         (Etempvar _cpuid tuint) (tptr tuint)) tuint))
        (Sassign
           (Ederef
              (Ebinop Oadd (Evar SLEEPER_LOC (tarray tuint 8))
                      (Etempvar _cpuid tuint) (tptr tuint)) tuint)
           (Ebinop Osub (Etempvar _sl tuint) (Econst_int (Int.repr 1) tint) tuint)))).

Definition f_sleeper_dec := {|
  fn_return := tvoid;
  fn_callconv := cc_default;
  fn_params := nil;
  fn_vars := nil;
  fn_temps := ((_cpuid, tuint) :: (_sl, tuint) :: nil);
  fn_body := f_sleeper_dec_body
|}.