Library mcertikos.trap.SysCallGenAsm2
*********************************************************************** * * * 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 TDispatch.
Require Import TSysCall.
Require Import SysCallGenAsmSource.
Require Import SysCallGenAsmData.
Require Import SysCallGenSpec.
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 (cdata_ops := pproc_data_ops) LDATA).
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModel}.
Context `{Hmwd: UseMemWithData mem}.
Context `{make_program_ops: !MakeProgramOps function Ctypes.type fundef unit}.
Context `{make_program_prf: !MakeProgram function Ctypes.type fundef unit}.
Lemma sys_sendtochan_pre_proof:
∀ ge (s: stencil) (rs: regset) m labd labd0 labd1 labd´ rs0 rs´ rs2 v0 v1 v2 v3 v5 v6
v8 v9 v10 v11 v12 v13 v14 v15 v16 v4 chanid vargs sg b rs_yield bs,
make_globalenv s (sys_sendtochan_pre ↦ sys_sendtochan_pre_function) tdispatch = ret ge →
trap_into_kernel_spec sys_sendtochan_pre s m rs labd labd0 vargs sg b
v0 v1 v2 v3 v4 v5 v6 chanid v8 v9 v10 v11 v12 v13 v14 v15 v16 →
trap_sendtochan_pre_spec labd0 = Some (labd1, Int.unsigned chanid) →
find_symbol s sys_sendtochan_post = Some bs →
rs_yield = (Pregmap.init Vundef)#ESP <- (Val.add (rs ESP) (Vint (Int.repr 28)))
#EDI <- (rs#EDI)#ESI <- (rs#ESI)
#EBX <- Vundef#EBP <- (rs#EBP)#RA <- (Vptr bs Int.zero) →
thread_sleep_spec labd1 rs_yield (Int.unsigned chanid) = Some (labd´, rs´) →
rs0 = (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)) →
rs2 = (rs0#ESP<- (rs´#ESP)#EDI <- (rs´#EDI)#ESI <- (rs´#ESI)#EBX <- (rs´#EBX)
#EBP <- (rs´#EBP)#PC <- (rs´#RA)) →
asm_invariant (mem := mwd LDATAOps) s rs (m, labd) →
high_level_invariant labd →
low_level_invariant (Mem.nextblock m) labd →
∃ r_: regset,
lasm_step (sys_sendtochan_pre ↦ sys_sendtochan_pre_function) (tdispatch (Hmwd:= Hmwd) (Hmem:= Hmem))
sys_sendtochan_pre s rs (m, labd) r_ (m, labd´)
∧ (∀ l,
Val.lessdef (Pregmap.get l rs2)
(Pregmap.get l r_)).
Proof.
intros. destruct H0 as [Hv [Hsg[Harg[Hsym[HPC[Hex [HESP HESP_STACK]]]]]]]. subst.
assert (HOS´: 0 ≤ 64 ≤ Int.max_unsigned) by rewrite_omega.
exploit Hexit; eauto.
intros [[b_exit [Hexit_symbol Hexit_fun]] prim_exit].
exploit Hsleep; eauto.
intros [[b_check [Hcheck_symbol Hcheck_fun]] prim_check].
exploit Hsendpre; eauto.
intros [[b_pre [Hpre_symbol Hpre_fun]] prim_pre].
exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
intros Hstencil_matches.
exploit Hsys_sendtochan_pre; eauto 2. intros Hfunct.
assert (Hblock: ∀ b0 o,
rs ESP = Vptr b0 o → Ple (Genv.genv_next ge) b0 ∧ Plt b0 (Mem.nextblock m)).
{
intros. exploit HESP_STACK; eauto.
inv Hstencil_matches.
rewrite stencil_matches_genv_next.
trivial.
}
clear HESP_STACK.
rewrite (Lregset_rewrite rs).
refine_split´; try eassumption.
rewrite HPC.
econstructor; eauto.
one_step_forward´.
Lregset_simpl_tac.
unfold symbol_offset. unfold fundef.
rewrite Hexit_symbol.
econstructor; eauto 1.
eapply (LAsm.exec_step_prim_call _ b_exit); eauto.
econstructor; eauto 1.
instantiate (4:= proc_exit_user).
change positive with ident in ×.
rewrite prim_exit.
refine_split´; try reflexivity.
econstructor; eauto 1.
refine_split´; try reflexivity; try eassumption.
simpl. econstructor; try eassumption; try reflexivity.
{
intros b1 o rsESP.
rewrite <- (stencil_matches_genv_next _ _ Hstencil_matches).
apply Hblock with o.
exact rsESP.
}
inv Harg.
constructor; eauto 1;
repeat match goal with
| [H0: extcall_arg _ _ _ _ |- extcall_arg _ _ _ _] ⇒ inv H0; econstructor; [reflexivity| eassumption]
| [H1: list_forall2 _ _ _ |- list_forall2 _ _ _] ⇒ inv H1; constructor
| H1: list_forall2 _ _ _ |- _ ⇒ inv H1
end.
inv Hstencil_matches. erewrite <- stencil_matches_symbols; eassumption.
Lregset_simpl_tac.
one_step_forward´.
Lregset_simpl_tac.
unfold symbol_offset. unfold fundef.
rewrite Hpre_symbol.
econstructor; eauto 1.
eapply (LAsm.exec_step_external _ b_pre); eauto 1.
econstructor; eauto 1.
econstructor; eauto 1.
red. red. red. red. red. red.
change positive with ident in ×.
rewrite prim_pre.
refine_split´; try reflexivity.
econstructor; eauto 1.
refine_split´; try reflexivity; try eassumption.
constructor_gen_sem_intro.
Lregset_simpl_tac.
discriminate.
Lregset_simpl_tac.
one_step_forward´.
unfold symbol_offset. unfold fundef.
pose proof Hstencil_matches as Hstencil_matches´.
inv Hstencil_matches. erewrite stencil_matches_symbols.
rewrite H2.
Lregset_simpl_tac.
one_step_forward´.
Lregset_simpl_tac.
one_step_forward´.
Lregset_simpl_tac.
unfold symbol_offset. unfold fundef.
rewrite Hcheck_symbol.
eapply star_one; eauto.
eapply (LAsm.exec_step_prim_call _ b_check); eauto 1.
econstructor; eauto 1.
instantiate (4:= thread_sleep).
change positive with ident in ×.
rewrite prim_check.
refine_split´; try reflexivity.
econstructor; eauto 1.
simpl.
assert (HUCTX: ∀ v r, ZtoPreg v = Some r →
Val.has_type (rs´ r) Tint
∧ val_inject (Mem.flat_inj (Mem.nextblock m))
(rs´ r) (rs´ r)).
{
eapply sys_sendtochan_pre_generate; eauto.
}
econstructor; try eassumption; try reflexivity.
inv Harg.
repeat lazymatch goal with
| H0: extcall_arg _ _ _ (Vint chanid) |- _ ⇒ fail
| _ ⇒ match goal with
| [H0: list_forall2 _ _ _ |- _ ] ⇒ inv H0
end
end.
econstructor; eauto.
inv H16. econstructor; eauto.
Lregset_simpl_tac.
simpl in H18. simpl.
destruct (rs ESP); try inv H18.
simpl. rewrite Int.add_zero. reflexivity.
constructor.
apply HUCTX.
apply HUCTX.
erewrite <- stencil_matches_symbols; eassumption.
reflexivity.
Lregset_simpl_tac.
simpl.
Lregset_simpl_tac.
intros reg.
unfold Lregset_fold; simpl.
repeat (rewrite Pregmap.gsspec).
simpl_destruct_reg.
exploit reg_false; try eassumption.
intros HF. inv HF.
Qed.
Require Import LAsmModuleSemSpec.
Lemma sys_sendtochan_pre_code_correct:
asm_spec_le (sys_sendtochan_pre ↦ sys_sendtochan_pre_spec_low)
(〚sys_sendtochan_pre ↦ sys_sendtochan_pre_function〛 tdispatch).
Proof.
eapply asm_sem_intro; try reflexivity.
intros. inv H.
eapply make_program_make_globalenv in H0.
exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
intros Hstencil_matches.
assert(Hfun: Genv.find_funct_ptr (Genv.globalenv p) b = Some (Internal sys_sendtochan_pre_function)).
{
assert (Hmodule: get_module_function sys_sendtochan_pre (sys_sendtochan_pre ↦ sys_sendtochan_pre_function)
= OK (Some sys_sendtochan_pre_function)) by
reflexivity.
assert (HInternal: make_internal sys_sendtochan_pre_function = OK (AST.Internal sys_sendtochan_pre_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.
destruct H1 as [_ [_[_[Hsym _]]]].
rewrite Hsym in Hsymbol. inv Hsymbol.
assumption.
}
exploit sys_sendtochan_pre_proof; eauto 2. intros HW. exploit HW; eauto 2.
intros [r_[Hstep Hv]].
assert (Hle: (Mem.nextblock m0 ≤ Mem.nextblock m0)%positive).
{
reflexivity.
}
refine_split´; try eassumption; try reflexivity.
- inv H8. inv inv_inject_neutral.
lift_unfold. split; try reflexivity.
eapply Mem.neutral_inject. assumption.
- esplit; reflexivity.
Qed.
Lemma sys_yield_spec:
∀ ge (s: stencil) (rs: regset) m labd labd0 labd´ rs0 rs´ rs2 v0 v1 v2 v3 v5 v6
v8 v9 v10 v11 v12 v13 v14 v15 v16 v4 v7 vargs sg b rs_yield bs,
make_globalenv s (sys_yield ↦ sys_yield_function) tdispatch = ret ge →
trap_into_kernel_spec sys_yield s m rs labd labd0 vargs sg b
v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 →
find_symbol s proc_start_user = Some bs →
rs_yield = (Pregmap.init Vundef) #ESP <- (rs#ESP) #EDI <- (rs#EDI) #ESI <- (rs#ESI)
#EBX <- Vundef #EBP <- (rs#EBP) #RA <- (Vptr bs Int.zero)→
thread_yield_spec labd0 rs_yield = Some (labd´, rs´) →
rs0 = (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)) →
rs2 = (rs0#ESP<- (rs´#ESP)#EDI <- (rs´#EDI)#ESI <- (rs´#ESI)#EBX <- (rs´#EBX)
#EBP <- (rs´#EBP)#PC <- (rs´#RA)) →
asm_invariant (mem := mwd LDATAOps) s rs (m, labd) →
high_level_invariant labd →
low_level_invariant (Mem.nextblock m) labd →
∃ r_: regset,
lasm_step (sys_yield ↦ sys_yield_function) (tdispatch (Hmwd:= Hmwd) (Hmem:= Hmem))
sys_yield s rs (m, labd) r_ (m, labd´)
∧ (∀ l,
Val.lessdef (Pregmap.get l rs2)
(Pregmap.get l r_)).
Proof.
intros. destruct H0 as [Hv [Hsg[Harg[Hsym[HPC[Hex [HESP HESP_STACK]]]]]]]. subst.
assert (HOS´: 0 ≤ 64 ≤ Int.max_unsigned) by rewrite_omega.
exploit Hexit; eauto.
intros [[b_exit [Hexit_symbol Hexit_fun]] prim_exit].
exploit Hyield; eauto.
intros [[b_check [Hcheck_symbol Hcheck_fun]] prim_check].
exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
intros Hstencil_matches.
exploit Hsys_yield; eauto 2. intros Hfunct.
assert (Hblock: ∀ b0 o,
rs ESP = Vptr b0 o → Ple (Genv.genv_next ge) b0 ∧ Plt b0 (Mem.nextblock m)).
{
intros. exploit HESP_STACK; eauto.
inv Hstencil_matches.
rewrite stencil_matches_genv_next.
trivial.
}
clear HESP_STACK.
rewrite (Lregset_rewrite rs).
refine_split´; try eassumption.
rewrite HPC.
econstructor; eauto.
one_step_forward´.
Lregset_simpl_tac.
unfold symbol_offset. unfold fundef.
rewrite Hexit_symbol.
econstructor; eauto 1.
eapply (LAsm.exec_step_prim_call _ b_exit); eauto.
econstructor; eauto 1.
instantiate (4:= proc_exit_user).
change positive with ident in ×.
rewrite prim_exit.
refine_split´; try reflexivity.
econstructor; eauto 1.
refine_split´; try reflexivity; try eassumption.
simpl. econstructor; try eassumption; try reflexivity.
{
intros b1 o rsESP.
rewrite <- (stencil_matches_genv_next _ _ Hstencil_matches).
apply Hblock with o.
exact rsESP.
}
inv Harg.
constructor; eauto 1;
repeat match goal with
| [H0: extcall_arg _ _ _ _ |- extcall_arg _ _ _ _] ⇒ inv H0; econstructor; [reflexivity| eassumption]
| [H1: list_forall2 _ _ _ |- list_forall2 _ _ _] ⇒ inv H1; constructor
| H1: list_forall2 _ _ _ |- _ ⇒ inv H1
end.
inv Hstencil_matches. erewrite <- stencil_matches_symbols; eassumption.
Lregset_simpl_tac.
one_step_forward´.
unfold symbol_offset. unfold fundef.
pose proof Hstencil_matches as Hstencil_matches´.
inv Hstencil_matches. erewrite stencil_matches_symbols.
rewrite H1.
Lregset_simpl_tac´ 2.
one_step_forward´.
Lregset_simpl_tac.
unfold symbol_offset. unfold fundef.
rewrite Hcheck_symbol.
eapply star_one; eauto.
eapply (LAsm.exec_step_prim_call _ b_check); eauto 1.
econstructor; eauto 1.
instantiate (4:= thread_yield).
change positive with ident in ×.
rewrite prim_check.
refine_split´; try reflexivity.
econstructor; eauto 1.
simpl.
assert (HUCTX: ∀ v r, ZtoPreg v = Some r →
Val.has_type (rs´ r) Tint
∧ val_inject (Mem.flat_inj (Mem.nextblock m))
(rs´ r) (rs´ r)).
{
eapply sys_yield_generate; eauto.
}
econstructor; try eassumption; try reflexivity.
eapply HUCTX.
eapply HUCTX.
erewrite <- stencil_matches_symbols; eassumption.
reflexivity.
Lregset_simpl_tac.
simpl.
Lregset_simpl_tac.
intros reg.
unfold Lregset_fold; simpl.
repeat (rewrite Pregmap.gsspec).
simpl_destruct_reg.
exploit reg_false; try eassumption.
intros HF. inv HF.
Qed.
Lemma sys_yield_code_correct:
asm_spec_le (sys_yield ↦ sys_yield_spec_low)
(〚sys_yield ↦ sys_yield_function〛 tdispatch).
Proof.
eapply asm_sem_intro; try reflexivity.
intros. inv H.
eapply make_program_make_globalenv in H0.
exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
intros Hstencil_matches.
assert(Hfun: Genv.find_funct_ptr (Genv.globalenv p) b = Some (Internal sys_yield_function)).
{
assert (Hmodule: get_module_function sys_yield (sys_yield ↦ sys_yield_function) = OK (Some sys_yield_function)) by
reflexivity.
assert (HInternal: make_internal sys_yield_function = OK (AST.Internal sys_yield_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.
destruct H1 as [_ [_[_[Hsym _]]]].
rewrite Hsym in Hsymbol. inv Hsymbol.
assumption.
}
exploit sys_yield_spec; eauto 2. intros HW. exploit HW; eauto 2.
intros [r_[Hstep Hv]].
assert (Hle: (Mem.nextblock m0 ≤ Mem.nextblock m0)%positive).
{
reflexivity.
}
refine_split´; try eassumption; try reflexivity.
- inv H7. inv inv_inject_neutral.
lift_unfold. split; try reflexivity.
eapply Mem.neutral_inject. assumption.
- esplit; reflexivity.
Qed.
Lemma sys_run_vm_proof:
∀ ge (s: stencil) (rs: regset) m labd labd0 labd´ rs01 rs0 rs´ rs2 v0 v1 v2 v3 v5 v6
v8 v9 v10 v11 v12 v13 v14 v15 v16 v4 v7 vargs sg b,
make_globalenv s (sys_run_vm ↦ sys_run_vm_function) tdispatch = ret ge →
trap_into_kernel_spec sys_run_vm s m rs labd labd0 vargs sg b
v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 →
rs01 = (Pregmap.init Vundef) #EDI <- (rs EDI) #EBP <- (rs EBP) →
vm_run_spec rs01 labd0 = Some (labd´, rs´) →
rs0 = (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) →
rs2 = (rs0#EAX<- (rs´#EAX)#EBX <- (rs´#EBX)#EDX <- (rs´#EDX)
#ESI <- (rs´#ESI)#EDI <- (rs´#EDI)#EBP <- (rs´#EBP)
#PC <- (rs´#RA)) →
asm_invariant (mem := mwd LDATAOps) s rs (m, labd) →
high_level_invariant labd →
low_level_invariant (Mem.nextblock m) labd →
∃ r_: regset,
lasm_step (sys_run_vm ↦ sys_run_vm_function) (tdispatch (Hmwd:= Hmwd) (Hmem:= Hmem))
sys_run_vm s rs (m, labd) r_ (m, labd´)
∧ (∀ l,
Val.lessdef (Pregmap.get l rs2)
(Pregmap.get l r_)).
Proof.
intros. destruct H0 as [Hv [Hsg[Harg[Hsym[HPC[Hex [HESP HESP_STACK]]]]]]]. subst.
exploit Hexit; eauto.
intros [[b_exit [Hexit_symbol Hexit_fun]] prim_exit].
exploit Hrun_vm; eauto.
intros [[b_check [Hcheck_symbol Hcheck_fun]] prim_check].
exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
intros Hstencil_matches.
exploit Hsys_run_vm; eauto 2. intros Hfunct.
assert (Hblock: ∀ b0 o,
rs ESP = Vptr b0 o → Ple (Genv.genv_next ge) b0 ∧ Plt b0 (Mem.nextblock m)).
{
intros. exploit HESP_STACK; eauto.
inv Hstencil_matches.
rewrite stencil_matches_genv_next.
trivial.
}
clear HESP_STACK.
rewrite (Lregset_rewrite rs).
refine_split´; try eassumption.
rewrite HPC.
econstructor; eauto.
one_step_forward´.
Lregset_simpl_tac.
unfold symbol_offset. unfold fundef.
rewrite Hexit_symbol.
econstructor; eauto 1.
eapply (LAsm.exec_step_prim_call _ b_exit); eauto.
econstructor; eauto 1.
instantiate (4:= proc_exit_user).
change positive with ident in ×.
rewrite prim_exit.
refine_split´; try reflexivity.
econstructor; eauto 1.
refine_split´; try reflexivity; try eassumption.
simpl. econstructor; try eassumption; try reflexivity.
{
intros b1 o rsESP.
rewrite <- (stencil_matches_genv_next _ _ Hstencil_matches).
apply Hblock with o.
exact rsESP.
}
inv Harg.
constructor; eauto 1;
repeat match goal with
| [H0: extcall_arg _ _ _ _ |- extcall_arg _ _ _ _] ⇒ inv H0; econstructor; [reflexivity| eassumption]
| [H1: list_forall2 _ _ _ |- list_forall2 _ _ _] ⇒ inv H1; constructor
| H1: list_forall2 _ _ _ |- _ ⇒ inv H1
end.
inv Hstencil_matches. erewrite <- stencil_matches_symbols; eassumption.
Lregset_simpl_tac.
one_step_forward´.
Lregset_simpl_tac.
unfold symbol_offset. unfold fundef.
rewrite Hcheck_symbol.
eapply star_one; eauto.
eapply (LAsm.exec_step_prim_call _ b_check); eauto 1.
econstructor; eauto 1.
instantiate (4:= vmx_run_vm).
change positive with ident in ×.
rewrite prim_check.
refine_split´; try reflexivity.
econstructor; eauto 1.
simpl.
assert (HUCTX: ∀ r, Val.has_type (rs´ r) Tint
∧ val_inject (Mem.flat_inj (Mem.nextblock m))
(rs´ r) (rs´ r)).
{
eapply sys_run_vm_generate; eauto.
}
econstructor; try eassumption; try reflexivity;
try eapply HUCTX.
erewrite <- stencil_matches_symbols; eassumption.
Lregset_simpl_tac.
intros. specialize (Hblock _ _ H0).
erewrite <- stencil_matches_genv_next; eassumption.
reflexivity.
Lregset_simpl_tac.
simpl.
Lregset_simpl_tac.
intros reg.
unfold Lregset_fold; simpl.
repeat (rewrite Pregmap.gsspec).
simpl_destruct_reg.
exploit reg_false; try eassumption.
intros HF. inv HF.
Qed.
Lemma sys_run_vm_code_correct:
asm_spec_le (sys_run_vm ↦ sys_run_vm_spec_low)
(〚sys_run_vm ↦ sys_run_vm_function〛 tdispatch).
Proof.
eapply asm_sem_intro; try reflexivity.
intros. inv H.
eapply make_program_make_globalenv in H0.
exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
intros Hstencil_matches.
assert(Hfun: Genv.find_funct_ptr (Genv.globalenv p) b = Some (Internal sys_run_vm_function)).
{
assert (Hmodule: get_module_function sys_run_vm (sys_run_vm ↦ sys_run_vm_function) = OK (Some sys_run_vm_function)) by
reflexivity.
assert (HInternal: make_internal sys_run_vm_function = OK (AST.Internal sys_run_vm_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.
destruct H1 as [_ [_[_[Hsym _]]]].
rewrite Hsym in Hsymbol. inv Hsymbol.
assumption.
}
exploit sys_run_vm_proof; eauto 2. intros HW. exploit HW; eauto 2.
intros [r_[Hstep Hv]].
assert (Hle: (Mem.nextblock m0 ≤ Mem.nextblock m0)%positive).
{
reflexivity.
}
refine_split´; try eassumption; try reflexivity.
- inv H6. inv inv_inject_neutral.
lift_unfold. split; try reflexivity.
eapply Mem.neutral_inject. assumption.
- esplit; reflexivity.
Qed.
Ltac accessors_simpl:=
match goal with
| |- exec_storeex _ _ _ _ _ _ _ = _ ⇒
unfold exec_storeex, LoadStoreSem2.exec_storeex2;
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, LoadStoreSem2.exec_loadex2;
simpl; Lregset_simpl_tac;
match goal with
| |- context[Asm.exec_load _ _ _ _ _ _ ] ⇒
unfold Asm.exec_load; simpl;
Lregset_simpl_tac; lift_trivial
end
end.
Lemma pgf_handler_spec:
∀ ge (s: stencil) (rs: regset) m labd labd0 labd1 labd´ rs0 vadr rs´ v0 v1 v2 v3 v5 v6
v8 v9 v10 v11 v12 v13 v14 v15 v16 v4 v7 vargs sg b,
make_globalenv s (pgf_handler ↦ pgf_handler_function) tdispatch = ret ge →
syscall_spec pgf_handler s m rs rs´ rs0 labd labd0 labd1 labd´ vargs sg b
v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 →
vadr = fst (ti labd0) →
ptfault_resv_spec (Int.unsigned vadr) labd0 = Some labd1 →
asm_invariant (mem := mwd LDATAOps) s rs (m, labd) →
low_level_invariant (Mem.nextblock m) labd →
∃ f´ m0´ r_,
lasm_step (pgf_handler ↦ pgf_handler_function) (tdispatch (Hmwd:= Hmwd) (Hmem:= Hmem))
pgf_handler s rs
(m, labd) r_ (m0´, labd´)
∧ inject_incr (Mem.flat_inj (Mem.nextblock m)) f´
∧ Memtype.Mem.inject f´ m m0´
∧ (Mem.nextblock m ≤ Mem.nextblock m0´)%positive
∧ (∀ l,
Val.lessdef (Pregmap.get l rs0)
(Pregmap.get l r_)).
Proof.
intros.
caseEq(Mem.alloc m 0 12).
intros m1 b0 HALC.
exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
intros Hstencil_matches.
assert (Hblock: Ple (Genv.genv_next ge) b0 ∧ Plt b0 (Mem.nextblock m1)).
{
erewrite Mem.nextblock_alloc; eauto.
apply Mem.alloc_result in HALC.
rewrite HALC.
inv H3. inv inv_inject_neutral.
inv Hstencil_matches.
rewrite stencil_matches_genv_next.
lift_unfold.
split; xomega.
}
destruct H0 as [Hk[Hst [Hr _]]]. subst.
destruct Hk as [Hv [Hsg[Harg[Hsym[HPC[Hex [HESP HESP_STACK]]]]]]]. subst.
assert (HOS´: 0 ≤ 64 ≤ Int.max_unsigned) by rewrite_omega.
exploit Hstart; eauto.
intros [[b_start [Hstart_symbol Hstart_fun]] prim_start].
exploit Hexit; eauto.
intros [[b_exit [Hexit_symbol Hexit_fun]] prim_exit].
exploit Hget; eauto.
intros [[b_check [Hcheck_symbol Hcheck_fun]] prim_check].
exploit Hpgfr; eauto.
intros [[b_pgfr [Hpgfr_symbol Hpgfr_fun]] prim_pgfr].
specialize (Mem.valid_access_alloc_same _ _ _ _ _ HALC). intros.
assert (HV1: Mem.valid_access m1 Mint32 b0 4 Freeable).
{
eapply H0; auto; simpl; try omega.
apply Z.divide_refl.
}
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 b0 8 Freeable).
{
eapply Mem.store_valid_access_1; eauto.
eapply H0; 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 _ _ _ _ Vundef HV2) as [m3 HST2].
assert (HV3: Mem.valid_access m3 Mint32 b0 0 Freeable).
{
eapply Mem.store_valid_access_1; eauto.
eapply Mem.store_valid_access_1; eauto.
eapply H0; auto; simpl; try omega.
apply Zdivide_0.
}
eapply Mem.valid_access_implies with (p2:= Writable) in HV3; [|constructor].
destruct (Mem.valid_access_store _ _ _ _ (Vint (fst (ti labd0))) HV3) as [m4 HST3].
assert(Hnextblock4: Mem.nextblock m4 = Mem.nextblock m1).
{
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST3); trivial.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST2); trivial.
rewrite (Mem.nextblock_store _ _ _ _ _ _ HST1); trivial.
}
assert (HV4: Mem.range_perm m4 b0 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 (HUCTX: ikern labd0 = true
∧ ihost labd0 = true
/\(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i rs´) in
Val.has_type v Tint
∧ val_inject (Mem.flat_inj (Mem.nextblock m5)) v v)).
{
eapply pgf_handler_generate; eauto.
intros. subst v.
inv_proc; try (split; constructor).
rewrite ZMap.gi.
split; constructor.
}
destruct HUCTX as [ik[ih HUCTX]].
exploit Hpgf_handler; eauto 2. intros Hfunct.
rewrite (Lregset_rewrite rs).
refine_split´; try eassumption.
rewrite HPC.
econstructor; eauto.
one_step_forward´.
Lregset_simpl_tac.
unfold symbol_offset. unfold fundef.
rewrite Hexit_symbol.
econstructor; eauto 1.
eapply (LAsm.exec_step_prim_call _ b_exit); eauto.
econstructor; eauto 1.
instantiate (4:= proc_exit_user).
change positive with ident in ×.
rewrite prim_exit.
refine_split´; try reflexivity.
econstructor; eauto 1.
refine_split´; try reflexivity; try eassumption.
simpl. econstructor; try eassumption; try reflexivity.
inv Harg.
constructor; eauto 1;
repeat match goal with
| [H0: extcall_arg _ _ _ _ |- extcall_arg _ _ _ _] ⇒ inv H0; econstructor; [reflexivity| eassumption]
| [H1: list_forall2 _ _ _ |- list_forall2 _ _ _] ⇒ inv H1; constructor
| H1: list_forall2 _ _ _ |- _ ⇒ inv H1
end.
inv Hstencil_matches. erewrite <- stencil_matches_symbols; eassumption.
Lregset_simpl_tac.
one_step_forward´.
Lregset_simpl_tac.
lift_trivial.
unfold set; simpl.
rewrite HALC. simpl.
change (Int.unsigned (Int.add Int.zero (Int.repr 8))) with 8.
change (Int.unsigned (Int.add Int.zero (Int.repr 4))) with 4.
rewrite HST1. simpl.
rewrite HST2.
reflexivity.
Lregset_simpl_tac.
one_step_forward´.
unfold symbol_offset. unfold fundef.
rewrite Hcheck_symbol.
Lregset_simpl_tac.
econstructor; eauto.
eapply (LAsm.exec_step_prim_call _ b_check); eauto 1.
econstructor; eauto 1.
instantiate (4:= trap_get).
change positive with ident in ×.
rewrite prim_check.
refine_split´; try reflexivity.
econstructor; eauto. simpl.
econstructor; eauto.
Lregset_simpl_tac.
unfold trap_info_get_spec.
one_step_forward´.
unfold exec_storeex, LoadStoreSem3.exec_storeex3.
simpl; Lregset_simpl_tac. rewrite ik, ih.
unfold Asm.exec_store; simpl.
Lregset_simpl_tac. lift_trivial.
change (Int.unsigned (Int.add Int.zero (Int.add Int.zero Int.zero))) with 0.
rewrite HST3. reflexivity.
unfold set; simpl.
one_step_forward´.
unfold symbol_offset. unfold fundef.
rewrite Hpgfr_symbol.
Lregset_simpl_tac.
econstructor; eauto.
eapply (LAsm.exec_step_external _ b_pgfr); eauto 1.
econstructor; eauto.
econstructor; eauto. simpl; lift_trivial.
erewrite Mem.load_store_same; eauto.
constructor; trivial.
econstructor; eauto 1.
red. red. red. red. red. red.
change positive with ident in ×.
rewrite prim_pgfr.
refine_split´; try reflexivity.
econstructor; eauto 1.
refine_split´; try reflexivity; try eassumption.
constructor_gen_sem_intro.
Lregset_simpl_tac.
lift_trivial.
intros. inv H1.
rewrite Hnextblock4; assumption.
discriminate.
discriminate.
Lregset_simpl_tac.
one_step_forward´.
lift_trivial.
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.
erewrite Mem.load_store_other; eauto; simpl.
erewrite Mem.load_store_same; eauto.
erewrite Mem.load_store_other; eauto; simpl.
erewrite Mem.load_store_other; eauto; simpl.
erewrite Mem.load_store_same; eauto.
erewrite register_type_load_result.
rewrite HFree. reflexivity.
inv H3.
apply inv_reg_wt.
right. left. omega.
right. right. omega.
right. right. omega.
Lregset_simpl_tac.
one_step_forward´.
Lregset_simpl_tac.
unfold symbol_offset. unfold fundef.
rewrite Hstart_symbol.
eapply star_one; eauto.
eapply (LAsm.exec_step_prim_call _ b_start); eauto 1.
econstructor; eauto 1.
instantiate (4:= proc_start_user).
change positive with ident in ×.
rewrite prim_start.
refine_split´; try reflexivity.
econstructor; eauto 1.
refine_split´; try reflexivity; try eassumption.
simpl.
econstructor; try eassumption; try reflexivity.
eapply HUCTX.
eapply HUCTX.
inv Hstencil_matches. erewrite <- stencil_matches_symbols; eassumption.
reflexivity.
reflexivity.
assert (HFB: ∀ b1 delta, Mem.flat_inj (Mem.nextblock m) b1 ≠ Some (b0, delta)).
{
intros. unfold Mem.flat_inj.
red; intros.
destruct (plt b1 (Mem.nextblock m)). inv H1.
rewrite (Mem.alloc_result _ _ _ _ _ HALC) in p.
xomega. inv H1.
}
eapply Mem.free_right_inject; eauto 1; [|intros; specialize (HFB b1 delta); apply HFB; trivial].
repeat (eapply Mem.store_outside_inject; [ | | eassumption]
; [|intros b1 delta; intros; specialize (HFB b1 delta); apply HFB; trivial]).
eapply Mem.alloc_right_inject; eauto 1.
inv H3. inv inv_inject_neutral.
apply Mem.neutral_inject; trivial.
rewrite (Mem.nextblock_free _ _ _ _ _ HFree); trivial.
rewrite Hnextblock4.
rewrite (Mem.nextblock_alloc _ _ _ _ _ HALC); eauto.
clear. abstract xomega.
Lregset_simpl_tac.
simpl.
Lregset_simpl_tac.
intros reg.
unfold Lregset_fold; simpl.
repeat (rewrite Pregmap.gsspec).
simpl_destruct_reg.
constructor.
Qed.
Lemma pgf_handler_code_correct:
asm_spec_le (pgf_handler ↦ pagefault_handler_spec_low)
(〚pgf_handler ↦ pgf_handler_function〛 tdispatch).
Proof.
eapply asm_sem_intro; try reflexivity.
intros. inv H.
eapply make_program_make_globalenv in H0.
exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
intros Hstencil_matches.
assert(Hfun: Genv.find_funct_ptr (Genv.globalenv p) b = Some (Internal pgf_handler_function)).
{
assert (Hmodule: get_module_function pgf_handler (pgf_handler ↦ pgf_handler_function) = OK (Some pgf_handler_function)) by
reflexivity.
assert (HInternal: make_internal pgf_handler_function = OK (AST.Internal pgf_handler_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.
destruct H1 as [Hk _]. subst.
destruct Hk as [_ [_[_[Hsym _]]]].
rewrite Hsym in Hsymbol. inv Hsymbol.
assumption.
}
exploit pgf_handler_spec; eauto 2. intros HW. exploit HW; eauto 2.
intros (f´ & m0´ & r_ & Hstep & Hincr & Hv & Hnext & HV).
refine_split´; try eassumption; try reflexivity.
- lift_unfold. split; [assumption| reflexivity].
- esplit; reflexivity.
Qed.
End WITHMEM.
End ASM_VERIFICATION.