Replace cast{8,16}{signed,unsigned} with zero_ext and sign_ext.

lib/Integers.v: added more properties for ARM port.
lib/Coqlib.v: added more properties for division and powers of 2.


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

8 files changed, 49 insertions, 44 deletions

diff --git a/backend/Cminor.v b/backend/Cminor.v
index 910eaa4..b6186f2 100644
--- a/backend/Cminor.v
+++ b/backend/Cminor.v
@@ -230,10 +230,10 @@ Definition eval_constant (sp: val) (cst: constant) : option val :=
 
 Definition eval_unop (op: unary_operation) (arg: val) : option val :=
   match op, arg with
-  | Ocast8unsigned, _ => Some (Val.cast8unsigned arg)
-  | Ocast8signed, _ => Some (Val.cast8signed arg)
-  | Ocast16unsigned, _ => Some (Val.cast16unsigned arg)
-  | Ocast16signed, _ => Some (Val.cast16signed arg)
+  | Ocast8unsigned, _ => Some (Val.zero_ext 8 arg)
+  | Ocast8signed, _ => Some (Val.sign_ext 8 arg)
+  | Ocast16unsigned, _ => Some (Val.zero_ext 16 arg)
+  | Ocast16signed, _ => Some (Val.sign_ext 16 arg)
   | Onegint, Vint n1 => Some (Vint (Int.neg n1))
   | Onotbool, Vint n1 => Some (Val.of_bool (Int.eq n1 Int.zero))
   | Onotbool, Vptr b1 n1 => Some Vfalse
diff --git a/backend/Constprop.v b/backend/Constprop.v
index e7feb10..75fb148 100644
--- a/backend/Constprop.v
+++ b/backend/Constprop.v
@@ -219,10 +219,10 @@ Definition eval_static_operation (op: operation) (vl: list approx) :=
   | Ointconst n, nil => I n
   | Ofloatconst n, nil => F n
   | Oaddrsymbol s n, nil => S s n
-  | Ocast8signed, I n1 :: nil => I(Int.cast8signed n)
-  | Ocast8unsigned, I n1 :: nil => I(Int.cast8unsigned n)
-  | Ocast16signed, I n1 :: nil => I(Int.cast16signed n)
-  | Ocast16unsigned, I n1 :: nil => I(Int.cast16unsigned n)
+  | Ocast8signed, I n1 :: nil => I(Int.sign_ext 8 n)
+  | Ocast8unsigned, I n1 :: nil => I(Int.zero_ext 8 n)
+  | Ocast16signed, I n1 :: nil => I(Int.sign_ext 16 n)
+  | Ocast16unsigned, I n1 :: nil => I(Int.zero_ext 16 n)
   | Oadd, I n1 :: I n2 :: nil => I(Int.add n1 n2)
   | Oadd, S s1 n1 :: I n2 :: nil => S s1 (Int.add n1 n2)
   | Oaddimm n, I n1 :: nil => I (Int.add n1 n)
@@ -533,9 +533,9 @@ Definition eval_static_operation (op: operation) (vl: list approx) :=
   | eval_static_operation_case4 s n =>
       S s n
   | eval_static_operation_case6 n1 =>
-      I(Int.cast8signed n1)
+      I(Int.sign_ext 8 n1)
   | eval_static_operation_case7 n1 =>
-      I(Int.cast16signed n1)
+      I(Int.sign_ext 16 n1)
   | eval_static_operation_case8 n1 n2 =>
       I(Int.add n1 n2)
   | eval_static_operation_case9 s1 n1 n2 =>
@@ -618,9 +618,9 @@ Definition eval_static_operation (op: operation) (vl: list approx) :=
       | Some b => I(if b then Int.one else Int.zero)
       end
   | eval_static_operation_case48 n1 =>
-      I(Int.cast8unsigned n1)
+      I(Int.zero_ext 8 n1)
   | eval_static_operation_case49 n1 =>
-      I(Int.cast16unsigned n1)
+      I(Int.zero_ext 16 n1)
   | eval_static_operation_case50 n1 =>
       I(Float.intuoffloat n1)
   | eval_static_operation_default op vl =>
