some advance and simplifications

1 files changed, 71 insertions, 67 deletions

diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v
index 8dad43c7..f23bfcf8 100644
--- a/scheduling/BTLtoRTLproof.v
+++ b/scheduling/BTLtoRTLproof.v
@@ -106,6 +106,25 @@ Proof.
   intros. inv H0. inv H. inv STACKS. constructor.
 Qed.
 
+(* TODO copied from Duplicateproof.v *)
+(*Lemma list_nth_z_dupmap:
+  forall dupmap ln ln' (pc pc': node) val,
+  list_nth_z ln val = Some pc' ->
+  list_forall2 (fun n n' => dupmap!n' = Some n) ln ln' ->
+  exists pc',
+     list_nth_z ln' val = Some pc'
+  /\ dupmap!pc' = Some pc.
+Proof.
+Admitted.
+  induction ln; intros until val; intros LNZ LFA.
+  - inv LNZ.
+  - inv LNZ. destruct (zeq val 0) eqn:ZEQ.
+    + inv H0. destruct ln'; inv LFA.
+      simpl. exists p. split; auto.
+    + inv LFA. simpl. rewrite ZEQ. exploit IHln. 2: eapply H0. all: eauto.
+      intros (pc'1 & LNZ & REV). exists pc'1. split; auto. congruence.
+   Qed.*)
+
 (* FIXME: unused ?
 Definition is_goto (i: final): option exit :=
   match i with
@@ -131,9 +150,8 @@ Proof.
   eapply plus_trans; eauto.
 Qed.
 
-
 Local Hint Constructors RTL.step match_states: core.
-Local Hint Resolve css_refl plus_one: core.
+Local Hint Resolve css_refl plus_one transf_fundef_correct: core.
 
 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):
