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.

2 files changed, 76 insertions, 12 deletions

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')).