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

6 files changed, 53 insertions, 53 deletions

diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v
index b18ae914..07764136 100644
--- a/arm/Asmgenproof1.v
+++ b/arm/Asmgenproof1.v
@@ -1089,10 +1089,10 @@ Proof.
     simpl in H1. destruct (ms m0); try discriminate.
     exists i0; split; auto. destruct (Int.ltu i (Int.repr 31)); discriminate || auto.
   destruct H3 as [n [ARG1 LTU]].
-  assert (LTU': Int.ltu i (Int.repr 32) = true).
+  assert (LTU': Int.ltu i Int.iwordsize = true).
     exploit Int.ltu_inv. eexact LTU. intro.
     unfold Int.ltu. apply zlt_true.
-    assert (Int.unsigned (Int.repr 31) < Int.unsigned (Int.repr 32)). vm_compute; auto.
+    assert (Int.unsigned (Int.repr 31) < Int.unsigned Int.iwordsize). vm_compute; auto.
     omega.
   assert (RSm0: rs (ireg_of m0) = Vint n).
     rewrite <- ARG1. symmetry. eapply ireg_val; eauto. 
diff --git a/arm/ConstpropOp.v b/arm/ConstpropOp.v
index b5e5a03b..e55c7f99 100644
--- a/arm/ConstpropOp.v
+++ b/arm/ConstpropOp.v
@@ -174,9 +174,9 @@ Definition eval_static_operation (op: operation) (vl: list approx) :=
   | Obicshift s, I n1 :: I n2 :: nil => I(Int.and n1 (Int.not (eval_shift s n2)))
   | Onot, I n1 :: nil => I(Int.not n1)
   | Onotshift s, I n1 :: nil => I(Int.not (eval_shift s n1))
-  | 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
-  | 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
+  | Oshru, I n1 :: I n2 :: nil => if Int.ltu n2 Int.iwordsize then I(Int.shru n1 n2) else Unknown
   | Oshift s, I n1 :: nil => I(eval_shift s n1)
   | Onegf, F n1 :: nil => F(Float.neg n1)
   | Oabsf, F n1 :: nil => F(Float.abs n1)
@@ -543,11 +543,11 @@ Definition eval_static_operation (op: operation) (vl: list approx) :=
   | eval_static_operation_case36 s n1 =>
       I(Int.not (eval_shift s n1))
   | eval_static_operation_case37 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_case38 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_case39 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_case40 s n1 =>
       I(eval_shift s n1)
   | eval_static_operation_case41 n1 =>
@@ -954,7 +954,7 @@ Definition op_strength_reduction (op: operation) (args: list reg) :=
   | op_strength_reduction_case16 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)
@@ -962,7 +962,7 @@ Definition op_strength_reduction (op: operation) (args: list reg) :=
   | op_strength_reduction_case17 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)
@@ -970,7 +970,7 @@ Definition op_strength_reduction (op: operation) (args: list reg) :=
   | op_strength_reduction_case18 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/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v
index bb9caffb..b718fc26 100644
--- a/arm/ConstpropOpproof.v
+++ b/arm/ConstpropOpproof.v
@@ -130,13 +130,13 @@ Proof.
   replace n2 with i0. destruct (Int.eq i0 Int.zero). 
   discriminate. injection H0; intro; subst v. simpl. congruence. 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. 
 
-  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.
@@ -284,7 +284,7 @@ Proof.
      with (eval_operation ge sp Oshl (rs # r :: Vint i :: nil)).
   apply make_shlimm_correct. 
   simpl. generalize (Int.is_power2_range _ _ H2). 
-  change (Z_of_nat wordsize) with 32. intro. rewrite H3.
+  change (Z_of_nat Int.wordsize) with 32. intro. rewrite H3.
   destruct rs#r; auto. rewrite (Int.mul_pow2 i0 _ _ H2). auto.
   simpl List.map. rewrite H. auto.
 Qed.
@@ -400,7 +400,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. 
@@ -474,19 +474,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/arm/Op.v b/arm/Op.v
index 47cbc0ce..da9903bd 100644
--- a/arm/Op.v
+++ b/arm/Op.v
@@ -37,7 +37,7 @@ Set Implicit Arguments.
 Record shift_amount : Type :=
   mk_shift_amount { 
     s_amount: int;
-    s_amount_ltu: Int.ltu s_amount (Int.repr 32) = true 
+    s_amount_ltu: Int.ltu s_amount Int.iwordsize = true 
   }.
 
 Inductive shift : Type :=
@@ -267,11 +267,11 @@ Definition eval_operation
   | Onot, Vint n1 :: nil => Some (Vint (Int.not n1))
   | Onotshift s, Vint n1 :: nil => Some (Vint (Int.not (eval_shift s n1)))
   | 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
   | 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
   | Oshift s, Vint n :: nil => Some (Vint (eval_shift s n))
   | Oshrximm n, Vint n1 :: nil =>
       if Int.ltu n (Int.repr 31) then Some (Vint (Int.shrx n1 n)) else None
@@ -548,11 +548,11 @@ 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 i0 (Int.repr 32)).
+  destruct (Int.ltu i0 Int.iwordsize).
   injection H0; intro; subst v; exact I. discriminate.
   destruct (Int.ltu i (Int.repr 31)).
   injection H0; intro; subst v; exact I. discriminate.
@@ -724,12 +724,12 @@ 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 i0 (Int.repr 32)); congruence.
+  destruct (Int.ltu i0 Int.iwordsize); congruence.
+  destruct (Int.ltu i0 Int.iwordsize); congruence.
+  destruct (Int.ltu i0 Int.iwordsize); congruence.
   unfold Int.ltu in H. destruct (zlt (Int.unsigned i) (Int.unsigned (Int.repr 31))).
   unfold Int.ltu. rewrite zlt_true. congruence. 
