Library mcertikos.mm.MALOpCSource

***********************************************************************
*                                                                     *
*            The CertiKOS Certified Kit Operating System              *
*                                                                     *
*                   The FLINT Group, Yale University                  *
*                                                                     *
*  Copyright The FLINT Group, Yale University.  All rights reserved.  *
*  This file is distributed under the terms of the Yale University    *
*  Non-Commercial License Agreement.                                  *
*                                                                     *
*********************************************************************** 

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

    void pfree(unsigned int pfree_index)
    {
        at_set(pfree_index, 0);
    }

Let tpfree_index: ident := 1 % positive.

Definition pfree_body : statement :=
  Scall None (Evar at_set (Tfunction (Tcons tint (Tcons tint Tnil)) Tvoid cc_default))
        (Etempvar tpfree_index tint::Econst_int (Int.repr 0) tint::nil).

Definition f_pfree := {|
                       fn_return := Tvoid;
                       fn_callconv := cc_default;
                       fn_params := ((tpfree_index, tint) :: nil);
                       fn_vars := nil;
                       fn_temps := nil;
                       fn_body := pfree_body
                     |}.

    unsigned int palloc()
    {
        unsigned int tnps;
        unsigned int palloc_index;
        unsigned int palloc_cur_at;
        unsigned int palloc_is_norm;
        unsigned int free_index;
        unsigned int container_alloc_succeeded;

        tnps = get_nps();
        palloc_index = 1;
        palloc_free_index = tnps;
        while( palloc_index < tnps && palloc_free_index == tnps )
        {
            palloc_is_norm = is_norm(palloc_index);
            if (palloc_is_norm == 1)
            {
                palloc_cur_at = at_get(palloc_index);
                if (palloc_cur_at == 0)
                    palloc_free_index = palloc_index;
            }
            palloc_index ++;
        }
        if (palloc_free_index == tnps)
            palloc_free_index = 0;
        else
        {
          container_alloc_succeeded = container_alloc(id);
          if (container_alloc_succeeded == 0)
          {
            palloc_free_index = 0;
          }
          else
          {
             at_set(palloc_free_index, 1);
             at_set_c(palloc_free_index, 0);
          }
        }
        return palloc_free_index;
    } 

Local Open Scope positive_scope.
Let tpalloc_index: ident := 1.
Let tpalloc_cur_at: ident := 2.
Let tpalloc_is_norm: ident := 3.
Let tnps: ident := 4.
Let tpalloc_free_index: ident := 5.
Let tcontainer_alloc_succeeded: ident := 6.
Let tid: ident := 7.

Definition palloc_while_condition : expr :=
  Ebinop Oand
         (Ebinop Olt (Etempvar tpalloc_index tint) (Etempvar tnps tint) tint)
         (Ebinop Oeq (Etempvar tpalloc_free_index tint) (Etempvar tnps tint) tint) tint.

Definition palloc_while_body : statement :=
  (Ssequence
     (Scall
        (Some tpalloc_is_norm)
        (Evar is_norm (Tfunction (Tcons tint Tnil) tint cc_default))
        (Etempvar tpalloc_index tint::nil)
     )
     (Ssequence
        (Sifthenelse
           (Ebinop Oeq (Etempvar tpalloc_is_norm tint)
                   (Econst_int (Int.repr 1) tint) tint)
           (Ssequence
              (Scall
                 (Some tpalloc_cur_at)
                 (Evar at_get (Tfunction (Tcons tint Tnil) tint cc_default))
                 (Etempvar tpalloc_index tint::nil)
              )
              (Sifthenelse
                 (Ebinop Oeq (Etempvar tpalloc_cur_at tint)
                         (Econst_int (Int.repr 0) tint) tint)
                 (Sset tpalloc_free_index (Etempvar tpalloc_index tint))
                 Sskip
              )
           )
           Sskip
        )
        (Sset
           tpalloc_index
           (Ebinop Oadd (Etempvar tpalloc_index tint)
                   (Econst_int (Int.repr 1) tint) tint)
        )
     )
  )
.

Definition palloc_body : statement :=
  Ssequence
    (Scall (Some tnps) (Evar get_nps (Tfunction Tnil tint cc_default)) nil)
    (Ssequence
       (Sset tpalloc_index (Econst_int (Int.repr 1) tint))
       (Ssequence
          (Sset tpalloc_free_index (Etempvar tnps tint))
          (Ssequence
             (Swhile
                palloc_while_condition
                palloc_while_body
             )
             (Ssequence
                (Sifthenelse
                   (Ebinop Oeq (Etempvar tpalloc_free_index tint)
                           (Etempvar tnps tint) tint)
                   (Sset tpalloc_free_index (Econst_int (Int.repr 0) tint))
                   (Ssequence
                      (Scall (Some tcontainer_alloc_succeeded)
                             (Evar container_alloc (Tfunction (Tcons tint Tnil) tint cc_default))
                             ((Etempvar tid tint) :: nil))
                      (Sifthenelse (Ebinop Oeq (Etempvar tcontainer_alloc_succeeded tint)
                                           (Econst_int (Int.repr 0) tint) tint)
                          (Sset tpalloc_free_index (Econst_int (Int.repr 0) tint))
                          (Ssequence
                             (Scall None
                                    (Evar at_set (Tfunction (Tcons tint (Tcons tint Tnil))
                                                             tvoid cc_default))
                                    ((Etempvar tpalloc_free_index tint) ::
                                                                    (Econst_int (Int.repr 1) tint) :: nil))
                             (Scall None
                                    (Evar at_set_c (Tfunction (Tcons tint (Tcons tint Tnil))
                                                             tvoid cc_default))
                                    ((Etempvar tpalloc_free_index tint) ::
                                                                    (Econst_int (Int.repr 0) tint) :: nil))
                ))))
                (Sreturn (Some (Etempvar tpalloc_free_index tint)))
    )))).

Definition f_palloc := {|
                        fn_return := tint;
                        fn_callconv := cc_default;
                        fn_params := (tid, tint) :: nil;
                        fn_vars := nil;
                        fn_temps := ((tcontainer_alloc_succeeded, tint) :: (tnps, tint) :: (tpalloc_index, tint) :: (tpalloc_cur_at, tint) :: (tpalloc_is_norm, tint) :: (tpalloc_free_index, tint) :: nil);
                        fn_body := palloc_body
                      |}.