Library mcertikos.trap.SysCallGenAsm
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_post_proof:
∀ ge (s: stencil) (rs: regset) m labd labd1 labd' rs0 rs' b,
make_globalenv s (sys_sendtochan_post ↦ sys_sendtochan_post_function) tdispatch = ret ge →
trap_sendtochan_post_spec labd = Some labd1 →
proc_start_user_spec labd1 = Some (labd', rs') →
rs0 = (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR ECX :: IR EAX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs))
# EDI <- (ZMap.get U_EDI rs')# ESI <- (ZMap.get U_ESI rs')
# EBP <- (ZMap.get U_EBP rs')# ESP <- (ZMap.get U_ESP rs')
# EBX <- (ZMap.get U_EBX rs')# EDX <- (ZMap.get U_EDX rs')
# ECX <- (ZMap.get U_ECX rs')# EAX <- (ZMap.get U_EAX rs')
# PC <- (ZMap.get U_EIP rs') →
(∀ i, 0 ≤ i < UCTXT_SIZE →
let v:= (ZMap.get i rs') in
Val.has_type v AST.Tint) →
(∀ i, 0 ≤ i < UCTXT_SIZE →
let v:= (ZMap.get i rs') in
val_inject (Mem.flat_inj (Mem.nextblock m)) v v) →
find_symbol s sys_sendtochan_post = Some b →
rs PC = Vptr b Int.zero →
rs ESP ≠ Vundef →
(∀ b0 o,
rs ESP = Vptr b0 o →
Ple (genv_next s) b0 ∧ Plt b0 (Mem.nextblock m)) →
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_post ↦ sys_sendtochan_post_function)
(tdispatch (Hmwd:= Hmwd) (Hmem:= Hmem))
sys_sendtochan_post s rs (m, labd) r_ (m, labd')
∧ (∀ l,
Val.lessdef (Pregmap.get l rs0)
(Pregmap.get l r_)).
Proof.
intros. subst.
assert (HOS': 0 ≤ 64 ≤ Int.max_unsigned) by rewrite_omega.
exploit Hstart; eauto.
intros [[b_start [Hstart_symbol Hstart_fun]] prim_start].
exploit Hsendpost; eauto.
intros [[b_check [Hcheck_symbol Hcheck_fun]] prim_check].
exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
intros Hstencil_matches.
exploit Hsys_sendtochan_post; 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 H8; eauto.
inv Hstencil_matches.
rewrite stencil_matches_genv_next.
trivial.
}
clear H8.
rewrite (Lregset_rewrite rs).
refine_split'; try eassumption.
rewrite H6.
econstructor; eauto.
one_step_forward'.
Lregset_simpl_tac.
unfold symbol_offset. unfold fundef.
rewrite Hcheck_symbol.
econstructor; eauto 1.
eapply (LAsm.exec_step_external _ b_check); simpl; eauto 1.
unfold trap_sendtochan_post_spec in H0; elim_none_eqn Hsend.
unfold syncsendto_chan_post_spec in Hsend; repeat elim_none; auto.
econstructor; eauto 1.
econstructor; eauto 1.
red. red. red. red. red. red.
change positive with ident in ×.
rewrite prim_check.
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'.
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.
assert (HUCTX': ∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i rs') in
Val.has_type v Tint
∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v).
{
eapply sys_sendtochan_post_generate; try eassumption.
}
econstructor; try eassumption; try reflexivity.
inv Hstencil_matches. 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_post_code_correct:
asm_spec_le (sys_sendtochan_post ↦ sys_sendtochan_post_spec_low)
(〚sys_sendtochan_post ↦ sys_sendtochan_post_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_post_function)).
{
assert (Hmodule: get_module_function sys_sendtochan_post (sys_sendtochan_post ↦ sys_sendtochan_post_function)
= OK (Some sys_sendtochan_post_function)) by
reflexivity.
assert (HInternal: make_internal sys_sendtochan_post_function
= OK (AST.Internal sys_sendtochan_post_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 H6 in Hsymbol. inv Hsymbol.
assumption.
}
exploit sys_sendtochan_post_proof; eauto 2.
inv H10.
inv inv_inject_neutral.
intros [r_[Hstep Hv]].
assert (Hle: (Mem.nextblock m0 ≤ Mem.nextblock m0)%positive).
{
reflexivity.
}
refine_split'; try eassumption; try reflexivity.
- lift_unfold. split; try reflexivity.
eapply Mem.neutral_inject. assumption.
- esplit; reflexivity.
Qed.
Lemma sys_dispatch_spec:
∀ ge (s: stencil) (rs: regset) m labd labd0 labd1 labd' rs0 rs' v0 v1 v2 v3 v5 v6
v8 v9 v10 v11 v12 v13 v14 v15 v16 v4 v7 vargs sg b,
make_globalenv s (syscall_dispatch ↦ sys_dispatch_function) tdispatch = ret ge →
syscall_spec syscall_dispatch 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 →
sys_dispatch_c_spec s m labd0 = Some labd1 →
asm_invariant (mem := mwd LDATAOps) s rs (m, labd) →
∃ r_: regset,
lasm_step (syscall_dispatch ↦ sys_dispatch_function)
(tdispatch (Hmwd:= Hmwd) (Hmem:= Hmem))
syscall_dispatch s rs (m, labd) r_ (m, labd')
∧ (∀ l,
Val.lessdef (Pregmap.get l rs0)
(Pregmap.get l r_)).
Proof.
intros. 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 Hdispatch_c; eauto.
intros [[b_check [Hcheck_symbol Hcheck_fun]] prim_check].
exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
intros Hstencil_matches.
exploit Hsys_dispatch_c; 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.
econstructor; eauto 1.
eapply (LAsm.exec_step_external _ b_check); simpl; eauto 1.
unfold sys_dispatch_c_spec in H1; elim_none_eqn Huctx.
unfold uctx_arg1_spec in Huctx; repeat elim_none; auto 2.
econstructor; eauto 1.
econstructor; eauto 1.
red. red. red. red. red. red.
change positive with ident in ×.
rewrite prim_check.
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'.
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.
assert (HUCTX': ∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i rs') in
Val.has_type v Tint
∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v).
{
eapply sys_dispatch_generate; try eassumption.
- inv H2. inv inv_inject_neutral. assumption.
- intros. subst v.
inv_proc; try (split; constructor).
rewrite ZMap.gi.
split; constructor.
}
econstructor; try eassumption; try reflexivity.
eapply HUCTX'.
eapply HUCTX'.
inv Hstencil_matches. 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_dispatch_code_correct:
asm_spec_le (syscall_dispatch ↦ sys_dispatch_c_spec_low)
(〚syscall_dispatch ↦ sys_dispatch_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_dispatch_function)).
{
assert (Hmodule: get_module_function syscall_dispatch (syscall_dispatch ↦ sys_dispatch_function)
= OK (Some sys_dispatch_function)) by
reflexivity.
assert (HInternal: make_internal sys_dispatch_function
= OK (AST.Internal sys_dispatch_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 sys_dispatch_spec; eauto 2.
inv H3.
inv inv_inject_neutral.
intros [r_[Hstep Hv]].
assert (Hle: (Mem.nextblock m0 ≤ Mem.nextblock m0)%positive).
{
reflexivity.
}
refine_split'; try eassumption; try reflexivity.
- lift_unfold. split; try reflexivity.
eapply Mem.neutral_inject. assumption.
- esplit; reflexivity.
Qed.
End WITHMEM.
End ASM_VERIFICATION.