Library mcertikos.proc.VVMCSInitCSource
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 v_VMX_LOC :=
{|
gvar_info := (tarray (tarray tuint VMX_Size´) 8);
gvar_init := (Init_space (VMX_Size´ × 4 × 8) :: nil);
gvar_readonly := false;
gvar_volatile := false
|}.
Definition _curid := 1 % positive.
Definition _vmx_idx := 2 % positive.
#define TOTAL_CPU 8
#define VMX_SIZE VMX_Size'
extern unsigned int get_CPU_ID(void);
extern unsigned int VMX_LOC[TOTAL_CPU][VMX_SIZE];
unsigned int vmx_readz(unsigned int vmx_idx){
unsigned int curid = get_CPU_ID();
return VMX_LOC[curid][vmx_idx];
}
Definition f_vmx_readz_body :=
(Ssequence
(Scall (Some _curid)
(Evar get_CPU_ID (Tfunction Tnil tuint cc_default)) nil)
(Sreturn (Some (Ederef
(Ebinop Oadd
(Ederef
(Ebinop Oadd
(Evar VMX_LOC (tarray (tarray tuint VMX_Size´) 8))
(Etempvar _curid tuint) (tptr (tarray tuint VMX_Size´)))
(tarray tuint VMX_Size´)) (Etempvar _vmx_idx tuint)
(tptr tuint)) tuint)))).
Definition f_vmx_readz :=
{|
fn_return := tuint;
fn_callconv := cc_default;
fn_params := ((_vmx_idx, tuint) :: nil);
fn_vars := nil;
fn_temps := ((_curid, tuint) :: nil);
fn_body := f_vmx_readz_body
|}.
#define TOTAL_CPU 8
#define VMX_SIZE VMX_Size'
extern unsigned int get_CPU_ID(void);
extern unsigned int VMX_LOC[VMX_SIZE];
void vmx_writez(unsigned int vmx_idx, unsigned int vmx_val){
unsigned int curid = get_CPU_ID();
VMX_LOC[curid][vmx_idx] = vmx_val;
}
Definition _vmx_val := 3 % positive.
Definition f_vmx_writez_body :=
(Ssequence
(Scall (Some _curid)
(Evar get_CPU_ID (Tfunction Tnil tuint cc_default)) nil)
(Sassign
(Ederef
(Ebinop Oadd
(Ederef
(Ebinop Oadd (Evar VMX_LOC (tarray (tarray tuint VMX_Size´) 8))
(Etempvar _curid tuint) (tptr (tarray tuint VMX_Size´)))
(tarray tuint VMX_Size´)) (Etempvar _vmx_idx tuint) (tptr tuint)) tuint)
(Etempvar _vmx_val tuint))).
Definition f_vmx_writez :=
{|
fn_return := tvoid;
fn_callconv := cc_default;
fn_params := ((_vmx_idx, tuint) :: (_vmx_val, tuint) :: nil);
fn_vars := nil;
fn_temps := ((_curid, tuint) :: nil);
fn_body := f_vmx_writez_body
|}.
#define TOTAL_CPU 8
#define VMX_G_RIP 14
#define C_VMCS_GUEST_RIP 26654
#define VMX_SIZE VMX_Size'
extern unsigned int get_CPU_ID(void);
extern unsigned int VMX_LOC[TOTAL_CPU][VMX_SIZE];
extern void vmcs_writez(unsigned int encoding, unsigned int val);
void vmx_enter_pre() {
unsigned int curid = get_CPU_ID();
unsigned int val = VMX_LOC[curid][VMX_G_RIP];
vmcs_writez(C_VMCS_GUEST_RIP, val);
}
Definition _val := 4 % positive.
Definition f_vmx_enter_pre_body :=
(Ssequence
(Scall (Some _curid)
(Evar get_CPU_ID (Tfunction Tnil tuint cc_default)) nil)
(Ssequence
(Sset _val
(Ederef
(Ebinop Oadd
(Ederef
(Ebinop Oadd (Evar VMX_LOC (tarray (tarray tuint VMX_Size´) 8))
(Etempvar _curid tuint) (tptr (tarray tuint VMX_Size´)))
(tarray tuint VMX_Size´)) (Econst_int (Int.repr 14) tint) (tptr tuint))
tuint))
(Scall None
(Evar vmcs_writez (Tfunction (Tcons tuint (Tcons tuint Tnil)) tvoid
cc_default))
((Econst_int (Int.repr 26654) tint) :: (Etempvar _val tuint) :: nil)))).
Definition f_vmx_enter_pre :=
{|
fn_return := tvoid;
fn_callconv := cc_default;
fn_params := nil;
fn_vars := nil;
fn_temps := ((_curid, tuint) :: (_val, tuint) :: nil);
fn_body := f_vmx_enter_pre_body
|}.
#define TOTAL_CPU 8
#define C_VMCS_GUEST_RIP 26654
#define C_VMCS_EXIT_REASON 17410
#define C_VMCS_EXIT_QUALIFICATION 25600
#define VMX_G_RIP 14
#define VMX_EXIT_REASON 27
#define VMX_EXIT_QUALIFICATION 28
#define VMX_LAUNCHED 31
#define VMX_SIZE VMX_Size'
extern unsigned int get_CPU_ID(void);
extern unsigned int VMX_LOC[TOTAL_CPU][VMX_SIZE];
extern unsigned int vmcs_readz(unsigned int encoding);
void vmx_exit_post(){
unsigned int curid = get_CPU_ID();
unsigned int val0 = vmcs_readz(C_VMCS_GUEST_RIP);
unsigned int val1 = vmcs_readz(C_VMCS_EXIT_REASON);
unsigned int val2 = vmcs_readz(C_VMCS_EXIT_QUALIFICATION);
VMX_LOC[curid][VMX_G_RIP] = val0;
VMX_LOC[curid][VMX_EXIT_REASON] = val1;
VMX_LOC[curid][VMX_EXIT_QUALIFICATION] = val2;
VMX_LOC[curid][VMX_LAUNCHED] = 1;
}
Definition _val0 := 5 % positive.
Definition _val1 := 6 % positive.
Definition _val2 := 7 % positive.
Definition f_vmx_exit_post_body :=
(Ssequence
(Scall (Some _curid)
(Evar get_CPU_ID (Tfunction Tnil tuint cc_default)) nil)
(Ssequence
(Scall (Some _val0)
(Evar vmcs_readz (Tfunction (Tcons tuint Tnil) tuint cc_default))
((Econst_int (Int.repr 26654) tint) :: nil))
(Ssequence
(Scall (Some _val1)
(Evar vmcs_readz (Tfunction (Tcons tuint Tnil) tuint cc_default))
((Econst_int (Int.repr 17410) tint) :: nil))
(Ssequence
(Scall (Some _val2)
(Evar vmcs_readz (Tfunction (Tcons tuint Tnil) tuint cc_default))
((Econst_int (Int.repr 25600) tint) :: nil))
(Ssequence
(Sassign
(Ederef
(Ebinop Oadd
(Ederef
(Ebinop Oadd (Evar VMX_LOC (tarray (tarray tuint VMX_Size´) 8))
(Etempvar _curid tuint) (tptr (tarray tuint VMX_Size´)))
(tarray tuint VMX_Size´)) (Econst_int (Int.repr 14) tint)
(tptr tuint)) tuint) (Etempvar _val0 tuint))
(Ssequence
(Sassign
(Ederef
(Ebinop Oadd
(Ederef
(Ebinop Oadd (Evar VMX_LOC (tarray (tarray tuint VMX_Size´) 8))
(Etempvar _curid tuint) (tptr (tarray tuint VMX_Size´)))
(tarray tuint VMX_Size´)) (Econst_int (Int.repr 27) tint)
(tptr tuint)) tuint) (Etempvar _val1 tuint))
(Ssequence
(Sassign
(Ederef
(Ebinop Oadd
(Ederef
(Ebinop Oadd
(Evar VMX_LOC (tarray (tarray tuint VMX_Size´) 8))
(Etempvar _curid tuint) (tptr (tarray tuint VMX_Size´)))
(tarray tuint VMX_Size´)) (Econst_int (Int.repr 28) tint)
(tptr tuint)) tuint) (Etempvar _val2 tuint))
(Sassign
(Ederef
(Ebinop Oadd
(Ederef
(Ebinop Oadd
(Evar VMX_LOC (tarray (tarray tuint VMX_Size´) 8))
(Etempvar _curid tuint) (tptr (tarray tuint VMX_Size´)))
(tarray tuint VMX_Size´)) (Econst_int (Int.repr 31) tint)
(tptr tuint)) tuint) (Econst_int (Int.repr 1) tint))))))))).
Definition f_vmx_exit_post :=
{|
fn_return := tvoid;
fn_callconv := cc_default;
fn_params := nil;
fn_vars := nil;
fn_temps := ((_curid, tuint) :: (_val0, tuint) :: (_val1, tuint) :: (_val2, tuint) :: nil);
fn_body := f_vmx_exit_post_body
|}.