From 05273f381d89d86c25d94f1b54b09fd6868db2ec Mon Sep 17 00:00:00 2001 From: Justus Fasse Date: Wed, 29 Jul 2020 12:39:03 +0200 Subject: Simplify unfold_bblock and complete unfold_body's case in find_instr_bblock The previous version of unfold_bblock was copied from kvx/Asm.v. kvx's version is slightly different in that for the (here removed) special case it does not put a semicolon to separate bundles. Since aarch64 does not have kvx's bundles the two versions should be equivalent. --- aarch64/Asmgen.v | 11 ++------ aarch64/Asmgenproof.v | 77 +++++++++++++++++++++++++++++++++++++++++++++++++-- 2 files changed, 76 insertions(+), 12 deletions(-) (limited to 'aarch64') diff --git a/aarch64/Asmgen.v b/aarch64/Asmgen.v index 0124bf63..e1a38c45 100644 --- a/aarch64/Asmgen.v +++ b/aarch64/Asmgen.v @@ -327,15 +327,8 @@ Definition unfold_bblock (bb: bblock) := * basic block. *) if zle (list_length_z (header bb)) 1 then - do rest <- (match (body bb), (exit bb) with - | (((Asmblock.Pfreeframe _ _ - | Asmblock.Pallocframe _ _)::nil) as bo), None => - unfold_body bo - | bo, ex => - do bo_is <- unfold_body bo; - OK (bo_is ++ unfold_exit ex) - end) - ; OK (lbl ++ rest) + do bo_is <- unfold_body (body bb); + OK (lbl ++ bo_is ++ unfold_exit (exit bb)) else Error (msg "Asmgen.unfold_bblock: Multiple labels were generated."). diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index 1ce519f0..7ef345b2 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -399,6 +399,25 @@ Proof. + eapply IHbbs; eauto. Qed. +Lemma entire_body_translated: + forall lbi tc, + unfold_body lbi = OK tc -> + forall bi, In bi lbi -> + exists bi', basic_to_instruction bi = OK bi'. +Proof. + induction lbi as [| a lbi IHlbi]. + - intros. contradiction. + - intros tc UNFOLD_BODY bi IN. + unfold unfold_body in UNFOLD_BODY. apply bind_inversion in UNFOLD_BODY. + destruct UNFOLD_BODY as (? & TRANSbi & REST). + apply bind_inversion in REST. destruct REST as (? & UNFOLD_BODY' & ?). + fold unfold_body in UNFOLD_BODY'. + + inversion IN as [EQ | NEQ]. + + rewrite <- EQ; eauto. + + eapply IHlbi; eauto. +Qed. + Lemma bblock_in_bblocks bbs bb: forall tc pos (UNFOLD: unfold bbs = OK tc) @@ -471,6 +490,48 @@ Proof. apply IHll; auto. Qed. +Lemma list_nth_z_find_bi: + forall lbi bi tlbi n bi' exit, + list_nth_z lbi n = Some bi -> + unfold_body lbi = OK tlbi -> + basic_to_instruction bi = OK bi' -> + Asm.find_instr n (tlbi ++ exit) = Some bi'. +Proof. + induction lbi. + - intros. inversion H. + - simpl. intros. + apply bind_inversion in H0. destruct H0 as (? & ? & ?). + apply bind_inversion in H2. destruct H2 as (? & ? & ?). + destruct (zeq n 0) as [Z | NZ]. + + destruct n. + * inversion H as (BI). rewrite BI in *. + inversion H3. simpl. congruence. + * (* absurd *) congruence. + * (* absurd *) congruence. + + inv H3. simpl. destruct (zeq n 0). { contradiction. } + eapply IHlbi; eauto. +Qed. + +Lemma list_nth_z_find_bi_with_header: + forall ll lbi bi tlbi n bi' (rest : list Asm.instruction), + list_nth_z lbi (n - list_length_z ll) = Some bi -> + unfold_body lbi = OK tlbi -> + basic_to_instruction bi = OK bi' -> + Asm.find_instr n ((unfold_label ll) ++ (tlbi) ++ (rest)) = Some bi'. +Proof. + induction ll. + - unfold list_length_z. simpl. intros. + replace (n - 0) with n in H by omega. eapply list_nth_z_find_bi; eauto. + - intros. simpl. destruct (zeq n 0). + + rewrite list_length_z_cons in H. rewrite e in H. + replace (0 - (list_length_z ll + 1)) with (-1 - (list_length_z ll)) in H by omega. + generalize (list_length_z_pos ll). intros. + rewrite list_nth_z_neg in H; try omega. inversion H. + + rewrite list_length_z_cons in H. + replace (n - (list_length_z ll + 1)) with (n -1 - (list_length_z ll)) in H by omega. + eapply IHll; eauto. +Qed. + Lemma find_instr_bblock: forall n lb pos bb tlb (FINDBB: find_bblock pos lb = Some bb) @@ -484,6 +545,7 @@ Proof. destruct pos. + inv FINDBB. simpl. exploit unfold_car_cdr; eauto. intros (tbb & tlb' & UNFOLD_BBLOCK & UNFOLD' & UNFOLD_cons). + rewrite UNFOLD in UNFOLD_cons. inversion UNFOLD_cons. unfold unfold_bblock in UNFOLD_BBLOCK. destruct (zle (list_length_z (header bb)) 1). 2: { inversion UNFOLD_BBLOCK. } apply bind_inversion in UNFOLD_BBLOCK. @@ -493,12 +555,21 @@ Proof. remember (list_nth_z (header bb) n) as label_opt eqn:LBL. destruct label_opt. * (* nth instruction is a label *) eexists; split. { eapply is_nth_label; eauto. } - rewrite UNFOLD in UNFOLD_cons. inversion UNFOLD_cons. + inversion UNFOLD_cons. symmetry in LBL. - rewrite <- UNFOLD_BBLOCK. rewrite <- app_assoc. apply list_nth_z_find_label; auto. - * admit. + * remember (list_nth_z (body bb) (n - list_length_z (header bb))) as bi_opt eqn:BI. + destruct bi_opt. + -- (* nth instruction is a basic instruction *) + exploit list_nth_z_in; eauto. intros INBB. + exploit entire_body_translated; eauto. intros BI'. + destruct BI'. + eexists; split. + ++ eapply is_nth_basic; eauto. + ++ repeat (rewrite <- app_assoc). eapply list_nth_z_find_bi_with_header; eauto. + -- (* nth instruction is the exit instruction *) + admit. + unfold find_bblock in FINDBB; simpl in FINDBB; fold find_bblock in FINDBB. inversion UNFOLD as (UNFOLD'). apply bind_inversion in UNFOLD'. destruct UNFOLD' as (? & (UNFOLD_BBLOCK' & UNFOLD')). -- cgit