Merge branch 'aarch64_block_multiple_labels' into aarch64-postpass

1 files changed, 171 insertions, 24 deletions

diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index bff18716..62b65a14 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -450,21 +450,22 @@ Proof.
   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.
-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 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.*)
+(*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.<]*)
+(*Admitted.*)
 
 Lemma list_nth_z_neg A (l: list A): forall n,
   n < 0 -> list_nth_z l n = None.
@@ -511,7 +512,7 @@ Lemma bblock_size_preserved bb tb:
   size bb = list_length_z tb.
 Proof.
   unfold unfold_bblock. intros UNFOLD_BBLOCK.
-  destruct (zle (list_length_z (header bb)) 1). 2: { inversion UNFOLD_BBLOCK. }
+  (*destruct (zle (list_length_z (header bb)) 1). 2: { inversion UNFOLD_BBLOCK. }*)
   apply bind_inversion in UNFOLD_BBLOCK. destruct UNFOLD_BBLOCK as (? & UNFOLD_BODY & CONS).
   inversion CONS.
   unfold size.
@@ -863,7 +864,7 @@ Proof.
       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. }
+      (*destruct (zle (list_length_z (header bb)) 1). 2: { inversion UNFOLD_BBLOCK. }*)
       apply bind_inversion in UNFOLD_BBLOCK.
       destruct UNFOLD_BBLOCK as (? & UNFOLD_BODY & H).
       inversion H as (UNFOLD_BBLOCK).
@@ -935,10 +936,57 @@ Lemma exec_header_simulation b ofs f bb rs m: forall
   exists s', star Asm.step tge (State rs m) E0 s'
              /\ match_internal (list_length_z (header bb)) (State rs m) s'.
 Proof.
