diff options
author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-31 21:26:19 +0200 |
---|---|---|
committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-31 21:26:19 +0200 |
commit | c4344192eca7711e5b781fd0cac9780c9691a881 (patch) | |
tree | 8cb5518a56068f3092def0ea1a5357af0dd9b064 | |
parent | 1e3b0a8b86fb661c66ebdacdc0f1ff42aa25a3b0 (diff) | |
parent | 16859dc21531591f575bcfe747f520c334f418f9 (diff) | |
download | compcert-kvx-c4344192eca7711e5b781fd0cac9780c9691a881.tar.gz compcert-kvx-c4344192eca7711e5b781fd0cac9780c9691a881.zip |
Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into BTL
-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. |