finishing proofs and cleanup

1 files changed, 48 insertions, 134 deletions

diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v
index f23bfcf8..da65d6ac 100644
--- a/scheduling/BTLtoRTLproof.v
+++ b/scheduling/BTLtoRTLproof.v
@@ -5,8 +5,8 @@ Require Import RTL Op Registers OptionMonad BTL.
 Require Import Errors Linking BTLtoRTL.
 
 
-(*****************************)
-(* Put this in an other file *)
+(**********************************)
+(* TODO Put this in an other file *)
 
 Require Import Linking.
 
@@ -106,32 +106,22 @@ Proof.
   intros. inv H0. inv H. inv STACKS. constructor.
 Qed.
 
-(* TODO copied from Duplicateproof.v *)
-(*Lemma list_nth_z_dupmap:
+(* Inspired 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 ->
+  list_forall2 (fun n n' => dupmap!n = Some n') ln ln' ->
+  exists (pc': node),
      list_nth_z ln' val = Some pc'
-  /\ dupmap!pc' = 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.
+      simpl. exists n. 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
-  | Bgoto pc => Some pc
-  | _ => None
-  end.
-*)
+Qed.
 
 (* variant of [star RTL.step] but requiring proposition [P] on the [refl] (stutttering) case. *)
 Inductive cond_star_step (P: Prop): RTL.state -> trace -> RTL.state -> Prop :=
@@ -150,6 +140,15 @@ Proof.
   eapply plus_trans; eauto.
 Qed.
 
+Lemma css_star P s0 s1 t:
+  cond_star_step P s0 t s1 ->
+  star RTL.step tge s0 t s1.
+Proof.
+  destruct 1.
+  - eapply star_refl; eauto.
+  - eapply plus_star; eauto.
+Qed.
+
 Local Hint Constructors RTL.step match_states: core.
 Local Hint Resolve css_refl plus_one transf_fundef_correct: core.
 
@@ -230,16 +229,6 @@ Proof.
           eapply plus_trans; 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.
-Proof.
-  destruct 1.
-  - eapply star_refl; eauto.
-  - eapply plus_star; eauto.
-Qed.
-
 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')
@@ -269,7 +258,35 @@ Proof.
       eexists; split. eapply exec_Icall; eauto. simpl. rewrite symbols_preserved.
       rewrite GFS. eassumption. apply function_sig_translated. assumption.
       repeat (econstructor; eauto).
-Admitted.
+  - (* tailcall *)
+    pose symbols_preserved as SYMPRES.
+    rename H2 into FIND.
+    destruct ri.
+    + simpl in FIND; apply functions_translated in FIND.
+      destruct FIND as (tf & cunit & TFUN & GFIND & LO).
+      eexists; split. eapply exec_Itailcall; eauto.
+      apply function_sig_translated. assumption.
+      erewrite <- preserv_fnstacksize; eauto.
+      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_Itailcall; eauto. simpl. rewrite symbols_preserved.
+      rewrite GFS. eassumption. apply function_sig_translated. assumption.
+      erewrite <- preserv_fnstacksize; eauto.
+      repeat (econstructor; eauto).
+  - (* builtin *)
+    pose symbols_preserved as SYMPRES.
+    eexists. split.
+    eapply exec_Ibuiltin; eauto. eapply eval_builtin_args_preserved; eauto.
+    eapply external_call_symbols_preserved; eauto. eapply senv_preserved.
+    econstructor; eauto.
+  - (* jumptable *)
+    pose symbols_preserved as SYMPRES.
+    exploit list_nth_z_dupmap; eauto. intros (pc'1 & LNZ & REVM).
+    eexists. split.
+    eapply exec_Ijumptable; eauto.
+    econstructor; eauto.
+Qed.
 
 Lemma iblock_step_simulation sp dupmap stack stack' f f' ib rs0 m0 rs1 m1 pc0 fin t s
  (STACKS: list_forall2 match_stackframes stack stack')
@@ -296,109 +313,6 @@ 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')
- (IBIS: iblock_istep ge sp rs0 m0 ib rs1 m1 (Some fin))
- (MIB : match_iblock dupmap (RTL.fn_code f') true pc0 ib None)
- (FS : final_step ge stack f sp rs1 m1 fin t s)
- :exists s', plus RTL.step tge (RTL.State stack' f' sp pc0 rs0 m0) t s' /\ match_states s s'.
-Proof.
-  intros; exploit iblock_istep_simulation; eauto.
-  simpl. intros (isfst' & pc1 & MI & STAR).
-  induction FS.
-  - inv MI.
-    + inv STAR; inv H3.
-    + inv STAR; try discriminate.
-      eexists; split. eauto.
-      econstructor; eauto.
-
-  - inv MI. pose symbols_preserved as SYMPRES.
-    inv STAR.
-    + inv H5. eexists; split.
-      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.
-
-
-Inductive iblock_istep_gen sp dupmap stack f pc0 cfg ib: trace -> bool -> option final -> option node -> Prop :=
-  | ibis_synced opc pc1
-      (HOPC: opc = Some pc1)
-      (MIB : match_iblock dupmap cfg true pc0 ib opc)
-      : iblock_istep_gen sp dupmap stack f pc0 cfg ib E0 true None opc
-  | ibis_stutter rs1 m1 fin ofin s t
-      (HFIN: ofin = Some fin)
-      (MIB : match_iblock dupmap cfg false pc0 ib None)
-      (FS : final_step ge stack f sp rs1 m1 fin t s)
-      : iblock_istep_gen sp dupmap stack f pc0 cfg ib t false ofin None.
-
-Lemma iblock_step_simulation
- sp dupmap stack stack' f f' rs0 m0 rs1 m1 ib ofin pc0 opc t s isfst
- (STACKS: list_forall2 match_stackframes stack stack')
- (TRANSF: match_function dupmap f f')
- (IBIS: iblock_istep ge sp rs0 m0 ib rs1 m1 ofin)
- (*(MIB : match_iblock dupmap cfg' isfst pc0 ib opc)*)
- (*(FS : final_step ge stack f sp rs1 m1 fin t s)*)
-(*FNC : (fn_code f) ! pc = Some ib*)
- (IBGEN: iblock_istep_gen sp dupmap stack f pc0 (RTL.fn_code f') ib t isfst ofin opc)
- :exists s', (if isfst then plus RTL.step else star RTL.step) tge (RTL.State stack' f' sp pc0 rs0 m0) t s' /\ match_states s s'.
-Proof.
-  (* TODO: généraliser ce lemme pour pouvoir le prouver par induction sur IBIS:
-       => il faut en particulier généraliser l'hypothèse MIB qui relie le iblock_istep ib en cours d'exécution.
-          avec le code RTL à partir de pc0. 
-       => ici, le "isfst" a déjà été généralisé: quand il vaut "false", ça veut dire qu'on a le droit de faire du "stuttering" côté RTL.
-       => il reste à comprendre comment généraliser le "None" en "opc"
-          ainsi que l'hypothese OFIN pour autoriser le cas "ofin=None" (nécessaire pour l'induction).
-          Idée: si "ofin = None" alors il y a un pc1 tq "opc = Some pc1" qui permet d'exécuter la suite du bloc...
-
-    Au final, il faut sans doute introduire un "Inductive" pour capturer ces idées dans un prédicat "lisible"/"manipulable"...
-  *)
-  (* XXX keep IBIS, MIB, and FS ? *)
-  induction IBIS.
-  - admit.
-  - inv IBGEN; try_simplify_someHyps.
-    inv MIB. eexists; split.
-    apply plus_one. econstructor; eauto.
-    (*
-  - inversion IBGEN; subst; try_simplify_someHyps.
-    exploit iblock_istep_simulation; eauto.
-    inv MIB.
-    eexists. split. apply plus_one.
-    eapply exec_Inop; eauto.
-    try_simplify_someHyps.
-      admit.
-  - (* exec_op *)
-    admit. (* cas absurde car hypothese OFIN trop restrictive *)
-  - (* exec_load_TRAP *)
-    admit. (* cas absurde car hypothese OFIN trop restrictive *)
-  - (* exec_load_store *)
-    admit. (* cas absurde car hypothese OFIN trop restrictive *)
-  - (* exec_seq_stop *)
-    (*inv MIB.*)
-    eapply IHIBIS; eauto.
-    (* TODO: c'est ici qu'on voit que l'hypothèse MIB est trop restrictive actuellement 
-       normalement, l'hypothèse d'induction IHIBIS devrait permettre de conclure quasi-directement ici.
-    *)
-    admit.
-  - (* exec_seq_continue *)
-    (* TODO: ici l'hypothèse d'induction IHIBIS1 n'est pas utilisable à cause de OFIN trop restrictive *)
-    try_simplify_someHyps.
-    (*inv MIB.*)
-    admit.
-  - (* exec_cond *)
-    try_simplify_someHyps.
-    (*inv MIB.*)
-       admit.*)
-Admitted.
-
-*)
-
 Theorem plus_simulation s1 t s1':
   step ge s1 t s1' ->
   forall s2 (MS: match_states s1 s2),