From 90b76a0842b7f080893dd70a7c0c6bc878f4056b Mon Sep 17 00:00:00 2001 From: Michael Schmidt Date: Tue, 5 Dec 2017 14:48:18 +0100 Subject: Optimization for division by one during constant propagation (#39) Signed and unsigned divisions by literal 1 are already optimized away during the Selection phase. This pull request also optimizes those divisions when the 1 divisor is produced by constant propagation. --- arm/ConstpropOp.vp | 26 ++++++++++++++++---------- arm/ConstpropOpproof.v | 8 ++++++++ powerpc/ConstpropOp.vp | 15 +++++++++------ powerpc/ConstpropOpproof.v | 4 ++++ riscV/ConstpropOp.vp | 26 ++++++++++++++++---------- riscV/ConstpropOpproof.v | 8 ++++++++ x86/ConstpropOp.vp | 26 ++++++++++++++++---------- x86/ConstpropOpproof.v | 8 ++++++++ 8 files changed, 85 insertions(+), 36 deletions(-) diff --git a/arm/ConstpropOp.vp b/arm/ConstpropOp.vp index f94606b0..bd08d597 100644 --- a/arm/ConstpropOp.vp +++ b/arm/ConstpropOp.vp @@ -160,18 +160,24 @@ Definition make_mulimm (n: int) (r1 r2: reg) := end. Definition make_divimm (n: int) (r1 r2: reg) := - match Int.is_power2 n with - | Some l => if Int.ltu l (Int.repr 31) - then (Oshrximm l, r1 :: nil) - else (Odiv, r1 :: r2 :: nil) - | None => (Odiv, r1 :: r2 :: nil) - end. + if Int.eq n Int.one then + (Omove, r1 :: nil) + else + match Int.is_power2 n with + | Some l => if Int.ltu l (Int.repr 31) + then (Oshrximm l, r1 :: nil) + else (Odiv, r1 :: r2 :: nil) + | None => (Odiv, r1 :: r2 :: nil) + end. Definition make_divuimm (n: int) (r1 r2: reg) := - match Int.is_power2 n with - | Some l => (Oshift (Slsr (mk_shift_amount l)), r1 :: nil) - | None => (Odivu, r1 :: r2 :: nil) - end. + if Int.eq n Int.one then + (Omove, r1 :: nil) + else + match Int.is_power2 n with + | Some l => (Oshift (Slsr (mk_shift_amount l)), r1 :: nil) + | None => (Odivu, r1 :: r2 :: nil) + end. Definition make_andimm (n: int) (r: reg) (a: aval) := if Int.eq n Int.zero then (Ointconst Int.zero, nil) diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v index 93ef2475..1eec5923 100644 --- a/arm/ConstpropOpproof.v +++ b/arm/ConstpropOpproof.v @@ -356,6 +356,10 @@ Lemma make_divimm_correct: exists w, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some w /\ Val.lessdef v w. Proof. intros; unfold make_divimm. + predSpec Int.eq Int.eq_spec n Int.one; intros. subst. rewrite H0 in H. + destruct (rs#r1) eqn:?; + try (rewrite Val.divs_one in H; exists (Vint i); split; simpl; try rewrite Heqv0; auto); + inv H; auto. destruct (Int.is_power2 n) eqn:?. destruct (Int.ltu i (Int.repr 31)) eqn:?. exists v; split; auto. simpl. eapply Val.divs_pow2; eauto. congruence. @@ -371,6 +375,10 @@ Lemma make_divuimm_correct: exists w, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some w /\ Val.lessdef v w. Proof. intros; unfold make_divuimm. + predSpec Int.eq Int.eq_spec n Int.one; intros. subst. rewrite H0 in H. + destruct (rs#r1) eqn:?; + try (rewrite Val.divu_one in H; exists (Vint i); split; simpl; try rewrite Heqv0; auto); + inv H; auto. destruct (Int.is_power2 n) eqn:?. replace v with (Val.shru rs#r1 (Vint i)). econstructor; split. simpl. rewrite mk_shift_amount_eq. eauto. diff --git a/powerpc/ConstpropOp.vp b/powerpc/ConstpropOp.vp index 0ed92e90..f18a72e9 100644 --- a/powerpc/ConstpropOp.vp +++ b/powerpc/ConstpropOp.vp @@ -124,12 +124,15 @@ Definition make_mulimm (n: int) (r1 r2: reg) := end. Definition make_divimm (n: int) (r1 r2: reg) := - match Int.is_power2 n with - | Some l => if Int.ltu l (Int.repr 31) - then (Oshrximm l, r1 :: nil) - else (Odiv, r1 :: r2 :: nil) - | None => (Odiv, r1 :: r2 :: nil) - end. + if Int.eq n Int.one then + (Omove, r1 :: nil) + else + match Int.is_power2 n with + | Some l => if Int.ltu l (Int.repr 31) + then (Oshrximm l, r1 :: nil) + else (Odiv, r1 :: r2 :: nil) + | None => (Odiv, r1 :: r2 :: nil) + end. Definition make_divuimm (n: int) (r1 r2: reg) := match Int.is_power2 n with diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v index e9d091ca..7fddd053 100644 --- a/powerpc/ConstpropOpproof.v +++ b/powerpc/ConstpropOpproof.v @@ -267,6 +267,10 @@ Lemma make_divimm_correct: exists w, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some w /\ Val.lessdef v w. Proof. intros; unfold make_divimm. + predSpec Int.eq Int.eq_spec n Int.one; intros. subst. rewrite H0 in H. + destruct (rs#r1) eqn:?; + try (rewrite Val.divs_one in H; exists (Vint i); split; simpl; try rewrite Heqv0; auto); + inv H; auto. destruct (Int.is_power2 n) eqn:?. destruct (Int.ltu i (Int.repr 31)) eqn:?. exists v; split; auto. simpl. eapply Val.divs_pow2; eauto. congruence. diff --git a/riscV/ConstpropOp.vp b/riscV/ConstpropOp.vp index 37241816..76a1e8f8 100644 --- a/riscV/ConstpropOp.vp +++ b/riscV/ConstpropOp.vp @@ -128,18 +128,24 @@ Definition make_xorimm (n: int) (r: reg) := else (Oxorimm n, r :: nil). Definition make_divimm n (r1 r2: reg) := - match Int.is_power2 n with - | Some l => if Int.ltu l (Int.repr 31) - then (Oshrximm l, r1 :: nil) - else (Odiv, r1 :: r2 :: nil) - | None => (Odiv, r1 :: r2 :: nil) - end. + if Int.eq n Int.one then + (Omove, r1 :: nil) + else + match Int.is_power2 n with + | Some l => if Int.ltu l (Int.repr 31) + then (Oshrximm l, r1 :: nil) + else (Odiv, r1 :: r2 :: nil) + | None => (Odiv, r1 :: r2 :: nil) + end. Definition make_divuimm n (r1 r2: reg) := - match Int.is_power2 n with - | Some l => (Oshruimm l, r1 :: nil) - | None => (Odivu, r1 :: r2 :: nil) - end. + if Int.eq n Int.one then + (Omove, r1 :: nil) + else + match Int.is_power2 n with + | Some l => (Oshruimm l, r1 :: nil) + | None => (Odivu, r1 :: r2 :: nil) + end. Definition make_moduimm n (r1 r2: reg) := match Int.is_power2 n with diff --git a/riscV/ConstpropOpproof.v b/riscV/ConstpropOpproof.v index f2e2b95e..b7452fd4 100644 --- a/riscV/ConstpropOpproof.v +++ b/riscV/ConstpropOpproof.v @@ -249,6 +249,10 @@ Lemma make_divimm_correct: exists w, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some w /\ Val.lessdef v w. Proof. intros; unfold make_divimm. + predSpec Int.eq Int.eq_spec n Int.one; intros. subst. rewrite H0 in H. + destruct (e#r1) eqn:?; + try (rewrite Val.divs_one in H; exists (Vint i); split; simpl; try rewrite Heqv0; auto); + inv H; auto. destruct (Int.is_power2 n) eqn:?. destruct (Int.ltu i (Int.repr 31)) eqn:?. exists v; split; auto. simpl. eapply Val.divs_pow2; eauto. congruence. @@ -264,6 +268,10 @@ Lemma make_divuimm_correct: exists w, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some w /\ Val.lessdef v w. Proof. intros; unfold make_divuimm. + predSpec Int.eq Int.eq_spec n Int.one; intros. subst. rewrite H0 in H. + destruct (e#r1) eqn:?; + try (rewrite Val.divu_one in H; exists (Vint i); split; simpl; try rewrite Heqv0; auto); + inv H; auto. destruct (Int.is_power2 n) eqn:?. econstructor; split. simpl; eauto. rewrite H0 in H. erewrite Val.divu_pow2 by eauto. auto. diff --git a/x86/ConstpropOp.vp b/x86/ConstpropOp.vp index f0000a85..be0cc09a 100644 --- a/x86/ConstpropOp.vp +++ b/x86/ConstpropOp.vp @@ -248,18 +248,24 @@ Definition make_xorimm (n: int) (r: reg) := else (Oxorimm n, r :: nil). Definition make_divimm n (r1 r2: reg) := - match Int.is_power2 n with - | Some l => if Int.ltu l (Int.repr 31) - then (Oshrximm l, r1 :: nil) - else (Odiv, r1 :: r2 :: nil) - | None => (Odiv, r1 :: r2 :: nil) - end. + if Int.eq n Int.one then + (Omove, r1 :: nil) + else + match Int.is_power2 n with + | Some l => if Int.ltu l (Int.repr 31) + then (Oshrximm l, r1 :: nil) + else (Odiv, r1 :: r2 :: nil) + | None => (Odiv, r1 :: r2 :: nil) + end. Definition make_divuimm n (r1 r2: reg) := - match Int.is_power2 n with - | Some l => (Oshruimm l, r1 :: nil) - | None => (Odivu, r1 :: r2 :: nil) - end. + if Int.eq n Int.one then + (Omove, r1 :: nil) + else + match Int.is_power2 n with + | Some l => (Oshruimm l, r1 :: nil) + | None => (Odivu, r1 :: r2 :: nil) + end. Definition make_moduimm n (r1 r2: reg) := match Int.is_power2 n with diff --git a/x86/ConstpropOpproof.v b/x86/ConstpropOpproof.v index ce20738c..e82c2963 100644 --- a/x86/ConstpropOpproof.v +++ b/x86/ConstpropOpproof.v @@ -421,6 +421,10 @@ Lemma make_divimm_correct: exists w, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some w /\ Val.lessdef v w. Proof. intros; unfold make_divimm. + predSpec Int.eq Int.eq_spec n Int.one; intros. subst. rewrite H0 in H. + destruct (e#r1) eqn:?; + try (rewrite Val.divs_one in H; exists (Vint i); split; simpl; try rewrite Heqv0; auto); + inv H; auto. destruct (Int.is_power2 n) eqn:?. destruct (Int.ltu i (Int.repr 31)) eqn:?. exists v; split; auto. simpl. eapply Val.divs_pow2; eauto. congruence. @@ -436,6 +440,10 @@ Lemma make_divuimm_correct: exists w, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some w /\ Val.lessdef v w. Proof. intros; unfold make_divuimm. + predSpec Int.eq Int.eq_spec n Int.one; intros. subst. rewrite H0 in H. + destruct (e#r1) eqn:?; + try (rewrite Val.divu_one in H; exists (Vint i); split; simpl; try rewrite Heqv0; auto); + inv H; auto. destruct (Int.is_power2 n) eqn:?. econstructor; split. simpl; eauto. rewrite H0 in H. erewrite Val.divu_pow2 by eauto. auto. -- cgit