Revised lib/Integers.v to make it parametric w.r.t. word size.

Introduced Int.iwordsize and used it in place of "Int.repr 32" or
"Int.repr (Z_of_nat wordsize)".



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

7 files changed, 66 insertions, 72 deletions

diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index 1582b41..60c3d34 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -302,9 +302,7 @@ lbl:    .long   0x43300000, 0x00000000
         lwz     r12, lo16(lbl)(r12)
         mtctr   r12
         bctr    r12
-        .const_data
 lbl:    .long   table[0], table[1], ...
-        .text
 >>
   Note that [reg] contains 4 times the index of the desired table entry.
 *)
diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v
index 3baeb79..7329e53 100644
--- a/powerpc/Asmgenproof1.v
+++ b/powerpc/Asmgenproof1.v
@@ -48,13 +48,13 @@ Proof.
   intros. unfold high_u, low_u.
   rewrite Int.shl_rolm. rewrite Int.shru_rolm. 
   rewrite Int.rolm_rolm. 
-  change (Int.modu (Int.add (Int.sub (Int.repr (Z_of_nat wordsize)) (Int.repr 16))
+  change (Int.modu (Int.add (Int.sub (Int.repr (Z_of_nat Int.wordsize)) (Int.repr 16))
                             (Int.repr 16))
-                   (Int.repr (Z_of_nat wordsize)))
+                   (Int.repr (Z_of_nat Int.wordsize)))
     with (Int.zero).
   rewrite Int.rolm_zero. rewrite <- Int.and_or_distrib.
   exact (Int.and_mone n).
-  reflexivity. reflexivity.
+  apply int_wordsize_divides_modulus. reflexivity. reflexivity.
 Qed.
 
 Lemma low_high_u_xor:
@@ -63,13 +63,13 @@ Proof.
   intros. unfold high_u, low_u.
   rewrite Int.shl_rolm. rewrite Int.shru_rolm. 
   rewrite Int.rolm_rolm. 
-  change (Int.modu (Int.add (Int.sub (Int.repr (Z_of_nat wordsize)) (Int.repr 16))
+  change (Int.modu (Int.add (Int.sub (Int.repr (Z_of_nat Int.wordsize)) (Int.repr 16))
                             (Int.repr 16))
-                   (Int.repr (Z_of_nat wordsize)))
+                   (Int.repr (Z_of_nat Int.wordsize)))
     with (Int.zero).
   rewrite Int.rolm_zero. rewrite <- Int.and_xor_distrib.
   exact (Int.and_mone n).
-  reflexivity. reflexivity.
+  apply int_wordsize_divides_modulus. reflexivity. reflexivity.
 Qed.
 
 Lemma low_high_s:
@@ -91,7 +91,7 @@ Proof.
   unfold Int.sub. 
   assert (forall a b, Int.eqm a b -> b mod 65536 = 0 -> a mod 65536 = 0).
   intros a b [k EQ] H1. rewrite EQ. 
-  change modulus with (65536 * 65536). 
+  change Int.modulus with (65536 * 65536). 
   rewrite Zmult_assoc. rewrite Zplus_comm. rewrite Z_mod_plus. auto.
   omega.
   eapply H0. apply Int.eqm_sym. apply Int.eqm_unsigned_repr. 
diff --git a/powerpc/ConstpropOp.v b/powerpc/ConstpropOp.v
index 87b2cfa..ededce0 100644
--- a/powerpc/ConstpropOp.v
+++ b/powerpc/ConstpropOp.v
@@ -166,11 +166,11 @@ Definition eval_static_operation (op: operation) (vl: list approx) :=
   | Onand, I n1 :: I n2 :: nil => I(Int.xor (Int.and n1 n2) Int.mone)
   | Onor, I n1 :: I n2 :: nil => I(Int.xor (Int.or n1 n2) Int.mone)
   | Onxor, I n1 :: I n2 :: nil => I(Int.xor (Int.xor n1 n2) Int.mone)
-  | Oshl, I n1 :: I n2 :: nil => if Int.ltu n2 (Int.repr 32) then I(Int.shl n1 n2) else Unknown
-  | Oshr, I n1 :: I n2 :: nil => if Int.ltu n2 (Int.repr 32) then I(Int.shr n1 n2) else Unknown
-  | Oshrimm n, I n1 :: nil => if Int.ltu n (Int.repr 32) then I(Int.shr n1 n) else Unknown
-  | Oshrximm n, I n1 :: nil => if Int.ltu n (Int.repr 32) then I(Int.shrx n1 n) else Unknown
-  | Oshru, I n1 :: I n2 :: nil => if Int.ltu n2 (Int.repr 32) then I(Int.shru n1 n2) else Unknown
+  | Oshl, I n1 :: I n2 :: nil => if Int.ltu n2 Int.iwordsize then I(Int.shl n1 n2) else Unknown
+  | Oshr, I n1 :: I n2 :: nil => if Int.ltu n2 Int.iwordsize then I(Int.shr n1 n2) else Unknown
+  | Oshrimm n, I n1 :: nil => if Int.ltu n Int.iwordsize then I(Int.shr n1 n) else Unknown
+  | Oshrximm n, I n1 :: nil => if Int.ltu n Int.iwordsize then I(Int.shrx n1 n) else Unknown
+  | Oshru, I n1 :: I n2 :: nil => if Int.ltu n2 Int.iwordsize then I(Int.shru n1 n2) else Unknown
   | Orolm amount mask, I n1 :: nil => I(Int.rolm n1 amount mask)
   | Onegf, F n1 :: nil => F(Float.neg n1)
   | Oabsf, F n1 :: nil => F(Float.abs n1)
@@ -500,15 +500,15 @@ Definition eval_static_operation (op: operation) (vl: list approx) :=
   | eval_static_operation_case28 n1 n2 =>
       I(Int.xor (Int.xor n1 n2) Int.mone)
   | eval_static_operation_case29 n1 n2 =>
-      if Int.ltu n2 (Int.repr 32) then I(Int.shl n1 n2) else Unknown
+      if Int.ltu n2 Int.iwordsize then I(Int.shl n1 n2) else Unknown
   | eval_static_operation_case30 n1 n2 =>
-      if Int.ltu n2 (Int.repr 32) then I(Int.shr n1 n2) else Unknown
+      if Int.ltu n2 Int.iwordsize then I(Int.shr n1 n2) else Unknown
   | eval_static_operation_case31 n n1 =>
-      if Int.ltu n (Int.repr 32) then I(Int.shr n1 n) else Unknown
+      if Int.ltu n Int.iwordsize then I(Int.shr n1 n) else Unknown
   | eval_static_operation_case32 n n1 =>
-      if Int.ltu n (Int.repr 32) then I(Int.shrx n1 n) else Unknown
+      if Int.ltu n Int.iwordsize then I(Int.shrx n1 n) else Unknown
   | eval_static_operation_case33 n1 n2 =>
-      if Int.ltu n2 (Int.repr 32) then I(Int.shru n1 n2) else Unknown
+      if Int.ltu n2 Int.iwordsize then I(Int.shru n1 n2) else Unknown
   | eval_static_operation_case34 amount mask n1 =>
       I(Int.rolm n1 amount mask)
   | eval_static_operation_case35 n1 =>
@@ -628,7 +628,7 @@ Definition make_shrimm (n: int) (r: reg) :=
 Definition make_shruimm (n: int) (r: reg) :=
   if Int.eq n Int.zero
   then (Omove, r :: nil)
-  else (Orolm (Int.sub (Int.repr 32) n) (Int.shru Int.mone n), r :: nil).
+  else (Orolm (Int.sub Int.iwordsize n) (Int.shru Int.mone n), r :: nil).
 
 Definition make_mulimm (n: int) (r: reg) :=
   if Int.eq n Int.zero then
@@ -789,7 +789,7 @@ Definition op_strength_reduction (op: operation) (args: list reg) :=
   | op_strength_reduction_case9 r1 r2 => (* Oshl *)
       match intval r2 with
       | Some n =>
-          if Int.ltu n (Int.repr 32)
+          if Int.ltu n Int.iwordsize
           then make_shlimm n r1
           else (op, args)
       | _ => (op, args)
@@ -797,7 +797,7 @@ Definition op_strength_reduction (op: operation) (args: list reg) :=
   | op_strength_reduction_case10 r1 r2 => (* Oshr *)
       match intval r2 with
       | Some n =>
-          if Int.ltu n (Int.repr 32)
+          if Int.ltu n Int.iwordsize
           then make_shrimm n r1
           else (op, args)
       | _ => (op, args)
@@ -805,7 +805,7 @@ Definition op_strength_reduction (op: operation) (args: list reg) :=
   | op_strength_reduction_case11 r1 r2 => (* Oshru *)
       match intval r2 with
       | Some n =>
-          if Int.ltu n (Int.repr 32)
+          if Int.ltu n Int.iwordsize
           then make_shruimm n r1
           else (op, args)
       | _ => (op, args)
diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v
index 0c7be7b..2e28d23 100644
--- a/powerpc/ConstpropOpproof.v
+++ b/powerpc/ConstpropOpproof.v
@@ -130,19 +130,19 @@ Proof.
   subst v. unfold Int.not. congruence.
   subst v. unfold Int.not. congruence.
 
-  replace n2 with i0. destruct (Int.ltu i0 (Int.repr 32)).
+  replace n2 with i0. destruct (Int.ltu i0 Int.iwordsize).
   injection H0; intro; subst v. simpl. congruence. discriminate. congruence. 
 
-  replace n2 with i0. destruct (Int.ltu i0 (Int.repr 32)).
+  replace n2 with i0. destruct (Int.ltu i0 Int.iwordsize).
   injection H0; intro; subst v. simpl. congruence. discriminate. congruence. 
 
-  destruct (Int.ltu n (Int.repr 32)).
+  destruct (Int.ltu n Int.iwordsize).
   injection H0; intro; subst v. simpl. congruence. discriminate. 
 
-  destruct (Int.ltu n (Int.repr 32)).
+  destruct (Int.ltu n Int.iwordsize).
   injection H0; intro; subst v. simpl. congruence. discriminate. 
 
-  replace n2 with i0. destruct (Int.ltu i0 (Int.repr 32)).
+  replace n2 with i0. destruct (Int.ltu i0 Int.iwordsize).
   injection H0; intro; subst v. simpl. congruence. discriminate. congruence. 
 
   rewrite <- H3. replace v0 with (Vfloat n1). reflexivity. congruence.
@@ -229,7 +229,7 @@ Proof.
   intros; unfold make_shlimm.
   generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros.
   subst n. simpl in *. FuncInv. rewrite Int.shl_zero in H. congruence.
-  simpl in *. FuncInv. caseEq (Int.ltu n (Int.repr 32)); intros.
+  simpl in *. FuncInv. caseEq (Int.ltu n Int.iwordsize); intros.
   rewrite H1 in H0. rewrite Int.shl_rolm in H0. auto. exact H1.
   rewrite H1 in H0. discriminate.
 Qed.
@@ -255,7 +255,7 @@ Proof.
   intros; unfold make_shruimm.
   generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros.
   subst n. simpl in *. FuncInv. rewrite Int.shru_zero in H. congruence.
-  simpl in *. FuncInv. caseEq (Int.ltu n (Int.repr 32)); intros.
+  simpl in *. FuncInv. caseEq (Int.ltu n Int.iwordsize); intros.
   rewrite H1 in H0. rewrite Int.shru_rolm in H0. auto. exact H1.
   rewrite H1 in H0. discriminate.
 Qed.
@@ -276,7 +276,7 @@ Proof.
      with (eval_operation ge sp Oshl (rs # r :: Vint i :: nil)).
   apply make_shlimm_correct. 
   simpl. generalize (Int.is_power2_range _ _ H1). 
-  change (Z_of_nat wordsize) with 32. intro. rewrite H2.
+  change (Z_of_nat Int.wordsize) with 32. intro. rewrite H2.
   destruct rs#r; auto. rewrite (Int.mul_pow2 i0 _ _ H1). auto.
   exact H2.
 Qed.
@@ -364,7 +364,7 @@ Proof.
   caseEq (Int.is_power2 i); intros.
   rewrite (intval_correct _ _ H) in H1.   
   simpl in *; FuncInv. destruct (Int.eq i Int.zero). congruence.
-  change 32 with (Z_of_nat wordsize). 
+  change 32 with (Z_of_nat Int.wordsize). 
   rewrite (Int.is_power2_range _ _ H0). 
   rewrite (Int.divs_pow2 i1 _ _ H0) in H1. auto.
   assumption.
@@ -377,7 +377,7 @@ Proof.
      with (eval_operation ge sp Oshru (rs # r1 :: Vint i0 :: nil)).
   apply make_shruimm_correct. 
   simpl. destruct rs#r1; auto. 
-  change 32 with (Z_of_nat wordsize). 
+  change 32 with (Z_of_nat Int.wordsize). 
   rewrite (Int.is_power2_range _ _ H0). 
   generalize (Int.eq_spec i Int.zero); case (Int.eq i Int.zero); intros.
   subst i. discriminate. 
@@ -416,19 +416,19 @@ Proof.
   assumption.
   (* Oshl *)
   caseEq (intval app r2); intros.
-  caseEq (Int.ltu i (Int.repr 32)); intros.
+  caseEq (Int.ltu i Int.iwordsize); intros.
   rewrite (intval_correct _ _ H). apply make_shlimm_correct.
   assumption.
   assumption.
   (* Oshr *)
   caseEq (intval app r2); intros.
-  caseEq (Int.ltu i (Int.repr 32)); intros.
+  caseEq (Int.ltu i Int.iwordsize); intros.
   rewrite (intval_correct _ _ H). apply make_shrimm_correct.
   assumption.
   assumption.
   (* Oshru *)
   caseEq (intval app r2); intros.
-  caseEq (Int.ltu i (Int.repr 32)); intros.
+  caseEq (Int.ltu i Int.iwordsize); intros.
   rewrite (intval_correct _ _ H). apply make_shruimm_correct.
   assumption.
   assumption.
diff --git a/powerpc/Op.v b/powerpc/Op.v
index 27e12c2..c6e196f 100644
--- a/powerpc/Op.v
+++ b/powerpc/Op.v
@@ -224,15 +224,15 @@ Definition eval_operation
   | Onor, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.not (Int.or n1 n2)))
   | Onxor, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.not (Int.xor n1 n2)))
   | Oshl, Vint n1 :: Vint n2 :: nil =>
-      if Int.ltu n2 (Int.repr 32) then Some (Vint (Int.shl n1 n2)) else None
+      if Int.ltu n2 Int.iwordsize then Some (Vint (Int.shl n1 n2)) else None
   | Oshr, Vint n1 :: Vint n2 :: nil =>
-      if Int.ltu n2 (Int.repr 32) then Some (Vint (Int.shr n1 n2)) else None
+      if Int.ltu n2 Int.iwordsize then Some (Vint (Int.shr n1 n2)) else None
   | Oshrimm n, Vint n1 :: nil =>
-      if Int.ltu n (Int.repr 32) then Some (Vint (Int.shr n1 n)) else None
+      if Int.ltu n Int.iwordsize then Some (Vint (Int.shr n1 n)) else None
   | Oshrximm n, Vint n1 :: nil =>
-      if Int.ltu n (Int.repr 32) then Some (Vint (Int.shrx n1 n)) else None
+      if Int.ltu n Int.iwordsize then Some (Vint (Int.shrx n1 n)) else None
   | Oshru, Vint n1 :: Vint n2 :: nil =>
-      if Int.ltu n2 (Int.repr 32) then Some (Vint (Int.shru n1 n2)) else None
+      if Int.ltu n2 Int.iwordsize then Some (Vint (Int.shru n1 n2)) else None
   | Orolm amount mask, Vint n1 :: nil =>
       Some (Vint (Int.rolm n1 amount mask))
   | Onegf, Vfloat f1 :: nil => Some (Vfloat (Float.neg f1))
@@ -522,15 +522,15 @@ Proof.
   injection H0; intro; subst v; exact I.
   destruct (Int.eq i0 Int.zero). discriminate. 
   injection H0; intro; subst v; exact I.
-  destruct (Int.ltu i0 (Int.repr 32)).
+  destruct (Int.ltu i0 Int.iwordsize).
   injection H0; intro; subst v; exact I. discriminate.
-  destruct (Int.ltu i0 (Int.repr 32)).
+  destruct (Int.ltu i0 Int.iwordsize).
   injection H0; intro; subst v; exact I. discriminate.
-  destruct (Int.ltu i (Int.repr 32)).
+  destruct (Int.ltu i Int.iwordsize).
   injection H0; intro; subst v; exact I. discriminate.
-  destruct (Int.ltu i (Int.repr 32)).
+  destruct (Int.ltu i Int.iwordsize).
   injection H0; intro; subst v; exact I. discriminate.
-  destruct (Int.ltu i0 (Int.repr 32)).
+  destruct (Int.ltu i0 Int.iwordsize).
   injection H0; intro; subst v; exact I. discriminate.
   destruct v0; exact I.
   destruct (eval_condition c vl). 
@@ -694,11 +694,11 @@ Proof.
   unfold eq_block in H. destruct (zeq b b0); congruence.
   destruct (Int.eq i0 Int.zero); congruence.
   destruct (Int.eq i0 Int.zero); congruence.
-  destruct (Int.ltu i0 (Int.repr 32)); congruence.
-  destruct (Int.ltu i0 (Int.repr 32)); congruence.
-  destruct (Int.ltu i (Int.repr 32)); congruence.
-  destruct (Int.ltu i (Int.repr 32)); congruence.
-  destruct (Int.ltu i0 (Int.repr 32)); congruence.
+  destruct (Int.ltu i0 Int.iwordsize); congruence.
+  destruct (Int.ltu i0 Int.iwordsize); congruence.
+  destruct (Int.ltu i Int.iwordsize); congruence.
+  destruct (Int.ltu i Int.iwordsize); congruence.
+  destruct (Int.ltu i0 Int.iwordsize); congruence.
   caseEq (eval_condition c vl); intros; rewrite H0 in H.
   replace v with (Val.of_bool b).
   eapply eval_condition_weaken; eauto.
@@ -797,11 +797,11 @@ Proof.
   destruct (eq_block b b0); inv H0. TrivialExists.
   destruct (Int.eq i0 Int.zero); inv H0; TrivialExists.
   destruct (Int.eq i0 Int.zero); inv H0; TrivialExists.
-  destruct (Int.ltu i0 (Int.repr 32)); inv H0; TrivialExists.
-  destruct (Int.ltu i0 (Int.repr 32)); inv H0; TrivialExists.
-  destruct (Int.ltu i (Int.repr 32)); inv H0; TrivialExists.
-  destruct (Int.ltu i (Int.repr 32)); inv H0; TrivialExists.
-  destruct (Int.ltu i0 (Int.repr 32)); inv H0; TrivialExists.
+  destruct (Int.ltu i0 Int.iwordsize); inv H0; TrivialExists.
+  destruct (Int.ltu i0 Int.iwordsize); inv H0; TrivialExists.
+  destruct (Int.ltu i Int.iwordsize); inv H0; TrivialExists.
+  destruct (Int.ltu i Int.iwordsize); inv H0; TrivialExists.
+  destruct (Int.ltu i0 Int.iwordsize); inv H0; TrivialExists.
   exists (Val.singleoffloat v2); split. auto. apply Val.singleoffloat_lessdef; auto.
   caseEq (eval_condition c vl1); intros. rewrite H1 in H0. 
   rewrite (eval_condition_lessdef c H H1).
diff --git a/powerpc/SelectOp.v b/powerpc/SelectOp.v
index ef55b8b..40201e7 100644
--- a/powerpc/SelectOp.v
+++ b/powerpc/SelectOp.v
@@ -396,7 +396,7 @@ Definition rolm (e1: expr) (amount2 mask2: int) :=
   | rolm_case1 n1 =>
       Eop (Ointconst(Int.and (Int.rol n1 amount2) mask2)) Enil
   | rolm_case2 amount1 mask1 t1 =>
-      let amount := Int.and (Int.add amount1 amount2) (Int.repr 31) in
+      let amount := Int.modu (Int.add amount1 amount2) Int.iwordsize in
       let mask := Int.and (Int.rol mask1 amount2) mask2 in
       if Int.is_rlw_mask mask
       then Eop (Orolm amount mask) (t1:::Enil)
@@ -408,7 +408,7 @@ Definition rolm (e1: expr) (amount2 mask2: int) :=
 Definition shlimm (e1: expr) (n2: int) :=
   if Int.eq n2 Int.zero then
     e1
-  else if Int.ltu n2 (Int.repr 32) then
+  else if Int.ltu n2 Int.iwordsize then
     rolm e1 n2 (Int.shl Int.mone n2)
   else
     Eop Oshl (e1:::Eop (Ointconst n2) Enil:::Enil).
@@ -416,8 +416,8 @@ Definition shlimm (e1: expr) (n2: int) :=
 Definition shruimm (e1: expr) (n2: int) :=
   if Int.eq n2 Int.zero then
     e1
-  else if Int.ltu n2 (Int.repr 32) then
-    rolm e1 (Int.sub (Int.repr 32) n2) (Int.shru Int.mone n2)
+  else if Int.ltu n2 Int.iwordsize then
+    rolm e1 (Int.sub Int.iwordsize n2) (Int.shru Int.mone n2)
   else
     Eop Oshru (e1:::Eop (Ointconst n2) Enil:::Enil).
 
diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v
index 77bca50..ae152b3 100644
--- a/powerpc/SelectOpproof.v
+++ b/powerpc/SelectOpproof.v
@@ -346,11 +346,7 @@ Proof.
   case (Int.is_rlw_mask (Int.and (Int.rol mask1 amount) mask)).
   EvalOp. simpl. subst x. 
   decEq. decEq. 
-  replace (Int.and (Int.add amount1 amount) (Int.repr 31))
-     with (Int.modu (Int.add amount1 amount) (Int.repr 32)).
-  symmetry. apply Int.rolm_rolm. 
-  change (Int.repr 31) with (Int.sub (Int.repr 32) Int.one).
-  apply Int.modu_and with (Int.repr 5). reflexivity.
+  symmetry. apply Int.rolm_rolm. apply int_wordsize_divides_modulus.
   EvalOp. econstructor. EvalOp. simpl. rewrite H. reflexivity. constructor. auto.  
   EvalOp.
 Qed.
@@ -358,7 +354,7 @@ Qed.
 Theorem eval_shlimm:
   forall le a n x,
   eval_expr ge sp e m le a (Vint x) ->
-  Int.ltu n (Int.repr 32) = true ->
+  Int.ltu n Int.iwordsize = true ->
   eval_expr ge sp e m le (shlimm a n) (Vint (Int.shl x n)).
 Proof.
   intros.  unfold shlimm.
@@ -372,14 +368,14 @@ Qed.
 Theorem eval_shruimm:
   forall le a n x,
   eval_expr ge sp e m le a (Vint x) ->
-  Int.ltu n (Int.repr 32) = true ->
+  Int.ltu n Int.iwordsize = true ->
   eval_expr ge sp e m le (shruimm a n) (Vint (Int.shru x n)).
 Proof.
   intros.  unfold shruimm.
   generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intro.
   subst n. rewrite Int.shru_zero. auto.
   rewrite H0.
-  replace (Int.shru x n) with (Int.rolm x (Int.sub (Int.repr 32) n) (Int.shru Int.mone n)).
+  replace (Int.shru x n) with (Int.rolm x (Int.sub Int.iwordsize n) (Int.shru Int.mone n)).
   apply eval_rolm. auto. symmetry. apply Int.shru_rolm. exact H0.
 Qed.
 
@@ -391,7 +387,7 @@ Proof.
   intros; unfold mulimm_base. 
   generalize (Int.one_bits_decomp n). 
   generalize (Int.one_bits_range n).
-  change (Z_of_nat wordsize) with 32.
+  change (Z_of_nat Int.wordsize) with 32.
   destruct (Int.one_bits n).
   intros. EvalOp. 
   destruct l.
@@ -611,7 +607,7 @@ Theorem eval_shl:
   forall le a x b y,
   eval_expr ge sp e m le a (Vint x) ->
   eval_expr ge sp e m le b (Vint y) ->
-  Int.ltu y (Int.repr 32) = true ->
+  Int.ltu y Int.iwordsize = true ->
   eval_expr ge sp e m le (shl a b) (Vint (Int.shl x y)).
 Proof.
   intros until y; unfold shl; case (shift_match b); intros.
@@ -623,7 +619,7 @@ Theorem eval_shru:
   forall le a x b y,
   eval_expr ge sp e m le a (Vint x) ->
   eval_expr ge sp e m le b (Vint y) ->
-  Int.ltu y (Int.repr 32) = true ->
+  Int.ltu y Int.iwordsize = true ->
   eval_expr ge sp e m le (shru a b) (Vint (Int.shru x y)).
 Proof.
   intros until y; unfold shru; case (shift_match b); intros.
@@ -908,7 +904,7 @@ Theorem eval_shr:
   forall le a x b y,
   eval_expr ge sp e m le a (Vint x) ->
   eval_expr ge sp e m le b (Vint y) ->
-  Int.ltu y (Int.repr 32) = true ->
+  Int.ltu y Int.iwordsize = true ->
   eval_expr ge sp e m le (shr a b) (Vint (Int.shr x y)).
 Proof. intros; unfold shr; EvalOp. simpl. rewrite H1. auto. Qed.