@@ -143,33 +161,37 @@ 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 =>
-     (* A CHANGER ? *)
+     (* XXX A CHANGER ? *)
      exists isfst' pc1, match_iblock dupmap (RTL.fn_code f') isfst' pc1 fin None
                 /\ cond_star_step (isfst = isfst') (RTL.State stack' f' sp pc0 rs0 m0) E0 (RTL.State stack' f' sp pc1 rs1 m1)
   end.
 Proof.
   induction IBIS; simpl; intros.
-  - assert (X: opc = None). { inv MIB; auto. }
+  - (* exec_final *)
+    assert (X: opc = None). { inv MIB; auto. }
     subst.
     repeat eexists; eauto.
-    (* eapply css_refl; auto. *)
-  - inv MIB. exists pc'; split; eauto.
-    (* apply plus_one; eauto. apply exec_Inop; trivial. *)
-  - inv MIB. exists pc'; split; auto.
+  - (* exec_nop *)
+    inv MIB. exists pc'; split; eauto.
+  - (* exec_op *)
+    inv MIB. exists pc'; split; auto.
     apply plus_one. eapply exec_Iop; eauto.
     erewrite <- eval_operation_preserved; eauto.
     intros; rewrite symbols_preserved; trivial.
-  - inv MIB. exists pc'; split; auto.
+  - (* exec_load *)
+    inv MIB. exists pc'; split; auto.
     apply plus_one. eapply exec_Iload; eauto.
     erewrite <- eval_addressing_preserved; eauto.
     intros; rewrite symbols_preserved; trivial.
-  - inv MIB. exists pc'; split; auto.
+  - (* exec_store *)
+    inv MIB. exists pc'; split; auto.
     apply plus_one. eapply exec_Istore; eauto.
     erewrite <- eval_addressing_preserved; eauto.
     intros; rewrite symbols_preserved; trivial.
-  - inv MIB; eauto.
-    (* exploit IHIBIS; eauto. *)
-  - inv MIB.
+  - (* exec_seq_stop *)
+    inv MIB; eauto.
+  - (* exec_seq_continue *)
+    inv MIB.
     exploit IHIBIS1; eauto.
     intros (pc1 & EQpc1 & STEP1); inv EQpc1.
     exploit IHIBIS2; eauto.
@@ -180,7 +202,8 @@ Proof.
     + intros (pc2 & EQpc2 & STEP2); inv EQpc2.
       eexists; split; auto.
       eapply plus_trans; eauto.
-  - inv MIB.
+  - (* exec_cond *)
+    inv MIB.
     assert (JOIN: is_join_opt opc1 opc2 opc). { exact H10. } clear H10. 
     destruct b; exploit IHIBIS; eauto.
     + (* taking ifso *)
@@ -189,34 +212,25 @@ Proof.
         intros (isfst' & pc1 & MI & STAR).
         repeat eexists; eauto.
         eapply css_plus_trans; eauto.
-        (* eapply plus_one. eapply exec_Icond; eauto.
-        eauto. *)
       * (* ofin is None *)
         intros (pc1 & OPC & PLUS). inv OPC.
         inv JOIN; eexists; split; eauto.
         all:
           eapply plus_trans; eauto.
-        (*
-          [ eapply plus_one; eapply exec_Icond; eauto
-          | eauto | eauto ].*)
     + (* taking ifnot *)
       destruct ofin; simpl.
       * (* ofin is Some final *)
         intros (isfst' & pc1 & MI & STAR).
         repeat eexists; eauto.
         eapply css_plus_trans; eauto.
-        (* eapply plus_one. eapply exec_Icond; eauto.
-           eauto. *)
       * (* ofin is None *)
         intros (pc1 & OPC & PLUS). subst.
         inv JOIN; eexists; split; eauto.
         all:
           eapply plus_trans; eauto.
-(*
-          [ eapply plus_one; eapply exec_Icond; eauto
-          | eauto | eauto ]. *)
 Qed.
 
+(* TODO move above *)
 Lemma css_star P s0 s1 t:
   cond_star_step P s0 t s1 ->
   star RTL.step tge s0 t s1.
@@ -226,19 +240,35 @@ Proof.
   - eapply plus_star; eauto.
 Qed.
 
-Lemma final_simu_except_goto sp dupmap stack stack' f f' rs0 m0 rs1 m1 pc0 fin t s
+Lemma final_simu_except_goto sp dupmap stack stack' f f' rs1 m1 pc1 fin t s
   (STACKS : list_forall2 match_stackframes stack stack')
   (TRANSF : match_function dupmap f f')
   (FS : final_step ge stack f sp rs1 m1 fin t s)
-  (pc1 : node)
-  (STAR : star RTL.step tge (RTL.State stack' f' sp pc0 rs0 m0) E0
-                            (RTL.State stack' f' sp pc1 rs1 m1))
   (i : instruction)
   (ATpc1 : (RTL.fn_code f') ! pc1 = Some i)
   (MF : match_final_inst dupmap fin i)
-  : exists s', plus RTL.step tge (RTL.State stack' f' sp pc0 rs0 m0) t s' /\ match_states s s'.
+  : exists s', RTL.step tge (RTL.State stack' f' sp pc1 rs1 m1) t s' /\ match_states s s'.
 Proof.
   inv MF; inv FS.
+  - (* return *)
+    eexists; split.
+    eapply exec_Ireturn; eauto.
+    erewrite <- preserv_fnstacksize; eauto.
+    econstructor; eauto.
+  - (* call *)
+    pose symbols_preserved as SYMPRES.
+    rename H7 into FIND.
+    destruct ri.
+    + simpl in FIND; apply functions_translated in FIND.
+      destruct FIND as (tf & cunit & TFUN & GFIND & LO).
+      eexists; split. eapply exec_Icall; eauto.
+      apply function_sig_translated. assumption.
+      repeat (econstructor; eauto).
+    + simpl in FIND. destruct (Genv.find_symbol _ _) eqn:GFS; try discriminate.
+      apply function_ptr_translated in FIND. destruct FIND as (tf & GFF & TF).
+      eexists; split. eapply exec_Icall; eauto. simpl. rewrite symbols_preserved.
+      rewrite GFS. eassumption. apply function_sig_translated. assumption.
+      repeat (econstructor; eauto).
 Admitted.
 
 Lemma iblock_step_simulation sp dupmap stack stack' f f' ib rs0 m0 rs1 m1 pc0 fin t s
@@ -254,7 +284,11 @@ Proof.
   inv MI.
   - (* final inst except goto *)
     exploit final_simu_except_goto; eauto.
-    eapply css_star; eauto.
+    intros (s' & STEP & MS). eexists; split.
+    + eapply plus_right.
+      eapply css_star; eauto.
+      eapply STEP. econstructor.
+    + eapply MS.
   - (* goto *)
     inv FS.
     inv STAR; try congruence.
@@ -262,6 +296,8 @@ Proof.
     econstructor; eauto.
 Qed.
 
+(* BROUILLON
+
 Lemma iblock_step_simulation_draft sp dupmap stack stack' f f' ib rs0 m0 rs1 m1 pc0 fin t s
  (STACKS: list_forall2 match_stackframes stack stack')
  (TRANSF: match_function dupmap f f')
@@ -279,49 +315,17 @@ Proof.
       eexists; split. eauto.
       econstructor; eauto.
 
-  - inv MI.
-    inv STAR.
-    + inv H5. eexists; split.
-      eapply plus_one. eapply exec_Ireturn; eauto.
-      erewrite <- preserv_fnstacksize; eauto.
-      econstructor; eauto.
-    + inv H5. eexists; split.
-      eapply plus_trans. eauto.
-      eapply plus_one. eapply exec_Ireturn; eauto.
-      erewrite <- preserv_fnstacksize; eauto. eauto.
-      econstructor; eauto.
-  - inv MI.
-    inv STAR.
-    + inv H5.
-      pose symbols_preserved as SYMPRES.
-      destruct ros.
-      * simpl in H. apply functions_translated in H.
-        destruct H as (tf & cunit & TFUN & GFIND & LO).
-        eexists; split.
-        eapply plus_one. eapply exec_Icall; eauto.
-        apply function_sig_translated. assumption.
-        admit.
-        (* TODO ?? *)
-      * admit.
-    + admit.
-  - admit.
   - inv MI. pose symbols_preserved as SYMPRES.
     inv STAR.
     + inv H5. eexists; split.
-      eapply plus_one. eapply exec_Ibuiltin; eauto.
-      eapply eval_builtin_args_preserved; eauto.
-      eapply external_call_symbols_preserved; eauto. eapply senv_preserved.
-      econstructor; eauto.
-    + inv H5. eexists; split.
-      eapply plus_trans. eauto.
-      eapply plus_one. eapply exec_Ibuiltin; eauto.
-      eapply eval_builtin_args_preserved; eauto.
-      eapply external_call_symbols_preserved; eauto. eapply senv_preserved.
-      eauto. econstructor; eauto.
+      eapply plus_one. eapply exec_Ijumptable; eauto.
+      exploit list_nth_z_dupmap; eauto. intros (pc'1 & LNZ & REVM).
+    eexists. split.
+    + eapply exec_Ijumptable; eauto.
+    + econstructor; eauto.
   - admit.
 Admitted.
 
-(* BROUILLON
 
 Inductive iblock_istep_gen sp dupmap stack f pc0 cfg ib: trace -> bool -> option final -> option node -> Prop :=
   | ibis_synced opc pc1