Restoring asmgenproof on multiple labels issue

1 files changed, 25 insertions, 172 deletions

diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index 7266cce8..c41d0a0b 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -450,22 +450,21 @@ 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.<]*)
-(*Admitted.*)
+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 list_nth_z_neg A (l: list A): forall n,
   n < 0 -> list_nth_z l n = None.
@@ -512,7 +511,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.
@@ -865,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).
@@ -937,57 +936,10 @@ 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.
@@ -1002,7 +954,7 @@ Admitted.
     intros (i & NTH & FIND_INSTR).
     inv NTH.
     * rewrite EQhead in H; simpl in H. inv H.
-      cutrewrite (Ptrofs.unsigned ofs + 0 = Ptrofs.unsigned ofs) in FIND_INSTR; try omega.
+      replace (Ptrofs.unsigned ofs + 0) with (Ptrofs.unsigned ofs) in FIND_INSTR by omega.
       eexists. split.
       - eapply star_one.
         eapply Asm.exec_step_internal; eauto.
@@ -1014,67 +966,9 @@ Admitted.
     * (* 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) ->
@@ -1573,8 +1467,7 @@ 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) +  list_length_z (body bb) <= size bb).
-      { generalize bblock_size_aux. intros. rewrite H0. generalize bblock_size_aux. intros. omega. }
+      assert (list_length_z (header bb) <= 1). { eapply size_header; eauto. }
       omega. }
     try rewrite list_length_z_nat; try split;
     simpl; rewrite <- !list_length_z_nat;
@@ -1730,56 +1623,16 @@ 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.
-Admitted.
-(*  induction bbs.
+  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 <- 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.
+    + 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.
@@ -1791,7 +1644,7 @@ Admitted.
         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),