Library mcertikos.mm.MALInitCSource

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

  extern int get_size(void);
  extern int get_mms(unsigned int);
  extern int get_mml(unsigned int);
  extern int is_usable(unsigned int);
  extern void set_norm(unsigned int, unsigned int);
  extern void set_nps(unsigned int);
  extern void container_init(unsigned int);

  void mem_init(unsigned int mbi_adr)
  {
    unsigned int i, j, s, l, isnorm, nps, maxs, size, mm, flag;
    container_init(mbi_adr);
    i = 0;
    size = get_size();
    nps = 0;
    while(i < size)
    {
        s = get_mms(i);
        l = get_mml(i);
        maxs = (s + l) / PgSize + 1;
        if(maxs > nps)
            nps = maxs;
        i++;
    }
    set_nps(nps);
    i = 0;
    while(i < nps)
    {
        if(i < kern_low || i >= kern_high)
            set_norm(i, 1);
        else
        {
            j = 0;
            flag = 0;
            isnorm = 0;
            while(j < size && flag == 0)
            {
                s = get_mms(j);
                l = get_mml(j);
                isnorm = is_usable(j);
                if(s <= i * PgSize && l + s >= (i + 1) * PgSize)
                    flag = 1;
                j++;
            }
            if(flag == 1 && isnorm == 1)
                set_norm(i, 2);
            else
                set_norm(i, 0);
        }
        i++;
    }
  }
Local temporaries used
Local Open Scope positive_scope.
Let _ti: ident := 1.
Let _tj: ident := 2.
Let _ts: ident := 3.
Let _tl: ident := 4.
Let _tisnorm: ident := 5.
Let _tnps: ident := 6.
Let _tmaxs: ident := 7.
Let _tsize: ident := 8.
Let _tmm: ident := 9.
Let _tflag: ident := 10.
Let _tmbi_adr: ident := 11.

Definition nps_while_condition : expr :=
  (Ebinop Olt (Etempvar _ti tint) (Etempvar _tsize tint) tint).

Definition nps_while_body : statement :=
  (Ssequence
     (Scall (Some _ts) (Evar get_mms (Tfunction (Tcons tint Tnil) tint cc_default))
            ((Etempvar _ti tint) :: nil))
     (Ssequence
        (Scall (Some _tl) (Evar get_mml (Tfunction (Tcons tint Tnil) tint cc_default))
               ((Etempvar _ti tint) :: nil))
        (Ssequence
           (Sset _tmaxs (Ebinop Oadd
                               (Ebinop Odiv
                                       (Ebinop Oadd (Etempvar _ts tint) (Etempvar _tl tint) tint)
                                       (Econst_int (Int.repr PgSize) tint) tint)
                               (Econst_int (Int.repr 1) tint) tint))
           (Ssequence
              (Sifthenelse
                 (Ebinop Ogt (Etempvar _tmaxs tint) (Etempvar _tnps tint) tint)
                 (Sset _tnps (Etempvar _tmaxs tint))
                 Sskip
              )
              (Sset _ti (Ebinop Oadd (Etempvar _ti tint)
                               (Econst_int (Int.repr 1) tint) tint))))))
.

Definition inner_while_condition : expr :=
  (Ebinop Oand
          (Ebinop Olt (Etempvar _tj tint) (Etempvar _tsize tint) tint)
          (Ebinop Oeq (Etempvar _tflag tint) (Econst_int (Int.repr 0) tint) tint) tint).

Definition inner_while_body : statement :=
  (Ssequence
     (Scall (Some _ts) (Evar get_mms (Tfunction (Tcons tint Tnil) tint cc_default))
            ((Etempvar _tj tint) :: nil))
     (Ssequence
        (Scall (Some _tl) (Evar get_mml (Tfunction (Tcons tint Tnil) tint cc_default))
               ((Etempvar _tj tint) :: nil))
        (Ssequence
           (Scall (Some _tisnorm) (Evar is_usable (Tfunction (Tcons tint Tnil) tint cc_default))
                  ((Etempvar _tj tint) :: nil))
           (Ssequence
              (Sifthenelse
                 (Ebinop Ole (Etempvar _ts tint)
                         (Ebinop Omul (Etempvar _ti tint) (Econst_int (Int.repr PgSize) tint) tint) tint)
                 (Sifthenelse
                    (Ebinop Oge (Ebinop Oadd (Etempvar _tl tint) (Etempvar _ts tint) tint)
                            (Ebinop Omul (Ebinop Oadd (Etempvar _ti tint) (Econst_int (Int.repr 1) tint) tint)
                                    (Econst_int (Int.repr PgSize) tint) tint) tint)
                    (Sset _tflag (Econst_int (Int.repr 1) tint))
                    Sskip
                 )
                 Sskip
              )
              (Sset _tj (Ebinop Oadd (Etempvar _tj tint) (Econst_int (Int.repr 1) tint) tint))))))
