Library mcertikos.proc.VVMCSIntroCSource
Require Import Coqlib.
Require Import AST.
Require Import Integers.
Require Import Values.
Require Import Cop.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
#define VMCS_PRI_PROC_BASED_CTLS 0x00004002
#define PROCBASED_INT_WINDOW_EXITING (1 << 2)
extern unsigned int vmcs_read32(unsigned int encoding);
void vmcs_write32(unsigned int encoding, unsigned int val);
void vmx_set_intercept_intwin(unsigned int enable)
{
unsigned int procbased_ctls = vmcs_read32(VMCS_PRI_PROC_BASED_CTLS);
if (enable == 1)
procbased_ctls |= PROCBASED_INT_WINDOW_EXITING;
else
procbased_ctls &= ~PROCBASED_INT_WINDOW_EXITING;
vmcs_write32(VMCS_PRI_PROC_BASED_CTLS, procbased_ctls);
}
Notation tvmid := 99999 % positive.
Notation tpctls := 1 % positive.
Notation tenable := 3 % positive.
Definition vmx_set_intercept_intwin_body :=
(Ssequence
(Scall (Some tpctls)
(Evar vmcs_readz (Tfunction (Tcons tint Tnil) tint cc_default))
((Econst_int (Int.repr 16386) tint) :: nil))
(Ssequence
(Sifthenelse (Ebinop Oeq (Etempvar tenable tint)
(Econst_int (Int.repr 1) tint) tint)
(Sset tpctls
(Ebinop Oor (Etempvar tpctls tint)
(Ebinop Oshl (Econst_int (Int.repr 1) tint)
(Econst_int (Int.repr 2) tint) tint) tint))
(Sset tpctls
(Ebinop Oand (Etempvar tpctls tint)
(Eunop Onotint
(Ebinop Oshl (Econst_int (Int.repr 1) tint)
(Econst_int (Int.repr 2) tint) tint) tint) tint)))
(Scall None
(Evar vmcs_writez (Tfunction (Tcons tint (Tcons tint Tnil)) tvoid
cc_default))
((Econst_int (Int.repr 16386) tint) ::
(Etempvar tpctls tint) :: nil)))).
Definition f_vmx_set_intercept_intwin := {|
fn_return := tvoid;
fn_callconv := cc_default;
fn_params := ((tenable, tint) :: nil);
fn_vars := nil;
fn_temps := ((tpctls, tint) :: nil);
fn_body := vmx_set_intercept_intwin_body
|}.
#define VMCS_ENTRY_INTR_INFO 0x00004016
#define VMCS_INTERRUPTION_INFO_VALID (1U << 31)
#define VMCS_ENTRY_EXCEPTION_ERROR 0x00004018
typedef unsigned char bool;
#define TRUE ((bool) 1)
#define FALSE ((bool) 0)
extern unsigned int vmcs_read32(unsigned int encoding);
extern void vmcs_write32(unsigned int encoding, unsigned int val);
void
vmx_inject_event (unsigned int type, unsigned int vector, unsigned int errcode,
unsigned int ev)
{
unsigned int new_info = VMCS_INTERRUPTION_INFO_VALID | type | vector;
unsigned int intr_info = vmcs_read32 (VMCS_ENTRY_INTR_INFO);
if ((intr_info & VMCS_INTERRUPTION_INFO_VALID) == 0)
{
if (ev == 1)
{
new_info = new_info | (1 << 11);
vmcs_write32 (VMCS_ENTRY_EXCEPTION_ERROR, errcode);
}
vmcs_write32 (VMCS_ENTRY_INTR_INFO, intr_info);
}
}
Notation _type := 4 % positive.
Notation _vector := 5 % positive.
Notation _errcode := 6 % positive.
Notation _ev := 7 % positive.
Notation _new_info := 8 % positive.
Notation _intr_info := 9 % positive.
Definition vmx_inject_event_body :=
(Ssequence
(Sset _new_info
(Ebinop Oor
(Ebinop Oor
(Ebinop Oshl (Econst_int (Int.repr 1) tuint)
(Econst_int (Int.repr 31) tint) tuint) (Etempvar _type tuint)
tuint) (Etempvar _vector tuint) tuint))
(Ssequence
(Scall (Some _intr_info)
(Evar vmcs_readz (Tfunction (Tcons tuint Tnil) tuint cc_default))
((Econst_int (Int.repr 16406) tint) :: nil))
(Sifthenelse (Ebinop Oeq
(Ebinop Oand (Etempvar _intr_info tuint)
(Ebinop Oshl (Econst_int (Int.repr 1) tuint)
(Econst_int (Int.repr 31) tint) tuint) tuint)
(Econst_int (Int.repr 0) tint) tint)
(Sifthenelse (Ebinop Oeq (Etempvar _ev tuint)
(Econst_int (Int.repr 1) tint) tint)
(Ssequence
(Scall None
(Evar vmcs_writez (Tfunction (Tcons tuint (Tcons tuint Tnil))
tvoid cc_default))
((Econst_int (Int.repr 16406) tint) ::
(Ebinop Oor (Etempvar _new_info tuint)
(Ebinop Oshl (Econst_int (Int.repr 1) tint)
(Econst_int (Int.repr 11) tint) tint) tuint) :: nil))
(Scall None
(Evar vmcs_writez (Tfunction (Tcons tuint (Tcons tuint Tnil))
tvoid cc_default))
((Econst_int (Int.repr 16408) tint) ::
(Etempvar _errcode tuint) :: nil)))
(Scall None
(Evar vmcs_writez (Tfunction (Tcons tuint (Tcons tuint Tnil))
tvoid cc_default))
((Econst_int (Int.repr 16406) tint) ::
(Etempvar _new_info tuint) :: nil)))
Sskip))).
Definition f_vmx_inject_event := {|
fn_return := tvoid;
fn_callconv := cc_default;
fn_params := ((_type, tuint) :: (_vector, tuint) :: (_errcode, tuint) ::
(_ev, tuint) :: nil);
fn_vars := nil;
fn_temps := ((_new_info, tuint) :: (_intr_info, tuint) :: nil);
fn_body := vmx_inject_event_body
|}.
#define VMCS_GUEST_INTERRUPTIBILITY 0x00004824
#define VMCS_INTERRUPTIBILITY_STI_BLOCKING (1 << 0)
#define VMCS_INTERRUPTIBILITY_MOVSS_BLOCKING (1 << 1)
extern unsigned int vmcs_read32(unsigned int encoding);
unsigned int
vmx_check_int_shadow()
{
return (vmcs_read32(VMCS_GUEST_INTERRUPTIBILITY) &
(VMCS_INTERRUPTIBILITY_STI_BLOCKING |
VMCS_INTERRUPTIBILITY_MOVSS_BLOCKING)) ? 1 : 0;
}
Definition vmx_check_int_shadow_body :=
(Ssequence
(Ssequence
(Scall (Some 36%positive)
(Evar vmcs_readz (Tfunction (Tcons tint Tnil) tint cc_default))
((Econst_int (Int.repr 18468) tint) :: nil))
(Sifthenelse (Ebinop Oand (Etempvar 36%positive tint)
(Ebinop Oor
(Ebinop Oshl (Econst_int (Int.repr 1) tint)
(Econst_int (Int.repr 0) tint) tint)
(Ebinop Oshl (Econst_int (Int.repr 1) tint)
(Econst_int (Int.repr 1) tint) tint) tint) tint)
(Sset 37%positive (Ecast (Econst_int (Int.repr 1) tint) tint))
(Sset 37%positive (Ecast (Econst_int (Int.repr 0) tint) tint))))
(Sreturn (Some (Etempvar 37%positive tint)))).
Definition f_vmx_check_int_shadow := {|
fn_return := tint;
fn_callconv := cc_default;
fn_params := nil;
fn_vars := nil;
fn_temps := ((37%positive, tint) :: (36%positive, tint) :: nil);
fn_body := vmx_check_int_shadow_body
|}.
#define VMCS_ENTRY_INTR_INFO 0x00004016
#define VMCS_INTERRUPTION_INFO_VALID (1U << 31)
extern unsigned int vmcs_read32(unsigned int encoding);
unsigned int
vmx_check_pending_event()
{
return (vmcs_read32(VMCS_ENTRY_INTR_INFO) &
VMCS_INTERRUPTION_INFO_VALID) ? 1 : 0;
}
Definition vmx_check_pending_event_body :=
(Ssequence
(Ssequence
(Scall (Some 36%positive)
(Evar vmcs_readz (Tfunction (Tcons tint Tnil) tint cc_default))
((Econst_int (Int.repr 16406) tint) :: nil))
(Sifthenelse (Ebinop Oand (Etempvar 36%positive tint)
(Ebinop Oshl (Econst_int (Int.repr 1) tint)
(Econst_int (Int.repr 31) tint) tint) tint)
(Sset 37%positive (Ecast (Econst_int (Int.repr 1) tint) tint))
(Sset 37%positive (Ecast (Econst_int (Int.repr 0) tint) tint))))
(Sreturn (Some (Etempvar 37%positive tint)))).
Definition f_vmx_check_pending_event := {|
fn_return := tint;
fn_callconv := cc_default;
fn_params := nil;
fn_vars := nil;
fn_temps := ((37%positive, tint) :: (36%positive, tint) :: nil);
fn_body := vmx_check_pending_event_body
|}.
enum
{
GUEST_CS = 0,
GUEST_DS,
GUEST_ES,
GUEST_FS,
GUEST_GS,
GUEST_SS,
GUEST_LDTR,
GUEST_TR,
GUEST_GDTR,
GUEST_IDTR,
GUEST_MAX_SEG_DESC
};
#define VMCS_GUEST_ES_SELECTOR 0x00000800
#define VMCS_GUEST_CS_SELECTOR 0x00000802
#define VMCS_GUEST_SS_SELECTOR 0x00000804
#define VMCS_GUEST_DS_SELECTOR 0x00000806
#define VMCS_GUEST_FS_SELECTOR 0x00000808
#define VMCS_GUEST_GS_SELECTOR 0x0000080A
#define VMCS_GUEST_LDTR_SELECTOR 0x0000080C
#define VMCS_GUEST_TR_SELECTOR 0x0000080E
#define VMCS_GUEST_ES_BASE 0x00006806
#define VMCS_GUEST_CS_BASE 0x00006808
#define VMCS_GUEST_SS_BASE 0x0000680A
#define VMCS_GUEST_DS_BASE 0x0000680C
#define VMCS_GUEST_FS_BASE 0x0000680E
#define VMCS_GUEST_GS_BASE 0x00006810
#define VMCS_GUEST_LDTR_BASE 0x00006812
#define VMCS_GUEST_TR_BASE 0x00006814
#define VMCS_GUEST_GDTR_BASE 0x00006816
#define VMCS_GUEST_IDTR_BASE 0x00006818
#define VMCS_GUEST_ES_LIMIT 0x00004800
#define VMCS_GUEST_CS_LIMIT 0x00004802
#define VMCS_GUEST_SS_LIMIT 0x00004804
#define VMCS_GUEST_DS_LIMIT 0x00004806
#define VMCS_GUEST_FS_LIMIT 0x00004808
#define VMCS_GUEST_GS_LIMIT 0x0000480A
#define VMCS_GUEST_LDTR_LIMIT 0x0000480C
#define VMCS_GUEST_TR_LIMIT 0x0000480E
#define VMCS_GUEST_GDTR_LIMIT 0x00004810
#define VMCS_GUEST_IDTR_LIMIT 0x00004812
#define VMCS_GUEST_ES_ACCESS_RIGHTS 0x00004814
#define VMCS_GUEST_CS_ACCESS_RIGHTS 0x00004816
#define VMCS_GUEST_SS_ACCESS_RIGHTS 0x00004818
#define VMCS_GUEST_DS_ACCESS_RIGHTS 0x0000481A
#define VMCS_GUEST_FS_ACCESS_RIGHTS 0x0000481C
#define VMCS_GUEST_GS_ACCESS_RIGHTS 0x0000481E
#define VMCS_GUEST_LDTR_ACCESS_RIGHTS 0x00004820
#define VMCS_GUEST_TR_ACCESS_RIGHTS 0x00004822
extern void vmcs_write32(unsigned int encoding, unsigned int val);
void
vmx_set_desc1 (unsigned int seg, unsigned int sel, unsigned int base)
{
if (seg == GUEST_CS)
{
vmcs_write32 (VMCS_GUEST_CS_BASE, base);
vmcs_write32 (VMCS_GUEST_CS_SELECTOR, sel);
}
else if (seg == GUEST_DS)
{
vmcs_write32 (VMCS_GUEST_DS_BASE, base);
vmcs_write32 (VMCS_GUEST_DS_SELECTOR, sel);
}
else if (seg == GUEST_ES)
{
vmcs_write32 (VMCS_GUEST_ES_BASE, base);
vmcs_write32 (VMCS_GUEST_ES_SELECTOR, sel);
}
else if (seg == GUEST_FS)
{
vmcs_write32 (VMCS_GUEST_FS_BASE, base);
vmcs_write32 (VMCS_GUEST_FS_SELECTOR, sel);
}
else if (seg == GUEST_GS)
{
vmcs_write32 (VMCS_GUEST_GS_BASE, base);
vmcs_write32 (VMCS_GUEST_GS_SELECTOR, sel);
}
else if (seg == GUEST_SS)
{
vmcs_write32 (VMCS_GUEST_SS_BASE, base);
vmcs_write32 (VMCS_GUEST_SS_SELECTOR, sel);
}
else if (seg == GUEST_LDTR)
{
vmcs_write32 (VMCS_GUEST_LDTR_BASE, base);
vmcs_write32 (VMCS_GUEST_LDTR_SELECTOR, sel);
}
else if (seg == GUEST_TR)
{
vmcs_write32 (VMCS_GUEST_TR_BASE, base);
vmcs_write32 (VMCS_GUEST_TR_SELECTOR, sel);
}
else if (seg == GUEST_GDTR)
{
vmcs_write32 (VMCS_GUEST_GDTR_BASE, base);
}
else if (seg == GUEST_IDTR)
{
vmcs_write32 (VMCS_GUEST_IDTR_BASE, base);
}
}
void
vmx_set_desc2 (unsigned int seg, unsigned int lim, unsigned int ar)
{
if (seg == GUEST_CS)
{
vmcs_write32 (VMCS_GUEST_CS_LIMIT, lim);
vmcs_write32 (VMCS_GUEST_CS_ACCESS_RIGHTS, ar);
}
else if (seg == GUEST_DS)
{
vmcs_write32 (VMCS_GUEST_DS_LIMIT, lim);
vmcs_write32 (VMCS_GUEST_DS_ACCESS_RIGHTS, ar);
}
else if (seg == GUEST_ES)
{
vmcs_write32 (VMCS_GUEST_ES_LIMIT, lim);
vmcs_write32 (VMCS_GUEST_ES_ACCESS_RIGHTS, ar);
}
else if (seg == GUEST_FS)
{
vmcs_write32 (VMCS_GUEST_FS_LIMIT, lim);
vmcs_write32 (VMCS_GUEST_FS_ACCESS_RIGHTS, ar);
}
else if (seg == GUEST_GS)
{
vmcs_write32 (VMCS_GUEST_GS_LIMIT, lim);
vmcs_write32 (VMCS_GUEST_GS_ACCESS_RIGHTS, ar);
}
else if (seg == GUEST_SS)
{
vmcs_write32 (VMCS_GUEST_SS_LIMIT, lim);
vmcs_write32 (VMCS_GUEST_SS_ACCESS_RIGHTS, ar);
}
else if (seg == GUEST_LDTR)
{
vmcs_write32 (VMCS_GUEST_LDTR_LIMIT, lim);
vmcs_write32 (VMCS_GUEST_LDTR_ACCESS_RIGHTS, ar);
}
else if (seg == GUEST_TR)
{
vmcs_write32 (VMCS_GUEST_TR_LIMIT, lim);
vmcs_write32 (VMCS_GUEST_TR_ACCESS_RIGHTS, ar);
}
else if (seg == GUEST_GDTR)
{
vmcs_write32 (VMCS_GUEST_GDTR_LIMIT, lim);
}
else if (seg == GUEST_IDTR)
{
vmcs_write32 (VMCS_GUEST_IDTR_LIMIT, lim);
}
}
Notation _base := 10 % positive.
Notation _sel := 11 % positive.
Notation _lim := 12 % positive.
Notation _ar := 13 % positive.
Notation _seg := 14 % positive.
Definition vmx_set_desc1_body :=
(Sifthenelse (Ebinop Oeq (Etempvar _seg tuint) (Econst_int (Int.repr 0) tint)
tint)
(Ssequence
(Scall None
(Evar vmcs_writez (Tfunction (Tcons tuint (Tcons tuint Tnil)) tvoid
cc_default))
((Econst_int (Int.repr 26632) tint) :: (Etempvar _base tuint) :: nil))
(Scall None
(Evar vmcs_writez (Tfunction (Tcons tuint (Tcons tuint Tnil)) tvoid
cc_default))
((Econst_int (Int.repr 2050) tint) :: (Etempvar _sel tuint) :: nil)))
(Sifthenelse (Ebinop Oeq (Etempvar _seg tuint)
(Econst_int (Int.repr 1) tint) tint)
(Ssequence
(Scall None
(Evar vmcs_writez (Tfunction (Tcons tuint (Tcons tuint Tnil)) tvoid
cc_default))
((Econst_int (Int.repr 26636) tint) :: (Etempvar _base tuint) :: nil))
(Scall None
(Evar vmcs_writez (Tfunction (Tcons tuint (Tcons tuint Tnil)) tvoid
cc_default))
((Econst_int (Int.repr 2054) tint) :: (Etempvar _sel tuint) :: nil)))
(Sifthenelse (Ebinop Oeq (Etempvar _seg tuint)
(Econst_int (Int.repr 2) tint) tint)
(Ssequence
(Scall None
(Evar vmcs_writez (Tfunction (Tcons tuint (Tcons tuint Tnil))
tvoid cc_default))
((Econst_int (Int.repr 26630) tint) :: (Etempvar _base tuint) ::
nil))
(Scall None
(Evar vmcs_writez (Tfunction (Tcons tuint (Tcons tuint Tnil))
tvoid cc_default))
((Econst_int (Int.repr 2048) tint) :: (Etempvar _sel tuint) :: nil)))
(Sifthenelse (Ebinop Oeq (Etempvar _seg tuint)
(Econst_int (Int.repr 3) tint) tint)
(Ssequence
(Scall None
(Evar vmcs_writez (Tfunction (Tcons tuint (Tcons tuint Tnil))
tvoid cc_default))
((Econst_int (Int.repr 26638) tint) :: (Etempvar _base tuint) ::
nil))
(Scall None
(Evar vmcs_writez (Tfunction (Tcons tuint (Tcons tuint Tnil))
tvoid cc_default))
((Econst_int (Int.repr 2056) tint) :: (Etempvar _sel tuint) ::
nil)))
(Sifthenelse (Ebinop Oeq (Etempvar _seg tuint)
(Econst_int (Int.repr 4) tint) tint)
(Ssequence
(Scall None
(Evar vmcs_writez (Tfunction (Tcons tuint (Tcons tuint Tnil))
tvoid cc_default))
((Econst_int (Int.repr 26640) tint) ::
(Etempvar _base tuint) :: nil))
(Scall None
(Evar vmcs_writez (Tfunction (Tcons tuint (Tcons tuint Tnil))
tvoid cc_default))
((Econst_int (Int.repr 2058) tint) :: (Etempvar _sel tuint) ::
nil)))
(Sifthenelse (Ebinop Oeq (Etempvar _seg tuint)
(Econst_int (Int.repr 5) tint) tint)
(Ssequence
(Scall None
(Evar vmcs_writez (Tfunction
(Tcons tuint (Tcons tuint Tnil)) tvoid
cc_default))
((Econst_int (Int.repr 26634) tint) ::
(Etempvar _base tuint) :: nil))
(Scall None
(Evar vmcs_writez (Tfunction
(Tcons tuint (Tcons tuint Tnil)) tvoid
cc_default))
((Econst_int (Int.repr 2052) tint) ::
(Etempvar _sel tuint) :: nil)))
(Sifthenelse (Ebinop Oeq (Etempvar _seg tuint)
(Econst_int (Int.repr 6) tint) tint)
(Ssequence
(Scall None
(Evar vmcs_writez (Tfunction
(Tcons tuint (Tcons tuint Tnil))
tvoid cc_default))
((Econst_int (Int.repr 26642) tint) ::
(Etempvar _base tuint) :: nil))
(Scall None
(Evar vmcs_writez (Tfunction
(Tcons tuint (Tcons tuint Tnil))
tvoid cc_default))
((Econst_int (Int.repr 2060) tint) ::
(Etempvar _sel tuint) :: nil)))
(Sifthenelse (Ebinop Oeq (Etempvar _seg tuint)
(Econst_int (Int.repr 7) tint) tint)
(Ssequence
(Scall None
(Evar vmcs_writez (Tfunction
(Tcons tuint (Tcons tuint Tnil))
tvoid cc_default))
((Econst_int (Int.repr 26644) tint) ::
(Etempvar _base tuint) :: nil))
(Scall None
(Evar vmcs_writez (Tfunction
(Tcons tuint (Tcons tuint Tnil))
tvoid cc_default))
((Econst_int (Int.repr 2062) tint) ::
(Etempvar _sel tuint) :: nil)))
(Sifthenelse (Ebinop Oeq (Etempvar _seg tuint)
(Econst_int (Int.repr 8) tint) tint)
(Scall None
(Evar vmcs_writez (Tfunction
(Tcons tuint (Tcons tuint Tnil))
tvoid cc_default))
((Econst_int (Int.repr 26646) tint) ::
(Etempvar _base tuint) :: nil))
(Sifthenelse (Ebinop Oeq (Etempvar _seg tuint)
(Econst_int (Int.repr 9) tint) tint)
(Scall None
(Evar vmcs_writez (Tfunction
(Tcons tuint (Tcons tuint Tnil))
tvoid cc_default))
((Econst_int (Int.repr 26648) tint) ::
(Etempvar _base tuint) :: nil))
Sskip))))))))))
.
Definition f_vmx_set_desc1 := {|
fn_return := tvoid;
fn_callconv := cc_default;
fn_params := ((_seg, tint) :: (_sel, tint) :: (_base, tint) :: nil);
fn_vars := nil;
fn_temps := nil;
fn_body := vmx_set_desc1_body
|}.
Definition vmx_set_desc2_body :=
(Sifthenelse (Ebinop Oeq (Etempvar _seg tuint) (Econst_int (Int.repr 0) tint)
tint)
(Ssequence
(Scall None
(Evar vmcs_writez (Tfunction (Tcons tuint (Tcons tuint Tnil)) tvoid
cc_default))
((Econst_int (Int.repr 18434) tint) :: (Etempvar _lim tuint) :: nil))
(Scall None
(Evar vmcs_writez (Tfunction (Tcons tuint (Tcons tuint Tnil)) tvoid
cc_default))
((Econst_int (Int.repr 18454) tint) :: (Etempvar _ar tuint) :: nil)))
(Sifthenelse (Ebinop Oeq (Etempvar _seg tuint)
(Econst_int (Int.repr 1) tint) tint)
(Ssequence
(Scall None
(Evar vmcs_writez (Tfunction (Tcons tuint (Tcons tuint Tnil)) tvoid
cc_default))
((Econst_int (Int.repr 18438) tint) :: (Etempvar _lim tuint) :: nil))
(Scall None
(Evar vmcs_writez (Tfunction (Tcons tuint (Tcons tuint Tnil)) tvoid
cc_default))
((Econst_int (Int.repr 18458) tint) :: (Etempvar _ar tuint) :: nil)))
(Sifthenelse (Ebinop Oeq (Etempvar _seg tuint)
(Econst_int (Int.repr 2) tint) tint)
(Ssequence
(Scall None
(Evar vmcs_writez (Tfunction (Tcons tuint (Tcons tuint Tnil))
tvoid cc_default))
((Econst_int (Int.repr 18432) tint) :: (Etempvar _lim tuint) ::
nil))
(Scall None
(Evar vmcs_writez (Tfunction (Tcons tuint (Tcons tuint Tnil))
tvoid cc_default))
((Econst_int (Int.repr 18452) tint) :: (Etempvar _ar tuint) :: nil)))
(Sifthenelse (Ebinop Oeq (Etempvar _seg tuint)
(Econst_int (Int.repr 3) tint) tint)
(Ssequence
(Scall None
(Evar vmcs_writez (Tfunction (Tcons tuint (Tcons tuint Tnil))
tvoid cc_default))
((Econst_int (Int.repr 18440) tint) :: (Etempvar _lim tuint) ::
nil))
(Scall None
(Evar vmcs_writez (Tfunction (Tcons tuint (Tcons tuint Tnil))
tvoid cc_default))
((Econst_int (Int.repr 18460) tint) :: (Etempvar _ar tuint) ::
nil)))
(Sifthenelse (Ebinop Oeq (Etempvar _seg tuint)
(Econst_int (Int.repr 4) tint) tint)
(Ssequence
(Scall None
(Evar vmcs_writez (Tfunction (Tcons tuint (Tcons tuint Tnil))
tvoid cc_default))
((Econst_int (Int.repr 18442) tint) :: (Etempvar _lim tuint) ::
nil))
(Scall None
(Evar vmcs_writez (Tfunction (Tcons tuint (Tcons tuint Tnil))
tvoid cc_default))
((Econst_int (Int.repr 18462) tint) :: (Etempvar _ar tuint) ::
nil)))
(Sifthenelse (Ebinop Oeq (Etempvar _seg tuint)
(Econst_int (Int.repr 5) tint) tint)
(Ssequence
(Scall None
(Evar vmcs_writez (Tfunction
(Tcons tuint (Tcons tuint Tnil)) tvoid
cc_default))
((Econst_int (Int.repr 18436) tint) ::
(Etempvar _lim tuint) :: nil))
(Scall None
(Evar vmcs_writez (Tfunction
(Tcons tuint (Tcons tuint Tnil)) tvoid
cc_default))
((Econst_int (Int.repr 18456) tint) ::
(Etempvar _ar tuint) :: nil)))
(Sifthenelse (Ebinop Oeq (Etempvar _seg tuint)
(Econst_int (Int.repr 6) tint) tint)
(Ssequence
(Scall None
(Evar vmcs_writez (Tfunction
(Tcons tuint (Tcons tuint Tnil))
tvoid cc_default))
((Econst_int (Int.repr 18444) tint) ::
(Etempvar _lim tuint) :: nil))
(Scall None
(Evar vmcs_writez (Tfunction
(Tcons tuint (Tcons tuint Tnil))
tvoid cc_default))
((Econst_int (Int.repr 18464) tint) ::
(Etempvar _ar tuint) :: nil)))
(Sifthenelse (Ebinop Oeq (Etempvar _seg tuint)
(Econst_int (Int.repr 7) tint) tint)
(Ssequence
(Scall None
(Evar vmcs_writez (Tfunction
(Tcons tuint (Tcons tuint Tnil))
tvoid cc_default))
((Econst_int (Int.repr 18446) tint) ::
(Etempvar _lim tuint) :: nil))
(Scall None
(Evar vmcs_writez (Tfunction
(Tcons tuint (Tcons tuint Tnil))
tvoid cc_default))
((Econst_int (Int.repr 18466) tint) ::
(Etempvar _ar tuint) :: nil)))
(Sifthenelse (Ebinop Oeq (Etempvar _seg tuint)
(Econst_int (Int.repr 8) tint) tint)
(Scall None
(Evar vmcs_writez (Tfunction
(Tcons tuint (Tcons tuint Tnil))
tvoid cc_default))
((Econst_int (Int.repr 18448) tint) ::
(Etempvar _lim tuint) :: nil))
(Sifthenelse (Ebinop Oeq (Etempvar _seg tuint)
(Econst_int (Int.repr 9) tint) tint)
(Scall None
(Evar vmcs_writez (Tfunction
(Tcons tuint (Tcons tuint Tnil))
tvoid cc_default))
((Econst_int (Int.repr 18450) tint) ::
(Etempvar _lim tuint) :: nil))
Sskip))))))))))
.
Definition f_vmx_set_desc2 := {|
fn_return := tvoid;
fn_callconv := cc_default;
fn_params := ((_seg, tint) :: (_lim, tint) :: (_ar, tint) :: nil);
fn_vars := nil;
fn_temps := nil;
fn_body := vmx_set_desc2_body
|}.
typedef unsigned long long uint64_t;
#define VMCS_TSC_OFFSET 0x00002010
uint64_t vmcs_read64(unsigned int encoding);
uint64_t
vmx_get_tsc_offset (void)
{
return vmcs_read64 (VMCS_TSC_OFFSET);
}
Definition vmx_get_tsc_offset_body :=
(Ssequence
(Scall (Some 36%positive)
(Evar vmcs_readz64 (Tfunction (Tcons tint Tnil) tulong cc_default))
((Econst_int (Int.repr 8208) tint) :: nil))
(Sreturn (Some (Etempvar 36%positive tulong)))).
Definition f_vmx_get_tsc_offset := {|
fn_return := tulong;
fn_callconv := cc_default;
fn_params := nil;
fn_vars := nil;
fn_temps := ((36%positive, tulong) :: nil);
fn_body := vmx_get_tsc_offset_body
|}.
typedef unsigned long long uint64_t;
#define VMCS_TSC_OFFSET 0x00002010
void vmcs_write64(unsigned encoding, uint64_t val);
void
vmx_set_tsc_offset(uint64_t tsc_offset)
{
vmcs_write64(VMCS_TSC_OFFSET, tsc_offset);
}
Notation ttsc_offset := 15 % positive.
Definition vmx_set_tsc_offset_body :=
(Scall None
(Evar vmcs_writez64 (Tfunction (Tcons tint (Tcons tulong Tnil)) tvoid
cc_default))
((Econst_int (Int.repr 8208) tint) :: (Etempvar ttsc_offset tulong) :: nil)).
Definition f_vmx_set_tsc_offset := {|
fn_return := tvoid;
fn_callconv := cc_default;
fn_params := ((ttsc_offset, tulong) :: nil);
fn_vars := nil;
fn_temps := nil;
fn_body := vmx_set_tsc_offset_body
|}.
#define VMCS_EXIT_REASON 0x00004402
#define EXIT_REASON_MASK 0x0000ffff
extern unsigned int vmcs_read32(unsigned int encoding);
unsigned int
vmx_get_exit_reason()
{
unsigned int exit_reason;
exit_reason = vmcs_read32(VMCS_EXIT_REASON);
return (exit_reason & EXIT_REASON_MASK);
}
Notation texit_reason := 16 % positive.
Notation texit_reason´ := 17 % positive.
Definition vmx_get_exit_reason_body :=
(Ssequence
(Ssequence
(Scall (Some texit_reason´)
(Evar vmcs_readz (Tfunction (Tcons tint Tnil) tint cc_default))
((Econst_int (Int.repr 17410) tint) :: nil))
(Sset texit_reason (Etempvar texit_reason´ tint)))
(Sreturn (Some (Ebinop Oand (Etempvar texit_reason tint)
(Econst_int (Int.repr 65535) tint) tint)))).
Definition f_vmx_get_exit_reason := {|
fn_return := tint;
fn_callconv := cc_default;
fn_params := nil;
fn_vars := nil;
fn_temps := ((texit_reason, tint) :: (texit_reason´, tint) :: nil);
fn_body := vmx_get_exit_reason_body
|}.
typedef unsigned int uint32_t;
/* 64-bit read-only fields */
#define VMCS_GUEST_PHYSICAL_ADDRESS 0x00002400
uint32_t vmcs_read32 (unsigned int encoding);
unsigned int
vmx_get_exit_fault_addr (void)
{
unsigned int addr = (unsigned int) vmcs_read32 (
VMCS_GUEST_PHYSICAL_ADDRESS);
return addr;
}
Notation _addr := 18 % positive.
Definition vmx_get_exit_fault_addr_body :=
(Ssequence
(Scall (Some _addr)
(Evar vmcs_readz (Tfunction (Tcons tuint Tnil) tuint cc_default))
((Econst_int (Int.repr 9216) tint) :: nil))
(Sreturn (Some (Etempvar _addr tuint)))).
Definition f_vmx_get_exit_fault_addr := {|
fn_return := tuint;
fn_callconv := cc_default;
fn_params := nil;
fn_vars := nil;
fn_temps := ((_addr, tuint) :: nil);
fn_body := vmx_get_exit_fault_addr_body
|}.
typedef unsigned int uint32_t;
typedef unsigned long long uint64_t;
#define VMX_INFO_VMX_ENABLED 1
#define VMX_INFO_PINBASED_CTLS 2
#define VMX_INFO_PROCBASED_CTLS 3
#define VMX_INFO_PROCBASED_CTLS2 4
#define VMX_INFO_EXIT_CTLS 5
#define VMX_INFO_ENTRY_CTLS 6
#define VMX_INFO_CR0_ONES_MASK 7
#define VMX_INFO_CR0_ZEROS_MASK 8
#define VMX_INFO_CR4_ONES_MASK 9
#define VMX_INFO_CR4_ZEROS_MASK 10
#define VMX_INFO_VMX_REGION 11
#define VMCS_VPID 0x00000000
#define VMCS_PIN_BASED_CTLS 0x00004000
#define VMCS_PRI_PROC_BASED_CTLS 0x00004002
#define VMCS_EXCEPTION_BITMAP 0x00004004
#define VMCS_PF_ERROR_MASK 0x00004006
#define VMCS_PF_ERROR_MATCH 0x00004008
#define VMCS_CR3_TARGET_COUNT 0x0000400A
#define VMCS_EXIT_CTLS 0x0000400C
#define VMCS_EXIT_MSR_STORE_COUNT 0x0000400E
#define VMCS_EXIT_MSR_LOAD_COUNT 0x00004010
#define VMCS_ENTRY_CTLS 0x00004012
#define VMCS_ENTRY_MSR_LOAD_COUNT 0x00004014
#define VMCS_ENTRY_INTR_INFO 0x00004016
#define VMCS_ENTRY_EXCEPTION_ERROR 0x00004018
#define VMCS_ENTRY_INST_LENGTH 0x0000401A
#define VMCS_TPR_THRESHOLD 0x0000401C
#define VMCS_SEC_PROC_BASED_CTLS 0x0000401E
#define VMCS_PLE_GAP 0x00004020
#define VMCS_PLE_WINDOW 0x00004022
#define VMCS_IO_BITMAP_A 0x00002000
#define VMCS_IO_BITMAP_B 0x00002002
#define VMCS_MSR_BITMAP 0x00002004
#define VMCS_EXIT_MSR_STORE 0x00002006
#define VMCS_EXIT_MSR_LOAD 0x00002008
#define VMCS_ENTRY_MSR_LOAD 0x0000200A
#define VMCS_EXECUTIVE_VMCS 0x0000200C
#define VMCS_TSC_OFFSET 0x00002010
#define VMCS_VIRTUAL_APIC 0x00002012
#define VMCS_APIC_ACCESS 0x00002014
#define VMCS_EPTP 0x0000201A
#define VMCS_CR0_MASK 0x00006000
#define VMCS_CR4_MASK 0x00006002
#define VMCS_CR0_SHADOW 0x00006004
#define VMCS_CR4_SHADOW 0x00006006
#define VMCS_CR3_TARGET0 0x00006008
#define VMCS_CR3_TARGET1 0x0000600A
#define VMCS_CR3_TARGET2 0x0000600C
#define VMCS_CR3_TARGET3 0x0000600E
#define VMCS_HOST_CR0 0x00006C00
#define VMCS_HOST_CR3 0x00006C02
#define VMCS_HOST_CR4 0x00006C04
#define VMCS_HOST_FS_BASE 0x00006C06
#define VMCS_HOST_GS_BASE 0x00006C08
#define VMCS_HOST_TR_BASE 0x00006C0A
#define VMCS_HOST_GDTR_BASE 0x00006C0C
#define VMCS_HOST_IDTR_BASE 0x00006C0E
#define VMCS_HOST_IA32_SYSENTER_ESP 0x00006C10
#define VMCS_HOST_IA32_SYSENTER_CS 0x00004C00
#define VMCS_HOST_IA32_SYSENTER_EIP 0x00006C12
#define VMCS_HOST_RSP 0x00006C14
#define VMCS_HOST_RIP 0x00006c16
#define VMCS_HOST_ES_SELECTOR 0x00000C00
#define VMCS_HOST_CS_SELECTOR 0x00000C02
#define VMCS_HOST_SS_SELECTOR 0x00000C04
#define VMCS_HOST_DS_SELECTOR 0x00000C06
#define VMCS_HOST_FS_SELECTOR 0x00000C08
#define VMCS_HOST_GS_SELECTOR 0x00000C0A
#define VMCS_HOST_TR_SELECTOR 0x00000C0C
#define VMCS_HOST_IA32_PAT 0x00002C00
#define VMCS_HOST_IA32_EFER 0x00002C02
#define VMCS_HOST_IA32_PERF_GLOBAL_CTRL 0x00002C04
/* Natural Width guest-state fields */
#define VMCS_GUEST_CR0 0x00006800
#define VMCS_GUEST_CR3 0x00006802
#define VMCS_GUEST_CR4 0x00006804
#define VMCS_GUEST_ES_BASE 0x00006806
#define VMCS_GUEST_CS_BASE 0x00006808
#define VMCS_GUEST_SS_BASE 0x0000680A
#define VMCS_GUEST_DS_BASE 0x0000680C
#define VMCS_GUEST_FS_BASE 0x0000680E
#define VMCS_GUEST_GS_BASE 0x00006810
#define VMCS_GUEST_LDTR_BASE 0x00006812
#define VMCS_GUEST_TR_BASE 0x00006814
#define VMCS_GUEST_GDTR_BASE 0x00006816
#define VMCS_GUEST_IDTR_BASE 0x00006818
#define VMCS_GUEST_DR7 0x0000681A
#define VMCS_GUEST_RSP 0x0000681C
#define VMCS_GUEST_RIP 0x0000681E
#define VMCS_GUEST_RFLAGS 0x00006820
#define VMCS_GUEST_PENDING_DBG_EXCEPTIONS 0x00006822
#define VMCS_GUEST_IA32_SYSENTER_ESP 0x00006824
#define VMCS_GUEST_IA32_SYSENTER_EIP 0x00006826
#define VMCS_LINK_POINTER 0x00002800
#define VMCS_GUEST_IA32_DEBUGCTL 0x00002802
#define VMCS_GUEST_IA32_PAT 0x00002804
#define VMCS_GUEST_IA32_EFER 0x00002806
#define VMCS_GUEST_IA32_PERF_GLOBAL_CTRL 0x00002808
#define VMCS_GUEST_PDPTE0 0x0000280A
#define VMCS_GUEST_PDPTE1 0x0000280C
#define VMCS_GUEST_PDPTE2 0x0000280E
#define VMCS_GUEST_PDPTE3 0x00002810
#define VMCS_GUEST_IA32_SYSENTER_CS 0x0000482A
#define VMCS_GUEST_ACTIVITY 0x00004826
#define VMCS_GUEST_SMBASE 0x00004828
#define VMCS_GUEST_IA32_SYSENTER_CS 0x0000482A
#define VMCS_PREEMPTION_TIMER_VALUE 0x0000482E
#define VMCS_GUEST_INTERRUPTIBILITY 0x00004824
#define MSR_IA32_SYSENTER_CS 0x174
#define MSR_IA32_SYSENTER_ESP 0x175
#define MSR_IA32_SYSENTER_EIP 0x176
#define MSR_PAT 0x277
#define MSR_IA32_PERF_GLOBAL_CTRL 0x38f
#define MSR_EFER 0xc0000080ul
#define CPU_GDT_NULL 0x00 /* null descriptor */
#define CPU_GDT_KCODE 0x08 /* kernel text */
#define CPU_GDT_KDATA 0x10 /* kernel data */
#define CPU_GDT_UCODE 0x18 /* user text */
#define CPU_GDT_UDATA 0x20 /* user data */
#define CPU_GDT_TSS 0x28 /* task state segment */
#define CPU_GDT_NDESC 6 /* number of GDT entries used */
/* CR0 */
#define CR0_PE 0x00000001 /* Protection Enable */
#define CR0_MP 0x00000002 /* Monitor coProcessor */
#define CR0_EM 0x00000004 /* Emulation */
#define CR0_TS 0x00000008 /* Task Switched */
#define CR0_ET 0x00000010 /* Extension Type */
#define CR0_NE 0x00000020 /* Numeric Errror */
#define CR0_WP 0x00010000 /* Write Protect */
#define CR0_AM 0x00040000 /* Alignment Mask */
#define CR0_NW 0x20000000 /* Not Writethrough */
#define CR0_CD 0x40000000 /* Cache Disable */
#define CR0_PG 0x80000000 /* Paging */
/* CR4 */
#define CR4_VME 0x00000001 /* V86 Mode Extensions */
#define CR4_PVI 0x00000002 /* Protected-Mode Virtual Interrupts */
#define CR4_TSD 0x00000004 /* Time Stamp Disable */
#define CR4_DE 0x00000008 /* Debugging Extensions */
#define CR4_PSE 0x00000010 /* Page Size Extensions */
#define CR4_PAE 0x00000020 /* Physical Address Extension */
#define CR4_MCE 0x00000040 /* Machine Check Enable */
#define CR4_PGE 0x00000080 /* Page Global Enable */
#define CR4_PCE 0x00000100 /* Performance counter enable */
#define CR4_OSFXSR 0x00000200 /* SSE and FXSAVE/FXRSTOR enable */
#define CR4_OSXMMEXCPT 0x00000400 /* Unmasked SSE FP exceptions */
#define CR4_VMXE (1<<13) /* enable VMX */
#define num_proc 1024
#define NUM_VMS 8
#define PAGE_SIZE 4096
#define MSR_VMX_BASIC 0x480
#define EPT_SIZE 8413184
#define GDT_OFFSET 0
#define TSS_OFFSET 48
extern void ept_init(void);
extern void vmcs_set_revid(unsigned int id);
extern void vmcs_writez(unsigned int encoding, unsigned int val);
extern void vmcs_writez64(unsigned int encoding, uint64_t val);
extern void vmcs_write_ident(unsigned int encoding, void * addr);
extern void vmptrld(void);
extern unsigned int vmxinfo_get (unsigned int);
extern unsigned int rcr0(void);
extern unsigned int rcr3(void);
extern unsigned int rcr4(void);
extern uint64_t rdmsr(uint32_t msr);
extern unsigned int get_CPU_ID(void);
extern unsigned int get_curid(void);
extern char * EPT_LOC;
extern char STACK_LOC[num_proc][PAGE_SIZE];
extern char idt_LOC[256][64];
extern char msr_bitmap_LOC[NUM_VMS][PAGE_SIZE];
extern char io_bitmap_LOC[NUM_VMS][PAGE_SIZE * 2];
extern char * vmx_return_from_guest;
void
vmcs_set_defaults ()
{
unsigned int cpuid, curid;
cpuid = get_CPU_ID();
curid = get_curid();
ept_init();
vmcs_set_revid(rdmsr (MSR_VMX_BASIC) & 0xffffffffull);
vmptrld ();
/*
* Load the VMX controls
*/
unsigned int pinbased_ctls = vmxinfo_get (VMX_INFO_PINBASED_CTLS);
unsigned int procbased_ctls = vmxinfo_get (VMX_INFO_PROCBASED_CTLS);
unsigned int procbased_ctls2 = vmxinfo_get (VMX_INFO_PROCBASED_CTLS2);
unsigned int exit_ctls = vmxinfo_get (VMX_INFO_EXIT_CTLS);
unsigned int entry_ctls = vmxinfo_get (VMX_INFO_ENTRY_CTLS);
unsigned int cr0_ones_mask = vmxinfo_get (VMX_INFO_CR0_ONES_MASK);
unsigned int cr0_zeros_mask = vmxinfo_get (VMX_INFO_CR0_ZEROS_MASK);
unsigned int cr4_ones_mask = vmxinfo_get (VMX_INFO_CR4_ONES_MASK);
unsigned int cr4_zeros_mask = vmxinfo_get (VMX_INFO_CR4_ZEROS_MASK);
vmcs_writez (VMCS_PIN_BASED_CTLS, pinbased_ctls);
vmcs_writez (VMCS_PRI_PROC_BASED_CTLS, procbased_ctls);
vmcs_writez (VMCS_SEC_PROC_BASED_CTLS, procbased_ctls2);
vmcs_writez (VMCS_EXIT_CTLS, exit_ctls);
vmcs_writez (VMCS_ENTRY_CTLS, entry_ctls);
/*
* Load host state. (Intel Software Developer's Manual Vol 3, Sec 24.5)
*/
/* host rip */
vmcs_write_ident (VMCS_HOST_RIP, vmx_return_from_guest);
/* host control registers */
vmcs_writez (VMCS_HOST_CR0, rcr0 ());
vmcs_writez (VMCS_HOST_CR3, rcr3 ());
vmcs_writez (VMCS_HOST_CR4, rcr4 ());
/* host segment selectors */
vmcs_writez (VMCS_HOST_ES_SELECTOR, CPU_GDT_KDATA);
vmcs_writez (VMCS_HOST_CS_SELECTOR, CPU_GDT_KCODE);
vmcs_writez (VMCS_HOST_SS_SELECTOR, CPU_GDT_KDATA);
vmcs_writez (VMCS_HOST_DS_SELECTOR, CPU_GDT_KDATA);
vmcs_writez (VMCS_HOST_FS_SELECTOR, CPU_GDT_KDATA);
vmcs_writez (VMCS_HOST_GS_SELECTOR, CPU_GDT_KDATA);
vmcs_writez (VMCS_HOST_TR_SELECTOR, CPU_GDT_TSS);
/* host segment base address */
vmcs_writez (VMCS_HOST_FS_BASE, 0);
vmcs_writez (VMCS_HOST_GS_BASE, 0);
//vmcs_write_ident (VMCS_HOST_TR_BASE, STACK_LOC + curid * PAGE_SIZE + TSS_OFFSET);
//vmcs_write_ident (VMCS_HOST_GDTR_BASE, STACK_LOC + curid * PAGE_SIZE + GDT_OFFSET);
vmcs_write_ident (VMCS_HOST_TR_BASE, &STACK_LOC[curid][TSS_OFFSET]);
vmcs_write_ident (VMCS_HOST_GDTR_BASE, &STACK_LOC[curid][GDT_OFFSET]);
vmcs_write_ident (VMCS_HOST_IDTR_BASE, (char * )idt_LOC);
/* host control registers */
vmcs_writez (VMCS_HOST_IA32_SYSENTER_CS, rdmsr (MSR_IA32_SYSENTER_CS));
vmcs_writez (VMCS_HOST_IA32_SYSENTER_ESP, rdmsr (MSR_IA32_SYSENTER_ESP));
vmcs_writez (VMCS_HOST_IA32_SYSENTER_EIP, rdmsr (MSR_IA32_SYSENTER_EIP));
vmcs_writez64 (VMCS_HOST_IA32_PERF_GLOBAL_CTRL,
rdmsr (MSR_IA32_PERF_GLOBAL_CTRL));
vmcs_writez64 (VMCS_HOST_IA32_PAT, rdmsr (MSR_PAT));
vmcs_writez64 (VMCS_HOST_IA32_EFER, rdmsr (MSR_EFER));
/*
* Load guest state. (Intel Software Developer's Manual Vol3, Sec 24.4,
* Sec 9.1)
*/
/* guest control registers */
vmcs_writez (VMCS_GUEST_CR0, 0x60000010 | CR0_NE);
vmcs_writez (VMCS_GUEST_CR3, 0);
vmcs_writez (VMCS_GUEST_CR4, CR4_VMXE);
/* guest debug registers */
vmcs_writez (VMCS_GUEST_DR7, 0x00000400);
/* guest MSRs */
vmcs_writez64 (VMCS_GUEST_IA32_PAT, 0x7040600070406ULL);
vmcs_writez (VMCS_GUEST_IA32_SYSENTER_CS, 0);
vmcs_writez (VMCS_GUEST_IA32_SYSENTER_ESP, 0);
vmcs_writez (VMCS_GUEST_IA32_SYSENTER_EIP, 0);
vmcs_writez64 (VMCS_GUEST_IA32_DEBUGCTL, 0);
/* EPTP */
vmcs_write_ident (VMCS_EPTP, EPT_LOC + cpuid * EPT_SIZE + 0x1e); // | (4 - 1) << 3 | 6
vmcs_writez (VMCS_EPTP + 1, 0);
/* VPID */
vmcs_writez (VMCS_VPID, 1);
/* MSR bitmap */
vmcs_write_ident (VMCS_MSR_BITMAP, msr_bitmap_LOC[cpuid]);
vmcs_writez (VMCS_MSR_BITMAP + 1, 0);
/* link pointer */
vmcs_writez64 (VMCS_LINK_POINTER, 0xffffffffffffffffULL);
/* CR0 mask & shadow */
vmcs_writez (VMCS_CR0_MASK, cr0_ones_mask | cr0_zeros_mask);
vmcs_writez (VMCS_CR0_SHADOW, cr0_ones_mask);
/* CR4 mask & shadow */
vmcs_writez (VMCS_CR4_MASK, cr4_ones_mask | cr4_zeros_mask);
vmcs_writez (VMCS_CR4_SHADOW, cr4_ones_mask);
/* I/O bitmap */
vmcs_write_ident (VMCS_IO_BITMAP_A, io_bitmap_LOC[cpuid]);
vmcs_writez (VMCS_IO_BITMAP_A + 1, 0);
vmcs_write_ident (VMCS_IO_BITMAP_B, io_bitmap_LOC[cpuid] + PAGE_SIZE);
vmcs_writez (VMCS_IO_BITMAP_B + 1, 0);
/* others */
vmcs_writez (VMCS_GUEST_ACTIVITY, 0);
vmcs_writez (VMCS_GUEST_INTERRUPTIBILITY, 0);
vmcs_writez (VMCS_GUEST_PENDING_DBG_EXCEPTIONS, 0);
vmcs_writez (VMCS_ENTRY_INTR_INFO, 0);
}
Notation _pinbased_ctls := 21 % positive.
Notation _procbased_ctls := 22 % positive.
Notation _procbased_ctls2 := 23 % positive.
Notation _exit_ctls := 24 % positive.
Notation _entry_ctls := 25 % positive.
Notation _cr0_ones_mask := 26 % positive.
Notation _cr0_zeros_mask := 27 % positive.
Notation _cr4_ones_mask := 28 % positive.
Notation _cr4_zeros_mask := 29 % positive.
Notation _cr4_zeros_mask´ := 30 % positive.
Notation _cr4_ones_mask´ := 31 % positive.
Notation _cr0_zeros_mask´ := 32 % positive.
Notation _cr0_ones_mask´ := 33 % positive.
Notation _entry_ctls´ := 34 % positive.
Notation _exit_ctls´ := 35 % positive.
Notation _procbased_ctls2´ := 36 % positive.
Notation _procbased_ctls´ := 37 % positive.
Notation _pinbased_ctls´ := 38 % positive.
Notation _cpuid := 388 % positive.
Notation _curid := 3888 % positive.
Definition vmcs_set_defaults_body :=
(Ssequence
(Scall (Some _cpuid)
(Evar get_CPU_ID (Tfunction Tnil tuint cc_default)) nil)
(Ssequence
(Scall (Some _curid)
(Evar get_curid (Tfunction Tnil tuint cc_default)) nil)
(Ssequence
(Scall None (Evar ept_init (Tfunction Tnil tvoid cc_default)) nil)
(Ssequence
(Ssequence
(Scall (Some 67%positive)
(Evar rdmsr (Tfunction (Tcons tuint Tnil) tulong cc_default))
((Econst_int (Int.repr 1152) tint) :: nil))
(Scall None
(Evar vmcs_set_revid (Tfunction (Tcons tuint Tnil) tvoid
cc_default))
((Ebinop Oand (Etempvar 67%positive tulong)
(Econst_long (Int64.repr 4294967295) tulong) tulong) :: nil)))
(Ssequence
(Scall None (Evar vmptrld (Tfunction Tnil tvoid cc_default)) nil)
(Ssequence
(Ssequence
(Scall (Some _pinbased_ctls´)
(Evar vmxinfo_get (Tfunction (Tcons tuint Tnil) tuint
cc_default))
((Econst_int (Int.repr 2) tint) :: nil))
(Sset _pinbased_ctls (Etempvar _pinbased_ctls´ tuint)))
(Ssequence
(Ssequence
(Scall (Some _procbased_ctls´)
(Evar vmxinfo_get (Tfunction (Tcons tuint Tnil) tuint
cc_default))
((Econst_int (Int.repr 3) tint) :: nil))
(Sset _procbased_ctls (Etempvar _procbased_ctls´ tuint)))
(Ssequence
(Ssequence
(Scall (Some _procbased_ctls2´)
(Evar vmxinfo_get (Tfunction (Tcons tuint Tnil) tuint
cc_default))
((Econst_int (Int.repr 4) tint) :: nil))
(Sset _procbased_ctls2 (Etempvar _procbased_ctls2´ tuint)))
(Ssequence
(Ssequence
(Scall (Some _exit_ctls´)
(Evar vmxinfo_get (Tfunction (Tcons tuint Tnil) tuint
cc_default))
((Econst_int (Int.repr 5) tint) :: nil))
(Sset _exit_ctls (Etempvar _exit_ctls´ tuint)))
(Ssequence
(Ssequence
(Scall (Some _entry_ctls´)
(Evar vmxinfo_get (Tfunction (Tcons tuint Tnil)
tuint cc_default))
((Econst_int (Int.repr 6) tint) :: nil))
(Sset _entry_ctls (Etempvar _entry_ctls´ tuint)))
(Ssequence
(Ssequence
(Scall (Some _cr0_ones_mask´)
(Evar vmxinfo_get (Tfunction (Tcons tuint Tnil)
tuint cc_default))
((Econst_int (Int.repr 7) tint) :: nil))
(Sset _cr0_ones_mask
(Etempvar _cr0_ones_mask´ tuint)))
(Ssequence
(Ssequence
(Scall (Some _cr0_zeros_mask´)
(Evar vmxinfo_get (Tfunction (Tcons tuint Tnil)
tuint cc_default))
((Econst_int (Int.repr 8) tint) :: nil))
(Sset _cr0_zeros_mask
(Etempvar _cr0_zeros_mask´ tuint)))
(Ssequence
(Ssequence
(Scall (Some _cr4_ones_mask´)
(Evar vmxinfo_get (Tfunction
(Tcons tuint Tnil) tuint
cc_default))
((Econst_int (Int.repr 9) tint) :: nil))
(Sset _cr4_ones_mask
(Etempvar _cr4_ones_mask´ tuint)))
(Ssequence
(Ssequence
(Scall (Some _cr4_zeros_mask´)
(Evar vmxinfo_get (Tfunction
(Tcons tuint Tnil) tuint
cc_default))
((Econst_int (Int.repr 10) tint) :: nil))
(Sset _cr4_zeros_mask
(Etempvar _cr4_zeros_mask´ tuint)))
(Ssequence
(Scall None
(Evar vmcs_writez (Tfunction
(Tcons tuint
(Tcons tuint Tnil))
tvoid cc_default))
((Econst_int (Int.repr 16384) tint) ::
(Etempvar _pinbased_ctls tuint) :: nil))
(Ssequence
(Scall None
(Evar vmcs_writez (Tfunction
(Tcons tuint
(Tcons tuint Tnil))
tvoid cc_default))
((Econst_int (Int.repr 16386) tint) ::
(Etempvar _procbased_ctls tuint) :: nil))
(Ssequence
(Scall None
(Evar vmcs_writez (Tfunction
(Tcons tuint
(Tcons tuint Tnil))
tvoid cc_default))
((Econst_int (Int.repr 16414) tint) ::
(Etempvar _procbased_ctls2 tuint) ::
nil))
(Ssequence
(Scall None
(Evar vmcs_writez (Tfunction
(Tcons tuint
(Tcons tuint
Tnil)) tvoid
cc_default))
((Econst_int (Int.repr 16396) tint) ::
(Etempvar _exit_ctls tuint) :: nil))
(Ssequence
(Scall None
(Evar vmcs_writez (Tfunction
(Tcons tuint
(Tcons tuint
Tnil)) tvoid
cc_default))
((Econst_int (Int.repr 16402) tint) ::
(Etempvar _entry_ctls tuint) :: nil))
(Ssequence
(Scall None
(Evar vmcs_write_ident (Tfunction
(Tcons
tuint
(Tcons
(tptr tvoid)
Tnil))
tvoid
cc_default))
((Econst_int (Int.repr 27670) tint) ::
(Eaddrof (Evar vmx_return_from_guest (tptr tchar)) (tptr tchar)) ::
nil))
(Ssequence
(Ssequence
(Scall (Some 77%positive)
(Evar rcr0 (Tfunction Tnil
tuint cc_default))
nil)
(Scall None
(Evar vmcs_writez (Tfunction
(Tcons
tuint
(Tcons
tuint
Tnil))
tvoid
cc_default))
((Econst_int (Int.repr 27648) tint) ::
(Etempvar 77%positive tuint) ::
nil)))
(Ssequence
(Ssequence
(Scall (Some 78%positive)
(Evar rcr3 (Tfunction Tnil
tuint
cc_default))
nil)
(Scall None
(Evar vmcs_writez (Tfunction
(Tcons
tuint
(Tcons
tuint
Tnil))
tvoid
cc_default))
((Econst_int (Int.repr 27650) tint) ::
(Etempvar 78%positive tuint) ::
nil)))
(Ssequence
(Ssequence
(Scall (Some 79%positive)
(Evar rcr4 (Tfunction Tnil
tuint
cc_default))
nil)
(Scall None
(Evar vmcs_writez
(Tfunction
(Tcons tuint
(Tcons tuint Tnil))
tvoid cc_default))
((Econst_int (Int.repr 27652) tint) ::
(Etempvar 79%positive tuint) ::
nil)))
(Ssequence
(Scall None
(Evar vmcs_writez
(Tfunction
(Tcons tuint
(Tcons tuint Tnil))
tvoid cc_default))
((Econst_int (Int.repr 3072) tint) ::
(Econst_int (Int.repr 16) tint) ::
nil))
(Ssequence
(Scall None
(Evar vmcs_writez
(Tfunction
(Tcons tuint
(Tcons tuint Tnil))
tvoid cc_default))
((Econst_int (Int.repr 3074) tint) ::
(Econst_int (Int.repr 8) tint) ::
nil))
(Ssequence
(Scall None
(Evar vmcs_writez
(Tfunction
(Tcons tuint
(Tcons tuint Tnil))
tvoid cc_default))
((Econst_int (Int.repr 3076) tint) ::
(Econst_int (Int.repr 16) tint) ::
nil))
(Ssequence
(Scall None
(Evar vmcs_writez
(Tfunction
(Tcons tuint
(Tcons tuint
Tnil)) tvoid
cc_default))
((Econst_int (Int.repr 3078) tint) ::
(Econst_int (Int.repr 16) tint) ::
nil))
(Ssequence
(Scall None
(Evar vmcs_writez
(Tfunction
(Tcons tuint
(Tcons tuint
Tnil)) tvoid
cc_default))
((Econst_int (Int.repr 3080) tint) ::
(Econst_int (Int.repr 16) tint) ::
nil))
(Ssequence
(Scall None
(Evar vmcs_writez
(Tfunction
(Tcons tuint
(Tcons tuint
Tnil))
tvoid
cc_default))
((Econst_int (Int.repr 3082) tint) ::
(Econst_int (Int.repr 16) tint) ::
nil))
(Ssequence
(Scall None
(Evar vmcs_writez
(Tfunction
(Tcons tuint
(Tcons
tuint
Tnil))
tvoid
cc_default))
((Econst_int (Int.repr 3084) tint) ::
(Econst_int (Int.repr 40) tint) ::
nil))
(Ssequence
(Scall None
(Evar vmcs_writez
(Tfunction
(Tcons
tuint
(Tcons
tuint
Tnil))
tvoid
cc_default))
((Econst_int (Int.repr 27654) tint) ::
(Econst_int (Int.repr 0) tint) ::
nil))
(Ssequence
(Scall None
(Evar vmcs_writez
(Tfunction
(Tcons
tuint
(Tcons
tuint
Tnil))
tvoid
cc_default))
((Econst_int (Int.repr 27656) tint) ::
(Econst_int (Int.repr 0) tint) ::
nil))
(Ssequence
(Scall None
(Evar vmcs_write_ident
(Tfunction
(Tcons
tuint
(Tcons
(tptr tvoid)
Tnil))
tvoid
cc_default))
((Econst_int (Int.repr 27658) tint) :: (Ebinop Oadd
(Ederef
(Ebinop Oadd
(Evar STACK_LOC (tarray (tarray tchar 4096) 1024))
(Etempvar _curid tuint)
(tptr (tarray tchar 4096)))
(tarray tchar 4096))
(Econst_int (Int.repr TSS_OFFSET) tint)
(tptr tchar)) ::
nil))
(Ssequence
(Scall None
(Evar vmcs_write_ident
(Tfunction
(Tcons
tuint
(Tcons
(tptr tvoid)
Tnil))
tvoid
cc_default))
((Econst_int (Int.repr 27660) tint) ::
(Ebinop Oadd
(Ederef
(Ebinop Oadd
(Evar STACK_LOC (tarray (tarray tchar 4096) 1024))
(Etempvar _curid tuint)
(tptr (tarray tchar 4096)))
(tarray tchar 4096))
(Econst_int (Int.repr 0) tint)
(tptr tchar)) ::
nil))
(Ssequence
(Scall None
(Evar vmcs_write_ident
(Tfunction
(Tcons
tuint
(Tcons
(tptr tvoid)
Tnil))
tvoid
cc_default))
((Econst_int (Int.repr 27662) tint) ::
(Ecast
(Eaddrof (Evar idt_LOC (tarray (tarray tchar 64) 256)) (tptr tchar))
(tptr tchar)) ::
nil))
(Ssequence
(Ssequence
(Scall (Some 80%positive)
(Evar rdmsr
(Tfunction
(Tcons
tuint
Tnil)
tulong
cc_default))
((Econst_int (Int.repr 372) tint) ::
nil))
(Scall None
(Evar vmcs_writez
(Tfunction
(Tcons
tuint
(Tcons
tuint
Tnil))
tvoid
cc_default))
((Econst_int (Int.repr 19456) tint) ::
(Etempvar 80%positive tulong) ::
nil)))
(Ssequence
(Ssequence
(Scall (Some 81%positive)
(Evar rdmsr
(Tfunction
(Tcons
tuint
Tnil)
tulong
cc_default))
((Econst_int (Int.repr 373) tint) ::
nil))
(Scall None
(Evar vmcs_writez
(Tfunction
(Tcons
tuint
(Tcons
tuint
Tnil))
tvoid
cc_default))
((Econst_int (Int.repr 27664) tint) ::
(Etempvar 81%positive tulong) ::
nil)))
(Ssequence
(Ssequence
(Scall (Some 82%positive)
(Evar rdmsr
(Tfunction
(Tcons
tuint
Tnil)
tulong
cc_default))
((Econst_int (Int.repr 374) tint) ::
nil))
(Scall None
(Evar vmcs_writez
(Tfunction
(Tcons
tuint
(Tcons
tuint
Tnil))
tvoid
cc_default))
((Econst_int (Int.repr 27666) tint) ::
(Etempvar 82%positive tulong) ::
nil)))
(Ssequence
(Ssequence
(Scall (Some 83%positive)
(Evar rdmsr
(Tfunction
(Tcons
tuint
Tnil)
tulong
cc_default))
((Econst_int (Int.repr 911) tint) ::
nil))
(Scall None
(Evar vmcs_writez64
(Tfunction
(Tcons
tuint
(Tcons
tulong
Tnil))
tvoid
cc_default))
((Econst_int (Int.repr 11268) tint) ::
(Etempvar 83%positive tulong) ::
nil)))
(Ssequence
(Ssequence
(Scall (Some 84%positive)
(Evar rdmsr
(Tfunction
(Tcons
tuint
Tnil)
tulong
cc_default))
((Econst_int (Int.repr 631) tint) ::
nil))
(Scall None
(Evar vmcs_writez64
(Tfunction
(Tcons
tuint
(Tcons
tulong
Tnil))
tvoid
cc_default))
((Econst_int (Int.repr 11264) tint) ::
(Etempvar 84%positive tulong) ::
nil)))
(Ssequence
(Ssequence
(Scall (Some 85%positive)
(Evar rdmsr
(Tfunction
(Tcons
tuint
Tnil)
tulong
cc_default))
((Econst_int (Int.repr (3221225600)) tuint) ::
nil))
(Scall None
(Evar vmcs_writez64
(Tfunction
(Tcons
tuint
(Tcons
tulong
Tnil))
tvoid
cc_default))
((Econst_int (Int.repr 11266) tint) ::
(Etempvar 85%positive tulong) ::
nil)))
(Ssequence
(Scall None
(Evar vmcs_writez
(Tfunction
(Tcons
tuint
(Tcons
tuint
Tnil))
tvoid
cc_default))
((Econst_int (Int.repr 26624) tint) ::
(Ebinop Oor
(Econst_int (Int.repr 1610612752) tint)
(Econst_int (Int.repr 32) tint)
tint) ::
nil))
(Ssequence
(Scall None
(Evar vmcs_writez
(Tfunction
(Tcons
tuint
(Tcons
tuint
Tnil))
tvoid
cc_default))
((Econst_int (Int.repr 26626) tint) ::
(Econst_int (Int.repr 0) tint) ::
nil))
(Ssequence
(Scall None
(Evar vmcs_writez
(Tfunction
(Tcons
tuint
(Tcons
tuint
Tnil))
tvoid
cc_default))
((Econst_int (Int.repr 26628) tint) ::
(Ebinop Oshl
(Econst_int (Int.repr 1) tint)
(Econst_int (Int.repr 13) tint)
tint) ::
nil))
(Ssequence
(Scall None
(Evar vmcs_writez
(Tfunction
(Tcons
tuint
(Tcons
tuint
Tnil))
tvoid
cc_default))
((Econst_int (Int.repr 26650) tint) ::
(Econst_int (Int.repr 1024) tint) ::
nil))
(Ssequence
(Scall None
(Evar vmcs_writez64
(Tfunction
(Tcons
tuint
(Tcons
tulong
Tnil))
tvoid
cc_default))
((Econst_int (Int.repr 10244) tint) ::
(Econst_long (Int64.repr 1974748653749254) tulong) ::
nil))
(Ssequence
(Scall None
(Evar vmcs_writez
(Tfunction
(Tcons
tuint
(Tcons
tuint
Tnil))
tvoid
cc_default))
((Econst_int (Int.repr 18474) tint) ::
(Econst_int (Int.repr 0) tint) ::
nil))
(Ssequence
(Scall None
(Evar vmcs_writez
(Tfunction
(Tcons
tuint
(Tcons
tuint
Tnil))
tvoid
cc_default))
((Econst_int (Int.repr 26660) tint) ::
(Econst_int (Int.repr 0) tint) ::
nil))
(Ssequence
(Scall None
(Evar vmcs_writez
(Tfunction
(Tcons
tuint
(Tcons
tuint
Tnil))
tvoid
cc_default))
((Econst_int (Int.repr 26662) tint) ::
(Econst_int (Int.repr 0) tint) ::
nil))
(Ssequence
(Scall None
(Evar vmcs_writez64
(Tfunction
(Tcons
tuint
(Tcons
tulong
Tnil))
tvoid
cc_default))
((Econst_int (Int.repr 10242) tint) ::
(Econst_int (Int.repr 0) tint) ::
nil))
(Ssequence
(Scall None
(Evar vmcs_write_ident
(Tfunction
(Tcons
tuint
(Tcons
(tptr tvoid)
Tnil))
tvoid
cc_default))
((Econst_int (Int.repr 8218) tint) ::
(Ebinop Oadd
(Ebinop Oadd
(Eaddrof (Evar EPT_LOC (tptr tchar)) (tptr tchar))
(Ebinop Omul
(Etempvar _cpuid tuint)
(Econst_int (Int.repr 8413184) tint)
tuint)
(tptr tchar))
(Econst_int (Int.repr 30) tint)
(tptr tchar)) ::
nil))
(Ssequence
(Scall None
(Evar vmcs_writez
(Tfunction
(Tcons
tuint
(Tcons
tuint
Tnil))
tvoid
cc_default))
((Ebinop Oadd
(Econst_int (Int.repr 8218) tint)
(Econst_int (Int.repr 1) tint)
tint) ::
(Econst_int (Int.repr 0) tint) ::
nil))
(Ssequence
(Scall None
(Evar vmcs_writez
(Tfunction
(Tcons
tuint
(Tcons
tuint
Tnil))
tvoid
cc_default))
((Econst_int (Int.repr 0) tint) ::
(Econst_int (Int.repr 1) tint) ::
nil))
(Ssequence
(Scall None
(Evar vmcs_write_ident
(Tfunction
(Tcons
tuint
(Tcons
(tptr tvoid)
Tnil))
tvoid
cc_default))
((Econst_int (Int.repr 8196) tint) ::
(Ederef
(Ebinop Oadd
(Evar msr_bitmap_LOC (tarray (tarray tchar 4096) 8))
(Etempvar _cpuid tuint)
(tptr (tarray tchar 4096)))
(tarray tchar 4096)) ::
nil))
(Ssequence
(Scall None
(Evar vmcs_writez
(Tfunction
(Tcons
tuint
(Tcons
tuint
Tnil))
tvoid
cc_default))
((Ebinop Oadd
(Econst_int (Int.repr 8196) tint)
(Econst_int (Int.repr 1) tint)
tint) ::
(Econst_int (Int.repr 0) tint) ::
nil))
(Ssequence
(Scall None
(Evar vmcs_writez64
(Tfunction
(Tcons
tuint
(Tcons
tulong
Tnil))
tvoid
cc_default))
((Econst_int (Int.repr 10240) tint) ::
(Econst_long (Int64.repr (18446744073709551615)) tulong) ::
nil))
(Ssequence
(Scall None
(Evar vmcs_writez
(Tfunction
(Tcons
tuint
(Tcons
tuint
Tnil))
tvoid
cc_default))
((Econst_int (Int.repr 24576) tint) ::
(Ebinop Oor
(Etempvar _cr0_ones_mask tuint)
(Etempvar _cr0_zeros_mask tuint)
tuint) ::
nil))
(Ssequence
(Scall None
(Evar vmcs_writez
(Tfunction
(Tcons
tuint
(Tcons
tuint
Tnil))
tvoid
cc_default))
((Econst_int (Int.repr 24580) tint) ::
(Etempvar _cr0_ones_mask tuint) ::
nil))
(Ssequence
(Scall None
(Evar vmcs_writez
(Tfunction
(Tcons
tuint
(Tcons
tuint
Tnil))
tvoid
cc_default))
((Econst_int (Int.repr 24578) tint) ::
(Ebinop Oor
(Etempvar _cr4_ones_mask tuint)
(Etempvar _cr4_zeros_mask tuint)
tuint) ::
nil))
(Ssequence
(Scall None
(Evar vmcs_writez
(Tfunction
(Tcons
tuint
(Tcons
tuint
Tnil))
tvoid
cc_default))
((Econst_int (Int.repr 24582) tint) ::
(Etempvar _cr4_ones_mask tuint) ::
nil))
(Ssequence
(Scall None
(Evar vmcs_write_ident
(Tfunction
(Tcons
tuint
(Tcons
(tptr tvoid)
Tnil))
tvoid
cc_default))
((Econst_int (Int.repr 8192) tint) ::
(Ederef
(Ebinop Oadd
(Evar io_bitmap_LOC (tarray (tarray tchar 8192) 8))
(Etempvar _cpuid tuint)
(tptr (tarray tchar 8192)))
(tarray tchar 8192)) ::
nil))
(Ssequence
(Scall None
(Evar vmcs_writez
(Tfunction
(Tcons
tuint
(Tcons
tuint
Tnil))
tvoid
cc_default))
((Ebinop Oadd
(Econst_int (Int.repr 8192) tint)
(Econst_int (Int.repr 1) tint)
tint) ::
(Econst_int (Int.repr 0) tint) ::
nil))
(Ssequence
(Scall None
(Evar vmcs_write_ident
(Tfunction
(Tcons
tuint
(Tcons
(tptr tvoid)
Tnil))
tvoid
cc_default))
((Econst_int (Int.repr 8194) tint) ::
(Ebinop Oadd
(Ederef
(Ebinop Oadd
(Evar io_bitmap_LOC (tarray (tarray tchar 8192) 8))
(Etempvar _cpuid tuint)
(tptr (tarray tchar 8192)))
(tarray tchar 8192))
(Econst_int (Int.repr 4096) tint)
(tptr tchar)) ::
nil))
(Ssequence
(Scall None
(Evar vmcs_writez
(Tfunction
(Tcons
tuint
(Tcons
tuint
Tnil))
tvoid
cc_default))
((Ebinop Oadd
(Econst_int (Int.repr 8194) tint)
(Econst_int (Int.repr 1) tint)
tint) ::
(Econst_int (Int.repr 0) tint) ::
nil))
(Ssequence
(Scall None
(Evar vmcs_writez
(Tfunction
(Tcons
tuint
(Tcons
tuint
Tnil))
tvoid
cc_default))
((Econst_int (Int.repr 18470) tint) ::
(Econst_int (Int.repr 0) tint) ::
nil))
(Ssequence
(Scall None
(Evar vmcs_writez
(Tfunction
(Tcons
tuint
(Tcons
tuint
Tnil))
tvoid
cc_default))
((Econst_int (Int.repr 18468) tint) ::
(Econst_int (Int.repr 0) tint) ::
nil))
(Ssequence
(Scall None
(Evar vmcs_writez
(Tfunction
(Tcons
tuint
(Tcons
tuint
Tnil))
tvoid
cc_default))
((Econst_int (Int.repr 26658) tint) ::
(Econst_int (Int.repr 0) tint) ::
nil))
(Scall None
(Evar vmcs_writez
(Tfunction
(Tcons
tuint
(Tcons
tuint
Tnil))
tvoid
cc_default))
((Econst_int (Int.repr 16406) tint) ::
(Econst_int (Int.repr 0) tint) ::
nil)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
.
Definition f_vmcs_set_defaults := {|
fn_return := tvoid;
fn_callconv := cc_default;
fn_params := nil;
fn_vars := nil;
fn_temps := ((_cpuid, tuint) :: (_curid, tuint) ::
(_pinbased_ctls, tuint) :: (_procbased_ctls, tuint) ::
(_procbased_ctls2, tuint) :: (_exit_ctls, tuint) ::
(_entry_ctls, tuint) :: (_cr0_ones_mask, tuint) ::
(_cr0_zeros_mask, tuint) :: (_cr4_ones_mask, tuint) ::
(_cr4_zeros_mask, tuint) :: (85%positive, tulong) ::
(84%positive, tulong) :: (83%positive, tulong) ::
(82%positive, tulong) :: (81%positive, tulong) ::
(80%positive, tulong) :: (79%positive, tuint) ::
(78%positive, tuint) :: (77%positive, tuint) ::
(_cr4_zeros_mask´, tuint) :: (_cr4_ones_mask´, tuint) ::
(_cr0_zeros_mask´, tuint) :: (_cr0_ones_mask´, tuint) ::
(_entry_ctls´, tuint) :: (_exit_ctls´, tuint) ::
(_procbased_ctls2´, tuint) :: (_procbased_ctls´, tuint) ::
(_pinbased_ctls´, tuint) :: (67%positive, tulong) :: nil);
fn_body := vmcs_set_defaults_body
|}.