Library mcertikos.proc.VVMXIntroCSource
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 C_GUEST_EIP 8
#define C_GUEST_EFLAGS 9
#define C_GUEST_CR0 10
#define C_GUEST_CR2 11
#define C_GUEST_CR3 12
#define C_GUEST_CR4 13
#define VMX_G_RAX 0
#define VMX_G_RBX 2
#define VMX_G_RCX 4
#define VMX_G_RDX 6
#define VMX_G_RSI 8
#define VMX_G_RDI 10
#define VMX_G_RBP 12
#define VMX_G_RIP 14
#define VMX_G_CR2 16
#define C_VMCS_GUEST_RSP 26652
#define C_VMCS_GUEST_RFLAGS 26656
#define C_VMCS_GUEST_CR0 26624
#define C_VMCS_GUEST_CR3 26626
#define C_VMCS_GUEST_CR4 26628
extern unsigned int vmcs_readz(unsigned int);
extern unsigned int vmx_readz(unsigned int);
unsigned int vmx_get_reg(unsigned int reg)
{
unsigned int result;
if (reg == C_GUEST_EAX)
result = vmx_readz(VMX_G_RAX);
else if (reg == C_GUEST_EBX)
result = vmx_readz(VMX_G_RBX);
else if (reg == C_GUEST_ECX)
result = vmx_readz(VMX_G_RCX);
else if (reg == C_GUEST_EDX)
result = vmx_readz(VMX_G_RDX);
else if (reg == C_GUEST_ESI)
result = vmx_readz(VMX_G_RSI);
else if (reg == C_GUEST_EDI)
result = vmx_readz(VMX_G_RDI);
else if (reg == C_GUEST_CR2)
result = vmx_readz(VMX_G_CR2);
else if (reg == C_GUEST_EBP)
result = vmx_readz(VMX_G_RBP);
else if (reg == C_GUEST_EIP)
result = vmx_readz(VMX_G_RIP);
else if (reg == C_GUEST_ESP)
result = vmcs_readz(C_VMCS_GUEST_RSP);
else if (reg == C_GUEST_EFLAGS)
result = vmcs_readz(C_VMCS_GUEST_RFLAGS);
else if (reg == C_GUEST_CR0)
result = vmcs_readz(C_VMCS_GUEST_CR0);
else if (reg == C_GUEST_CR3)
result = vmcs_readz(C_VMCS_GUEST_CR3);
else if (reg == C_GUEST_CR4)
result = vmcs_readz(C_VMCS_GUEST_CR4);
return result;
}
Definition _reg := 1 % positive.
Definition _result := 2 % positive.
Definition vmx_get_reg_body :=
(Ssequence
(Sifthenelse (Ebinop Oeq (Etempvar _reg tint)
(Econst_int (Int.repr 0) tint) tint)
(Scall (Some _result)
(Evar vmx_readz (Tfunction (Tcons tint Tnil) tint cc_default))
((Econst_int (Int.repr 0) tint) :: nil))
(Sifthenelse (Ebinop Oeq (Etempvar _reg tint)
(Econst_int (Int.repr 1) tint) tint)
(Scall (Some _result)
(Evar vmx_readz (Tfunction (Tcons tint Tnil) tint cc_default))
((Econst_int (Int.repr 2) tint) :: nil))
(Sifthenelse (Ebinop Oeq (Etempvar _reg tint)
(Econst_int (Int.repr 2) tint) tint)
(Scall (Some _result)
(Evar vmx_readz (Tfunction (Tcons tint Tnil) tint cc_default))
((Econst_int (Int.repr 4) tint) :: nil))
(Sifthenelse (Ebinop Oeq (Etempvar _reg tint)
(Econst_int (Int.repr 3) tint) tint)
(Scall (Some _result)
(Evar vmx_readz (Tfunction (Tcons tint Tnil) tint
cc_default))
((Econst_int (Int.repr 6) tint) :: nil))
(Sifthenelse (Ebinop Oeq (Etempvar _reg tint)
(Econst_int (Int.repr 4) tint) tint)
(Scall (Some _result)
(Evar vmx_readz (Tfunction (Tcons tint Tnil) tint
cc_default))
((Econst_int (Int.repr 8) tint) :: nil))
(Sifthenelse (Ebinop Oeq (Etempvar _reg tint)
(Econst_int (Int.repr 5) tint) tint)
(Scall (Some _result)
(Evar vmx_readz (Tfunction (Tcons tint Tnil) tint
cc_default))
((Econst_int (Int.repr 10) tint) :: nil))
(Sifthenelse (Ebinop Oeq (Etempvar _reg tint)
(Econst_int (Int.repr 11) tint) tint)
(Scall (Some _result)
(Evar vmx_readz (Tfunction (Tcons tint Tnil) tint
cc_default))
((Econst_int (Int.repr 16) tint) :: nil))
(Sifthenelse (Ebinop Oeq (Etempvar _reg tint)
(Econst_int (Int.repr 6) tint) tint)
(Scall (Some _result)
(Evar vmx_readz (Tfunction (Tcons tint Tnil) tint
cc_default))
((Econst_int (Int.repr 12) tint) :: nil))
(Sifthenelse (Ebinop Oeq (Etempvar _reg tint)
(Econst_int (Int.repr 8) tint) tint)
(Scall (Some _result)
(Evar vmx_readz (Tfunction (Tcons tint Tnil) tint
cc_default))
((Econst_int (Int.repr 14) tint) :: nil))
(Sifthenelse (Ebinop Oeq (Etempvar _reg tint)
(Econst_int (Int.repr 7) tint) tint)
(Scall (Some _result)
(Evar vmcs_readz (Tfunction (Tcons tint Tnil)
tint cc_default))
((Econst_int (Int.repr 26652) tint) :: nil))
(Sifthenelse (Ebinop Oeq (Etempvar _reg tint)
(Econst_int (Int.repr 9) tint) tint)
(Scall (Some _result)
(Evar vmcs_readz (Tfunction (Tcons tint Tnil)
tint cc_default))
((Econst_int (Int.repr 26656) tint) :: nil))
(Sifthenelse (Ebinop Oeq (Etempvar _reg tint)
(Econst_int (Int.repr 10) tint) tint)
(Scall (Some _result)
(Evar vmcs_readz (Tfunction (Tcons tint Tnil)
tint cc_default))
((Econst_int (Int.repr 26624) tint) :: nil))
(Sifthenelse (Ebinop Oeq (Etempvar _reg tint)
(Econst_int (Int.repr 12) tint)
tint)
(Scall (Some _result)
(Evar vmcs_readz (Tfunction
(Tcons tint Tnil) tint
cc_default))
((Econst_int (Int.repr 26626) tint) :: nil))
(Sifthenelse (Ebinop Oeq (Etempvar _reg tint)
(Econst_int (Int.repr 13) tint)
tint)
(Scall (Some _result)
(Evar vmcs_readz (Tfunction
(Tcons tint Tnil)
tint cc_default))
((Econst_int (Int.repr 26628) tint) :: nil))
Sskip))))))))))))))
(Sreturn (Some (Etempvar _result tint)))).
Definition f_vmx_get_reg := {|
fn_return := tint;
fn_callconv := cc_default;
fn_params := ((_reg, tint) :: nil);
fn_vars := nil;
fn_temps := ((_result, tint) :: nil);
fn_body := vmx_get_reg_body
|}.
#define C_GUEST_EIP 8
#define C_GUEST_EFLAGS 9
#define C_GUEST_CR0 10
#define C_GUEST_CR2 11
#define C_GUEST_CR3 12
#define C_GUEST_CR4 13
#define VMX_G_RAX 0
#define VMX_G_RBX 2
#define VMX_G_RCX 4
#define VMX_G_RDX 6
#define VMX_G_RSI 8
#define VMX_G_RDI 10
#define VMX_G_RBP 12
#define VMX_G_RIP 14
#define VMX_G_CR2 16
#define C_VMCS_GUEST_RSP 26652
#define C_VMCS_GUEST_RFLAGS 26656
#define C_VMCS_GUEST_CR0 26624
#define C_VMCS_GUEST_CR3 26626
#define C_VMCS_GUEST_CR4 26628
extern void vmcs_writez(unsigned int, unsigned int);
extern void vmx_writez(unsigned int, unsigned int);
void vmx_set_reg(unsigned int reg, unsigned int val)
{
if (reg == C_GUEST_EAX)
vmx_writez(VMX_G_RAX, val);
else if (reg == C_GUEST_EBX)
vmx_writez(VMX_G_RBX, val);
else if (reg == C_GUEST_ECX)
vmx_writez(VMX_G_RCX, val);
else if (reg == C_GUEST_EDX)
vmx_writez(VMX_G_RDX, val);
else if (reg == C_GUEST_ESI)
vmx_writez(VMX_G_RSI, val);
else if (reg == C_GUEST_EDI)
vmx_writez(VMX_G_RDI, val);
else if (reg == C_GUEST_CR2)
vmx_writez(VMX_G_CR2, val);
else if (reg == C_GUEST_EBP)
vmx_writez(VMX_G_RBP, val);
else if (reg == C_GUEST_EIP)
vmx_writez(VMX_G_RIP, val);
else if (reg == C_GUEST_ESP)
vmcs_writez(C_VMCS_GUEST_RSP, val);
else if (reg == C_GUEST_EFLAGS)
vmcs_writez(C_VMCS_GUEST_RFLAGS, val);
else if (reg == C_GUEST_CR0)
vmcs_writez(C_VMCS_GUEST_CR0, val);
else if (reg == C_GUEST_CR3)
vmcs_writez(C_VMCS_GUEST_CR3, val);
else if (reg == C_GUEST_CR4)
vmcs_writez(C_VMCS_GUEST_CR4, val);
}
Definition _val := 3 % positive.
Definition vmx_set_reg_body :=
(Sifthenelse (Ebinop Oeq (Etempvar _reg tuint) (Econst_int (Int.repr 0) tint)
tint)
(Scall None
(Evar vmx_writez (Tfunction (Tcons tuint (Tcons tuint Tnil)) tvoid
cc_default))
((Econst_int (Int.repr 0) tint) :: (Etempvar _val tuint) :: nil))
(Sifthenelse (Ebinop Oeq (Etempvar _reg tuint)
(Econst_int (Int.repr 1) tint) tint)
(Scall None
(Evar vmx_writez (Tfunction (Tcons tuint (Tcons tuint Tnil)) tvoid
cc_default))
((Econst_int (Int.repr 2) tint) :: (Etempvar _val tuint) :: nil))
(Sifthenelse (Ebinop Oeq (Etempvar _reg tuint)
(Econst_int (Int.repr 2) tint) tint)
(Scall None
(Evar vmx_writez (Tfunction (Tcons tuint (Tcons tuint Tnil)) tvoid
cc_default))
((Econst_int (Int.repr 4) tint) :: (Etempvar _val tuint) :: nil))
(Sifthenelse (Ebinop Oeq (Etempvar _reg tuint)
(Econst_int (Int.repr 3) tint) tint)
(Scall None
(Evar vmx_writez (Tfunction (Tcons tuint (Tcons tuint Tnil)) tvoid
cc_default))
((Econst_int (Int.repr 6) tint) :: (Etempvar _val tuint) :: nil))
(Sifthenelse (Ebinop Oeq (Etempvar _reg tuint)
(Econst_int (Int.repr 4) tint) tint)
(Scall None
(Evar vmx_writez (Tfunction (Tcons tuint (Tcons tuint Tnil))
tvoid cc_default))
((Econst_int (Int.repr 8) tint) :: (Etempvar _val tuint) :: nil))
(Sifthenelse (Ebinop Oeq (Etempvar _reg tuint)
(Econst_int (Int.repr 5) tint) tint)
(Scall None
(Evar vmx_writez (Tfunction (Tcons tuint (Tcons tuint Tnil))
tvoid cc_default))
((Econst_int (Int.repr 10) tint) :: (Etempvar _val tuint) ::
nil))
(Sifthenelse (Ebinop Oeq (Etempvar _reg tuint)
(Econst_int (Int.repr 11) tint) tint)
(Scall None
(Evar vmx_writez (Tfunction (Tcons tuint (Tcons tuint Tnil))
tvoid cc_default))
((Econst_int (Int.repr 16) tint) :: (Etempvar _val tuint) ::
nil))
(Sifthenelse (Ebinop Oeq (Etempvar _reg tuint)
(Econst_int (Int.repr 6) tint) tint)
(Scall None
(Evar vmx_writez (Tfunction
(Tcons tuint (Tcons tuint Tnil)) tvoid
cc_default))
((Econst_int (Int.repr 12) tint) ::
(Etempvar _val tuint) :: nil))
(Sifthenelse (Ebinop Oeq (Etempvar _reg tuint)
(Econst_int (Int.repr 8) tint) tint)
(Scall None
(Evar vmx_writez (Tfunction
(Tcons tuint (Tcons tuint Tnil))
tvoid cc_default))
((Econst_int (Int.repr 14) tint) ::
(Etempvar _val tuint) :: nil))
(Sifthenelse (Ebinop Oeq (Etempvar _reg tuint)
(Econst_int (Int.repr 7) tint) tint)
(Scall None
(Evar vmcs_writez (Tfunction
(Tcons tuint (Tcons tuint Tnil))
tvoid cc_default))
((Econst_int (Int.repr 26652) tint) ::
(Etempvar _val tuint) :: nil))
(Sifthenelse (Ebinop Oeq (Etempvar _reg 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 26656) tint) ::
(Etempvar _val tuint) :: nil))
(Sifthenelse (Ebinop Oeq (Etempvar _reg tuint)
(Econst_int (Int.repr 10) tint) tint)
(Scall None
(Evar vmcs_writez (Tfunction
(Tcons tuint
(Tcons tuint Tnil)) tvoid
cc_default))
((Econst_int (Int.repr 26624) tint) ::
(Etempvar _val tuint) :: nil))
(Sifthenelse (Ebinop Oeq (Etempvar _reg tuint)
(Econst_int (Int.repr 12) tint) tint)
(Scall None
(Evar vmcs_writez (Tfunction
(Tcons tuint
(Tcons tuint Tnil)) tvoid
cc_default))
((Econst_int (Int.repr 26626) tint) ::
(Etempvar _val tuint) :: nil))
(Sifthenelse (Ebinop Oeq (Etempvar _reg tuint)
(Econst_int (Int.repr 13) tint)
tint)
(Scall None
(Evar vmcs_writez (Tfunction
(Tcons tuint
(Tcons tuint Tnil))
tvoid cc_default))
((Econst_int (Int.repr 26628) tint) ::
(Etempvar _val tuint) :: nil))
Sskip)))))))))))))).
Definition f_vmx_set_reg := {|
fn_return := tvoid;
fn_callconv := cc_default;
fn_params := ((_reg, tuint) :: (_val, tuint) :: nil);
fn_vars := nil;
fn_temps := nil;
fn_body := vmx_set_reg_body
|}.
#define VMX_G_RIP 14
#define VMCS_EXIT_ITRUCTION_LENGTH 17420
extern unsigned int vmcs_readz(unsigned int);
extern unsigned int vmx_readz(unsigned int);
unsigned int vmx_get_next_eip()
{
return vmx_readz(VMX_G_RIP) + vmcs_readz(VMCS_EXIT_ITRUCTION_LENGTH);
}
Definition _grip := 4 % positive.
Definition _exit_instruction_length := 5 % positive.
Definition vmx_get_next_eip_body :=
(Ssequence
(Ssequence
(Scall (Some _grip)
(Evar vmx_readz (Tfunction (Tcons tuint Tnil) tuint cc_default))
((Econst_int (Int.repr 14) tint) :: nil))
(Scall (Some _exit_instruction_length)
(Evar vmcs_readz (Tfunction (Tcons tuint Tnil) tuint cc_default))
((Econst_int (Int.repr 17420) tint) :: nil)))
(Sreturn (Some (Ebinop Oadd (Etempvar _grip tuint)
(Etempvar _exit_instruction_length tuint) tuint)))).
Definition f_vmx_get_next_eip := {|
fn_return := tuint;
fn_callconv := cc_default;
fn_params := nil;
fn_vars := nil;
fn_temps := ((_grip, tuint) :: (_exit_instruction_length, tuint) :: nil);
fn_body := vmx_get_next_eip_body
|}.
#define VMX_EXIT_QUALIFICATION 28
#define EXIT_QUAL_IO_ONE_BYTE 0
#define EXIT_QUAL_IO_TWO_BYTE 1
#define EXIT_QUAL_IO_FOUR_BYTE 3
#define SZ8 0
#define SZ16 1
#define SZ32 2
extern unsigned int vmx_readz(unsigned int);
unsigned int vmx_get_exit_qualification()
{
return vmx_readz(VMX_EXIT_QUALIFICATION);
}
Definition vmx_get_exit_qualification_body :=
(Ssequence
(Scall (Some 36%positive)
(Evar vmx_readz (Tfunction (Tcons tuint Tnil) tuint cc_default))
((Econst_int (Int.repr 28) tint) :: nil))
(Sreturn (Some (Etempvar 36%positive tuint)))).
Definition f_vmx_get_exit_qualification := {|
fn_return := tuint;
fn_callconv := cc_default;
fn_params := nil;
fn_vars := nil;
fn_temps := ((36%positive, tuint) :: nil);
fn_body := vmx_get_exit_qualification_body
|}.
#define VMX_EXIT_QUALIFICATION 28
#define EXIT_QUAL_IO_ONE_BYTE 0
#define EXIT_QUAL_IO_TWO_BYTE 1
#define EXIT_QUAL_IO_FOUR_BYTE 3
#define SZ8 0
#define SZ16 1
#define SZ32 2
extern unsigned int vmx_readz(unsigned int);
unsigned int vmx_get_io_width()
{
unsigned int eq;
unsigned int width;
eq = vmx_readz(VMX_EXIT_QUALIFICATION);
eq = eq & 7;
if (eq == EXIT_QUAL_IO_ONE_BYTE)
width = SZ8;
else if (eq == EXIT_QUAL_IO_TWO_BYTE)
width = SZ16;
else
width = SZ32;
return width;
}
Definition _eq := 6 % positive.
Definition _width := 7 % positive.
Definition vmx_get_io_width_body :=
(Ssequence
(Scall (Some _eq)
(Evar vmx_readz (Tfunction (Tcons tuint Tnil) tuint cc_default))
((Econst_int (Int.repr 28) tint) :: nil))
(Ssequence
(Sset _eq
(Ebinop Oand (Etempvar _eq tuint) (Econst_int (Int.repr 7) tint) tuint))
(Ssequence
(Sifthenelse (Ebinop Oeq (Etempvar _eq tuint)
(Econst_int (Int.repr 0) tint) tint)
(Sset _width (Econst_int (Int.repr 0) tint))
(Sifthenelse (Ebinop Oeq (Etempvar _eq tuint)
(Econst_int (Int.repr 1) tint) tint)
(Sset _width (Econst_int (Int.repr 1) tint))
(Sset _width (Econst_int (Int.repr 2) tint))))
(Sreturn (Some (Etempvar _width tuint)))))).
Definition f_vmx_get_io_width := {|
fn_return := tuint;
fn_callconv := cc_default;
fn_params := nil;
fn_vars := nil;
fn_temps := ((_eq, tuint) :: (_width, tuint) :: nil);
fn_body := vmx_get_io_width_body
|}.
#define VMX_EXIT_QUALIFICATION 28
#define EXIT_QUAL_IO_OUT 0
#define EXIT_QUAL_IO_IN 1
extern unsigned int vmx_readz(unsigned int);
unsigned int vmx_get_io_write()
{
unsigned int eq;
unsigned int write;
eq = vmx_readz(VMX_EXIT_QUALIFICATION);
if (((eq
3) & 1) == EXIT_QUAL_IO_IN)
write = 0;
else
write = 1;
return write;
}
>>
Definition _write := 8 % positive.
Definition vmx_get_io_write_body :=
(Ssequence
(Scall (Some _eq)
(Evar vmx_readz (Tfunction (Tcons tuint Tnil) tuint cc_default))
((Econst_int (Int.repr 28) tint) :: nil))
(Ssequence
(Sifthenelse (Ebinop Oeq
(Ebinop Oand
(Ebinop Oshr (Etempvar _eq tuint)
(Econst_int (Int.repr 3) tint) tuint)
(Econst_int (Int.repr 1) tint) tuint)
(Econst_int (Int.repr 1) tint) tint)
(Sset _write (Econst_int (Int.repr 0) tint))
(Sset _write (Econst_int (Int.repr 1) tint)))
(Sreturn (Some (Etempvar _write tuint))))).
Definition f_vmx_get_io_write := {|
fn_return := tuint;
fn_callconv := cc_default;
fn_params := nil;
fn_vars := nil;
fn_temps := ((_eq, tuint) :: (_write, tuint) :: nil);
fn_body := vmx_get_io_write_body
|}.
#define VMX_EXIT_QUALIFICATION 28
extern unsigned int vmx_readz(unsigned int);
unsigned int vmx_get_exit_io_rep()
{
unsigned int eq;
unsigned int rep;
eq = vmx_readz(VMX_EXIT_QUALIFICATION);
rep = (eq
5) & 1;
return rep;
}
>>
Definition _rep := 9 % positive.
Definition vmx_get_exit_io_rep_body :=
(Ssequence
(Scall (Some _eq)
(Evar vmx_readz (Tfunction (Tcons tuint Tnil) tuint cc_default))
((Econst_int (Int.repr 28) tint) :: nil))
(Ssequence
(Sset _rep
(Ebinop Oand
(Ebinop Oshr (Etempvar _eq tuint) (Econst_int (Int.repr 5) tint)
tuint) (Econst_int (Int.repr 1) tint) tuint))
(Sreturn (Some (Etempvar _rep tuint))))).
Definition f_vmx_get_exit_io_rep := {|
fn_return := tuint;
fn_callconv := cc_default;
fn_params := nil;
fn_vars := nil;
fn_temps := ((_eq, tuint) :: (_rep, tuint) :: nil);
fn_body := vmx_get_exit_io_rep_body
|}.
#define VMX_EXIT_QUALIFICATION 28
extern unsigned int vmx_readz(unsigned int);
unsigned int vmx_get_exit_io_str()
{
unsigned int eq;
unsigned int str;
eq = vmx_readz(VMX_EXIT_QUALIFICATION);
str = (eq
4) & 1;
return str;
}
>>
Definition _str := 10 % positive.
Definition vmx_get_exit_io_str_body :=
(Ssequence
(Scall (Some _eq)
(Evar vmx_readz (Tfunction (Tcons tuint Tnil) tuint cc_default))
((Econst_int (Int.repr 28) tint) :: nil))
(Ssequence
(Sset _str
(Ebinop Oand
(Ebinop Oshr (Etempvar _eq tuint) (Econst_int (Int.repr 4) tint)
tuint) (Econst_int (Int.repr 1) tint) tuint))
(Sreturn (Some (Etempvar _str tuint))))).
Definition f_vmx_get_exit_io_str := {|
fn_return := tuint;
fn_callconv := cc_default;
fn_params := nil;
fn_vars := nil;
fn_temps := ((_eq, tuint) :: (_str, tuint) :: nil);
fn_body := vmx_get_exit_io_str_body
|}.
#define VMX_EXIT_QUALIFICATION 28
#define C_EXIT_QUAL_IO_PORT 65536
extern unsigned int vmx_readz(unsigned int);
unsigned int vmx_get_exit_io_port()
{
unsigned int eq;
eq = vmx_readz(VMX_EXIT_QUALIFICATION);
return eq / C_EXIT_QUAL_IO_PORT;
}
Definition vmx_get_exit_io_port_body :=
(Ssequence
(Scall (Some _eq)
(Evar vmx_readz (Tfunction (Tcons tuint Tnil) tuint cc_default))
((Econst_int (Int.repr 28) tint) :: nil))
(Sreturn (Some (Ebinop Odiv (Etempvar _eq tuint)
(Econst_int (Int.repr 65536) tuint) tuint)))).
Definition f_vmx_get_exit_io_port := {|
fn_return := tuint;
fn_callconv := cc_default;
fn_params := nil;
fn_vars := nil;
fn_temps := ((_eq, tuint) :: nil);
fn_body := vmx_get_exit_io_port_body
|}.
extern unsigned int ept_add_mapping(unsigned int, unsigned int, unsigned int);
extern unsigned int ept_invalidate_mappings(void);
unsigned int vmx_set_mmap(unsigned int gpa, unsigned int hpa, unsigned int mem_type)
{
unsigned int rc;
rc = ept_add_mapping(gpa, hpa, mem_type);
if (rc == 0)
rc = ept_invalidate_mappings();
return rc;
}
Definition _gpa := 11 % positive.
Definition _hpa := 12 % positive.
Definition _mem_type := 13 % positive.
Definition _rc := 14 % positive.
Definition vmx_set_mmap_body :=
(Ssequence
(Scall (Some _rc)
(Evar ept_add_mapping (Tfunction
(Tcons tuint (Tcons tuint (Tcons tuint Tnil)))
tuint cc_default))
((Etempvar _gpa tuint) :: (Etempvar _hpa tuint) ::
(Etempvar _mem_type tuint) :: nil))
(Ssequence
(Sifthenelse (Ebinop Oeq (Etempvar _rc tuint)
(Econst_int (Int.repr 0) tint) tint)
(Scall (Some _rc)
(Evar ept_invalidate_mappings (Tfunction Tnil tuint cc_default))
nil)
Sskip)
(Sreturn (Some (Etempvar _rc tuint)))))
.
Definition f_vmx_set_mmap := {|
fn_return := tuint;
fn_callconv := cc_default;
fn_params := ((_gpa, tuint) :: (_hpa, tuint) :: (_mem_type, tuint) :: nil);
fn_vars := nil;
fn_temps := ((_rc, tuint) :: nil);
fn_body := vmx_set_mmap_body
|}.
#define VMX_G_RIP 14
#define VMX_VPID 26
#define VMX_G_CR2 16
#define VMX_G_DR0 17
#define VMX_G_DR1 18
#define VMX_G_DR2 19
#define VMX_G_DR3 20
#define VMX_G_DR6 21
extern void vmcs_set_defaults(void);
extern void vmx_writez(unsigned int, unsigned int);
void vmx_init(unsigned int mbi_adr)
{
vmcs_set_defaults();
vmx_writez(VMX_G_RIP, 0xfff0);
vmx_writez(VMX_VPID, 1);
vmx_writez(VMX_G_CR2, 0);
vmx_writez(VMX_G_DR0, 0);
vmx_writez(VMX_G_DR1, 0);
vmx_writez(VMX_G_DR2, 0);
vmx_writez(VMX_G_DR3, 0);
vmx_writez(VMX_G_DR6, 0xffff0ff0);
}
Definition vmx_init_body :=
(Ssequence
(Scall None
(Evar vmcs_set_defaults (Tfunction Tnil tvoid cc_default)) nil)
(Ssequence
(Scall None
(Evar vmx_writez (Tfunction (Tcons tuint (Tcons tuint Tnil)) tvoid
cc_default))
((Econst_int (Int.repr 14) tint) ::
(Econst_int (Int.repr 65520) tint) :: nil))
(Ssequence
(Scall None
(Evar vmx_writez (Tfunction (Tcons tuint (Tcons tuint Tnil)) tvoid
cc_default))
((Econst_int (Int.repr 26) tint) :: (Econst_int (Int.repr 1) tint) ::
nil))
(Ssequence
(Scall None
(Evar vmx_writez (Tfunction (Tcons tuint (Tcons tuint Tnil)) tvoid
cc_default))
((Econst_int (Int.repr 16) tint) ::
(Econst_int (Int.repr 0) tint) :: nil))
(Ssequence
(Scall None
(Evar vmx_writez (Tfunction (Tcons tuint (Tcons tuint Tnil))
tvoid cc_default))
((Econst_int (Int.repr 17) tint) ::
(Econst_int (Int.repr 0) tint) :: nil))
(Ssequence
(Scall None
(Evar vmx_writez (Tfunction (Tcons tuint (Tcons tuint Tnil))
tvoid cc_default))
((Econst_int (Int.repr 18) tint) ::
(Econst_int (Int.repr 0) tint) :: nil))
(Ssequence
(Scall None
(Evar vmx_writez (Tfunction (Tcons tuint (Tcons tuint Tnil))
tvoid cc_default))
((Econst_int (Int.repr 19) tint) ::
(Econst_int (Int.repr 0) tint) :: nil))
(Ssequence
(Scall None
(Evar vmx_writez (Tfunction
(Tcons tuint (Tcons tuint Tnil)) tvoid
cc_default))
((Econst_int (Int.repr 20) tint) ::
(Econst_int (Int.repr 0) tint) :: nil))
(Scall None
(Evar vmx_writez (Tfunction
(Tcons tuint (Tcons tuint Tnil)) tvoid
cc_default))
((Econst_int (Int.repr 21) tint) ::
(Econst_int (Int.repr (4294905840)) tuint) :: nil)))))))))).
Definition f_vmx_init := {|
fn_return := tvoid;
fn_callconv := cc_default;
fn_params := nil;
fn_vars := nil;
fn_temps := nil;
fn_body := vmx_init_body
|}.