Library mcertikos.proc.VMCSIntroGenAsm1
Require Import Coqlib.
Require Import Errors.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Op.
Require Import Locations.
Require Import AuxStateDataType.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Op.
Require Import Values.
Require Import Memory.
Require Import Maps.
Require Import FlatMemory.
Require Import RefinementTactic.
Require Import AuxLemma.
Require Import RealParams.
Require Import Constant.
Require Import AsmImplLemma.
Require Import AsmImplTactic.
Require Import GlobIdent.
Require Import CommonTactic.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compcertx.MakeProgram.
Require Import LAsmModuleSem.
Require Import LAsm.
Require Import liblayers.compat.CompatGenSem.
Require Import PrimSemantics.
Require Import Conventions.
Require Import VEPTInit.
Require Import VMCSIntroGenSpec.
Require Import VMCSIntroGenAsmSource.
Require Import LAsmModuleSemSpec.
Require Import LRegSet.
Require Import AbstractDataType.
Section ASM_VERIFICATION.
Local Open Scope string_scope.
Local Open Scope error_monad_scope.
Local Open Scope Z_scope.
Context `{real_params: RealParams}.
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.
Section VMX_ENABLE.
Lemma vmx_enable_proof:
∀ ge (s: stencil) (rs rs´: regset) b (m0: mwd LDATAOps),
find_symbol s vmx_enable = Some b →
make_globalenv s (vmx_enable ↦ vmx_enable_function) eptinit = ret ge →
rs PC = Vptr b Int.zero →
asm_invariant (mem := mwd LDATAOps) s rs m0 →
∃ r_: regset,
lasm_step (vmx_enable ↦ vmx_enable_function) (eptinit (Hmwd:= Hmwd) (Hmem:= Hmem)) vmx_enable s rs m0 r_ m0
∧ (∀ l,
Val.lessdef (Pregmap.get l (rs#RA<- Vundef#PC <- (rs#RA)))
(Pregmap.get l r_)).
Proof.
intros.
exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
intros Hstencil_matches.
assert(Hfun: Genv.find_funct_ptr ge b = Some (Internal vmx_enable_function)).
{
assert (Hmodule: get_module_function vmx_enable (vmx_enable ↦ vmx_enable_function) = OK (Some vmx_enable_function)) by
reflexivity.
assert (HInternal: make_internal vmx_enable_function = OK (AST.Internal vmx_enable_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.
}
rewrite (Lregset_rewrite rs).
esplit; split.
econstructor; try eassumption.
rewrite H1.
one_step_forward´.
Lregset_simpl_tac.
econstructor.
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_enable_code_correct:
asm_spec_le (vmx_enable ↦ vmx_enable_spec_low)
(〚vmx_enable ↦ vmx_enable_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 vmx_enable_proof; eauto 2.
intros [r_[Hstep Hv]].
refine_split´; try eassumption; try reflexivity.
- inv H3. inv inv_inject_neutral.
eapply Mem.neutral_inject in inv_mem_inject_neutral.
assumption.
- esplit; reflexivity.
Qed.
End VMX_ENABLE.
Section VMPTR_LD.
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 vmptrld_spec:
∀ ge (s: stencil) (rs rs´: regset) b b0 (m0: mwd LDATAOps) (Hhigh: high_level_invariant (snd m0)),
find_symbol s vmptrld = Some b →
make_globalenv s (vmptrld ↦ vmptrld_function) eptinit = ret ge →
rs PC = Vptr b Int.zero →
asm_invariant (mem := mwd LDATAOps) s rs m0 →
kernel_mode (snd m0) →
find_symbol s VMCS_LOC = Some b0 →
let rs´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR EDX :: IR EAX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) in
∃ f´ m0´ r_,
lasm_step (vmptrld ↦ vmptrld_function) (eptinit (Hmwd:= Hmwd) (Hmem:= Hmem)) vmptrld 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)))
(Pregmap.get l r_)).
Proof.
generalize max_unsigned_val; intro muval.
intros. destruct H3 as [Hikern Hihost].
destruct m0 as [m0 d].
lift_unfold.
caseEq(Mem.alloc m0 0 16).
intros m1 b1 HALC.
exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
intros Hstencil_matches.
assert (Hsymbol: Genv.find_symbol ge VMCS_LOC = Some b0).
{
inv Hstencil_matches.
congruence.
}
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 H2.
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 8 Freeable).
{
eapply HV; auto; simpl; try omega.
unfold Z.divide.
∃ 2; 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 12 Freeable).
{
eapply Mem.store_valid_access_1; eauto.
eapply HV; auto; simpl; try omega.
unfold Z.divide.
∃ 3; 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.
∃ 0; omega.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HV3; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (Vptr b0 (Int.repr (CPU_ID d × 4096))) HV3) as [m4 HST3].
assert (HV4: Mem.valid_access m4 Mint32 b1 4 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.
∃ 1; omega.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HV4; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (Vint Int.zero) HV4) as [m5 HST4].
assert (HV5: Mem.range_perm m5 b1 0 16 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 vmptrld_function)).
{
assert (Hmodule: get_module_function vmptrld (vmptrld ↦ vmptrld_function) = OK (Some vmptrld_function)) by
reflexivity.
assert (HInternal: make_internal vmptrld_function = OK (AST.Internal vmptrld_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].
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 8))) with 8.
change (Int.unsigned (Int.add Int.zero (Int.repr 12))) with 12.
unfold set; simpl.
rewrite HALC. simpl.
rewrite HST1. simpl.
rewrite HST2.
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.
unfold set; simpl.
unfold lift; simpl.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST2); trivial.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST1); trivial.
inv H3; assumption.
Lregset_simpl_tac.
intro contra; discriminate contra.
Lregset_simpl_tac.
intro contra; discriminate contra.
Lregset_simpl_tac.
Require Import VCGen.
one_step_forward´.
inv Hhigh.
discharge_cmp.
one_step_forward´.
unfold Int.mul.
unfold symbol_offset.
rewrite Hsymbol.
discharge_cmp.
rewrite Z.add_0_r.
Lregset_simpl_tac.
one_step_forward´.
{
accessors_simpl.
rewrite Hikern, Hihost.
change (Int.unsigned (Int.add Int.zero (Int.add Int.zero (Int.repr 0)))) with 0.
rewrite HST3.
reflexivity.
}
Lregset_simpl_tac.
one_step_forward´.
Lregset_simpl_tac.
one_step_forward´.
{
accessors_simpl.
rewrite Hikern, Hihost.
change (Int.unsigned (Int.add Int.zero (Int.add Int.zero (Int.repr 4)))) with 4.
rewrite HST4.
reflexivity.
}
Lregset_simpl_tac.
one_step_forward´.
Lregset_simpl_tac.
one_step_forward´.
{
lift_trivial.
inv H2.
change (Int.unsigned (Int.add Int.zero (Int.repr 8))) with 8.
change (Int.unsigned (Int.add Int.zero (Int.repr 12))) with 12.
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 H2. 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 H2.
rewrite (Mem.alloc_result _ _ _ _ _ HALC) in p.
xomega. inv H2.
}
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 Lregset_fold; simpl.
intros reg.
repeat (rewrite Pregmap.gsspec).
simpl_destruct_reg.
exploit reg_false; try eassumption.
intros HF. inv HF.
Qed.
Lemma vmptrld_code_correct:
asm_spec_le (vmptrld ↦ vmptr_ld_spec_low)
(〚vmptrld ↦ vmptrld_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 vmptrld_spec; eauto 2.
intros (f´ & m0´ & r_ & Hstep & Hincr & Hinject & Hnb & Hv).
refine_split´; try eassumption; try reflexivity.
esplit; reflexivity.
Qed.
End VMPTR_LD.
Section RDMSR.
Lemma rdmsr_spec:
∀ ge (s: stencil) (rs rs´: regset) b (m0: mwd LDATAOps) sig i,
find_symbol s rdmsr = Some b →
make_globalenv s (rdmsr ↦ rdmsr_function) eptinit = ret ge →
rs PC = Vptr b Int.zero →
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 (rdmsr ↦ rdmsr_function) (eptinit (Hmwd:= Hmwd) (Hmem:= Hmem)) rdmsr 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´#EAX<- Vzero#EDX <- Vzero#PC <- (rs#RA)))
(Pregmap.get l r_)).
Proof.
intros.
destruct m0 as [m0 d].
lift_unfold.
caseEq(Mem.alloc m0 0 8).
intros m1 b1 HALC.
exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
intros Hstencil_matches.
assert (Hblock: Ple (Genv.genv_next ge) b1 ∧ Plt b1 (Mem.nextblock m1)).
{
erewrite Mem.nextblock_alloc; eauto.
apply Mem.alloc_result in HALC.
rewrite HALC. inv H2.
inv inv_inject_neutral.
inv Hstencil_matches.
rewrite stencil_matches_genv_next.
lift_unfold.
split; xomega.
}
specialize (Mem.valid_access_alloc_same _ _ _ _ _ HALC). intros HV.
assert (HV1: Mem.valid_access m1 Mint32 b1 0 Freeable).
{
eapply HV; auto; simpl; try omega.
unfold Z.divide.
∃ 0; omega.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HV1; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (rs ESP) HV1) as [m2 HST1].
assert (HV2: Mem.valid_access m2 Mint32 b1 4 Freeable).
{
eapply Mem.store_valid_access_1; eauto.
eapply HV; auto; simpl; try omega.
unfold Z.divide.
∃ 1; omega.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HV2; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (rs RA) HV2) as [m3 HST2].
assert (HV3: Mem.range_perm m3 b1 0 8 Cur Freeable).
{
unfold Mem.range_perm. intros.
repeat (eapply Mem.perm_store_1; [eassumption|]).
eapply Mem.perm_alloc_2; eauto.
}
destruct (Mem.range_perm_free _ _ _ _ HV3) as [m4 HFree].
assert(Hfun: Genv.find_funct_ptr ge b = Some (Internal rdmsr_function)).
{
assert (Hmodule: get_module_function rdmsr (rdmsr ↦ rdmsr_function) = OK (Some rdmsr_function)) by
reflexivity.
assert (HInternal: make_internal rdmsr_function = OK (AST.Internal rdmsr_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 H5 as [Hikern Hihost].
rewrite (Lregset_rewrite rs).
refine_split´; try eassumption; try reflexivity.
rewrite H1.
econstructor; eauto.
- one_step_forward´.
{
Lregset_simpl_tac.
lift_trivial.
change (Int.unsigned (Int.add Int.zero (Int.repr 0))) with 0.
change (Int.unsigned (Int.add Int.zero (Int.repr 4))) with 4.
unfold set; simpl.
rewrite HALC. simpl.
rewrite HST1. simpl.
rewrite HST2.
reflexivity.
}
Lregset_simpl_tac.
one_step_forward´.
{
accessors_simpl.
change (Int.add Int.zero (Int.repr 0)) with (Int.repr 0).
simpl in ×.
rewrite Hikern, Hihost.
inv H4. inv H5. inv H8. simpl in H7.
destruct (Val.add (rs ESP) (Vint (Int.repr 0))); try (inv H7; fail).
lift_unfold.
exploit Mem.load_alloc_other; eauto.
intros HLD.
pose proof (alloc_load_other _ _ _ _ _ _ _ _ _ HALC H7) as Hneq.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_other; eauto.
rewrite HLD.
reflexivity.
}
Lregset_simpl_tac.
one_step_forward´.
Lregset_simpl_tac.
one_step_forward´.
{
lift_trivial.
inv H2.
change (Int.unsigned (Int.add Int.zero (Int.repr 0))) with 0.
change (Int.unsigned (Int.add Int.zero (Int.repr 4))) with 4.
unfold set; simpl.
repeat(erewrite Mem.load_store_other; [|eassumption| simpl; right; right; omega]).
erewrite Mem.load_store_same; eauto 1.
erewrite register_type_load_result.
repeat(erewrite Mem.load_store_other; [|eassumption | simpl; right; right; omega]).
erewrite Mem.load_store_other; eauto 1.
erewrite Mem.load_store_same; eauto 1.
erewrite register_type_load_result.
rewrite HFree. reflexivity.
apply inv_reg_wt.
right; left. simpl. omega.
apply inv_reg_wt.
}
Lregset_simpl_tac.
one_step_forward´.
Lregset_simpl_tac.
econstructor.
reflexivity.
- inv H2. 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 H2.
rewrite (Mem.alloc_result _ _ _ _ _ HALC) in p.
xomega. inv H2.
}
assert (HINJ: Mem.inject (mem:= mwd LDATAOps) (Mem.flat_inj (Mem.nextblock (mem:= mwd LDATAOps) (m0, d)))
(m0, d) (m4, d)).
{
lift_unfold.
split; trivial.
eapply Mem.free_right_inject; eauto 1; [|intros; specialize (HFB b0 delta); apply HFB; trivial].
repeat (eapply Mem.store_outside_inject; [ | | eassumption]
; [|intros b2 delta; intros; specialize (HFB b2 delta); apply HFB; trivial]).
eapply Mem.alloc_right_inject; eauto 1.
eapply inv_mem_inject_neutral.
}
assumption.
- simpl. rewrite (Mem.nextblock_free _ _ _ _ _ HFree); trivial.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST2); trivial.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST1); trivial.
rewrite (Mem.nextblock_alloc _ _ _ _ _ HALC) ; eauto.
clear. abstract xomega.
- subst rs´0. Lregset_simpl_tac.
unfold Lregset_fold; simpl.
intros reg.
repeat (rewrite Pregmap.gsspec).
simpl_destruct_reg.
exploit reg_false; try eassumption.
intros HF. inv HF.
Qed.
Lemma rdmsr_code_correct:
asm_spec_le (rdmsr ↦ rdmsr_spec_low)
(〚rdmsr ↦ rdmsr_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 rdmsr_spec; eauto 2.
intros (f´ & m0´ & r_ & Hstep & Hincr & Hinject & Hnb & Hv).
refine_split´; try eassumption; try reflexivity.
esplit; reflexivity.
Qed.
End RDMSR.
Section WRMSR.
Lemma wrmsr_spec:
∀ ge (s: stencil) (rs rs´: regset) b (m0: mwd LDATAOps) sig v i0 i1,
find_symbol s wrmsr = Some b →
make_globalenv s (wrmsr ↦ wrmsr_function) eptinit = ret ge →
rs PC = Vptr b Int.zero →
asm_invariant (mem := mwd LDATAOps) s rs m0 →
sig = mksignature (AST.Tint::AST.Tlong::nil) (Some AST.Tint) cc_default →
extcall_arguments rs m0 sig (Vint v :: Vint i1 :: Vint i0 :: nil) →
kernel_mode (snd m0) →
let rs´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR ECX :: IR EDX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) in
∃ f´ m0´ r_,
lasm_step (wrmsr ↦ wrmsr_function) (eptinit (Hmwd:= Hmwd) (Hmem:= Hmem)) wrmsr 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 <- Vzero))
(Pregmap.get l r_)).
Proof.
intros.
destruct m0 as [m0 d].
lift_unfold.
caseEq(Mem.alloc m0 0 8).
intros m1 b1 HALC.
exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
intros Hstencil_matches.
assert (Hblock: Ple (Genv.genv_next ge) b1 ∧ Plt b1 (Mem.nextblock m1)).
{
erewrite Mem.nextblock_alloc; eauto.
apply Mem.alloc_result in HALC.
rewrite HALC. inv H2.
inv inv_inject_neutral.
inv Hstencil_matches.
rewrite stencil_matches_genv_next.
lift_unfold.
split; xomega.
}
specialize (Mem.valid_access_alloc_same _ _ _ _ _ HALC). intros HV.
assert (HV1: Mem.valid_access m1 Mint32 b1 0 Freeable).
{
eapply HV; auto; simpl; try omega.
unfold Z.divide.
∃ 0; omega.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HV1; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (rs ESP) HV1) as [m2 HST1].
assert (HV2: Mem.valid_access m2 Mint32 b1 4 Freeable).
{
eapply Mem.store_valid_access_1; eauto.
eapply HV; auto; simpl; try omega.
unfold Z.divide.
∃ 1; omega.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HV2; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (rs RA) HV2) as [m3 HST2].
assert (HV3: Mem.range_perm m3 b1 0 8 Cur Freeable).
{
unfold Mem.range_perm. intros.
repeat (eapply Mem.perm_store_1; [eassumption|]).
eapply Mem.perm_alloc_2; eauto.
}
destruct (Mem.range_perm_free _ _ _ _ HV3) as [m4 HFree].
assert(Hfun: Genv.find_funct_ptr ge b = Some (Internal wrmsr_function)).
{
assert (Hmodule: get_module_function wrmsr (wrmsr ↦ wrmsr_function) = OK (Some wrmsr_function)) by
reflexivity.
assert (HInternal: make_internal wrmsr_function = OK (AST.Internal wrmsr_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 H5 as [Hikern Hihost].
rewrite (Lregset_rewrite rs).
refine_split´; try eassumption; try reflexivity.
rewrite H1.
inv H4. inv H5. inv H9. inv H10.
inv H6. inv H7. inv H8. simpl in ×.
econstructor; eauto.
- one_step_forward´.
{
Lregset_simpl_tac.
lift_trivial.
change (Int.unsigned (Int.add Int.zero (Int.repr 0))) with 0.
change (Int.unsigned (Int.add Int.zero (Int.repr 4))) with 4.
unfold set; simpl.
rewrite HALC. simpl.
rewrite HST1. simpl.
rewrite HST2.
reflexivity.
}
Lregset_simpl_tac.
one_step_forward´.
{
accessors_simpl.
change (Int.add Int.zero (Int.repr 0)) with (Int.repr 0).
simpl in ×.
rewrite Hikern, Hihost.
destruct (Val.add (rs ESP) (Vint (Int.repr 0))); try (inv H7; fail).
lift_unfold.
exploit Mem.load_alloc_other; eauto.
intros HLD.
pose proof (alloc_load_other _ _ _ _ _ _ _ _ _ HALC H7) as Hneq.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_other; eauto.
rewrite HLD.
reflexivity.
}
Lregset_simpl_tac.
one_step_forward´.
{
accessors_simpl.
change (Int.add Int.zero (Int.repr 4)) with (Int.repr 4).
simpl in ×.
rewrite Hikern, Hihost.
destruct (Val.add (rs ESP) (Vint (Int.repr 4))); try (inv H9; fail).
lift_unfold.
exploit Mem.load_alloc_other; eauto.
intros HLD.
pose proof (alloc_load_other _ _ _ _ _ _ _ _ _ HALC H9) as Hneq.
erewrite Mem.load_store_other; eauto.
erewrite Mem.load_store_other; eauto.
rewrite HLD.
reflexivity.
}
Lregset_simpl_tac.
one_step_forward´.
{
accessors_simpl.
change (Int.add Int.zero (Int.repr 8)) with (Int.repr 8).
simpl in ×.
rewrite Hikern, Hihost.
destruct (Val.add (rs ESP) (Vint (Int.repr 8))); try (inv 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´.
Lregset_simpl_tac.
one_step_forward´.
Lregset_simpl_tac.
Lregset_simpl_tac.
one_step_forward´.
{
lift_trivial.
inv H2.
change (Int.unsigned (Int.add Int.zero (Int.repr 0))) with 0.
change (Int.unsigned (Int.add Int.zero (Int.repr 4))) with 4.
unfold set; simpl.
repeat(erewrite Mem.load_store_other; [|eassumption| simpl; right; right; omega]).
erewrite Mem.load_store_same; eauto 1.
erewrite register_type_load_result.
repeat(erewrite Mem.load_store_other; [|eassumption | simpl; right; right; omega]).
erewrite Mem.load_store_other; eauto 1.
erewrite Mem.load_store_same; eauto 1.
erewrite register_type_load_result.
rewrite HFree. reflexivity.
apply inv_reg_wt.
right; left. simpl. omega.
apply inv_reg_wt.
}
Lregset_simpl_tac.
one_step_forward´.
Lregset_simpl_tac.
econstructor.
reflexivity.
- inv H2. 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 H2.
rewrite (Mem.alloc_result _ _ _ _ _ HALC) in p.
xomega. inv H2.
}
assert (HINJ: Mem.inject (mem:= mwd LDATAOps) (Mem.flat_inj (Mem.nextblock (mem:= mwd LDATAOps) (m0, d)))
(m0, d) (m4, d)).
{
lift_unfold.
split; trivial.
eapply Mem.free_right_inject; eauto 1; [|intros; specialize (HFB b0 delta); apply HFB; trivial].
repeat (eapply Mem.store_outside_inject; [ | | eassumption]
; [|intros b2 delta; intros; specialize (HFB b2 delta); apply HFB; trivial]).
eapply Mem.alloc_right_inject; eauto 1.
eapply inv_mem_inject_neutral.
}
assumption.
- simpl. rewrite (Mem.nextblock_free _ _ _ _ _ HFree); trivial.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST2); trivial.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST1); trivial.
rewrite (Mem.nextblock_alloc _ _ _ _ _ HALC) ; eauto.
clear. abstract xomega.
- subst rs´0. Lregset_simpl_tac.
unfold Lregset_fold; simpl.
intros reg.
repeat (rewrite Pregmap.gsspec).
simpl_destruct_reg.
exploit reg_false; try eassumption.
intros HF. inv HF.
Qed.
Lemma wrmsr_code_correct:
asm_spec_le (wrmsr ↦ wrmsr_spec_low)
(〚wrmsr ↦ wrmsr_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 wrmsr_spec; eauto 2.
intros (f´ & m0´ & r_ & Hstep & Hincr & Hinject & Hnb & Hv).
refine_split´; try eassumption; try reflexivity.
esplit; reflexivity.
Qed.
End WRMSR.
Section RCR0.
Lemma rcr0_spec:
∀ ge (s: stencil) (rs rs´: regset) b (m0: mwd LDATAOps),
find_symbol s rcr0 = Some b →
make_globalenv s (rcr0 ↦ rcr0_function) eptinit = ret ge →
rs PC = Vptr b Int.zero →
asm_invariant (mem := mwd LDATAOps) s rs m0 →
∃ r_: regset,
lasm_step (rcr0 ↦ rcr0_function) (eptinit (Hmwd:= Hmwd) (Hmem:= Hmem)) rcr0 s rs m0 r_ m0
∧ (∀ l,
Val.lessdef (Pregmap.get l (rs#RA<- Vundef#PC <- (rs#RA)#EAX <- Vzero))
(Pregmap.get l r_)).
Proof.
intros.
exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
intros Hstencil_matches.
assert(Hfun: Genv.find_funct_ptr ge b = Some (Internal rcr0_function)).
{
assert (Hmodule: get_module_function rcr0 (rcr0 ↦ rcr0_function) = OK (Some rcr0_function)) by
reflexivity.
assert (HInternal: make_internal rcr0_function = OK (AST.Internal rcr0_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.
}
rewrite (Lregset_rewrite rs).
esplit; split.
econstructor; try eassumption.
rewrite H1.
one_step_forward´.
Lregset_simpl_tac.
one_step_forward´.
Lregset_simpl_tac.
econstructor.
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 rcr0_code_correct:
asm_spec_le (rcr0 ↦ rcr0_spec_low)
(〚rcr0 ↦ rcr0_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 rcr0_spec; eauto 2.
intros [r_[Hstep Hv]].
refine_split´; try eassumption; try reflexivity.
- inv H3. inv inv_inject_neutral.
eapply Mem.neutral_inject in inv_mem_inject_neutral.
assumption.
- esplit; reflexivity.
Qed.
End RCR0.
Section RCR3.
Lemma rcr3_spec:
∀ ge (s: stencil) (rs rs´: regset) b (m0: mwd LDATAOps),
find_symbol s rcr3 = Some b →
make_globalenv s (rcr3 ↦ rcr3_function) eptinit = ret ge →
rs PC = Vptr b Int.zero →
asm_invariant (mem := mwd LDATAOps) s rs m0 →
∃ r_: regset,
lasm_step (rcr3 ↦ rcr3_function) (eptinit (Hmwd:= Hmwd) (Hmem:= Hmem)) rcr3 s rs m0 r_ m0
∧ (∀ l,
Val.lessdef (Pregmap.get l (rs#RA<- Vundef#PC <- (rs#RA)#EAX <- Vzero))
(Pregmap.get l r_)).
Proof.
intros.
exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
intros Hstencil_matches.
assert(Hfun: Genv.find_funct_ptr ge b = Some (Internal rcr3_function)).
{
assert (Hmodule: get_module_function rcr3 (rcr3 ↦ rcr3_function) = OK (Some rcr3_function)) by
reflexivity.
assert (HInternal: make_internal rcr3_function = OK (AST.Internal rcr3_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.
}
rewrite (Lregset_rewrite rs).
esplit; split.
econstructor; try eassumption.
rewrite H1.
one_step_forward´.
Lregset_simpl_tac.
one_step_forward´.
Lregset_simpl_tac.
econstructor.
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 rcr3_code_correct:
asm_spec_le (rcr3 ↦ rcr3_spec_low)
(〚rcr3 ↦ rcr3_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 rcr3_spec; eauto 2.
intros [r_[Hstep Hv]].
refine_split´; try eassumption; try reflexivity.
- inv H3. inv inv_inject_neutral.
eapply Mem.neutral_inject in inv_mem_inject_neutral.
assumption.
- esplit; reflexivity.
Qed.
End RCR3.
Section RCR4.
Lemma rcr4_spec:
∀ ge (s: stencil) (rs rs´: regset) b (m0: mwd LDATAOps),
find_symbol s rcr4 = Some b →
make_globalenv s (rcr4 ↦ rcr4_function) eptinit = ret ge →
rs PC = Vptr b Int.zero →
asm_invariant (mem := mwd LDATAOps) s rs m0 →
∃ r_: regset,
lasm_step (rcr4 ↦ rcr4_function) (eptinit (Hmwd:= Hmwd) (Hmem:= Hmem)) rcr4 s rs m0 r_ m0
∧ (∀ l,
Val.lessdef (Pregmap.get l (rs#RA<- Vundef#PC <- (rs#RA)#EAX <- Vzero))
(Pregmap.get l r_)).
Proof.
intros.
exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
intros Hstencil_matches.
assert(Hfun: Genv.find_funct_ptr ge b = Some (Internal rcr4_function)).
{
assert (Hmodule: get_module_function rcr4 (rcr4 ↦ rcr4_function) = OK (Some rcr4_function)) by
reflexivity.
assert (HInternal: make_internal rcr4_function = OK (AST.Internal rcr4_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.
}
rewrite (Lregset_rewrite rs).
esplit; split.
econstructor; try eassumption.
rewrite H1.
one_step_forward´.
Lregset_simpl_tac.
one_step_forward´.
Lregset_simpl_tac.
econstructor.
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 rcr4_code_correct:
asm_spec_le (rcr4 ↦ rcr4_spec_low)
(〚rcr4 ↦ rcr4_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 rcr4_spec; eauto 2.
intros [r_[Hstep Hv]].
refine_split´; try eassumption; try reflexivity.
- inv H3. inv inv_inject_neutral.
eapply Mem.neutral_inject in inv_mem_inject_neutral.
assumption.
- esplit; reflexivity.
Qed.
End RCR4.
End WITHMEM.
End ASM_VERIFICATION.