-  assert (Int.unsigned (Int.repr 31) < Int.unsigned (Int.repr 32)). vm_compute; auto.
+  assert (Int.unsigned (Int.repr 31) < Int.unsigned Int.iwordsize). vm_compute; auto.
   omega. discriminate.
   caseEq (eval_condition c vl); intros; rewrite H0 in H.
   replace v with (Val.of_bool b).
@@ -825,11 +825,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 i0 (Int.repr 32)); inv H1; TrivialExists.
-  destruct (Int.ltu i0 (Int.repr 32)); inv H1; 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 i0 Int.iwordsize); inv H1; TrivialExists.
+  destruct (Int.ltu i0 Int.iwordsize); inv H1; TrivialExists.
   destruct (Int.ltu i (Int.repr 31)); inv H0; TrivialExists.
   exists (Val.singleoffloat v2); split. auto. apply Val.singleoffloat_lessdef; auto.
   caseEq (eval_condition c vl1); intros. rewrite H1 in H0. 
@@ -853,10 +853,10 @@ End EVAL_LESSDEF.
 (** Recognition of integers that are valid shift amounts. *)
 
 Definition is_shift_amount_aux (n: int) :
-  { Int.ltu n (Int.repr 32) = true } +
-  { Int.ltu n (Int.repr 32) = false }.
+  { Int.ltu n Int.iwordsize = true } +
+  { Int.ltu n Int.iwordsize = false }.
 Proof.
-  intro. case (Int.ltu n (Int.repr 32)). left; auto. right; auto.
+  intro. case (Int.ltu n Int.iwordsize). left; auto. right; auto.
 Defined.
 
 Definition is_shift_amount (n: int) : option shift_amount :=
@@ -875,7 +875,7 @@ Proof.
 Qed.
 
 Lemma is_shift_amount_None:
-  forall n, is_shift_amount n = None -> Int.ltu n (Int.repr 32) = true -> False.
+  forall n, is_shift_amount n = None -> Int.ltu n Int.iwordsize = true -> False.
 Proof.
   intro n. unfold is_shift_amount.
   destruct (is_shift_amount_aux n). 
diff --git a/arm/SelectOp.v b/arm/SelectOp.v
index 4b5fde7f..abf39aff 100644
--- a/arm/SelectOp.v
+++ b/arm/SelectOp.v
@@ -385,7 +385,7 @@ Definition shlimm (e1: expr) :=
   if Int.eq n Int.zero then e1 else 
   match e1 with
   | Eop (Ointconst n1) Enil => Eop (Ointconst(Int.shl n1 n))
-  | Eop (Oshift (Olsl n1)) (t1:::Enil) => if Int.ltu (Int.add n n1) (Int.repr 32) then Eop (Oshift (Olsl (Int.add n n1))) (t1:::Enil) else Eop (Oshift (Olsl n)) (e1:::Enil)
+  | Eop (Oshift (Olsl n1)) (t1:::Enil) => if Int.ltu (Int.add n n1) Int.iwordsize then Eop (Oshift (Olsl (Int.add n n1))) (t1:::Enil) else Eop (Oshift (Olsl n)) (e1:::Enil)
   | _ => Eop (Oshift (Olsl n)) (e1:::Enil)
   end.
 *)
@@ -436,7 +436,7 @@ Definition shruimm (e1: expr) :=
   if Int.eq n Int.zero then e1 else
   match e1 with
   | Eop (Ointconst n1) Enil => Eop (Ointconst(Int.shru n1 n))
