Absurd case in find_instr_bblock

n points to neither label nor basic instruction but there is also no
final exit instruction

1 files changed, 107 insertions, 1 deletions

diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index 6e54d399..3f48042e 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -619,6 +619,104 @@ Proof.
       eapply IHll; eauto.
 Qed.
 
+(* XXX unused *)
+Lemma range_list_nth_z:
+  forall (A: Type) (l: list A) n,
+  0 <= n < list_length_z l ->
+  exists x, list_nth_z l n = Some x.
+Proof.
+  induction l.
+  - intros. unfold list_length_z in H. simpl in H. omega.
+  - intros n. destruct (zeq n 0).
+    + intros. simpl. destruct (zeq n 0). { eauto. } contradiction.
+    + intros H. rewrite list_length_z_cons in H.
+      simpl. destruct (zeq n 0). { contradiction. }
+      replace (Z.pred n) with (n - 1) by omega.
+      eapply IHl; omega.
+Qed.
+
+Lemma list_nth_z_n_too_big:
+  forall (A: Type) (l: list A) n,
+  0 <= n ->
+  list_nth_z l n = None ->
+  n >= list_length_z l.
+Proof.
+  induction l.
+  - intros. unfold list_length_z. simpl. omega.
+  - intros. rewrite list_length_z_cons.
+    simpl in H0.
+    destruct (zeq n 0) as [N | N].
+    + inversion H0.
+    + (* XXX there must be a more elegant way to prove this simple fact *)
+      assert (n > 0). { omega. }
+      assert (0 <= n - 1). { omega. }
+      generalize (IHl (n - 1)). intros IH.
+      assert (n - 1 >= list_length_z l). { auto. }
+      assert (n > list_length_z l); omega.
+Qed.
+
+Lemma find_instr_past_header:
+  forall labels n rest,
+  list_nth_z labels n = None ->
+  Asm.find_instr n (unfold_label labels ++ rest) =
+  Asm.find_instr (n - list_length_z labels) rest.
+Proof.
+  induction labels as [| label labels' IH].
+  - unfold list_length_z; simpl; intros; rewrite Z.sub_0_r; reflexivity.
+  - intros. simpl. destruct (zeq n 0) as [N | N].
+    + rewrite N in H. inversion H.
+    + rewrite list_length_z_cons.
+      replace (n - (list_length_z labels' + 1)) with (n - 1 - list_length_z labels') by omega.
+      simpl in H. destruct (zeq n 0). { contradiction. }
+      replace (Z.pred n) with (n - 1) in H by omega.
+      apply IH; auto.
+Qed.
+
+(* very similar to find_instr_past_header *)
+Lemma find_instr_past_body:
+  forall lbi n tlbi rest,
+  list_nth_z lbi n = None ->
+  unfold_body lbi = OK tlbi ->
+  Asm.find_instr n (tlbi ++ rest) =
+  Asm.find_instr (n - list_length_z lbi) rest.
+Proof.
+  induction lbi.
+  - unfold list_length_z; simpl; intros ? ? ? ? H. inv H; rewrite Z.sub_0_r; reflexivity.
+  - intros n tlib ? NTH UNFOLD_BODY.
+    unfold unfold_body in UNFOLD_BODY. apply bind_inversion in UNFOLD_BODY.
+    destruct UNFOLD_BODY as (? & BI & H).
+    apply bind_inversion in H. destruct H as (? & UNFOLD_BODY' & CONS).
+    fold unfold_body in UNFOLD_BODY'. inv CONS.
+    simpl; destruct (zeq n 0) as [N|N].
+    + rewrite N in NTH; inversion NTH.
+    + rewrite list_length_z_cons.
+      replace (n - (list_length_z lbi + 1)) with (n - 1 - list_length_z lbi) by omega.
+      simpl in NTH. destruct (zeq n 0). { contradiction. }
+      replace (Z.pred n) with (n - 1)  in NTH by omega.
+      apply IHlbi; auto.
+Qed.
+
+Lemma n_beyond_body:
+  forall bb n,
+  0 <= n < size bb ->
+  list_nth_z (header bb) n = None ->
+  list_nth_z (body bb) (n - list_length_z (header bb)) = None ->
+  n >= Z.of_nat (length (header bb) + length (body bb)).
+Proof.
+  intros.
+  assert (0 <= n). { omega. }
+  generalize (list_nth_z_n_too_big label (header bb) n H2 H0). intros.
+  generalize (list_nth_z_n_too_big _ (body bb) (n - list_length_z (header bb))). intros.
+  unfold size in H.
+
+  assert (0 <= n - list_length_z (header bb)). { omega. }
+  assert (n - list_length_z (header bb) >= list_length_z (body bb)). { apply H4; auto. }
+
+  assert (n >= list_length_z (header bb) + list_length_z (body bb)). { omega. }
+  rewrite Nat2Z.inj_add.
+  repeat (rewrite <- length_agree). assumption.
+Qed.
+
 Lemma find_instr_bblock:
   forall n lb pos bb tlb
   (FINDBB: find_bblock pos lb = Some bb)
@@ -656,7 +754,15 @@ Proof.
             ++ 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.
+           rewrite <- app_assoc. rewrite find_instr_past_header; auto.
+           rewrite <- app_assoc. erewrite find_instr_past_body; eauto.
+           remember (exit bb) as exit_opt eqn:EXIT. destruct exit_opt.
+           ++ admit.
+           ++ (* absurd *)
+              generalize n_beyond_body. intros.
+              assert (n >= Z.of_nat (Datatypes.length (header bb) + Datatypes.length (body bb))). { auto. }
+              unfold size in SIZE. rewrite <- EXIT in SIZE. simpl in SIZE.
+              destruct SIZE as (? & SIZE'). rewrite Nat.add_0_r in SIZE'. omega.
     + 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')).