Library mcertikos.mm.MPTBitCSource

***********************************************************************
*                                                                     *
*            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.

      extern unsigned int palloc(unsigned int);
      extern unsigned int pt_insert(unsigned int, unsigned int, unsigned int, unsigned int);

      #define MagicNumber 1048577

      unsigned int pt_resv(unsigned int proc_index, unsigned int vaddr, unsigned int perm)
      {
          unsigned int pi;
          unsigned int result;
          pi = palloc(proc_index);
          if (pi == 0)
            result = MagicNumber;
          else
            result = pt_insert(proc_index, vaddr, pi, perm);
          return result;
      }
Function parameters and local temporaries used in the function
Local Open Scope positive_scope.
Let tproc_index: ident := 1.
Let tvaddr: ident := 2.
Let tperm: ident := 3.
Let tpi: ident := 4.
Let tresult: ident := 5.

Local Open Scope Z_scope.

Definition pt_resv_body : statement :=
  (Ssequence
     (Scall (Some tpi) (Evar palloc (Tfunction (Tcons tint Tnil) tint cc_default)) ((Etempvar tproc_index tint) :: nil))
     (Ssequence
        (Sifthenelse (Ebinop Oeq (Etempvar tpi tint)
                             (Econst_int (Int.repr 0) tint) tint)
                     (Sset tresult (Econst_int (Int.repr 1048577) tint))
                     (Scall (Some tresult)
                            (Evar pt_insert (Tfunction
                                               (Tcons tint
                                                      (Tcons tint (Tcons tint (Tcons tint Tnil))))
                                               tint cc_default))
                            ((Etempvar tproc_index tint) :: (Etempvar tvaddr tint) ::
                                                         (Etempvar tpi tint) :: (Etempvar tperm tint) :: nil)))
        (Sreturn (Some (Etempvar tresult tint)))))
   .

Definition f_pt_resv := {|
                         fn_return := tint;
                         fn_callconv := cc_default;
                         fn_vars := nil;
                         fn_params := ((tproc_index, tint) :: (tvaddr, tint) :: (tperm, tint) :: nil);
                         fn_temps := ((tpi, tint) :: (tresult, tint) :: nil);
                         fn_body := pt_resv_body
                       |}.

      extern unsigned int palloc(unsigned int);
      extern unsigned int pt_insert(unsigned int, unsigned int, unsigned int, unsigned int);

      #define MagicNumber 1048577

      unsigned int pt_resv2(unsigned int proc_index, unsigned int vaddr, unsigned int perm, unsigned int proc_index2, unsigned int vaddr2, unsigned int perm2)
      {
          unsigned int pi;
          unsigned int result;
          pi = palloc(proc_index);
          if (pi == 0)
            result = MagicNumber;
          else
          {
            result = pt_insert(proc_index, vaddr, pi, perm);
            if (result == MagicNumber)
              result = pt_insert(proc_index2, vaddr2, pi, perm2);
          }
          return result;
      }
Function parameters and local temporaries used in the function
Local Open Scope positive_scope.
Let tproc_index2: ident := 6.
Let tvaddr2: ident := 7.
Let tperm2: ident := 8.

Local Open Scope Z_scope.

Definition pt_resv2_body : statement :=
  (Ssequence
     (Scall (Some tpi) (Evar palloc (Tfunction (Tcons tint Tnil) tint cc_default)) ((Etempvar tproc_index tint) :: nil))
     (Ssequence
        (Sifthenelse (Ebinop Oeq (Etempvar tpi tint)
                             (Econst_int (Int.repr 0) tint) tint)
                     (Sset tresult (Econst_int (Int.repr 1048577) tint))
                     (Ssequence
                        (Scall (Some tresult)
                               (Evar pt_insert (Tfunction
                                                  (Tcons tint
                                                         (Tcons tint
                                                                (Tcons tint (Tcons tint Tnil)))) tint cc_default))
                               ((Etempvar tproc_index tint) :: (Etempvar tvaddr tint) ::
                                                            (Etempvar tpi tint) :: (Etempvar tperm tint) :: nil))
                        (Sifthenelse (Ebinop One (Etempvar tresult tint)
                                             (Econst_int (Int.repr 1048577) tint) tint)
                                     (Scall (Some tresult)
                                            (Evar pt_insert (Tfunction
                                                               (Tcons tint
                                                                      (Tcons tint
                                                                             (Tcons tint (Tcons tint Tnil))))
                                                               tint cc_default))
                                            ((Etempvar tproc_index2 tint) :: (Etempvar tvaddr2 tint) ::
                                                                          (Etempvar tpi tint) :: (Etempvar tperm2 tint) :: nil))
                                     Sskip)))
        (Sreturn (Some (Etempvar tresult tint)))))
.

Definition f_pt_resv2 := {|
                         fn_return := tint;
                         fn_callconv := cc_default;
                         fn_vars := nil;
                         fn_params := ((tproc_index, tint) :: (tvaddr, tint) :: (tperm, tint) :: (tproc_index2, tint) :: (tvaddr2, tint) :: (tperm2, tint) :: nil);
                         fn_temps := ((tpi, tint) :: (tresult, tint) :: nil);
                         fn_body := pt_resv2_body
                       |}.

      extern void pt_init(unsigned int);
      extern void set_bit(unsigned int, unsigned int);
      
      #define num_proc 64
       
      void pmap_init(unsigned int mbi_adr)
      {
          unsigned int i;
          pt_init(mbi_adr);
          set_bit(0, 1);
          i = 1;
          while(i < num_proc)
          {
              set_bit(i, 0);
              i++;
          }
      }