.

Definition outter_while_condition : expr :=
  (Ebinop Olt (Etempvar _ti tint) (Etempvar _tnps tint) tint).

Definition outter_while_body : statement :=
  (Ssequence
     (Sifthenelse
        (Ebinop Olt (Etempvar _ti tint) (Econst_int (Int.repr kern_low) tint) tint)
        (Scall None (Evar set_norm (Tfunction (Tcons tint (Tcons tint Tnil)) Tvoid cc_default))
               ((Etempvar _ti tint) :: (Econst_int (Int.repr 1) tint) :: nil))
        (Sifthenelse
           (Ebinop Oge (Etempvar _ti tint) (Econst_int (Int.repr kern_high) tint) tint)
           (Scall None (Evar set_norm (Tfunction (Tcons tint (Tcons tint Tnil)) Tvoid cc_default))
                  ((Etempvar _ti tint) :: (Econst_int (Int.repr 1) tint) :: nil))
           (Ssequence
              (Sset _tj (Econst_int (Int.repr 0) tint))
              (Ssequence
                 (Sset _tflag (Econst_int (Int.repr 0) tint))
                 (Ssequence
                    (Sset _tisnorm (Econst_int (Int.repr 0) tint))
                    (Ssequence
                       (Swhile inner_while_condition inner_while_body)
                       (Sifthenelse
                          (Ebinop Oeq (Etempvar _tflag tint) (Econst_int (Int.repr 1) tint) tint)
                          (Sifthenelse
                             (Ebinop Oeq (Etempvar _tisnorm tint) (Econst_int (Int.repr 1) tint) tint)
                             (Scall None (Evar set_norm (Tfunction (Tcons tint (Tcons tint Tnil)) Tvoid cc_default))
                                    ((Etempvar _ti tint) :: (Econst_int (Int.repr 2) tint) :: nil))
                             (Scall None (Evar set_norm (Tfunction (Tcons tint (Tcons tint Tnil)) Tvoid cc_default))
                                    ((Etempvar _ti tint) :: (Econst_int (Int.repr 0) tint) :: nil))
                          )
                          (Scall None (Evar set_norm (Tfunction (Tcons tint (Tcons tint Tnil)) Tvoid cc_default))
                                 ((Etempvar _ti tint) :: (Econst_int (Int.repr 0) tint) :: nil))
                       )
           ))))
        )
     )
     (Sset _ti (Ebinop Oadd (Etempvar _ti tint)
                      (Econst_int (Int.repr 1) tint) tint))
  )
.

Definition mem_init_body : statement :=
  (Ssequence
     (Scall None (Evar container_init (Tfunction (Tcons tint Tnil) Tvoid cc_default)) ((Etempvar _tmbi_adr tint)::nil))
     (Ssequence
        (Sset _ti (Econst_int (Int.repr 0) tint))
        (Ssequence
           (Scall (Some _tsize) (Evar get_size (Tfunction Tnil tint cc_default)) nil)
           (Ssequence
              (Sset _tnps (Econst_int (Int.repr 0) tint))
              (Ssequence
                 (Swhile nps_while_condition nps_while_body)
                 (Ssequence
                    (Scall None (Evar set_nps (Tfunction (Tcons tint Tnil) Tvoid cc_default)) ((Etempvar _tnps tint) :: nil))
                    (Ssequence
                       (Sset _ti (Econst_int (Int.repr 0) tint))
                       (Swhile outter_while_condition outter_while_body)
  )))))))
.

Definition f_mem_init := {|
                          fn_return := Tvoid;
                          fn_callconv := cc_default;
                          fn_params := ((_tmbi_adr, tint)::nil);
                          fn_vars := nil;
                          fn_temps := ((_ti, tint) :: (_tj, tint) :: (_ts, tint) :: (_tl, tint) :: (_tisnorm, tint) :: (_tnps, tint) :: (_tmaxs, tint) :: (_tsize, tint) :: (_tmm, tint) :: (_tflag, tint) :: nil);
                          fn_body := mem_init_body
                        |}.