From 92fc8a425034abc1247203a4c0d471e8b6d0e941 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Wed, 5 Jul 2017 12:20:18 +0200
Subject: Issue #16P: wrong rlwinm instruction generated by constant
 propagation

This happens when the divisor of an unsigned int32 division is constant-propagated to 1.
---
 Changelog                  |  6 ++++--
 powerpc/ConstpropOp.vp     | 12 ++++++++----
 powerpc/ConstpropOpproof.v | 25 ++++++++++++++++++-------
 3 files changed, 30 insertions(+), 13 deletions(-)

diff --git a/Changelog b/Changelog
index ecf50f7d..ddd495e1 100644
--- a/Changelog
+++ b/Changelog
@@ -10,8 +10,10 @@ Bug fixing:
 - Issue #179: clightgen produces wrong output for "switch" statements.
 - Do not generate code for functions with "inline" specifier that are
   neither static nor extern, as per ISO C99.
-- Some line number information was missing for some goto labels and switch cases.
-
+- Some line number information was missing for some goto labels and
+  switch cases.
+- Issue #P16: illegal PowerPC asm generated for unsigned division after
+  constant propagation.
 
 Release 3.0.1, 2017-02-14
 =========================
diff --git a/powerpc/ConstpropOp.vp b/powerpc/ConstpropOp.vp
index 8946ae27..886655a0 100644
--- a/powerpc/ConstpropOp.vp
+++ b/powerpc/ConstpropOp.vp
@@ -92,11 +92,15 @@ Definition make_shrimm (n: int) (r1 r2: reg) :=
   else
     (Oshr, r1 :: r2 :: nil).
 
-Definition make_shruimm (n: int) (r1 r2: reg) :=
+Definition make_shruimm_aux (n: int) (r1: reg) :=
   if Int.eq n Int.zero then
     (Omove, r1 :: nil)
-  else if Int.ltu n Int.iwordsize then
-    (Orolm (Int.sub Int.iwordsize n) (Int.shru Int.mone n), r1 :: nil)
+  else
+    (Orolm (Int.sub Int.iwordsize n) (Int.shru Int.mone n), r1 :: nil).
+
+Definition make_shruimm (n: int) (r1 r2: reg) :=
+  if Int.ltu n Int.iwordsize then
+    make_shruimm_aux n r1
   else
     (Oshru, r1 :: r2 :: nil).
 
@@ -121,7 +125,7 @@ Definition make_divimm (n: int) (r1 r2: reg) :=
 
 Definition make_divuimm (n: int) (r1 r2: reg) :=
   match Int.is_power2 n with
-  | Some l => (Orolm (Int.sub Int.iwordsize l) (Int.shru Int.mone l), r1 :: nil)
+  | Some l => make_shruimm_aux l r1
   | None   => (Odivu, r1 :: r2 :: nil)
   end.
 
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.
 
-- 
cgit