diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2017-07-05 12:20:18 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2017-07-05 12:23:42 +0200 |
commit | 92fc8a425034abc1247203a4c0d471e8b6d0e941 (patch) | |
tree | e5fb2b099e1cab906b2a72adf54a2c0e1148f062 /powerpc/ConstpropOpproof.v | |
parent | 1971ab6cd3aff8939edd0e1ca9779b4b44bcc88e (diff) | |
download | compcert-92fc8a425034abc1247203a4c0d471e8b6d0e941.tar.gz compcert-92fc8a425034abc1247203a4c0d471e8b6d0e941.zip |
Issue #16P: wrong rlwinm instruction generated by constant propagation
This happens when the divisor of an unsigned int32 division is constant-propagated to 1.
Diffstat (limited to 'powerpc/ConstpropOpproof.v')
-rw-r--r-- | powerpc/ConstpropOpproof.v | 25 |
1 files changed, 18 insertions, 7 deletions
diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v index d2ebf52d..dd39dc10 100644 --- a/powerpc/ConstpropOpproof.v +++ b/powerpc/ConstpropOpproof.v @@ -209,6 +209,18 @@ Proof. econstructor; split; eauto. simpl. congruence. Qed. +Lemma make_shruimm_aux_correct: + forall n r1, + Int.ltu n Int.iwordsize = true -> + let (op, args) := make_shruimm_aux n r1 in + exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.shru rs#r1 (Vint n)) v. +Proof. + intros; unfold make_shruimm_aux. + predSpec Int.eq Int.eq_spec n Int.zero; intros. subst. + exists (rs#r1); split; auto. destruct (rs#r1); simpl; auto. rewrite Int.shru_zero. auto. + rewrite Val.shru_rolm; auto. econstructor; split; eauto. auto. +Qed. + Lemma make_shruimm_correct: forall n r1 r2, rs#r2 = Vint n -> @@ -216,10 +228,8 @@ Lemma make_shruimm_correct: exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.shru rs#r1 (Vint n)) v. Proof. intros; unfold make_shruimm. - predSpec Int.eq Int.eq_spec n Int.zero; intros. subst. - exists (rs#r1); split; auto. destruct (rs#r1); simpl; auto. rewrite Int.shru_zero. auto. destruct (Int.ltu n Int.iwordsize) eqn:?; intros. - rewrite Val.shru_rolm; auto. econstructor; split; eauto. auto. + apply make_shruimm_aux_correct; auto. econstructor; split; eauto. simpl. congruence. Qed. @@ -265,12 +275,13 @@ Lemma make_divuimm_correct: Proof. intros; unfold make_divuimm. destruct (Int.is_power2 n) eqn:?. - econstructor; split. simpl; eauto. exploit Int.is_power2_range; eauto. intros RANGE. - rewrite <- Val.shru_rolm; auto. rewrite H0 in H. - destruct (rs#r1); simpl in *; inv H. + replace v with (Val.shru rs#r1 (Vint i)). + apply make_shruimm_aux_correct; auto. + rewrite H0 in H. + destruct (rs#r1); simpl in *; inv H. rewrite RANGE. destruct (Int.eq n Int.zero); inv H2. - rewrite RANGE. rewrite (Int.divu_pow2 i0 _ _ Heqo). auto. + f_equal; symmetry; apply Int.divu_pow2; auto. exists v; auto. Qed. |