Library mcertikos.virt.intel.VMCSIntroGenAsm
*********************************************************************** * * * 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 Errors.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Op.
Require Import Locations.
Require Import AuxStateDataType.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Op.
Require Import Values.
Require Import Memory.
Require Import Maps.
Require Import FlatMemory.
Require Import RefinementTactic.
Require Import AuxLemma.
Require Import RealParams.
Require Import Constant.
Require Import AsmImplLemma.
Require Import AsmImplTactic.
Require Import GlobIdent.
Require Import CommonTactic.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compcertx.MakeProgram.
Require Import LAsmModuleSem.
Require Import LAsm.
Require Import liblayers.compat.CompatGenSem.
Require Import PrimSemantics.
Require Import Conventions.
Require Import VEPTInit.
Require Import VMCSIntroGenSpec.
Require Import VMCSIntroGenAsmSource.
Require Import LAsmModuleSemSpec.
Require Import LRegSet.
Require Import AbstractDataType.
Section ASM_VERIFICATION.
Local Open Scope string_scope.
Local Open Scope error_monad_scope.
Local Open Scope Z_scope.
Context `{real_params: RealParams}.
Notation LDATA := RData.
Notation LDATAOps := (cdata LDATA).
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModel}.
Context `{Hmwd: UseMemWithData mem}.
Context `{make_program_ops: !MakeProgramOps function Ctypes.type fundef unit}.
Context `{make_program_prf: !MakeProgram function Ctypes.type fundef unit}.
Lemma alloc_load_other:
∀ m0 m1 i1 i2 i3 v b1 b2 chunk,
Mem.alloc m0 i1 i2 = (m1, b1) →
Mem.load chunk m0 b2 i3 = Some v →
b1 ≠ b2.
Proof.
red; intros; subst.
exploit Mem.fresh_block_alloc; eauto.
eapply Mem.load_valid_access in H0.
eapply Mem.valid_access_valid_block; eauto.
eapply Mem.valid_access_implies; eauto.
constructor.
Qed.
Ltac accessors_simpl:=
match goal with
| |- exec_storeex _ _ _ _ _ _ _ = _ ⇒
unfold exec_storeex, LoadStoreSem3.exec_storeex3;
simpl; Lregset_simpl_tac;
match goal with
| |- context[Asm.exec_store _ _ _ _ _ _ _ ] ⇒
unfold Asm.exec_store; simpl;
Lregset_simpl_tac; lift_trivial
end
| |- exec_loadex _ _ _ _ _ _ = _ ⇒
unfold exec_loadex, LoadStoreSem3.exec_loadex3;
simpl; Lregset_simpl_tac;
match goal with
| |- context[Asm.exec_load _ _ _ _ _ _ ] ⇒
unfold Asm.exec_load; simpl;
Lregset_simpl_tac; lift_trivial
end
end.
Section VMCS_READZ.
Lemma vmcs_readz_spec:
∀ ge (s: stencil) (rs rs´: regset) b (m0: mwd LDATAOps) sig i b0 res res´,
find_symbol s vmcs_readz = Some b →
make_globalenv s (vmcs_readz ↦ vmcs_readz_function) eptinit = ret ge →
rs PC = Vptr b Int.zero →
find_symbol s VMCS_LOC = Some b0 →
vmcs_ZtoEncoding (Int.unsigned i) = Some res´ →
Mem.load Mint32 m0 b0 ((Int.unsigned i) × 4 + 8) = Some (Vint res) →
asm_invariant (mem := mwd LDATAOps) s rs m0 →
sig = mksignature (AST.Tint::nil) (Some AST.Tint) cc_default →
extcall_arguments rs m0 sig (Vint i ::nil) →
kernel_mode (snd m0) →
let rs´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR EDX :: IR ECX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) in
∃ f´ m0´ r_,
lasm_step (vmcs_readz ↦ vmcs_readz_function) (eptinit (Hmwd:= Hmwd) (Hmem:= Hmem)) vmcs_readz s rs m0 r_ m0´
∧ inject_incr (Mem.flat_inj (Mem.nextblock m0)) f´
∧ Memtype.Mem.inject f´ m0 m0´
∧ (Mem.nextblock m0 ≤ Mem.nextblock m0´)%positive
∧ (∀ l,
Val.lessdef (Pregmap.get l (rs´#PC <- (rs#RA)#EAX <- (Vint res)))
(Pregmap.get l r_)).
Proof.
intros.
destruct m0 as [m0 d].
lift_unfold.
caseEq(Mem.alloc m0 0 8).
intros m1 b1 HALC.
exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
intros Hstencil_matches.
assert (Hblock: Ple (Genv.genv_next ge) b1 ∧ Plt b1 (Mem.nextblock m1)).
{
erewrite Mem.nextblock_alloc; eauto.
apply Mem.alloc_result in HALC.
rewrite HALC. inv H5.
inv inv_inject_neutral.
inv Hstencil_matches.
rewrite stencil_matches_genv_next.
lift_unfold.
split; xomega.
}
specialize (Mem.valid_access_alloc_same _ _ _ _ _ HALC). intros HV.
assert (HV1: Mem.valid_access m1 Mint32 b1 0 Freeable).
{
eapply HV; auto; simpl; try omega.
unfold Z.divide.
∃ 0; omega.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HV1; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (rs ESP) HV1) as [m2 HST1].
assert (HV2: Mem.valid_access m2 Mint32 b1 4 Freeable).
{
eapply Mem.store_valid_access_1; eauto.
eapply HV; auto; simpl; try omega.
unfold Z.divide.
∃ 1; omega.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HV2; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (rs RA) HV2) as [m3 HST2].
assert (HV3: Mem.range_perm m3 b1 0 8 Cur Freeable).
{
unfold Mem.range_perm. intros.
repeat (eapply Mem.perm_store_1; [eassumption|]).
eapply Mem.perm_alloc_2; eauto.
}
destruct (Mem.range_perm_free _ _ _ _ HV3) as [m4 HFree].
assert(Hfun: Genv.find_funct_ptr ge b = Some (Internal vmcs_readz_function)).
{
assert (Hmodule: get_module_function vmcs_readz (vmcs_readz ↦ vmcs_readz_function) = OK (Some vmcs_readz_function)) by
reflexivity.
assert (HInternal: make_internal vmcs_readz_function = OK (AST.Internal vmcs_readz_function)) by reflexivity.
eapply make_globalenv_get_module_function in H0; eauto.
destruct H0 as [?[Hsymbol ?]].
inv Hstencil_matches.
rewrite stencil_matches_symbols in Hsymbol.
rewrite H in Hsymbol. inv Hsymbol.
assumption.
}
destruct H8 as [Hikern Hihost].
rewrite (Lregset_rewrite rs).
refine_split´; try eassumption; try reflexivity.
rewrite H1.
econstructor; eauto.
- one_step_forward´.
{
Lregset_simpl_tac.
lift_trivial.
change (Int.unsigned (Int.add Int.zero (Int.repr 0))) with 0.
change (Int.unsigned (Int.add Int.zero (Int.repr 4))) with 4.
unfold set; simpl.
rewrite HALC. simpl.
rewrite HST1. simpl.
rewrite HST2.
reflexivity.
}
Lregset_simpl_tac.
one_step_forward´.
{
accessors_simpl.
change (Int.add Int.zero (Int.repr 0)) with (Int.repr 0).
simpl in ×.
rewrite Hikern, Hihost.
inv H7. inv H8. inv H11. simpl in H10.
destruct (Val.add (rs ESP) (Vint (Int.repr 0))); try (inv H10; fail).
lift_unfold.
exploit Mem.load_alloc_other; eauto.
intros HLD.
pose proof (alloc_load_other _ _ _ _ _ _ _ _ _ HALC H10) as Hneq.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_other; eauto.
rewrite HLD.
reflexivity.
}
Lregset_simpl_tac.
one_step_forward´.
{
accessors_simpl.
Lregset_simpl_tac.
rewrite Hikern, Hihost.
unfold symbol_offset.
assert (Hsymbol: Genv.find_symbol ge VMCS_LOC = Some b0).
{
inv Hstencil_matches.
congruence.
}
rewrite Hsymbol.
rewrite Int.eq_false; [|discriminate]. simpl.
lift_unfold.
replace (Int.unsigned
(Int.add (Int.add (Int.repr 8) (Int.mul i (Int.repr 4))) Int.zero)) with
(Int.unsigned i × 4 + 8).
{
exploit Mem.load_alloc_other; eauto.
intros HLD.
pose proof (alloc_load_other _ _ _ _ _ _ _ _ _ HALC H4) as Hneq.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_other; eauto.
rewrite HLD.
reflexivity.
}
{
apply vmcs_ZtoEncoding_range in H3.
rewrite Int.add_zero.
unfold Int.add, Int.mul.
change (Int.unsigned (Int.repr 8)) with 8.
change (Int.unsigned (Int.repr 4)) with 4.
rewrite (Int.unsigned_repr (Int.unsigned i × 4)); [| rewrite_omega].
rewrite Int.unsigned_repr; rewrite_omega.
}
}
Lregset_simpl_tac.
one_step_forward´.
{
lift_trivial.
inv H5.
change (Int.unsigned (Int.add Int.zero (Int.repr 0))) with 0.
change (Int.unsigned (Int.add Int.zero (Int.repr 4))) with 4.
unfold set; simpl.
repeat(erewrite Mem.load_store_other; [|eassumption| simpl; right; right; omega]).
erewrite Mem.load_store_same; eauto 1.
erewrite register_type_load_result.
repeat(erewrite Mem.load_store_other; [|eassumption | simpl; right; right; omega]).
erewrite Mem.load_store_other; eauto 1.
erewrite Mem.load_store_same; eauto 1.
erewrite register_type_load_result.
rewrite HFree. reflexivity.
apply inv_reg_wt.
right; left. simpl. omega.
apply inv_reg_wt.
}
Lregset_simpl_tac.
one_step_forward´.
Lregset_simpl_tac.
econstructor.
reflexivity.
- inv H5. inv inv_inject_neutral.
eapply Mem.neutral_inject in inv_mem_inject_neutral.
assert (HFB: ∀ b2 delta, Mem.flat_inj (Mem.nextblock m0) b2 ≠ Some (b1, delta)).
{
intros. unfold Mem.flat_inj.
red; intros.
destruct (plt b2 (Mem.nextblock m0)). inv H5.
rewrite (Mem.alloc_result _ _ _ _ _ HALC) in p.
xomega. inv H5.
}
assert (HINJ: Mem.inject (mem:= mwd LDATAOps) (Mem.flat_inj (Mem.nextblock (mem:= mwd LDATAOps) (m0, d)))
(m0, d) (m4, d)).
{
lift_unfold.
split; trivial.
eapply Mem.free_right_inject; eauto 1; [|intros; specialize (HFB b2 delta); apply HFB; trivial].
repeat (eapply Mem.store_outside_inject; [ | | eassumption]
; [|intros b2 delta; intros; specialize (HFB b2 delta); apply HFB; trivial]).
eapply Mem.alloc_right_inject; eauto 1.
eapply inv_mem_inject_neutral.
}
assumption.
- simpl. rewrite (Mem.nextblock_free _ _ _ _ _ HFree); trivial.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST2); trivial.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST1); trivial.
rewrite (Mem.nextblock_alloc _ _ _ _ _ HALC) ; eauto.
clear. abstract xomega.
- subst rs´0. Lregset_simpl_tac.
unfold Lregset_fold; simpl.
intros reg.
repeat (rewrite Pregmap.gsspec).
simpl_destruct_reg.
exploit reg_false; try eassumption.
intros HF. inv HF.
Qed.
Lemma vmcs_readz_code_correct:
asm_spec_le (vmcs_readz ↦ vmcs_readz_spec_low)
(〚vmcs_readz ↦ vmcs_readz_function 〛 eptinit).
Proof.
eapply asm_sem_intro; try reflexivity; simpl.
intros. inv H.
eapply make_program_make_globalenv in H0.
exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
intros Hstencil_matches.
exploit vmcs_readz_spec; eauto 2.
intros (f´ & m0´ & r_ & Hstep & Hincr & Hinject & Hnb & Hv).
refine_split´; try eassumption; try reflexivity.
esplit; reflexivity.
Qed.
End VMCS_READZ.
Require Import Z64Lemma.
Section VMCS_READZ64.
Lemma vmcs_readz64_spec:
∀ ge (s: stencil) (rs rs´: regset) b (m0: mwd LDATAOps) sig i b0 res res´ v1 v2,
find_symbol s vmcs_readz64 = Some b →
make_globalenv s (vmcs_readz64 ↦ vmcs_readz64_function) eptinit = ret ge →
rs PC = Vptr b Int.zero →
find_symbol s VMCS_LOC = Some b0 →
vmcs_ZtoEncoding (Int.unsigned i) = Some res´ →
Mem.load Mint32 m0 b0 ((Int.unsigned i) × 4 + 8) = Some (Vint v1) →
Mem.load Mint32 m0 b0 ((Int.unsigned i) × 4 + 12) = Some (Vint v2) →
VZ64 (Int64.unsigned res) = VZ64 (Z64ofwords (Int.unsigned v2) (Int.unsigned v1)) →
asm_invariant (mem := mwd LDATAOps) s rs m0 →
sig = mksignature (AST.Tint::nil) (Some AST.Tlong) cc_default →
extcall_arguments rs m0 sig (Vint i ::nil) →
kernel_mode (snd m0) →
let rs´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR EDX :: IR ECX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) in
∃ f´ m0´ r_,
lasm_step (vmcs_readz64 ↦ vmcs_readz64_function) (eptinit (Hmwd:= Hmwd) (Hmem:= Hmem)) vmcs_readz64 s rs m0 r_ m0´
∧ inject_incr (Mem.flat_inj (Mem.nextblock m0)) f´
∧ Memtype.Mem.inject f´ m0 m0´
∧ (Mem.nextblock m0 ≤ Mem.nextblock m0´)%positive
∧ (∀ l,
Val.lessdef (Pregmap.get l (rs´#PC <- (rs#RA)
#EAX <- (Vint v1) #EDX <- (Vint v2)))
(Pregmap.get l r_)).
Proof.
intros.
destruct m0 as [m0 d].
lift_unfold.
caseEq(Mem.alloc m0 0 8).
intros m1 b1 HALC.
exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
intros Hstencil_matches.
assert (Hblock: Ple (Genv.genv_next ge) b1 ∧ Plt b1 (Mem.nextblock m1)).
{
erewrite Mem.nextblock_alloc; eauto.
apply Mem.alloc_result in HALC.
rewrite HALC. inv H7.
inv inv_inject_neutral.
inv Hstencil_matches.
rewrite stencil_matches_genv_next.
lift_unfold.
split; xomega.
}
specialize (Mem.valid_access_alloc_same _ _ _ _ _ HALC). intros HV.
assert (HV1: Mem.valid_access m1 Mint32 b1 0 Freeable).
{
eapply HV; auto; simpl; try omega.
unfold Z.divide.
∃ 0; omega.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HV1; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (rs ESP) HV1) as [m2 HST1].
assert (HV2: Mem.valid_access m2 Mint32 b1 4 Freeable).
{
eapply Mem.store_valid_access_1; eauto.
eapply HV; auto; simpl; try omega.
unfold Z.divide.
∃ 1; omega.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HV2; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (rs RA) HV2) as [m3 HST2].
assert (HV3: Mem.range_perm m3 b1 0 8 Cur Freeable).
{
unfold Mem.range_perm. intros.
repeat (eapply Mem.perm_store_1; [eassumption|]).
eapply Mem.perm_alloc_2; eauto.
}
destruct (Mem.range_perm_free _ _ _ _ HV3) as [m4 HFree].
assert(Hfun: Genv.find_funct_ptr ge b = Some (Internal vmcs_readz64_function)).
{
assert (Hmodule: get_module_function vmcs_readz64 (vmcs_readz64 ↦ vmcs_readz64_function) = OK (Some vmcs_readz64_function)) by
reflexivity.
assert (HInternal: make_internal vmcs_readz64_function = OK (AST.Internal vmcs_readz64_function)) by reflexivity.
eapply make_globalenv_get_module_function in H0; eauto.
destruct H0 as [?[Hsymbol ?]].
inv Hstencil_matches.
rewrite stencil_matches_symbols in Hsymbol.
rewrite H in Hsymbol. inv Hsymbol.
assumption.
}
assert (Hsymbol: Genv.find_symbol ge VMCS_LOC = Some b0).
{
inv Hstencil_matches.
congruence.
}
destruct H10 as [Hikern Hihost].
rewrite (Lregset_rewrite rs).
refine_split´; try eassumption; try reflexivity.
rewrite H1.
Local Opaque Z.shiftl.
econstructor; eauto.
- one_step_forward´.
{
Lregset_simpl_tac.
lift_trivial.
change (Int.unsigned (Int.add Int.zero (Int.repr 0))) with 0.
change (Int.unsigned (Int.add Int.zero (Int.repr 4))) with 4.
unfold set; simpl.
rewrite HALC. simpl.
rewrite HST1. simpl.
rewrite HST2.
reflexivity.
}
Lregset_simpl_tac.
one_step_forward´.
{
accessors_simpl.
change (Int.add Int.zero (Int.repr 0)) with (Int.repr 0).
simpl in ×.
rewrite Hikern, Hihost.
inv H9. inv H10. inv H13. simpl in H12.
destruct (Val.add (rs ESP) (Vint (Int.repr 0))); try (inv H12; fail).
lift_unfold.
exploit Mem.load_alloc_other; eauto.
intros HLD.
pose proof (alloc_load_other _ _ _ _ _ _ _ _ _ HALC H12) as Hneq.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_other; eauto.
rewrite HLD.
reflexivity.
}
Lregset_simpl_tac.
one_step_forward´.
{
accessors_simpl.
Lregset_simpl_tac.
rewrite Hikern, Hihost.
unfold symbol_offset.
rewrite Hsymbol.
rewrite Int.eq_false; [|discriminate]. simpl.
replace (Int.unsigned
(Int.add (Int.add (Int.repr 8) (Int.mul i (Int.repr 4))) Int.zero)) with
(Int.unsigned i × 4 + 8).
lift_trivial.
{
clear H5.
exploit Mem.load_alloc_other; eauto.
intros HLD.
pose proof (alloc_load_other _ _ _ _ _ _ _ _ _ HALC H4) as Hneq.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_other; eauto.
rewrite HLD.
reflexivity.
}
{
apply vmcs_ZtoEncoding_range in H3.
rewrite Int.add_zero.
unfold Int.add, Int.mul.
change (Int.unsigned (Int.repr 8)) with 8.
change (Int.unsigned (Int.repr 4)) with 4.
rewrite (Int.unsigned_repr (Int.unsigned i × 4)); [| rewrite_omega].
rewrite Int.unsigned_repr; rewrite_omega.
}
}
Lregset_simpl_tac.
one_step_forward´.
Lregset_simpl_tac.
one_step_forward´.
{
accessors_simpl.
Lregset_simpl_tac.
rewrite Hikern, Hihost.
unfold symbol_offset.
rewrite Hsymbol.
rewrite Int.eq_false; [|discriminate]. simpl.
replace (Int.unsigned
(Int.add
(Int.add (Int.repr 8)
(Int.mul (Int.add i (Int.add Int.zero Int.one))
(Int.repr 4))) Int.zero)) with
(Int.unsigned i × 4 + 12).
lift_trivial.
{
exploit Mem.load_alloc_other; eauto.
intros HLD.
pose proof (alloc_load_other _ _ _ _ _ _ _ _ _ HALC H4) as Hneq.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_other; eauto.
rewrite HLD.
reflexivity.
}
{
apply vmcs_ZtoEncoding_range in H3.
rewrite Int.add_zero.
change (Int.add Int.zero Int.one) with Int.one.
unfold Int.add, Int.mul.
change (Int.unsigned (Int.repr 8)) with 8.
change (Int.unsigned (Int.repr 4)) with 4.
change (Int.unsigned Int.one) with 1.
rewrite (Int.unsigned_repr (Int.unsigned i + 1)); [| rewrite_omega].
rewrite (Int.unsigned_repr ((Int.unsigned i + 1) × 4)); [| rewrite_omega].
rewrite (Int.unsigned_repr (8 + (Int.unsigned i + 1) × 4)); [| rewrite_omega].
omega.
}
}
Lregset_simpl_tac.
one_step_forward´.
{
lift_trivial.
inv H7.
change (Int.unsigned (Int.add Int.zero (Int.repr 0))) with 0.
change (Int.unsigned (Int.add Int.zero (Int.repr 4))) with 4.
unfold set; simpl.
repeat(erewrite Mem.load_store_other; [|eassumption| simpl; right; right; omega]).
erewrite Mem.load_store_same; eauto 1.
erewrite register_type_load_result.
repeat(erewrite Mem.load_store_other; [|eassumption | simpl; right; right; omega]).
erewrite Mem.load_store_other; eauto 1.
erewrite Mem.load_store_same; eauto 1.
erewrite register_type_load_result.
rewrite HFree. reflexivity.
apply inv_reg_wt.
right; left. simpl. omega.
apply inv_reg_wt.
}
Lregset_simpl_tac.
one_step_forward´.
Lregset_simpl_tac.
econstructor.
reflexivity.
- inv H7. inv inv_inject_neutral.
eapply Mem.neutral_inject in inv_mem_inject_neutral.
assert (HFB: ∀ b2 delta, Mem.flat_inj (Mem.nextblock m0) b2 ≠ Some (b1, delta)).
{
intros. unfold Mem.flat_inj.
red; intros.
destruct (plt b2 (Mem.nextblock m0)). inv H7.
rewrite (Mem.alloc_result _ _ _ _ _ HALC) in p.
xomega. inv H7.
}
assert (HINJ: Mem.inject (mem:= mwd LDATAOps) (Mem.flat_inj (Mem.nextblock (mem:= mwd LDATAOps) (m0, d)))
(m0, d) (m4, d)).
{
lift_unfold.
split; trivial.
eapply Mem.free_right_inject; eauto 1; [|intros; specialize (HFB b2 delta); apply HFB; trivial].
repeat (eapply Mem.store_outside_inject; [ | | eassumption]
; [|intros b2 delta; intros; specialize (HFB b2 delta); apply HFB; trivial]).
eapply Mem.alloc_right_inject; eauto 1.
eapply inv_mem_inject_neutral.
}
assumption.
- simpl. rewrite (Mem.nextblock_free _ _ _ _ _ HFree); trivial.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST2); trivial.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST1); trivial.
rewrite (Mem.nextblock_alloc _ _ _ _ _ HALC) ; eauto.
clear. abstract xomega.
- subst rs´0. Lregset_simpl_tac.
unfold Lregset_fold; simpl.
intros reg.
repeat (rewrite Pregmap.gsspec).
simpl_destruct_reg.
exploit reg_false; try eassumption.
intros HF. inv HF.
Qed.
Lemma vmcs_readz64_code_correct:
asm_spec_le (vmcs_readz64 ↦ vmcs_readz64_spec_low)
(〚vmcs_readz64 ↦ vmcs_readz64_function 〛 eptinit).
Proof.
eapply asm_sem_intro; try reflexivity; simpl.
intros. inv H.
eapply make_program_make_globalenv in H0.
exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
intros Hstencil_matches.
exploit vmcs_readz64_spec; eauto 2.
intros (f´ & m0´ & r_ & Hstep & Hincr & Hinject & Hnb & Hv).
refine_split´; try eassumption; try reflexivity.
esplit; reflexivity.
Qed.
End VMCS_READZ64.
Lemma alloc_store_other:
∀ m0 m1 i1 i2 i3 v v´ b1 b2 chunk,
Mem.alloc m0 i1 i2 = (m1, b1) →
Mem.store chunk m0 b2 i3 v = Some v´ →
b1 ≠ b2.
Proof.
red; intros; subst.
exploit Mem.fresh_block_alloc; eauto.
eapply Mem.store_valid_access_3 in H0.
eapply Mem.valid_access_valid_block; eauto.
eapply Mem.valid_access_implies; eauto.
constructor.
Qed.
Section VMCS_WRITEZ.
Lemma vmcs_writez_spec:
∀ ge (s: stencil) (rs rs´: regset) b (m0 m´0: mwd LDATAOps) sig i b0 res´ v,
find_symbol s vmcs_writez = Some b →
make_globalenv s (vmcs_writez ↦ vmcs_writez_function) eptinit = ret ge →
rs PC = Vptr b Int.zero →
find_symbol s VMCS_LOC = Some b0 →
vmcs_ZtoEncoding (Int.unsigned i) = Some res´ →
Mem.store Mint32 m0 b0 ((Int.unsigned i) × 4 + 8) (Vint v) = Some m´0 →
asm_invariant (mem := mwd LDATAOps) s rs m0 →
sig = mksignature (AST.Tint::AST.Tint::nil) None cc_default →
extcall_arguments rs m0 sig (Vint i :: Vint v :: nil) →
kernel_mode (snd m0) →
let rs´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR EDX :: IR EAX :: IR ECX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) in
∃ f´ m0´ r_,
lasm_step (vmcs_writez ↦ vmcs_writez_function) (eptinit (Hmwd:= Hmwd) (Hmem:= Hmem)) vmcs_writez s rs m0 r_ m0´
∧ inject_incr (Mem.flat_inj (Mem.nextblock m0)) f´
∧ Memtype.Mem.inject f´ m´0 m0´
∧ (Mem.nextblock m0 ≤ Mem.nextblock m0´)%positive
∧ (∀ l,
Val.lessdef (Pregmap.get l (rs´#PC <- (rs#RA)))
(Pregmap.get l r_)).
Proof.
intros.
destruct m0 as [m0 d]. destruct m´0 as [m´0 ?].
lift_unfold. destruct H4 as [H4 Heq]. inv Heq.
caseEq(Mem.alloc m0 0 8).
intros m1 b1 HALC.
exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
intros Hstencil_matches.
assert (Hblock: Ple (Genv.genv_next ge) b1 ∧ Plt b1 (Mem.nextblock m1)).
{
erewrite Mem.nextblock_alloc; eauto.
apply Mem.alloc_result in HALC.
rewrite HALC. inv H5.
inv inv_inject_neutral.
inv Hstencil_matches.
rewrite stencil_matches_genv_next.
lift_unfold.
split; xomega.
}
specialize (alloc_store_other _ _ _ _ _ _ _ _ _ _ HALC H4). intros Hneq.
specialize (Mem.valid_access_alloc_same _ _ _ _ _ HALC). intros HV.
assert (HV1: Mem.valid_access m1 Mint32 b1 0 Freeable).
{
eapply HV; auto; simpl; try omega.
unfold Z.divide.
∃ 0; omega.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HV1; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (rs ESP) HV1) as [m2 HST1].
assert (HV2: Mem.valid_access m2 Mint32 b1 4 Freeable).
{
eapply Mem.store_valid_access_1; eauto.
eapply HV; auto; simpl; try omega.
unfold Z.divide.
∃ 1; omega.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HV2; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (rs RA) HV2) as [m3 HST2].
assert (HV3: Mem.valid_access m3 Mint32 b0 (Int.unsigned i × 4 + 8) Writable).
{
eapply Mem.store_valid_access_1; eauto.
eapply Mem.store_valid_access_1; eauto.
eapply Mem.valid_access_alloc_other; eauto.
eapply Mem.store_valid_access_3; eauto.
}
destruct (Mem.valid_access_store _ _ _ _ (Vint v) HV3) as [m4 HST3].
assert (HV4: Mem.range_perm m4 b1 0 8 Cur Freeable).
{
unfold Mem.range_perm. intros.
repeat (eapply Mem.perm_store_1; [eassumption|]).
eapply Mem.perm_alloc_2; eauto.
}
destruct (Mem.range_perm_free _ _ _ _ HV4) as [m5 HFree].
assert(Hfun: Genv.find_funct_ptr ge b = Some (Internal vmcs_writez_function)).
{
assert (Hmodule: get_module_function vmcs_writez (vmcs_writez ↦ vmcs_writez_function) = OK (Some vmcs_writez_function)) by
reflexivity.
assert (HInternal: make_internal vmcs_writez_function = OK (AST.Internal vmcs_writez_function)) by reflexivity.
eapply make_globalenv_get_module_function in H0; eauto.
destruct H0 as [?[Hsymbol ?]].
inv Hstencil_matches.
rewrite stencil_matches_symbols in Hsymbol.
rewrite H in Hsymbol. inv Hsymbol.
assumption.
}
destruct H8 as [Hikern Hihost].
rewrite (Lregset_rewrite rs).
refine_split´; try eassumption; try reflexivity.
rewrite H1.
lift_unfold; store_split.
inv H7. inv H12. inv H9. inv H10.
simpl in ×.
econstructor; eauto.
- one_step_forward´.
{
Lregset_simpl_tac.
lift_trivial.
change (Int.unsigned (Int.add Int.zero (Int.repr 0))) with 0.
change (Int.unsigned (Int.add Int.zero (Int.repr 4))) with 4.
unfold set; simpl.
rewrite HALC. simpl.
rewrite HST1. simpl.
rewrite HST2.
reflexivity.
}
Lregset_simpl_tac.
one_step_forward´.
{
accessors_simpl.
change (Int.add Int.zero (Int.repr 0)) with (Int.repr 0).
simpl in ×.
rewrite Hikern, Hihost.
destruct (Val.add (rs ESP) (Vint (Int.repr 0))); try (inv H11; fail).
lift_unfold.
exploit Mem.load_alloc_other; eauto.
intros HLD.
pose proof (alloc_load_other _ _ _ _ _ _ _ _ _ HALC H11) as Hneq´.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_other; eauto.
rewrite HLD.
reflexivity.
}
Lregset_simpl_tac.
one_step_forward´.
{
accessors_simpl.
change (Int.add Int.zero (Int.repr 4)) with (Int.repr 4).
simpl in ×.
rewrite Hikern, Hihost.
destruct (Val.add (rs ESP) (Vint (Int.repr 4))); try (inv H12; fail).
lift_unfold.
exploit Mem.load_alloc_other; eauto.
intros HLD.
pose proof (alloc_load_other _ _ _ _ _ _ _ _ _ HALC H12) as Hneq´.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_other; eauto.
rewrite HLD.
reflexivity.
}
Lregset_simpl_tac.
one_step_forward´.
{
accessors_simpl.
Lregset_simpl_tac.
rewrite Hikern, Hihost.
unfold symbol_offset.
assert (Hsymbol: Genv.find_symbol ge VMCS_LOC = Some b0).
{
inv Hstencil_matches.
congruence.
}
rewrite Hsymbol.
rewrite Int.eq_false; [|discriminate]. simpl.
replace (Int.unsigned
(Int.add (Int.add (Int.repr 8) (Int.mul i (Int.repr 4))) Int.zero)) with
(Int.unsigned i × 4 + 8).
lift_trivial.
{
rewrite HST3.
reflexivity.
}
{
apply vmcs_ZtoEncoding_range in H3.
rewrite Int.add_zero.
unfold Int.add, Int.mul.
change (Int.unsigned (Int.repr 8)) with 8.
change (Int.unsigned (Int.repr 4)) with 4.
rewrite (Int.unsigned_repr (Int.unsigned i × 4)); [| rewrite_omega].
rewrite Int.unsigned_repr; rewrite_omega.
}
}
Lregset_simpl_tac.
one_step_forward´.
{
lift_trivial.
inv H5.
change (Int.unsigned (Int.add Int.zero (Int.repr 0))) with 0.
change (Int.unsigned (Int.add Int.zero (Int.repr 4))) with 4.
unfold set; simpl.
erewrite Mem.load_store_other; [|eassumption| eauto].
repeat(erewrite Mem.load_store_other; [|eassumption| simpl; right; right; omega]).
erewrite Mem.load_store_same; eauto 1.
erewrite register_type_load_result.
erewrite Mem.load_store_other; [|eassumption| eauto].
repeat(erewrite Mem.load_store_other; [|eassumption | simpl; right; right; omega]).
erewrite Mem.load_store_other; eauto 1.
erewrite Mem.load_store_same; eauto 1.
erewrite register_type_load_result.
rewrite HFree. reflexivity.
apply inv_reg_wt.
right; left. simpl. omega.
apply inv_reg_wt.
}
Lregset_simpl_tac.
one_step_forward´.
Lregset_simpl_tac.
econstructor.
reflexivity.
- inv H5. inv inv_inject_neutral.
eapply Mem.neutral_inject in inv_mem_inject_neutral.
assert (HFB: ∀ b2 delta, Mem.flat_inj (Mem.nextblock m0) b2 ≠ Some (b1, delta)).
{
intros. unfold Mem.flat_inj.
red; intros.
destruct (plt b2 (Mem.nextblock m0)). inv H5.
rewrite (Mem.alloc_result _ _ _ _ _ HALC) in p.
xomega. inv H5.
}
assert (HINJ: Mem.inject (mem:= mwd LDATAOps) (Mem.flat_inj (Mem.nextblock (mem:= mwd LDATAOps) (m0, l)))
(m´0, l) (m5, l)).
{
lift_unfold.
split; trivial.
eapply Mem.free_right_inject; eauto 1; [|intros; specialize (HFB b2 delta); apply HFB; trivial].
assert (HINJ: Mem.inject (Mem.flat_inj (Mem.nextblock m0)) m0 m3).
{
repeat (eapply Mem.store_outside_inject; [ | | eassumption]
; [|intros b2 delta; intros; specialize (HFB b2 delta); apply HFB; trivial]).
eapply Mem.alloc_right_inject; eauto 1.
eapply inv_mem_inject_neutral.
}
exploit Mem.store_mapped_inject; eauto.
{
eapply stencil_find_symbol_inject´; eauto.
eapply flat_inj_inject_incr.
xomega.
}
rewrite Z.add_0_r.
rewrite HST3.
intros (m´ & Heq & Hinj). inv Heq.
assumption.
}
assumption.
- simpl. rewrite (Mem.nextblock_free _ _ _ _ _ HFree); trivial.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST3); trivial.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST2); trivial.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST1); trivial.
rewrite (Mem.nextblock_alloc _ _ _ _ _ HALC) ; eauto.
clear. abstract xomega.
- subst rs´0. Lregset_simpl_tac.
unfold Lregset_fold; simpl.
intros reg.
repeat (rewrite Pregmap.gsspec).
simpl_destruct_reg.
exploit reg_false; try eassumption.
intros HF. inv HF.
Qed.
Lemma vmcs_writez_code_correct:
asm_spec_le (vmcs_writez ↦ vmcs_writez_spec_low)
(〚vmcs_writez ↦ vmcs_writez_function 〛 eptinit).
Proof.
eapply asm_sem_intro; try reflexivity; simpl.
intros. inv H.
eapply make_program_make_globalenv in H0.
exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
intros Hstencil_matches.
exploit vmcs_writez_spec; eauto 2.
intros (f´ & m0´ & r_ & Hstep & Hincr & HINJ & Hle & Hreg).
assert (Heq: (Mem.nextblock m = Mem.nextblock m´)%positive)
by link_nextblock_asm.
assert (Hle´: (Mem.nextblock m ≤ Mem.nextblock m´)%positive).
{
rewrite Heq; reflexivity.
}
refine_split´; try eassumption.
- lift_unfold. rewrite <- Heq. eassumption.
- lift_unfold. destruct HINJ as (HINJ & Heq´). inv Heq´.
split; trivial.
- lift_unfold. rewrite <- Heq. assumption.
- esplit; reflexivity.
Qed.
End VMCS_WRITEZ.
Section VMCS_WRITE_IDENT.
Lemma vmcs_write_ident_spec:
∀ ge (s: stencil) (rs rs´: regset) b (m0 m´0: mwd LDATAOps) sig i b0 res´ ba ofsa,
find_symbol s vmcs_write_ident = Some b →
make_globalenv s (vmcs_write_ident ↦ vmcs_write_ident_function) eptinit = ret ge →
rs PC = Vptr b Int.zero →
find_symbol s VMCS_LOC = Some b0 →
vmcs_ZtoEncoding (Int.unsigned i) = Some res´ →
Mem.store Mint32 m0 b0 ((Int.unsigned i) × 4 + 8) (Vptr ba ofsa) = Some m´0 →
asm_invariant (mem := mwd LDATAOps) s rs m0 →
sig = mksignature (AST.Tint::AST.Tint::nil) None cc_default →
extcall_arguments rs m0 sig (Vint i :: Vptr ba ofsa :: nil) →
kernel_mode (snd m0) →
(∃ ident, find_symbol s ident = Some ba) →
let rs´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR EDX :: IR EAX :: IR ECX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) in
∃ f´ m0´ r_,
lasm_step (vmcs_write_ident ↦ vmcs_write_ident_function) (eptinit (Hmwd:= Hmwd) (Hmem:= Hmem))
vmcs_write_ident s rs m0 r_ m0´
∧ inject_incr (Mem.flat_inj (Mem.nextblock m0)) f´
∧ Memtype.Mem.inject f´ m´0 m0´
∧ (Mem.nextblock m0 ≤ Mem.nextblock m0´)%positive
∧ (∀ l,
Val.lessdef (Pregmap.get l (rs´#PC <- (rs#RA)))
(Pregmap.get l r_)).
Proof.
intros. rename H9 into Hident.
destruct m0 as [m0 d]. destruct m´0 as [m´0 ?].
lift_unfold. destruct H4 as [H4 Heq]. inv Heq.
caseEq(Mem.alloc m0 0 8).
intros m1 b1 HALC.
exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
intros Hstencil_matches.
assert (Hblock: Ple (Genv.genv_next ge) b1 ∧ Plt b1 (Mem.nextblock m1)).
{
erewrite Mem.nextblock_alloc; eauto.
apply Mem.alloc_result in HALC.
rewrite HALC. inv H5.
inv inv_inject_neutral.
inv Hstencil_matches.
rewrite stencil_matches_genv_next.
lift_unfold.
split; xomega.
}
specialize (alloc_store_other _ _ _ _ _ _ _ _ _ _ HALC H4). intros Hneq.
specialize (Mem.valid_access_alloc_same _ _ _ _ _ HALC). intros HV.
assert (HV1: Mem.valid_access m1 Mint32 b1 0 Freeable).
{
eapply HV; auto; simpl; try omega.
unfold Z.divide.
∃ 0; omega.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HV1; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (rs ESP) HV1) as [m2 HST1].
assert (HV2: Mem.valid_access m2 Mint32 b1 4 Freeable).
{
eapply Mem.store_valid_access_1; eauto.
eapply HV; auto; simpl; try omega.
unfold Z.divide.
∃ 1; omega.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HV2; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (rs RA) HV2) as [m3 HST2].
assert (HV3: Mem.valid_access m3 Mint32 b0 (Int.unsigned i × 4 + 8) Writable).
{
eapply Mem.store_valid_access_1; eauto.
eapply Mem.store_valid_access_1; eauto.
eapply Mem.valid_access_alloc_other; eauto.
eapply Mem.store_valid_access_3; eauto.
}
destruct (Mem.valid_access_store _ _ _ _ (Vptr ba ofsa) HV3) as [m4 HST3].
assert (HV4: Mem.range_perm m4 b1 0 8 Cur Freeable).
{
unfold Mem.range_perm. intros.
repeat (eapply Mem.perm_store_1; [eassumption|]).
eapply Mem.perm_alloc_2; eauto.
}
destruct (Mem.range_perm_free _ _ _ _ HV4) as [m5 HFree].
assert(Hfun: Genv.find_funct_ptr ge b = Some (Internal vmcs_write_ident_function)).
{
assert (Hmodule: get_module_function vmcs_write_ident (vmcs_write_ident ↦ vmcs_write_ident_function)
= OK (Some vmcs_write_ident_function)) by
reflexivity.
assert (HInternal: make_internal vmcs_write_ident_function = OK (AST.Internal vmcs_write_ident_function)) by reflexivity.
eapply make_globalenv_get_module_function in H0; eauto.
destruct H0 as [?[Hsymbol ?]].
inv Hstencil_matches.
rewrite stencil_matches_symbols in Hsymbol.
rewrite H in Hsymbol. inv Hsymbol.
assumption.
}
destruct H8 as [Hikern Hihost].
rewrite (Lregset_rewrite rs).
refine_split´; try eassumption; try reflexivity.
rewrite H1.
inv H5. inv H7. inv H11. inv H12.
inv H8. inv H9.
simpl in ×.
econstructor; eauto.
- one_step_forward´.
{
Lregset_simpl_tac.
lift_trivial.
change (Int.unsigned (Int.add Int.zero (Int.repr 0))) with 0.
change (Int.unsigned (Int.add Int.zero (Int.repr 4))) with 4.
unfold set; simpl.
rewrite HALC. simpl.
rewrite HST1. simpl.
rewrite HST2.
reflexivity.
}
Lregset_simpl_tac.
one_step_forward´.
{
accessors_simpl.
change (Int.add Int.zero (Int.repr 0)) with (Int.repr 0).
simpl in ×.
rewrite Hikern, Hihost.
destruct (Val.add (rs ESP) (Vint (Int.repr 0))); try (inv H10; fail).
lift_unfold.
exploit Mem.load_alloc_other; eauto.
intros HLD.
pose proof (alloc_load_other _ _ _ _ _ _ _ _ _ HALC H10) as Hneq´.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_other; eauto.
rewrite HLD.
reflexivity.
}
Lregset_simpl_tac.
one_step_forward´.
{
accessors_simpl.
change (Int.add Int.zero (Int.repr 4)) with (Int.repr 4).
simpl in ×.
rewrite Hikern, Hihost.
destruct (Val.add (rs ESP) (Vint (Int.repr 4))); try (inv H11; fail).
lift_unfold.
exploit Mem.load_alloc_other; eauto.
intros HLD.
pose proof (alloc_load_other _ _ _ _ _ _ _ _ _ HALC H11) as Hneq´.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_other; eauto.
rewrite HLD.
reflexivity.
}
Lregset_simpl_tac.
one_step_forward´.
{
accessors_simpl.
Lregset_simpl_tac.
rewrite Hikern, Hihost.
unfold symbol_offset.
assert (Hsymbol: Genv.find_symbol ge VMCS_LOC = Some b0).
{
inv Hstencil_matches.
congruence.
}
rewrite Hsymbol.
rewrite Int.eq_false; [|discriminate]. simpl.
replace (Int.unsigned
(Int.add (Int.add (Int.repr 8) (Int.mul i (Int.repr 4))) Int.zero)) with
(Int.unsigned i × 4 + 8).
lift_trivial.
{
rewrite HST3.
reflexivity.
}
{
apply vmcs_ZtoEncoding_range in H3.
rewrite Int.add_zero.
unfold Int.add, Int.mul.
change (Int.unsigned (Int.repr 8)) with 8.
change (Int.unsigned (Int.repr 4)) with 4.
rewrite (Int.unsigned_repr (Int.unsigned i × 4)); [| rewrite_omega].
rewrite Int.unsigned_repr; rewrite_omega.
}
}
Lregset_simpl_tac.
one_step_forward´.
{
lift_trivial.
change (Int.unsigned (Int.add Int.zero (Int.repr 0))) with 0.
change (Int.unsigned (Int.add Int.zero (Int.repr 4))) with 4.
unfold set; simpl.
erewrite Mem.load_store_other; [|eassumption| eauto].
repeat(erewrite Mem.load_store_other; [|eassumption| simpl; right; right; omega]).
erewrite Mem.load_store_same; eauto 1.
erewrite register_type_load_result.
erewrite Mem.load_store_other; [|eassumption| eauto].
repeat(erewrite Mem.load_store_other; [|eassumption | simpl; right; right; omega]).
erewrite Mem.load_store_other; eauto 1.
erewrite Mem.load_store_same; eauto 1.
erewrite register_type_load_result.
rewrite HFree. reflexivity.
apply inv_reg_wt.
right; left. simpl. omega.
apply inv_reg_wt.
}
Lregset_simpl_tac.
one_step_forward´.
Lregset_simpl_tac.
econstructor.
reflexivity.
- inv H5. inv inv_inject_neutral.
eapply Mem.neutral_inject in inv_mem_inject_neutral.
assert (HFB: ∀ b2 delta, Mem.flat_inj (Mem.nextblock m0) b2 ≠ Some (b1, delta)).
{
intros. unfold Mem.flat_inj.
red; intros.
destruct (plt b2 (Mem.nextblock m0)). inv H5.
rewrite (Mem.alloc_result _ _ _ _ _ HALC) in p.
xomega. inv H5.
}
assert (HINJ: Mem.inject (mem:= mwd LDATAOps) (Mem.flat_inj (Mem.nextblock (mem:= mwd LDATAOps) (m0, l)))
(m´0, l) (m5, l)).
{
lift_unfold.
split; trivial.
eapply Mem.free_right_inject; eauto 1; [|intros; specialize (HFB b2 delta); apply HFB; trivial].
assert (HINJ: Mem.inject (Mem.flat_inj (Mem.nextblock m0)) m0 m3).
{
repeat (eapply Mem.store_outside_inject; [ | | eassumption]
; [|intros b2 delta; intros; specialize (HFB b2 delta); apply HFB; trivial]).
eapply Mem.alloc_right_inject; eauto 1.
eapply inv_mem_inject_neutral.
}
exploit Mem.store_mapped_inject; eauto.
{
eapply stencil_find_symbol_inject´; eauto.
eapply flat_inj_inject_incr.
xomega.
}
{
instantiate (1:= (Vptr ba ofsa)).
econstructor; eauto.
destruct Hident as (ident & Hident).
eapply stencil_find_symbol_inject´; eauto.
eapply flat_inj_inject_incr.
xomega.
rewrite Int.add_zero. trivial.
}
rewrite Z.add_0_r.
rewrite HST3.
intros (m´ & Heq & Hinj). inv Heq.
assumption.
}
assumption.
- simpl. rewrite (Mem.nextblock_free _ _ _ _ _ HFree); trivial.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST3); trivial.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST2); trivial.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST1); trivial.
rewrite (Mem.nextblock_alloc _ _ _ _ _ HALC) ; eauto.
clear. abstract xomega.
- subst rs´0. Lregset_simpl_tac.
unfold Lregset_fold; simpl.
intros reg.
repeat (rewrite Pregmap.gsspec).
simpl_destruct_reg.
exploit reg_false; try eassumption.
intros HF. inv HF.
Qed.
Lemma vmcs_write_ident_code_correct:
asm_spec_le (vmcs_write_ident ↦ vmcs_write_ident_spec_low)
(〚vmcs_write_ident ↦ vmcs_write_ident_function 〛 eptinit).
Proof.
eapply asm_sem_intro; try reflexivity; simpl.
intros. inv H.
eapply make_program_make_globalenv in H0.
exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
intros Hstencil_matches.
exploit vmcs_write_ident_spec; eauto 2.
intros (f´ & m0´ & r_ & Hstep & Hincr & HINJ & Hle´ & Hreg).
assert (Heq: (Mem.nextblock m = Mem.nextblock m´)%positive)
by link_nextblock_asm.
assert (Hle: (Mem.nextblock m ≤ Mem.nextblock m´)%positive).
{
rewrite Heq; reflexivity.
}
refine_split´; try eassumption.
- lift_unfold. rewrite <- Heq. eassumption.
- lift_unfold. destruct HINJ as (HINJ & Heq´). inv Heq´.
split; trivial.
- lift_unfold. rewrite <- Heq. assumption.
- esplit; reflexivity.
Qed.
End VMCS_WRITE_IDENT.
Section VMCS_WRITEZ64.
Lemma vmcs_writez64_spec:
∀ ge (s: stencil) (rs rs´: regset) b (m0 m´0 m´1: mwd LDATAOps) sig i b0 res´ v1 v2,
find_symbol s vmcs_writez64 = Some b →
make_globalenv s (vmcs_writez64 ↦ vmcs_writez64_function) eptinit = ret ge →
rs PC = Vptr b Int.zero →
find_symbol s VMCS_LOC = Some b0 →
vmcs_ZtoEncoding (Int.unsigned i) = Some res´ →
Mem.store Mint32 m0 b0 ((Int.unsigned i) × 4 + 8) (Vint v1) = Some m´0 →
Mem.store Mint32 m´0 b0 ((Int.unsigned i) × 4 + 12) (Vint v2) = Some m´1 →
asm_invariant (mem := mwd LDATAOps) s rs m0 →
sig = mksignature (AST.Tint::AST.Tlong::nil) None cc_default →
extcall_arguments rs m0 sig (Vint i :: Vint v2 :: Vint v1 :: nil) →
kernel_mode (snd m0) →
let rs´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR EAX :: IR ECX :: IR EDX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) in
∃ f´ m0´ r_,
lasm_step (vmcs_writez64 ↦ vmcs_writez64_function) (eptinit (Hmwd:= Hmwd) (Hmem:= Hmem)) vmcs_writez64 s rs m0 r_ m0´
∧ inject_incr (Mem.flat_inj (Mem.nextblock m0)) f´
∧ Memtype.Mem.inject f´ m´1 m0´
∧ (Mem.nextblock m0 ≤ Mem.nextblock m0´)%positive
∧ (∀ l,
Val.lessdef (Pregmap.get l (rs´#PC <- (rs#RA)))
(Pregmap.get l r_)).
Proof.
intros.
destruct H9 as [Hikern Hihost].
destruct m0 as [m0 d].
destruct m´0 as [m´0 ?].
destruct m´1 as [m´1 ?].
lift_unfold; store_split.
caseEq(Mem.alloc m0 0 8).
intros m1 b1 HALC.
exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
intros Hstencil_matches.
assert (Hblock: Ple (Genv.genv_next ge) b1 ∧ Plt b1 (Mem.nextblock m1)).
{
erewrite Mem.nextblock_alloc; eauto.
apply Mem.alloc_result in HALC.
rewrite HALC. inv H6.
inv inv_inject_neutral.
inv Hstencil_matches.
rewrite stencil_matches_genv_next.
lift_unfold.
split; xomega.
}
specialize (alloc_store_other _ _ _ _ _ _ _ _ _ _ HALC H4). intros Hneq.
specialize (Mem.valid_access_alloc_same _ _ _ _ _ HALC). intros HV.
assert (HV1: Mem.valid_access m1 Mint32 b1 0 Freeable).
{
eapply HV; auto; simpl; try omega.
unfold Z.divide.
∃ 0; omega.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HV1; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (rs ESP) HV1) as [m2 HST1].
assert (HV2: Mem.valid_access m2 Mint32 b1 4 Freeable).
{
eapply Mem.store_valid_access_1; eauto.
eapply HV; auto; simpl; try omega.
unfold Z.divide.
∃ 1; omega.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HV2; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (rs RA) HV2) as [m3 HST2].
assert (HV3: Mem.valid_access m3 Mint32 b0 (Int.unsigned i × 4 + 8) Writable).
{
eapply Mem.store_valid_access_1; eauto.
eapply Mem.store_valid_access_1; eauto.
eapply Mem.valid_access_alloc_other; eauto.
eapply Mem.store_valid_access_3; eauto.
}
destruct (Mem.valid_access_store _ _ _ _ (Vint v1) HV3) as [m4 HST3].
assert (HV4: Mem.valid_access m4 Mint32 b0 (Int.unsigned i × 4 + 12) Writable).
{
eapply Mem.store_valid_access_1; eauto.
eapply Mem.store_valid_access_1; eauto.
eapply Mem.store_valid_access_1; eauto.
eapply Mem.valid_access_alloc_other; eauto.
eapply Mem.store_valid_access_2; eauto.
eapply Mem.store_valid_access_3; eauto.
}
destruct (Mem.valid_access_store _ _ _ _ (Vint v2) HV4) as [m5 HST4].
assert (HV5: Mem.range_perm m5 b1 0 8 Cur Freeable).
{
unfold Mem.range_perm. intros.
repeat (eapply Mem.perm_store_1; [eassumption|]).
eapply Mem.perm_alloc_2; eauto.
}
destruct (Mem.range_perm_free _ _ _ _ HV5) as [m6 HFree].
assert(Hfun: Genv.find_funct_ptr ge b = Some (Internal vmcs_writez64_function)).
{
assert (Hmodule: get_module_function vmcs_writez64 (vmcs_writez64 ↦ vmcs_writez64_function) = OK (Some vmcs_writez64_function)) by
reflexivity.
assert (HInternal: make_internal vmcs_writez64_function = OK (AST.Internal vmcs_writez64_function)) by reflexivity.
eapply make_globalenv_get_module_function in H0; eauto.
destruct H0 as [?[Hsymbol ?]].
inv Hstencil_matches.
rewrite stencil_matches_symbols in Hsymbol.
rewrite H in Hsymbol. inv Hsymbol.
assumption.
}
assert (Hsymbol: Genv.find_symbol ge VMCS_LOC = Some b0).
{
inv Hstencil_matches.
congruence.
}
rewrite (Lregset_rewrite rs).
refine_split´; try eassumption; try reflexivity.
rewrite H1.
inv H8. inv H13. inv H14. inv H11.
inv H12. inv H10.
simpl in ×.
econstructor; eauto.
- one_step_forward´.
{
Lregset_simpl_tac.
lift_trivial.
change (Int.unsigned (Int.add Int.zero (Int.repr 0))) with 0.
change (Int.unsigned (Int.add Int.zero (Int.repr 4))) with 4.
unfold set; simpl.
rewrite HALC. simpl.
rewrite HST1. simpl.
rewrite HST2.
reflexivity.
}
Lregset_simpl_tac.
one_step_forward´.
{
accessors_simpl.
change (Int.add Int.zero (Int.repr 0)) with (Int.repr 0).
simpl in ×.
rewrite Hikern, Hihost.
destruct (Val.add (rs ESP) (Vint (Int.repr 0))); try (inv H14; fail).
lift_unfold.
exploit Mem.load_alloc_other; eauto.
intros HLD.
pose proof (alloc_load_other _ _ _ _ _ _ _ _ _ HALC H14) as Hneq´.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_other; eauto.
rewrite HLD.
reflexivity.
}
Lregset_simpl_tac.
one_step_forward´.
{
accessors_simpl.
change (Int.add Int.zero (Int.repr 4)) with (Int.repr 4).
simpl in ×.
rewrite Hikern, Hihost.
destruct (Val.add (rs ESP) (Vint (Int.repr 4))); try (inv H13; fail).
lift_unfold.
exploit Mem.load_alloc_other; eauto.
intros HLD.
pose proof (alloc_load_other _ _ _ _ _ _ _ _ _ HALC H13) as Hneq´.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_other; eauto.
rewrite HLD.
reflexivity.
}
Lregset_simpl_tac.
one_step_forward´.
{
accessors_simpl.
change (Int.add Int.zero (Int.repr 8)) with (Int.repr 8).
simpl in ×.
rewrite Hikern, Hihost.
destruct (Val.add (rs ESP) (Vint (Int.repr 8))); try (inv H12; fail).
lift_unfold.
exploit Mem.load_alloc_other; eauto.
intros HLD.
pose proof (alloc_load_other _ _ _ _ _ _ _ _ _ HALC H12) as Hneq´.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_other; eauto.
rewrite HLD.
reflexivity.
}
Lregset_simpl_tac.
one_step_forward´.
{
accessors_simpl.
Lregset_simpl_tac.
rewrite Hikern, Hihost.
unfold symbol_offset.
rewrite Hsymbol.
rewrite Int.eq_false; [|discriminate]. simpl.
replace (Int.unsigned
(Int.add (Int.add (Int.repr 8) (Int.mul i (Int.repr 4))) Int.zero)) with
(Int.unsigned i × 4 + 8).
lift_trivial.
{
rewrite HST3.
reflexivity.
}
{
apply vmcs_ZtoEncoding_range in H3.
rewrite Int.add_zero.
unfold Int.add, Int.mul.
change (Int.unsigned (Int.repr 8)) with 8.
change (Int.unsigned (Int.repr 4)) with 4.
rewrite (Int.unsigned_repr (Int.unsigned i × 4)); [| rewrite_omega].
rewrite Int.unsigned_repr; rewrite_omega.
}
}
Lregset_simpl_tac.
one_step_forward´.
Lregset_simpl_tac.
one_step_forward´.
{
accessors_simpl.
Lregset_simpl_tac.
rewrite Hikern, Hihost.
unfold symbol_offset.
rewrite Hsymbol.
rewrite Int.eq_false; [|discriminate]. simpl.
lift_trivial.
replace (Int.unsigned
(Int.add
(Int.add (Int.repr 8)
(Int.mul (Int.add i (Int.add Int.zero Int.one))
(Int.repr 4))) Int.zero)) with
(Int.unsigned i × 4 + 12).
{
rewrite HST4.
reflexivity.
}
{
apply vmcs_ZtoEncoding_range in H3.
rewrite Int.add_zero.
change (Int.add Int.zero Int.one) with Int.one.
unfold Int.add, Int.mul.
change (Int.unsigned (Int.repr 8)) with 8.
change (Int.unsigned (Int.repr 4)) with 4.
change (Int.unsigned Int.one) with 1.
rewrite (Int.unsigned_repr (Int.unsigned i + 1)); [| rewrite_omega].
rewrite (Int.unsigned_repr ((Int.unsigned i + 1) × 4)); [| rewrite_omega].
rewrite Int.unsigned_repr; rewrite_omega.
}
}
Lregset_simpl_tac.
one_step_forward´.
{
lift_trivial.
inv H6.
change (Int.unsigned (Int.add Int.zero (Int.repr 0))) with 0.
change (Int.unsigned (Int.add Int.zero (Int.repr 4))) with 4.
unfold set; simpl.
erewrite Mem.load_store_other; [|eassumption| eauto].
erewrite Mem.load_store_other; [|eassumption| eauto].
repeat(erewrite Mem.load_store_other; [|eassumption| simpl; right; right; omega]).
erewrite Mem.load_store_same; eauto 1.
erewrite register_type_load_result.
erewrite Mem.load_store_other; [|eassumption| eauto].
erewrite Mem.load_store_other; [|eassumption| eauto].
repeat(erewrite Mem.load_store_other; [|eassumption | simpl; right; right; omega]).
erewrite Mem.load_store_other; eauto 1.
erewrite Mem.load_store_same; eauto 1.
erewrite register_type_load_result.
rewrite HFree. reflexivity.
apply inv_reg_wt.
right; left. simpl. omega.
apply inv_reg_wt.
}
Lregset_simpl_tac.
one_step_forward´.
Lregset_simpl_tac.
econstructor.
reflexivity.
- inv H6. inv inv_inject_neutral.
eapply Mem.neutral_inject in inv_mem_inject_neutral.
assert (HFB: ∀ b2 delta, Mem.flat_inj (Mem.nextblock m0) b2 ≠ Some (b1, delta)).
{
intros. unfold Mem.flat_inj.
red; intros.
destruct (plt b2 (Mem.nextblock m0)). inv H6.
rewrite (Mem.alloc_result _ _ _ _ _ HALC) in p.
xomega. inv H6.
}
assert (HINJ: Mem.inject (mem:= mwd LDATAOps) (Mem.flat_inj (Mem.nextblock (mem:= mwd LDATAOps) (m0, l0)))
(m´1, l0) (m6, l0)).
{
lift_unfold.
split; trivial.
eapply Mem.free_right_inject; eauto 1; [|intros; specialize (HFB b2 delta); apply HFB; trivial].
assert (HINJ: Mem.inject (Mem.flat_inj (Mem.nextblock m0)) m0 m3).
{
repeat (eapply Mem.store_outside_inject; [ | | eassumption]
; [|intros b2 delta; intros; specialize (HFB b2 delta); apply HFB; trivial]).
eapply Mem.alloc_right_inject; eauto 1.
eapply inv_mem_inject_neutral.
}
assert (Hinj: Mem.flat_inj (Mem.nextblock m0) b0 = Some (b0, 0)).
{
eapply stencil_find_symbol_inject´; eauto.
eapply flat_inj_inject_incr.
xomega.
}
exploit Mem.store_mapped_inject; eauto.
rewrite Z.add_0_r.
rewrite HST3.
intros (m´ & Heq & Hinj1). inv Heq.
exploit Mem.store_mapped_inject; eauto.
rewrite Z.add_0_r.
rewrite HST4.
intros (m´´ & Heq & Hinj2). inv Heq.
assumption.
}
assumption.
- simpl. rewrite (Mem.nextblock_free _ _ _ _ _ HFree); trivial.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST4); trivial.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST3); trivial.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST2); trivial.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST1); trivial.
rewrite (Mem.nextblock_alloc _ _ _ _ _ HALC) ; eauto.
clear. abstract xomega.
- subst rs´0. Lregset_simpl_tac.
unfold Lregset_fold; simpl.
intros reg.
repeat (rewrite Pregmap.gsspec).
simpl_destruct_reg.
exploit reg_false; try eassumption.
intros HF. inv HF.
Qed.
Lemma vmcs_writez64_code_correct:
asm_spec_le (vmcs_writez64 ↦ vmcs_writez64_spec_low)
(〚vmcs_writez64 ↦ vmcs_writez64_function 〛 eptinit).
Proof.
eapply asm_sem_intro; try reflexivity; simpl.
intros. inv H.
eapply make_program_make_globalenv in H0.
exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
intros Hstencil_matches.
exploit vmcs_writez64_spec; eauto 2.
intros (f´ & m0´ & r_ & Hstep & Hincr & HINJ & Hle & Hreg).
assert (Heq: (Mem.nextblock m = Mem.nextblock m´)%positive)
by link_nextblock_asm.
assert (Hle´: (Mem.nextblock m ≤ Mem.nextblock m´)%positive).
{
rewrite Heq; reflexivity.
}
refine_split´; try eassumption.
- lift_unfold. rewrite <- Heq. eassumption.
- lift_unfold. destruct HINJ as (HINJ & Heq´). inv Heq´.
split; trivial.
- lift_unfold. rewrite <- Heq. assumption.
- esplit; reflexivity.
Qed.
End VMCS_WRITEZ64.
End WITHMEM.
End ASM_VERIFICATION.