From c7bc74b1860f30df678bf384a32cd9c6eb113beb Mon Sep 17 00:00:00 2001
From: Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>
Date: Thu, 6 May 2021 09:07:07 +0200
Subject: start RTL -> BTL

---
 Makefile                   |   2 +-
 scheduling/BTL.v           | 119 ++++++++++++----------
 scheduling/BTLtoRTLproof.v |  50 ++++++++++
 scheduling/RTLtoBTL.v      |  23 +++++
 scheduling/RTLtoBTLproof.v | 239 +++++++++++++++++++++++++++++++++++++++++++++
 5 files changed, 383 insertions(+), 50 deletions(-)
 create mode 100644 scheduling/RTLtoBTL.v
 create mode 100644 scheduling/RTLtoBTLproof.v

diff --git a/Makefile b/Makefile
index 90c39907..934b8586 100644
--- a/Makefile
+++ b/Makefile
@@ -143,7 +143,7 @@ SCHEDULING= \
   RTLpathproof.v           RTLpathSE_theory.v \
   RTLpathSchedulerproof.v  RTLpath.v \
   RTLpathScheduler.v       RTLpathWFcheck.v \
-  BTL.v BTLtoRTL.v BTLtoRTLproof.v \
+  BTL.v BTLtoRTL.v BTLtoRTLproof.v RTLtoBTL.v RTLtoBTLproof.v
 
 # C front-end modules (in cfrontend/)
 
diff --git a/scheduling/BTL.v b/scheduling/BTL.v
index 7bc091ef..fb67d150 100644
--- a/scheduling/BTL.v
+++ b/scheduling/BTL.v
@@ -342,6 +342,8 @@ Definition semantics (p: program) :=
   Semantics step (initial_state p) final_state (Genv.globalenv p).
 
 