diff --git a/backend/Op.v b/backend/Op.v
index 707bcb0..5665d72 100644
--- a/backend/Op.v
+++ b/backend/Op.v
@@ -175,10 +175,10 @@ Definition eval_operation
       | Some b => Some (Vptr b ofs)
       end
   | Oaddrstack ofs, nil => offset_sp sp ofs
-  | Ocast8signed, v1 :: nil => Some (Val.cast8signed v1)
-  | Ocast8unsigned, v1 :: nil => Some (Val.cast8unsigned v1)
-  | Ocast16signed, v1 :: nil => Some (Val.cast16signed v1)
-  | Ocast16unsigned, v1 :: nil => Some (Val.cast16unsigned v1)
+  | Ocast8signed, v1 :: nil => Some (Val.sign_ext 8 v1)
+  | Ocast8unsigned, v1 :: nil => Some (Val.zero_ext 8 v1)
+  | Ocast16signed, v1 :: nil => Some (Val.sign_ext 16 v1)
+  | Ocast16unsigned, v1 :: nil => Some (Val.zero_ext 16 v1)
   | Oadd, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.add n1 n2))
   | Oadd, Vint n1 :: Vptr b2 n2 :: nil => Some (Vptr b2 (Int.add n2 n1))
   | Oadd, Vptr b1 n1 :: Vint n2 :: nil => Some (Vptr b1 (Int.add n1 n2))
@@ -632,10 +632,10 @@ Definition eval_operation_total (sp: val) (op: operation) (vl: list val) : val :
   | Ofloatconst n, nil => Vfloat n
   | Oaddrsymbol s ofs, nil => find_symbol_offset s ofs
   | Oaddrstack ofs, nil => Val.add sp (Vint ofs)
-  | Ocast8signed, v1::nil => Val.cast8signed v1
-  | Ocast8unsigned, v1::nil => Val.cast8unsigned v1
-  | Ocast16signed, v1::nil => Val.cast16signed v1
-  | Ocast16unsigned, v1::nil => Val.cast16unsigned v1
+  | Ocast8signed, v1::nil => Val.sign_ext 8 v1
+  | Ocast8unsigned, v1::nil => Val.zero_ext 8 v1
+  | Ocast16signed, v1::nil => Val.sign_ext 16 v1
+  | Ocast16unsigned, v1::nil => Val.zero_ext 16 v1
   | Oadd, v1::v2::nil => Val.add v1 v2
   | Oaddimm n, v1::nil => Val.add v1 (Vint n)
   | Osub, v1::v2::nil => Val.sub v1 v2
@@ -843,10 +843,10 @@ Proof.
   exists v2; auto.
   destruct (Genv.find_symbol genv i); inv H0. TrivialExists.
   exists v1; auto.
-  exists (Val.cast8signed v2); split. auto. apply Val.cast8signed_lessdef; auto.
-  exists (Val.cast8unsigned v2); split. auto. apply Val.cast8unsigned_lessdef; auto.
-  exists (Val.cast16signed v2); split. auto. apply Val.cast16signed_lessdef; auto.
-  exists (Val.cast16unsigned v2); split. auto. apply Val.cast16unsigned_lessdef; auto.
+  exists (Val.sign_ext 8 v2); split. auto. apply Val.sign_ext_lessdef; auto.
+  exists (Val.zero_ext 8 v2); split. auto. apply Val.zero_ext_lessdef; auto.
+  exists (Val.sign_ext 16 v2); split. auto. apply Val.sign_ext_lessdef; auto.
+  exists (Val.zero_ext 16 v2); split. auto. apply Val.zero_ext_lessdef; auto.
   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.
