Library mcertikos.proc.PKContextCSource

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

#define num_proc 1024

extern unsigned int pt_new(unsigned int, unsigned int);
extern void set_RA(unsigned int, void * );
extern void set_SP(unsigned int, void * );

extern char STACK_LOC[num_proc][PAGE_SIZE];

unsigned int kctxt_new(void * entry, unsigned int id, unsigned int quota)
{
    unsigned int proc_index;
    proc_index = pt_new(id, quota);
    if (proc_index == num_proc) {
        return num_proc;
    }
    else {
        set_SP(proc_index, &STACK_LOC[proc_index][4092]);
        set_RA(proc_index, entry);
        return proc_index;
    }
}

Local Open Scope positive_scope.
Let _entry: ident := 1.
Let _proc_index: ident := 2.
Let _id: ident := 3.
Let _quota: ident := 4.

Local Open Scope Z_scope.

Definition kctxt_new_body : statement :=
(Ssequence
    (Scall (Some _proc_index)
      (Evar pt_new (Tfunction (Tcons tuint (Tcons tuint Tnil)) tuint
                      cc_default))
      ((Etempvar _id tuint) :: (Etempvar _quota tuint) :: nil))
  (Sifthenelse (Ebinop Oeq (Etempvar _proc_index tuint)
                 (Econst_int (Int.repr 1024) tint) tint)
    (Sreturn (Some (Econst_int (Int.repr 1024) tint)))
    (Ssequence
      (Scall None
        (Evar set_SP (Tfunction (Tcons tuint (Tcons (tptr tvoid) Tnil))
                        tvoid cc_default))
        ((Etempvar _proc_index tuint) :: (Ebinop Oadd
               (Ederef
                 (Ebinop Oadd
                   (Evar STACK_LOC (tarray (tarray tchar 4096) 1024))
                   (Etempvar _proc_index tuint) (tptr (tarray tchar 4096)))
                 (tarray tchar 4096)) (Econst_int (Int.repr 4092) tint)
               (tptr tchar)) :: nil))
      (Ssequence
        (Scall None
          (Evar set_RA (Tfunction (Tcons tuint (Tcons (tptr tvoid) Tnil))
                          tvoid cc_default))
          ((Etempvar _proc_index tuint) :: (Etempvar _entry (tptr tvoid)) ::
           nil))
        (Sreturn (Some (Etempvar _proc_index tuint)))))))
.


Definition f_kctxt_new :=
  {|
    fn_return := tint;
    fn_callconv := cc_default;
    fn_vars := nil;
    fn_params := ((_entry, tptr tvoid) :: (_id, tint) :: (_quota, tint) :: nil);
    fn_temps := ((_proc_index, tint) :: nil);
    fn_body := kctxt_new_body
  |}.