From 16859dc21531591f575bcfe747f520c334f418f9 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Mon, 31 May 2021 17:57:01 +0200 Subject: prove fsem2cfgsem_ibistep_simu --- scheduling/BTLmatchRTL.v | 32 +++++++++++++------------------- 1 file changed, 13 insertions(+), 19 deletions(-) (limited to 'scheduling/BTLmatchRTL.v') 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. -- cgit