Library mcertikos.virt.intel.VVMCSInitCSource
*********************************************************************** * * * 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 v_VMX_LOC := {|
gvar_info := (tarray tuint 36);
gvar_init := Init_space (VMX_Size´ × 4) :: nil;
gvar_readonly := false;
gvar_volatile := false
|}.
Definition _vmx_idx := 1 % positive.
#define VMX_SIZE 36
extern unsigned int VMX_LOC[VMX_SIZE];
unsigned int vmx_readz(unsigned int vmx_idx){
return VMX_LOC[vmx_idx];
}
Definition vmx_readz_body :=
(Sreturn (Some (Ederef
(Ebinop Oadd (Evar VMX_LOC (tarray tuint 36))
(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 := nil;
fn_body := vmx_readz_body
|}.
#define VMX_SIZE 36
extern unsigned int VMX_LOC[VMX_SIZE];
void vmx_writez(unsigned int vmx_idx, unsigned int vmx_val){
VMX_LOC[vmx_idx] = vmx_val;
}
Definition _vmx_val := 2 % positive.
Definition vmx_writez_body :=
(Sassign
(Ederef
(Ebinop Oadd (Evar VMX_LOC (tarray tuint 36)) (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 := nil;
fn_body := vmx_writez_body
|}.
#define VMX_G_RIP 14
#define C_VMCS_GUEST_RIP 26654
#define VMX_SIZE 36
extern unsigned int VMX_LOC[VMX_SIZE];
extern void vmcs_writez(unsigned int encoding, unsigned int val);
void vmx_enter_pre() {
unsigned int val = VMX_LOC[VMX_G_RIP];
vmcs_writez(C_VMCS_GUEST_RIP, val);
}
Definition _val := 3 % positive.
Definition vmx_enter_pre_body :=
(Ssequence
(Sset _val
(Ederef
(Ebinop Oadd (Evar VMX_LOC (tarray tuint 36))
(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 := ((_val, tuint) :: nil);
fn_body := vmx_enter_pre_body
|}.
#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 36
extern unsigned int VMX_LOC[VMX_SIZE];
extern unsigned int vmcs_readz(unsigned int encoding);
void vmx_exit_post(){
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[VMX_G_RIP] = val0;
VMX_LOC[VMX_EXIT_REASON] = val1;
VMX_LOC[VMX_EXIT_QUALIFICATION] = val2;
VMX_LOC[VMX_LAUNCHED] = 1;
}
Definition _val0 := 4 % positive.
Definition _val1 := 5 % positive.
Definition _val2 := 6 % positive.
Definition vmx_exit_post_body :=
(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 (Evar VMX_LOC (tarray tuint 36))
(Econst_int (Int.repr 14) tint) (tptr tuint)) tuint)
(Etempvar _val0 tuint))
(Ssequence
(Sassign
(Ederef
(Ebinop Oadd (Evar VMX_LOC (tarray tuint 36))
(Econst_int (Int.repr 27) tint) (tptr tuint)) tuint)
(Etempvar _val1 tuint))
(Ssequence
(Sassign
(Ederef
(Ebinop Oadd (Evar VMX_LOC (tarray tuint 36))
(Econst_int (Int.repr 28) tint) (tptr tuint)) tuint)
(Etempvar _val2 tuint))
(Sassign
(Ederef
(Ebinop Oadd (Evar VMX_LOC (tarray tuint 36))
(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 := ((_val0, tuint) :: (_val1, tuint) :: (_val2, tuint) :: nil);
fn_body := vmx_exit_post_body
|}.