From 199817b69389aa095fe23821af9618ff714cfd73 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Sat, 28 Nov 2020 11:52:21 +0100 Subject: Optimizing Asmblockdeps proof Proof is now two times faster (from 60 to 30 seconds) --- aarch64/Asmblockdeps.v | 150 ++++++++++++++++++++++++++++++------------------- 1 file changed, 92 insertions(+), 58 deletions(-) (limited to 'aarch64/Asmblockdeps.v') diff --git a/aarch64/Asmblockdeps.v b/aarch64/Asmblockdeps.v index a913313b..71b7c317 100644 --- a/aarch64/Asmblockdeps.v +++ b/aarch64/Asmblockdeps.v @@ -1224,18 +1224,6 @@ Proof. intros. congruence. Qed. -(* Lemma sr_ireg_pos_ppos: forall (sr: state) r, - sr (ireg_to_pos r) = sr (# r). -Proof. - intros. simpl. reflexivity. -Qed. - -Lemma sr_freg_pos_ppos: forall (sr: state) r, - sr (freg_to_pos r) = sr (# r). -Proof. - intros. simpl. reflexivity. -Qed. *) - Lemma ireg_pos_ppos: forall r, ireg_to_pos r = # r. Proof. @@ -1314,6 +1302,49 @@ Proof. intros; destruct r; discriminate. Qed. +Ltac DPRM pr := + destruct pr as [drDPRF|crDPRF|]; + [destruct drDPRF as [irDPRF|frDPRF]; [destruct irDPRF |] + | destruct crDPRF|]. + +Ltac DPRF pr := + destruct pr as [drDPRF|crDPRF|]; + [destruct drDPRF as [irDPRF|frDPRF]; [destruct irDPRF as [irrDPRF|]; [destruct irrDPRF|] + | destruct frDPRF] + | destruct crDPRF|]. + +Lemma preg_not_pmem: forall r, + pmem <> # r. +Proof. + intros. DPRF r; simpl; discriminate. +Qed. + +Ltac DIRN1 ir := destruct ir as [irrDIRN1|]; subst; try destruct irrDIRN1; simpl. + +Lemma dreg_not_CN: forall (r: dreg), + 2 <> (#r). +Proof. + intros; DIRN1 r; [ apply ireg_not_CN | discriminate | apply freg_not_CN]. +Qed. + +Lemma dreg_not_CZ: forall (r: dreg), + 3 <> (#r). +Proof. + intros; DIRN1 r; [ apply ireg_not_CZ | discriminate | apply freg_not_CZ]. +Qed. + +Lemma dreg_not_CC: forall (r: dreg), + 4 <> (#r). +Proof. + intros; DIRN1 r; [ apply ireg_not_CC | discriminate | apply freg_not_CC]. +Qed. + +Lemma dreg_not_CV: forall (r: dreg), + 5 <> (#r). +Proof. + intros; DIRN1 r; [ apply ireg_not_CV | discriminate | apply freg_not_CV]. +Qed. + Lemma sr_update_both: forall sr rsr r1 rr v (HEQV: forall r : preg, sr (# r) = Val (rsr r)), (sr <[ (#r1) <- Val (v) ]>) (#rr) = @@ -1358,8 +1389,6 @@ Ltac replace_ppos := try replace (7) with (#XSP) by eauto; try replace (24) with (#X16) by auto. -Ltac DIRN1 ir := destruct ir as [irrDIRN1|]; subst; try destruct irrDIRN1; simpl. - Ltac DDRM dr := destruct dr as [irsDDRF|frDDRF]; [destruct irsDDRF @@ -1370,17 +1399,6 @@ Ltac DDRM dr := [destruct irsDDRF as [irsDDRF|]; [destruct irsDDRF|] | destruct frDDRF]. *) -Ltac DPRF pr := - destruct pr as [drDPRF|crDPRF|]; - [destruct drDPRF as [irDPRF|frDPRF]; [destruct irDPRF as [irrDPRF|]; [destruct irrDPRF|] - | destruct frDPRF] - | destruct crDPRF|]. - -Ltac DPRM pr := - destruct pr as [drDPRF|crDPRF|]; - [destruct drDPRF as [irDPRF|frDPRF]; [destruct irDPRF |] - | destruct crDPRF|]. - (* Ltac DPRI pr := destruct pr as [drDPRI|crDPRI|]; [destruct drDPRI as [irDPRI|frDPRI]; [destruct irDPRI as [irrDPRI|]; [destruct irrDPRI|]|] @@ -1399,6 +1417,10 @@ Ltac discriminate_ppos := try apply freg_not_CZ; try apply freg_not_CC; try apply freg_not_CV; + try apply dreg_not_CN; + try apply dreg_not_CZ; + try apply dreg_not_CC; + try apply dreg_not_CV; try(simpl; discriminate). Ltac replace_pc := try replace (6) with (#PC) by eauto. @@ -1581,10 +1603,11 @@ Proof. + (* OArithARRRR0 *) simpl; Simpl sr. + (* OArithARRRR0_XZR *) simpl; destruct (arith_arrrr0_isize _); Simpl sr. - (* PArithComparisonPP *) - DIRN1 r2; DIRN1 r1; destruct i; - repeat Simpl_rep sr; Simpl_exists sr; - unfold arith_eval_comparison_pp; destruct arith_prepare_comparison_pp; - simpl; intros rr; try destruct sz; + simpl; destruct i; + unfold arith_eval_comparison_pp, arith_prepare_comparison_pp; simpl; + fold (ppos r2); fold(ppos r1); try rewrite !H0; repeat Simpl_rep sr; + Simpl sr; + try destruct sz; try (eapply compare_single_res; eauto); try (eapply compare_long_res; eauto); try (eapply compare_float_res; eauto). @@ -1597,13 +1620,14 @@ Proof. try (eapply compare_long_res; eauto); try (eapply compare_int_res; eauto)). - (* PArithComparisonP *) - DIRN1 r1; destruct i; - repeat Simpl_rep sr; Simpl_exists sr; - unfold arith_eval_comparison_p; destruct arith_prepare_comparison_p; - simpl; try intros rr; try destruct sz; + simpl; destruct i; + unfold arith_eval_comparison_p, arith_prepare_comparison_p; simpl; + fold(ppos r1); try rewrite !H0; repeat Simpl_rep sr; + Simpl sr; + try destruct sz; + try (eapply compare_int_res; eauto); try (eapply compare_single_res; eauto); try (eapply compare_long_res; eauto); - try (eapply compare_int_res; eauto); try (eapply compare_float_res; eauto). - (* Pcset *) simpl; unfold eval_testcond, get_testcond_rlocs, cflags_eval; @@ -1614,8 +1638,7 @@ Proof. - (* Pfmovi *) simpl; destruct r1; simpl; destruct fsz; Simpl sr. - (* Pcsel *) - simpl. destruct c; simpl; - DIRN1 r1; DIRN1 r2; Simpl_rep sr; DDRM rd; Simpl_exists sr; try intros rr; Simpl_update. + destruct c; simpl; DIRN1 rd; fold (ppos r2); fold (ppos r1); Simpl sr. - (* Pfnmul *) simpl; destruct fsz; Simpl sr. Qed. @@ -1668,7 +1691,8 @@ Local Ltac preg_eq_discr r rd := injection MEMAL2; intros Hm2 Hb2; try rewrite Hm2, Hb2; rewrite Hm, Hb; rewrite MEMS; reflexivity. * eauto. - * intros rr; DPRF rr; repeat Simpl_exists sr. + * intros rr. rewrite assign_diff; try apply preg_not_pmem; try rewrite sp_xsp. + replace 37 with (#X29) by auto; repeat (Simpl_update; intros). + simpl; repeat Simpl_exists sr. erewrite H. destruct (Mem.alloc _ _ _) eqn:HMEMAL2. injection MEMAL; intros Hm Hb. try rewrite Hm, Hb; clear Hm Hb. @@ -1679,7 +1703,10 @@ Local Ltac preg_eq_discr r rd := + destruct (rsr SP) eqn:EQSP; simpl; rewrite <- sp_xsp; rewrite EQSP; rewrite MLOAD; try reflexivity. destruct (Mem.free _ _ _) eqn:EQFREE; try reflexivity. rewrite assign_diff; discriminate_ppos. replace_regs_pos sr; sr_val_rwrt. rewrite <- sp_xsp; rewrite EQSP; rewrite MLOAD. rewrite EQFREE. - Simpl_exists sr. intros rr; DPRF rr; repeat Simpl_exists sr. + replace 24 with (#X16) by auto; rewrite sp_xsp; Simpl sr. + intros rr'; destruct (PregEq.eq XSP rr'). + * rewrite e; rewrite Pregmap.gss, sr_gss; auto. + * rewrite Pregmap.gso, !assign_diff; auto; apply ppos_discr in n; auto. + rewrite <- sp_xsp; rewrite MLOAD; reflexivity. Qed. @@ -1778,27 +1805,34 @@ Proof. replace_pc. rewrite (H0 PC). unfold control_eval. destruct Ge. simpl. unfold incrPC. try (eexists; split; [ | split ]); eauto. - intros rr; DPRF rr; Simpl_update. - 68: rewrite sr_gss, Pregmap.gss; - try rewrite Pregmap.gso; discriminate_ppos; fold (ppos r); rewrite H0; auto. - all: repeat Simpl_rep sr; rewrite !Pregmap.gso; discriminate_ppos; auto. + intros rr; destruct (PregEq.eq PC rr). + + replace_pc; rewrite e; rewrite !Pregmap.gss, !sr_gss; + rewrite Pregmap.gso; fold (ppos r); try rewrite H0; auto. + rewrite <- e; destruct r; discriminate. + + replace_pc; rewrite Pregmap.gso, assign_diff; auto; apply ppos_discr in n; auto; + rewrite Pregmap.gss, sr_gss. destruct (PregEq.eq X30 rr); replace 38 with (#X30) by auto. + * rewrite e; rewrite Pregmap.gss, sr_gss; auto. + * replace_pc; rewrite !Pregmap.gso, !assign_diff; auto; apply ppos_discr in n0; auto; + apply ppos_discr; eauto. - (* Obtbl *) - replace_pc. rewrite (H0 PC). - unfold control_eval. destruct Ge. simpl. unfold incrPC. - destruct r1. - 17: rewrite Pregmap.gss, sr_gss; try reflexivity. - all: rewrite !Pregmap.gso, !assign_diff; discriminate_ppos; - rewrite ireg_pos_ppos; try erewrite H0; destruct (rsr _); - try destruct (list_nth_z _ _); try reflexivity; - unfold goto_label, goto_label_deps; destruct (label_pos _ _ _); - try rewrite 2Pregmap.gso, Pregmap.gss; destruct (Val.offset_ptr (rsr PC) (Ptrofs.repr sz)); - try reflexivity; discriminate_ppos; simpl; Simpl_exists sr; - intros rr; - destruct (PregEq.eq X16 rr); [ subst; Simpl_update |]; - destruct (PregEq.eq X17 rr); [ subst; Simpl_update |]; - destruct (PregEq.eq PC rr); [ subst; Simpl_update |]; - rewrite !Pregmap.gso; auto; apply ppos_discr in n; apply ppos_discr in n0; apply ppos_discr in n1; - simpl in *;repeat Simpl_rep sr; auto. + replace_pc; rewrite (H0 PC); + unfold control_eval; destruct Ge; simpl; unfold incrPC. + destruct (PregEq.eq X16 r1). + + fold (ppos r1); rewrite <- e; rewrite Pregmap.gss, sr_gss; reflexivity. + + rewrite !Pregmap.gso; auto; rewrite ppos_discr in n; + fold (ppos r1); replace 24 with (#X16) by auto; try rewrite !assign_diff; auto; + discriminate_ppos; rewrite H0; destruct (rsr r1) eqn:EQR; + try (try rewrite EQR; reflexivity). + try destruct (list_nth_z _ _); try reflexivity; + unfold goto_label, goto_label_deps; destruct (label_pos _ _ _); + try rewrite 2Pregmap.gso, Pregmap.gss; destruct (Val.offset_ptr (rsr PC) (Ptrofs.repr sz)); + try reflexivity; discriminate_ppos. Simpl sr. + destruct (PregEq.eq X16 rr); [ subst; Simpl_update |]; + destruct (PregEq.eq X17 rr); [ subst; Simpl_update |]; + destruct (PregEq.eq PC rr); [ subst; Simpl_update |]. + rewrite !Pregmap.gso; auto; + apply ppos_discr in n0; apply ppos_discr in n1; apply ppos_discr in n2; + rewrite !assign_diff; auto. Qed. Theorem bisimu_exit ex sz rsr mr sr: -- cgit