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/ConstpropOpproof.v | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'arm/ConstpropOpproof.v') 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. -- cgit