diff --git a/backend/PPC.v b/backend/PPC.v
index 13c7a87..e47cba0 100644
--- a/backend/PPC.v
+++ b/backend/PPC.v
@@ -616,9 +616,9 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
   | Peqv rd r1 r2 =>
       OK (nextinstr (rs#rd <- (Val.notint (Val.xor rs#r1 rs#r2)))) m
   | Pextsb rd r1 =>
-      OK (nextinstr (rs#rd <- (Val.cast8signed rs#r1))) m
+      OK (nextinstr (rs#rd <- (Val.sign_ext 8 rs#r1))) m
   | Pextsh rd r1 =>
-      OK (nextinstr (rs#rd <- (Val.cast16signed rs#r1))) m
+      OK (nextinstr (rs#rd <- (Val.sign_ext 16 rs#r1))) m
   | Pfreeframe ofs =>
       match Mem.loadv Mint32 m (Val.add rs#GPR1 (Vint ofs)) with
       | None => Error
diff --git a/backend/PPCgen.v b/backend/PPCgen.v
index 1484a1e..faedcb1 100644
--- a/backend/PPCgen.v
+++ b/backend/PPCgen.v
@@ -80,7 +80,7 @@ Definition freg_of (r: mreg) : freg :=
 
 Definition low_u (n: int) := Int.and n (Int.repr 65535).
 Definition high_u (n: int) := Int.shru n (Int.repr 16).
-Definition low_s (n: int) := Int.cast16signed n.
+Definition low_s (n: int) := Int.sign_ext 16 n.
 Definition high_s (n: int) := Int.shru (Int.sub n (low_s n)) (Int.repr 16).
 
 (** Smart constructors for arithmetic operations involving
diff --git a/backend/PPCgenproof.v b/backend/PPCgenproof.v
index fd5843b..6db8b47 100644
--- a/backend/PPCgenproof.v
+++ b/backend/PPCgenproof.v
@@ -567,14 +567,14 @@ Qed.
 Lemma loadv_8_signed_unsigned:
   forall m a,
   Mem.loadv Mint8signed m a = 
-    option_map Val.cast8signed (Mem.loadv Mint8unsigned m a).
+    option_map (Val.sign_ext 8) (Mem.loadv Mint8unsigned m a).
 Proof.
   intros. unfold Mem.loadv. destruct a; try reflexivity.
   unfold load. rewrite (in_bounds_equiv Mint8signed Mint8unsigned).
   destruct (in_bounds m Mint8unsigned b (Int.signed i)); auto.
   simpl.
   destruct (getN 0 (Int.signed i) (contents (blocks m b))); auto.
-  simpl. rewrite Int.cast8_signed_unsigned. auto.
+  simpl. rewrite Int.sign_ext_zero_ext. auto. compute; auto. 
   auto.
 Qed.
 
diff --git a/backend/PPCgenproof1.v b/backend/PPCgenproof1.v
index ba347ea..dd142c5 100644
--- a/backend/PPCgenproof1.v
+++ b/backend/PPCgenproof1.v
@@ -95,7 +95,8 @@ Proof.
   rewrite Zmult_assoc. rewrite Zplus_comm. rewrite Z_mod_plus. auto.
   omega.
   eapply H0. apply Int.eqm_sym. apply Int.eqm_unsigned_repr. 
-  unfold low_s. unfold Int.cast16signed. 
+  unfold low_s. unfold Int.sign_ext. 
+  change (two_p 16) with 65536. change (two_p (16-1)) with 32768. 
   set (N := Int.unsigned n).
   case (zlt (N mod 65536) 32768); intro.
   apply H0 with (N - N mod 65536). auto with ints.
@@ -1273,19 +1274,19 @@ Proof.
   (* Ocast8unsigned *)
   exists (nextinstr (rs#(ireg_of res) <- (Val.rolm (ms m0) Int.zero (Int.repr 255)))).
   split. apply exec_straight_one. repeat (rewrite (ireg_val ms sp rs)); auto. reflexivity.
-  replace (Val.cast8unsigned (ms m0))
+  replace (Val.zero_ext 8 (ms m0))
       with (Val.rolm (ms m0) Int.zero (Int.repr 255)).
   auto with ppcgen. 
-  unfold Val.rolm, Val.cast8unsigned. destruct (ms m0); auto. 
-  rewrite Int.rolm_zero. rewrite Int.cast8unsigned_and. auto.
+  unfold Val.rolm, Val.zero_ext. destruct (ms m0); auto. 
+  rewrite Int.rolm_zero. rewrite Int.zero_ext_and. auto. compute; auto.
   (* Ocast16unsigned *)
   exists (nextinstr (rs#(ireg_of res) <- (Val.rolm (ms m0) Int.zero (Int.repr 65535)))).
   split. apply exec_straight_one. repeat (rewrite (ireg_val ms sp rs)); auto. reflexivity.
-  replace (Val.cast16unsigned (ms m0))
+  replace (Val.zero_ext 16 (ms m0))
       with (Val.rolm (ms m0) Int.zero (Int.repr 65535)).
   auto with ppcgen. 
-  unfold Val.rolm, Val.cast16unsigned. destruct (ms m0); auto. 
-  rewrite Int.rolm_zero. rewrite Int.cast16unsigned_and. auto.
+  unfold Val.rolm, Val.zero_ext. destruct (ms m0); auto. 
+  rewrite Int.rolm_zero. rewrite Int.zero_ext_and. auto. compute; auto.
   (* Oaddimm *)
   generalize (addimm_correct (ireg_of res) (ireg_of m0) i k rs m
                             (ireg_of_not_GPR12 m0)).
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index b779488..6d62979 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -748,40 +748,44 @@ Qed.
 Theorem eval_cast8signed:
   forall le a v,
   eval_expr ge sp e m le a v ->
-  eval_expr ge sp e m le (cast8signed a) (Val.cast8signed v).
+  eval_expr ge sp e m le (cast8signed a) (Val.sign_ext 8 v).
 Proof. 
   intros until v; unfold cast8signed; case (cast8signed_match a); intros; InvEval.
-  EvalOp. simpl. subst v. destruct v1; simpl; auto. rewrite Int.cast8_signed_idem. reflexivity.
+  EvalOp. simpl. subst v. destruct v1; simpl; auto.
+  rewrite Int.sign_ext_idem. reflexivity. compute; auto.
   EvalOp.
 Qed.
 
 Theorem eval_cast8unsigned:
   forall le a v,
   eval_expr ge sp e m le a v ->
-  eval_expr ge sp e m le (cast8unsigned a) (Val.cast8unsigned v).
+  eval_expr ge sp e m le (cast8unsigned a) (Val.zero_ext 8 v).
 Proof. 
   intros until v; unfold cast8unsigned; case (cast8unsigned_match a); intros; InvEval.
-  EvalOp. simpl. subst v. destruct v1; simpl; auto. rewrite Int.cast8_unsigned_idem. reflexivity.
+  EvalOp. simpl. subst v. destruct v1; simpl; auto.
+  rewrite Int.zero_ext_idem. reflexivity. compute; auto.
   EvalOp.
 Qed.
 
 Theorem eval_cast16signed:
   forall le a v,
   eval_expr ge sp e m le a v ->
-  eval_expr ge sp e m le (cast16signed a) (Val.cast16signed v).
+  eval_expr ge sp e m le (cast16signed a) (Val.sign_ext 16 v).
 Proof. 
   intros until v; unfold cast16signed; case (cast16signed_match a); intros; InvEval.
-  EvalOp. simpl. subst v. destruct v1; simpl; auto. rewrite Int.cast16_signed_idem. reflexivity.
+  EvalOp. simpl. subst v. destruct v1; simpl; auto.
+  rewrite Int.sign_ext_idem. reflexivity. compute; auto.
   EvalOp.
 Qed.
 
 Theorem eval_cast16unsigned:
   forall le a v,
   eval_expr ge sp e m le a v ->
-  eval_expr ge sp e m le (cast16unsigned a) (Val.cast16unsigned v).
+  eval_expr ge sp e m le (cast16unsigned a) (Val.zero_ext 16 v).
 Proof. 
   intros until v; unfold cast16unsigned; case (cast16unsigned_match a); intros; InvEval.
-  EvalOp. simpl. subst v. destruct v1; simpl; auto. rewrite Int.cast16_unsigned_idem. reflexivity.
+  EvalOp. simpl. subst v. destruct v1; simpl; auto.
+  rewrite Int.zero_ext_idem. reflexivity. compute; auto.
   EvalOp.
 Qed.