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.
Require Import GlobalOracleProp.
Require Import SingleOracle.
Section ASM_VERIFICATION.
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 LDATA := RData.
Notation LDATAOps := (cdata (cdata_ops := pipcintro_data_ops) 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}.
Require Import LAsmModuleSemSpec.
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
(HUEIP_cond: v12 ≠ Int.repr 0),
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; simpl.
exploit Hstart2; eauto.
intros [[b_start [Hstart_symbol Hstart_fun]] prim_start].
exploit Hexit2; 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_user2).
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); eauto 1.
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_user2).
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.
intros contra.
erewrite <- sys_dispatch_ueip_value in contra; eauto.
rewrite ZMap.gso in contra; [ | intro contra´; inv contra´].
rewrite ZMap.gso in contra; [ | intro contra´; inv contra´].
rewrite ZMap.gso in contra; [ | intro contra´; inv contra´].
rewrite ZMap.gso in contra; [ | intro contra´; inv contra´].
rewrite ZMap.gss in contra.
elim HUEIP_cond.
inv contra; auto.
intros contra.
erewrite <- sys_dispatch_ueip_value in contra; eauto.
rewrite ZMap.gso in contra; [ | intro contra´; inv contra´].
rewrite ZMap.gso in contra; [ | intro contra´; inv contra´].
rewrite ZMap.gso in contra; [ | intro contra´; inv contra´].
rewrite ZMap.gso in contra; [ | intro contra´; inv contra´].
rewrite ZMap.gss in contra.
inv contra.
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 H2 as [Hk _]. subst.
destruct Hk as [_ [_[_[Hsym _]]]].
rewrite Hsym in Hsymbol. inv Hsymbol.
assumption.
}
exploit sys_dispatch_spec; eauto 2.
inv H4.
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.