Library mcertikos.virt.intel.PProcCSource
*********************************************************************** * * * The CertiKOS Certified Kit Operating System * * * * The FLINT Group, Yale University * * * * Copyright The FLINT Group, Yale University. All rights reserved. * * This file is distributed under the terms of the Yale University * * Non-Commercial License Agreement. * * * ***********************************************************************
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.
Notation 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 := t_struct_ept;
gvar_init := Init_space (sizeof t_struct_ept) :: nil;
gvar_readonly := false;
gvar_volatile := false
|}.
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_EPML4E(unsigned int pml4_idx)
{
ept.pml4[0] = 0;
ept.pml4[1] = (char * ) (ept.pdpt) + 7;
}
Definition tpml4_idx := 1 % positive.
Definition set_EPML4E_body :=
(Ssequence
(Sassign
(Ederef
(Ebinop Oadd
(Efield (Evar EPT_LOC 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 (Evar EPT_LOC t_struct_ept) _pml4
(tarray (tptr tchar) 1024)) (Econst_int (Int.repr 0) tint)
(tptr (tptr tchar))) (tptr tchar))
(Ebinop Oadd
(Ecast
(Efield (Evar EPT_LOC 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, tint) :: nil);
fn_vars := nil;
fn_temps := nil;
fn_body := set_EPML4E_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_EPDPTE(unsigned int pml4_idx, unsigned int pdpt_idx)
{
ept.pdpt[pdpt_idx * 2] = 0;
ept.pdpt[pdpt_idx * 2 + 1] =
(char * ) (&ept.pdt[pdpt_idx][0]) + 7;
}
Definition tpdpt_idx := 2 % positive.
Definition set_EPDPTE_body :=
(Ssequence
(Sassign
(Ederef
(Ebinop Oadd
(Efield (Evar EPT_LOC 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 (Evar EPT_LOC 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 (Evar EPT_LOC 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 := nil;
fn_body := set_EPDPTE_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_EPDTE(unsigned int pml4_idx, unsigned int pdpt_idx,
unsigned int pdir_idx)
{
ept.pdt[pdpt_idx][pdir_idx * 2] = 0;
ept.pdt[pdpt_idx][pdir_idx * 2 + 1] =
(char * ) (&ept.ptab[pdpt_idx][pdir_idx][0]) + 7;
}
Definition tpdir_idx := 3 % positive.
Definition set_EPDTE_body :=
(Ssequence
(Sassign
(Ederef
(Ebinop Oadd
(Ederef
(Ebinop Oadd
(Efield (Evar EPT_LOC 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 (Evar EPT_LOC 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 (Evar EPT_LOC 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 := nil;
fn_body := set_EPDTE_body
|}.
struct eptStruct {
char * pml4[1024];
char * pdpt[1024];
char * pdt[4][1024];
unsigned long long ptab[4][512][512];
};
extern struct eptStruct ept;
unsigned int get_EPTE(unsigned int pml4_idx, unsigned int pdpt_idx, unsigned int pdir_idx, unsigned int ptab_idx)
{
return (unsigned int) ept.ptab[pdpt_idx][pdir_idx][ptab_idx];
}
Definition tptab_idx := 4 % positive.
Definition get_EPTE_body :=
(Sreturn (Some (Ecast
(Ederef
(Ebinop Oadd
(Ederef
(Ebinop Oadd
(Ederef
(Ebinop Oadd
(Efield (Evar EPT_LOC 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 := nil;
fn_body := 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 := 5 % positive.
Definition set_EPTE_body :=
(Sassign
(Ederef
(Ebinop Oadd
(Ederef
(Ebinop Oadd
(Ederef
(Ebinop Oadd
(Efield (Evar EPT_LOC 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)
(Etempvar hpa_val tuint)).
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 := nil;
fn_body := set_EPTE_body
|}.