Library mcertikos.mm.MPTInitCSource

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 void pt_init(unsigned int);
    
      void pmap_init(unsigned int mbi_adr)
      {   
          pt_init(mbi_adr);
      }

Local Open Scope positive_scope.
Let tmbi_adr: ident := 15.

Local Open Scope Z_scope.

Definition pmap_init_body : statement :=
   Scall None (Evar pt_init (Tfunction (Tcons tint Tnil) Tvoid cc_default)) ((Etempvar tmbi_adr tint )::nil).

Definition f_pmap_init := {|
                           fn_return := tvoid;
                           fn_callconv := cc_default;
                           fn_vars := nil;
                           fn_params := ((tmbi_adr, tint) :: nil);
                           fn_temps := nil;
                           fn_body := pmap_init_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_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 unsigned int container_split(unsigned int, unsigned int);
    
    unsigned int pt_new(unsigned int id, unsigned int quota)
    {   
        unsigned int child;
        child = container_split(id, quota);
        return child;
    }

Local temporaries used in pt_new function

Local Open Scope positive_scope.
Let tchild: ident := 9.
Let tid: ident := 10.
Let tquota: ident := 11.

Local Open Scope Z_scope.

Definition pt_new_body : statement :=
  Ssequence
    (Scall (Some tchild)
       (Evar container_split (Tfunction (Tcons tint (Tcons tint Tnil)) tint cc_default))
       (Etempvar tid tint :: Etempvar tquota tint :: nil))
    (Sreturn (Some (Etempvar tchild tint))).

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