From a70e5fc5b6310513803cf26ca91bdc3b4384d706 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 19 Oct 2020 16:27:36 +0200 Subject: Improvements in Asmgenproof * Deleting the (duplicated) length_agree lemma (there was an equivalent lemma named list_length_z_nat for this purpose) * Lemmas about labels : * label_in_header_list * no_label_in_basic_inst * label_pos_body * label_pos_preserved_gen and label_pos_preserved --- aarch64/Asmgenproof.v | 143 +++++++++++++++++++++++++++++++++++++++----------- 1 file changed, 111 insertions(+), 32 deletions(-) (limited to 'aarch64/Asmgenproof.v') diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index 7d1f1d05..db6548fe 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -22,7 +22,7 @@ Require Machblockgenproof Asmblockgenproof. Require Import Asmgen. Require Import Axioms. Require Import IterList. - +Require Import Ring. Module Asmblock_PRESERVATION. @@ -314,18 +314,18 @@ Proof. unfold list_length_z; simpl; rewrite list_length_add_acc; reflexivity. Qed. -Lemma length_agree A (l : list A): - list_length_z l = Z.of_nat (length l). -Proof. - induction l as [| ? l IH]; intros. - - unfold list_length_z; reflexivity. - - simpl; rewrite list_length_z_cons, Zpos_P_of_succ_nat; omega. -Qed. +(*Lemma length_agree A (l : list A):*) + (*list_length_z l = Z.of_nat (length l).*) +(*Proof.*) + (*induction l as [| ? l IH]; intros.*) + (*- unfold list_length_z; reflexivity.*) + (*- simpl; rewrite list_length_z_cons, Zpos_P_of_succ_nat; omega.*) +(*Qed.*) Lemma bblock_size_aux bb: size bb = list_length_z (header bb) + list_length_z (body bb) + Z.of_nat (length_opt (exit bb)). Proof. unfold size. - repeat (rewrite length_agree). repeat (rewrite Nat2Z.inj_add). reflexivity. + repeat (rewrite list_length_z_nat). repeat (rewrite Nat2Z.inj_add). reflexivity. Qed. Lemma header_size_lt_block_size bb: @@ -334,14 +334,14 @@ Proof. rewrite bblock_size_aux. generalize (bblock_non_empty bb); intros NEMPTY; destruct NEMPTY as [HDR|EXIT]. - destruct (body bb); try contradiction; rewrite list_length_z_cons; - repeat rewrite length_agree; omega. - - destruct (exit bb); try contradiction; simpl; repeat rewrite length_agree; omega. + repeat rewrite list_length_z_nat; omega. + - destruct (exit bb); try contradiction; simpl; repeat rewrite list_length_z_nat; omega. Qed. Lemma body_size_le_block_size bb: list_length_z (body bb) <= size bb. Proof. - rewrite bblock_size_aux; repeat rewrite length_agree; omega. + rewrite bblock_size_aux; repeat rewrite list_length_z_nat; omega. Qed. @@ -516,7 +516,7 @@ Proof. unfold size. rewrite equal_header_size, equal_exit_size. erewrite equal_body_size; eauto. - rewrite length_agree. + rewrite list_length_z_nat. repeat (rewrite app_length). rewrite plus_assoc. auto. Qed. @@ -537,12 +537,12 @@ Proof. destruct (zeq pos 0). + inv FINDBB. exploit bblock_size_preserved; eauto; intros SIZE; rewrite SIZE. - repeat (rewrite length_agree). rewrite app_length, Nat2Z.inj_add. + repeat (rewrite list_length_z_nat). rewrite app_length, Nat2Z.inj_add. omega. + generalize (IHbbs tbbs' (pos - size bb) bb' FINDBB UNFOLD). intros IH. exploit bblock_size_preserved; eauto; intros SIZE. - repeat (rewrite length_agree); rewrite app_length. - rewrite Nat2Z.inj_add; repeat (rewrite <- length_agree). + repeat (rewrite list_length_z_nat); rewrite app_length. + rewrite Nat2Z.inj_add; repeat (rewrite <- list_length_z_nat). omega. Qed. @@ -776,7 +776,7 @@ Proof. assert (n >= list_length_z (header bb) + list_length_z (body bb)). { omega. } rewrite Nat2Z.inj_add. - repeat (rewrite <- length_agree). assumption. + repeat (rewrite <- list_length_z_nat). assumption. Qed. Lemma exec_arith_instr_dont_move_PC ai rs rs': forall @@ -893,12 +893,12 @@ Proof. unfold size in SIZE. rewrite <- EXIT in SIZE. simpl in SIZE. destruct SIZE as (LOWER & UPPER). repeat (rewrite Nat2Z.inj_add in UPPER). - repeat (rewrite <- length_agree in UPPER). repeat (rewrite Nat2Z.inj_add in NGE). - repeat (rewrite <- length_agree in NGE). simpl in UPPER. + repeat (rewrite <- list_length_z_nat in UPPER). repeat (rewrite Nat2Z.inj_add in NGE). + repeat (rewrite <- list_length_z_nat in NGE). simpl in UPPER. assert (n = list_length_z (header bb) + list_length_z (body bb)). { omega. } assert (n = size bb - 1). { unfold size. rewrite <- EXIT. simpl. - repeat (rewrite Nat2Z.inj_add). repeat (rewrite <- length_agree). simpl. omega. + repeat (rewrite Nat2Z.inj_add). repeat (rewrite <- list_length_z_nat). simpl. omega. } symmetry in EXIT. eexists; split. @@ -1297,8 +1297,8 @@ Proof. assert (tc' = tc) by congruence; subst. exploit (find_instr_bblock (list_length_z (header bb) + Z.of_nat n)); eauto. { unfold size; split. - - rewrite length_agree; omega. - - repeat (rewrite length_agree). repeat (rewrite Nat2Z.inj_add). omega. } + - rewrite list_length_z_nat; omega. + - repeat (rewrite list_length_z_nat). repeat (rewrite Nat2Z.inj_add). omega. } intros (i & NTH & FIND_INSTR). exists i; intros. inv NTH. @@ -1308,7 +1308,7 @@ Proof. rewrite Z.add_assoc in FIND_INSTR; intuition. - (* absurd *) rewrite bblock_size_aux in H0; - rewrite H in H0; simpl in H0; repeat rewrite length_agree in H0; omega. + rewrite H in H0; simpl in H0; repeat rewrite list_length_z_nat in H0; omega. Qed. (** "is_tail" auxiliary lemma about is_tail to move in IterList ou Coqlib (déplacer aussi Machblockgenproof.is_tail_app_inv) ? *) @@ -1406,7 +1406,11 @@ Proof. assert (BOUNDBB: Ptrofs.unsigned ofs + size bb <= Ptrofs.max_unsigned) by (eapply size_of_blocks_bounds; eauto). exploit exec_basic_simulation; eauto. - { admit. (* TODO *) } + { assert (list_length_z (header bb) >= 0) by eapply list_length_z_pos. + assert (list_length_z (header bb) < size bb) by eapply header_size_lt_block_size. + destruct BOUNDBB. + (*assert (size bb < Ptrofs.max_unsigned) by omega.*) + admit. (* TODO *) } intros (rs_next' & m_next' & EXEC_INSTR & MI_NEXT). (* Code from the star' lemma bellow. We need this to exploit exec_step_internal. *) exploit exec_basic_dont_move_PC; eauto. intros AGPC. @@ -1422,8 +1426,8 @@ Proof. (* Execute internal step. *) exploit (Asm.exec_step_internal tge b); eauto. { (* unfold Ptrofs.add. repeat (rewrite Ptrofs.unsigned_repr); - try rewrite length_agree; try split; try omega. - simpl; rewrite <- length_agree; assumption. *) + try rewrite list_length_z_nat; try split; try omega. + simpl; rewrite <- list_length_z_nat; assumption. *) admit. (* TODO *) } (* This is our STEP hypothesis. *) @@ -1508,16 +1512,91 @@ Proof. exploit list_nth_z_range; eauto. omega. Qed. -Lemma basic_block_header_length: forall bb, - (length (header bb) <= 1)%nat. +Lemma label_in_header_list lbl a: + is_label lbl a = true -> list_length_z (header a) <= 1 -> header a = lbl :: nil. Proof. -Admitted. - -Lemma label_pos_preserved f lbl z tf: forall + intros. + eapply is_label_correct_true in H. + destruct (header a). + - eapply in_nil in H. contradiction. + - rewrite list_length_z_cons in H0. + assert (list_length_z l0 >= 0) by eapply list_length_z_pos. + assert (list_length_z l0 = 0) by omega. + rewrite list_length_z_nat in H2. + assert (Datatypes.length l0 = 0%nat) by omega. + eapply length_zero_iff_nil in H3. subst. + unfold In in H. destruct H. + + subst; eauto. + + destruct H. +Qed. + +Lemma no_label_in_basic_inst: forall a lbl x, + basic_to_instruction a = OK x -> Asm.is_label lbl x = false. +Proof. + intros. + destruct a; simpl in *; + repeat destruct i; simpl in *; + try (try destruct_reg_inv; monadInv H; simpl in *; reflexivity). +Qed. + +Lemma label_pos_body bdy: forall c1 c2 z ex lbl + (HUNF : unfold_body bdy = OK c2), + Asm.label_pos lbl (z + Z.of_nat ((Datatypes.length bdy) + length_opt ex)) c1 = Asm.label_pos lbl (z) ((c2 ++ unfold_exit ex) ++ c1). +Proof. + induction bdy. + - intros. inversion HUNF. simpl in *. + destruct ex eqn:EQEX. + + simpl in *. unfold Asm.is_label. destruct c; simpl; try congruence. + destruct i; simpl; try congruence. + + simpl in *. ring_simplify (z + 0). auto. + - intros. inversion HUNF; clear HUNF. monadInv H0. simpl in *. + erewrite no_label_in_basic_inst; eauto. rewrite <- IHbdy; eauto. + erewrite Zpos_P_of_succ_nat. + apply f_equal2; auto. omega. +Qed. + +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. + - intros. simpl in *. inversion HUNF. simpl. reflexivity. + - intros. simpl in *. monadInv HUNF. unfold unfold_bblock in EQ. + destruct (zle _ _); try congruence. monadInv EQ. + destruct (is_label _ _) eqn:EQLBL. + + erewrite label_in_header_list; eauto. + simpl in *. destruct (peq lbl lbl); try congruence. + + erewrite IHbbs; eauto. + assert (Asm.label_pos lbl (z + size a) x0 = Asm.label_pos lbl (z + list_length_z (header a)) ((x1 ++ unfold_exit (exit a)) ++ x0)). + { unfold size. + rewrite <- plus_assoc. rewrite Nat2Z.inj_add. + rewrite list_length_z_nat. + replace (z + (Z.of_nat (Datatypes.length (header a)) + Z.of_nat (Datatypes.length (body a) + length_opt (exit a)))) with (z + Z.of_nat (Datatypes.length (header a)) + Z.of_nat (Datatypes.length (body a) + length_opt (exit a))) by omega. + eapply (label_pos_body (body a) x0 x1 (z + Z.of_nat (Datatypes.length (header a))) (exit a) lbl). auto. } + unfold is_label in *. + destruct (header a). + * replace (z + list_length_z (@nil label)) with (z) in H; eauto. + unfold list_length_z. simpl. omega. + * assert (l1 = nil). + { destruct l1; try congruence. rewrite !list_length_z_cons in l. + assert (list_length_z l2 >= 0) by eapply list_length_z_pos. + assert (list_length_z l2 + 1 + 1 >= 2) by omega. + assert (2 <= 1) by omega. contradiction H2. omega. } + subst. simpl in *. destruct (in_dec _ _) as [HIN|HNIN]; try congruence. + simpl in *. + destruct (peq _ _); try intuition congruence. +Qed. + +Lemma label_pos_preserved b f lbl z tf: forall + (FIND: Genv.find_funct_ptr ge b = Some (Internal f)) (FINDF: transf_function f = OK tf), label_pos lbl z (fn_blocks f) = Asm.label_pos lbl z (Asm.fn_code tf). Proof. -Admitted. + intros. + eapply label_pos_preserved_gen. + unfold transf_function in FINDF. monadInv FINDF. + destruct zlt; try congruence. inversion EQ0. eauto. +Qed. Lemma goto_label_preserved bb rs1 m1 rs1' m1' rs2 m2 lbl f tf v: forall (FINDF: transf_function f = OK tf) -- cgit