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.

1 files changed, 8 insertions, 0 deletions

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.