diff options
author | Michael Schmidt <github@mschmidt.me> | 2017-12-05 14:48:18 +0100 |
---|---|---|
committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2017-12-05 14:48:18 +0100 |
commit | 90b76a0842b7f080893dd70a7c0c6bc878f4056b (patch) | |
tree | 277edd1eecf7bc7574a4b4dc3b925e3479dab8fd /powerpc/ConstpropOpproof.v | |
parent | 442e82e6ffc6958192f73382d2270e926ead9c80 (diff) | |
download | compcert-90b76a0842b7f080893dd70a7c0c6bc878f4056b.tar.gz compcert-90b76a0842b7f080893dd70a7c0c6bc878f4056b.zip |
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.
Diffstat (limited to 'powerpc/ConstpropOpproof.v')
-rw-r--r-- | powerpc/ConstpropOpproof.v | 4 |
1 files changed, 4 insertions, 0 deletions
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. |