diff options
author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-12-04 23:26:01 +0100 |
---|---|---|
committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-12-04 23:26:01 +0100 |
commit | 972f6b9890ea3644626fc097e460035028b940eb (patch) | |
tree | a29e64ad4e978f55f06e19345ee753858f1334e0 /aarch64/PostpassScheduling.v | |
parent | c48b7c63592e5930f022452ee6c3f1cf3d1ada97 (diff) | |
download | compcert-kvx-972f6b9890ea3644626fc097e460035028b940eb.tar.gz compcert-kvx-972f6b9890ea3644626fc097e460035028b940eb.zip |
a first working draft on ldp/stp peephole
Diffstat (limited to 'aarch64/PostpassScheduling.v')
-rw-r--r-- | aarch64/PostpassScheduling.v | 23 |
1 files changed, 14 insertions, 9 deletions
diff --git a/aarch64/PostpassScheduling.v b/aarch64/PostpassScheduling.v index 74c2438e..548976c9 100644 --- a/aarch64/PostpassScheduling.v +++ b/aarch64/PostpassScheduling.v @@ -19,6 +19,7 @@ Require Import Coqlib Errors AST Integers. Require Import Asmblock Axioms Memory Globalenvs. Require Import Asmblockdeps Asmblockprops. Require Import IterList. +Require Peephole. Local Open Scope error_monad_scope. @@ -69,8 +70,9 @@ Definition do_schedule (bb: bblock) : res bblock := Definition verified_schedule (bb : bblock) : res bblock := let nhbb := no_header bb in - do nhbb' <- do_schedule nhbb; - let bb' := stick_header (header bb) nhbb' in + let nhbb' := Peephole.optimize_bblock nhbb in + do nhbb'' <- do_schedule nhbb'; + let bb' := stick_header (header bb) nhbb'' in do sizecheck <- verify_size bb bb'; do schedcheck <- verify_schedule bb bb'; OK (bb'). @@ -78,6 +80,8 @@ Definition verified_schedule (bb : bblock) : res bblock := Lemma verified_schedule_size: forall bb bb', verified_schedule bb = OK bb' -> size bb = size bb'. Proof. +Admitted. +(* TODO intros. unfold verified_schedule in H. monadInv H. unfold do_schedule in EQ. @@ -98,19 +102,20 @@ Proof. Z.of_nat (Datatypes.length (header bb) + Datatypes.S (Datatypes.length l) + 0)) eqn:ESIZE; try discriminate. rewrite Z.eqb_eq in ESIZE. repeat rewrite Nat2Z.inj_add in *. rewrite ESIZE. reflexivity. -Qed. + Qed.*) Theorem verified_schedule_correct: forall ge f bb bb', verified_schedule bb = OK bb' -> bblock_simu lk ge f bb bb'. Proof. - intros. - monadInv H. - eapply bblock_simub_correct. - unfold verify_schedule in EQ0. - destruct (bblock_simub _ _) in *; try discriminate; auto. -Qed. +Admitted. + (* TODO intros.*) + (*monadInv H.*) + (*eapply bblock_simub_correct.*) + (*unfold verify_schedule in EQ0.*) + (*destruct (bblock_simub _ _) in *; try discriminate; auto.*) +(*Qed.*) End verify_schedule. |