Library mcertikos.mm.MALHCSource
Require Import Coqlib.
Require Import AST.
Require Import Integers.
Require Import Values.
Require Import Cop.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import AST.
Require Import Integers.
Require Import Values.
Require Import Cop.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
#define NUM_PROC 64
extern void set_cr3 (char ** );
extern char * PTPool_LOC[NUM_PROC][1024];
void set_pt(unsigned int index)
{
set_cr3(PTPool_LOC[index]);
}
Let tsetpt_index: ident := 1 % positive.
Definition set_pt_body : statement :=
(Scall None
(Evar set_cr3 (Tfunction (Tcons (tptr tvoid) Tnil) tvoid cc_default))
((Ederef
(Ebinop Oadd (Evar PTPool_LOC (tarray (tarray (tptr tchar) 1024) 64))
(Etempvar tsetpt_index tint) (tptr (tarray (tptr tchar) 1024)))
(tarray (tptr tchar) 1024)) :: nil))
.
Definition f_set_pt := {|
fn_return := Tvoid;
fn_callconv := cc_default;
fn_vars := nil;
fn_params := ((tsetpt_index, tint) :: nil);
fn_temps := nil;
fn_body := set_pt_body
|}.
#define NUM_PROC 64
extern char * PTPool_LOC[NUM_PROC][1024];
unsigned int get_PDE(unsigned int proc_index, unsigned int pde_index)
{
unsigned int pde;
pde = (unsigned int)PTPool_LOC[proc_index][pde_index] / 4096;
return pde;
}
Let tproc_index: ident := 1 % positive.
Let tpde_index: ident := 2 % positive.
Let tpde: ident := 3 % positive.
Definition get_PDE_body : statement :=
(Ssequence
(Sset tpde
(Ebinop Odiv
(Ecast
(Ederef
(Ebinop Oadd
(Ederef
(Ebinop Oadd
(Evar PTPool_LOC (tarray (tarray (tptr tchar) 1024) 64))
(Etempvar tproc_index tint)
(tptr (tarray (tptr tchar) 1024)))
(tarray (tptr tchar) 1024)) (Etempvar tpde_index tint)
(tptr (tptr tchar))) (tptr tchar)) tint)
(Econst_int (Int.repr 4096) tint) tint))
(Sreturn (Some (Etempvar tpde tint))))
.
Definition f_get_PDE := {|
fn_return := tint;
fn_callconv := cc_default;
fn_params := ((tproc_index, tint) :: (tpde_index, tint) :: nil);
fn_vars := nil;
fn_temps := ((tpde, tint) :: nil);
fn_body := get_PDE_body
|}.
#define NUM_PROC 64
#define PT_PERM_PTU 7
extern char * PTPool_LOC[NUM_PROC][1024];
extern unsigned int IDPMap_LOC[1024][1024];
void set_PDE(unsigned int proc_index, unsigned int pde_index)
{
PTPool_LOC[proc_index][pde_index] = ((char * )(IDPMap_LOC[pde_index])) + PT_PERM_PTU;
}
Definition set_pde_body: statement :=
(Sassign
(Ederef
(Ebinop Oadd
(Ederef
(Ebinop Oadd
(Evar PTPool_LOC (tarray (tarray (tptr tchar) 1024) 64))
(Etempvar tproc_index tint) (tptr (tarray (tptr tchar) 1024)))
(tarray (tptr tchar) 1024)) (Etempvar tpde_index tint)
(tptr (tptr tchar))) (tptr tchar))
(Ebinop Oadd
(Ecast
(Ederef
(Ebinop Oadd (Evar IDPMap_LOC (tarray (tarray tint 1024) 1024))
(Etempvar tpde_index tint) (tptr (tarray tint 1024)))
(tarray tint 1024)) (tptr tchar)) (Econst_int (Int.repr 7) tint)
(tptr tchar))).
Definition f_set_pde := {|
fn_return := Tvoid;
fn_callconv := cc_default;
fn_vars := nil;
fn_params := ((tproc_index, tint) :: (tpde_index, tint) :: nil);
fn_temps := nil;
fn_body := set_pde_body
|}.
#define NUM_PROC 64
#define PT_PERM_UP 0
extern char * PTPool_LOC[NUM_PROC][1024];
void rmv_PDE(unsigned int proc_index, unsigned int pde_index)
{
PTPool_LOC[proc_index][pde_index] = (char * )PT_PERM_UP;
}
Definition rmv_pde_body: statement :=
(Sassign
(Ederef
(Ebinop Oadd
(Ederef
(Ebinop Oadd
(Evar PTPool_LOC (tarray (tarray (tptr tchar) 1024) 64))
(Etempvar tproc_index tint) (tptr (tarray (tptr tchar) 1024)))
(tarray (tptr tchar) 1024)) (Etempvar tpde_index tint)
(tptr (tptr tchar))) (tptr tchar))
(Ecast (Econst_int (Int.repr 0) tint) (tptr tchar))).
Definition f_rmv_pde := {|
fn_return := Tvoid;
fn_callconv := cc_default;
fn_vars := nil;
fn_params := ((tproc_index, tint) :: (tpde_index, tint) :: nil);
fn_temps := nil;
fn_body := rmv_pde_body
|}.
#define NUM_PROC 64
#define PT_PERM_PTU 7
extern char * PTPool_LOC[NUM_PROC][1024];
void set_PDEU(unsigned int proc_index, unsigned int pde_index, unsigned int pi)
{
PTPool_LOC[proc_index][pde_index] = (char * )(pi * 4096 + PT_PERM_PTU);
}
Let tpi: ident := 4 % positive.
Definition set_pdeu_body: statement :=
(Sassign
(Ederef
(Ebinop Oadd
(Ederef
(Ebinop Oadd
(Evar PTPool_LOC (tarray (tarray (tptr tchar) 1024) 64))
(Etempvar tproc_index tint) (tptr (tarray (tptr tchar) 1024)))
(tarray (tptr tchar) 1024)) (Etempvar tpde_index tint)
(tptr (tptr tchar))) (tptr tchar))
(Ecast
(Ebinop Oadd
(Ebinop Omul (Etempvar tpi tint) (Econst_int (Int.repr 4096) tint)
tint) (Econst_int (Int.repr 7) tint) tint) (tptr tchar))).
Definition f_set_pdeu := {|
fn_return := Tvoid;
fn_callconv := cc_default;
fn_vars := nil;
fn_params := ((tproc_index, tint) :: (tpde_index, tint) :: (tpi, tint) :: nil);
fn_temps := nil;
fn_body := set_pdeu_body
|}.
#define NUM_PROC 64
#define PT_PERM_PTU 7
extern char * PTPool_LOC[NUM_PROC][1024];
extern unsigned int fload(unsigned int);
unsigned int get_PTE(unsigned int proc_index, unsigned int pde_index, unsigned int vadr)
{
unsigned int pte;
unsigned int offset;
offset = ((unsigned int)PTPool_LOC[proc_index][pde_index] - PT_PERM_PTU) / 4096;
pte = fload(offset * 1024 + vadr);
return pte;
}
Let tpte: ident := 5 % positive.
Let toffset: ident := 6 % positive.
Let tvadr: ident := 7 % positive.
Definition get_pte_body: statement :=
(Ssequence
(Sset toffset
(Ebinop Odiv
(Ebinop Osub
(Ecast
(Ederef
(Ebinop Oadd
(Ederef
(Ebinop Oadd
(Evar PTPool_LOC (tarray (tarray (tptr tchar) 1024) 64))
(Etempvar tproc_index tint)
(tptr (tarray (tptr tchar) 1024)))
(tarray (tptr tchar) 1024)) (Etempvar tpde_index tint)
(tptr (tptr tchar))) (tptr tchar)) tint)
(Econst_int (Int.repr 7) tint) tint)
(Econst_int (Int.repr 4096) tint) tint))
(Ssequence
(Ssequence
(Scall (Some 13%positive)
(Evar fload (Tfunction (Tcons tint Tnil) tint cc_default))
((Ebinop Oadd
(Ebinop Omul (Etempvar toffset tint)
(Econst_int (Int.repr 1024) tint) tint) (Etempvar tvadr tint)
tint) :: nil))
(Sset tpte (Etempvar 13%positive tint)))
(Sreturn (Some (Etempvar tpte tint))))).
Definition f_get_pte := {|
fn_return := tint;
fn_callconv := cc_default;
fn_vars := nil;
fn_params := ((tproc_index, tint) :: (tpde_index, tint) :: (tvadr, tint) :: nil);
fn_temps := (toffset, tint) :: (tpte, tint) :: (13%positive, tint) :: nil;
fn_body := get_pte_body
|}.
#define NUM_PROC 64
#define PT_PERM_PTU 7
extern char * PTPool_LOC[NUM_PROC][1024];
extern void fstore(unsigned int, unsigned int);
void set_PTE(unsigned int proc_index, unsigned int pde_index, unsigned int vadr, unsigned int padr, unsigned int perm)
{
unsigned int offset;
offset = ((unsigned int)PTPool_LOC[proc_index][pde_index] - PT_PERM_PTU) / 4096;
fstore(offset * 1024 + vadr, padr * 4096 + perm);
}
Let tpadr: ident := 8 % positive.
Let tperm: ident := 9 % positive.
Definition set_pte_body: statement :=
(Ssequence
(Sset toffset
(Ebinop Odiv
(Ebinop Osub
(Ecast
(Ederef
(Ebinop Oadd
(Ederef
(Ebinop Oadd
(Evar PTPool_LOC (tarray (tarray (tptr tchar) 1024) 64))
(Etempvar tproc_index tint)
(tptr (tarray (tptr tchar) 1024)))
(tarray (tptr tchar) 1024)) (Etempvar tpde_index tint)
(tptr (tptr tchar))) (tptr tchar)) tint)
(Econst_int (Int.repr 7) tint) tint)
(Econst_int (Int.repr 4096) tint) tint))
(Scall None
(Evar fstore (Tfunction (Tcons tint (Tcons tint Tnil)) tvoid cc_default))
((Ebinop Oadd
(Ebinop Omul (Etempvar toffset tint)
(Econst_int (Int.repr 1024) tint) tint) (Etempvar tvadr tint)
tint) ::
(Ebinop Oadd
(Ebinop Omul (Etempvar tpadr tint) (Econst_int (Int.repr 4096) tint)
tint) (Etempvar tperm tint) tint) :: nil))).
Definition f_set_pte := {|
fn_return := Tvoid;
fn_callconv := cc_default;
fn_vars := nil;
fn_params := ((tproc_index, tint) :: (tpde_index, tint) :: (tvadr, tint) :: (tpadr, tint) :: (tperm, tint) :: nil);
fn_temps := (toffset, tint) :: nil;
fn_body := set_pte_body
|}.
#define NUM_PROC 64
#define PT_PERM_PTU 7
extern char * PTPool_LOC[NUM_PROC][1024];
extern void fstore(unsigned int, unsigned int);
void rmv_PTE(unsigned int proc_index, unsigned int pde_index, unsigned int vadr)
{
unsigned int offset;
offset = ((unsigned int)PTPool_LOC[proc_index][pde_index] - PT_PERM_PTU) / 4096;
fstore(offset * 1024 + vadr, 0);
}
Definition rmv_pte_body: statement :=
(Ssequence
(Sset toffset
(Ebinop Odiv
(Ebinop Osub
(Ecast
(Ederef
(Ebinop Oadd
(Ederef
(Ebinop Oadd
(Evar PTPool_LOC (tarray (tarray (tptr tchar) 1024) 64))
(Etempvar tproc_index tint)
(tptr (tarray (tptr tchar) 1024)))
(tarray (tptr tchar) 1024)) (Etempvar tpde_index tint)
(tptr (tptr tchar))) (tptr tchar)) tint)
(Econst_int (Int.repr 7) tint) tint)
(Econst_int (Int.repr 4096) tint) tint))
(Scall None
(Evar fstore (Tfunction (Tcons tint (Tcons tint Tnil)) tvoid cc_default))
((Ebinop Oadd
(Ebinop Omul (Etempvar toffset tint)
(Econst_int (Int.repr 1024) tint) tint) (Etempvar tvadr tint)
tint) :: (Econst_int (Int.repr 0) tint) :: nil))).
Definition f_rmv_pte := {|
fn_return := Tvoid;
fn_callconv := cc_default;
fn_vars := nil;
fn_params := ((tproc_index, tint) :: (tpde_index, tint) :: (tvadr, tint) :: nil);
fn_temps := (toffset, tint) :: nil;
fn_body := rmv_pte_body
|}.
extern unsigned int IDPMap_LOC[1024][1024];
void set_IDPTE(unsigned int pde_index, unsigned int vadr, unsigned int perm)
{
IDPMap_LOC[pde_index][vadr] = (pde_index * 1024 + vadr) * 4096 + perm;
}
Definition set_idpte_body: statement :=
(Sassign
(Ederef
(Ebinop Oadd
(Ederef
(Ebinop Oadd (Evar IDPMap_LOC (tarray (tarray tint 1024) 1024))
(Etempvar tpde_index tint) (tptr (tarray tint 1024)))
(tarray tint 1024)) (Etempvar tvadr tint) (tptr tint)) tint)
(Ebinop Oadd
(Ebinop Omul
(Ebinop Oadd
(Ebinop Omul (Etempvar tpde_index tint)
(Econst_int (Int.repr 1024) tint) tint) (Etempvar tvadr tint)
tint) (Econst_int (Int.repr 4096) tint) tint)
(Etempvar tperm tint) tint)).
Definition f_set_idpte := {|
fn_return := Tvoid;
fn_callconv := cc_default;
fn_vars := nil;
fn_params := ((tpde_index, tint) :: (tvadr, tint) :: (tperm, tint) :: nil);
fn_temps := nil;
fn_body := set_idpte_body
|}.