diff options
| -rw-r--r-- | scheduling/BTL.v | 66 | ||||
| -rw-r--r-- | scheduling/RTLtoBTL.v | 3 | ||||
| -rw-r--r-- | scheduling/RTLtoBTLproof.v | 2 |
3 files changed, 66 insertions, 5 deletions
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); |