Library mcertikos.virt.intel.VVMCSInitCode
*********************************************************************** * * * 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 TacticsForTesting.
Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import MemoryX.
Require Import EventsX.
Require Import Globalenvs.
Require Import Locations.
Require Import Smallstep.
Require Import ClightBigstep.
Require Import Cop.
Require Import ZArith.Zwf.
Require Import RealParams.
Require Import LoopProof.
Require Import VCGen.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import CompatClightSem.
Require Import PrimSemantics.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import VMXIntroGenSpec.
Require Import VVMCSInitCSource.
Require Import AbstractDataType.
Require Import ObjVMCS.
Require Import Constant.
Module VVMCSInitCode.
Section WithPrimitives.
Context `{real_params_ops : RealParamsOps}.
Context {memb} `{Hmemx: Mem.MemoryModelX memb}.
Context `{Hmwd: UseMemWithData memb}.
Let mem := mwd (cdata RData).
Context `{Hstencil: Stencil}.
Context `{make_program_ops: !MakeProgramOps Clight.function type Clight.fundef type}.
Context `{Hmake_program: !MakeProgram Clight.function type Clight.fundef type}.
Local Open Scope Z_scope.
Lemma tptrsize: sizeof (Tpointer tuint noattr) = 4.
Proof. reflexivity. Qed.
Section VMXREADZ.
Let L: compatlayer (cdata RData) := VMX_LOC ↦ v_VMX_LOC.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section VMXReadZBody.
Context `{Hwb: WritableBlockAllowGlobals}.
Variables (ge: genv).
Variable bvmx_loc: block.
Hypothesis hvmx_loc1 : Genv.find_symbol ge VMX_LOC = Some bvmx_loc.
Lemma VMX_readz_body_correct: ∀ m d env le vmx_idx vmx_val,
env = PTree.empty _ →
PTree.get _vmx_idx le = Some (Vint vmx_idx) →
0 ≤ (Int.unsigned vmx_idx) < VMX_Size´ →
Mem.load Mint32 (m, d) bvmx_loc ((Int.unsigned vmx_idx) × 4) = Some (Vint vmx_val) →
exec_stmt ge env le ((m, d): mem) vmx_readz_body E0 le (m, d) (Out_return (Some (Vint vmx_val, tint))).
Proof.
intros; subst.
generalize max_unsigned_val; intro muval.
generalize tptrsize; intro tptrsize.
generalize tintsize; intro tintsize.
unfold vmx_readz_body.
repeat vcgen.
unfold Mem.loadv.
rewrite tintsize.
rewrite Z.add_0_l.
rewrite Z.mul_comm.
rewrite Int.unsigned_repr; [assumption | omega].
Qed.
End VMXReadZBody.
Theorem VMX_readz_code_correct:
spec_le (vmx_readz ↦ vmx_readz_spec_low) (〚vmx_readz ↦ f_vmx_readz 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
destruct m´.
fbigstep (VMX_readz_body_correct (Genv.globalenv p) b0 H m l (PTree.empty _)
(bind_parameter_temps´ (fn_params f_vmx_readz)
(Vint i::nil)
(create_undef_temps (fn_temps f_vmx_readz)))) H0.
Qed.
End VMXREADZ.
Section VMXWRITEZ.
Let L: compatlayer (cdata RData) := VMX_LOC ↦ v_VMX_LOC.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section VMXWriteZBody.
Context `{Hwb: WritableBlockAllowGlobals}.
Variables (ge: genv).
Variable bvmx_loc: block.
Hypothesis hvmx_loc1 : Genv.find_symbol ge VMX_LOC = Some bvmx_loc.
Lemma VMX_writez_body_correct: ∀ m m´ d env le vmx_idx vmx_val,
env = PTree.empty _ →
PTree.get _vmx_idx le = Some (Vint vmx_idx) →
PTree.get _vmx_val le = Some (Vint vmx_val) →
0 ≤ (Int.unsigned vmx_idx) < VMX_Size´ →
Mem.store Mint32 (m, d) bvmx_loc ((Int.unsigned vmx_idx) × 4) (Vint vmx_val) = Some (m´, d) →
exec_stmt ge env le ((m, d): mem) vmx_writez_body E0 le (m´, d) Out_normal.
Proof.
intros; subst.
generalize max_unsigned_val; intro muval.
generalize tptrsize; intro tptrsize.
generalize tintsize; intro tintsize.
unfold vmx_writez_body.
repeat vcgen.
unfold Mem.storev.
rewrite tintsize.
rewrite Z.add_0_l.
rewrite Z.mul_comm.
rewrite Int.unsigned_repr; [assumption | omega].
Qed.
End VMXWriteZBody.
Theorem VMX_writez_code_correct:
spec_le (vmx_writez ↦ vmx_writez_spec_low) (〚vmx_writez ↦ f_vmx_writez 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
destruct m´.
destruct m.
destruct H1.
fbigstep (VMX_writez_body_correct (Genv.globalenv p) b0 H m m0 l (PTree.empty _)
(bind_parameter_temps´ (fn_params f_vmx_writez)
(Vint i::Vint v::nil)
(create_undef_temps (fn_temps f_vmx_writez)))) H0.
Qed.
End VMXWRITEZ.
Section VMXENTERPRE.
Let L: compatlayer (cdata RData) := VMX_LOC ↦ v_VMX_LOC ⊕ vmcs_writez ↦ gensem vmcs_writez_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section VMXEnterPreBody.
Context `{Hwb: WritableBlockAllowGlobals}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Variable bvmx_loc: block.
Hypothesis hvmx_loc1 : Genv.find_symbol ge VMX_LOC = Some bvmx_loc.
Variable bvmcs_writez: block.
Hypothesis hvmcs_writez1 : Genv.find_symbol ge vmcs_writez = Some bvmcs_writez.
Hypothesis hvmcs_writez2 : Genv.find_funct_ptr ge bvmcs_writez = Some (External (EF_external vmcs_writez (signature_of_type (Tcons tint (Tcons tint Tnil)) tvoid cc_default)) (Tcons tint (Tcons tint Tnil)) tvoid cc_default).
Lemma VMX_enter_pre_body_correct: ∀ m d d´ env le val,
env = PTree.empty _ →
Mem.load Mint32 ((m, d): mem) bvmx_loc VMX_G_RIP = Some (Vint val) →
vmcs_writez_spec C_VMCS_GUEST_RIP (Int.unsigned val) d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) vmx_enter_pre_body E0 le´ (m, d´) Out_normal.
Proof.
intros; subst.
generalize max_unsigned_val; intro muval.
generalize tptrsize; intro tptrsize.
generalize tintsize; intro tintsize.
unfold vmx_enter_pre_body.
esplit.
repeat vcgen.
Qed.
End VMXEnterPreBody.
Theorem VMX_enter_pre_code_correct:
spec_le (vmx_enter_pre ↦ vmx_enter_pre_spec_low) (〚vmx_enter_pre ↦ f_vmx_enter_pre 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep (VMX_enter_pre_body_correct s (Genv.globalenv p) makeglobalenv b0 H b2 Hb2fs Hb2fp m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_vmx_enter_pre)
(nil)
(create_undef_temps (fn_temps f_vmx_enter_pre)))) H2.
Qed.
End VMXENTERPRE.
Section VMXEXITPOST.
Let L: compatlayer (cdata RData) := VMX_LOC ↦ v_VMX_LOC ⊕ vmcs_readz ↦ gensem vmcs_readz_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section VMXExitPostBody.
Context `{Hwb: WritableBlockAllowGlobals}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Variable bvmx_loc: block.
Hypothesis hvmx_loc1 : Genv.find_symbol ge VMX_LOC = Some bvmx_loc.
Variable bvmcs_readz: block.
Hypothesis hvmcs_readz1 : Genv.find_symbol ge vmcs_readz = Some bvmcs_readz.
Hypothesis hvmcs_readz2 : Genv.find_funct_ptr ge bvmcs_readz = Some (External (EF_external vmcs_readz (signature_of_type (Tcons tint Tnil) tint cc_default)) (Tcons tint Tnil) tint cc_default).
Lemma VMX_exit_post_body_correct: ∀ m m´ m´´ m´´´ m´´´´ d env le val0 val1 val2,
env = PTree.empty _ →
vmcs_readz_spec C_VMCS_GUEST_RIP d = Some (Int.unsigned val0) →
vmcs_readz_spec C_VMCS_EXIT_REASON d = Some (Int.unsigned val1) →
vmcs_readz_spec C_VMCS_EXIT_QUALIFICATION d = Some (Int.unsigned val2) →
Mem.store Mint32 ((m, d): mem) bvmx_loc VMX_G_RIP (Vint val0) = Some (m´, d) →
Mem.store Mint32 ((m´, d): mem) bvmx_loc VMX_EXIT_REASON (Vint val1) = Some (m´´, d) →
Mem.store Mint32 ((m´´, d): mem) bvmx_loc VMX_EXIT_QUALIFICATION (Vint val2) = Some (m´´´, d) →
Mem.store Mint32 ((m´´´, d): mem) bvmx_loc VMX_LAUNCHED Vone = Some (m´´´´, d) →
∃ le´,
exec_stmt ge env le ((m, d): mem) vmx_exit_post_body E0 le´ (m´´´´, d) Out_normal.
Proof.
intros; subst.
generalize max_unsigned_val; intro muval.
generalize tptrsize; intro tptrsize.
generalize tintsize; intro tintsize.
unfold vmx_exit_post_body.
esplit.
repeat vcgen.
Qed.
End VMXExitPostBody.
Theorem VMX_exit_post_code_correct:
spec_le (vmx_exit_post ↦ vmx_exit_post_spec_low) (〚vmx_exit_post ↦ f_vmx_exit_post 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep (VMX_exit_post_body_correct s (Genv.globalenv p) makeglobalenv b0 H b2 Hb2fs Hb2fp m´0 m0 m1 m2 m3 labd (PTree.empty _)
(bind_parameter_temps´ (fn_params f_vmx_exit_post)
(nil)
(create_undef_temps (fn_temps f_vmx_exit_post)))) H7.
Qed.
End VMXEXITPOST.
End WithPrimitives.
End VVMCSInitCode.