+(** TODO: est-ce qu'il faudrait déplacer ceci dans une librairie du genre "BTLlib" ? *)
+
 (** Matching BTL and RTL code 
 
 We should be able to define a single verifier able to prove a bisimulation between BTL and RTL code.
@@ -429,49 +431,10 @@ Inductive match_iblock (dupmap: PTree.t node) (cfg: RTL.code): bool -> node -> i
       match_iblock dupmap cfg isfst pc (Bcond c lr bso bnot i) opc
   .
 
-(* Partial copy of Duplicate and Duplicateproof. *)
-
 Definition match_cfg dupmap (cfg: code) (cfg':RTL.code): Prop :=
     forall pc pc', dupmap!pc = Some pc' ->
     exists ib, cfg!pc = Some ib /\ match_iblock dupmap cfg' true pc' ib.(entry) None.
 
-Record match_function dupmap f f': Prop := {
-  dupmap_correct: match_cfg dupmap (fn_code f) (RTL.fn_code f');
-  dupmap_entrypoint: dupmap!(fn_entrypoint f) = Some (RTL.fn_entrypoint f');
-  preserv_fnsig: fn_sig f = RTL.fn_sig f';
-  preserv_fnparams: fn_params f = RTL.fn_params f';
-  preserv_fnstacksize: fn_stacksize f = RTL.fn_stacksize f'
-}.
-
-Inductive match_fundef: fundef -> RTL.fundef -> Prop :=
-  | match_Internal dupmap f f': match_function dupmap f f' -> match_fundef (Internal f) (Internal f')
-  | match_External ef: match_fundef (External ef) (External ef).
-
-Inductive match_stackframes: stackframe -> RTL.stackframe -> Prop :=
-  | match_stackframe_intro 
-      dupmap res f sp pc rs f' pc'
-      (TRANSF: match_function dupmap f f')
-      (DUPLIC: dupmap!pc = Some pc')
-      : match_stackframes (Stackframe res f sp pc rs) (RTL.Stackframe res f' sp pc' rs).
-
-Inductive match_states: state -> RTL.state -> Prop :=
-  | match_states_intro 
-      dupmap st f sp pc rs m st' f' pc'
-      (STACKS: list_forall2 match_stackframes st st')
-      (TRANSF: match_function dupmap f f')
-      (DUPLIC: dupmap!pc = Some pc')
-      : match_states (State st f sp pc rs m) (RTL.State st' f' sp pc' rs m)
-  | match_states_call
-      st st' f f' args m
-      (STACKS: list_forall2 match_stackframes st st')
-      (TRANSF: match_fundef f f')
-      : match_states (Callstate st f args m) (RTL.Callstate st' f' args m)
-  | match_states_return
-      st st' v m
-      (STACKS: list_forall2 match_stackframes st st')
-      : match_states (Returnstate st v m) (RTL.Returnstate st' v m)
-   .
-
 (** Shared verifier between RTL -> BTL and BTL -> RTL *)
 
 Local Open Scope error_monad_scope.
@@ -536,7 +499,6 @@ Remark builtin_res_eq_pos: forall (a b: builtin_res positive), {a=b} + {a<>b}.
 Proof. intros. apply (builtin_res_eq Pos.eq_dec). Qed.
 Global Opaque builtin_res_eq_pos.
 
-(* TODO: deuxième étape (après BTLtoRTLproof.plus_simulation) *)
 Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) :=
   match ib with
   | BF fi =>
@@ -801,14 +763,73 @@ Definition verify_function dupmap f f' : res unit :=
   do _ <- verify_is_copy dupmap (fn_entrypoint f) (RTL.fn_entrypoint f');
   verify_cfg dupmap (fn_code f) (RTL.fn_code f').
 
-Lemma verify_function_correct dupmap f f' tt:
-  verify_function dupmap f f' = OK tt ->
-  fn_sig f = RTL.fn_sig f' ->
-  fn_params f = RTL.fn_params f' ->
-  fn_stacksize f = RTL.fn_stacksize f' ->
-  match_function dupmap f f'.
+Definition is_seq (ib: iblock): bool :=
+ match ib with
+ | Bseq _ _ => true 
+ | _ => false
+ end.
+
+Definition is_atom (ib: iblock): bool :=
+ match ib with
+ | Bseq _ _ | Bcond _ _ _ _ _ => false 
+ | _ => true
+ end.
+
+
+Inductive is_right_assoc: iblock -> Prop :=
+  | ira_Bseq ib1 ib2:
+     is_seq ib1 = false ->
+     is_right_assoc ib1 ->
+     is_right_assoc ib2 -> 
+     is_right_assoc (Bseq ib1 ib2)
+ | ira_Bcond cond args ib1 ib2 i:
+     is_right_assoc ib1 ->
+     is_right_assoc ib2 -> 
+     is_right_assoc (Bcond cond args ib1 ib2 i)
+ | ira_others ib:
+     is_atom ib = true ->
+     is_right_assoc ib
+     .
+Local Hint Constructors is_right_assoc: core.
+
+Fixpoint right_assoc (ib: iblock): iblock :=
+  match ib with
+  | Bseq ib1 ib2 => rec_rotate ib1 (right_assoc ib2)
+  | Bcond cond args ib1 ib2 i => 
+     Bcond cond args (right_assoc ib1) (right_assoc ib2) i
+  | ib => ib
+  end
+with rec_rotate (ib: iblock) rem: iblock :=
+  match ib with
+  | Bseq ib1 ib2 => 
+     rec_rotate ib1 (rec_rotate ib2 rem)
+  | Bcond cond args ib1 ib2 i => 
+     Bseq (Bcond cond args (right_assoc ib1) (right_assoc ib2) i) rem
+  | ib => Bseq ib rem
+end.
+
+Lemma right_assoc_rec_rotate_correct ib:
+    is_right_assoc (right_assoc ib)
+ /\ (forall rem, is_right_assoc rem -> is_right_assoc (rec_rotate ib rem)).
 Proof.
-  unfold verify_function; intro VERIF. monadInv VERIF.
-  constructor; eauto.
-  eapply verify_cfg_correct; eauto.
+  induction ib; simpl; intuition.
 Qed.
+
+Lemma right_assoc_correct ib:
+  is_right_assoc (right_assoc ib).
+Proof.
+  destruct (right_assoc_rec_rotate_correct ib); auto.
+Qed.
+
+Definition right_assoc_code (cfg: code): code :=
+  (PTree.map (fun _ ib => {| entry:=right_assoc ib.(entry); input_regs := ib.(input_regs) |}) cfg).
+
+Lemma right_assoc_code_correct cfg pc ib :
+  (right_assoc_code cfg)!pc=Some ib -> is_right_assoc (ib.(entry)).
+Proof.
+  unfold right_assoc_code.
+  rewrite PTree.gmap.
+  destruct (cfg!pc); simpl; intros; try_simplify_someHyps.
+  apply right_assoc_correct; auto.
+Qed.
+
diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v
index 3944e756..08a77ae4 100644
--- a/scheduling/BTLtoRTLproof.v
+++ b/scheduling/BTLtoRTLproof.v
@@ -6,6 +6,56 @@ Require Import Errors Linking BTLtoRTL.
 
 Require Import Linking.
 
+Record match_function dupmap f f': Prop := {
+  dupmap_correct: match_cfg dupmap (fn_code f) (RTL.fn_code f');
+  dupmap_entrypoint: dupmap!(fn_entrypoint f) = Some (RTL.fn_entrypoint f');
+  preserv_fnsig: fn_sig f = RTL.fn_sig f';
+  preserv_fnparams: fn_params f = RTL.fn_params f';
+  preserv_fnstacksize: fn_stacksize f = RTL.fn_stacksize f'
+}.
+
+Inductive match_fundef: fundef -> RTL.fundef -> Prop :=
+  | match_Internal dupmap f f': match_function dupmap f f' -> match_fundef (Internal f) (Internal f')
+  | match_External ef: match_fundef (External ef) (External ef).
+
+Inductive match_stackframes: stackframe -> RTL.stackframe -> Prop :=
+  | match_stackframe_intro 
+      dupmap res f sp pc rs f' pc'
+      (TRANSF: match_function dupmap f f')
+      (DUPLIC: dupmap!pc = Some pc')
+      : match_stackframes (Stackframe res f sp pc rs) (RTL.Stackframe res f' sp pc' rs).
+
+Inductive match_states: state -> RTL.state -> Prop :=
+  | match_states_intro 
+      dupmap st f sp pc rs m st' f' pc'
+      (STACKS: list_forall2 match_stackframes st st')
+      (TRANSF: match_function dupmap f f')
+      (DUPLIC: dupmap!pc = Some pc')
+      : match_states (State st f sp pc rs m) (RTL.State st' f' sp pc' rs m)
+  | match_states_call
+      st st' f f' args m
+      (STACKS: list_forall2 match_stackframes st st')
+      (TRANSF: match_fundef f f')
+      : match_states (Callstate st f args m) (RTL.Callstate st' f' args m)
+  | match_states_return
+      st st' v m
+      (STACKS: list_forall2 match_stackframes st st')
+      : match_states (Returnstate st v m) (RTL.Returnstate st' v m)
+   .
+
+Lemma verify_function_correct dupmap f f' tt:
+  verify_function dupmap f f' = OK tt ->
+  fn_sig f = RTL.fn_sig f' ->
+  fn_params f = RTL.fn_params f' ->
+  fn_stacksize f = RTL.fn_stacksize f' ->
+  match_function dupmap f f'.
+Proof.
+  unfold verify_function; intro VERIF. monadInv VERIF.
+  constructor; eauto.
+  - eapply verify_cfg_correct; eauto.
+  - eapply verify_is_copy_correct; eauto.
+Qed.
+
 Lemma transf_function_correct f f':
   transf_function f = OK f' -> exists dupmap, match_function dupmap f f'.
 Proof.
diff --git a/scheduling/RTLtoBTL.v b/scheduling/RTLtoBTL.v
new file mode 100644
index 00000000..14aecb21
--- /dev/null
+++ b/scheduling/RTLtoBTL.v
@@ -0,0 +1,23 @@
+Require Import Coqlib Maps.
+Require Import AST Integers Values Events Memory Globalenvs Smallstep.
+Require Import RTL Op Registers OptionMonad BTL.
+
+Require Import Errors Linking.
+
+(** External oracle *)
+Parameter rtl2btl: RTL.function -> BTL.code * node * (PTree.t node).
+
+Local Open Scope error_monad_scope.
+
+Definition transf_function (f: RTL.function) : res BTL.function :=
+  let (tcte, dupmap) := rtl2btl f in
+  let (tc, te) := tcte in
+  let f' := BTL.mkfunction (RTL.fn_sig f) (RTL.fn_params f) (RTL.fn_stacksize f) (right_assoc_code tc) te in
+  do u <- verify_function dupmap f' f;
+  OK f'.
+
+Definition transf_fundef (f: RTL.fundef) : res fundef :=
+  transf_partial_fundef transf_function f.
+
+Definition transf_program (p: RTL.program) : res program :=
+  transform_partial_program transf_fundef p.
diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v
new file mode 100644
index 00000000..4f76d0b7
--- /dev/null
+++ b/scheduling/RTLtoBTLproof.v
@@ -0,0 +1,239 @@
+Require Import Coqlib Maps.
+Require Import AST Integers Values Events Memory Globalenvs Smallstep.
+Require Import RTL Op Registers OptionMonad BTL.
+
+Require Import Errors Linking RTLtoBTL.
+
+Require Import Linking.
+
+Record match_function dupmap f tf: Prop := {
+  dupmap_correct: match_cfg dupmap (fn_code tf) (RTL.fn_code f);
+  dupmap_entrypoint: dupmap!(fn_entrypoint tf) = Some (RTL.fn_entrypoint f);
+  code_right_assoc: forall pc ib, (fn_code tf)!pc=Some ib -> is_right_assoc ib.(entry);
+  preserv_fnsig: fn_sig tf = RTL.fn_sig f;
+  preserv_fnparams: fn_params tf = RTL.fn_params f;
+  preserv_fnstacksize: fn_stacksize tf = RTL.fn_stacksize f
+}.
+
+Inductive match_fundef: RTL.fundef -> fundef -> Prop :=
+  | match_Internal dupmap f tf: match_function dupmap f tf -> match_fundef (Internal f) (Internal tf)
+  | match_External ef: match_fundef (External ef) (External ef).
+
+Inductive match_stackframes: RTL.stackframe -> stackframe -> Prop :=
+  | match_stackframe_intro 
+      dupmap res f sp pc rs f' pc'
+      (TRANSF: match_function dupmap f f')
+      (DUPLIC: dupmap!pc' = Some pc)
+      : match_stackframes (RTL.Stackframe res f sp pc rs) (Stackframe res f' sp pc' rs).
+
+Lemma verify_function_correct dupmap f f' tt:
+  verify_function dupmap f' f = OK tt ->
+  fn_sig f' = RTL.fn_sig f ->
+  fn_params f' = RTL.fn_params f ->
+  fn_stacksize f' = RTL.fn_stacksize f ->
+  (forall pc ib, (fn_code f')!pc=Some ib -> is_right_assoc ib.(entry)) ->
+  match_function dupmap f f'.
+Proof.
+  unfold verify_function; intro VERIF. monadInv VERIF.
+  constructor; eauto.
+  - eapply verify_cfg_correct; eauto.
+  - eapply verify_is_copy_correct; eauto.
+Qed.
+
+Lemma transf_function_correct f f':
+  transf_function f = OK f' -> exists dupmap, match_function dupmap f f'.
+Proof.
+  unfold transf_function; unfold bind. repeat autodestruct.
+  intros H _ _ X. inversion X; subst; clear X.
+  eexists; eapply verify_function_correct; simpl; eauto.
+  eapply right_assoc_code_correct; eauto.
+Qed.
+
+Lemma transf_fundef_correct f f':
+  transf_fundef f = OK f' -> match_fundef f f'.
+Proof.
+  intros TRANSF; destruct f; simpl; monadInv TRANSF.
+  + exploit transf_function_correct; eauto.
+    intros (dupmap & MATCH_F).
+    eapply match_Internal; eauto.
+  + eapply match_External.
+Qed.
+
+Definition match_prog (p: RTL.program) (tp: program) :=
+  match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp.
+
+Lemma transf_program_match:
+  forall prog tprog, transf_program prog = OK tprog -> match_prog prog tprog.
+Proof.
+  intros. eapply match_transform_partial_program_contextual; eauto.
+Qed.
+
+Section BTL_SIMULATES_RTL.
+
+Variable prog: RTL.program.
+Variable tprog: program.
+
+Hypothesis TRANSL: match_prog prog tprog.
+
+Let ge := Genv.globalenv prog.
+Let tge := Genv.globalenv tprog.
+
+Local Open Scope nat_scope.
+
+(* TODO: 
+  faire un dessin ASCII art de la simulation avec match_states_intro 
+
+Le 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
+*)
+
+Inductive match_states: 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' pc' pc0' pc0 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)
+      (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))
+      (BTL_RUN: iblock_istep_run tge sp ib0.(entry) rs0 m0 = iblock_istep_run tge sp ib rs m)
+      : match_states ib (RTL.State st f sp pc rs m) (State st' f' sp pc' rs m)
+  | match_states_call
+      ib st st' f f' args m
+      (STACKS: list_forall2 match_stackframes st st')
+      (TRANSF: match_fundef f f')
+      : match_states ib (RTL.Callstate st f args m) (Callstate st' f' args m)
+  | match_states_return
+      ib st st' v m
+      (STACKS: list_forall2 match_stackframes st st')
+      : match_states ib (RTL.Returnstate st v m) (Returnstate st' v m)
+   .
+
+Lemma symbols_preserved s: Genv.find_symbol tge s = Genv.find_symbol ge s.
+Proof.
+  rewrite <- (Genv.find_symbol_match TRANSL). reflexivity.
+Qed.
+
+Lemma senv_preserved: Senv.equiv ge tge.
+Proof.
+  eapply (Genv.senv_match TRANSL).
+Qed.
+
+Lemma functions_translated (v: val) (f: RTL.fundef):
+  Genv.find_funct ge v = Some f ->
+  exists tf cunit, transf_fundef f = OK tf /\ Genv.find_funct tge v = Some tf /\ linkorder cunit prog.
+Proof.
+  intros. exploit (Genv.find_funct_match TRANSL); eauto.
+  intros (cu & tf & A & B & C).
+  repeat eexists; intuition eauto.
+  + unfold incl; auto.
+  + eapply linkorder_refl.
+Qed.
+
+Lemma function_ptr_translated v f:
+  Genv.find_funct_ptr ge v = Some f ->
+  exists tf,
+  Genv.find_funct_ptr tge v = Some tf /\ transf_fundef f = OK tf.
+Proof.
+  intros.
+  exploit (Genv.find_funct_ptr_transf_partial TRANSL); eauto.
+Qed.
+
+Lemma function_sig_translated f tf: transf_fundef f = OK tf -> funsig tf = RTL.funsig f.
+Proof.
+  intros H; apply transf_fundef_correct in H; destruct H; simpl; eauto.
+  erewrite preserv_fnsig; eauto.
+Qed.
+
+Lemma transf_initial_states s1:
+  RTL.initial_state prog s1 ->
+  exists ib s2, initial_state tprog s2 /\ match_states ib s1 s2.
+Proof.
+  intros. inv H.
+  exploit function_ptr_translated; eauto. intros (tf & FIND & TRANSF).
+  eexists. eexists. split.
+  - econstructor; eauto.
+    + eapply (Genv.init_mem_transf_partial TRANSL); eauto.
+    + replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved. eauto.
+      symmetry. eapply match_program_main. eauto.
+    + erewrite function_sig_translated; eauto.
+  - constructor; eauto.
+    constructor.
+    apply transf_fundef_correct; auto.
+Admitted. (* TODO *)
+
+Lemma transf_final_states ib s1 s2 r:
+  match_states ib s1 s2 -> RTL.final_state s1 r -> final_state s2 r.
+Proof.
+  intros. inv H0. inv H. inv STACKS. constructor.
+Qed.
+
+Lemma find_function_preserved ri rs0 fd
+  (FIND : RTL.find_function ge ri rs0 = Some fd)
+  : exists fd', find_function tge ri rs0 = Some fd'
+                /\ transf_fundef fd = OK fd'.
+Proof.
+  pose symbols_preserved as SYMPRES.
+  destruct ri.
+  + simpl in FIND; apply functions_translated in FIND.
+    destruct FIND as (tf & cunit & TFUN & GFIND & LO).
+    eexists; split. eauto. assumption.
+  + 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. simpl. rewrite symbols_preserved.
+    rewrite GFS. eassumption. assumption.
+Qed.
+
+(* 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': node),
+     list_nth_z ln' val = Some pc'
+  /\ dupmap!pc = Some pc'.
+Proof.
+  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 n. split; auto.
+    + inv LFA. simpl. rewrite ZEQ. exploit IHln. 2: eapply H0. all: eauto.
+Qed.
+
+(* TODO: definir une measure sur les iblocks.
+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.
+
+Theorem opt_simu s1 t s1':
+ RTL.step ge s1 t s1' ->
+ forall ib s2,
+ match_states ib s1 s2 ->
+ exists (ib' : iblock),
+     (exists s2', step tge s2 t s2' /\ match_states ib' s1' s2')
+  \/ (measure ib' < measure ib /\ t=E0 /\ match_states ib' s1' s2) 
+ .
+Admitted.
+
+Local Hint Resolve plus_one star_refl: core.
+
+Theorem transf_program_correct:
+  forward_simulation (RTL.semantics prog) (BTL.semantics tprog).
+Proof.
+  eapply (Forward_simulation (L1:=RTL.semantics prog) (L2:=semantics tprog) (ltof _ measure) match_states).
+  constructor 1; simpl.
+  - apply well_founded_ltof.
+  - eapply transf_initial_states.
+  - eapply transf_final_states.
+  - intros s1 t s1' STEP i s2 MATCH. exploit opt_simu; eauto. clear MATCH STEP.
+    destruct 1 as (ib' & [ (s2' & STEP & MATCH) | (MEASURE & TRACE & MATCH) ]).
+    + repeat eexists; eauto.
+    + subst. repeat eexists; eauto.
+  - eapply senv_preserved.
+Qed.
+
+End BTL_SIMULATES_RTL.
-- 
cgit