start RTL -> BTL

1 files changed, 70 insertions, 49 deletions

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.
+