Library mcertikos.trap.SysCallGenAsmData
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 SysCallGenAsmSource.
Require Import AbstractDataType.
Section ASM_DATA.
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 proc_start_generate:
∀ abd1 abd' rs' m,
proc_start_user_spec abd1 = Some (abd', rs') →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (cid abd1)
(uctxt abd1))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v) →
(∀ 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).
Proof.
intros. unfold proc_start_user_spec in ×.
subdestruct. subst v.
inv H. eauto.
Qed.
Lemma set_errno_generate:
∀ abd0 abd1 m n,
uctx_set_errno_spec n abd0 = Some abd1 →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (cid abd0)
(uctxt abd0))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (cid abd1)
(uctxt abd1))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v).
Proof.
intros. subst v.
functional inversion H; simpl.
repeat rewrite ZMap.gss.
subst uctx' uctx.
destruct (zeq i 7).
subst.
rewrite ZMap.gss.
split; constructor.
rewrite ZMap.gso; auto.
Qed.
Lemma set_retval1_generate:
∀ abd0 abd1 m shadow,
uctx_set_retval1_spec shadow abd0 = Some abd1 →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (cid abd0)
(uctxt abd0))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (cid abd1)
(uctxt abd1))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v).
Proof.
intros. subst v.
functional inversion H; simpl.
repeat rewrite ZMap.gss.
subst uctx' uctx.
destruct (zeq i 4).
subst.
rewrite ZMap.gss.
split; constructor.
rewrite ZMap.gso; auto.
Qed.
Lemma set_retval2_generate:
∀ abd0 abd1 m shadow,
uctx_set_retval2_spec shadow abd0 = Some abd1 →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (cid abd0)
(uctxt abd0))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (cid abd1)
(uctxt abd1))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v).
Proof.
intros. subst v.
functional inversion H; simpl.
repeat rewrite ZMap.gss.
subst uctx' uctx.
destruct (zeq i 6).
subst.
rewrite ZMap.gss.
split; constructor.
rewrite ZMap.gso; auto.
Qed.
Lemma set_retval3_generate:
∀ abd0 abd1 m shadow,
uctx_set_retval3_spec shadow abd0 = Some abd1 →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (cid abd0)
(uctxt abd0))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (cid abd1)
(uctxt abd1))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v).
Proof.
intros. subst v.
functional inversion H; simpl.
repeat rewrite ZMap.gss.
subst uctx' uctx.
destruct (zeq i 5).
subst.
rewrite ZMap.gss.
split; constructor.
rewrite ZMap.gso; auto.
Qed.
Lemma set_retval4_generate:
∀ abd0 abd1 m shadow,
uctx_set_retval4_spec shadow abd0 = Some abd1 →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (cid abd0)
(uctxt abd0))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (cid abd1)
(uctxt abd1))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v).
Proof.
intros. subst v.
functional inversion H; simpl.
repeat rewrite ZMap.gss.
subst uctx' uctx.
destruct (zeq i 1).
subst.
rewrite ZMap.gss.
split; constructor.
rewrite ZMap.gso; auto.
Qed.
Lemma proc_exit_generate:
∀ m abd abd1 uctx,
proc_exit_user_spec abd uctx = Some abd1 →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i uctx) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (cid abd1)
(uctxt abd1))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v).
Proof.
intros. subst v.
functional inversion H; simpl.
repeat rewrite ZMap.gss. auto.
Qed.
Lemma sys_yield_generate:
∀ m labd abd abd0 rs' uctx rs1,
proc_exit_user_spec labd uctx = Some abd →
thread_yield_spec abd rs' = Some (abd0, rs1) →
high_level_invariant labd →
low_level_invariant (Mem.nextblock m) labd →
(∀ v r, ZtoPreg v = Some r →
Val.has_type (rs1 r) Tint
∧ val_inject (Mem.flat_inj (Mem.nextblock m))
(rs1 r) (rs1 r)).
Proof.
intros.
functional inversion H; subst.
Opaque remove.
unfold thread_yield_spec in H0; simpl in H0.
rewrite H5, H6 in H0; simpl in H0. subdestruct. inv H0. inv H1.
assert(HIn: In (last l num_proc) l).
{
apply last_correct; auto.
}
assert (HOS: 0≤ num_proc ≤ num_proc) by omega.
unfold AbQCorrect in ×.
specialize (valid_TDQ H6 _ HOS).
destruct valid_TDQ as [lt[HM HP]].
rewrite Hdestruct in HM. inv HM.
inv H2.
eapply kctxt_INJECT.
apply HP; trivial.
eassumption.
Qed.
Lemma ptInsertPTE0_generate:
∀ abd0 abd1 m n vadr v1 v2,
ptInsertPTE0_spec n vadr v1 v2 abd0 = Some abd1 →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (cid abd0)
(uctxt abd0))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (cid abd1)
(uctxt abd1))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v).
Proof.
intros. subst v.
functional inversion H; simpl; eauto.
Qed.
Lemma ptAllocPDE0_generate:
∀ abd0 abd1 m n vadr z,
ptAllocPDE0_spec n vadr abd0 = Some (abd1, z) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (cid abd0)
(uctxt abd0))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (cid abd1)
(uctxt abd1))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v).
Proof.
intros. subst v.
functional inversion H; simpl; subst; eauto.
Qed.
Lemma ptInsert0_generate:
∀ abd0 abd1 m n vadr v1 v2 z,
ptInsert0_spec n vadr v1 v2 abd0 = Some (abd1, z) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (cid abd0)
(uctxt abd0))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (cid abd1)
(uctxt abd1))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v).
Proof.
intros. subst v.
functional inversion H; simpl.
- eapply ptInsertPTE0_generate; eauto.
- eapply ptAllocPDE0_generate; eauto.
- eapply ptInsertPTE0_generate; eauto.
eapply ptAllocPDE0_generate; eauto.
Qed.
Lemma pgf_handler_generate:
∀ m labd abd abd' abd0 rs' uctx vadr,
proc_exit_user_spec labd uctx = Some abd →
ptfault_resv_spec vadr abd = Some abd0 →
proc_start_user_spec abd0 = Some (abd', rs') →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i uctx) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v) →
ikern abd = true
∧ ihost abd = true
∧ ikern abd0 = true
∧ ihost abd0 = 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 m)) v v).
Proof.
intros.
functional inversion H; subst; simpl in ×.
unfold ptfault_resv_spec in *; simpl in ×.
unfold ptResv_spec in ×.
unfold alloc_spec in *; simpl in ×.
assert (Habd0: ikern abd0 = true ∧ ihost abd0 = true)
by (clear H0; unfold proc_start_user_spec in *; subdestruct; auto).
destruct Habd0; subdestruct; refine_split'; trivial; inv H0.
- eapply proc_start_generate; eauto.
simpl. rewrite ZMap.gss. intros.
exploit proc_exit_generate; eauto.
- eapply proc_start_generate; eauto.
eapply ptInsert0_generate; eauto.
simpl. rewrite ZMap.gss. intros.
exploit proc_exit_generate; eauto.
- eapply proc_start_generate; eauto.
simpl. rewrite ZMap.gss. intros.
exploit proc_exit_generate; eauto.
- eapply proc_start_generate; eauto.
simpl. rewrite ZMap.gss. intros.
exploit proc_exit_generate; eauto.
Qed.
Lemma sys_sendtochan_pre_generate:
∀ m labd abd abd0 abd1 rs' uctx chanid rs_yield,
proc_exit_user_spec labd uctx = Some abd →
trap_sendtochan_pre_spec abd = Some (abd0, Int.unsigned chanid) →
thread_sleep_spec abd0 rs_yield (Int.unsigned chanid) = Some (abd1, rs') →
high_level_invariant labd →
low_level_invariant (Mem.nextblock m) labd →
(∀ v r, ZtoPreg v = Some r →
Val.has_type (rs'#r) Tint
∧ val_inject (Mem.flat_inj (Mem.nextblock m)) (rs'#r) (rs'#r)).
Proof.
intros. functional inversion H; subst.
unfold thread_sleep_spec in H1.
unfold proc_exit_user_spec in H.
unfold trap_sendtochan_pre_spec in H0.
subdestruct; inv H1. inv H. inv H0.
assert(HIn: In (last l num_proc) l).
{
apply last_correct; auto.
}
assert (HOS: 0≤ num_proc ≤ num_proc) by omega.
unfold AbQCorrect_range, AbQCorrect in ×.
inv H2.
specialize (valid_TDQ Hdestruct0 _ HOS).
destruct valid_TDQ as [lt[HM HP]].
functional inversion H1; simpl in ×.
- inv H; simpl in *; rewrite Hdestruct10 in HM. inv HM.
eapply kctxt_INJECT; eauto.
- inv H. inv H17. simpl in ×.
rewrite Hdestruct10 in HM. inv HM.
eapply kctxt_INJECT; eauto.
Qed.
Lemma trap_sendtochan_post_generate:
∀ abd0 abd m,
trap_sendtochan_post_spec abd = Some abd0 →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (cid abd)
(uctxt abd))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (cid abd0)
(uctxt abd0))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v).
Proof.
intros. subst v.
functional inversion H.
eapply set_errno_generate; eauto.
eapply set_retval1_generate; eauto.
functional inversion H3;
subst; simpl; auto.
Qed.
Lemma sys_sendtochan_post_generate:
∀ m abd abd' abd0 rs',
trap_sendtochan_post_spec abd = Some abd0 →
proc_start_user_spec abd0 = Some (abd', rs') →
high_level_invariant abd →
low_level_invariant (Mem.nextblock m) abd →
(∀ 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).
Proof.
intros.
eapply proc_start_generate; eauto.
eapply trap_sendtochan_post_generate; eauto.
inv H1. unfold uctxt_inject_neutral in ×.
intros; eapply uctxt_INJECT; eauto.
Qed.
Lemma ptResv_generate:
∀ abd0 abd1 m v1 v2 v3 z,
ptResv_spec v1 v2 v3 abd0 = Some (abd1, z) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (cid abd0)
(uctxt abd0))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (cid abd1)
(uctxt abd1))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v).
Proof.
intros. subst v.
functional inversion H; subst; simpl; eauto.
eapply ptInsert0_generate; eauto.
functional inversion H3; subst; eauto.
Qed.
Lemma trap_proc_create_generate:
∀ abd0 abd1 m s,
trap_proc_create_spec s m abd0 = Some abd1 →
(genv_next s ≤ Mem.nextblock m)%positive →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (cid abd0)
(uctxt abd0))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (cid abd1)
(uctxt abd1))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v).
Proof.
intros. subst v.
rename H into Hspec; unfold trap_proc_create_spec in Hspec.
destruct (uctx_arg3_spec abd0); try discriminate Hspec.
destruct (zle_le 0 z
(cquota (ZMap.get (cid abd0) (AC abd0)) -
cusage (ZMap.get (cid abd0) (AC abd0)))) eqn:Hquota.
destruct (zle_le 0 (cid abd0 × max_children + 1 + max_children) num_id) eqn:Hchild.
destruct (zlt (Z.of_nat (length (cchildren (ZMap.get (cid abd0) (AC abd0)))))
max_children) eqn:Hnc; subdestruct; subst.
- eapply set_errno_generate; eauto.
eapply set_retval1_generate; eauto.
unfold proc_create_spec in ×. subdestruct; subst.
inv Hdestruct11; simpl in ×.
intros; zmap_solve; split; auto.
econstructor.
eapply stencil_find_symbol_inject'; eauto.
eapply flat_inj_inject_incr. assumption.
rewrite Int.add_zero. reflexivity.
- eapply set_errno_generate; eauto.
- eapply set_errno_generate; eauto.
- eapply set_errno_generate; eauto.
Qed.
Lemma ptResv2_generate:
∀ abd0 abd1 m v1 v2 v3 v4 v5 v6 z,
ptResv2_spec v1 v2 v3 v4 v5 v6 abd0 = Some (abd1, z) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (cid abd0)
(uctxt abd0))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (cid abd1)
(uctxt abd1))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v).
Proof.
intros. subst v.
functional inversion H; subst; simpl; eauto.
- eapply ptInsert0_generate; eauto.
functional inversion H4; subst; eauto.
- eapply ptInsert0_generate; eauto.
eapply ptInsert0_generate; eauto.
functional inversion H3; subst; eauto.
Qed.
Lemma offer_shared_mem_generate:
∀ abd0 abd1 i1 i2 i3 m z,
offer_shared_mem_spec i1 i2 i3 abd0 = Some (abd1, z) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (cid abd0)
(uctxt abd0))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (cid abd1)
(uctxt abd1))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v).
Proof.
intros. subst v.
functional inversion H; subst; simpl; eauto; clear H.
- eapply ptResv2_generate; eauto.
- eapply ptResv2_generate; eauto.
Qed.
Lemma trap_offer_shared_mem_generate:
∀ abd0 abd1 m,
trap_offer_shared_mem_spec abd0 = Some abd1 →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (cid abd0)
(uctxt abd0))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (cid abd1)
(uctxt abd1))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v).
Proof.
intros. subst v.
functional inversion H; subst; simpl; eauto; clear H.
- eapply set_errno_generate; eauto.
eapply set_retval1_generate; eauto.
eapply offer_shared_mem_generate; eauto.
- eapply set_errno_generate; eauto.
Qed.
Lemma print_generate:
∀ abd0 abd1 m,
print_spec abd0 = Some abd1 →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (cid abd0)
(uctxt abd0))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (cid abd1)
(uctxt abd1))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v).
Proof.
intros. subst v.
functional inversion H; subst; simpl; eauto; clear H.
eapply set_errno_generate; eauto.
Qed.
Lemma sys_dispatch_c_generate:
∀ abd0 abd1 m s,
sys_dispatch_c_spec s m abd0 = Some abd1 →
∀ (Hgenv: (genv_next s ≤ Mem.nextblock m)%positive),
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (cid abd0)
(uctxt abd0))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v) →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i (ZMap.get (cid abd1)
(uctxt abd1))) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v).
Proof.
intros. subst v.
unfold sys_dispatch_c_spec in ×.
subdestruct;
try (eapply set_errno_generate; eauto; fail).
-
eapply trap_proc_create_generate; eauto.
-
functional inversion H.
eapply set_errno_generate; eauto.
eapply set_retval1_generate; eauto.
-
eapply trap_offer_shared_mem_generate; eauto.
-
eapply print_generate; eauto.
Qed.
Lemma sys_dispatch_generate:
∀ m labd abd abd' abd0 rs' uctx s,
proc_exit_user_spec labd uctx = Some abd →
sys_dispatch_c_spec s m abd = Some abd0 →
proc_start_user_spec abd0 = Some (abd', rs') →
(genv_next s ≤ Mem.nextblock m)%positive →
(∀ i, 0≤ i < UCTXT_SIZE →
let v:= (ZMap.get i uctx) in
Val.has_type v Tint ∧ val_inject (Mem.flat_inj (Mem.nextblock m)) v v) →
(∀ 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).
Proof.
intros. subst v.
eapply proc_start_generate; eauto.
eapply sys_dispatch_c_generate; eauto.
eapply proc_exit_generate; eauto.
Qed.
Lemma Hstart:
∀ MCode_Asm s ge,
make_globalenv s MCode_Asm tdispatch = ret ge →
(∃ b, Genv.find_symbol ge proc_start_user = Some b
∧ Genv.find_funct_ptr ge b =
Some (External (EF_external proc_start_user proc_start_user_sig)))
∧ get_layer_primitive proc_start_user tdispatch =
OK (Some (primcall_start_user_compatsem proc_start_user_spec)).
Proof.
intros.
assert (Hprim: get_layer_primitive proc_start_user tdispatch =
OK (Some (primcall_start_user_compatsem proc_start_user_spec)))
by reflexivity.
split; try assumption.
eapply make_globalenv_get_layer_primitive; eauto.
Qed.
Lemma Hexit:
∀ MCode_Asm s ge,
make_globalenv s MCode_Asm tdispatch = ret ge →
(∃ b, Genv.find_symbol ge proc_exit_user = Some b
∧ Genv.find_funct_ptr ge b =
Some (External (EF_external proc_exit_user proc_exit_user_sig)))
∧ get_layer_primitive proc_exit_user tdispatch =
OK (Some (primcall_exit_user_compatsem proc_exit_user_spec)).
Proof.
intros.
assert (Hprim: get_layer_primitive proc_exit_user tdispatch =
OK (Some (primcall_exit_user_compatsem proc_exit_user_spec)))
by reflexivity.
split; try assumption.
eapply make_globalenv_get_layer_primitive; eauto.
Qed.
Lemma Hyield:
∀ MCode_Asm s ge,
make_globalenv s MCode_Asm tdispatch = ret ge →
(∃ b, Genv.find_symbol ge thread_yield = Some b
∧ Genv.find_funct_ptr ge b =
Some (External (EF_external thread_yield thread_yield_sig)))
∧ get_layer_primitive thread_yield tdispatch =
OK (Some (primcall_thread_schedule_compatsem
thread_yield_spec (prim_ident:= thread_yield))).
Proof.
intros.
assert (Hprim: get_layer_primitive thread_yield tdispatch =
OK (Some (primcall_thread_schedule_compatsem
thread_yield_spec (prim_ident:= thread_yield))))
by reflexivity.
split; try assumption.
eapply make_globalenv_get_layer_primitive; eauto.
Qed.
Lemma Hsleep:
∀ MCode_Asm s ge,
make_globalenv s MCode_Asm tdispatch = ret ge →
(∃ b, Genv.find_symbol ge thread_sleep = Some b
∧ Genv.find_funct_ptr ge b =
Some (External (EF_external thread_sleep thread_sleep_sig)))
∧ get_layer_primitive thread_sleep tdispatch =
OK (Some (primcall_thread_transfer_compatsem thread_sleep_spec)).
Proof.
intros.
assert (Hprim: get_layer_primitive thread_sleep tdispatch =
OK (Some (primcall_thread_transfer_compatsem thread_sleep_spec)))
by reflexivity.
split; try assumption.
eapply make_globalenv_get_layer_primitive; eauto.
Qed.
Lemma Hget:
∀ MCode_Asm s ge,
make_globalenv s MCode_Asm tdispatch = ret ge →
(∃ b, Genv.find_symbol ge trap_get = Some b
∧ Genv.find_funct_ptr ge b =
Some (External (EF_external trap_get trap_get_sig)))
∧ get_layer_primitive trap_get tdispatch =
OK (Some (primcall_trap_info_get_compatsem trap_info_get_spec)).
Proof.
intros.
assert (Hprim: get_layer_primitive trap_get tdispatch =
OK (Some (primcall_trap_info_get_compatsem trap_info_get_spec)))
by reflexivity.
split; try assumption.
eapply make_globalenv_get_layer_primitive; eauto.
Qed.
Lemma Hpgfr:
∀ MCode_Asm s ge,
make_globalenv s MCode_Asm tdispatch = ret ge →
(∃ b, Genv.find_symbol ge ptfault_resv = Some b
∧ Genv.find_funct_ptr ge b =
Some (External (EF_external ptfault_resv ptfault_resv_sig)))
∧ get_layer_primitive ptfault_resv tdispatch =
OK (Some (gensem ptfault_resv_spec)).
Proof.
intros.
assert (Hprim: get_layer_primitive ptfault_resv tdispatch =
OK (Some (gensem ptfault_resv_spec)))
by reflexivity.
split; try assumption.
eapply make_globalenv_get_layer_primitive; eauto.
Qed.
Lemma Hdispatch_c:
∀ MCode_Asm s ge,
make_globalenv s MCode_Asm tdispatch = ret ge →
(∃ b, Genv.find_symbol ge syscall_dispatch_C = Some b
∧ Genv.find_funct_ptr ge b =
Some (External (EF_external syscall_dispatch_C syscall_c_dispatch_sig)))
∧ get_layer_primitive syscall_dispatch_C tdispatch =
OK (Some (trap_proccreate_compatsem sys_dispatch_c_spec)).
Proof.
intros.
assert (Hprim: get_layer_primitive syscall_dispatch_C tdispatch =
OK (Some (trap_proccreate_compatsem sys_dispatch_c_spec)))
by reflexivity.
split; try assumption.
eapply make_globalenv_get_layer_primitive; eauto.
Qed.
Lemma Hsys_dispatch_c:
∀ ge s b,
make_globalenv s (syscall_dispatch ↦ sys_dispatch_function) tdispatch = ret ge →
find_symbol s syscall_dispatch = Some b →
stencil_matches s ge →
Genv.find_funct_ptr ge b = Some (Internal sys_dispatch_function).
Proof.
intros.
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 H; eauto.
destruct H as [?[Hsymbol ?]].
inv H1.
rewrite stencil_matches_symbols in Hsymbol.
rewrite H0 in Hsymbol. inv Hsymbol.
assumption.
Qed.
Lemma Hsendpre:
∀ MCode_Asm s ge,
make_globalenv s MCode_Asm tdispatch = ret ge →
(∃ b, Genv.find_symbol ge trap_sendtochan_pre = Some b
∧ Genv.find_funct_ptr ge b =
Some (External (EF_external trap_sendtochan_pre trap_sendtochan_pre_sig)))
∧ get_layer_primitive trap_sendtochan_pre tdispatch =
OK (Some (gensem trap_sendtochan_pre_spec)).
Proof.
intros.
assert (Hprim: get_layer_primitive trap_sendtochan_pre tdispatch =
OK (Some (gensem trap_sendtochan_pre_spec)))
by reflexivity.
split; try assumption.
eapply make_globalenv_get_layer_primitive; eauto.
Qed.
Lemma Hsendpost:
∀ MCode_Asm s ge,
make_globalenv s MCode_Asm tdispatch = ret ge →
(∃ b, Genv.find_symbol ge trap_sendtochan_post = Some b
∧ Genv.find_funct_ptr ge b =
Some (External (EF_external trap_sendtochan_post null_signature)))
∧ get_layer_primitive trap_sendtochan_post tdispatch =
OK (Some (gensem trap_sendtochan_post_spec)).
Proof.
intros.
assert (Hprim: get_layer_primitive trap_sendtochan_post tdispatch =
OK (Some (gensem trap_sendtochan_post_spec)))
by reflexivity.
split; try assumption.
eapply make_globalenv_get_layer_primitive; eauto.
Qed.
Lemma Hsys_yield:
∀ ge s b,
make_globalenv s (sys_yield ↦ sys_yield_function) tdispatch = ret ge →
find_symbol s sys_yield = Some b →
stencil_matches s ge →
Genv.find_funct_ptr ge b = Some (Internal sys_yield_function).
Proof.
intros.
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 H; eauto.
destruct H as [?[Hsymbol ?]].
inv H1.
rewrite stencil_matches_symbols in Hsymbol.
rewrite H0 in Hsymbol. inv Hsymbol.
assumption.
Qed.
Lemma Hsys_sendtochan_pre:
∀ ge s b,
make_globalenv s (sys_sendtochan_pre ↦ sys_sendtochan_pre_function) tdispatch = ret ge →
find_symbol s sys_sendtochan_pre = Some b →
stencil_matches s ge →
Genv.find_funct_ptr ge b = Some (Internal sys_sendtochan_pre_function).
Proof.
intros.
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 H; eauto.
destruct H as [?[Hsymbol ?]].
inv H1.
rewrite stencil_matches_symbols in Hsymbol.
rewrite H0 in Hsymbol. inv Hsymbol.
assumption.
Qed.
Lemma Hsys_sendtochan_post:
∀ ge s b,
make_globalenv s (sys_sendtochan_post ↦ sys_sendtochan_post_function) tdispatch = ret ge →
find_symbol s sys_sendtochan_post = Some b →
stencil_matches s ge →
Genv.find_funct_ptr ge b = Some (Internal sys_sendtochan_post_function).
Proof.
intros.
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 H; eauto.
destruct H as [?[Hsymbol ?]].
inv H1.
rewrite stencil_matches_symbols in Hsymbol.
rewrite H0 in Hsymbol. inv Hsymbol.
assumption.
Qed.
Lemma Hpgf_handler:
∀ ge s b,
make_globalenv s (pgf_handler ↦ pgf_handler_function) tdispatch = ret ge →
find_symbol s pgf_handler = Some b →
stencil_matches s ge →
Genv.find_funct_ptr ge b = Some (Internal pgf_handler_function).
Proof.
intros.
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 H; eauto.
destruct H as [?[Hsymbol ?]].
inv H1.
rewrite stencil_matches_symbols in Hsymbol.
rewrite H0 in Hsymbol. inv Hsymbol.
assumption.
Qed.
End WITHMEM.
End ASM_DATA.