Complete size_header

1 files changed, 66 insertions, 1 deletions

diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index d69d8886..36d39695 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -535,11 +535,76 @@ Proof.
   omega.
 Qed.
 
+Lemma all_blocks_translated:
+  forall bbs tc,
+  unfold bbs = OK tc ->
+  forall bb, In bb bbs ->
+  exists c, unfold_bblock bb = OK c.
+Proof.
+  induction bbs as [| bb bbs IHbbs].
+  - contradiction.
+  - intros ? UNFOLD ? IN.
+    (* unfold proceeds by unfolding the basic block at the head of the list and
+     * then recurring *)
+    unfold unfold in UNFOLD.
+    apply bind_inversion in UNFOLD. destruct UNFOLD as (? & UBB). destruct UBB as (UBB & REST).
+    apply bind_inversion in REST. destruct REST as (? & UNFOLD').
+    fold unfold in UNFOLD'. destruct UNFOLD'.
+    (* basic block is either in head or tail *)
+    inversion IN as [EQ | NEQ].
+    + rewrite <- EQ; eexists; eauto.
+    + eapply IHbbs; eauto.
+Qed.
+
+Lemma bblock_in_bblocks b f bb: forall
+  tc pos
+  (FINDF: Genv.find_funct_ptr ge b = Some (Internal f))
+  (UNFOLD: unfold (fn_blocks f) = OK tc)
+  (FINDBB: find_bblock pos (fn_blocks f) = Some bb),
+  In bb (fn_blocks f).
+Proof.
+  induction (fn_blocks f).
+  - intros. inversion FINDBB.
+  - destruct pos.
+    + intros. inversion FINDBB as (EQ). rewrite <- EQ. apply in_eq.
+    + intros.
+      unfold unfold in UNFOLD.
+      apply bind_inversion in UNFOLD. destruct UNFOLD as (? & UBB). destruct UBB as (UBB & REST).
+      apply bind_inversion in REST. destruct REST as (? & UNFOLD').
+      fold unfold in UNFOLD'. destruct UNFOLD'.
+      unfold find_bblock in FINDBB. simpl in FINDBB.
+      fold find_bblock in FINDBB.
+      apply in_cons. eapply IHb0; eauto.
+    + intros. inversion FINDBB.
+Qed.
+
+Lemma blocks_translated b pos f bb: forall
+  (FINDF: Genv.find_funct_ptr ge b = Some (Internal f))
+  (FINDBB: find_bblock pos (fn_blocks f) = Some bb),
+  exists tbb, unfold_bblock bb = OK tbb.
+Proof.
+  intros.
+  exploit internal_functions_unfold; eauto.
+  intros (tc & FINDtf & TRANStf & ?).
+  exploit bblock_in_bblocks; eauto. intros BB.
+  eapply all_blocks_translated; eauto.
+Qed.
+
 Lemma size_header b pos f bb: forall
   (FINDF: Genv.find_funct_ptr ge b = Some (Internal f))
   (FINDBB: find_bblock pos (fn_blocks f) = Some bb),
   list_length_z (header bb) <= 1.
-Admitted.
+Proof.
+  intros.
+  exploit internal_functions_unfold; eauto.
+  intros (tc & FINDtf & TRANStf & ?).
+  exploit blocks_translated; eauto. intros TBB.
+
+  unfold unfold_bblock in TBB.
+  destruct (zle (list_length_z (header bb)) 1).
+  - assumption.
+  - destruct TBB as (? & TBB). discriminate TBB.
+Qed.
 
 Lemma list_nth_z_neg A (l: list A): forall n,
   n < 0 -> list_nth_z l n = None.