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/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.