From 16129a71dcb593beca6e17214167117b4e10889c Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Thu, 15 Oct 2020 13:09:42 +0200 Subject: Progress in exec_basic_simu - New ltacs - simplifications - new subcases - two lemmas for nextinstr agree --- aarch64/Asmgenproof.v | 252 +++++++++++++++++++++++++++++--------------------- 1 file changed, 148 insertions(+), 104 deletions(-) (limited to 'aarch64/Asmgenproof.v') diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index 8003b975..173ce8f8 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -977,6 +977,79 @@ Qed. Ltac next_stuck_cong := try (unfold Next, Stuck in *; congruence). +Ltac inv_ok_eq := + repeat match goal with + | [EQ: OK ?x = OK ?y |- _ ] + => inversion EQ; clear EQ; subst + end. + +Ltac reg_rwrt := + match goal with + | [e: DR _ = DR _ |- _ ] + => rewrite e in * + end. + +Ltac destruct_reg_inv := + repeat match goal with + | [ H : match ?reg with _ => _ end = _ |- _ ] + => simpl in *; destruct reg; try congruence; try inv_ok_eq; try reg_rwrt + end. + +Ltac destruct_ireg_inv := + repeat match goal with + | [ H : match ?reg with _ => _ end = _ |- _ ] + => destruct reg as [[r|]|]; try congruence; try inv_ok_eq; subst + end. + +Ltac destruct_reg_size := + simpl in *; + match goal with + | [ |- context [ match ?reg with _ => _ end ] ] + => destruct reg; try congruence + end. + +Ltac find_rwrt_ag := + simpl in *; + match goal with + | [ AG: forall r, r <> ?PC -> _ r = _ r |- _ ] + => repeat rewrite <- AG; try congruence + end. + +Ltac inv_matchi := + match goal with + | [ MATCHI : match_internal _ _ _ |- _ ] + => inversion MATCHI; subst; find_rwrt_ag + end. + +Ltac destruct_ir0_reg := + match goal with + | [ |- context [ ir0 _ _ ?r ] ] + => unfold ir0 in *; destruct r; find_rwrt_ag; eauto + end. + +Ltac update_x_access_x := + subst; rewrite !Pregmap.gss; auto. + +Ltac update_x_access_r := + rewrite !Pregmap.gso; auto. + +Lemma nextinstr_agree_but_pc rs1 rs2: forall + (AG: forall r, r <> PC -> rs1 r = rs2 r), + forall r, r <> PC -> rs1 r = Asm.nextinstr rs2 r. +Proof. + intros; unfold Asm.nextinstr in *; rewrite Pregmap.gso in *; eauto. +Qed. + +Lemma ptrofs_nextinstr_agree rs1 rs2 n: forall + (BOUNDED : 0 <= n <= Ptrofs.max_unsigned) + (AGPC : Val.offset_ptr (rs1 PC) (Ptrofs.repr n) = rs2 PC), + Val.offset_ptr (rs1 PC) (Ptrofs.repr (n + 1)) = Asm.nextinstr rs2 PC. +Proof. + intros; unfold Asm.nextinstr; rewrite Pregmap.gss. + rewrite <- Ptrofs.unsigned_one; rewrite <- (Ptrofs.unsigned_repr n); eauto; + rewrite <- Ptrofs.add_unsigned; rewrite <- Val.offset_ptr_assoc; rewrite AGPC; eauto. +Qed. + Lemma load_preserved n rs1 m1 rs1' m1' rs2 m2 rd chk f a: forall (BOUNDED: 0 <= n <= Ptrofs.max_unsigned) (MATCHI: match_internal n (State rs1 m1) (State rs2 m2)) @@ -990,14 +1063,9 @@ Proof. rewrite <- (eval_addressing_preserved a rs1 rs2); auto. destruct (Mem.loadv _ _ _). + inversion HLOAD; auto. repeat (econstructor; eauto). - * intros. unfold Asm.nextinstr. rewrite (Pregmap.gso (i := r) (j := PC)); auto. - destruct (PregEq.eq r rd). - { subst. rewrite !Pregmap.gss; auto. } - { rewrite !Pregmap.gso; auto. } - * unfold Asm.nextinstr. rewrite Pregmap.gss. rewrite !Pregmap.gso; try congruence. - rewrite <- Ptrofs.unsigned_one. rewrite <- (Ptrofs.unsigned_repr n). - rewrite <- Ptrofs.add_unsigned. rewrite <- Val.offset_ptr_assoc. rewrite EQPC. - reflexivity. omega. + * eapply nextinstr_agree_but_pc; intros. + destruct (PregEq.eq r rd); try update_x_access_x; try update_x_access_r. + * eapply ptrofs_nextinstr_agree; eauto. + next_stuck_cong. Qed. @@ -1014,12 +1082,9 @@ Proof. rewrite <- (eval_addressing_preserved a rs1 rs2); auto. destruct (Mem.storev _ _ _ _). + inversion HSTORE; auto. repeat (econstructor; eauto). - * intros. unfold Asm.nextinstr. rewrite (Pregmap.gso (i := r) (j := PC)); auto. + * eapply nextinstr_agree_but_pc; intros. subst. apply EQR. auto. - * unfold Asm.nextinstr. rewrite Pregmap.gss. - rewrite <- Ptrofs.unsigned_one. rewrite <- (Ptrofs.unsigned_repr n). - rewrite <- Ptrofs.add_unsigned. rewrite <- Val.offset_ptr_assoc. subst. rewrite EQPC. - reflexivity. omega. + * eapply ptrofs_nextinstr_agree; subst; eauto. + next_stuck_cong. Qed. @@ -1034,63 +1099,11 @@ Proof. intros. inversion MATCHI as [n0 r1 mx1 r2 mx2 EQM EQR EQPC]; subst. inversion NEXTI. repeat (econstructor; eauto). - * intros. unfold Asm.nextinstr. - rewrite (Pregmap.gso (i := PC) (j := x)); try congruence. - rewrite (Pregmap.gso (i := r) (j := PC)); try congruence. - destruct (PregEq.eq r x). - { subst. rewrite !Pregmap.gss; auto. } - { rewrite !Pregmap.gso; try congruence. auto. } - * unfold Asm.nextinstr. - rewrite Pregmap.gss. rewrite !(Pregmap.gso (i := PC) (j := x)); try congruence. - rewrite <- Ptrofs.unsigned_one. rewrite <- (Ptrofs.unsigned_repr n); eauto. - rewrite <- Ptrofs.add_unsigned. rewrite <- Val.offset_ptr_assoc. rewrite EQPC; eauto. + * eapply nextinstr_agree_but_pc; intros. + destruct (PregEq.eq r x); try update_x_access_x; try update_x_access_r. + * eapply ptrofs_nextinstr_agree; eauto. Qed. -Ltac inv_ok_eq := - repeat match goal with - | [EQ: OK ?x = OK ?y |- _ ] - => inversion EQ; clear EQ; subst - end. - -Ltac reg_rwrt := - match goal with - | [e: DR _ = DR _ |- _ ] - => rewrite e in * - end. - -Ltac destruct_reg_inv := - repeat match goal with - | [ H : match ?reg with _ => _ end = _ |- _ ] - => simpl in *; destruct reg; try congruence; try inv_ok_eq; try reg_rwrt - end. - -Ltac destruct_reg_size := - simpl in *; - repeat match goal with - | [ |- context [ match ?reg with _ => _ end = _ ] ] - => destruct reg; try congruence - end. - -Ltac find_rwrt_ag := - simpl in *; - match goal with - | [ AG: forall r, r <> ?PC -> _ r = _ r |- _ ] - => repeat rewrite <- AG; try congruence - end. - -Ltac inv_matchi := - match goal with - | [ MATCHI : match_internal _ _ _ |- _ ] - => inversion MATCHI; subst; find_rwrt_ag - end. - -Ltac destruct_ir0_reg := - match goal with - | [ |- context [ ir0 _ _ ?r ] ] - => unfold ir0 in *; destruct r; find_rwrt_ag; eauto - end. - - Lemma match_internal_nextinstr_switch: forall n s rs2 m2 r v, r <> PC -> @@ -1099,12 +1112,9 @@ Lemma match_internal_nextinstr_switch: Proof. unfold Asm.nextinstr; intros n s rs2 m2 r v NOTPC1 MI. inversion MI; subst; constructor; auto. - - intros r' NOTPC2; - rewrite Pregmap.gso; try congruence. + - eapply nextinstr_agree_but_pc; intros. rewrite AG; try congruence. - destruct (PregEq.eq r r'). - + subst. rewrite !Pregmap.gss; try congruence. - + rewrite !Pregmap.gso; try congruence. + destruct (PregEq.eq r r0); try update_x_access_x; try update_x_access_r. - rewrite !Pregmap.gss, !Pregmap.gso; try congruence. rewrite AGPC. rewrite Pregmap.gso, Pregmap.gss; try congruence. @@ -1148,7 +1158,7 @@ Proof. try (destruct_reg_inv); try (inv_matchi); try (exploit next_inst_preserved; eauto); - try (destruct_reg_size). + try (repeat destruct_reg_size). + (* PArithPPP *) destruct i; try (monadInv TRANSBI); @@ -1178,34 +1188,60 @@ Proof. try (destruct_reg_size); try (destruct_ir0_reg). + (* PArithComparisonPP *) - destruct i. - { + destruct i; try (monadInv TRANSBI); try (inv_matchi); - try (destruct_reg_inv). - simpl in *. - inversion BASIC; clear BASIC; subst. - eexists; eexists; split; eauto. - unfold compare_long. - repeat (eapply match_internal_nextinstr_set_parallel; [ congruence | idtac | try (rewrite !AG; congruence)]). - econstructor; eauto. - * intros. unfold Asm.nextinstr. - rewrite Pregmap.gso; eauto. - * unfold Asm.nextinstr. rewrite Pregmap.gss. - rewrite <- Ptrofs.unsigned_one. rewrite <- (Ptrofs.unsigned_repr n); eauto. - rewrite <- Ptrofs.add_unsigned. rewrite <- Val.offset_ptr_assoc. rewrite AGPC; eauto. - } - - - + try (destruct_reg_inv); + simpl in *; + inversion BASIC; clear BASIC; subst; + eexists; eexists; split; eauto; unfold compare_long, compare_int, compare_float, compare_single; - repeat (eapply match_internal_nextinstr_set_parallel; [ congruence | idtac | try (rewrite !AG; congruence)]). - + try (destruct_reg_size); + try (destruct_reg_size); + try (destruct_reg_size); + repeat (eapply match_internal_nextinstr_set_parallel; [ congruence | idtac | try (rewrite !AG; congruence)]); + try (econstructor; eauto); + try (eapply nextinstr_agree_but_pc; eauto); + try (eapply ptrofs_nextinstr_agree; eauto). + (* TODO find a solution to avoid destructing a lot of subcases *) + (** destruct sz.*) + (*{ [> Vsingle <]*) + (*try (exploit next_inst_preserved; eauto). intros.*) + (*destruct (rs1 x).*) + (*unfold Asm.nextinstr.*) + (*inversion MATCHI.*) + (*}*) all:admit. + (* PArithComparisonR0R *) - all:admit. + destruct i; + try (monadInv TRANSBI); + try (inv_matchi); + try (destruct_reg_inv); + try (destruct_reg_size); + simpl in *; + inversion BASIC; clear BASIC; subst; + eexists; eexists; split; eauto; + unfold compare_long, compare_int, compare_float, compare_single; + repeat (eapply match_internal_nextinstr_set_parallel; [ congruence | idtac | try (rewrite !AG; congruence)]); + try (econstructor; eauto); + try (destruct_ir0_reg); + try (eapply nextinstr_agree_but_pc; eauto); + try (eapply ptrofs_nextinstr_agree; eauto). + (* PArithComparisonP *) - all:admit. + destruct i; + try (monadInv TRANSBI); + try (inv_matchi); + try (destruct_reg_inv); + try (destruct_reg_size); + simpl in *; + inversion BASIC; clear BASIC; subst; + eexists; eexists; split; eauto; + unfold compare_long, compare_int, compare_float, compare_single; + try (destruct_reg_size); + repeat (eapply match_internal_nextinstr_set_parallel; [ congruence | idtac | try (rewrite !AG; congruence)]); + try (econstructor; eauto); + try (eapply nextinstr_agree_but_pc; eauto); + try (eapply ptrofs_nextinstr_agree; eauto). + (* Pcset *) try (monadInv TRANSBI); try (inv_matchi); @@ -1235,18 +1271,27 @@ Proof. try (exploit next_inst_preserved; eauto); try (find_rwrt_ag). - (* PLoad *) - destruct ld; monadInv TRANSBI; destruct rd as [[r|]|]; try congruence; inversion EQ; subst; exploit load_preserved; eauto; + destruct ld; monadInv TRANSBI; try destruct_ireg_inv; exploit load_preserved; eauto; intros; simpl in *; destruct sz; eauto. - (* PStore *) - destruct st; monadInv TRANSBI; destruct r as [[r|]|]; try congruence; inversion EQ; subst; exploit store_preserved; eauto; simpl in *; inv_matchi; find_rwrt_ag. + destruct st; monadInv TRANSBI; try destruct_ireg_inv; exploit store_preserved; eauto; + simpl in *; inv_matchi; find_rwrt_ag. - (* Pallocframe *) monadInv TRANSBI. simpl in *. - inversion MATCHI; subst. - destruct Mem.alloc. - inversion BASIC. repeat (econstructor; eauto). - unfold Asm.nextinstr. rewrite <- AG. - destruct (Mem.store _ _ _ _ _); try congruence; eauto. + inversion MATCHI; subst; + destruct Mem.alloc; + destruct Mem.store in BASIC; + inversion BASIC; subst; clear BASIC. + destruct Mem.store. + (* TODO find a way to complete this proof *) + + eexists; eexists; split; eauto. + repeat (eapply match_internal_nextinstr_set_parallel; [ try congruence | idtac | try reflexivity ]). + destruct (PregEq.eq SP PC); try (repeat congruence); discriminate. + -- admit. + -- eapply AG; destruct (PregEq.eq SP PC); try (repeat congruence); discriminate. + + repeat (econstructor; eauto). + admit. (* TODO *) all:admit. @@ -1257,7 +1302,6 @@ Proof. try (monadInv TRANSBI); try (inv_matchi); try (exploit next_inst_preserved; eauto); - simpl in *; rewrite symbol_addresses_preserved; eauto. - (* Pcvtsw2x *) try (monadInv TRANSBI); -- cgit