From a1cde0686dfb40595423f40ccc40e18de3539e52 Mon Sep 17 00:00:00 2001
From: Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>
Date: Sat, 8 May 2021 07:31:05 +0200
Subject: idee pour simplifier la preuve: restreindre le "right_assoc" en
 "expand" !

---
 scheduling/BTL.v           | 66 ++++++++++++++++++++++++++++++++++++++++++----
 scheduling/RTLtoBTL.v      |  3 +++
 scheduling/RTLtoBTLproof.v |  2 ++
 3 files changed, 66 insertions(+), 5 deletions(-)

(limited to 'scheduling')

diff --git a/scheduling/BTL.v b/scheduling/BTL.v
index 8ccab024..7f3d327b 100644
--- a/scheduling/BTL.v
+++ b/scheduling/BTL.v
@@ -785,11 +785,6 @@ 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').
 
-Definition is_seq (ib: iblock): bool :=
- match ib with
- | Bseq _ _ => true 
- | _ => false
- end.
 
 Definition is_atom (ib: iblock): bool :=
  match ib with
@@ -797,6 +792,67 @@ Definition is_atom (ib: iblock): bool :=
  | _ => true
  end.
 
+Inductive is_expand: iblock -> Prop :=
+  | exp_Bseq ib1 ib2:
+     is_atom ib1 = true ->
+     is_expand ib2 -> 
+     is_expand (Bseq ib1 ib2)
+  | exp_Bcond cond args ib1 ib2 i:
+     is_expand ib1 ->
+     is_expand ib2 -> 
+     is_expand (Bcond cond args ib1 ib2 i)
+  | exp_others ib:
+     is_atom ib = true ->
+     is_expand ib
+     .
+Local Hint Constructors is_expand: core.
+
+Fixpoint expand (ib: iblock) (k: option iblock): iblock :=
+  match ib with
+  | Bseq ib1 ib2 => expand ib1 (Some (expand ib2 k))
+  | Bcond cond args ib1 ib2 i => 
+     Bcond cond args (expand ib1 k) (expand ib2 k) i
+  | ib => 
+    match k with 
+    | None => ib
+    | Some rem => Bseq ib rem
+    end
+  end.
+
+Lemma expand_correct ib: forall k,
+  (match k with Some rem => is_expand rem | None => True end)
+  -> is_expand (expand ib k).
+Proof.
+  induction ib; simpl; intros; try autodestruct; auto.
+Qed.
+
+Lemma expand_None_correct ib: 
+   is_expand (expand ib None).
+Proof.
+  apply expand_correct; simpl; auto.
+Qed.
+
+Definition expand_code (cfg: code): code :=
+  (PTree.map (fun _ ib => {| entry:=expand ib.(entry) None; input_regs := ib.(input_regs) |}) cfg).
+
+Lemma expand_code_correct cfg pc ib :
+  (expand_code cfg)!pc=Some ib -> is_expand (ib.(entry)).
+Proof.
+  unfold expand_code.
+  rewrite PTree.gmap.
+  destruct (cfg!pc); simpl; intros; try_simplify_someHyps.
+  apply expand_None_correct; auto.
+Qed.
+
+
+(* TODO: eliminer toute la suite quand "right_assoc" sera remplace par "expand" *)
+
+Definition is_seq (ib: iblock): bool :=
+ match ib with
+ | Bseq _ _ => true 
+ | _ => false
+ end.
+
 
 Inductive is_right_assoc: iblock -> Prop :=
   | ira_Bseq ib1 ib2:
diff --git a/scheduling/RTLtoBTL.v b/scheduling/RTLtoBTL.v
index 14aecb21..2b2bd15c 100644
--- a/scheduling/RTLtoBTL.v
+++ b/scheduling/RTLtoBTL.v
@@ -12,6 +12,9 @@ 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
+  (* TODO, pour finir la preuve: remplacer ci-dessous "right_assoc_code" par "expand_code" 
+     on s'arrangera pour éliminer cette transformation "coûteuse" à la fin !
+  *)
   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'.
diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v
index 7d58de5a..7c9fb456 100644
--- a/scheduling/RTLtoBTLproof.v
+++ b/scheduling/RTLtoBTLproof.v
@@ -6,6 +6,8 @@ Require Import Errors Linking RTLtoBTL.
 
 Require Import Linking.
 
+(* TODO: remplacer "right_assoc" par "expand" ci-dessous *)
+
 Record match_function dupmap (f:RTL.function) (tf: BTL.function): Prop := {
   dupmap_correct: match_cfg dupmap (fn_code tf) (RTL.fn_code f);
   dupmap_entrypoint: dupmap!(fn_entrypoint tf) = Some (RTL.fn_entrypoint f);
-- 
cgit