From 2ee3bc6fecc3607b368fbf2a034bdfd8ccdf2d3e Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 12 Jul 2017 14:05:06 +0200 Subject: Constprop strength reduction (#17) PowerPC port: add strength reduction for 64-bit operations * Added strength reduction for 64bit compare, subl, addl, mull, andl, orl, xorl, divl, shll, shrl, shrlu, shrluimm, shllimm, mullimm, divlu. (Bug 21748) * Moved shru_rolml proof to Values. --- powerpc/ConstpropOp.vp | 96 +++++++++++++++++++++ powerpc/ConstpropOpproof.v | 206 +++++++++++++++++++++++++++++++++++++++++++++ powerpc/SelectLongproof.v | 18 +--- 3 files changed, 304 insertions(+), 16 deletions(-) (limited to 'powerpc') diff --git a/powerpc/ConstpropOp.vp b/powerpc/ConstpropOp.vp index 886655a0..0ed92e90 100644 --- a/powerpc/ConstpropOp.vp +++ b/powerpc/ConstpropOp.vp @@ -50,6 +50,14 @@ Nondetfunction cond_strength_reduction (Ccompuimm (swap_comparison c) n1, r2 :: nil) | Ccompu c, r1 :: r2 :: nil, v1 :: I n2 :: nil => (Ccompuimm c n2, r1 :: nil) + | Ccompl c, r1 :: r2 :: nil, L n1 :: v2 :: nil => + (Ccomplimm (swap_comparison c) n1, r2 :: nil) + | Ccompl c, r1 :: r2 :: nil, v1 :: L n2 :: nil => + (Ccomplimm c n2, r1 :: nil) + | Ccomplu c, r1 :: r2 :: nil, L n1 :: v2 :: nil => + (Ccompluimm (swap_comparison c) n1, r2 :: nil) + | Ccomplu c, r1 :: r2 :: nil, v1 :: L n2 :: nil => + (Ccompluimm c n2, r1 :: nil) | _, _, _ => (cond, args) end. @@ -147,6 +155,77 @@ Definition make_xorimm (n: int) (r: reg) := else if Int.eq n Int.mone then (Onot, r :: nil) else (Oxorimm n, r :: nil). +Definition make_shllimm (n: int) (r1 r2: reg) := + if Int.eq n Int.zero then (Omove, r1 :: nil) + else if Int.ltu n Int64.iwordsize' then + let n' := Int64.repr (Int.unsigned n) in + (Orolml n (Int64.shl Int64.mone n'), r1::nil) + else (Oshll, r1 :: r2 :: nil). + +Definition make_shrlimm (n: int) (r1 r2: reg) := + if Int.eq n Int.zero then (Omove, r1 :: nil) + else (Oshrl, r1 :: r2 :: nil). + +Definition make_shrluimm_aux (n: int) (r1: reg) := + if Int.eq n Int.zero then + (Omove, r1 :: nil) + else + let n' := Int64.repr (Int.unsigned n) in + (Orolml (Int.sub Int64.iwordsize' n) (Int64.shru Int64.mone n'), r1 :: nil). + +Definition make_shrluimm (n: int) (r1 r2: reg) := + if Int.ltu n Int64.iwordsize' then + make_shrluimm_aux n r1 + else + (Oshrlu, r1 :: r2 :: nil). + +Definition make_addlimm (n: int64) (r: reg) := + if Int64.eq n Int64.zero + then (Omove, r :: nil) + else (Oaddlimm n, r :: nil). + +Definition make_mullimm (n: int64) (r1 r2: reg) := + if Int64.eq n Int64.zero then + (Olongconst Int64.zero, nil) + else if Int64.eq n Int64.one then + (Omove, r1 :: nil) + else + match Int64.is_power2' n with + | Some l => + let l' := Int64.repr (Int.unsigned l) in + (Orolml l (Int64.shl Int64.mone l'), r1 :: nil) + | None => (Omull, r1 :: r2 :: nil) + end. + +Definition make_andlimm (n: int64) (r: reg) (a: aval) := + if Int64.eq n Int64.zero then (Olongconst Int64.zero, nil) + else if Int64.eq n Int64.mone then (Omove, r :: nil) + else (Oandlimm n, r :: nil). + +Definition make_orlimm (n: int64) (r: reg) := + if Int64.eq n Int64.zero then (Omove, r :: nil) + else if Int64.eq n Int64.mone then (Olongconst Int64.mone, nil) + else (Oorlimm n, r :: nil). + +Definition make_xorlimm (n: int64) (r: reg) := + if Int64.eq n Int64.zero then (Omove, r :: nil) + else if Int64.eq n Int64.mone then (Onotl, r :: nil) + else (Oxorlimm n, r :: nil). + +Definition make_divlimm n (r1 r2: reg) := + match Int64.is_power2' n with + | Some l => if Int.ltu l (Int.repr 63) + then (Oshrxlimm l, r1 :: nil) + else (Odivl, r1 :: r2 :: nil) + | None => (Odivl, r1 :: r2 :: nil) + end. + +Definition make_divluimm n (r1 r2: reg) := + match Int64.is_power2' n with + | Some l => make_shrluimm_aux l r1 + | None => (Odivlu, r1 :: r2 :: nil) + end. + Definition make_mulfimm (n: float) (r r1 r2: reg) := if Float.eq_dec n (Float.of_int (Int.repr 2)) then (Oaddf, r :: r :: nil) @@ -187,6 +266,23 @@ Nondetfunction op_strength_reduction | Oshl, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shlimm n2 r1 r2 | Oshr, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shrimm n2 r1 r2 | Oshru, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shruimm n2 r1 r2 + | Oaddl, r1 :: r2 :: nil, L n1 :: v2 :: nil => make_addlimm n1 r2 + | Oaddl, r1 :: r2 :: nil, v1 :: L n2 :: nil => make_addlimm n2 r1 + | Osubl, r1 :: r2 :: nil, v1 :: L n2 :: nil => make_addlimm (Int64.neg n2) r1 + | Omull, r1 :: r2 :: nil, L n1 :: v2 :: nil => make_mullimm n1 r2 r1 + | Omull, r1 :: r2 :: nil, v1 :: L n2 :: nil => make_mullimm n2 r1 r2 + | Odivl, r1 :: r2 :: nil, v1 :: L n2 :: nil => make_divlimm n2 r1 r2 + | Odivlu, r1 :: r2 :: nil, v1 :: L n2 :: nil => make_divluimm n2 r1 r2 + | Oandl, r1 :: r2 :: nil, L n1 :: v2 :: nil => make_andlimm n1 r2 v2 + | Oandl, r1 :: r2 :: nil, v1 :: L n2 :: nil => make_andlimm n2 r1 v1 + | Oandlimm n, r1 :: nil, v1 :: nil => make_andlimm n r1 v1 + | Oorl, r1 :: r2 :: nil, L n1 :: v2 :: nil => make_orlimm n1 r2 + | Oorl, r1 :: r2 :: nil, v1 :: L n2 :: nil => make_orlimm n2 r1 + | Oxorl, r1 :: r2 :: nil, L n1 :: v2 :: nil => make_xorlimm n1 r2 + | Oxorl, r1 :: r2 :: nil, v1 :: L n2 :: nil => make_xorlimm n2 r1 + | Oshll, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shllimm n2 r1 r2 + | Oshrl, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shrlimm n2 r1 r2 + | Oshrlu, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shrluimm n2 r1 r2 | Ocmp c, args, vl => make_cmp c args vl | Omulf, r1 :: r2 :: nil, v1 :: F n2 :: nil => make_mulfimm n2 r1 r1 r2 | Omulf, r1 :: r2 :: nil, F n1 :: v2 :: nil => make_mulfimm n1 r2 r1 r2 diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v index dd39dc10..e9d091ca 100644 --- a/powerpc/ConstpropOpproof.v +++ b/powerpc/ConstpropOpproof.v @@ -68,6 +68,10 @@ Ltac SimplVM := let E := fresh in assert (E: v = Vint n) by (inversion H; auto); rewrite E in *; clear H; SimplVM + | [ H: vmatch _ ?v (L ?n) |- _ ] => + let E := fresh in + assert (E: v = Vlong n) by (inversion H; auto); + rewrite E in *; clear H; SimplVM | [ H: vmatch _ ?v (F ?n) |- _ ] => let E := fresh in assert (E: v = Vfloat n) by (inversion H; auto); @@ -121,6 +125,10 @@ Proof. - auto. - apply Val.swap_cmpu_bool. - auto. +- apply Val.swap_cmpl_bool. +- auto. +- apply Val.swap_cmplu_bool. +- auto. - auto. Qed. @@ -337,6 +345,149 @@ Proof. econstructor; split; eauto. auto. Qed. +Lemma make_addlimm_correct: + forall n r, + let (op, args) := make_addlimm n r in + exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.addl rs#r (Vlong n)) v. +Proof. + intros. unfold make_addlimm. + predSpec Int64.eq Int64.eq_spec n Int64.zero; intros. + subst. exists (rs#r); split; auto. + destruct (rs#r); simpl; auto. rewrite Int64.add_zero. auto. + exists (Val.addl rs#r (Vlong n)); split; auto. +Qed. + +Lemma make_mullimm_correct: + forall n r1 r2, + rs#r2 = Vlong n -> + let (op, args) := make_mullimm n r1 r2 in + exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.mull rs#r1 (Vlong n)) v. +Proof. + intros; unfold make_mullimm. + predSpec Int64.eq Int64.eq_spec n Int64.zero; intros. subst. + exists (Vlong Int64.zero); split; auto. destruct (rs#r1); simpl; auto. rewrite Int64.mul_zero; auto. + predSpec Int64.eq Int64.eq_spec n Int64.one; intros. subst. + exists (rs#r1); split; auto. destruct (rs#r1); simpl; auto. rewrite Int64.mul_one; auto. + destruct (Int64.is_power2' n) eqn:?; intros. + assert (Int.ltu i Int64.iwordsize' = true) by (erewrite Int64.is_power2'_range; eauto). + exists (Val.shll rs#r1 (Vint i)); split; auto. + rewrite Val.shll_rolml by apply H2. auto. + destruct (rs#r1); auto. simpl. rewrite H2. + erewrite Int64.mul_pow2'; auto. + econstructor ; split; auto. simpl. congruence. +Qed. + +Lemma make_shllimm_correct: + forall n r1 r2, + rs#r2 = Vint n -> + let (op, args) := make_shllimm n r1 r2 in + exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.shll rs#r1 (Vint n)) v. +Proof. + intros; unfold make_shllimm. + predSpec Int.eq Int.eq_spec n Int.zero; intros. subst. + exists (rs#r1); split; auto. destruct (rs#r1); simpl; auto. + unfold Int64.shl'. rewrite Z.shiftl_0_r, Int64.repr_unsigned. auto. + destruct (Int.ltu n Int64.iwordsize') eqn:LT; simpl. + rewrite Val.shll_rolml by apply LT. eauto. + econstructor; split. simpl. eauto. rewrite H; auto. +Qed. + +Lemma make_shrlimm_correct: + forall n r1 r2, + rs#r2 = Vint n -> + let (op, args) := make_shrlimm n r1 r2 in + exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.shrl rs#r1 (Vint n)) v. +Proof. + intros; unfold make_shrlimm. + predSpec Int.eq Int.eq_spec n Int.zero; intros. subst. + exists (rs#r1); split; auto. destruct (rs#r1); simpl; auto. + unfold Int64.shr'. rewrite Z.shiftr_0_r, Int64.repr_signed. auto. + econstructor; split. simpl. eauto. rewrite H; auto. +Qed. + +Lemma make_shrluimm_aux_correct: + forall n r1, + Int.ltu n Int64.iwordsize' = true -> + let (op, args) := make_shrluimm_aux n r1 in + exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.shrlu rs#r1 (Vint n)) v. +Proof. + intros; unfold make_shrluimm_aux. + predSpec Int.eq Int.eq_spec n Int.zero; intros. subst. + - exists (rs#r1); split; auto. destruct (rs#r1); simpl; auto. + unfold Int64.shru'. rewrite Z.shiftr_0_r, Int64.repr_unsigned. auto. + - rewrite Val.shrlu_rolml by apply H; auto. econstructor; split; eauto. auto. +Qed. + +Lemma make_shrluimm_correct: + forall n r1 r2, + rs#r2 = Vint n -> + let (op, args) := make_shrluimm n r1 r2 in + exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.shrlu rs#r1 (Vint n)) v. +Proof. + intros; unfold make_shrluimm. + destruct (Int.ltu n Int64.iwordsize') eqn:LT; simpl. + apply make_shrluimm_aux_correct; auto. + rewrite H. eauto. +Qed. + +Lemma make_andlimm_correct: + forall n r x, + let (op, args) := make_andlimm n r x in + exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.andl rs#r (Vlong n)) v. +Proof. + intros; unfold make_andlimm. + predSpec Int64.eq Int64.eq_spec n Int64.zero; intros. + subst n. exists (Vlong Int64.zero); split; auto. destruct (rs#r); simpl; auto. rewrite Int64.and_zero; auto. + predSpec Int64.eq Int64.eq_spec n Int64.mone; intros. + subst n. exists (rs#r); split; auto. destruct (rs#r); simpl; auto. rewrite Int64.and_mone; auto. + econstructor; split; eauto. auto. +Qed. + +Lemma make_orlimm_correct: + forall n r, + let (op, args) := make_orlimm n r in + exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.orl rs#r (Vlong n)) v. +Proof. + intros; unfold make_orlimm. + predSpec Int64.eq Int64.eq_spec n Int64.zero; intros. + subst n. exists (rs#r); split; auto. destruct (rs#r); simpl; auto. rewrite Int64.or_zero; auto. + predSpec Int64.eq Int64.eq_spec n Int64.mone; intros. + subst n. exists (Vlong Int64.mone); split; auto. destruct (rs#r); simpl; auto. rewrite Int64.or_mone; auto. + econstructor; split; eauto. auto. +Qed. + +Lemma make_xorlimm_correct: + forall n r, + let (op, args) := make_xorlimm n r in + exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.xorl rs#r (Vlong n)) v. +Proof. + intros; unfold make_xorlimm. + predSpec Int64.eq Int64.eq_spec n Int64.zero; intros. + subst n. exists (rs#r); split; auto. destruct (rs#r); simpl; auto. rewrite Int64.xor_zero; auto. + predSpec Int64.eq Int64.eq_spec n Int64.mone; intros. + subst n. exists (Val.notl rs#r); split; auto. + econstructor; split; eauto. auto. +Qed. + +Lemma make_divluimm_correct: + forall n r1 r2 v, + Val.divlu rs#r1 rs#r2 = Some v -> + rs#r2 = Vlong n -> + let (op, args) := make_divluimm n r1 r2 in + exists w, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some w /\ Val.lessdef v w. +Proof. + intros; unfold make_divluimm. + destruct (Int64.is_power2' n) eqn:?. + exploit Int64.is_power2'_range; eauto. intros RANGE. + replace v with (Val.shrlu rs#r1 (Vint i)). + apply make_shrluimm_aux_correct; auto. + rewrite H0 in H. + destruct (rs#r1); simpl in *; inv H. rewrite RANGE. + destruct (Int64.eq n Int64.zero); inv H2. + rewrite (Int64.divu_pow2' i0 n i) by auto. auto. + exists v; auto. +Qed. + Lemma make_mulfimm_correct: forall n r1 r2, rs#r2 = Vfloat n -> @@ -350,6 +501,20 @@ Proof. simpl. econstructor; split; eauto. Qed. +Lemma make_divlimm_correct: + forall n r1 r2 v, + Val.divls rs#r1 rs#r2 = Some v -> + rs#r2 = Vlong n -> + let (op, args) := make_divlimm n r1 r2 in + exists w, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some w /\ Val.lessdef v w. +Proof. + intros; unfold make_divlimm. + destruct (Int64.is_power2' n) eqn:?. destruct (Int.ltu i (Int.repr 63)) eqn:?. + rewrite H0 in H. econstructor; split. simpl; eauto. eapply Val.divls_pow2; eauto. auto. + exists v; auto. + exists v; auto. +Qed. + Lemma make_mulfimm_correct_2: forall n r1 r2, rs#r1 = Vfloat n -> @@ -470,6 +635,47 @@ Proof. InvApproxRegs; SimplVM; inv H0. apply make_shrimm_correct; auto. (* shru *) InvApproxRegs; SimplVM; inv H0. apply make_shruimm_correct; auto. +(* addl *) + InvApproxRegs; SimplVM; inv H0. + change (let (op', args') := make_addlimm n1 r2 in + exists w : val, + eval_operation ge (Vptr sp Ptrofs.zero) op' rs ## args' m = Some w /\ + Val.lessdef (Val.addl (Vlong n1) rs#r2) w). + rewrite Val.addl_commut. apply make_addlimm_correct. + InvApproxRegs; SimplVM; inv H0. apply make_addlimm_correct. +(* subl *) + InvApproxRegs; SimplVM; inv H0. + replace (Val.subl rs#r1 (Vlong n2)) with (Val.addl rs#r1 (Vlong (Int64.neg n2))). + apply make_addlimm_correct; auto. + unfold Val.addl, Val.subl. destruct Archi.ptr64 eqn:SF, rs#r1; auto. + rewrite Int64.sub_add_opp; auto. + rewrite Ptrofs.sub_add_opp. do 2 f_equal. auto with ptrofs. + rewrite Int64.sub_add_opp; auto. +(* mull *) + InvApproxRegs; SimplVM; inv H0. fold (Val.mull (Vlong n1) rs#r2). rewrite Val.mull_commut. apply make_mullimm_correct; auto. + InvApproxRegs; SimplVM; inv H0. apply make_mullimm_correct; auto. +(* divl *) + assert (rs#r2 = Vlong n2). clear H0. InvApproxRegs; SimplVM; auto. + apply make_divlimm_correct; auto. +(* divlu *) + assert (rs#r2 = Vlong n2). clear H0. InvApproxRegs; SimplVM; auto. + apply make_divluimm_correct; auto. +(* andl *) + InvApproxRegs; SimplVM; inv H0. fold (Val.andl (Vlong n1) rs#r2). rewrite Val.andl_commut. apply make_andlimm_correct; auto. + InvApproxRegs; SimplVM; inv H0. apply make_andlimm_correct; auto. + inv H; inv H0. apply make_andlimm_correct; auto. +(* orlimm *) + InvApproxRegs; SimplVM; inv H0. fold (Val.orl (Vlong n1) rs#r2). rewrite Val.orl_commut. apply make_orlimm_correct; auto. + InvApproxRegs; SimplVM; inv H0. apply make_orlimm_correct; auto. +(* xorlimm *) + InvApproxRegs; SimplVM; inv H0. fold (Val.xorl (Vlong n1) rs#r2). rewrite Val.xorl_commut. apply make_xorlimm_correct; auto. + InvApproxRegs; SimplVM; inv H0. apply make_xorlimm_correct; auto. +(* shll *) + InvApproxRegs; SimplVM; inv H0. apply make_shllimm_correct; auto. +(* shrl *) + InvApproxRegs; SimplVM; inv H0. apply make_shrlimm_correct; auto. +(* shrlu *) + InvApproxRegs; SimplVM; inv H0. apply make_shrluimm_correct; auto. (* cmp *) inv H0. apply make_cmp_correct; auto. (* mulf *) diff --git a/powerpc/SelectLongproof.v b/powerpc/SelectLongproof.v index 3e5e82d3..a214d131 100644 --- a/powerpc/SelectLongproof.v +++ b/powerpc/SelectLongproof.v @@ -240,18 +240,12 @@ Theorem eval_shllimm: forall n, unary_constructor_sound (fun e => shllimm e n) ( Proof. intros; unfold shllimm. destruct Archi.splitlong eqn:SL. apply SplitLongproof.eval_shllimm; auto. red; intros. - assert (ROLM: forall n1 v, - Int.ltu n1 Int64.iwordsize' = true -> - Val.shll v (Vint n1) = Val.rolml v n1 (Int64.shl Int64.mone (Int64.repr (Int.unsigned n1)))). - { intros. destruct v; auto. simpl. rewrite H0. rewrite <- Int64.shl_rolm. unfold Int64.shl. - rewrite Int64.int_unsigned_repr. constructor. unfold Int64.ltu. rewrite Int64.int_unsigned_repr. - apply H0. } predSpec Int.eq Int.eq_spec n Int.zero. exists x; split; auto. subst n; destruct x; simpl; auto. destruct (Int.ltu Int.zero Int64.iwordsize'); auto. change (Int64.shl' i Int.zero) with (Int64.shl i Int64.zero). rewrite Int64.shl_zero; auto. destruct (Int.ltu n Int64.iwordsize') eqn:LT; simpl. -- rewrite ROLM by apply LT. apply eval_rolml. auto. +- rewrite Val.shll_rolml by apply LT. apply eval_rolml. auto. - TrivialExists. constructor; eauto. constructor. EvalOp. simpl; eauto. constructor. constructor. Qed. @@ -260,18 +254,10 @@ Theorem eval_shrluimm: forall n, unary_constructor_sound (fun e => shrluimm e n) Proof. unfold shrluimm; destruct Archi.splitlong. apply SplitLongproof.eval_shrluimm. auto. red; intros. - assert (ROLM: forall n1 v, - Int.ltu n1 Int64.iwordsize' = true -> - Val.shrlu v (Vint n1) = Val.rolml v (Int.sub Int64.iwordsize' n1) (Int64.shru Int64.mone (Int64.repr (Int.unsigned n1)))). - { intros. destruct v; auto. simpl. rewrite H0. - rewrite Int64.int_sub_ltu by apply H0. rewrite Int64.repr_unsigned. rewrite <- Int64.shru_rolm. unfold Int64.shru'. unfold Int64.shru. - rewrite Int64.unsigned_repr. reflexivity. apply Int64.int_unsigned_range. - unfold Int64.ltu. rewrite Int64.int_unsigned_repr. auto. - } predSpec Int.eq Int.eq_spec n Int.zero. exists x. split. apply H. destruct x; simpl; auto. rewrite H0. rewrite Int64.shru'_zero. constructor. destruct (Int.ltu n Int64.iwordsize') eqn:LT; simpl. -- rewrite ROLM by apply LT. apply eval_rolml. auto. +- rewrite Val.shrlu_rolml by apply LT. apply eval_rolml. auto. - TrivialExists. constructor; eauto. constructor. EvalOp. simpl; eauto. constructor. constructor. Qed. -- cgit