Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into BTL

1 files changed, 82 insertions, 11 deletions

diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v
index ed661280..7d58de5a 100644
--- a/scheduling/RTLtoBTLproof.v
+++ b/scheduling/RTLtoBTLproof.v
@@ -80,27 +80,40 @@ Let tge := Genv.globalenv tprog.
 
 Local Open Scope nat_scope.
 
-(* TODO:
+(** * Match relation from a RTL state to a BTL state
 
-Le (option iblock) en paramètre représente l'état de l'exécution côté BTL 
-depuis le début de l'exécution du block
+The "option iblock" parameter represents the current BTL execution state.
+Thus, each RTL single step is symbolized by a new BTL "option iblock"
+starting at the equivalent PC.
 
-  faire un dessin ASCII art de la simulation avec match_states_intro 
+The simulation diagram for match_states_intro is as follows:
 
+<<
+
+        RTL state       match_states_intro        BTL state
+      [pcR0,rs0,m0 ---------------------------- [pcB0,rs0,m0]
+           |                                         |
+           |                                         |
+   RTL_RUN | *E0                                     | BTL_RUN
+           |                                         |
+           |                   MIB                   |
+      [pcR1,rs,m] -------------------------------- [ib]
+
+>>
 *)
 
 Inductive match_states: (option iblock) -> RTL.state -> state -> Prop :=
   | match_states_intro (* TODO: LES DETAILS SONT SANS DOUTE A REVOIR !!! *)
-      ib dupmap st f sp pc rs m st' f' pc0' pc0 rs0 m0 isfst ib0
+      ib dupmap st f sp rs m st' f' pcB0 pcR0 pcR1 rs0 m0 isfst ib0
       (STACKS: list_forall2 match_stackframes st st')
       (TRANSF: match_function dupmap f f')
-      (ATpc0: (fn_code f')!pc0' = Some ib0)
-      (DUPLIC: dupmap!pc0' = Some pc0)
-      (MIB: match_iblock dupmap (RTL.fn_code f) isfst pc ib None)
+      (ATpc0: (fn_code f')!pcB0 = Some ib0)
+      (DUPLIC: dupmap!pcB0 = Some pcR0)
+      (MIB: match_iblock dupmap (RTL.fn_code f) isfst pcR1 ib None)
       (RIGHTA: is_right_assoc ib)
-      (RTL_RUN: star RTL.step ge (RTL.State st f sp pc0 rs0 m0) E0 (RTL.State st f sp pc rs m))
+      (RTL_RUN: star RTL.step ge (RTL.State st f sp pcR0 rs0 m0) E0 (RTL.State st f sp pcR1 rs m))
       (BTL_RUN: iblock_istep_run tge sp ib0.(entry) rs0 m0 = iblock_istep_run tge sp ib rs m)
-      : match_states (Some ib) (RTL.State st f sp pc rs m) (State st' f' sp pc0' rs0 m0)
+      : match_states (Some ib) (RTL.State st f sp pcR1 rs m) (State st' f' sp pcB0 rs0 m0)
   | match_states_call
       st st' f f' args m
       (STACKS: list_forall2 match_stackframes st st')
@@ -209,7 +222,20 @@ Cette mesure décroit strictement quand on exécute un "petit-pas" de iblock.
 Par exemple, le nombre de noeuds (ou d'instructions "RTL") dans le iblock devrait convenir.
 La hauteur de l'arbre aussi.
 *)
-Parameter measure: iblock -> nat.
+(** Representing an intermediate BTL state
+
+We keep a measure of code that remains to be executed with the omeasure
+type defined below. Intuitively, each RTL step corresponds to either
+   - a single BTL step if we are on the last instruction of the block
+   - no BTL step (as we use a "big step" semantics) but a change in
+     the measure which represents the new intermediate state of the BTL code
+ *)
+Fixpoint measure ib: nat :=
+  match ib with
+  | Bseq ib1 ib2
+  | Bcond _ _ ib1 ib2 _ => measure ib1 + measure ib2
+  | ib => 1
+  end.
 
 Definition omeasure (oib: option iblock): nat :=
  match oib with
@@ -224,6 +250,51 @@ Theorem opt_simu s1 t s1' oib s2:
      (exists s2', step tge s2 t s2' /\ match_states oib' s1' s2')
   \/ (omeasure oib' < omeasure oib /\ t=E0 /\ match_states oib' s1' s2) 
  .
+Proof.
+  inversion 2; subst; clear H0.
+  - (* State *)
+    inv H.
+
+    1: { (* Inop *)
+      eexists; right; split.
+      2: split; trivial.
+      2: {
+        econstructor; eauto.
+        all: admit. } admit. }
+    all: admit. 
+  - (* Callstate *)
+    inv H.
+    + (* Internal function *)
+      inv TRANSF.
+      rename H0 into TRANSF.
+      eapply dupmap_entrypoint in TRANSF as ENTRY.
+      eapply dupmap_correct in TRANSF as DMC. unfold match_cfg in DMC.
+      apply DMC in ENTRY as DMC'.
+      destruct DMC' as [ib [CENTRY MI]]; clear DMC.
+      eexists; left; eexists; split.
+      * eapply exec_function_internal.
+        erewrite preserv_fnstacksize; eauto.
+      * econstructor; eauto.
+        eapply code_right_assoc; eauto.
+        all: erewrite preserv_fnparams; eauto.
+        constructor.
+    + (* External function *)
+      inv TRANSF.
+      eexists; left; eexists; split.
+      * eapply exec_function_external.
+        eapply external_call_symbols_preserved.
+        eapply senv_preserved. eauto.
+      * econstructor; eauto.
+  - (* Returnstate *)
+    inv H. inv STACKS. inv H1.
+    eapply dupmap_correct in TRANSF as DMC. unfold match_cfg in DMC.
+    remember DUPLIC as ODUPLIC; clear HeqODUPLIC.
+    apply DMC in DUPLIC as [ib [FNC MI]]; clear DMC.
+    eexists; left; eexists; split.
+    + eapply exec_return.
+    + econstructor; eauto.
+      eapply code_right_assoc; eauto.
+      constructor.
 Admitted.
 
 Local Hint Resolve plus_one star_refl: core.