Library mcertikos.proc.VMXIntroGenAsm
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 VVMCSInit.
Require Import VMXIntroGenSpec.
Require Import VMXIntroGenAsmSource.
Require Import LAsmModuleSemSpec.
Require Import LRegSet.
Require Import AbstractDataType.
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}.
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.
Definition vmx_size := VMX_Size´ × 4.
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.
Lemma Hhost_out:
∀ s ge,
make_globalenv s (vmx_enter ↦ vmx_enter_function) vmcsinit = ret ge →
(∃ b_host_out, Genv.find_symbol ge host_out = Some b_host_out
∧ Genv.find_funct_ptr ge b_host_out =
Some (External (EF_external host_out null_signature)))
∧ get_layer_primitive host_out vmcsinit = OK (Some (primcall_general_compatsem hostout_spec)).
Proof.
intros.
assert (Hprim: get_layer_primitive host_out vmcsinit =
OK (Some (primcall_general_compatsem hostout_spec)))
by (unfold vmcsinit; reflexivity).
split; try assumption.
eapply make_globalenv_get_layer_primitive; eauto.
Qed.
Lemma vmx_exit_spec:
∀ ge (s: stencil) (rs: regset) rs´ b (m0 m´1 m´2 m´3 m´4 m´5 m´6: mem) b0 v0 v1 labd
(Hhigh: high_level_invariant labd)
(Hasminv: asm_invariant (mem := mwd LDATAOps) s rs (m0, labd))
(HECSVal: rs ECX = Vint (Int.repr (CPU_ID labd × (38 × 4)))),
find_symbol s vmx_exit = Some b →
make_globalenv s (vmx_exit ↦ vmx_exit_function) vmcsinit = ret ge →
rs PC = Vptr b Int.zero →
find_symbol s VMX_LOC = Some b0 →
let rs01 := (Pregmap.init Vundef) #EAX <- (rs EAX) #EBX <- (rs EBX)
#EDX <- (rs EDX) #EDI <- (rs EDI)
#ESI <- (rs ESI) #EBP <- (rs EBP) in
Mem.store Mint32 m0 b0 (vmx_size × (CPU_ID labd) + VMX_G_RDI) (rs01 EDI) = Some m´1 →
Mem.store Mint32 m´1 b0 (vmx_size × (CPU_ID labd) + VMX_G_RAX) (rs01 EAX) = Some m´2 →
Mem.store Mint32 m´2 b0 (vmx_size × (CPU_ID labd) + VMX_G_RBX) (rs01 EBX) = Some m´3 →
Mem.store Mint32 m´3 b0 (vmx_size × (CPU_ID labd) + VMX_G_RDX) (rs01 EDX) = Some m´4 →
Mem.store Mint32 m´4 b0 (vmx_size × (CPU_ID labd) + VMX_G_RSI) (rs01 ESI) = Some m´5 →
Mem.store Mint32 m´5 b0 (vmx_size × (CPU_ID labd) + VMX_G_RBP) (rs01 EBP) = Some m´6 →
Mem.load Mint32 m´6 b0 (vmx_size × (CPU_ID labd) + VMX_HOST_EBP) = Some v0 →
Mem.load Mint32 m´6 b0 (vmx_size × (CPU_ID labd) + VMX_HOST_EDI) = Some v1 →
rs´ = (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR EDX :: IR ECX :: IR EAX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) →
kernel_mode labd →
∃ r_,
lasm_step (vmx_exit ↦ vmx_exit_function)
(vmcsinit (Hmwd:= Hmwd) (Hmem:= Hmem)) vmx_exit s rs (m0, labd) r_ (m´6, labd)
∧ (∀ l,
Val.lessdef (Pregmap.get l (rs´#Asm.EBP <- v0 #Asm.EDI <- v1 #PC <- (rs RA)))
(Pregmap.get l r_)).
Proof.
Opaque Z.mul.
generalize max_unsigned_val; intro muval.
simpl; intros.
inversion Hasminv.
rename H11 into HRR.
destruct H12 as [Hkern Hhost].
exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
intros Hstencil_matches.
assert (Hfunct: Genv.find_funct_ptr ge b = Some (Internal vmx_exit_function)).
{
assert (Hmodule: get_module_function vmx_exit (vmx_exit ↦ vmx_exit_function) = OK (Some vmx_exit_function))
by reflexivity.
assert (HInternal: make_internal vmx_exit_function = OK (AST.Internal vmx_exit_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 (HLOC: Genv.find_symbol ge VMX_LOC = Some b0).
{
inv Hstencil_matches.
congruence.
}
rewrite (Lregset_rewrite rs).
inv inv_inject_neutral.
lift_unfold.
eapply Mem.neutral_inject in 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.
assumption.
}
inv Hhigh.
esplit.
split.
- econstructor; try eassumption.
rewrite H1.
unfold vmx_size in ×.
rewrite HECSVal.
one_step_forward´.
{
accessors_simpl.
rewrite Hhost, Hkern.
unfold symbol_offset. rewrite HLOC.
simpl. lift_trivial.
Opaque Z.add.
discharge_cmp.
lift_trivial.
replace (40 + CPU_ID labd × (VMX_Size´ × 4) + 0) with ((VMX_Size´ × 4) × CPU_ID labd + 40) by omega.
change ((((((((Pregmap.init Vundef) # EAX <- (rs EAX)) # EBX <- (rs EBX))
# EDX <- (rs EDX)) # EDI <- (rs EDI)) # ESI <-
(rs ESI)) # EBP <- (rs EBP) EDI)) with (rs EDI) in H3.
rewrite H3.
unfold set; simpl; reflexivity.
}
one_step_forward´.
Lregset_simpl_tac.
one_step_forward´.
Lregset_simpl_tac.
one_step_forward´.
{
accessors_simpl.
rewrite Hhost, Hkern.
unfold symbol_offset. rewrite HLOC.
simpl. lift_trivial.
discharge_cmp.
lift_trivial.
replace (0 + CPU_ID labd × (VMX_Size´ × 4) + 0) with (VMX_Size´ × 4 × CPU_ID labd + 0) by omega.
change (((((((Pregmap.init Vundef) # EAX <- (rs EAX)) # EBX <- (rs EBX))
# EDX <- (rs EDX)) # EDI <- (rs EDI)) # ESI <-
(rs ESI)) # EBP <- (rs EBP) EAX) with (rs EAX) in H4.
rewrite H4.
unfold set; simpl; reflexivity.
}
one_step_forward´.
{
accessors_simpl.
rewrite Hhost, Hkern.
unfold symbol_offset. rewrite HLOC.
simpl. lift_trivial.
discharge_cmp.
lift_trivial.
replace (8 + CPU_ID labd × (VMX_Size´ × 4) + 0) with (VMX_Size´ × 4 × CPU_ID labd + 8) by omega.
change (((((((Pregmap.init Vundef) # EAX <- (rs EAX)) # EBX <- (rs EBX))
# EDX <- (rs EDX)) # EDI <- (rs EDI)) # ESI <-
(rs ESI)) # EBP <- (rs EBP) EBX) with (rs EBX) in H5.
rewrite H5.
unfold set; simpl; reflexivity.
}
one_step_forward´.
{
accessors_simpl.
rewrite Hhost, Hkern.
unfold symbol_offset. rewrite HLOC.
simpl. lift_trivial.
discharge_cmp.
lift_trivial.
replace (24 + CPU_ID labd × (VMX_Size´ × 4) + 0) with (VMX_Size´ × 4 × CPU_ID labd + 24) by omega.
change (((((((Pregmap.init Vundef) # EAX <- (rs EAX)) # EBX <- (rs EBX))
# EDX <- (rs EDX)) # EDI <- (rs EDI)) # ESI <-
(rs ESI)) # EBP <- (rs EBP) EDX) with (rs EDX) in H6.
rewrite H6.
unfold set; simpl; reflexivity.
}
one_step_forward´.
{
accessors_simpl.
rewrite Hhost, Hkern.
unfold symbol_offset. rewrite HLOC.
simpl. lift_trivial.
discharge_cmp.
lift_trivial.
replace (32 + CPU_ID labd × (VMX_Size´ × 4) + 0) with (VMX_Size´ × 4 × CPU_ID labd + 32) by omega.
change (((((((Pregmap.init Vundef) # EAX <- (rs EAX)) # EBX <- (rs EBX))
# EDX <- (rs EDX)) # EDI <- (rs EDI)) # ESI <-
(rs ESI)) # EBP <- (rs EBP) ESI) with (rs ESI) in H7.
rewrite H7.
unfold set; simpl; reflexivity.
}
one_step_forward´.
{
accessors_simpl.
rewrite Hhost, Hkern.
unfold symbol_offset. rewrite HLOC.
simpl. lift_trivial.
discharge_cmp.
lift_trivial.
replace (48 + CPU_ID labd × (VMX_Size´ × 4) + 0) with (VMX_Size´ × 4 × CPU_ID labd + 48) by omega.
change (((((((Pregmap.init Vundef) # EAX <- (rs EAX)) # EBX <- (rs EBX))
# EDX <- (rs EDX)) # EDI <- (rs EDI)) # ESI <-
(rs ESI)) # EBP <- (rs EBP) EBP) with (rs EBP) in H8.
rewrite H8.
unfold set; simpl; reflexivity.
}
one_step_forward´.
{
accessors_simpl.
rewrite Hhost, Hkern.
unfold symbol_offset. rewrite HLOC.
simpl. lift_trivial.
discharge_cmp.
lift_trivial.
replace (132 + CPU_ID labd × (VMX_Size´ × 4) + 0) with (VMX_Size´ × 4 × CPU_ID labd + 132) by omega.
rewrite H9.
reflexivity.
}
one_step_forward´.
{
accessors_simpl.
rewrite Hhost, Hkern.
unfold symbol_offset. rewrite HLOC.
simpl. lift_trivial.
discharge_cmp.
lift_trivial.
replace (136 + CPU_ID labd × (VMX_Size´ × 4) + 0) with (VMX_Size´ × 4 × CPU_ID labd + 136) by omega.
rewrite H10.
reflexivity.
}
one_step_forward´.
Lregset_simpl_tac.
lift_trivial.
constructor.
reflexivity.
-
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.
Qed.
Lemma vmx_exit_code_correct:
asm_spec_le (vmx_exit ↦ vmx_exit_spec_low)
(〚 vmx_exit ↦ vmx_exit_function 〛 vmcsinit).
Proof.
eapply asm_sem_intro; try solve [ reflexivity | eexists; reflexivity ].
intros. inv H.
eapply make_program_make_globalenv in H0.
exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
intros Hstencil_matches.
exploit vmx_exit_spec; eauto 2.
intros [r_[Hstep Hv]].
assert (Heq: (Mem.nextblock m0 = Mem.nextblock m6)%positive)
by link_nextblock_asm.
assert (Hle´: (Mem.nextblock m0 ≤ Mem.nextblock m6)%positive).
{
rewrite Heq; reflexivity.
}
refine_split´; try eassumption; try reflexivity.
lift_unfold. split; trivial.
inv H16. inv inv_inject_neutral.
eapply Mem.neutral_inject.
assert (Plt b0 (Mem.nextblock m0)).
{
eapply genv_symb_range in H4.
change (Mem.nextblock (m0, labd)) with (Mem.nextblock m0) in ×.
xomega.
}
pose proof (inv_reg_le _ _ _ inv_reg_inject_neutral Hle´) as Hinv_inject.
rewrite <- Heq.
subst rs01.
link_inject_neutral_asm;
eapply inv_reg_inject_neutral.
Qed.
Lemma vmx_enter_spec:
∀ ge (s: stencil) (rs: regset) rs´ b (m0 m1 m2: mem) b0 v0 v1 v2 v3 v4 v5 v6 labd labd´
(Hhigh: high_level_invariant labd)
(ESPValid: rs ESP ≠ Vundef)
(ESPNextblock: (∀ b1 o,
rs ESP = Vptr b1 o →
Ple (Genv.genv_next ge) b1 ∧ Plt b1 (Mem.nextblock m0)))
(Hasminv: asm_invariant (mem := mwd LDATAOps) s rs (m0, labd)),
find_symbol s vmx_enter = Some b →
make_globalenv s (vmx_enter ↦ vmx_enter_function) vmcsinit = ret ge →
rs PC = Vptr b Int.zero →
find_symbol s VMX_LOC = Some b0 →
let rs01 := (Pregmap.init Vundef) #EDI <- (rs EDI) #EBP <- (rs EBP) in
Mem.store Mint32 m0 b0 (vmx_size × (CPU_ID labd) + VMX_HOST_EBP) (rs01 EBP) = Some m1 →
Mem.store Mint32 m1 b0 (vmx_size × (CPU_ID labd) + VMX_HOST_EDI) (rs01 EDI) = Some m2 →
Mem.load Mint32 m2 b0 (vmx_size × (CPU_ID labd) + VMX_G_RAX) = Some v0 →
Mem.load Mint32 m2 b0 (vmx_size × (CPU_ID labd) + VMX_G_RBX) = Some v1 →
Mem.load Mint32 m2 b0 (vmx_size × (CPU_ID labd) + VMX_G_RDX) = Some v2 →
Mem.load Mint32 m2 b0 (vmx_size × (CPU_ID labd) + VMX_G_RSI) = Some v3 →
Mem.load Mint32 m2 b0 (vmx_size × (CPU_ID labd) + VMX_G_RDI) = Some v4 →
Mem.load Mint32 m2 b0 (vmx_size × (CPU_ID labd) + VMX_G_RBP) = Some v5 →
Mem.load Mint32 m2 b0 (vmx_size × (CPU_ID labd) + VMX_G_RIP) = Some v6 →
rs´ = (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) →
hostout_spec labd = Some labd´ →
kernel_mode labd →
∃ r_,
lasm_step (vmx_enter ↦ vmx_enter_function)
(vmcsinit (Hmwd:= Hmwd) (Hmem:= Hmem)) vmx_enter s rs (m0, labd) r_ (m2, labd´)
∧ (∀ l,
Val.lessdef (Pregmap.get l (rs´#Asm.EAX <- v0 #Asm.EBX <- v1 #Asm.EDX <- v2 #Asm.ESI<- v3#Asm.EDI <- v4
#EBP<- v5 #PC <- v6))
(Pregmap.get l r_)).
Proof.
Opaque Z.mul.
generalize max_unsigned_val; intro muval.
simpl; intros.
rename H12 into HRR, H13 into HTRAP.
destruct H14 as [Hkern Hhost].
inversion Hasminv.
exploit Hhost_out; eauto.
intros [[b_hostout [Hhostout_symbol Hhostout_fun]] prim_hostout].
exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
intros Hstencil_matches.
assert (Hfunct: Genv.find_funct_ptr ge b = Some (Internal vmx_enter_function)).
{
assert (Hmodule: get_module_function vmx_enter (vmx_enter ↦ vmx_enter_function) = OK (Some vmx_enter_function))
by reflexivity.
assert (HInternal: make_internal vmx_enter_function = OK (AST.Internal vmx_enter_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 (HLOC: Genv.find_symbol ge VMX_LOC = Some b0).
{
inv Hstencil_matches.
congruence.
}
Lemma Hget_CPU_ID:
∀ MCode_Asm s ge,
make_globalenv s MCode_Asm vmcsinit = 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 vmcsinit = OK (Some (gensem get_CPU_ID_spec)).
Proof.
intros.
assert (Hprim: get_layer_primitive get_CPU_ID vmcsinit = OK (Some (gensem get_CPU_ID_spec)))
by (unfold vmcsinit; reflexivity).
split; try assumption.
eapply make_globalenv_get_layer_primitive; eauto.
Qed.
exploit Hget_CPU_ID; eauto.
intros [[b_get_CPU_ID [HCPU_ID_symbol HCPU_ID_fun]] prim_get_CPU_ID].
rewrite (Lregset_rewrite rs).
esplit; split.
- econstructor; try eassumption.
rewrite H1.
one_step_forward´.
change (Int.add Int.zero Int.one) with (Int.repr 1).
unfold symbol_offset. unfold fundef.
rewrite HCPU_ID_symbol.
Lregset_simpl_tac.
econstructor; eauto.
eapply (LAsm.exec_step_external _ b_get_CPU_ID); eauto.
constructor_gen_sem_intro.
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.
rewrite Hhost, Hkern.
rewrite Int.unsigned_repr.
reflexivity.
inv Hhigh; omega.
Lregset_simpl_tac.
intro contra; discriminate contra.
Lregset_simpl_tac.
one_step_forward´.
Lregset_simpl_tac.
inv Hhigh.
rewrite Pregmap.gss in H3.
rewrite Pregmap.gso in H4; try intro contra; try inv contra.
rewrite Pregmap.gss in H4.
one_step_forward´.
discharge_cmp.
Lregset_simpl_tac.
Opaque Z.mul Z.add.
one_step_forward´.
{
accessors_simpl.
rewrite Hhost, Hkern.
unfold symbol_offset. rewrite HLOC.
discharge_cmp.
unfold lift; simpl.
replace (132 + CPU_ID labd × (VMX_Size´ × 4) + 0) with (vmx_size × CPU_ID labd + 132) by (unfold vmx_size; omega).
rewrite H3.
unfold set; simpl; reflexivity.
}
one_step_forward´.
{
accessors_simpl.
rewrite Hhost, Hkern.
unfold symbol_offset. rewrite HLOC.
discharge_cmp.
unfold lift; simpl.
replace (136 + CPU_ID labd × (VMX_Size´ × 4) + 0) with (vmx_size × CPU_ID labd + 136) by (unfold vmx_size; omega).
rewrite H4.
unfold set; simpl; reflexivity.
}
one_step_forward´.
Lregset_simpl_tac.
one_step_forward´.
Lregset_simpl_tac.
one_step_forward´.
{
accessors_simpl.
rewrite Hhost, Hkern.
unfold symbol_offset. rewrite HLOC.
discharge_cmp.
unfold lift; simpl.
replace (0 + CPU_ID labd × (VMX_Size´ × 4) + 0) with (vmx_size × CPU_ID labd + 0) by (unfold vmx_size; omega).
rewrite H5.
reflexivity.
}
one_step_forward´.
{
accessors_simpl.
rewrite Hhost, Hkern.
unfold symbol_offset. rewrite HLOC.
discharge_cmp.
unfold lift; simpl.
replace (8 + CPU_ID labd × (VMX_Size´ × 4) + 0) with (vmx_size × CPU_ID labd + 8) by (unfold vmx_size; omega).
rewrite H6; reflexivity.
}
one_step_forward´.
{
accessors_simpl.
rewrite Hhost, Hkern.
unfold symbol_offset. rewrite HLOC.
discharge_cmp.
unfold lift; simpl.
replace (24 + CPU_ID labd × (VMX_Size´ × 4) + 0) with (vmx_size × CPU_ID labd + 24) by (unfold vmx_size; omega).
rewrite H7; reflexivity.
}
one_step_forward´.
{
accessors_simpl.
rewrite Hhost, Hkern.
unfold symbol_offset. rewrite HLOC.
discharge_cmp.
unfold lift; simpl.
replace (32 + CPU_ID labd × (VMX_Size´ × 4) + 0) with (vmx_size × CPU_ID labd + 32) by (unfold vmx_size; omega).
rewrite H8; reflexivity.
}
one_step_forward´.
{
accessors_simpl.
rewrite Hhost, Hkern.
unfold symbol_offset. rewrite HLOC.
discharge_cmp.
unfold lift; simpl.
replace (40 + CPU_ID labd × (VMX_Size´ × 4) + 0) with (vmx_size × CPU_ID labd + 40) by (unfold vmx_size; omega).
rewrite H9; reflexivity.
}
one_step_forward´.
{
accessors_simpl.
rewrite Hhost, Hkern.
unfold symbol_offset. rewrite HLOC.
discharge_cmp.
unfold lift; simpl.
replace (48 + CPU_ID labd × (VMX_Size´ × 4) + 0) with (vmx_size × CPU_ID labd + 48) by (unfold vmx_size; omega).
rewrite H10; reflexivity.
}
one_step_forward´.
{
accessors_simpl.
rewrite Hhost, Hkern.
unfold symbol_offset. rewrite HLOC.
discharge_cmp.
unfold lift; simpl.
replace (56 + CPU_ID labd × (VMX_Size´ × 4) + 0) with (vmx_size × CPU_ID labd + 56) by (unfold vmx_size; omega).
rewrite H11; reflexivity.
}
one_step_forward´.
unfold symbol_offset. unfold fundef.
rewrite Hhostout_symbol.
Lregset_simpl_tac.
{
eapply star_one; eauto.
eapply (LAsm.exec_step_prim_call _ b_hostout); eauto 1.
econstructor.
refine_split´; eauto 1.
econstructor; eauto 1. simpl.
econstructor.
apply HTRAP.
}
reflexivity.
- unfold Lregset_fold.
simpl. intros reg.
repeat (rewrite Pregmap.gsspec).
simpl_destruct_reg.
exploit reg_false; try eassumption.
intros HF. inv HF.
Qed.
Lemma vmx_enter_code_correct:
asm_spec_le (vmx_enter ↦ vmx_enter_spec_low)
(〚 vmx_enter ↦ vmx_enter_function 〛 vmcsinit).
Proof.
eapply asm_sem_intro; try solve [ reflexivity | eexists; reflexivity ].
intros. inv H.
eapply make_program_make_globalenv in H0.
exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
intros Hstencil_matches.
rewrite <- (stencil_matches_genv_next _ _ Hstencil_matches) in H19.
assert(tmp: undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: RA :: nil)
(undef_regs (map preg_of destroyed_at_call) rs) = undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: RA :: nil)
(undef_regs (map preg_of destroyed_at_call) rs)) by reflexivity.
exploit vmx_enter_spec; eauto.
intros tmprw.
specialize (tmprw tmp H15 H16).
destruct tmprw as [r_[Hstep Hv]].
assert (Heq: (Mem.nextblock m0 = Mem.nextblock m2)%positive)
by link_nextblock_asm.
assert (Hle: (Mem.nextblock m0 ≤ Mem.nextblock m2)%positive).
{
rewrite Heq; reflexivity.
}
refine_split´; try eassumption; try reflexivity.
lift_unfold. split; trivial.
inv H17. inv inv_inject_neutral.
eapply Mem.neutral_inject.
assert (Plt b0 (Mem.nextblock m0)).
{
eapply genv_symb_range in H3.
change (Mem.nextblock (m0, labd)) with (Mem.nextblock m0) in ×.
xomega.
}
pose proof (inv_reg_le _ _ _ inv_reg_inject_neutral Hle) as Hinv_inject.
rewrite <- Heq.
link_inject_neutral_asm;
eapply inv_reg_inject_neutral.
Qed.
End WITHMEM.
End ASM_VERIFICATION.