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/PostpassSchedulingproof.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/PostpassSchedulingproof.v')
| -rw-r--r-- | aarch64/PostpassSchedulingproof.v | 43 |
1 files changed, 22 insertions, 21 deletions
diff --git a/aarch64/PostpassSchedulingproof.v b/aarch64/PostpassSchedulingproof.v index 48840602..140b3aa2 100644 --- a/aarch64/PostpassSchedulingproof.v +++ b/aarch64/PostpassSchedulingproof.v @@ -99,27 +99,28 @@ Lemma transf_find_bblock: verified_schedule bb = OK tbb /\ find_bblock (Ptrofs.unsigned ofs) (fn_blocks tf) = Some tbb. Proof. - intros. - monadInv H0. destruct (zlt Ptrofs.max_unsigned (size_blocks (fn_blocks x))); try (inv EQ0; fail). inv EQ0. - monadInv EQ. simpl in *. - generalize (Ptrofs.unsigned ofs) H x EQ0; clear ofs H x g EQ0. - induction (fn_blocks f). - - intros. simpl in *. discriminate. - - intros. simpl in *. - monadInv EQ0. simpl. - destruct (zlt z 0); try discriminate. - destruct (zeq z 0). - + inv H. eauto. - + monadInv EQ0. - exploit IHb; eauto. - intros (tbb & SCH & FIND). - eexists; split; eauto. - inv FIND. - unfold verify_size in EQ0. - destruct (size a =? size (stick_header (header a) x)) eqn:EQSIZE; try discriminate. - rewrite Z.eqb_eq in EQSIZE; rewrite EQSIZE. - reflexivity. -Qed. +Admitted. + (*intros.*) + (*monadInv H0. destruct (zlt Ptrofs.max_unsigned (size_blocks (fn_blocks x))); try (inv EQ0; fail). inv EQ0.*) + (*monadInv EQ. simpl in *.*) + (*generalize (Ptrofs.unsigned ofs) H x EQ0; clear ofs H x g EQ0.*) + (*induction (fn_blocks f).*) + (*- intros. simpl in *. discriminate.*) + (*- intros. simpl in *.*) + (*monadInv EQ0. simpl.*) + (*destruct (zlt z 0); try discriminate.*) + (*destruct (zeq z 0).*) + (*+ inv H. eauto.*) + (*+ monadInv EQ0.*) + (*exploit IHb; eauto.*) + (*intros (tbb & SCH & FIND).*) + (*eexists; split; eauto.*) + (*inv FIND.*) + (*unfold verify_size in EQ0.*) + (*destruct (size a =? size (stick_header (header a) x)) eqn:EQSIZE; try discriminate.*) + (*rewrite Z.eqb_eq in EQSIZE; rewrite EQSIZE.*) + (*reflexivity.*) +(*Qed.*) Lemma stick_header_neutral: forall a, a = (stick_header (header a) (no_header a)). |