+Admitted.
+  (*  intros.
+  exploit internal_functions_unfold; eauto.
+  intros (tc & FINDtf & TRANStf & _).
+  induction (header bb) eqn:EQhead.
+  + eexists; split.
+    - eapply star_refl.
+    - split; eauto.
+      unfold list_length_z; rewrite !ATPC; simpl.
+      rewrite Ptrofs.add_zero; auto.
+  + assert (Lgen: list_length_z (header bb) < (size bb)) by eapply header_size_lt_block_size.
+    assert (Lpos: list_length_z (l) >= 0) by eapply list_length_z_pos.
+    assert (Lsmaller: list_length_z (l) < list_length_z (header bb)).
+    { rewrite EQhead. rewrite list_length_z_cons. omega. }
+
+
+
+    exploit (find_instr_bblock (list_length_z (l))); eauto.
+    { generalize (bblock_size_pos bb). rewrite EQhead in *. intros. omega. }
+    intros (i & NTH & FIND_INSTR).
+    inv NTH.
+    - eexists. split. eapply star_one. eapply Asm.exec_step_internal; eauto.
+      inv FIND_INSTR.
+      eapply list_nth_z_range in H. rewrite EQhead in H.
+    eapply Nat.lt_neq in H0.
+
+
+  
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
   intros.
   exploit internal_functions_unfold; eauto.
   intros (tc & FINDtf & TRANStf & _).
-  assert (BNDhead: list_length_z (header bb) <= 1). { eapply size_header; eauto. }
+  (*assert (BNDhead: list_length_z (header bb) <= 1). { eapply size_header; eauto. }*)
   destruct (header bb) as [|l[|]] eqn: EQhead.
   + (* header nil *)
     eexists; split.
@@ -965,9 +1013,67 @@ Proof.
     * (* absurd case *)
       rewrite bblock_size_aux, Lhead in *. generalize (bblock_size_aux_pos bb). omega.
   + (* absurd case *)
+    assert (Lgen: list_length_z (header bb) < (size bb)) by eapply header_size_lt_block_size.
+    assert (Ll1pos: list_length_z (l1) >= 0) by eapply list_length_z_pos.
+    assert (Lpos: list_length_z (header bb) - 1 > 0).
+    { rewrite EQhead. erewrite !list_length_z_cons. omega. }
+    exploit (find_instr_bblock (list_length_z (l :: l0 :: l1))); eauto.
+    { generalize (bblock_size_pos bb). rewrite EQhead in *. intros. omega. }
+    intros (i & NTH & FIND_INSTR).
+    inv NTH.
+    (*eapply list_nth_z_range in H. rewrite EQhead in H. destruct H.*)
+    (*eapply Nat.lt_neq in H0.*)
+    * rewrite EQhead in *; simpl in H.
+      assert ((list_length_z (l :: l0 :: l1) - 1) <> 0) by omega.
+      destruct zeq.
+      - rewrite e in FIND_INSTR. cutrewrite (Ptrofs.unsigned ofs + 0 = Ptrofs.unsigned ofs) in FIND_INSTR; try omega.
+      - destruct zeq; try (rewrite <- Z.sub_1_r in e; congruence).
+        inv H. eexists; split.
+        { eapply star_one. eapply list_nth_z_find_label in H2.
+          erewrite find_instr_past_header in H2.
+          assert (Z.pred (Z.pred (list_length_z (l :: l0 :: l1))) = list_length_z l1).
+          { erewrite <- !Z.sub_1_r. erewrite !list_length_z_cons. omega. }
+          replace (Z.pred (Z.pred (list_length_z (l :: l0 :: l1))) - list_length_z l1) with (0) in H2 by omega.
+          rewrite <- FIND_INSTR in H2. 
+          unfold find_instr in H2.
+          destruct tc eqn:HTC.
+          { simpl in *. inversion FIND_INSTR. }
+          { simpl in *. 
+
+            destruct zeq eqn:HZEQ.
+            
+            { fold find_instr in H2. assert (0 <= Ptrofs.unsigned ofs <= Ptrofs.max_unsigned) by eapply Ptrofs.unsigned_range_2. assert (list_length_z (l :: l0 :: l1) > 0) by omega.
+              assert (Ptrofs.unsigned ofs = - list_length_z (l :: l0 :: l1)) by omega.
+              assert (Ptrofs.unsigned ofs = 0) by omega. 
+              assert (list_length_z (l :: l0 :: l1)  = 0) by omega. congruence. }
+            { simpl in *. 
+              rewrite H4 in H5. 
+          
+          eapply Asm.exec_step_internal; eauto.
+
+      destruct zeq.
+      - inv H. eexists. split.
+        assert (list_length_z (l :: l2 :: l1) - 1 = 1) by omega. rewrite H in *.
+        { eapply star_one. exploit (find_instr_bblock 0); eauto; try omega.
+          intros (i' & NTH' & FIND_INSTR').
+          eapply Asm.exec_step_internal; eauto.
+          
+
+      inv H.
+      cutrewrite (Ptrofs.unsigned ofs + 0 = Ptrofs.unsigned ofs) in FIND_INSTR; try omega.
+      eexists. split.
+      - eapply star_one.
+        eapply Asm.exec_step_internal; eauto.
+        simpl; eauto.
+      - unfold list_length_z; simpl. split. eauto.
+        intros r; destruct r; simpl; congruence || auto.
+    * (* absurd case *)
+      erewrite list_nth_z_neg in * |-; [ congruence | rewrite Lhead; omega].
+    * (* absurd case *)
+      rewrite bblock_size_aux, Lhead in *. generalize (bblock_size_aux_pos bb). omega.
     unfold list_length_z in BNDhead. simpl in *.
     generalize (list_length_z_aux_increase _ l1 2); omega.
-Qed.
+Qed.*)
 
 Lemma eval_addressing_preserved a rs1 rs2:
   (forall r : preg, r <> PC -> rs1 r = rs2 r) ->
@@ -1445,7 +1551,8 @@ Proof.
     2: {
       assert (BOUNDOFS: 0 <= Ptrofs.unsigned ofs <= Ptrofs.max_unsigned) by eapply Ptrofs.unsigned_range_2.
       assert (list_length_z (body bb) <= size bb) by eapply body_size_le_block_size.
-      assert (list_length_z (header bb) <= 1). { eapply size_header; eauto. }
+      assert (list_length_z (header bb) +  list_length_z (body bb) <= size bb).
+      { generalize bblock_size_aux. intros. rewrite H0. generalize bblock_size_aux. intros. omega. }
       omega. }
     try rewrite list_length_z_nat; try split;
     simpl; rewrite <- !list_length_z_nat;
@@ -1601,16 +1708,56 @@ Proof.
   assert (2 <= 1) by omega. contradiction H1. omega.
 Qed.
 
+(*Lemma unfold_label_not_nil: forall a lbl*)
+  (*(HIN: In lbl (header a)),*)
+  (*unfold_label (header a) <> nil.*)
+(*Proof.*)
+  (*intros. induction (header a).*)
+  (*- contradiction.*)
+  (*- destruct (peq lbl a0);*)
+    (*simpl; unfold not; intros; generalize nil_cons; intros;*)
+      (*specialize (H0 label a0 l); unfold not in H0; congruence.*)
+(*Qed.*)
+
+(*Lemma label_pos_in a: forall lbl z*)
+  (*(EQLBL: In lbl (header a)),*)
+  (*Asm.label_pos lbl z (unfold_label (header a)) = Some z.*)
+(*Proof.*)
+  (*intros.*)
+  (*induction (Asm.label_pos _ _ _) eqn:Hind.*)
+  (*- induction (unfold_label (header a)) eqn:Hunf.*)
+    (*+ eapply unfold_label_not_nil in EQLBL. congruence.*)
+    (*+ simpl in *. *)
+      (*destruct (Asm.is_label _ _) eqn:Hlbla.*)
+      (** symmetry. assumption.*)
+      (** apply IHl.*)
+
+      (*induction (header a).*)
+      (** apply in_nil in EQLBL. contradiction.*)
+      (** simpl in *.*)
+  (*- unfold Asm.label_pos.*)
+    (*destruct (Asm.is_label) eqn:EQis; try reflexivity.*)
+    (*destruct (peq lbl (PLabel a0)).*)
+
 Lemma label_pos_preserved_gen bbs: forall lbl c z
   (HUNF: unfold bbs = OK c),
   label_pos lbl z bbs = Asm.label_pos lbl z c.
 Proof.
-  induction bbs.
+Admitted.
+(*  induction bbs.
   - intros. simpl in *. inversion HUNF. simpl. reflexivity.
   - intros. simpl in *. monadInv HUNF. unfold unfold_bblock in EQ.
-    destruct (zle _ _); try congruence. monadInv EQ.
+    (*destruct (zle _ _); try congruence.*)
+    monadInv EQ.
     destruct (is_label _ _) eqn:EQLBL.
-    + erewrite label_in_header_list; eauto.
+    erewrite <- is_label_correct_true in EQLBL.
+    + induction (Asm.label_pos) eqn:Hind.
+      * 
+    + induction (header a) eqn:Hhead.
+      * apply in_nil in EQLBL. contradiction.
+      * simpl in *. destruct peq; try reflexivity.
+        erewrite IHl. 
+      erewrite label_in_header_list; eauto.
       simpl in *. destruct (peq lbl lbl); try congruence.
     + erewrite IHbbs; eauto.
       rewrite (asm_label_pos_header z a x0 x1 lbl); auto.
@@ -1622,7 +1769,7 @@ Proof.
         subst. simpl in *. destruct (in_dec _ _); try congruence.
         simpl in *.
         destruct (peq _ _); try intuition congruence.
-Qed.
+Qed.*)
 
 Lemma label_pos_preserved f lbl z tf: forall
   (FINDF: transf_function f = OK tf),