Library mcertikos.virt.intel.VMXIntroGenAsm
*********************************************************************** * * * 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 VVMCSInit.
Require Import VMXIntroGenSpec.
Require Import VMXIntroGenAsmSource.
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}.
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 vmx_exit_spec:
∀ ge (s: stencil) (rs: regset) rs´ b (m0 m1 m2 m3 m4 m5 m6: mem) b0 v0 v1 labd,
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_G_RDI (rs01 EDI) = Some m1 →
Mem.store Mint32 m1 b0 VMX_G_RAX (rs01 EAX) = Some m2 →
Mem.store Mint32 m2 b0 VMX_G_RBX (rs01 EBX) = Some m3 →
Mem.store Mint32 m3 b0 VMX_G_RDX (rs01 EDX) = Some m4 →
Mem.store Mint32 m4 b0 VMX_G_RSI (rs01 ESI) = Some m5 →
Mem.store Mint32 m5 b0 VMX_G_RBP (rs01 EBP) = Some m6 →
Mem.load Mint32 m6 b0 VMX_HOST_EBP = Some v0 →
Mem.load Mint32 m6 b0 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_: regset,
lasm_step (vmx_exit ↦ vmx_exit_function)
(vmcsinit (Hmwd:= Hmwd) (Hmem:= Hmem)) vmx_exit s rs (m0, labd) r_ (m6, labd)
∧ (∀ l,
Val.lessdef (Pregmap.get l (rs´#Asm.EBP <- v0 #Asm.EDI <- v1 #PC <- (rs RA)))
(Pregmap.get l r_)).
Proof.
simpl; intros.
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).
esplit; split.
- econstructor; try eassumption.
rewrite H1.
one_step_forward´.
{
accessors_simpl.
rewrite Hhost, Hkern.
unfold symbol_offset. rewrite HLOC.
simpl. lift_trivial.
change (Int.unsigned (Int.add (Int.add (Int.repr 40) Int.zero) Int.zero)) with 40.
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.
change (Int.unsigned (Int.add (Int.add (Int.repr 0) Int.zero) Int.zero)) with 0.
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.
change (Int.unsigned (Int.add (Int.add (Int.repr 8) Int.zero) Int.zero)) with 8.
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.
change (Int.unsigned (Int.add (Int.add (Int.repr 24) Int.zero) Int.zero)) with 24.
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.
change (Int.unsigned (Int.add (Int.add (Int.repr 32) Int.zero) Int.zero)) with 32.
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.
change (Int.unsigned (Int.add (Int.add (Int.repr 48) Int.zero) Int.zero)) with 48.
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.
change (Int.unsigned (Int.add (Int.add (Int.repr 132) Int.zero) Int.zero)) with 132.
rewrite H9.
reflexivity.
}
one_step_forward´.
{
accessors_simpl.
rewrite Hhost, Hkern.
unfold symbol_offset. rewrite HLOC.
simpl. lift_trivial.
change (Int.unsigned (Int.add (Int.add (Int.repr 136) Int.zero) Int.zero)) with 136.
rewrite H10.
reflexivity.
}
one_step_forward´.
Lregset_simpl_tac.
constructor.
reflexivity.
- 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 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 H14. 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.
subst rs01.
link_inject_neutral_asm;
eapply inv_reg_inject_neutral.
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_enter_spec:
∀ ge (s: stencil) (rs: regset) rs´ b (m0 m1 m2: mem) b0 v0 v1 v2 v3 v4 v5 v6 labd 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_HOST_EBP (rs01 EBP) = Some m1 →
Mem.store Mint32 m1 b0 VMX_HOST_EDI (rs01 EDI) = Some m2 →
Mem.load Mint32 m2 b0 VMX_G_RAX = Some v0 →
Mem.load Mint32 m2 b0 VMX_G_RBX = Some v1 →
Mem.load Mint32 m2 b0 VMX_G_RDX = Some v2 →
Mem.load Mint32 m2 b0 VMX_G_RSI = Some v3 →
Mem.load Mint32 m2 b0 VMX_G_RDI = Some v4 →
Mem.load Mint32 m2 b0 VMX_G_RBP = Some v5 →
Mem.load Mint32 m2 b0 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_: regset,
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.
simpl; intros.
rename H12 into HRR, H13 into HTRAP.
destruct H14 as [Hkern Hhost].
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.
}
rewrite (Lregset_rewrite rs).
esplit; split.
- econstructor; try eassumption.
rewrite H1.
one_step_forward´.
{
accessors_simpl.
rewrite Hhost, Hkern.
unfold symbol_offset. rewrite HLOC.
simpl. lift_trivial.
change (Int.unsigned (Int.add (Int.add (Int.repr 132) Int.zero) Int.zero)) with 132.
change (((Pregmap.init Vundef) # EDI <- (rs EDI)) # EBP <- (rs EBP) EBP) with (rs EBP) in H3.
rewrite H3.
unfold set; simpl; reflexivity.
}
one_step_forward´.
{
accessors_simpl.
rewrite Hhost, Hkern.
unfold symbol_offset. rewrite HLOC.
simpl. lift_trivial.
change (Int.unsigned (Int.add (Int.add (Int.repr 136) Int.zero) Int.zero)) with 136.
change (((Pregmap.init Vundef) # EDI <- (rs EDI)) # EBP <- (rs EBP) EDI) with (rs EDI) in H4.
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.
simpl. lift_trivial.
change (Int.unsigned (Int.add (Int.add (Int.repr 0) Int.zero) Int.zero)) with 0.
rewrite H5.
reflexivity.
}
one_step_forward´.
{
accessors_simpl.
rewrite Hhost, Hkern.
unfold symbol_offset. rewrite HLOC.
simpl. lift_trivial.
change (Int.unsigned (Int.add (Int.add (Int.repr 8) Int.zero) Int.zero)) with 8.
rewrite H6.
reflexivity.
}
one_step_forward´.
{
accessors_simpl.
rewrite Hhost, Hkern.
unfold symbol_offset. rewrite HLOC.
simpl. lift_trivial.
change (Int.unsigned (Int.add (Int.add (Int.repr 24) Int.zero) Int.zero)) with 24.
rewrite H7.
reflexivity.
}
one_step_forward´.
{
accessors_simpl.
rewrite Hhost, Hkern.
unfold symbol_offset. rewrite HLOC.
simpl. lift_trivial.
change (Int.unsigned (Int.add (Int.add (Int.repr 32) Int.zero) Int.zero)) with 32.
rewrite H8.
reflexivity.
}
one_step_forward´.
{
accessors_simpl.
rewrite Hhost, Hkern.
unfold symbol_offset. rewrite HLOC.
simpl. lift_trivial.
change (Int.unsigned (Int.add (Int.add (Int.repr 40) Int.zero) Int.zero)) with 40.
rewrite H9.
reflexivity.
}
one_step_forward´.
{
accessors_simpl.
rewrite Hhost, Hkern.
unfold symbol_offset. rewrite HLOC.
simpl. lift_trivial.
change (Int.unsigned (Int.add (Int.add (Int.repr 48) Int.zero) Int.zero)) with 48.
rewrite H10.
reflexivity.
}
one_step_forward´.
{
accessors_simpl.
rewrite Hhost, Hkern.
unfold symbol_offset. rewrite HLOC.
simpl. lift_trivial.
change (Int.unsigned (Int.add (Int.add (Int.repr 56) Int.zero) Int.zero)) with 56.
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.
- 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 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.
exploit vmx_enter_spec; eauto 2.
intros [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 H16. 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.