diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-05-31 17:57:01 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-05-31 17:57:01 +0200 |
| commit | 16859dc21531591f575bcfe747f520c334f418f9 (patch) | |
| tree | f2353c010bbd603529371c460e585cd8a81ef6cb /scheduling/BTLmatchRTL.v | |
| parent | 271f87ba08f42340900378c0797511d4071fc1b8 (diff) | |
| download | compcert-kvx-16859dc21531591f575bcfe747f520c334f418f9.tar.gz compcert-kvx-16859dc21531591f575bcfe747f520c334f418f9.zip | |
prove fsem2cfgsem_ibistep_simu
Diffstat (limited to 'scheduling/BTLmatchRTL.v')
| -rw-r--r-- | scheduling/BTLmatchRTL.v | 32 |
1 files changed, 13 insertions, 19 deletions
diff --git a/scheduling/BTLmatchRTL.v b/scheduling/BTLmatchRTL.v index 8081b3a6..439ba9cc 100644 --- a/scheduling/BTLmatchRTL.v +++ b/scheduling/BTLmatchRTL.v @@ -32,12 +32,12 @@ Local Hint Resolve tr_inputs_lessdef init_regs_lessdef_preserv find_function_les lessdef_state_refl: core. Local Hint Unfold regs_lessdef: core. -Lemma fsem2cfgsem_ibistep_simu ge sp rs1 m1 rs1' m1' of - rs2 m2 ib - (ISTEP: iblock_istep ge sp rs1 m1 ib rs1' m1' of) +Lemma fsem2cfgsem_ibistep_simu ge sp rs1 m1 rs1' m1' of ib + (ISTEP: iblock_istep ge sp rs1 m1 ib rs1' m1' of): forall + rs2 m2 (REGS: forall r, Val.lessdef rs1#r rs2#r) - (MEMS: Mem.extends m1 m2) - : exists rs2' m2', iblock_istep_run ge sp ib rs2 m2 = Some (out rs2' m2' of) + (MEMS: Mem.extends m1 m2), + exists rs2' m2', iblock_istep_run ge sp ib rs2 m2 = Some (out rs2' m2' of) /\ (forall r, Val.lessdef rs1'#r rs2'#r) /\ (Mem.extends m1' m2'). Proof. @@ -63,20 +63,14 @@ Proof. destruct (iblock_istep_run _ _ _ _ _); try congruence. destruct o, _fin; simpl in *; try congruence. eauto. - (* Bseq continue *) - - (* TODO gourdinl induction pb? - exploit IHISTEP1; eauto. intros (rs3 & m3 & IBIS1 & REGS1 & MEMS1). - rewrite IBIS1; simpl. rewrite iblock_istep_run_equiv in ISTEP2. - exploit IHISTEP2; eauto. intros (rs4 & m4 & IBIS2 & REGS2 & MEMS2). - destruct o, _fin; simpl in *; try congruence; try_simplify_someHyps. - intros; apply IHISTEP1 in MEMS; auto. - exploit IHISTEP2; eauto. intros (rs3 & m3 & IBIS1 & REGS1 & MEMS1). - - - destruct (iblock_istep_run _ _ _ _ _) eqn:EQb1. - 2: { rewrite iblock_istep_run_equiv in ISTEP1. destruct b1; simpl in *; try congruence. - destruct o, _fin; simpl in *; try congruence; try_simplify_someHyps.*) -Admitted. + exploit IHISTEP1; eauto. + clear ISTEP1 REGS MEMS. + intros (rs3 & m3 & ISTEP3 & REGS3 & MEMS3). + rewrite ISTEP3; simpl. rewrite iblock_istep_run_equiv in ISTEP2. + exploit IHISTEP2; eauto. + - (* Bcond *) + erewrite (@eval_condition_lessdef cond (rs ## args)); eauto. +Qed. Local Hint Constructors lessdef_stackframe lessdef_state final_step list_forall2 step: core. |