Library mcertikos.proc.PProcCSource
Require Import Coqlib.
Require Import AST.
Require Import Integers.
Require Import Values.
Require Import Cop.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Definition _eptStruct : ident := 6100%positive.
Definition _pml4 : ident := 6200%positive.
Definition _ptab : ident := 6300%positive.
Definition _pdt : ident := 6400%positive.
Definition _pdpt : ident := 6500%positive.
Definition t_struct_ept :=
(Tstruct _eptStruct
(Fcons _pml4 (tarray (tptr tchar) 1024)
(Fcons _pdpt (tarray (tptr tchar) 1024)
(Fcons _pdt (tarray (tarray (tptr tchar) 1024) 4)
(Fcons _ptab (tarray (tarray (tarray tulong 512) 512) 4) Fnil))))
noattr).
Definition v_ept := {|
gvar_info := (tarray t_struct_ept 8);
gvar_init := (Init_space (8*8413184) :: nil);
gvar_readonly := false;
gvar_volatile := false
|}.
Require Import AST.
Require Import Integers.
Require Import Values.
Require Import Cop.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Definition _eptStruct : ident := 6100%positive.
Definition _pml4 : ident := 6200%positive.
Definition _ptab : ident := 6300%positive.
Definition _pdt : ident := 6400%positive.
Definition _pdpt : ident := 6500%positive.
Definition t_struct_ept :=
(Tstruct _eptStruct
(Fcons _pml4 (tarray (tptr tchar) 1024)
(Fcons _pdpt (tarray (tptr tchar) 1024)
(Fcons _pdt (tarray (tarray (tptr tchar) 1024) 4)
(Fcons _ptab (tarray (tarray (tarray tulong 512) 512) 4) Fnil))))
noattr).
Definition v_ept := {|
gvar_info := (tarray t_struct_ept 8);
gvar_init := (Init_space (8*8413184) :: nil);
gvar_readonly := false;
gvar_volatile := false
|}.
#define TOTAL_CPU 8
struct eptStruct {
char * pml4[1024];
char * pdpt[1024];
char * pdt[4][1024];
unsigned long long ptab[4][512][512];
};
extern unsigned int get_CPU_ID(void);
extern struct eptStruct ept[TOTAL_CPU];
void set_EPML4E(unsigned int pml4_idx)
{
unsigned int cpuid = get_CPU_ID();
ept[cpuid].pml4[1] = 0;
ept[cpuid].pml4[0] = (char * ) (ept[cpuid].pdpt) + 7;
}
Definition tpml4_idx := 1 % positive.
Definition tcpuid := 2 % positive.
Definition f_set_EPML4E_body :=
(Ssequence
(Scall (Some tcpuid)
(Evar get_CPU_ID (Tfunction Tnil tuint cc_default)) nil)
(Ssequence
(Sassign
(Ederef
(Ebinop Oadd
(Efield
(Ederef
(Ebinop Oadd (Evar EPT_LOC (tarray t_struct_ept 8))
(Etempvar tcpuid tuint) (tptr t_struct_ept))
t_struct_ept) _pml4 (tarray (tptr tchar) 1024))
(Econst_int (Int.repr 1) tint) (tptr (tptr tchar))) (tptr tchar))
(Econst_int (Int.repr 0) tint))
(Sassign
(Ederef
(Ebinop Oadd
(Efield
(Ederef
(Ebinop Oadd (Evar EPT_LOC (tarray t_struct_ept 8))
(Etempvar tcpuid tuint) (tptr t_struct_ept))
t_struct_ept) _pml4 (tarray (tptr tchar) 1024))
(Econst_int (Int.repr 0) tint) (tptr (tptr tchar))) (tptr tchar))
(Ebinop Oadd
(Ecast
(Efield
(Ederef
(Ebinop Oadd (Evar EPT_LOC (tarray t_struct_ept 8))
(Etempvar tcpuid tuint) (tptr t_struct_ept))
t_struct_ept) _pdpt (tarray (tptr tchar) 1024))
(tptr tchar)) (Econst_int (Int.repr 7) tint) (tptr tchar))))).
Definition f_set_EPML4E :=
{|
fn_return := tvoid;
fn_callconv := cc_default;
fn_params := ((tpml4_idx, tuint) :: nil);
fn_vars := nil;
fn_temps := ((tcpuid, tuint) :: nil);
fn_body := f_set_EPML4E_body
|}.
struct eptStruct {
char * pml4[1024];
char * pdpt[1024];
char * pdt[4][1024];
unsigned long long ptab[4][512][512];
};
extern unsigned int get_CPU_ID(void);
extern struct eptStruct ept[TOTAL_CPU];
void set_EPDPTE(unsigned int pml4_idx, unsigned int pdpt_idx)
{
unsigned int cpuid = get_CPU_ID();
ept[cpuid].pdpt[pdpt_idx * 2] = 0;
ept[cpuid].pdpt[pdpt_idx * 2 + 1] =
(char * ) (&ept[cpuid].pdt[pdpt_idx][0]) + 7;
}
Definition tpdpt_idx := 3 % positive.
Definition f_set_EPDPTE_body :=
(Ssequence
(Scall (Some tcpuid)
(Evar get_CPU_ID (Tfunction Tnil tuint cc_default)) nil)
(Ssequence
(Sassign
(Ederef
(Ebinop Oadd
(Efield
(Ederef
(Ebinop Oadd (Evar EPT_LOC (tarray t_struct_ept 8))
(Etempvar tcpuid tuint) (tptr t_struct_ept))
t_struct_ept) _pdpt (tarray (tptr tchar) 1024))
(Ebinop Oadd
(Ebinop Omul (Etempvar tpdpt_idx tuint)
(Econst_int (Int.repr 2) tint) tuint)
(Econst_int (Int.repr 1) tint) tuint) (tptr (tptr tchar)))
(tptr tchar)) (Econst_int (Int.repr 0) tint))
(Sassign
(Ederef
(Ebinop Oadd
(Efield
(Ederef
(Ebinop Oadd (Evar EPT_LOC (tarray t_struct_ept 8))
(Etempvar tcpuid tuint) (tptr t_struct_ept))
t_struct_ept) _pdpt (tarray (tptr tchar) 1024))
(Ebinop Omul (Etempvar tpdpt_idx tuint)
(Econst_int (Int.repr 2) tint) tuint) (tptr (tptr tchar)))
(tptr tchar))
(Ebinop Oadd
(Ecast
(Eaddrof
(Ederef
(Ebinop Oadd
(Ederef
(Ebinop Oadd
(Efield
(Ederef
(Ebinop Oadd
(Evar EPT_LOC (tarray t_struct_ept 8))
(Etempvar tcpuid tuint)
(tptr t_struct_ept))
t_struct_ept) _pdt
(tarray (tarray (tptr tchar) 1024) 4))
(Etempvar tpdpt_idx tuint)
(tptr (tarray (tptr tchar) 1024)))
(tarray (tptr tchar) 1024)) (Econst_int (Int.repr 0) tint)
(tptr (tptr tchar))) (tptr tchar)) (tptr (tptr tchar)))
(tptr tchar)) (Econst_int (Int.repr 7) tint) (tptr tchar))))).
Definition f_set_EPDPTE := {|
fn_return := tvoid;
fn_callconv := cc_default;
fn_params := ((tpml4_idx, tuint) :: (tpdpt_idx, tuint) :: nil);
fn_vars := nil;
fn_temps := ((tcpuid, tuint) :: nil);
fn_body := f_set_EPDPTE_body
|}.
#define TOTAL_CPU 8
struct eptStruct {
char * pml4[1024];
char * pdpt[1024];
char * pdt[4][1024];
unsigned long long ptab[4][512][512];
};
extern unsigned int get_CPU_ID(void);
extern struct eptStruct ept[8];
void set_EPDTE(unsigned int pml4_idx, unsigned int pdpt_idx,
unsigned int pdir_idx)
{
unsigned int cpuid = get_CPU_ID();
ept[cpuid].pdt[pdpt_idx][pdir_idx * 2 + 1] = 0;
ept[cpuid].pdt[pdpt_idx][pdir_idx * 2] =
(char * ) (&ept[cpuid].ptab[pdpt_idx][pdir_idx][0]) + 7;
}
Definition tpdir_idx := 4 % positive.
Definition f_set_EPDTE_body :=
(Ssequence
(Scall (Some tcpuid)
(Evar get_CPU_ID (Tfunction Tnil tuint cc_default)) nil)
(Ssequence
(Sassign
(Ederef
(Ebinop Oadd
(Ederef
(Ebinop Oadd
(Efield
(Ederef
(Ebinop Oadd (Evar EPT_LOC (tarray t_struct_ept 8))
(Etempvar tcpuid tuint) (tptr t_struct_ept))
t_struct_ept) _pdt
(tarray (tarray (tptr tchar) 1024) 4))
(Etempvar tpdpt_idx tuint) (tptr (tarray (tptr tchar) 1024)))
(tarray (tptr tchar) 1024))
(Ebinop Oadd
(Ebinop Omul (Etempvar tpdir_idx tuint)
(Econst_int (Int.repr 2) tint) tuint)
(Econst_int (Int.repr 1) tint) tuint) (tptr (tptr tchar)))
(tptr tchar)) (Econst_int (Int.repr 0) tint))
(Sassign
(Ederef
(Ebinop Oadd
(Ederef
(Ebinop Oadd
(Efield
(Ederef
(Ebinop Oadd (Evar EPT_LOC (tarray t_struct_ept 8))
(Etempvar tcpuid tuint) (tptr t_struct_ept))
t_struct_ept) _pdt
(tarray (tarray (tptr tchar) 1024) 4))
(Etempvar tpdpt_idx tuint) (tptr (tarray (tptr tchar) 1024)))
(tarray (tptr tchar) 1024))
(Ebinop Omul (Etempvar tpdir_idx tuint)
(Econst_int (Int.repr 2) tint) tuint) (tptr (tptr tchar)))
(tptr tchar))
(Ebinop Oadd
(Ecast
(Eaddrof
(Ederef
(Ebinop Oadd
(Ederef
(Ebinop Oadd
(Ederef
(Ebinop Oadd
(Efield
(Ederef
(Ebinop Oadd
(Evar EPT_LOC (tarray t_struct_ept 8))
(Etempvar tcpuid tuint)
(tptr t_struct_ept)) t_struct_ept)
_ptab (tarray (tarray (tarray tulong 512) 512) 4))
(Etempvar tpdpt_idx tuint)
(tptr (tarray (tarray tulong 512) 512)))
(tarray (tarray tulong 512) 512))
(Etempvar tpdir_idx tuint) (tptr (tarray tulong 512)))
(tarray tulong 512)) (Econst_int (Int.repr 0) tint)
(tptr tulong)) tulong) (tptr tulong)) (tptr tchar))
(Econst_int (Int.repr 7) tint) (tptr tchar))))).
Definition f_set_EPDTE := {|
fn_return := tvoid;
fn_callconv := cc_default;
fn_params := ((tpml4_idx, tuint) :: (tpdpt_idx, tuint) ::
(tpdir_idx, tuint) :: nil);
fn_vars := nil;
fn_temps := ((tcpuid, tuint) :: nil);
fn_body := f_set_EPDTE_body
|}.
#define TOTAL_CPU 8
struct eptStruct {
char * pml4[1024];
char * pdpt[1024];
char * pdt[4][1024];
unsigned long long ptab[4][512][512];
};
extern unsigned int get_CPU_ID(void);
extern struct eptStruct ept[TOTAL_CPU];
unsigned int get_EPTE(unsigned int pml4_idx, unsigned int pdpt_idx, unsigned int pdir_idx, unsigned int ptab_idx)
{
unsigned int cpuid = get_CPU_ID();
return (unsigned int) ept[cpuid].ptab[pdpt_idx][pdir_idx][ptab_idx];
}
Definition tptab_idx := 5 % positive.
Definition f_get_EPTE_body :=
(Ssequence
(Scall (Some tcpuid)
(Evar get_CPU_ID (Tfunction Tnil tuint cc_default)) nil)
(Sreturn (Some (Ecast
(Ederef
(Ebinop Oadd
(Ederef
(Ebinop Oadd
(Ederef
(Ebinop Oadd
(Efield
(Ederef
(Ebinop Oadd
(Evar EPT_LOC (tarray t_struct_ept 8))
(Etempvar tcpuid tuint)
(tptr t_struct_ept))
t_struct_ept) _ptab
(tarray (tarray (tarray tulong 512) 512) 4))
(Etempvar tpdpt_idx tuint)
(tptr (tarray (tarray tulong 512) 512)))
(tarray (tarray tulong 512) 512))
(Etempvar tpdir_idx tuint)
(tptr (tarray tulong 512))) (tarray tulong 512))
(Etempvar tptab_idx tuint) (tptr tulong)) tulong)
tuint)))).
Definition f_get_EPTE := {|
fn_return := tuint;
fn_callconv := cc_default;
fn_params := ((tpml4_idx, tuint) :: (tpdpt_idx, tuint) ::
(tpdir_idx, tuint) :: (tptab_idx, tuint) :: nil);
fn_vars := nil;
fn_temps := ((tcpuid, tuint) :: nil);
fn_body := f_get_EPTE_body
|}.
struct eptStruct {
char * pml4[1024];
char * pdpt[1024];
char * pdt[4][1024];
unsigned long long ptab[4][512][512];
};
extern struct eptStruct ept;
void set_EPTE(unsigned int pml4_idx, unsigned int pdpt_idx, unsigned int pdir_idx, unsigned int ptab_idx, unsigned int hpa_val)
{
ept.ptab[pdpt_idx][pdir_idx][ptab_idx] = hpa_val;
}
Definition hpa_val := 56 % positive.
Definition f_set_EPTE_body :=
(Ssequence
(Scall (Some tcpuid)
(Evar get_CPU_ID (Tfunction Tnil tuint cc_default)) nil)
(Sassign
(Ederef
(Ebinop Oadd
(Ederef
(Ebinop Oadd
(Ederef
(Ebinop Oadd
(Efield
(Ederef
(Ebinop Oadd (Evar EPT_LOC (tarray t_struct_ept 8))
(Etempvar tcpuid tuint) (tptr t_struct_ept))
t_struct_ept) _ptab
(tarray (tarray (tarray tulong 512) 512) 4))
(Etempvar tpdpt_idx tuint)
(tptr (tarray (tarray tulong 512) 512)))
(tarray (tarray tulong 512) 512)) (Etempvar tpdir_idx tuint)
(tptr (tarray tulong 512))) (tarray tulong 512))
(Etempvar tptab_idx tuint) (tptr tulong)) tulong)
(Ecast (Etempvar hpa_val tuint) tulong))).
Definition f_set_EPTE :=
{|
fn_return := tvoid;
fn_callconv := cc_default;
fn_params := ((tpml4_idx, tuint) :: (tpdpt_idx, tuint) ::
(tpdir_idx, tuint) :: (tptab_idx, tuint) ::
(hpa_val, tuint) :: nil);
fn_vars := nil;
fn_temps := ((tcpuid, tuint) :: nil);
fn_body := f_set_EPTE_body
|}.