Library mcertikos.trap.SysCallGen
Require Import Coqlib.
Require Import Errors.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Op.
Require Import Asm.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Values.
Require Import Memory.
Require Import Maps.
Require Import CommonTactic.
Require Import AuxLemma.
Require Import FlatMemory.
Require Import AuxStateDataType.
Require Import Constant.
Require Import GlobIdent.
Require Import RealParams.
Require Import AsmImplLemma.
Require Import GenSem.
Require Import RefinementTactic.
Require Import PrimSemantics.
Require Import XOmega.
Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import compcert.cfrontend.Ctypes.
Require Import LayerCalculusLemma.
Require Import AbstractDataType.
Require Import LAsmModuleSemAux.
Require Import LoadStoreSem3high.
Require Import GlobalOracleProp.
Require Import SingleOracle.
Require Import ObjTMINTELVIRT.
Require Import ObjTMVMXINIT.
Require Import TSysCall.
Require Export DispatchGen.
Require Import SysCallGenSpec.
Require Import Errors.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Op.
Require Import Asm.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Values.
Require Import Memory.
Require Import Maps.
Require Import CommonTactic.
Require Import AuxLemma.
Require Import FlatMemory.
Require Import AuxStateDataType.
Require Import Constant.
Require Import GlobIdent.
Require Import RealParams.
Require Import AsmImplLemma.
Require Import GenSem.
Require Import RefinementTactic.
Require Import PrimSemantics.
Require Import XOmega.
Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import compcert.cfrontend.Ctypes.
Require Import LayerCalculusLemma.
Require Import AbstractDataType.
Require Import LAsmModuleSemAux.
Require Import LoadStoreSem3high.
Require Import GlobalOracleProp.
Require Import SingleOracle.
Require Import ObjTMINTELVIRT.
Require Import ObjTMVMXINIT.
Require Import TSysCall.
Require Export DispatchGen.
Require Import SysCallGenSpec.
Section Refinement.
Local Open Scope string_scope.
Local Open Scope error_monad_scope.
Local Open Scope Z_scope.
Context `{single_oracle_prop: SingleOracleProp}.
Context `{real_params : RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Notation HDATA := RData.
Notation LDATA := RData.
Notation HDATAOps := (cdata (cdata_ops := pipcintro_data_ops) HDATA).
Notation LDATAOps := (cdata (cdata_ops := pipcintro_data_ops) LDATA).
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Section PRIM_EXISTS.
Lemma trap_into_kernel_exists:
∀ s hm lm habd habd0 labd (rs1 rs2 :regset) v0 v1 v2 v3 v5 v6
v8 v9 v10 v11 v12 v13 v14 v15 v16 v4 v7 vargs id sg b f,
trap_into_kernel_spec id s hm rs1 habd habd0 vargs sg b v0 v1 v2
v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 →
Mem.inject f hm lm →
relate_AbData s f habd labd →
high_level_invariant habd →
(∀ reg,
val_inject f (Pregmap.get reg rs1) (Pregmap.get reg rs2)) →
(∀ b1 b2 delta,
f b1 = Some (b2, delta) → delta = 0 ∧ (b1 ≤ b2)%positive) →
inject_incr (Mem.flat_inj (genv_next s)) f →
(asm_invariant (mem:= mwd LDATAOps) s rs2 (lm, labd)) →
∃ labd0, trap_into_kernel_spec id s lm rs2 labd labd0 vargs sg b v0 v1 v2
v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16
∧ relate_AbData s f habd0 labd0
∧ high_level_invariant habd0.
Proof.
unfold trap_into_kernel_spec.
intros.
destruct H as [Hv[Hs[Ha[Hf[Hpc[Hp [Hesp hesp´]]]]]]]. subst.
exploit thread_proc_exit_user_exist; eauto.
intros. inv_proc. rewrite ZMap.gi. constructor.
intros [labd0[Hspec Hr]].
refine_split´; try (econstructor; fail); eauto.
- exploit (extcall_args_inject (D1:= HDATAOps) (D2:= LDATAOps)); eauto.
instantiate (3:= habd0).
apply extcall_args_with_data; eauto.
instantiate (1:= labd).
intros [?[? Hinv]]. inv_val_inject.
apply extcall_args_without_data in H; eauto.
- eapply reg_symbol_inject; eassumption.
- eapply reg_val_inject_defined; eauto 1.
- intros.
specialize (H3 ESP). unfold Pregmap.get in ×.
rewrite H in H3. inv H3; try congruence.
specialize (H4 _ _ _ H10). destruct H4 as [? Hle]; subst.
exploit hesp´; eauto.
intros [Hle1 Hle2].
split. revert Hle1 Hle. clear.
intros. Coqlib.xomega. inv H6.
inv inv_inject_neutral.
specialize (inv_reg_inject_neutral ESP).
rewrite H in inv_reg_inject_neutral.
revert inv_reg_inject_neutral; clear.
lift_unfold.
intros inv_reg_inject_neutral.
inv inv_reg_inject_neutral.
unfold Mem.flat_inj in ×.
destruct (plt b0 (Mem.nextblock lm)).
assumption. discriminate.
- destruct thread_proc_exit_user_inv.
eapply tm_exit_user_high_level_invariant; eauto.
Qed.
End PRIM_EXISTS.
Lemma syscall_dispatch_spec_ref:
compatsim (crel HDATA LDATA)
primcall_sys_dispatch_c_compatsem
sys_dispatch_c_spec_low.
Proof.
compatsim_simpl (@match_AbData).
inv Hmatch_ext. inv match_extcall_states.
destruct H7 as [Htrapk[Hext [Hrs [He1 He2]]]]. subst.
exploit trap_into_kernel_exists; eauto. intros Ht.
exploit Ht; eauto.
intros [labd1´[Hk[Hr Hh]]].
exploit sys_dispatch_c_exist; eauto.
eapply valid_curid; eauto.
intros [labd´[Hm´ Hr´]].
exploit thread_proc_start_user_exist; eauto.
eapply valid_curid; eauto.
clear Hm´.
exploit (trap_proc_create_high_inv sys_dispatch_c_spec); eauto.
intros (labd´´ & r´0 & Hm´´ & Hr´´ & Hf & Heq´ & Hrange).
refine_split; econstructor; eauto 1.
split; eauto 1.
split; eauto 1.
split; eauto 1.
eapply trap_into_kernel_low_inv in Hlow; eauto.
exploit (trap_proc_create_low_inv sys_dispatch_c_spec); eauto.
inv ASM_INV. inv inv_inject_neutral. eauto.
inversion 1; intros.
unfold uctxt_inject_neutral in ×.
subst r´0.
split; intros;
eapply uctxt_INJECT; eauto.
econstructor; eauto.
constructor.
val_inject_simpl; try (eapply Hf; omega).
Qed.
Lemma sys_run_vm_spec_ref:
compatsim (crel HDATA LDATA)
primcall_sys_run_vm_compatsem
sys_run_vm_spec_low.
Proof.
compatsim_simpl (@match_AbData).
intros.
inv Hmatch_ext. inv match_extcall_states.
exploit trap_into_kernel_exists; eauto. intros Ht.
exploit Ht; eauto.
intros [labd1[Hk[Hr Hh]]].
assert (HVAL: ∀ reg,
val_inject ι (Pregmap.get reg ((Pregmap.init Vundef) # EDI <- (rs1 EDI)) # EBP <- (rs1 EBP))
(Pregmap.get reg ((Pregmap.init Vundef) # EDI <- (rs2 EDI)) # EBP <- (rs2 EBP))).
{
val_inject_simpl.
}
exploit thread_vm_run_exist; eauto.
intros r; destruct r as [| [] | [] | | [] |]; try constructor;
try apply ASM_INV.
intros r; destruct r as [| [] | [] | | [] |]; try constructor;
try apply ASM_INV.
assert (HLOW: low_level_invariant (Mem.nextblock m2) labd1).
{
eapply trap_into_kernel_low_inv; eauto.
}
eapply HLOW.
intros (labd´ & r´0 & HM & HR & HP & HP0 & HP1).
refine_split; econstructor; eauto.
econstructor; eauto.
constructor.
val_inject_simpl.
Qed.
Lemma pagefault_handler_spec_ref:
compatsim (crel HDATA LDATA)
primcall_pagefault_handler_compatsem
pagefault_handler_spec_low.
Proof.
compatsim_simpl (@match_AbData).
intros.
inv Hmatch_ext. inv match_extcall_states.
destruct H7 as [Htrapk[Hext [Hrs [He1 He2]]]]. subst.
exploit trap_into_kernel_exists; eauto. intros Ht.
exploit Ht; eauto.
intros [labd1´[Hk[Hr Hh]]].
exploit ptfault_resv_exist; eauto.
eapply valid_curid; eauto.
intros [labd´[Hm´ Hr´]].
exploit thread_proc_start_user_exist; eauto.
eapply valid_curid; eauto.
eapply ptfault_resv_high_inv; eauto.
intros (labd´´ & r´0 & Hm´´ & Hr´´ & Hf & Heq´ & Hrange).
refine_split;
econstructor; try eassumption; eauto 1.
split; eauto 1.
split; eauto 1.
split; eauto 1.
eapply trap_into_kernel_low_inv in Hlow; eauto.
exploit (ptfault_resv_low_inv); eauto.
inversion 1; intros.
unfold uctxt_inject_neutral in ×.
subst r´0.
split; intros;
eapply uctxt_INJECT; eauto.
inv Hr. congruence.
econstructor; eauto.
constructor.
val_inject_simpl; try (eapply Hf; omega).
Qed.
Lemma passthrough_correct:
sim (crel HDATA LDATA) tsyscall_passthrough tdispatch.
Proof.
sim_oplus. - apply thread_vmxinfo_get_sim.
- apply thread_ptRead_sim.
- apply thread_uctx_get_sim.
- apply thread_uctx_set_sim.
- apply thread_get_CPU_ID_sim.
- apply thread_get_curid_sim.
- apply thread_vmx_return_from_guest_sim.
- apply thread_vmx_init_sim.
- apply thread_trap_info_get_sim.
- apply thread_trap_info_ret_sim.
- layer_sim_simpl.
+ eapply load_correct3high.
+ eapply store_correct3high.
Qed.
End WITHMEM.
End Refinement.
Local Open Scope string_scope.
Local Open Scope error_monad_scope.
Local Open Scope Z_scope.
Context `{single_oracle_prop: SingleOracleProp}.
Context `{real_params : RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Notation HDATA := RData.
Notation LDATA := RData.
Notation HDATAOps := (cdata (cdata_ops := pipcintro_data_ops) HDATA).
Notation LDATAOps := (cdata (cdata_ops := pipcintro_data_ops) LDATA).
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Section PRIM_EXISTS.
Lemma trap_into_kernel_exists:
∀ s hm lm habd habd0 labd (rs1 rs2 :regset) v0 v1 v2 v3 v5 v6
v8 v9 v10 v11 v12 v13 v14 v15 v16 v4 v7 vargs id sg b f,
trap_into_kernel_spec id s hm rs1 habd habd0 vargs sg b v0 v1 v2
v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 →
Mem.inject f hm lm →
relate_AbData s f habd labd →
high_level_invariant habd →
(∀ reg,
val_inject f (Pregmap.get reg rs1) (Pregmap.get reg rs2)) →
(∀ b1 b2 delta,
f b1 = Some (b2, delta) → delta = 0 ∧ (b1 ≤ b2)%positive) →
inject_incr (Mem.flat_inj (genv_next s)) f →
(asm_invariant (mem:= mwd LDATAOps) s rs2 (lm, labd)) →
∃ labd0, trap_into_kernel_spec id s lm rs2 labd labd0 vargs sg b v0 v1 v2
v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16
∧ relate_AbData s f habd0 labd0
∧ high_level_invariant habd0.
Proof.
unfold trap_into_kernel_spec.
intros.
destruct H as [Hv[Hs[Ha[Hf[Hpc[Hp [Hesp hesp´]]]]]]]. subst.
exploit thread_proc_exit_user_exist; eauto.
intros. inv_proc. rewrite ZMap.gi. constructor.
intros [labd0[Hspec Hr]].
refine_split´; try (econstructor; fail); eauto.
- exploit (extcall_args_inject (D1:= HDATAOps) (D2:= LDATAOps)); eauto.
instantiate (3:= habd0).
apply extcall_args_with_data; eauto.
instantiate (1:= labd).
intros [?[? Hinv]]. inv_val_inject.
apply extcall_args_without_data in H; eauto.
- eapply reg_symbol_inject; eassumption.
- eapply reg_val_inject_defined; eauto 1.
- intros.
specialize (H3 ESP). unfold Pregmap.get in ×.
rewrite H in H3. inv H3; try congruence.
specialize (H4 _ _ _ H10). destruct H4 as [? Hle]; subst.
exploit hesp´; eauto.
intros [Hle1 Hle2].
split. revert Hle1 Hle. clear.
intros. Coqlib.xomega. inv H6.
inv inv_inject_neutral.
specialize (inv_reg_inject_neutral ESP).
rewrite H in inv_reg_inject_neutral.
revert inv_reg_inject_neutral; clear.
lift_unfold.
intros inv_reg_inject_neutral.
inv inv_reg_inject_neutral.
unfold Mem.flat_inj in ×.
destruct (plt b0 (Mem.nextblock lm)).
assumption. discriminate.
- destruct thread_proc_exit_user_inv.
eapply tm_exit_user_high_level_invariant; eauto.
Qed.
End PRIM_EXISTS.
Lemma syscall_dispatch_spec_ref:
compatsim (crel HDATA LDATA)
primcall_sys_dispatch_c_compatsem
sys_dispatch_c_spec_low.
Proof.
compatsim_simpl (@match_AbData).
inv Hmatch_ext. inv match_extcall_states.
destruct H7 as [Htrapk[Hext [Hrs [He1 He2]]]]. subst.
exploit trap_into_kernel_exists; eauto. intros Ht.
exploit Ht; eauto.
intros [labd1´[Hk[Hr Hh]]].
exploit sys_dispatch_c_exist; eauto.
eapply valid_curid; eauto.
intros [labd´[Hm´ Hr´]].
exploit thread_proc_start_user_exist; eauto.
eapply valid_curid; eauto.
clear Hm´.
exploit (trap_proc_create_high_inv sys_dispatch_c_spec); eauto.
intros (labd´´ & r´0 & Hm´´ & Hr´´ & Hf & Heq´ & Hrange).
refine_split; econstructor; eauto 1.
split; eauto 1.
split; eauto 1.
split; eauto 1.
eapply trap_into_kernel_low_inv in Hlow; eauto.
exploit (trap_proc_create_low_inv sys_dispatch_c_spec); eauto.
inv ASM_INV. inv inv_inject_neutral. eauto.
inversion 1; intros.
unfold uctxt_inject_neutral in ×.
subst r´0.
split; intros;
eapply uctxt_INJECT; eauto.
econstructor; eauto.
constructor.
val_inject_simpl; try (eapply Hf; omega).
Qed.
Lemma sys_run_vm_spec_ref:
compatsim (crel HDATA LDATA)
primcall_sys_run_vm_compatsem
sys_run_vm_spec_low.
Proof.
compatsim_simpl (@match_AbData).
intros.
inv Hmatch_ext. inv match_extcall_states.
exploit trap_into_kernel_exists; eauto. intros Ht.
exploit Ht; eauto.
intros [labd1[Hk[Hr Hh]]].
assert (HVAL: ∀ reg,
val_inject ι (Pregmap.get reg ((Pregmap.init Vundef) # EDI <- (rs1 EDI)) # EBP <- (rs1 EBP))
(Pregmap.get reg ((Pregmap.init Vundef) # EDI <- (rs2 EDI)) # EBP <- (rs2 EBP))).
{
val_inject_simpl.
}
exploit thread_vm_run_exist; eauto.
intros r; destruct r as [| [] | [] | | [] |]; try constructor;
try apply ASM_INV.
intros r; destruct r as [| [] | [] | | [] |]; try constructor;
try apply ASM_INV.
assert (HLOW: low_level_invariant (Mem.nextblock m2) labd1).
{
eapply trap_into_kernel_low_inv; eauto.
}
eapply HLOW.
intros (labd´ & r´0 & HM & HR & HP & HP0 & HP1).
refine_split; econstructor; eauto.
econstructor; eauto.
constructor.
val_inject_simpl.
Qed.
Lemma pagefault_handler_spec_ref:
compatsim (crel HDATA LDATA)
primcall_pagefault_handler_compatsem
pagefault_handler_spec_low.
Proof.
compatsim_simpl (@match_AbData).
intros.
inv Hmatch_ext. inv match_extcall_states.
destruct H7 as [Htrapk[Hext [Hrs [He1 He2]]]]. subst.
exploit trap_into_kernel_exists; eauto. intros Ht.
exploit Ht; eauto.
intros [labd1´[Hk[Hr Hh]]].
exploit ptfault_resv_exist; eauto.
eapply valid_curid; eauto.
intros [labd´[Hm´ Hr´]].
exploit thread_proc_start_user_exist; eauto.
eapply valid_curid; eauto.
eapply ptfault_resv_high_inv; eauto.
intros (labd´´ & r´0 & Hm´´ & Hr´´ & Hf & Heq´ & Hrange).
refine_split;
econstructor; try eassumption; eauto 1.
split; eauto 1.
split; eauto 1.
split; eauto 1.
eapply trap_into_kernel_low_inv in Hlow; eauto.
exploit (ptfault_resv_low_inv); eauto.
inversion 1; intros.
unfold uctxt_inject_neutral in ×.
subst r´0.
split; intros;
eapply uctxt_INJECT; eauto.
inv Hr. congruence.
econstructor; eauto.
constructor.
val_inject_simpl; try (eapply Hf; omega).
Qed.
Lemma passthrough_correct:
sim (crel HDATA LDATA) tsyscall_passthrough tdispatch.
Proof.
sim_oplus. - apply thread_vmxinfo_get_sim.
- apply thread_ptRead_sim.
- apply thread_uctx_get_sim.
- apply thread_uctx_set_sim.
- apply thread_get_CPU_ID_sim.
- apply thread_get_curid_sim.
- apply thread_vmx_return_from_guest_sim.
- apply thread_vmx_init_sim.
- apply thread_trap_info_get_sim.
- apply thread_trap_info_ret_sim.
- layer_sim_simpl.
+ eapply load_correct3high.
+ eapply store_correct3high.
Qed.
End WITHMEM.
End Refinement.