From 241fdcc4461c4069ef09e147ff9dfe8687408fac Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 10 Nov 2020 11:42:51 +0100 Subject: Simplifications using ltacs and XZR special case --- aarch64/Asmblockdeps.v | 183 ++++++++++++++++++++++++++++++++++++++++--------- 1 file changed, 150 insertions(+), 33 deletions(-) (limited to 'aarch64/Asmblockdeps.v') diff --git a/aarch64/Asmblockdeps.v b/aarch64/Asmblockdeps.v index 571e511f..ae4e12b2 100644 --- a/aarch64/Asmblockdeps.v +++ b/aarch64/Asmblockdeps.v @@ -75,7 +75,15 @@ Inductive control_op := . Inductive arith_op := + | OArithP (n: arith_p) + | OArithPP (n: arith_pp) | OArithPPP (n: arith_ppp) + | OArithRR0R (n: arith_rr0r) + | OArithRR0R_XZR (n: arith_rr0r) (vz: val) + | OArithRR0 (n: arith_rr0) + | OArithRR0_XZR (n: arith_rr0) (vz: val) + | OArithARRRR0 (n: arith_arrrr0) + | OArithARRRR0_XZR (n: arith_arrrr0) (vz: val) . Inductive op_wrap := @@ -88,7 +96,15 @@ Definition op:=op_wrap. Definition arith_op_eval (op: arith_op) (l: list value) := match op, l with + | OArithP n, [] => Some (Val (arith_eval_p Ge.(_lk) n)) + | OArithPP n, [Val v] => Some (Val (arith_eval_pp Ge.(_lk) n v)) | OArithPPP n, [Val v1; Val v2] => Some (Val (arith_eval_ppp n v1 v2)) + | OArithRR0R n, [Val v1; Val v2] => Some (Val (arith_eval_rr0r n v1 v2)) + | OArithRR0R_XZR n vz, [Val v] => Some (Val (arith_eval_rr0r n vz v)) + | OArithRR0 n, [Val v] => Some (Val (arith_eval_rr0 n v)) + | OArithRR0_XZR n vz, [] => Some (Val (arith_eval_rr0 n vz)) + | OArithARRRR0 n, [Val v1; Val v2; Val v3] => Some (Val (arith_eval_arrrr0 n v1 v2 v3)) + | OArithARRRR0_XZR n vz, [Val v1; Val v2] => Some (Val (arith_eval_arrrr0 n v1 v2 vz)) | _, _ => None end. @@ -119,8 +135,24 @@ Definition op_eval (op: op) (l:list value) := Definition arith_op_eq (o1 o2: arith_op): ?? bool := match o1 with + | OArithP n1 => + match o2 with OArithP n2 => phys_eq n1 n2 | _ => RET false end + | OArithPP n1 => + match o2 with OArithPP n2 => phys_eq n1 n2 | _ => RET false end | OArithPPP n1 => - match o2 with OArithPPP n2 => struct_eq n1 n2 (*| _ => RET false*) end + match o2 with OArithPPP n2 => phys_eq n1 n2 | _ => RET false end + | OArithRR0R n1 => + match o2 with OArithRR0R n2 => phys_eq n1 n2 | _ => RET false end + | OArithRR0R_XZR n1 vz1 => + match o2 with OArithRR0R_XZR n2 vz2 => iandb (phys_eq n1 n2) (phys_eq vz1 vz2) | _ => RET false end + | OArithRR0 n1 => + match o2 with OArithRR0 n2 => phys_eq n1 n2 | _ => RET false end + | OArithRR0_XZR n1 vz1 => + match o2 with OArithRR0_XZR n2 vz2 => iandb (phys_eq n1 n2) (phys_eq vz1 vz2) | _ => RET false end + | OArithARRRR0 n1 => + match o2 with OArithARRRR0 n2 => phys_eq n1 n2 | _ => RET false end + | OArithARRRR0_XZR n1 vz1 => + match o2 with OArithARRRR0_XZR n2 vz2 => iandb (phys_eq n1 n2) (phys_eq vz1 vz2) | _ => RET false end (*| OArithRR n1 => *) (*match o2 with OArithRR n2 => phys_eq n1 n2 | _ => RET false end*) (*| OArithRI32 n1 i1 =>*) @@ -274,6 +306,13 @@ Definition ppos (r: preg) : R.t := end . +(*Definition ppos_ireg0 (r: ireg0) : R.t :=*) + (*match r with*) + (*| RR0 p => ppos p*) + (*| XZR => 71*) + (*end*) +(*.*) + Notation "# r" := (ppos r) (at level 100, right associativity). Lemma not_eq_add: @@ -369,7 +408,36 @@ Definition trans_exit (ex: option control) : L.inst := Definition trans_arith (ai: ar_instruction) : inst := match ai with + | PArithP n rd => [(#rd, Op(Arith (OArithP n)) Enil)] + | PArithPP n rd r1 => [(#rd, Op(Arith (OArithPP n)) (PReg(#r1) @ Enil))] | PArithPPP n rd r1 r2 => [(#rd, Op(Arith (OArithPPP n)) (PReg(#r1) @ PReg(#r2) @ Enil))] + | PArithRR0R n rd r1 r2 => let lr := match r1 with + | RR0 r1' => Op(Arith (OArithRR0R n)) (PReg(#r1') @ PReg(#r2) @ Enil) + | XZR => let vz := match arith_rr0r_isize n with + | W => Vint Int.zero + | X => Vlong Int64.zero + end in + Op(Arith (OArithRR0R_XZR n vz)) (PReg(#r2) @ Enil) + end in + [(#rd, lr)] + | PArithRR0 n rd r1 => let lr := match r1 with + | RR0 r1' => Op(Arith (OArithRR0 n)) (PReg(#r1') @ Enil) + | XZR => let vz := match arith_rr0_isize n with + | W => Vint Int.zero + | X => Vlong Int64.zero + end in + Op(Arith (OArithRR0_XZR n vz)) (Enil) + end in + [(#rd, lr)] + | PArithARRRR0 n rd r1 r2 r3 => let lr := match r3 with + | RR0 r3' => Op(Arith (OArithARRRR0 n)) (PReg(#r1) @ PReg (#r2) @ PReg(#r3') @ Enil) + | XZR => let vz := match arith_arrrr0_isize n with + | W => Vint Int.zero + | X => Vlong Int64.zero + end in + Op(Arith (OArithARRRR0_XZR n vz)) (PReg(#r1) @ PReg(#r2) @ Enil) + end in + [(#rd, lr)] | _ => [] (*| PArithR n d => [(#d, Op (Arith (OArithR n)) Enil)]*) (*| PArithRR n d s => [(#d, Op (Arith (OArithRR n)) (PReg(#s) @ Enil))]*) @@ -587,25 +655,72 @@ Qed. (*Import PChk.*) -Ltac Simplif := - (*((rewrite nextblock_inv by eauto with asmgen)*) - (*|| (rewrite nextblock_inv1 by eauto with asmgen)*) - ((rewrite Pregmap.gss) - (*|| (rewrite nextblock_pc)*) - || (rewrite Pregmap.gso by eauto with asmgen) - || (rewrite assign_diff by (auto; try discriminate; try (apply ppos_discr; try discriminate; congruence); try (apply ppos_pmem_discr); - try (apply not_eq_sym; apply ppos_discr; try discriminate; congruence); try (apply not_eq_sym; apply ppos_pmem_discr); auto)) - || (rewrite assign_eq) - ); auto with asmgen. +(*Ltac Simplif :=*) + (*[>((rewrite nextblock_inv by eauto with asmgen)<]*) + (*[>|| (rewrite nextblock_inv1 by eauto with asmgen)<]*) + (*((rewrite Pregmap.gss)*) + (*[>|| (rewrite nextblock_pc)<]*) + (*|| (rewrite Pregmap.gso by eauto with asmgen)*) + (*|| (rewrite assign_diff by (auto; try discriminate; try (apply ppos_discr; try discriminate; congruence); try (apply ppos_pmem_discr); *) + (*try (apply not_eq_sym; apply ppos_discr; try discriminate; congruence); try (apply not_eq_sym; apply ppos_pmem_discr); auto))*) + (*|| (rewrite assign_eq)*) + (*); auto with asmgen.*) + +(*Ltac Simpl := repeat Simplif.*) + +Ltac sr_val_rwrt := + repeat match goal with + | [H: forall r: preg, ?sr (# r) = Val (?rsr r) |- _ ] + => rewrite H + end. + +Ltac sr_memstate_rwrt := + repeat match goal with + | [H: ?sr pmem = Memstate ?mr |- _ ] + => rewrite <- H + end. + +Ltac replace_ppos := + try erewrite !ireg_pos_ppos; + try erewrite !freg_pos_ppos. + +Ltac DI0N0 ir0 := destruct ir0 as [rr0DIRN0|]; subst; simpl. + +Ltac DIRN1 ir := destruct ir as [irrDIRN1|]; subst; try destruct irrDIRN1; simpl. + +Ltac DDRN2 dr := destruct dr as [irDDRN2|frDDRN2]; subst; try destruct irDDRN2; simpl. + +Ltac DPRF pr := + destruct pr as [drDPRF|crDPRF|]; + [destruct drDPRF as [irDPRF|frDPRF]; [destruct irDPRF as [irrDPRF|]; [destruct irrDPRF|] + | destruct frDPRF] + | destruct crDPRF|]. + +Ltac DPRI pr := + destruct pr as [drDPRI|crDPRI|]; + [destruct drDPRI as [irDPRI|frDPRI]; [destruct irDPRI as [irrDPRI|]; [destruct irrDPRI|]|] + | idtac + | idtac ]. + +Ltac TARITH := + replace_ppos; + try replace (7) with (ppos XSP) by eauto; + try sr_val_rwrt; + try (eexists; split; [| split]); eauto; + try (sr_memstate_rwrt; rewrite assign_diff; + try reflexivity; try apply ireg_not_pmem; + try apply freg_not_pmem). -Ltac Simpl := repeat Simplif. +Ltac SRVUPDATE := + try eapply sr_ireg_update_both; eauto; + try eapply sr_freg_update_both; eauto; + try eapply sr_xsp_update_both; eauto. (*Arguments Pos.add: simpl never.*) (*Arguments ppos: simpl never.*) Variable Ge: genv. -(*Lemma trans_arith_par_correct o rs m m' old:*) Lemma trans_arith_correct rsr mr sr rsw' old i: (*Ge = Genv ge fn ->*) (*match_states (State rs m) m' ->*) @@ -619,26 +734,28 @@ Lemma trans_arith_correct rsr mr sr rsw' old i: /\ match_states (State rsw' mr) sw. Proof. induction i. - 3: { intros MS EARITH. subst. inv MS. - unfold exec_arith_instr. - (*eexists; split; [| split]. *) - - simpl. destruct r1 eqn:EQR1; subst; try destruct i0; simpl; - destruct r2 eqn:EQR2; subst; try destruct i0; simpl; - (*destruct (sr 8).*) destruct rd eqn:EQRD; subst; try destruct i0; simpl; - try erewrite !ireg_pos_ppos; - try erewrite !freg_pos_ppos; - try replace (7) with (ppos XSP) by eauto; - try rewrite !H0; - try (eexists; split; [| split]); eauto; - try (rewrite <- H; rewrite assign_diff; - try reflexivity; try apply ireg_not_pmem; - try apply freg_not_pmem). - all: intros rr; destruct rr as [dr|cr|]; try destruct dr as [ir|fr]; try destruct ir as [irr|]; - try destruct irr; try destruct fr; - try eapply sr_ireg_update_both; eauto; - try eapply sr_freg_update_both; eauto; - try eapply sr_xsp_update_both; eauto. - } + all: intros MS EARITH; subst; inv MS; unfold exec_arith_instr. + - (* PArithP *) + DDRN2 rd; TARITH; intros rr; DPRF rr; SRVUPDATE. + - (* PArithPP *) + DIRN1 rs; DIRN1 rd; TARITH; + intros rr; DPRI rr; SRVUPDATE. + - (* PArithPPP *) + DIRN1 r1; DIRN1 r2; DIRN1 rd; TARITH; + intros rr; DPRI rr; SRVUPDATE. + - (* PArithRR0R *) + simpl. destruct r1. + + (* OArithRR0R *) simpl; TARITH; intros rr; DPRI rr; SRVUPDATE. + + (* OArithRR0R_XZR *) simpl; destruct (arith_rr0r_isize _); TARITH; intros rr; DPRI rr; SRVUPDATE. + - (* PArithRR0 *) + simpl. destruct r1. + + (* OArithRR0 *) simpl; TARITH; intros rr; DPRI rr; SRVUPDATE. + + (* OArithRR0_XZR *) simpl; destruct (arith_rr0_isize _); TARITH; intros rr; DPRI rr; SRVUPDATE. + - (* PArithARRRR0 *) + simpl. destruct r3. + + (* OArithARRRR0 *) simpl; TARITH; intros rr; DPRI rr; SRVUPDATE. + + (* OArithARRRR0_XZR *) simpl; destruct (arith_arrrr0_isize _); TARITH; intros rr; DPRI rr; SRVUPDATE. + - (* PArithComparisonPP *) all:admit. (* -- cgit