Library mcertikos.ticketlog.MBootCSource

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.

Local Open Scope positive_scope.
Let tindex: ident := 1.
Let tcurid : ident := 4.

Definition get_curid_body :=
  (Ssequence
     (Scall (Some tindex) (Evar get_CPU_ID (Tfunction Tnil tuint cc_default)) nil)
     (Sreturn (Some (Ederef
                       (Ebinop Oadd (Evar CURID_LOC (tarray tuint TOTAL_CPU))
                               (Etempvar tindex tuint) (tptr tuint)) tuint)))).

Definition f_get_curid :=
  {|
    fn_return := tuint;
    fn_callconv := cc_default;
    fn_params := nil;
    fn_vars := nil;
    fn_temps := ((tindex, tuint) :: nil);
    fn_body := get_curid_body
  |}.

Definition set_curid_body :=
  (Ssequence
     (Scall (Some tindex) (Evar get_CPU_ID (Tfunction Tnil tuint cc_default)) nil)
     (Sassign
        (Ederef
           (Ebinop Oadd (Evar CURID_LOC (tarray tuint TOTAL_CPU)) (Etempvar tindex tuint)
                   (tptr tuint)) tuint) (Etempvar tcurid tuint))).

Definition f_set_curid :=
  {|
    fn_return := tvoid;
    fn_callconv := cc_default;
    fn_params := ((tcurid, tuint) :: nil);
    fn_vars := nil;
    fn_temps := ((tindex, tuint) :: nil);
    fn_body := set_curid_body
  |}.

Definition set_curid_init_body :=
  (Sassign
     (Ederef
        (Ebinop Oadd (Evar CURID_LOC (tarray tuint TOTAL_CPU)) (Etempvar tindex tuint)
                (tptr tuint)) tuint)
     (Ebinop Oadd (Etempvar tindex tuint) (Econst_int (Int.repr 1) tint) tuint)).


Definition f_set_curid_init :=
  {|
    fn_return := tvoid;
    fn_callconv := cc_default;
    fn_params := ((tindex, tuint) :: nil);
    fn_vars := nil;
    fn_temps := nil;
    fn_body := set_curid_init_body
  |}.