Library mcertikos.proc.VEPTIntroCSource
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 get_EPTE(unsigned int, unsigned int, unsigned int, unsigned int);
unsigned int ept_get_page_entry(unsigned int gpa)
{
unsigned int pdpt;
unsigned int pdir;
unsigned int ptab;
unsigned int entry;
pdpt = gpa / (512 * 512) % 512;
pdir = gpa / 512 % 512;
ptab = gpa % 512;
entry = get_EPTE(0, pdpt, pdir, ptab);
return entry;
}
Definition _gpa := 1 % positive.
Definition _pdpt := 2 % positive.
Definition _pdir := 3 % positive.
Definition _ptab := 4 % positive.
Definition _entry := 5 % positive.
Definition _entry´ := 6 % positive.
Definition ept_get_page_entry_body :=
(Ssequence
(Sset _pdpt
(Ebinop Omod
(Ebinop Odiv (Etempvar _gpa tuint)
(Ebinop Omul (Econst_int (Int.repr 512) tint)
(Econst_int (Int.repr 512) tint) tint) tuint)
(Econst_int (Int.repr 512) tint) tuint))
(Ssequence
(Sset _pdir
(Ebinop Omod
(Ebinop Odiv (Etempvar _gpa tuint) (Econst_int (Int.repr 512) tint)
tuint) (Econst_int (Int.repr 512) tint) tuint))
(Ssequence
(Sset _ptab
(Ebinop Omod (Etempvar _gpa tuint) (Econst_int (Int.repr 512) tint)
tuint))
(Ssequence
(Ssequence
(Scall (Some _entry´)
(Evar get_EPTE (Tfunction
(Tcons tuint
(Tcons tuint
(Tcons tuint (Tcons tuint Tnil)))) tuint
cc_default))
((Econst_int (Int.repr 0) tint) :: (Etempvar _pdpt tuint) ::
(Etempvar _pdir tuint) :: (Etempvar _ptab tuint) :: nil))
(Sset _entry (Etempvar _entry´ tuint)))
(Sreturn (Some (Etempvar _entry tuint))))))).
Definition f_ept_get_page_entry := {|
fn_return := tuint;
fn_callconv := cc_default;
fn_params := ((_gpa, tuint) :: nil);
fn_vars := nil;
fn_temps := ((_pdpt, tuint) :: (_pdir, tuint) :: (_ptab, tuint) ::
(_entry, tuint) :: (_entry´, tuint) :: nil);
fn_body := ept_get_page_entry_body
|}.
extern void set_EPTE(unsigned int, unsigned int, unsigned int, unsigned int, unsigned int);
void ept_set_page_entry(unsigned int gpa, unsigned int hpa)
{
unsigned int pdpt;
unsigned int pdir;
unsigned int ptab;
pdpt = gpa / (512 * 512) % 512;
pdir = gpa / 512 % 512;
ptab = gpa % 512;
set_EPTE(0, pdpt, pdir, ptab, hpa);
}
Definition _hpa := 7 % positive.
Definition ept_set_page_entry_body :=
(Ssequence
(Sset _pdpt
(Ebinop Omod
(Ebinop Odiv (Etempvar _gpa tuint)
(Ebinop Omul (Econst_int (Int.repr 512) tint)
(Econst_int (Int.repr 512) tint) tint) tuint)
(Econst_int (Int.repr 512) tint) tuint))
(Ssequence
(Sset _pdir
(Ebinop Omod
(Ebinop Odiv (Etempvar _gpa tuint) (Econst_int (Int.repr 512) tint)
tuint) (Econst_int (Int.repr 512) tint) tuint))
(Ssequence
(Sset _ptab
(Ebinop Omod (Etempvar _gpa tuint) (Econst_int (Int.repr 512) tint)
tuint))
(Scall None
(Evar set_EPTE (Tfunction
(Tcons tuint
(Tcons tuint
(Tcons tuint (Tcons tuint (Tcons tuint Tnil)))))
tvoid cc_default))
((Econst_int (Int.repr 0) tint) :: (Etempvar _pdpt tuint) ::
(Etempvar _pdir tuint) :: (Etempvar _ptab tuint) ::
(Etempvar _hpa tuint) :: nil))))).
Definition f_ept_set_page_entry := {|
fn_return := tvoid;
fn_callconv := cc_default;
fn_params := ((_gpa, tuint) :: (_hpa, tuint) :: nil);
fn_vars := nil;
fn_temps := ((_pdpt, tuint) :: (_pdir, tuint) :: (_ptab, tuint) :: nil);
fn_body := ept_set_page_entry_body
|}.
#define EPT_ADDR_MASK 4294963200ULL
#define EPT_PG_IGNORE_PAT_or_PERM 71
#define EPT_PG_MEMORY_TYPE 3
extern void set_EPTE(unsigned int, unsigned int, unsigned int, unsigned int, unsigned int);
unsigned int ept_add_mapping(unsigned int gpa, unsigned int hpa, unsigned int mem_type)
{
unsigned int pdpt;
unsigned int pdir;
unsigned int ptab;
pdpt = gpa / (512 * 512) % 512;
pdir = gpa / 512 % 512;
ptab = gpa % 512;
set_EPTE(0, pdpt, pdir, ptab, hpa & EPT_ADDR_MASK | EPT_PG_IGNORE_PAT_or_PERM | (mem_type << EPT_PG_MEMORY_TYPE));
return 0;
}
Definition _mem_type := 8 % positive.
Definition ept_add_mapping_body :=
(Ssequence
(Sset _pdpt
(Ebinop Omod
(Ebinop Odiv (Etempvar _gpa tuint)
(Ebinop Omul (Econst_int (Int.repr 1024) tint)
(Ebinop Omul (Econst_int (Int.repr 1024) tint)
(Econst_int (Int.repr 1024) tint) tint) tint) tuint)
(Econst_int (Int.repr 512) tint) tuint))
(Ssequence
(Sset _pdir
(Ebinop Omod
(Ebinop Odiv (Etempvar _gpa tuint)
(Ebinop Omul (Econst_int (Int.repr 2) tint)
(Ebinop Omul (Econst_int (Int.repr 1024) tint)
(Econst_int (Int.repr 1024) tint) tint) tint) tuint)
(Econst_int (Int.repr 512) tint) tuint))
(Ssequence
(Sset _ptab
(Ebinop Omod
(Ebinop Odiv (Etempvar _gpa tuint)
(Ebinop Omul (Econst_int (Int.repr 4) tint)
(Econst_int (Int.repr 1024) tint) tint) tuint)
(Econst_int (Int.repr 512) tint) tuint))
(Ssequence
(Scall None
(Evar set_EPTE (Tfunction
(Tcons tuint
(Tcons tuint
(Tcons tuint
(Tcons tuint (Tcons tuint Tnil))))) tvoid
cc_default))
((Econst_int (Int.repr 0) tint) :: (Etempvar _pdpt tuint) ::
(Etempvar _pdir tuint) :: (Etempvar _ptab tuint) ::
(Ebinop Oor
(Ebinop Oor
(Ebinop Oand (Etempvar _hpa tuint)
(Econst_int (Int.repr (4294963200)) tuint) tuint)
(Econst_int (Int.repr 71) tint) tuint)
(Ebinop Oshl (Etempvar _mem_type tuint)
(Econst_int (Int.repr 3) tint) tuint) tuint) :: nil))
(Sreturn (Some (Econst_int (Int.repr 0) tint))))))).
Definition f_ept_add_mapping := {|
fn_return := tuint;
fn_callconv := cc_default;
fn_params := ((_gpa, tuint) :: (_hpa, tuint) :: (_mem_type, tuint) :: nil);
fn_vars := nil;
fn_temps := ((_pdpt, tuint) :: (_pdir, tuint) :: (_ptab, tuint) :: nil);
fn_body := ept_add_mapping_body
|}.
extern void set_EPML4E(unsigned int);
extern void set_EPDPTE(unsigned int, unsigned int);
extern void set_EPDTE(unsigned int, unsigned int, unsigned int);
void ept_init(void)
{
unsigned int i, j;
set_EPML4E(0);
i = 0;
while(i < 4)
{
set_EPDPTE(0, i);
j = 0;
while (j < 512)
{
set_EPDTE(0, i, j);
j ++;
}
i ++;
}
}
Definition _i := 10 % positive.
Definition _j := 11 % positive.
Definition ept_init_inner_while_condition :=
(Ebinop Olt (Etempvar _j tint)
(Econst_int (Int.repr 512) tint) tint).
Definition ept_init_inner_while_body :=
(Ssequence
(Scall None
(Evar set_EPDTE (Tfunction
(Tcons tint
(Tcons tint (Tcons tint Tnil)))
tvoid cc_default))
((Econst_int (Int.repr 0) tint) :: (Etempvar _i tint) ::
(Etempvar _j tint) :: nil))
(Sset _j
(Ebinop Oadd (Etempvar _j tint)
(Econst_int (Int.repr 1) tint) tint))).
Definition ept_init_outter_while_condition :=
(Ebinop Olt (Etempvar _i tint) (Econst_int (Int.repr 4) tint) tint).
Definition ept_init_outter_while_body :=
(Ssequence
(Scall None
(Evar set_EPDPTE (Tfunction (Tcons tint (Tcons tint Tnil)) tvoid
cc_default))
((Econst_int (Int.repr 0) tint) :: (Etempvar _i tint) :: nil))
(Ssequence
(Sset _j (Econst_int (Int.repr 0) tint))
(Ssequence
(Swhile ept_init_inner_while_condition ept_init_inner_while_body)
(Sset _i
(Ebinop Oadd (Etempvar _i tint) (Econst_int (Int.repr 1) tint)
tint))))).
Definition f_ept_init_body :=
(Ssequence
(Scall None
(Evar set_EPML4E (Tfunction (Tcons tint Tnil) tvoid cc_default))
((Econst_int (Int.repr 0) tint) :: nil))
(Ssequence
(Sset _i (Econst_int (Int.repr 0) tint))
(Swhile ept_init_outter_while_condition ept_init_outter_while_body))).
Definition f_ept_init :=
{|
fn_return := tvoid;
fn_callconv := cc_default;
fn_params := nil;
fn_vars := nil;
fn_temps := ((_i, tuint) :: (_j, tuint) :: nil);
fn_body := f_ept_init_body
|}.