essais

1 files changed, 31 insertions, 16 deletions

diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v
index 8f892020..ef640d22 100644
--- a/scheduling/BTLtoRTLproof.v
+++ b/scheduling/BTLtoRTLproof.v
@@ -106,6 +106,12 @@ Proof.
   intros. inv H0. inv H. inv STACKS. constructor.
 Qed.
 
+Definition is_goto (i: final): option exit :=
+  match i with
+  | Bgoto pc => Some pc
+  | _ => None
+  end.
+
 (* suggestion *)
 Lemma iblock_istep_simulation sp dupmap stack' f' rs0 m0 ib rs1 m1 ofin
  (IBIS: iblock_istep ge sp rs0 m0 ib rs1 m1 ofin):
@@ -114,11 +120,14 @@ Lemma iblock_istep_simulation sp dupmap stack' f' rs0 m0 ib rs1 m1 ofin
  ,
   match ofin with 
   | None => exists pc1,(opc = Some pc1) /\ plus RTL.step tge (RTL.State stack' f' sp pc0 rs0 m0) E0 (RTL.State stack' f' sp pc1 rs1 m1)
-  | Some fin => True (* TODO: A CHANGER *)
+  | Some fin =>
+     (* A CHANGER ? *)
+     exists isfst' pc1, match_iblock dupmap (RTL.fn_code f') isfst' pc1 fin opc
+                /\ star RTL.step tge (RTL.State stack' f' sp pc0 rs0 m0) E0 (RTL.State stack' f' sp pc1 rs1 m1)
   end.
 Proof.
-  induction IBIS; simpl; auto;
-  intros.
+  induction IBIS; simpl; intros.
+  - repeat econstructor; eauto.
   - inv MIB. exists pc'; split; auto.
     apply plus_one. apply exec_Inop; trivial.
   - inv MIB. exists pc'; split; auto.
@@ -133,19 +142,25 @@ Proof.
     apply plus_one. eapply exec_Istore; eauto.
     erewrite <- eval_addressing_preserved; eauto.
     intros; rewrite symbols_preserved; trivial.
-  - 
-    destruct ofin; simpl; auto.
-    inv MIB.
-    admit.
-    (*eexists; split; auto.*)
-    (*apply IHIBIS2.*)
-    (*inv MIB. exists pc'; split; auto.*)
-    (*apply plus_one. eapply exec_Istore; eauto.*)
-    (*erewrite <- eval_addressing_preserved; eauto.*)
-    (*intros; rewrite symbols_preserved; trivial.*)
-  - destruct ofin; simpl; auto. inv MIB.
-    destruct b.
-    eapply IHIBIS.
+  - inv MIB.
+    exploit IHIBIS; eauto.
+    intros (isfst' & pc1 & M1 & STAR).
+    inv M1.
+  - inv MIB.
+    exploit IHIBIS1; eauto.
+    intros (pc1 & EQpc1 & STEP1); inv EQpc1.
+    exploit IHIBIS2; eauto.
+    destruct ofin; simpl.
+    + intros (ifst2 & pc2 & M2 & STEP2).
+      repeat eexists; eauto.
+      eapply star_trans; eauto.
+      eapply plus_star; eauto.
+      eauto.
+    + intros (pc2 & EQpc2 & STEP2); inv EQpc2.
+      eexists; split; auto.
+      eapply plus_trans; eauto.
+  - inv MIB.
+    destruct b; exploit IHIBIS; eauto.
 Admitted.
 
 Inductive iblock_istep_gen sp dupmap stack f pc0 cfg ib: trace -> bool -> option final -> option node -> Prop :=