Library mcertikos.ticketlog.MCurIDCSource

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


Definition ticket_lock_struct := 15%positive.
Definition tl_next := 16%positive.
Definition tl_now := 17%positive.
Definition _lock_id := 18%positive.
Definition _offset := 19%positive.
Definition _lock_loc := 20%positive.

Notation t_ticket_lock_struct :=
  (Tstruct ticket_lock_struct (Fcons tl_next tuint (Fcons tl_now tuint Fnil))
           noattr).

Notation ticket_lock_type :=
  {|
    gvar_info := (tarray t_ticket_lock_struct lock_range);
    gvar_init := (Init_space (lock_range × 8) :: nil);
    gvar_readonly := false;
    gvar_volatile := false
  |}.

Notation f_incr_now_body :=
  (Ssequence
     (Scall None
            (Evar log_incr (Tfunction
                              (Tcons tuint (Tcons tuint Tnil)) tvoid cc_default))
            ((Etempvar _lock_id tuint) :: (Etempvar _offset tuint) :: nil))
     (Ssequence
        (Sifthenelse (Ebinop Oeq (Etempvar _lock_id tuint)
                             (Econst_int (Int.repr 0) tint) tint)
                     (Sset _lock_loc
                           (Ebinop Oadd (Econst_int (Int.repr 0) tint)
                                   (Etempvar _offset tuint) tuint))
                     (Sifthenelse (Ebinop Oeq (Etempvar _lock_id tuint)
                                          (Econst_int (Int.repr 1) tint) tint)
                                  (Sset _lock_loc
                                        (Ebinop Oadd
                                                (Ebinop Oadd (Econst_int (Int.repr 0) tint)
                                                        (Econst_int (Int.repr 1) tint) tint) (Etempvar _offset tuint)
                                                tuint))
                                  (Sifthenelse (Ebinop Oeq (Etempvar _lock_id tuint)
                                                       (Econst_int (Int.repr 2) tint) tint)
                                               (Sset _lock_loc
                                                     (Ebinop Oadd
                                                             (Ebinop Oadd
                                                                     (Ebinop Oadd (Econst_int (Int.repr 0) tint)
                                                                             (Econst_int (Int.repr 1) tint) tint)
                                                                     (Econst_int (Int.repr num_chan) tint) tint)
                                                             (Etempvar _offset tuint) tuint))
                                               (Sset _lock_loc (Econst_int (Int.repr 12345678) tint)))))
        (Sassign
           (Efield
              (Ederef
                 (Ebinop Oadd
                         (Evar TICKET_LOCK_LOC (tarray t_ticket_lock_struct 32675))
                         (Etempvar _lock_loc tint) (tptr t_ticket_lock_struct))
                 t_ticket_lock_struct) tl_now tint)
           (Ebinop Oadd
                   (Efield
                      (Ederef
                         (Ebinop Oadd
                                 (Evar TICKET_LOCK_LOC (tarray t_ticket_lock_struct 32675))
                                 (Etempvar _lock_loc tint) (tptr t_ticket_lock_struct))
                         t_ticket_lock_struct) tl_now tint)
                   (Econst_int (Int.repr 1) tint) tuint)))).

Definition f_incr_now :=
  {|
    fn_return := tvoid;
    fn_callconv := cc_default;
    fn_params := ((_lock_id, tuint) :: (_offset, tuint) :: nil);
    fn_vars := nil;
    fn_temps := ((_lock_loc, tuint) :: nil);
    fn_body := f_incr_now_body
  |}.


Notation f_init_ticket_body :=
  (Ssequence
     (Scall None
            (Evar log_init (Tfunction (Tcons tuint (Tcons tuint Tnil)) tvoid
                                      cc_default))
            ((Etempvar _lock_id tuint) :: (Etempvar _offset tuint) :: nil))
     (Ssequence
        (Sifthenelse (Ebinop Oeq (Etempvar _lock_id tuint)
                             (Econst_int (Int.repr 0) tint) tint)
                     (Sset _lock_loc
                           (Ebinop Oadd (Econst_int (Int.repr 0) tint)
                                   (Etempvar _offset tuint) tuint))

                     (Sifthenelse (Ebinop Oeq (Etempvar _lock_id tuint)
                                          (Econst_int (Int.repr 1) tint) tint)
                                  (Sset _lock_loc
                                        (Ebinop Oadd
                                                (Ebinop Oadd (Econst_int (Int.repr 0) tint)
                                                        (Econst_int (Int.repr 1) tint) tint) (Etempvar _offset tuint)
                                                tuint))

                                  (Sifthenelse (Ebinop Oeq (Etempvar _lock_id tuint)
                                                       (Econst_int (Int.repr 2) tint) tint)
                                               (Sset _lock_loc
                                                     (Ebinop Oadd
                                                             (Ebinop Oadd
                                                                     (Ebinop Oadd (Econst_int (Int.repr 0) tint)
                                                                             (Econst_int (Int.repr 1) tint) tint)
                                                                     (Econst_int (Int.repr num_chan) tint) tint)
                                                             (Etempvar _offset tuint) tuint))
                                               (Sset _lock_loc (Econst_int (Int.repr 12345678) tint)))))
        (Ssequence
           (Sassign
              (Efield
                 (Ederef
                    (Ebinop Oadd
                            (Evar TICKET_LOCK_LOC (tarray t_ticket_lock_struct 32675))
                            (Etempvar _lock_loc tuint) (tptr t_ticket_lock_struct))
                    t_ticket_lock_struct) tl_next tuint)
              (Econst_int (Int.repr 0) tint))
           (Sassign
              (Efield
                 (Ederef
                    (Ebinop Oadd
                            (Evar TICKET_LOCK_LOC (tarray t_ticket_lock_struct 32675))
                            (Etempvar _lock_loc tuint) (tptr t_ticket_lock_struct))
                    t_ticket_lock_struct) tl_now tuint) (Econst_int (Int.repr 0) tint))))).

Definition f_init_ticket :=
  {|
    fn_return := tvoid;
    fn_callconv := cc_default;
    fn_params := ((_lock_id, tuint) :: (_offset, tuint) :: nil);
    fn_vars := nil;
    fn_temps := ((_lock_loc, tuint) :: nil);
    fn_body := f_init_ticket_body
  |}.