Library mcertikos.conlib.conmtlib.LAsmAbsDataProperty
Require Import Coqlib.
Require Import Maps.
Require Import ASTExtra.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import MemoryX.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Asm.
Require Import Conventions.
Require Import Machregs.
Require Import AuxLemma.
Require Import liblayers.logic.PTreeModules.
Require Import liblayers.compcertx.MemWithData.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compat.CompatData.
Require Import liblayers.compat.CompatPrimSem.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatExternalCalls.
Require Import Decision.
Require Import GlobIdent.
Require Import CommonTactic.
Require Import Constant.
Require Import PrimSemantics.
Require Import AuxStateDataType.
Require Import AsmImplLemma.
Require Import AsmImplTactic.
Require Import LAsm.
Require Import liblayers.compat.CompatGenSem.
Require Import AlgebraicMem.
Require Import RegsetLessdef.
Section Refinement.
Context {RData}`{data_prf : CompatData RData}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Context `{Hstencil: Stencil}.
Context `{L: compatlayer (cdata RData)}.
Context `{ass_def: !AccessorsDefined L}.
Context `{agmem: !AlgebraicMemory}.
Local Instance : ExternalCallsOps (mwd (cdata RData)) := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance : LayerConfigurationOps := compatlayer_configuration_ops L.
Class LAsmAbsDataProp :=
{
acc_exec_load_nextblock:
∀ (ge: genv) a rs rd rs´ ty (m m´: mwd (cdata RData)),
(acc_exec_load L) fundef unit ge ty m a rs rd = Next rs´ m´ →
(Mem.nextblock m ≤ Mem.nextblock m´)%positive;
acc_exec_store_nextblock:
∀ (ge: genv) a rs rd rs´ ty ST (m m´: mwd (cdata RData)),
(acc_exec_store L) fundef unit ge ty m a rs rd ST = Next rs´ m´ →
(Mem.nextblock m ≤ Mem.nextblock m´)%positive;
acc_exec_load_disjoint_union:
∀ (ge: genv) a rs rd rs´ rs0 ty m m´ m0 gm abd abd´,
(acc_exec_load L) fundef unit ge ty (m, abd) a rs rd = Next rs´ (m´, abd´) →
regset_lessdef rs rs0 →
mem_disjoint_union m m0 gm →
(Mem.nextblock m0 ≤ Mem.nextblock m)%positive →
∃ gm´ rs0´,
(acc_exec_load L) fundef unit ge ty (gm, abd) a rs0 rd = Next rs0´ (gm´, abd´)
∧ mem_disjoint_union m´ m0 gm´
∧ regset_lessdef rs´ rs0´;
acc_exec_store_disjoint_union:
∀ (ge: genv) a rs rd rs´ rs0 ty ST m m´ m0 gm abd abd´,
(acc_exec_store L) fundef unit ge ty (m, abd) a rs rd ST = Next rs´ (m´, abd´) →
mem_disjoint_union m m0 gm →
(Mem.nextblock m0 ≤ Mem.nextblock m)%positive →
∃ gm´ rs0´,
(acc_exec_store L) fundef unit ge ty (gm, abd) a rs0 rd ST = Next rs0´ (gm´, abd´)
∧ mem_disjoint_union m´ m0 gm´
∧ regset_lessdef rs´ rs0´;
exec_external_nextblock´:
∀ (ge: genv) m m´ abd abd´ ef vl t args WB
(BUILTIN_ENABLED : match ef with
| EF_external id _ ⇒
if peq id thread_yield then False
else if peq id thread_sleep then False
else True
| _ ⇒ True
end),
external_call´ WB ef ge args (m, abd) t vl (m´, abd´) →
(Mem.nextblock m ≤ Mem.nextblock m´)%positive;
exec_primitive_nextblock:
∀ (ge: genv) m m´ abd abd´ ef t rs rs´
(BUILTIN_ENABLED : match ef with
| EF_external id _ ⇒
if peq id thread_yield then False
else if peq id thread_sleep then False
else True
| _ ⇒ True
end),
primitive_call ef ge rs (m, abd) t rs´ (m´, abd´) →
(Mem.nextblock m ≤ Mem.nextblock m´)%positive;
exec_external_disjoint_union0´:
∀ (ge: genv) m m´ m0 gm abd abd´ ef vl t args args´ WB
(BUILTIN_ENABLED : match ef with
| EF_external id _ ⇒
if peq id thread_yield then False
else if peq id thread_sleep then False
else True
| _ ⇒ True
end),
external_call´ WB ef ge args (m, abd) t vl (m´, abd´) →
mem_disjoint_union m m0 gm →
(Mem.nextblock m0 ≤ Mem.nextblock m)%positive →
Val.lessdef_list args args´ →
∃ gm´ vl´,
external_call´ WB ef ge args´ (gm, abd) t vl´ (gm´, abd´)
∧ mem_disjoint_union m´ m0 gm´
∧ Val.lessdef_list vl vl´;
exec_primitive_disjoint_union0:
∀ (ge: genv) m m´ m0 gm abd abd´ ef t rs rs0 rs´
(BUILTIN_ENABLED : match ef with
| EF_external id _ ⇒
if peq id thread_yield then False
else if peq id thread_sleep then False
else True
| _ ⇒ True
end),
primitive_call ef ge rs (m, abd) t rs´ (m´, abd´) →
mem_disjoint_union m m0 gm →
(Mem.nextblock m0 ≤ Mem.nextblock m)%positive →
regset_lessdef rs rs0 →
∃ gm´ rs0´,
primitive_call ef ge rs0 (gm, abd) t rs0´ (gm´, abd´)
∧ mem_disjoint_union m´ m0 gm´
∧ regset_lessdef rs´ rs0´
}.
Context `{lasmprop: LAsmAbsDataProp}.
Lemma exec_external_disjoint_union´:
∀ (ge: genv) m m´ m0 gm abd abd´ ef vl t args args´ WB
(BUILTIN_ENABLED : match ef with
| EF_external id _ ⇒
if peq id thread_yield then False
else if peq id thread_sleep then False
else True
| _ ⇒ True
end),
external_call´ WB ef ge args (m, abd) t vl (m´, abd´) →
mem_disjoint_union m m0 gm →
(Mem.nextblock m0 ≤ Mem.nextblock m)%positive →
Val.lessdef_list args args´ →
∃ gm´ vl´,
external_call´ WB ef ge args´ (gm, abd) t vl´ (gm´, abd´)
∧ mem_disjoint_union m´ m0 gm´
∧ (Mem.nextblock m0 ≤ Mem.nextblock m´)%positive
∧ Val.lessdef_list vl vl´.
Proof.
intros. exploit exec_external_disjoint_union0´; eauto.
intros (gm´ & vl´ & Hexe & Hdis & Hreg).
refine_split´; eauto.
eapply exec_external_nextblock´ in H; eauto.
lift_unfold. xomega.
Qed.
Lemma exec_primitive_disjoint_union:
∀ (ge: genv) m m´ m0 gm abd abd´ ef t rs rs0 rs´
(BUILTIN_ENABLED : match ef with
| EF_external id _ ⇒
if peq id thread_yield then False
else if peq id thread_sleep then False
else True
| _ ⇒ True
end),
primitive_call ef ge rs (m, abd) t rs´ (m´, abd´) →
mem_disjoint_union m m0 gm →
(Mem.nextblock m0 ≤ Mem.nextblock m)%positive →
regset_lessdef rs rs0 →
∃ gm´ rs0´,
primitive_call ef ge rs0 (gm, abd) t rs0´ (gm´, abd´)
∧ mem_disjoint_union m´ m0 gm´
∧ (Mem.nextblock m0 ≤ Mem.nextblock m´)%positive
∧ regset_lessdef rs´ rs0´.
Proof.
intros. exploit exec_primitive_disjoint_union0; eauto.
intros (gm´ & rs0´ & Hexe & Hdis & Hreg).
refine_split´; eauto.
eapply exec_primitive_nextblock in H; eauto.
lift_unfold. xomega.
Qed.
Lemma goto_label_nextblock :
∀ f i rs rs´ (m m´: mwd (cdata RData)),
goto_label f i rs m = Next rs´ m´ →
(Mem.nextblock m ≤ Mem.nextblock m´)%positive.
Proof.
unfold goto_label. intros.
subdestruct; inv H. reflexivity.
Qed.
Lemma asm_exec_instr_nextblock :
∀ (ge: genv) f (i : Asm.instruction) rs rs´ (m m´: mwd (cdata RData)),
exec_instr ge f i rs m = Next rs´ m´ →
(Mem.nextblock m ≤ Mem.nextblock m´)%positive.
Proof.
intros.
destruct i; simpl in H;
try (subdestruct; inv H; try reflexivity;
eauto using acc_exec_load_nextblock, acc_exec_store_nextblock;
eapply goto_label_nextblock; eauto; fail).
- lift_unfold; simpl in H.
destruct m, m´; subst; simpl in H.
subdestruct. inv H.
eapply Mem.nextblock_store in Hdestruct0.
eapply Mem.nextblock_store in Hdestruct1.
eapply Mem.nextblock_alloc in Hdestruct.
rewrite Hdestruct1.
rewrite Hdestruct0.
rewrite Hdestruct.
xomega.
- subdestruct.
destruct m, m´; simpl in H. inv H.
lift_unfold.
destruct Hdestruct2 as (Hfree & _).
eapply Mem.nextblock_free in Hfree.
rewrite Hfree. reflexivity.
Qed.
Lemma exec_instr_nextblock:
∀ (ge: genv) f i rs rs´ (m m´: mwd (cdata RData)),
exec_instr ge f i rs m = Next rs´ m´ →
(Mem.nextblock m ≤ Mem.nextblock m´)%positive.
Proof.
intros.
destruct m; destruct m´; subst.
destruct i; simpl in H;
try (subdestruct; inv H; try reflexivity;
eauto using acc_exec_load_nextblock, acc_exec_store_nextblock; fail).
eapply asm_exec_instr_nextblock; eauto.
Qed.
Lemma volatile_store_nextblock:
∀ WB (ge: genv) chunk m m´ d d´ b ofs v t,
volatile_store (mem:= mwd(cdata RData)) WB ge chunk (m, d) b ofs v t (m´, d´) →
(Mem.nextblock m ≤ Mem.nextblock m´)%positive.
Proof.
intros. inv H.
- reflexivity.
- eapply Mem.nextblock_store in H1. lift_unfold.
rewrite H1. reflexivity.
Qed.
Lemma exec_external_nextblock:
∀ (ge: genv) WB ef args t vl (m m´: mwd (cdata RData)),
external_call´ WB ef ge args m t vl m´ →
∀ (BUILTIN_ENABLED : match ef with
| EF_external _ _ ⇒ False
| _ ⇒ True
end),
(Mem.nextblock m ≤ Mem.nextblock m´)%positive.
Proof.
intros.
destruct m, m´. inv H.
destruct ef; try contradiction;
try (inv H0; reflexivity; fail).
+ inv H0. lift_unfold. eapply volatile_store_nextblock; eauto.
+ inv H0. lift_unfold. eapply volatile_store_nextblock; eauto.
+ inv H0.
eapply Mem.nextblock_alloc in H1.
eapply Mem.nextblock_store in H2.
rewrite H2. rewrite H1. xomega.
+ inv H0.
eapply Mem.nextblock_free in H3.
rewrite H3. reflexivity.
+ inv H0.
eapply Mem.nextblock_storebytes in H8.
rewrite H8. reflexivity.
Qed.
Lemma asm_exec_instr_disjoint_union:
∀ (ge: genv) f (i : Asm.instruction) rs rs´ rs0 m m´ m0 gm abd abd´,
exec_instr (mem:= mwd (cdata RData)) ge f i rs (m, abd) = Next rs´ (m´, abd´) →
mem_disjoint_union m m0 gm →
(Mem.nextblock m0 ≤ Mem.nextblock m)%positive →
regset_lessdef rs rs0 →
∃ gm´ rs0´,
exec_instr ge f i rs0 (gm, abd) = Next rs0´ (gm´, abd´)
∧ mem_disjoint_union m´ m0 gm´
∧ regset_lessdef rs´ rs0´.
Proof.
intros; simpl in ×.
destruct i eqn: Hi; simpl in *;
try (inv H; refine_split´; auto; regset_lessdef_solve_tac; fail);
try (eauto using acc_exec_load_disjoint_union, acc_exec_store_disjoint_union; fail).
- subdestruct.
eapply (Val_divu_lessdef (rs0 EAX) (rs0 # EDX <- Vundef r1)) in Hdestruct;
regset_lessdef_solve_tac.
destruct Hdestruct as (v´ & Hdiv & Hless). rewrite Hdiv.
eapply (Val_modu_lessdef (rs0 EAX) (rs0 # EDX <- Vundef r1)) in Hdestruct0;
regset_lessdef_solve_tac.
destruct Hdestruct0 as (v´´ & Hmod & Hless´). rewrite Hmod.
inv H; refine_split´; auto; regset_lessdef_solve_tac.
- subdestruct.
eapply (Val_divs_lessdef (rs0 EAX) (rs0 # EDX <- Vundef r1)) in Hdestruct;
regset_lessdef_solve_tac.
destruct Hdestruct as (v´ & Hdiv & Hless). rewrite Hdiv.
eapply (Val_mods_lessdef (rs0 EAX) (rs0 # EDX <- Vundef r1)) in Hdestruct0;
regset_lessdef_solve_tac.
destruct Hdestruct0 as (v´´ & Hmod & Hless´). rewrite Hmod.
inv H; refine_split´; auto; regset_lessdef_solve_tac.
- destruct (eval_testcond c rs) eqn:Heval.
+ eapply regset_lessdef_eval_testcond in Heval; eauto.
rewrite Heval.
destruct b; inv H; refine_split´; auto; regset_lessdef_solve_tac.
+ inv H.
destruct (eval_testcond c rs0); try destruct b;
refine_split´; auto; regset_lessdef_solve_tac.
eapply regset_lessdef_set_undef. assumption.
- inv H; refine_split´; auto; regset_lessdef_solve_tac.
eapply Val.of_optbool_lessdef. intros.
eapply regset_lessdef_eval_testcond; eauto.
- inv H; refine_split´; auto; regset_lessdef_solve_tac.
eapply compare_floats_lessdef; eauto.
- eapply goto_label_disjoint_union; eauto.
- destruct (eval_testcond c rs) eqn:Heval.
+ eapply regset_lessdef_eval_testcond in Heval; eauto.
rewrite Heval.
destruct b.
× eapply goto_label_disjoint_union; eauto.
× inv H; refine_split´; auto; regset_lessdef_solve_tac.
+ inv H.
- destruct (eval_testcond c1 rs) eqn:Heval; try (inv H; fail).
eapply regset_lessdef_eval_testcond in Heval; eauto.
rewrite Heval.
destruct b.
× destruct (eval_testcond c2 rs) eqn:Heval´; try (inv H; fail).
eapply regset_lessdef_eval_testcond in Heval´; eauto.
rewrite Heval´.
destruct b.
{ eapply goto_label_disjoint_union; eauto. }
{ inv H; refine_split´; auto; regset_lessdef_solve_tac. }
× destruct (eval_testcond c2 rs) eqn:Heval´; try (inv H; fail).
eapply regset_lessdef_eval_testcond in Heval´; eauto.
rewrite Heval´.
inv H; refine_split´; auto; regset_lessdef_solve_tac.
- pose proof (H2 r) as Hr.
destruct (rs r); contra_inv. inv Hr.
subdestruct.
eapply goto_label_disjoint_union; eauto.
- lift_unfold; simpl in ×.
destruct (Mem.alloc m 0 sz) eqn: Halloc. simpl in H.
exploit mem_alloc_disjoint_union; eauto. intros (gm1 & Halloc1 & Hunion1 & Hnble1).
rewrite Halloc1. simpl.
destruct (Mem.store Mint32 m1 b (Int.unsigned (Int.add Int.zero ofs_link)) (rs ESP)) eqn: Hstore;
[simpl in H | inversion H].
exploit mem_store_disjoint_union; eauto. intros (gm2 & Hstore2 & Hunion2).
rewrite Hstore2. simpl.
destruct (Mem.store Mint32 m2 b (Int.unsigned (Int.add Int.zero ofs_ra)) (rs RA)) eqn: Hstore´;
[inversion H; subst; auto | inversion H].
exploit mem_store_disjoint_union; eauto. intros (gm3 & Hstore3 & Hunion3).
rewrite Hstore3. inv H. unfold set; simpl.
refine_split´; auto. regset_lessdef_solve_tac.
- pose proof (H2 ESP) as Hesp.
destruct (rs ESP); simpl in H; contra_inv. inv Hesp. simpl.
lift_unfold.
destruct (Mem.load Mint32 m b (Int.unsigned (Int.add i0 ofs_ra))) eqn: Hload; [ | inversion H].
exploit mem_load_disjoint_union; eauto. intros (v0 & Hload0 & Hless0).
rewrite Hload0.
destruct (Mem.load Mint32 m b (Int.unsigned (Int.add i0 ofs_link))) eqn: Hload´; [ | inversion H].
clear Hload0.
exploit mem_load_disjoint_union; eauto. intros (v0´ & Hload0´ & Hless0´).
rewrite Hload0´.
destruct (Mem.free m b 0 sz) eqn: Hfree; inv H.
exploit mem_free_disjoint_union; eauto. intros (gm´ & Hfree´ & Hunion´).
rewrite Hfree´. unfold set; simpl.
refine_split´; auto.
{ regset_lessdef_solve_tac. }
Qed.
Lemma exec_instr_disjoint_union0:
∀ ge f i rs rs0 rs´ m m´ m0 gm abd abd´,
exec_instr ge f i rs (m, abd) = Next rs´ (m´, abd´) →
mem_disjoint_union m m0 gm →
(Mem.nextblock m0 ≤ Mem.nextblock m)%positive →
regset_lessdef rs rs0 →
∃ gm´ rs0´,
exec_instr ge f i rs0 (gm, abd) = Next rs0´ (gm´, abd´)
∧ mem_disjoint_union m´ m0 gm´
∧ regset_lessdef rs´ rs0´.
Proof.
intros.
destruct i eqn: Hi;
simpl in *; try (inv H; refine_split´; eauto; regset_lessdef_solve_tac; fail);
eauto using acc_exec_load_disjoint_union, acc_exec_store_disjoint_union.
eapply asm_exec_instr_disjoint_union; eauto.
Qed.
Lemma exec_instr_disjoint_union:
∀ ge f i rs rs0 rs´ m m´ m0 gm abd abd´,
exec_instr ge f i rs (m, abd) = Next rs´ (m´, abd´) →
mem_disjoint_union m m0 gm →
(Mem.nextblock m0 ≤ Mem.nextblock m)%positive →
regset_lessdef rs rs0 →
∃ gm´ rs0´,
exec_instr ge f i rs0 (gm, abd) = Next rs0´ (gm´, abd´)
∧ mem_disjoint_union m´ m0 gm´
∧ (Mem.nextblock m0 ≤ Mem.nextblock m´)%positive
∧ regset_lessdef rs´ rs0´.
Proof.
intros. exploit exec_instr_disjoint_union0; eauto.
intros (gm´ & rs0´ & Hexec & Hdis & Hreg).
refine_split´; eauto.
eapply exec_instr_nextblock in H. lift_unfold. xomega.
Qed.
Lemma volatile_load_disjoint_union:
∀ (ge: genv) chunk m m0 gm abd b ofs t v,
volatile_load (mem:= mwd (cdata RData)) ge chunk (m, abd) b ofs t v →
mem_disjoint_union m m0 gm →
(Mem.nextblock m0 ≤ Mem.nextblock m)%positive →
∃ v´,
volatile_load ge chunk (gm, abd) b ofs t v´
∧ Val.lessdef v v´.
Proof.
intros. inv H.
- refine_split´; eauto. econstructor; eauto.
- lift_unfold.
exploit mem_load_disjoint_union; eauto.
intros (v´ & Hload & Hless).
refine_split´; eauto. econstructor; eauto.
Qed.
Lemma volatile_store_disjoint_union:
∀ WB (ge: genv) chunk m m´ m0 gm abd abd´ b ofs t v v´,
volatile_store (mem:= mwd (cdata RData)) WB ge chunk (m, abd) b ofs v t (m´, abd´) →
mem_disjoint_union m m0 gm →
(Mem.nextblock m0 ≤ Mem.nextblock m)%positive →
Val.lessdef v v´ →
∃ gm´,
volatile_store WB ge chunk (gm, abd) b ofs v´ t (gm´, abd´)
∧ mem_disjoint_union m´ m0 gm´.
Proof.
intros. inv H.
- refine_split´; eauto. econstructor; eauto.
eapply eventval_match_lessdef; eauto.
Val_lessdef_solve_tac.
- lift_unfold. destruct H4 as (Hst & Heq). inv Heq.
exploit mem_store_disjoint_union; eauto.
intros (gm´ & Hstore´ & Hunion).
refine_split´; eauto. econstructor; eauto.
lift_unfold; eauto.
Qed.
Local Transparent decode_longs.
Lemma decode_longs_l_lessdef vs1 vs2 v1:
v1 :: nil = decode_longs (sig_args SelectLong.sig_l_l) vs1 →
Val.lessdef_list vs1 vs2 →
∃ v2,
v2 :: nil = decode_longs (sig_args SelectLong.sig_l_l) vs2 ∧
Val.lessdef v1 v2.
Proof.
intros Hv1 Hvs.
destruct Hvs as [ | ? ? ? ? ? [ | ? ? ? ? ? [ | ? ? ? ? ? Hvs]]];
inv Hv1; simpl; eauto using Val.longofwords_lessdef.
Qed.
Lemma decode_longs_ll_lessdef vs1 vs2 x1 y1:
x1 :: y1 :: nil = decode_longs (sig_args SelectLong.sig_ll_l) vs1 →
Val.lessdef_list vs1 vs2 →
∃ x2 y2,
x2 :: y2 :: nil = decode_longs (sig_args SelectLong.sig_ll_l) vs2 ∧
Val.lessdef x1 x2 ∧
Val.lessdef y1 y2.
Proof.
intros Hxy1 Hvs.
simpl in ×.
repeat (destruct Hvs as [ | ? ? ? ? ? Hvs]; [ discriminate | ]).
∃ (Val.longofwords v2 v3).
destruct Hvs; inv Hxy1; eauto using Val.longofwords_lessdef.
inv Hvs.
∃ (Val.longofwords v5 v7).
eauto using Val.longofwords_lessdef.
Qed.
Lemma decode_longs_i_lessdef vs1 vs2 x1:
x1 :: nil = decode_longs (Tint :: nil) vs1 →
Val.lessdef_list vs1 vs2 →
∃ x2,
x2 :: nil = decode_longs (Tint :: nil) vs2 ∧
Val.lessdef x1 x2.
Proof.
intros Hxy1 Hvs.
simpl in ×.
repeat (destruct Hvs as [ | ? ? ? ? ? Hvs]; [ discriminate | ]).
inv Hxy1.
inv Hvs.
eauto.
Qed.
Lemma decode_longs_ii_lessdef vs1 vs2 x1 y1:
x1 :: y1 :: nil = decode_longs (sig_args SelectLong.sig_ii_l) vs1 →
Val.lessdef_list vs1 vs2 →
∃ x2 y2,
x2 :: y2 :: nil = decode_longs (sig_args SelectLong.sig_ii_l) vs2 ∧
Val.lessdef x1 x2 ∧
Val.lessdef y1 y2.
Proof.
intros Hxy1 Hvs.
simpl in ×.
repeat (destruct Hvs as [ | ? ? ? ? ? Hvs]; [ discriminate | ]).
inv Hxy1.
inv Hvs.
eauto.
Qed.
Local Opaque decode_longs.
Lemma exec_external_disjoint_union0:
∀ (ge: genv) m m´ m0 gm abd abd´ ef vl t args args´ WB
(BUILTIN_ENABLED : match ef with
| EF_external _ _ ⇒ False
| _ ⇒ True
end),
external_call´ WB ef ge args (m, abd) t vl (m´, abd´) →
mem_disjoint_union m m0 gm →
(Mem.nextblock m0 ≤ Mem.nextblock m)%positive →
Val.lessdef_list args args´ →
∃ gm´ vl´,
external_call´ WB ef ge args´ (gm, abd) t vl´ (gm´, abd´)
∧ mem_disjoint_union m´ m0 gm´
∧ Val.lessdef_list vl vl´.
Proof.
intros; simpl in ×.
destruct H as [v Hstep Hvres]; subst.
destruct ef; destruct BUILTIN_ENABLED; inv Hstep; simpl;
lazymatch goal with
| H: _ :: nil = decode_longs (sig_args SelectLong.sig_l_l) _ |- _ ⇒
edestruct (decode_longs_l_lessdef _ _ _ H H2) as (? & Hdl & ?);
clear H H2
| H: _ :: _ :: nil = decode_longs (sig_args SelectLong.sig_ll_l) _ |- _ ⇒
edestruct (decode_longs_ll_lessdef _ _ _ _ H H2) as (?&? & Hdl & ?&?);
clear H H2
| H: _ :: nil = decode_longs (Tint :: nil) _ |- _ ⇒
edestruct (decode_longs_i_lessdef _ _ _ H H2) as (? & Hdl & ?);
clear H H2
| H: _ :: _ :: nil = decode_longs (sig_args SelectLong.sig_ii_l) _ |- _ ⇒
edestruct (decode_longs_ii_lessdef _ _ _ _ H H2) as (?&? & Hdl & ?&?);
clear H H2
| _ ⇒ idtac
end.
- refine_split´.
+ econstructor; eauto.
simpl in Hdl |- *; rewrite <- Hdl.
eapply CompCertBuiltins.builtin_sem_i64_neg; eauto.
+ eassumption.
+ Val_lessdef_list_solve_tac.
- refine_split´.
+ econstructor; eauto.
simpl in Hdl |- *; rewrite <- Hdl.
eapply CompCertBuiltins.builtin_sem_i64_add; eauto.
+ eassumption.
+ Val_lessdef_list_solve_tac.
- refine_split´.
+ econstructor; eauto.
simpl in Hdl |- *; rewrite <- Hdl.
eapply CompCertBuiltins.builtin_sem_i64_sub; eauto.
+ eassumption.
+ Val_lessdef_list_solve_tac.
- refine_split´.
+ econstructor; eauto.
simpl in Hdl |- *; rewrite <- Hdl.
eapply CompCertBuiltins.builtin_sem_i64_mul; eauto.
+ eassumption.
+ Val_lessdef_list_solve_tac.
- destruct args´; try discriminate.
destruct args´; try discriminate.
exploit volatile_load_disjoint_union; eauto.
intros (v´ & Hload & Hless).
refine_split´; try eassumption.
+ econstructor; eauto.
simpl in Hdl |- *; rewrite <- Hdl.
inversion H3.
econstructor; eauto.
+ simpl; destruct (type_of_chunk chunk);
Val_lessdef_list_solve_tac.
- exploit (decode_longs_lessdef (Tint :: type_of_chunk_use chunk :: nil)); eauto.
rewrite <- H. intros Hless.
destruct (decode_longs (Tint :: type_of_chunk_use chunk :: nil) args´) eqn: Hde;
inv_val_inject. inv H7.
exploit volatile_store_disjoint_union; eauto.
intros (gm´ & Hst & Hunion).
refine_split´; try eassumption.
+ econstructor; trivial.
simpl. rewrite Hde.
econstructor; eauto.
+ Val_lessdef_list_solve_tac.
- destruct args; try discriminate.
inv H2.
exploit volatile_load_disjoint_union; eauto.
intros (v´ & Hload & Hless).
refine_split´; try eassumption.
+ econstructor; trivial.
econstructor; eauto.
+ simpl; destruct (type_of_chunk chunk);
Val_lessdef_list_solve_tac.
- exploit (decode_longs_lessdef (type_of_chunk_use chunk :: nil)); eauto.
rewrite <- H. intros Hless.
destruct (decode_longs (type_of_chunk_use chunk :: nil) args´) eqn: Hde;
inv_val_inject.
exploit volatile_store_disjoint_union; eauto.
intros (gm´ & Hst & Hunion).
refine_split´; try eassumption.
+ econstructor; trivial.
simpl. rewrite Hde.
econstructor; eauto.
+ Val_lessdef_list_solve_tac.
- destruct args´; try discriminate.
destruct args´; try discriminate.
destruct m´0; lift_unfold. destruct H4 as (Halloc & Heq). subst.
destruct H3 as (Hst & Heq). subst.
exploit mem_alloc_disjoint_union; eauto.
intros (gm1 & Halloc1 & Hunion1 & Hnb1).
exploit mem_store_disjoint_union; eauto.
intros (gm2 & Hst2 & Hunion2).
refine_split´; try eassumption.
+ econstructor; trivial.
simpl. rewrite <- Hdl.
inv H5.
econstructor; eauto.
instantiate (1:= b).
instantiate (1:= (gm1, abd´)).
lift_unfold. split; eauto.
lift_unfold. split; eauto.
+ Val_lessdef_list_solve_tac.
- destruct args´; try discriminate.
destruct args´; try discriminate.
exploit (decode_longs_lessdef (Tint :: nil)); eauto.
inv_val_inject.
lift_unfold. destruct H5 as (Hfree & Heq). subst.
exploit mem_load_disjoint_union; eauto.
intros (v´ & Hload & Hless). inv Hless.
exploit mem_free_disjoint_union; eauto.
intros (gm´ & Hfree´ & Hunion´).
refine_split´; try eassumption.
+ econstructor; trivial.
simpl. rewrite <- Hdl.
econstructor; eauto.
lift_unfold. split; eauto.
+ Val_lessdef_list_solve_tac.
- exploit (decode_longs_lessdef (Tint :: Tint :: nil)); eauto.
rewrite <- H. intros Hless.
destruct (decode_longs (Tint :: Tint :: nil) args´) eqn: Hde;
inv_val_inject. inv H13. inv H14.
lift_unfold. destruct H10 as (Hstore & Heq). subst.
exploit mem_loadbytes_disjoint_union; eauto.
intros (bytes´ & Hload & Hless).
exploit mem_storebytes_disjoint_union; eauto.
intros (gm´ & Hstore´ & Hunion´).
refine_split´; try eassumption.
+ econstructor; trivial.
simpl. rewrite Hde.
econstructor; eauto.
lift_unfold. split; eauto.
+ Val_lessdef_list_solve_tac.
- exploit (decode_longs_lessdef (sig_args (ef_sig (EF_annot text targs)))); eauto.
intros Hless.
exploit eventval_list_match_lessdef; eauto. intros.
refine_split´; try eassumption.
+ econstructor; trivial.
econstructor; eauto.
+ Val_lessdef_list_solve_tac.
- exploit (decode_longs_lessdef (targ::nil)); eauto.
rewrite <- H. intros Hless.
destruct (decode_longs (targ :: nil) args´) eqn: Hde;
inv_val_inject.
refine_split´; try eassumption.
+ econstructor; trivial.
simpl. rewrite Hde.
econstructor; eauto.
eapply eventval_match_lessdef; eauto.
+ simpl. destruct targ; Val_lessdef_list_solve_tac.
Qed.
Lemma exec_external_disjoint_union:
∀ (ge: genv) m m´ m0 gm abd abd´ ef vl t args args´ WB
(BUILTIN_ENABLED : match ef with
| EF_external _ _ ⇒ False
| _ ⇒ True
end),
external_call´ WB ef ge args (m, abd) t vl (m´, abd´) →
mem_disjoint_union m m0 gm →
(Mem.nextblock m0 ≤ Mem.nextblock m)%positive →
Val.lessdef_list args args´ →
∃ gm´ vl´,
external_call´ WB ef ge args´ (gm, abd) t vl´ (gm´, abd´)
∧ mem_disjoint_union m´ m0 gm´
∧ (Mem.nextblock m0 ≤ Mem.nextblock m´)%positive
∧ Val.lessdef_list vl vl´.
Proof.
intros. exploit exec_external_disjoint_union0; eauto.
intros (gm´ & vl´ & Hexe & Hdis & Hless).
refine_split´; eauto.
eapply exec_external_nextblock in H; eauto.
lift_unfold. xomega.
Qed.
Lemma exec_external_disjoint_union_regset:
∀ (ge: genv) m m´ m0 gm abd abd´ ef vl t rs rs0 args WB
(BUILTIN_ENABLED : match ef with
| EF_external _ _ ⇒ False
| _ ⇒ True
end),
external_call´ WB ef ge (map rs args) (m, abd) t vl (m´, abd´) →
mem_disjoint_union m m0 gm →
(Mem.nextblock m0 ≤ Mem.nextblock m)%positive →
regset_lessdef rs rs0 →
∃ gm´ vl´,
external_call´ WB ef ge (map rs0 args) (gm, abd) t vl´ (gm´, abd´)
∧ mem_disjoint_union m´ m0 gm´
∧ (Mem.nextblock m0 ≤ Mem.nextblock m´)%positive
∧ Val.lessdef_list vl vl´.
Proof.
intros. eapply exec_external_disjoint_union; eauto.
eapply regset_lessdef_imply_list_lessdef; eauto.
Qed.
Lemma annot_arg_disjoint_union:
∀ args rs rs0 m m0 gm vargs,
annot_arg (mem:= mem) rs m args vargs →
mem_disjoint_union m m0 gm →
regset_lessdef rs rs0 →
∃ vargs´,
annot_arg (mem:= mem) rs0 gm args vargs´
∧ Val.lessdef vargs vargs´.
Proof.
intros. destruct args.
- inv H. refine_split´; eauto. constructor.
- inv H. lift_unfold.
exploit mem_load_disjoint_union; eauto.
intros (v´ & Hload & Hless).
refine_split´; eauto. econstructor.
+ eapply regset_lessdef_eq; eauto. congruence.
+ lift_unfold. assumption.
Qed.
Lemma annot_arguments_disjoint_union:
∀ args rs rs0 m m0 gm vargs,
annot_arguments (mem:= mem) rs m args vargs →
mem_disjoint_union m m0 gm →
regset_lessdef rs rs0 →
∃ vargs´,
annot_arguments (mem:= mem) rs0 gm args vargs´
∧ Val.lessdef_list vargs vargs´.
Proof.
induction 1; intros.
- refine_split´; constructor.
- exploit IHlist_forall2; eauto.
intros (vargs´ & Hargs & Hless).
exploit annot_arg_disjoint_union; eauto.
intros (b´ & Harg & Hless´).
∃ (b´ :: vargs´).
split; constructor; eauto.
Qed.
Lemma extcall_arg_disjoint_union:
∀ vl args rs rs0 m m0 gm,
extcall_arg (mem:= mem) rs m vl args →
mem_disjoint_union m m0 gm →
regset_lessdef rs rs0 →
∃ args´,
extcall_arg rs0 gm vl args´ ∧
Val.lessdef args args´.
Proof.
intros. destruct vl.
- inv H. refine_split´; eauto. constructor.
- inv H. pose proof (H1 ESP) as Hesp.
destruct (rs ESP); contra_inv.
Local Opaque Z.mul.
simpl in ×.
lift_unfold.
exploit mem_load_disjoint_union; eauto.
intros (v´ & Hload & Hless).
refine_split´; eauto. econstructor; eauto.
inv Hesp. simpl. lift_unfold. assumption.
Local Transparent Z.mul.
Qed.
Lemma extcall_args_disjoint_union:
∀ vl args rs rs0 m m0 gm,
list_forall2 (extcall_arg (mem:= mem) rs m) vl args →
mem_disjoint_union m m0 gm →
regset_lessdef rs rs0 →
∃ args´,
list_forall2 (extcall_arg rs0 gm) vl args´ ∧
Val.lessdef_list args args´.
Proof.
induction 1; intros.
- refine_split´; eauto. constructor.
- exploit IHlist_forall2; eauto.
intros (args´ & Hlist & Hless).
exploit extcall_arg_disjoint_union; eauto.
intros (b´ & Harg & Hless´).
∃ (b´ :: args´).
split; constructor; eauto.
Qed.
Lemma extcall_arguments_disjoint_union:
∀ args sig rs rs0 m m0 gm,
extcall_arguments (mem:= mem) rs m sig args →
mem_disjoint_union m m0 gm →
regset_lessdef rs rs0 →
∃ args´,
extcall_arguments (mem:= mem) rs0 gm sig args´
∧ Val.lessdef_list args args´.
Proof.
unfold extcall_arguments. intros.
eapply extcall_args_disjoint_union; eauto.
Qed.
End Refinement.