From 1975837dbd2b3a924bc77fd4e64cce0a37c21994 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 24 Nov 2020 17:34:53 +0100 Subject: Restoring asmgenproof on multiple labels issue --- aarch64/Asmgenproof.v | 197 +++++++------------------------------------------- 1 file changed, 25 insertions(+), 172 deletions(-) (limited to 'aarch64/Asmgenproof.v') 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), -- cgit