Library mcertikos.proc.VMCSIntroGenAsm
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.
Require Import Z64Lemma.
Require Import VCGen.
Section ASM_VERIFICATION.
Local Open Scope string_scope.
Local Open Scope error_monad_scope.
Local Open Scope Z_scope.
Context `{real_params: RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Notation LDATA := RData.
Notation LDATAOps := (cdata LDATA).
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
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.
Lemma Hget_CPU_ID:
∀ MCode_Asm s ge,
make_globalenv s MCode_Asm eptinit = ret ge →
(∃ b_get_CPU_ID, Genv.find_symbol ge get_CPU_ID = Some b_get_CPU_ID
∧ Genv.find_funct_ptr ge b_get_CPU_ID =
Some (External (EF_external get_CPU_ID (mksignature nil (Some Tint) cc_default))))
∧ get_layer_primitive get_CPU_ID eptinit = OK (Some (gensem get_CPU_ID_spec)).
Proof.
intros.
assert (Hprim: get_layer_primitive get_CPU_ID eptinit = OK (Some (gensem get_CPU_ID_spec)))
by (unfold eptinit; reflexivity).
split; try assumption.
eapply make_globalenv_get_layer_primitive; eauto.
Qed.
Notation v_vmcs_size := 4096.
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_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 (Hhigh: high_level_invariant (snd m0)),
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 (v_vmcs_size × (CPU_ID (snd m0)) + (Int.unsigned i) × 4 + 8) (Vint v1) = Some m´0 →
Mem.store Mint32 m´0 b0 (v_vmcs_size × (CPU_ID (snd m0)) + (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.
generalize max_unsigned_val; intro muval.
intros.
destruct H9 as [Hikern Hihost].
destruct m0 as [m0 d].
destruct m´0 as [m´0 ?].
destruct m´1 as [m´1 ?].
Opaque Z.mul.
lift_unfold; store_split.
caseEq(Mem.alloc m0 0 12).
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 4 Freeable).
{
eapply HV; auto; simpl; try omega.
unfold Z.divide.
∃ 1; 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 8 Freeable).
{
eapply Mem.store_valid_access_1; eauto.
eapply HV; auto; simpl; try omega.
unfold Z.divide.
∃ 2; omega.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HV2; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (rs RA) HV2) as [m3 HST2].
assert (HVdx: Mem.valid_access m3 Mint32 b1 0 Freeable).
{
eapply Mem.store_valid_access_1; eauto.
eapply Mem.store_valid_access_1; eauto.
eapply HV; auto; simpl; try omega.
unfold Z.divide.
∃ 0; omega.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HVdx; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (rs ESP) HVdx) as [mdx HSTdx].
assert (HVsi: Mem.valid_access mdx Mint32 b1 0 Freeable).
{
eapply Mem.store_valid_access_1; eauto.
eapply Mem.store_valid_access_1; eauto.
eapply Mem.store_valid_access_1; eauto.
eapply HV; auto; simpl; try omega.
unfold Z.divide.
∃ 0; omega.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HVsi; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (rs ESI) HVsi) as [msi HSTsi].
assert (HV3: Mem.valid_access msi Mint32 b0 (4096 × CPU_ID l0 + Int.unsigned i × 4 + 8) Writable).
{
eapply Mem.store_valid_access_1; eauto.
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_3; eauto.
}
destruct (Mem.valid_access_store _ _ _ _ (Vint v1) HV3) as [m4 HST3].
assert (HV4: Mem.valid_access m4 Mint32 b0 (4096 × CPU_ID l0 + 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.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 12 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.
}
exploit Hget_CPU_ID; eauto.
intros [[b_get_CPU_ID [HCPU_ID_symbol HCPU_ID_fun]] prim_get_CPU_ID].
rewrite (Lregset_rewrite rs).
refine_split´; try eassumption; try reflexivity.
rewrite H1.
inv H8. inv H13. inv H14. inv H11.
inv H12. inv H10.
econstructor; eauto.
- one_step_forward´.
{
Lregset_simpl_tac.
lift_trivial.
change (Int.unsigned (Int.add Int.zero (Int.repr 8))) with 8.
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.unsigned (Int.add Int.zero (Int.add Int.zero (Int.repr 0)))) with 0.
rewrite Hikern, Hihost.
rewrite HSTdx.
reflexivity.
}
one_step_forward´.
change (Int.add (Int.add Int.zero Int.one) Int.one) with (Int.repr 2).
unfold symbol_offset. unfold fundef.
rewrite HCPU_ID_symbol.
Lregset_simpl_tac.
eapply star_step; eauto.
eapply (LAsm.exec_step_external _ b_get_CPU_ID); eauto.
constructor_gen_sem_intro.
simpl. econstructor; eauto.
red. red. red. red. red. red.
change positive with ident in ×.
rewrite prim_get_CPU_ID.
refine_split´; try reflexivity.
econstructor; eauto.
refine_split´; try reflexivity; try eassumption.
simpl. repeat split.
unfold get_CPU_ID_spec.
unfold ObjMultiprocessor.get_CPU_ID_spec.
simpl.
subrewrite´.
rewrite Int.unsigned_repr.
reflexivity.
inv Hhigh; omega.
intros.
inv H6.
unfold set; simpl.
unfold lift; simpl.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HSTdx); trivial.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST2); trivial.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST1); trivial.
inv H7; assumption.
Lregset_simpl_tac.
intro contra; discriminate contra.
Lregset_simpl_tac.
intro contra; discriminate contra.
Lregset_simpl_tac.
one_step_forward´.
unfold Int.mul.
inv Hhigh.
discharge_cmp.
Lregset_simpl_tac.
one_step_forward´.
{
accessors_simpl.
change (Int.unsigned (Int.add Int.zero (Int.add Int.zero (Int.repr 0)))) with 0.
rewrite Hikern, Hihost.
erewrite Mem.load_store_same; eauto.
}
one_step_forward´.
{
accessors_simpl.
change (Int.unsigned (Int.add Int.zero (Int.add Int.zero (Int.repr 0)))) with 0.
rewrite Hikern, Hihost.
rewrite HSTsi.
reflexivity.
}
one_step_forward´.
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.
unfold nextinstr_nf, nextinstr; simpl.
inv H6.
unfold AsmX.wt_regset in inv_reg_wt.
specialize (inv_reg_wt ESP).
simpl in inv_reg_wt.
assert(tmp: match rs ESP with
| Vundef ⇒ Vundef
| Vint n ⇒ Vint n
| Vlong _ ⇒ Vundef
| Vfloat _ ⇒ Vundef
| Vptr b2 ofs ⇒ Vptr b2 ofs
end = rs ESP).
{
destruct (rs ESP); try inv inv_reg_wt; reflexivity.
}
rewrite tmp.
change (4 × 0) with 0 in H14.
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.
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.
change (4 × 1) with 4 in H13.
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.
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.
change (4 × 2) with 8 in H12.
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.
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.repr (CPU_ID l0 × 4096)))) with (4096 × CPU_ID l0 + Int.unsigned i × 4 + 8).
Opaque Z.mul.
unfold lift; simpl.
{
rewrite HST3.
reflexivity.
}
{
apply vmcs_ZtoEncoding_range in H3.
discharge_cmp.
}
}
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.repr (CPU_ID l0 × 4096)))) with (4096 × CPU_ID l0 + Int.unsigned i × 4 + 12).
Opaque Z.mul.
unfold lift; simpl.
{
rewrite HST4.
reflexivity.
}
{
apply vmcs_ZtoEncoding_range in H3.
discharge_cmp.
}
}
one_step_forward´.
{
accessors_simpl.
change (Int.unsigned (Int.add Int.zero (Int.add Int.zero (Int.repr 0)))) with 0.
rewrite Hikern, Hihost.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_same; eauto.
}
Lregset_simpl_tac.
one_step_forward´.
{
unfold lift; simpl.
inv H6.
change (Int.unsigned (Int.add Int.zero (Int.repr 8))) with 8.
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 msi).
{
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 _ _ _ _ _ _ HSTsi); trivial.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HSTdx); 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.
inv H6.
unfold AsmX.wt_regset in inv_reg_wt.
specialize (inv_reg_wt ESI).
simpl in inv_reg_wt.
eapply register_type_load_result in inv_reg_wt.
simpl in inv_reg_wt.
rewrite inv_reg_wt.
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.
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
(Hhigh: high_level_invariant (snd m0)),
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 (v_vmcs_size × (CPU_ID (snd m0)) + (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.
generalize max_unsigned_val; intro muval.
intros. rename H9 into Hident.
destruct m0 as [m0 d]. destruct m´0 as [m´0 ?].
Opaque Z.mul.
lift_unfold. destruct H4 as [H4 Heq]. inv Heq.
caseEq(Mem.alloc m0 0 12).
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 4 Freeable).
{
eapply HV; auto; simpl; try omega.
unfold Z.divide.
∃ 1; 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 8 Freeable).
{
eapply Mem.store_valid_access_1; eauto.
eapply HV; auto; simpl; try omega.
unfold Z.divide.
∃ 2; omega.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HV2; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (rs RA) HV2) as [m3 HST2].
assert (HVdx: Mem.valid_access m3 Mint32 b1 0 Freeable).
{
eapply Mem.store_valid_access_1; eauto.
eapply Mem.store_valid_access_1; eauto.
eapply HV; auto; simpl; try omega.
unfold Z.divide.
∃ 0; omega.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HVdx; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (rs ESP) HVdx) as [mdx HSTdx].
assert (HV3: Mem.valid_access mdx Mint32 b0 (4096 × CPU_ID l + Int.unsigned i × 4 + 8) 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_3; eauto.
}
destruct (Mem.valid_access_store _ _ _ _ (Vptr ba ofsa) HV3) as [m4 HST3].
assert (HV4: Mem.range_perm m4 b1 0 12 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.
}
exploit Hget_CPU_ID; eauto.
intros [[b_get_CPU_ID [HCPU_ID_symbol HCPU_ID_fun]] prim_get_CPU_ID].
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.
econstructor; eauto.
- one_step_forward´.
{
Lregset_simpl_tac.
lift_trivial.
change (Int.unsigned (Int.add Int.zero (Int.repr 8))) with 8.
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.unsigned (Int.add Int.zero (Int.add Int.zero (Int.repr 0)))) with 0.
rewrite Hikern, Hihost.
rewrite HSTdx.
reflexivity.
}
one_step_forward´.
change (Int.add (Int.add Int.zero Int.one) Int.one) with (Int.repr 2).
unfold symbol_offset. unfold fundef.
rewrite HCPU_ID_symbol.
Lregset_simpl_tac.
eapply star_step; eauto.
eapply (LAsm.exec_step_external _ b_get_CPU_ID); eauto.
constructor_gen_sem_intro.
simpl. econstructor; eauto.
red. red. red. red. red. red.
change positive with ident in ×.
rewrite prim_get_CPU_ID.
refine_split´; try reflexivity.
econstructor; eauto.
refine_split´; try reflexivity; try eassumption.
simpl. repeat split.
unfold get_CPU_ID_spec.
unfold ObjMultiprocessor.get_CPU_ID_spec.
simpl.
subrewrite´.
rewrite Int.unsigned_repr.
reflexivity.
inv Hhigh; omega.
intros.
inv H5.
unfold set; simpl; unfold lift; simpl.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HSTdx); trivial.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST2); trivial.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST1); trivial.
Lregset_simpl_tac.
intro contra; discriminate contra.
Lregset_simpl_tac.
intro contra; discriminate contra.
Lregset_simpl_tac.
one_step_forward´.
unfold Int.mul.
inv Hhigh.
discharge_cmp.
Lregset_simpl_tac.
one_step_forward´.
{
accessors_simpl.
change (Int.unsigned (Int.add Int.zero (Int.add Int.zero (Int.repr 0)))) with 0.
rewrite Hikern, Hihost.
erewrite Mem.load_store_same; eauto.
}
clear prim_get_CPU_ID.
change (4 × 0) with 0 in H10.
change (4 × 1) with 4 in H11.
one_step_forward´.
{
accessors_simpl.
change (Int.add Int.zero (Int.repr 0)) with (Int.repr 0).
simpl in ×.
rewrite Hikern, Hihost.
unfold AsmX.wt_regset in inv_reg_wt.
specialize (inv_reg_wt ESP).
simpl in inv_reg_wt.
eapply register_type_load_result in inv_reg_wt.
simpl in inv_reg_wt.
rewrite inv_reg_wt.
destruct (Val.add (rs ESP) (Vint (Int.repr 0))); try (inv H10; fail).
unfold set; simpl.
unfold lift; simpl.
assert (Plt b2 (Mem.nextblock m0)).
{
eapply Mem.load_valid_access in H10.
eapply Mem.valid_access_implies with (p2:= Nonempty) in H10; [|constructor].
exploit Mem.valid_access_valid_block; eauto.
apply H10.
}
exploit Mem.alloc_result; eauto.
intro nbm1.
assert (b1 ≠ b2).
{
intro.
rewrite <- nbm1 in H5.
rewrite H6 in H5.
xomega.
}
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_alloc_other; eauto.
}
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.
assert (Plt b2 (Mem.nextblock m0)).
{
eapply Mem.load_valid_access in H11.
eapply Mem.valid_access_implies with (p2:= Nonempty) in H11; [|constructor].
exploit Mem.valid_access_valid_block; eauto.
}
exploit Mem.alloc_result; eauto.
intro nbm1.
assert (b1 ≠ b2).
{
intro.
rewrite <- nbm1 in H5.
rewrite H6 in H5.
xomega.
}
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_alloc_other; eauto.
}
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.
Opaque Z.mul Z.add.
apply vmcs_ZtoEncoding_range in H3.
discharge_cmp.
unfold lift; simpl.
replace (8 + Int.unsigned i × 4 + CPU_ID l × 4096) with (4096 × CPU_ID l + Int.unsigned i × 4 + 8) by omega.
rewrite HST3.
reflexivity.
}
Lregset_simpl_tac.
one_step_forward´.
{
unfold set; unfold lift; simpl.
inv H4.
change (Int.unsigned (Int.add Int.zero (Int.repr 8))) with 8.
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 mdx).
{
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 _ _ _ _ _ _ HSTdx); 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.
unfold nextinstr_nf, nextinstr; simpl.
repeat (rewrite Pregmap.gsspec).
simpl_destruct_reg.
exploit reg_false; try eassumption.
intros HF. inv HF.
Opaque Z.mul Z.add.
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_WRITEZ.
Lemma vmcs_writez_spec:
∀ ge (s: stencil) (rs rs´: regset) b (m0 m´0: mwd LDATAOps) sig i b0 res´ v
(Hhigh: high_level_invariant (snd m0)),
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 (v_vmcs_size × (CPU_ID (snd m0)) + (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.
generalize max_unsigned_val; intro muval.
intros.
destruct m0 as [m0 d]. destruct m´0 as [m´0 ?].
Opaque Z.mul.
lift_unfold.
Transparent Z.mul.
destruct H4 as [H4 Heq]. inv Heq.
caseEq(Mem.alloc m0 0 12).
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 4 Freeable).
{
eapply HV; auto; simpl; try omega.
unfold Z.divide.
∃ 1; 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 8 Freeable).
{
eapply Mem.store_valid_access_1; eauto.
eapply HV; auto; simpl; try omega.
unfold Z.divide.
∃ 2; omega.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HV2; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (rs RA) HV2) as [m3 HST2].
assert (HVdx: Mem.valid_access m3 Mint32 b1 0 Freeable).
{
eapply Mem.store_valid_access_1; eauto.
eapply Mem.store_valid_access_1; eauto.
eapply HV; auto; simpl; try omega.
unfold Z.divide.
∃ 0; omega.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HVdx; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (rs ESP) HVdx) as [mdx HSTdx].
assert (HV3: Mem.valid_access mdx Mint32 b0 (4096 × CPU_ID l + Int.unsigned i × 4 + 8) 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_3; eauto.
}
destruct (Mem.valid_access_store _ _ _ _ (Vint v) HV3) as [m4 HST3].
assert (HV4: Mem.range_perm m4 b1 0 12 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.
}
Opaque Z.mul Z.add.
lift_unfold.
exploit Hget_CPU_ID; eauto.
intros [[b_get_CPU_ID [HCPU_ID_symbol HCPU_ID_fun]] prim_get_CPU_ID].
destruct H8 as [Hikern Hihost].
rewrite (Lregset_rewrite rs).
refine_split´; try eassumption; try reflexivity.
rewrite H1.
store_split.
inv H7. inv H12. inv H9. inv H10.
econstructor; eauto.
- one_step_forward´.
{
Lregset_simpl_tac.
Opaque Z.mul.
lift_trivial.
Transparent Z.mul.
change (Int.unsigned (Int.add Int.zero (Int.repr 8))) with 8.
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.unsigned (Int.add Int.zero (Int.add Int.zero (Int.repr 0)))) with 0.
rewrite Hikern, Hihost.
rewrite HSTdx.
reflexivity.
}
one_step_forward´.
change (Int.add (Int.add Int.zero Int.one) Int.one) with (Int.repr 2).
unfold symbol_offset. unfold fundef.
rewrite HCPU_ID_symbol.
Lregset_simpl_tac.
eapply star_step; eauto.
eapply (LAsm.exec_step_external _ b_get_CPU_ID); eauto.
constructor_gen_sem_intro.
simpl. econstructor; eauto.
red. red. red. red. red. red.
change positive with ident in ×.
rewrite prim_get_CPU_ID.
refine_split´; try reflexivity.
econstructor; eauto.
refine_split´; try reflexivity; try eassumption.
simpl. repeat split.
unfold get_CPU_ID_spec.
unfold ObjMultiprocessor.get_CPU_ID_spec.
simpl.
subrewrite´.
rewrite Int.unsigned_repr.
reflexivity.
inv Hhigh; omega.
intros.
inv H6.
unfold set; simpl.
unfold lift; simpl.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HSTdx); trivial.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST2); trivial.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST1); trivial.
Lregset_simpl_tac.
intro contra; discriminate contra.
Lregset_simpl_tac.
intro contra; discriminate contra.
Lregset_simpl_tac.
one_step_forward´.
unfold Int.mul.
inv Hhigh.
discharge_cmp.
Lregset_simpl_tac.
one_step_forward´.
{
accessors_simpl.
change (Int.unsigned (Int.add Int.zero (Int.add Int.zero (Int.repr 0)))) with 0.
rewrite Hikern, Hihost.
erewrite Mem.load_store_same; eauto.
}
one_step_forward´.
{
accessors_simpl.
change (Int.add Int.zero (Int.repr 0)) with (Int.repr 0).
simpl in ×.
rewrite Hikern, Hihost.
unfold nextinstr_nf, nextinstr; simpl.
inv H5.
unfold AsmX.wt_regset in inv_reg_wt.
specialize (inv_reg_wt ESP).
simpl in inv_reg_wt.
assert(tmp: match rs ESP with
| Vundef ⇒ Vundef
| Vint n ⇒ Vint n
| Vlong _ ⇒ Vundef
| Vfloat _ ⇒ Vundef
| Vptr b2 ofs ⇒ Vptr b2 ofs
end = rs ESP).
{
destruct (rs ESP); try inv inv_reg_wt; reflexivity.
}
rewrite tmp.
change (Stacklayout.fe_ofs_arg + 0) with 0 in H11.
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.
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.
change (Stacklayout.fe_ofs_arg +
match 0 + 1 with
| 0 ⇒ 0
| Z.pos y´ ⇒ Z.pos y´~0~0
| Z.neg y´ ⇒ Z.neg y´~0~0
end) with 4 in H12.
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.
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.repr (CPU_ID l × 4096)))) with (4096 × CPU_ID l + Int.unsigned i × 4 + 8).
Opaque Z.mul.
lift_trivial.
{
rewrite HST3.
reflexivity.
}
{
generalize max_unsigned_val; intro muval1.
apply vmcs_ZtoEncoding_range in H3.
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.
Opaque Z.add.
discharge_cmp.
generalize max_unsigned_val; intro.
omega.
generalize max_unsigned_val; intro; omega.
generalize max_unsigned_val; intro; repeat rewrite Int.unsigned_repr; try omega.
}
}
Lregset_simpl_tac.
one_step_forward´.
{
lift_trivial.
inv H5.
change (Int.unsigned (Int.add Int.zero (Int.repr 8))) with 8.
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 mdx).
{
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 _ _ _ _ _ _ HSTdx); 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.
unfold nextinstr_nf, nextinstr; simpl.
repeat (rewrite Pregmap.gsspec).
simpl_destruct_reg.
exploit reg_false; try eassumption.
intros HF. inv HF.
Transparent Z.mul Z.add.
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_READZ64.
Lemma vmcs_readz64_spec:
∀ ge (s: stencil) (rs rs´: regset) b (m0: mwd LDATAOps) sig i b0 res res´ v1 v2
(Hhigh: high_level_invariant (snd m0)),
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 (v_vmcs_size × (CPU_ID (snd m0)) + (Int.unsigned i) × 4 + 8) = Some (Vint v1) →
Mem.load Mint32 m0 b0 (v_vmcs_size × (CPU_ID (snd m0)) + (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.
generalize max_unsigned_val; intro muval.
intros.
destruct m0 as [m0 d].
Opaque Z.mul.
lift_unfold.
Transparent Z.mul.
caseEq(Mem.alloc m0 0 12).
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 4 Freeable).
{
eapply HV; auto; simpl; try omega.
unfold Z.divide.
∃ 1; 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 8 Freeable).
{
eapply Mem.store_valid_access_1; eauto.
eapply HV; auto; simpl; try omega.
unfold Z.divide.
∃ 2; 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 b1 0 Freeable).
{
eapply Mem.store_valid_access_1; eauto.
eapply Mem.store_valid_access_1; eauto.
eapply HV; auto; simpl; try omega.
unfold Z.divide.
∃ 0; omega.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HV3; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (Vint i) HV3) as [m4 HST3].
assert (HV4: Mem.valid_access m4 Mint32 b1 0 Freeable).
{
eapply Mem.store_valid_access_1; eauto.
eapply Mem.store_valid_access_1; eauto.
eapply Mem.store_valid_access_1; eauto.
eapply HV; auto; simpl; try omega.
unfold Z.divide.
∃ 0; omega.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HV4; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (rs ESI) HV4) as [m5 HST4].
assert (HV5: Mem.range_perm m5 b1 0 12 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_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].
exploit Hget_CPU_ID; eauto.
intros [[b_get_CPU_ID [HCPU_ID_symbol HCPU_ID_fun]] prim_get_CPU_ID].
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 8))) with 8.
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).
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.
}
one_step_forward´.
{
accessors_simpl.
change (Int.unsigned (Int.add Int.zero (Int.add Int.zero (Int.repr 0)))) with 0.
rewrite Hikern, Hihost.
rewrite HST3.
reflexivity.
}
one_step_forward´.
change (Int.add (Int.add (Int.add Int.zero Int.one) Int.one)
Int.one) with (Int.repr 3).
unfold symbol_offset. unfold fundef.
rewrite HCPU_ID_symbol.
Lregset_simpl_tac.
eapply star_step; eauto.
eapply (LAsm.exec_step_external _ b_get_CPU_ID); eauto.
constructor_gen_sem_intro.
simpl. econstructor; eauto.
red. red. red. red. red. red.
change positive with ident in ×.
rewrite prim_get_CPU_ID.
refine_split´; try reflexivity.
econstructor; eauto.
refine_split´; try reflexivity; try eassumption.
simpl. repeat split.
unfold get_CPU_ID_spec.
unfold ObjMultiprocessor.get_CPU_ID_spec.
simpl.
subrewrite´.
rewrite Int.unsigned_repr.
reflexivity.
inv Hhigh; omega.
intros.
unfold set; simpl; unfold lift; simpl.
inv H10.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST3); trivial.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST2); trivial.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST1); trivial.
Lregset_simpl_tac.
intro contra; discriminate contra.
Lregset_simpl_tac.
intro contra; discriminate contra.
Lregset_simpl_tac.
one_step_forward´.
unfold Int.mul.
inv Hhigh.
discharge_cmp.
Lregset_simpl_tac.
one_step_forward´.
{
accessors_simpl.
change (Int.unsigned (Int.add Int.zero (Int.add Int.zero (Int.repr 0)))) with 0.
rewrite Hikern, Hihost.
erewrite Mem.load_store_same; eauto.
}
one_step_forward´.
{
accessors_simpl.
change (Int.unsigned (Int.add Int.zero (Int.add Int.zero (Int.repr 0)))) with 0.
rewrite Hikern, Hihost.
unfold nextinstr_nf, nextinstr; simpl.
unfold Int.add; discharge_cmp.
repeat rewrite Pregmap.gso; try intro contra; try inv contra.
Lregset_simpl_tac.
rewrite HST4.
reflexivity.
}
one_step_forward´.
unfold Int.add.
discharge_cmp.
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.
Opaque Z.mul.
lift_unfold.
Transparent Z.mul.
replace (Int.unsigned
(Int.add (Int.add (Int.repr 8) (Int.mul i (Int.repr 4)))
(Int.repr (CPU_ID d × 4096)))) with (4096 × CPU_ID d + Int.unsigned i × 4 + 8).
{
exploit Mem.load_alloc_other.
eauto.
apply H4.
intros HLD.
pose proof (alloc_load_other _ _ _ _ _ _ _ _ _ HALC H4) as Hneq.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_other; eauto.
rewrite HLD.
reflexivity.
}
{
apply vmcs_ZtoEncoding_range in H3.
Opaque Z.mul.
discharge_cmp.
}
}
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.
Opaque Z.mul.
lift_unfold.
Transparent Z.mul.
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.repr (CPU_ID d × 4096)))) with (4096 × CPU_ID d + Int.unsigned i × 4 + 12).
{
exploit Mem.load_alloc_other.
eauto.
apply H5.
intros HLD.
pose proof (alloc_load_other _ _ _ _ _ _ _ _ _ HALC H5) as Hneq.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_other; eauto.
rewrite HLD.
reflexivity.
}
{
apply vmcs_ZtoEncoding_range in H3.
Opaque Z.mul.
discharge_cmp.
}
}
one_step_forward´.
{
accessors_simpl.
change (Int.unsigned (Int.add Int.zero (Int.add Int.zero (Int.repr 0)))) with 0.
rewrite Hikern, Hihost.
erewrite Mem.load_store_same; eauto.
}
Lregset_simpl_tac.
one_step_forward´.
{
lift_trivial.
inv H7.
change (Int.unsigned (Int.add Int.zero (Int.repr 4))) with 4.
change (Int.unsigned (Int.add Int.zero (Int.repr 8))) with 8.
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.
eapply star_refl.
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) (m6, 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 _ _ _ _ _ _ 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 nextinstr_nf, nextinstr; simpl.
unfold Lregset_fold; simpl.
unfold Int.add; discharge_cmp.
intros reg.
repeat (rewrite Pregmap.gsspec).
simpl_destruct_reg.
unfold Pregmap.get.
inv H7.
unfold AsmX.wt_regset in inv_reg_wt.
specialize (inv_reg_wt ESI).
simpl in inv_reg_wt.
destruct (rs ESI); econstructor || inv inv_reg_wt.
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.
Section VMCS_READZ.
Lemma vmcs_readz_spec:
∀ ge (s: stencil) (rs rs´: regset) b (m0: mwd LDATAOps) sig i b0 res res´
(Hhigh: high_level_invariant (snd m0)),
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 (v_vmcs_size × (CPU_ID (snd m0)) + (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].
Opaque Z.mul.
lift_unfold.
Transparent Z.mul.
generalize max_unsigned_val; intro muval.
caseEq(Mem.alloc m0 0 12).
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 4 Freeable).
{
eapply HV; auto; simpl; try omega.
unfold Z.divide.
∃ 1; 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 8 Freeable).
{
eapply Mem.store_valid_access_1; eauto.
eapply HV; auto; simpl; try omega.
unfold Z.divide.
∃ 2; 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 b1 0 Freeable).
{
eapply Mem.store_valid_access_1; eauto.
eapply Mem.store_valid_access_1; eauto.
eapply HV; auto; simpl; try omega.
unfold Z.divide.
∃ 0; omega.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HV3; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (Vint i) HV3) as [m4 HST3].
assert (HV4: Mem.range_perm m4 b1 0 12 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_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].
exploit Hget_CPU_ID; eauto.
intros [[b_get_CPU_ID [HCPU_ID_symbol HCPU_ID_fun]] prim_get_CPU_ID].
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.
discharge_cmp.
rewrite HST2.
reflexivity.
}
Lregset_simpl_tac.
one_step_forward´.
{
accessors_simpl.
change (Int.add Int.zero (Int.repr 0)) with (Int.repr 0).
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.
}
one_step_forward´.
{
accessors_simpl.
change (Int.unsigned (Int.add Int.zero (Int.add Int.zero (Int.repr 0)))) with 0.
rewrite Hikern, Hihost.
rewrite HST3.
reflexivity.
}
one_step_forward´.
change (Int.add (Int.add (Int.add Int.zero Int.one) Int.one)
Int.one) with (Int.repr 3).
unfold symbol_offset. unfold fundef.
rewrite HCPU_ID_symbol.
Lregset_simpl_tac.
eapply star_step; eauto.
eapply (LAsm.exec_step_external _ b_get_CPU_ID); eauto.
constructor_gen_sem_intro.
simpl. econstructor; eauto.
red. red. red. red. red. red.
change positive with ident in ×.
rewrite prim_get_CPU_ID.
refine_split´; try reflexivity.
econstructor; eauto.
refine_split´; try reflexivity; try eassumption.
simpl. repeat split.
unfold get_CPU_ID_spec.
unfold ObjMultiprocessor.get_CPU_ID_spec.
simpl.
subrewrite´.
rewrite Int.unsigned_repr.
reflexivity.
inv Hhigh; omega.
intros.
inv H8.
lift_unfold.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST3); trivial.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST2); trivial.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST1); trivial.
Lregset_simpl_tac.
intro contra; discriminate contra.
Lregset_simpl_tac.
intro contra; discriminate contra.
Lregset_simpl_tac.
one_step_forward´.
unfold Int.mul.
inv Hhigh.
discharge_cmp.
Lregset_simpl_tac.
one_step_forward´.
{
accessors_simpl.
change (Int.unsigned (Int.add Int.zero (Int.add Int.zero (Int.repr 0)))) with 0.
rewrite Hikern, Hihost.
erewrite Mem.load_store_same; eauto.
}
unfold nextinstr_nf, nextinstr; simpl.
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.
Opaque Z.mul.
lift_unfold.
Transparent Z.mul.
replace (Int.unsigned
(Int.add (Int.add (Int.repr 8) (Int.mul i (Int.repr 4)))
(Int.repr (CPU_ID d × 4096)))) with (4096 × CPU_ID d + 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.
erewrite Mem.load_store_other; eauto.
rewrite HLD.
reflexivity.
}
{
apply vmcs_ZtoEncoding_range in H3.
Opaque Z.mul.
discharge_cmp.
}
}
Lregset_simpl_tac.
one_step_forward´.
{
lift_trivial.
inv H5.
change (Int.unsigned (Int.add Int.zero (Int.repr 4))) with 4.
change (Int.unsigned (Int.add Int.zero (Int.repr 8))) with 8.
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) (m5, 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 _ _ _ _ _ _ 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 nextinstr_nf, nextinstr; simpl.
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.
End WITHMEM.
End ASM_VERIFICATION.