Local Open Scope positive_scope.
Let ti: ident := 5.
Let tmbi_adr: ident := 6.

Local Open Scope Z_scope.

Definition pmap_init_while_condition : expr :=
  (Ebinop Olt (Etempvar ti tint) (Econst_int (Int.repr num_proc) tint) tint).

Definition pmap_init_while_body : statement :=
  (Ssequence
     (Scall None (Evar set_bit (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 pmap_init_body : statement :=
  (Ssequence
     (Scall None (Evar pt_init (Tfunction (Tcons tint Tnil) Tvoid cc_default)) ((Etempvar tmbi_adr tint)::nil))
     (Ssequence
        (Scall None (Evar set_bit (Tfunction (Tcons tint (Tcons tint Tnil)) Tvoid cc_default))
               ((Econst_int (Int.repr 0) tint) :: (Econst_int (Int.repr 1) tint) :: nil))
        (Ssequence
           (Sset ti (Econst_int (Int.repr 1) tint))
           (Swhile pmap_init_while_condition pmap_init_while_body)))).

Definition f_pmap_init := {|
                           fn_return := tvoid;
                           fn_callconv := cc_default;
                           fn_vars := nil;
                           fn_params := ((tmbi_adr, tint) :: nil);
                           fn_temps := ((ti, tint) :: nil);
                           fn_body := pmap_init_body
                         |}.

    extern unsigned int is_used(unsigned int);
    extern unsigned int set_bit(unsigned int, unsigned int);
    extern unsigned int container_split(unsigned int, unsigned int, unsigned int);
    
    #define num_proc 64
     
     unsigned int pt_new(unsigned int id, unsigned int quota)
     {
         unsigned int pt_new_index;
         unsigned int pt_new_is_used;
         unsigned int pt_new_free_index;
         pt_new_index = 1;
         pt_new_free_index = num_proc;
         while( pt_new_index < num_proc && pt_new_free_index == num_proc ) {
                pt_new_is_used = is_used(pt_new_index);
                if (pt_new_is_used != 1)
                     pt_new_free_index = pt_new_index;
                pt_new_index ++;
         }    
         if (pt_new_free_index != num_proc) {
             set_bit(pt_new_free_index, 1);
             container_split(id, quota, pt_new_free_index);
         }
         return pt_new_free_index;
     }
Local temporaries used in pt_new function
Local Open Scope positive_scope.
Let tpt_new_index: ident := 7.
Let tpt_new_is_used: ident := 8.
Let tpt_new_free_index: ident := 9.
Let tid: ident := 10.
Let tquota: ident := 11.

Local Open Scope Z_scope.

Definition pt_new_while_condition : expr :=
  Ebinop Oand
         (Ebinop Olt (Etempvar tpt_new_index tint) (Econst_int (Int.repr num_proc) tint) tint)
         (Ebinop Oeq (Etempvar tpt_new_free_index tint) (Econst_int (Int.repr num_proc) tint) tint) tint.

Definition pt_new_while_body : statement :=
  (Ssequence
     (Scall
        (Some tpt_new_is_used)
        (Evar is_used (Tfunction (Tcons tint Tnil) tint cc_default))
        (Etempvar tpt_new_index tint::nil)
     )
     (Ssequence
        (Sifthenelse
           (Ebinop One (Etempvar tpt_new_is_used tint)
                   (Econst_int (Int.repr 1) tint) tint)
           (Sset tpt_new_free_index (Etempvar tpt_new_index tint))
           Sskip
        )
        (Sset
           tpt_new_index
           (Ebinop Oadd (Etempvar tpt_new_index tint)
                   (Econst_int (Int.repr 1) tint) tint)
        )
     )
  )
.

Definition pt_new_body : statement :=
  (Ssequence
     (Sset tpt_new_index (Econst_int (Int.repr 1) tint))
     (Ssequence
        (Sset tpt_new_free_index (Econst_int (Int.repr num_proc) tint))
        (Ssequence
           (Swhile pt_new_while_condition pt_new_while_body)
           (Ssequence
              (Sifthenelse (Ebinop One (Etempvar tpt_new_free_index tint)
                                   (Econst_int (Int.repr 64) tint) tint)
                           (Ssequence
                              (Scall None
                                  (Evar set_bit (Tfunction (Tcons tint (Tcons tint Tnil)) tvoid cc_default))
                                  ((Etempvar tpt_new_free_index tint) :: (Econst_int (Int.repr 1) tint) ::
                                                                      nil))
                              (Scall None
                                  (Evar container_split (Tfunction (Tcons tint (Tcons tint (Tcons tint Tnil)))
                                                                   tint cc_default))
                                  (Etempvar tid tint :: Etempvar tquota tint ::
                                            Etempvar tpt_new_free_index tint :: nil)))
                           Sskip)
              (Sreturn (Some (Etempvar tpt_new_free_index tint)))
  )))).

Definition f_pt_new := {|
                        fn_return := tint;
                        fn_callconv := cc_default;
                        fn_vars := nil;
                        fn_params := (tid,tint) :: (tquota,tint) :: nil;
                        fn_temps := ((tpt_new_index, tint) :: (tpt_new_is_used, tint) :: (tpt_new_free_index, tint) :: nil);
                        fn_body := pt_new_body
                      |}.