From 45ce514eaeb2fb1d80cb145ba769cd281195cb69 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Sun, 1 Nov 2020 13:02:25 +0100 Subject: Yarpgen C file to test multiple labels and corresponding code In this branch I remove the multiple label limitation to pass some tests but the proof is admitted ! --- aarch64/Asmgenproof.v | 195 +++++++++++++++++++++++++++++++++++++++++++------- 1 file changed, 171 insertions(+), 24 deletions(-) (limited to 'aarch64/Asmgenproof.v') diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index f28bcb2e..54cc2364 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), -- cgit