Instead of having two expansions of shrximm (one in SelectOp, one in Asmgen), move the most efficient expansion to Asmgen.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2504 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

4 files changed, 54 insertions, 78 deletions

diff --git a/arm/Asmgen.v b/arm/Asmgen.v
index fcc5061..2513a5e 100644
--- a/arm/Asmgen.v
+++ b/arm/Asmgen.v
@@ -376,10 +376,12 @@ Definition transl_op
       OK (Pmov r (transl_shift s r1) :: k)
   | Oshrximm n, a1 :: nil =>
       do r <- ireg_of res; do r1 <- ireg_of a1;
-      OK (Pcmp r1 (SOimm Int.zero) ::
-          addimm IR14 r1 (Int.sub (Int.shl Int.one n) Int.one)
-             (Pmovc TCge IR14 (SOreg r1) ::
-              Pmov r (SOasrimm IR14 n) :: k))
+      if Int.eq n Int.zero then
+        OK (Pmov r (SOreg r1) :: k)
+      else
+        OK (Pmov IR14 (SOasrimm r1 (Int.repr 31)) ::
+            Padd IR14 r1 (SOlsrimm IR14 (Int.sub Int.iwordsize n)) ::
+            Pmov r (SOasrimm IR14 n) :: k)
   | Onegf, a1 :: nil =>
       do r <- freg_of res; do r1 <- freg_of a1;
       OK (Pfnegd r r1 :: k)
diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v
index ec6d405..3e00217 100644
--- a/arm/Asmgenproof1.v
+++ b/arm/Asmgenproof1.v
@@ -981,34 +981,51 @@ Local Transparent destroyed_by_op.
   intros [rs' [A [B C]]]. 
   exists rs'; auto with asmgen.
   (* Oshrximm *)
-  exploit Val.shrx_shr; eauto. intros [n [i' [ARG1 [ARG2 RES]]]].
-  injection ARG2; intro ARG2'; subst i'; clear ARG2.
-  set (islt := Int.lt n Int.zero) in *.
-  set (rs1 := nextinstr (compare_int rs (Vint n) (Vint Int.zero) m)).
-  assert (OTH1: forall r', data_preg r' = true -> rs1#r' = rs#r').
-  { apply compare_int_inv; auto. }
-  exploit (addimm_correct IR14 x0 (Int.sub (Int.shl Int.one i) Int.one)).
-  intros [rs2 [EXEC2 [RES2 OTH2]]].
-  set (rs3 := nextinstr (if islt then rs2 else rs2#IR14 <- (Vint n))).
-  set (rs4 := nextinstr (rs3#x <- (Val.shr rs3#IR14 (Vint i)))).
-  exists rs4; split.
-  apply exec_straight_step with rs1 m.
-  simpl. rewrite ARG1. auto. auto.
-  eapply exec_straight_trans. eexact EXEC2.
-  apply exec_straight_two with rs3 m.
-  unfold exec_instr. 
-  assert (TC: eval_testcond TCge rs2 = Some (negb islt)).
-  { simpl. rewrite ! OTH2 by auto with asmgen. simpl. 
-    rewrite Int.lt_sub_overflow. fold islt. destruct islt; auto. }
-  rewrite TC. simpl. rewrite OTH2 by eauto with asmgen. rewrite OTH1. rewrite ARG1.
-  unfold rs3; destruct islt; reflexivity.
-  rewrite <- (ireg_of_eq _ _ EQ1). auto with asmgen.
-  reflexivity.
-  unfold rs3; destruct islt; reflexivity.
-  reflexivity.
-  split. unfold rs4; Simpl. unfold rs3. destruct islt. 
-  Simpl. rewrite RES2. unfold rs1. Simpl. Simpl. congruence.
-  intros. unfold rs4, rs3; Simpl. destruct islt; Simpl; rewrite OTH2; auto with asmgen. 
+  destruct (rs x0) eqn: X0; simpl in H0; try discriminate. 
+  destruct (Int.ltu i (Int.repr 31)) eqn: LTU; inv H0. 
+  revert EQ2. predSpec Int.eq Int.eq_spec i Int.zero; intros EQ2. 
+  (* i = 0 *)
+  inv EQ2. econstructor. 
+  split. apply exec_straight_one. simpl. reflexivity. auto. 
+  split. Simpl. unfold Int.shrx. rewrite Int.shl_zero. unfold Int.divs. 
+  change (Int.signed Int.one) with 1. rewrite Z.quot_1_r. rewrite Int.repr_signed. auto.
+  intros. Simpl. 
+  (* i <> 0 *)
+  inv EQ2.
+  assert (LTU': Int.ltu (Int.sub Int.iwordsize i) Int.iwordsize = true).
+  {
+    generalize (Int.ltu_inv _ _ LTU). intros.
+    unfold Int.sub, Int.ltu. rewrite Int.unsigned_repr_wordsize. 
+    rewrite Int.unsigned_repr. apply zlt_true.
+    assert (Int.unsigned i <> 0). 
+    { red; intros; elim H. rewrite <- (Int.repr_unsigned i). rewrite H1; reflexivity. }
+    omega. 
+    change (Int.unsigned (Int.repr 31)) with (Int.zwordsize - 1) in H0.
+    generalize Int.wordsize_max_unsigned; omega. 
+  }
+  assert (LTU'': Int.ltu i Int.iwordsize = true).
+  {
+    generalize (Int.ltu_inv _ _ LTU). intros.
+    unfold Int.ltu. rewrite Int.unsigned_repr_wordsize. apply zlt_true.
+    change (Int.unsigned (Int.repr 31)) with (Int.zwordsize - 1) in H0.
+    omega.
+  }
+  set (j := Int.sub Int.iwordsize i) in *.
+  set (rs1 := nextinstr (rs#IR14 <- (Val.shr (Vint i0) (Vint (Int.repr 31))))).
+  set (rs2 := nextinstr (rs1#IR14 <- (Val.add (Vint i0) (Val.shru rs1#IR14 (Vint j))))).
+  set (rs3 := nextinstr (rs2#x <- (Val.shr rs2#IR14 (Vint i)))).
+  exists rs3; split.
+  apply exec_straight_three with rs1 m rs2 m.
+  simpl. rewrite X0; reflexivity.
+  simpl. f_equal. Simpl. replace (rs1 x0) with (rs x0). rewrite X0; reflexivity.
+  unfold rs1; Simpl.
+  reflexivity. 
+  auto. auto. auto.
+  split. unfold rs3; Simpl. unfold rs2; Simpl. unfold rs1; Simpl. 
+  simpl. change (Int.ltu (Int.repr 31) Int.iwordsize) with true. simpl. 
+  rewrite LTU'; simpl. rewrite LTU''; simpl. 
+  f_equal. symmetry. apply Int.shrx_shr_2. assumption. 
+  intros. unfold rs3; Simpl. unfold rs2; Simpl. unfold rs1; Simpl. 
   (* intoffloat *)
   econstructor; split. apply exec_straight_one; simpl. rewrite H0; simpl. eauto. auto.
 Transparent destroyed_by_op. 
diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp
index efd9e48..e4005c9 100644
--- a/arm/SelectOp.vp
+++ b/arm/SelectOp.vp
@@ -291,14 +291,7 @@ Definition divu_base (e1: expr) (e2: expr) := Eop Odivu (e1:::e2:::Enil).
 Definition modu_base := mod_aux Odivu.
 
 Definition shrximm (e1: expr) (n2: int) :=
-  if Int.eq n2 Int.zero
-  then e1
-  else Elet e1
-         (shrimm
-             (add (Eletvar O)
-                  (shruimm (shrimm (Eletvar O) (Int.repr 31))
-                           (Int.sub Int.iwordsize n2)))
-             n2).
+  if Int.eq n2 Int.zero then e1 else Eop (Oshrximm n2) (e1:::Enil).
 
 (** ** General shifts *)
 
diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v
index 4b89119..1dd2c20 100644
--- a/arm/SelectOpproof.v
+++ b/arm/SelectOpproof.v
@@ -542,49 +542,13 @@ Theorem eval_shrximm:
 Proof.
   intros. unfold shrximm. 
   predSpec Int.eq Int.eq_spec n Int.zero.
-- subst n. exists x; split; auto. 
+  subst n. exists x; split; auto. 
   destruct x; simpl in H0; try discriminate.
   destruct (Int.ltu Int.zero (Int.repr 31)); inv H0.
   replace (Int.shrx i Int.zero) with i. auto. 
   unfold Int.shrx, Int.divs. rewrite Int.shl_zero. 
   change (Int.signed Int.one) with 1. rewrite Z.quot_1_r. rewrite Int.repr_signed; auto.
-- destruct x; simpl in H0; try discriminate.
-  destruct (Int.ltu n (Int.repr 31)) eqn:LT31; inv H0.
-  assert (A: eval_expr ge sp e m (Vint i :: le) (Eletvar 0) (Vint i))
-  by (constructor; auto).
-  exploit (eval_shrimm (Int.repr 31)). eexact A.
-  intros [v [B LD]]. simpl in LD. 
-  change (Int.ltu (Int.repr 31) Int.iwordsize) with true in LD. 
-  simpl in LD; inv LD.
-  exploit (eval_shruimm (Int.sub Int.iwordsize n)). eexact B.
-  intros [v [C LD]]. simpl in LD.
-  assert (RANGE: Int.ltu (Int.sub Int.iwordsize n) Int.iwordsize = true).
-  {
-    generalize (Int.ltu_inv _ _ LT31). intros.
-    unfold Int.sub, Int.ltu. rewrite Int.unsigned_repr_wordsize. 
-    rewrite Int.unsigned_repr. apply zlt_true.
-    assert (Int.unsigned n <> 0). 
-    { red; intros; elim H1. rewrite <- (Int.repr_unsigned n). rewrite H2; reflexivity. }
-    omega. 
-    change (Int.unsigned (Int.repr 31)) with (Int.zwordsize - 1) in H0.
-    generalize Int.wordsize_max_unsigned; omega. 
-  }
-  rewrite RANGE in LD. inv LD. 
-  exploit eval_add. eexact A. eexact C. intros [v [D LD]].
-  simpl in LD. inv LD. 
-  exploit (eval_shrimm n). eexact D. intros [v [E LD]].
-  simpl in LD. 
-  assert (RANGE2: Int.ltu n Int.iwordsize = true).
-  {
-    generalize (Int.ltu_inv _ _ LT31). intros.
-    unfold Int.ltu. rewrite Int.unsigned_repr_wordsize. apply zlt_true.
-    change (Int.unsigned (Int.repr 31)) with (Int.zwordsize - 1) in H0.
-    omega.
-  }
-  rewrite RANGE2 in LD. inv LD. 
-  econstructor; split. econstructor. eassumption. eexact E. 
-  rewrite Int.shrx_shr_2 by auto.
-  auto.
+  econstructor; split. EvalOp. auto.
 Qed.
 
 Theorem eval_shl: binary_constructor_sound shl Val.shl.