-  | Eop (Oshift (Olsr n1)) (t1:::Enil) => if Int.ltu (Int.add n n1) (Int.repr 32) then Eop (Oshift (Olsr (Int.add n n1))) (t1:::Enil) else Eop (Oshift (Olsr n)) (e1:::Enil)
+  | Eop (Oshift (Olsr n1)) (t1:::Enil) => if Int.ltu (Int.add n n1) Int.iwordsize then Eop (Oshift (Olsr (Int.add n n1))) (t1:::Enil) else Eop (Oshift (Olsr n)) (e1:::Enil)
   | _ => Eop (Oshift (Olsr n)) (e1:::Enil)
   end.
 *)
@@ -486,7 +486,7 @@ Definition shruimm (e1: expr) (n: int) :=
 Definition shrimm (e1: expr) :=
   match e1 with
   | Eop (Ointconst n1) Enil => Eop (Ointconst(Int.shr n1 n))
-  | Eop (Oshift (Oasr n1)) (t1:::Enil) => if Int.ltu (Int.add n n1) (Int.repr 32) then Eop (Oshift (Oasr (Int.add n n1))) (t1:::Enil) else Eop (Oshift (Oasr n)) (e1:::Enil)
+  | Eop (Oshift (Oasr n1)) (t1:::Enil) => if Int.ltu (Int.add n n1) Int.iwordsize then Eop (Oshift (Oasr (Int.add n n1))) (t1:::Enil) else Eop (Oshift (Oasr n)) (e1:::Enil)
   | _ => Eop (Oshift (Oasr n)) (e1:::Enil)
   end.
 *)
@@ -825,7 +825,7 @@ Definition or_match (e1: expr) (e2: expr) :=
 Definition or (e1: expr) (e2: expr) :=
   match or_match e1 e2 with
   | or_case1 n1 t1 n2 t2 =>
-      if Int.eq (Int.add (s_amount n1) (s_amount n2)) (Int.repr 32)
+      if Int.eq (Int.add (s_amount n1) (s_amount n2)) Int.iwordsize
       && same_expr_pure t1 t2
       then Eop (Oshift (Sror n2)) (t1:::Enil)
       else Eop (Oorshift (Slsr n2)) (e1:::t2:::Enil)
diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v
index 68b49fd8..32aba30c 100644
--- a/arm/SelectOpproof.v
+++ b/arm/SelectOpproof.v
@@ -342,7 +342,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 until x.  unfold shlimm, is_shift_amount.
@@ -365,7 +365,7 @@ 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 until x.  unfold shruimm, is_shift_amount.
@@ -388,7 +388,7 @@ Qed.
 Theorem eval_shrimm:
   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 (shrimm a n) (Vint (Int.shr x n)).
 Proof.
   intros until x.  unfold shrimm, is_shift_amount.
@@ -416,7 +416,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. constructor. EvalOp. simpl; reflexivity.
   constructor. eauto. constructor. simpl. rewrite Int.mul_commut. auto.
@@ -497,7 +497,7 @@ Proof.
   rewrite (Int.divs_pow2 x y i H0). auto.
   exploit Int.ltu_inv; eauto. 
   change (Int.unsigned (Int.repr 31)) with 31.
-  change (Int.unsigned (Int.repr 32)) with 32.
+  change (Int.unsigned Int.iwordsize) with 32.
   omega.
   apply eval_divs_base. auto. EvalOp. auto.
   apply eval_divs_base. auto. EvalOp. auto.
@@ -634,10 +634,10 @@ Lemma eval_or:
   eval_expr ge sp e m le (or a b) (Vint (Int.or x y)).
 Proof.
   intros until y; unfold or; case (or_match a b); intros; InvEval.
-  caseEq (Int.eq (Int.add (s_amount n1) (s_amount n2)) (Int.repr 32)
+  caseEq (Int.eq (Int.add (s_amount n1) (s_amount n2)) Int.iwordsize
           && same_expr_pure t1 t2); intro.
   destruct (andb_prop _ _ H1).
-  generalize (Int.eq_spec (Int.add (s_amount n1) (s_amount n2)) (Int.repr 32)).
+  generalize (Int.eq_spec (Int.add (s_amount n1) (s_amount n2)) Int.iwordsize).
   rewrite H4. intro. 
   exploit eval_same_expr; eauto. intros [EQ1 EQ2]. inv EQ1. inv EQ2. 
   simpl. EvalOp. simpl. decEq. decEq. apply Int.or_ror.
@@ -666,7 +666,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.
@@ -678,7 +678,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.
@@ -690,7 +690,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 until y; unfold shr; case (shift_match b); intros.