Optimisation des casts (idempotence, etc)

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

2 files changed, 121 insertions, 51 deletions

diff --git a/backend/Cmconstr.v b/backend/Cmconstr.v
index da642f8..e6168d1 100644
--- a/backend/Cmconstr.v
+++ b/backend/Cmconstr.v
@@ -187,19 +187,6 @@ Fixpoint notbool (e: expr) {struct e} : expr :=
       notbool_base e
   end.
 
-(** ** Truncations and sign extensions *)
-
-Definition cast8signed (e: expr) := Eop Ocast8signed (e ::: Enil).
-
-Definition cast8unsigned (e: expr) :=
-  Eop (Orolm Int.zero (Int.repr 255)) (e ::: Enil).
-Definition cast16signed (e: expr) :=
-  Eop Ocast16signed (e ::: Enil).
-Definition cast16unsigned (e: expr) :=
-  Eop (Orolm Int.zero (Int.repr 65535)) (e ::: Enil).
-Definition singleoffloat (e: expr) :=
-  Eop Osingleoffloat (e ::: Enil).
-
 (** ** Integer addition and pointer addition *)
 
 (*
@@ -806,6 +793,79 @@ Definition subf (e1: expr) (e2: expr) :=
 Definition mulf (e1 e2: expr) := Eop Omulf (e1:::e2:::Enil).
 Definition divf (e1 e2: expr) := Eop Odivf (e1:::e2:::Enil).
 
+(** ** Truncations and sign extensions *)
+
+Definition cast8unsigned (e: expr) :=
+  rolm e Int.zero (Int.repr 255).
+Definition cast16unsigned (e: expr) :=
+  rolm e Int.zero (Int.repr 65535).
+
+Inductive cast8signed_cases: forall (e1: expr), Set :=
+  | cast8signed_case1:
+      forall (e2: expr),
+      cast8signed_cases (Eop Ocast8signed (e2 ::: Enil))
+  | cast8signed_default:
+      forall (e1: expr),
+      cast8signed_cases e1.
+
+Definition cast8signed_match (e1: expr) :=
+  match e1 as z1 return cast8signed_cases z1 with
+  | Eop Ocast8signed (e2 ::: Enil) =>
+      cast8signed_case1 e2
+  | e1 =>
+      cast8signed_default e1
+  end.
+
+Definition cast8signed (e: expr) := 
+  match cast8signed_match e with
+  | cast8signed_case1 e1 => e
+  | cast8signed_default e1 => Eop Ocast8signed (e1 ::: Enil)
+  end.
+
+Inductive cast16signed_cases: forall (e1: expr), Set :=
+  | cast16signed_case1:
+      forall (e2: expr),
+      cast16signed_cases (Eop Ocast16signed (e2 ::: Enil))
+  | cast16signed_default:
+      forall (e1: expr),
+      cast16signed_cases e1.
+
+Definition cast16signed_match (e1: expr) :=
+  match e1 as z1 return cast16signed_cases z1 with
+  | Eop Ocast16signed (e2 ::: Enil) =>
+      cast16signed_case1 e2
+  | e1 =>
+      cast16signed_default e1
+  end.
+
+Definition cast16signed (e: expr) := 
+  match cast16signed_match e with
+  | cast16signed_case1 e1 => e
+  | cast16signed_default e1 => Eop Ocast16signed (e1 ::: Enil)
+  end.
+
+Inductive singleoffloat_cases: forall (e1: expr), Set :=
+  | singleoffloat_case1:
+      forall (e2: expr),
+      singleoffloat_cases (Eop Osingleoffloat (e2 ::: Enil))
+  | singleoffloat_default:
+      forall (e1: expr),
+      singleoffloat_cases e1.
+
+Definition singleoffloat_match (e1: expr) :=
+  match e1 as z1 return singleoffloat_cases z1 with
+  | Eop Osingleoffloat (e2 ::: Enil) =>
+      singleoffloat_case1 e2
+  | e1 =>
+      singleoffloat_default e1
+  end.
+
+Definition singleoffloat (e: expr) := 
+  match singleoffloat_match e with
+  | singleoffloat_case1 e1 => e
+  | singleoffloat_default e1 => Eop Osingleoffloat (e1 ::: Enil)
+  end.
+
 (** ** Comparisons and conditional expressions *)
 
 Definition cmp (c: comparison) (e1 e2: expr) :=
diff --git a/backend/Cmconstrproof.v b/backend/Cmconstrproof.v
index b7469be..f27fa73 100644
--- a/backend/Cmconstrproof.v
+++ b/backend/Cmconstrproof.v
@@ -329,44 +329,6 @@ Proof.
   destruct v1; eauto.
 Qed.
 
-Theorem eval_cast8signed:
-  forall sp le e1 m1 a e2 m2 x,
-  eval_expr ge sp le e1 m1 a e2 m2 (Vint x) ->
-  eval_expr ge sp le e1 m1 (cast8signed a) e2 m2 (Vint (Int.cast8signed x)).
-Proof. TrivialOp cast8signed. Qed.
-
-Theorem eval_cast8unsigned:
-  forall sp le e1 m1 a e2 m2 x,
-  eval_expr ge sp le e1 m1 a e2 m2 (Vint x) ->
-  eval_expr ge sp le e1 m1 (cast8unsigned a) e2 m2 (Vint (Int.cast8unsigned x)).
-Proof. 
-  TrivialOp cast8unsigned. simpl. 
-  rewrite Int.rolm_zero. rewrite Int.cast8unsigned_and. auto.
-Qed.
-    
-Theorem eval_cast16signed:
-  forall sp le e1 m1 a e2 m2 x,
-  eval_expr ge sp le e1 m1 a e2 m2 (Vint x) ->
-  eval_expr ge sp le e1 m1 (cast16signed a) e2 m2 (Vint (Int.cast16signed x)).
-Proof. TrivialOp cast16signed. Qed.
-
-Theorem eval_cast16unsigned:
-  forall sp le e1 m1 a e2 m2 x,
-  eval_expr ge sp le e1 m1 a e2 m2 (Vint x) ->
-  eval_expr ge sp le e1 m1 (cast16unsigned a) e2 m2 (Vint (Int.cast16unsigned x)).
-Proof. 
-  TrivialOp cast16unsigned. simpl. 
-  rewrite Int.rolm_zero. rewrite Int.cast16unsigned_and. auto.
-Qed.
-
-Theorem eval_singleoffloat:
-  forall sp le e1 m1 a e2 m2 x,
-  eval_expr ge sp le e1 m1 a e2 m2 (Vfloat x) ->
-  eval_expr ge sp le e1 m1 (singleoffloat a) e2 m2 (Vfloat (Float.singleoffloat x)).
-Proof. 
-  TrivialOp singleoffloat. 
-Qed.
-
 Theorem eval_addimm:
   forall sp le e1 m1 n a e2 m2 x,
   eval_expr ge sp le e1 m1 a e2 m2 (Vint x) ->
@@ -929,6 +891,54 @@ Theorem eval_divf:
   eval_expr ge sp le e1 m1 (divf a b) e3 m3 (Vfloat (Float.div x y)).
 Proof. TrivialOp divf. Qed.
 
+Theorem eval_cast8signed:
+  forall sp le e1 m1 a e2 m2 x,
+  eval_expr ge sp le e1 m1 a e2 m2 (Vint x) ->
+  eval_expr ge sp le e1 m1 (cast8signed a) e2 m2 (Vint (Int.cast8signed x)).
+Proof. 
+  intros until x; unfold cast8signed; case (cast8signed_match a); intros.
+  InvEval H. FuncInv. EvalOp. subst x. rewrite Int.cast8_signed_idem. reflexivity.
+  EvalOp.
+Qed.
+
+Theorem eval_cast8unsigned:
+  forall sp le e1 m1 a e2 m2 x,
+  eval_expr ge sp le e1 m1 a e2 m2 (Vint x) ->
+  eval_expr ge sp le e1 m1 (cast8unsigned a) e2 m2 (Vint (Int.cast8unsigned x)).
+Proof. 
+  intros. unfold cast8unsigned. rewrite Int.cast8unsigned_and.
+  rewrite <- Int.rolm_zero. eapply eval_rolm; eauto. 
+Qed.
+    
+Theorem eval_cast16signed:
+  forall sp le e1 m1 a e2 m2 x,
+  eval_expr ge sp le e1 m1 a e2 m2 (Vint x) ->
+  eval_expr ge sp le e1 m1 (cast16signed a) e2 m2 (Vint (Int.cast16signed x)).
+Proof. 
+  intros until x; unfold cast16signed; case (cast16signed_match a); intros.
+  InvEval H. FuncInv. EvalOp. subst x. rewrite Int.cast16_signed_idem. reflexivity.
+  EvalOp.
+Qed.
+
+Theorem eval_cast16unsigned:
+  forall sp le e1 m1 a e2 m2 x,
+  eval_expr ge sp le e1 m1 a e2 m2 (Vint x) ->
+  eval_expr ge sp le e1 m1 (cast16unsigned a) e2 m2 (Vint (Int.cast16unsigned x)).
+Proof. 
+  intros. unfold cast16unsigned. rewrite Int.cast16unsigned_and.
+  rewrite <- Int.rolm_zero. eapply eval_rolm; eauto. 
+Qed.
+
+Theorem eval_singleoffloat:
+  forall sp le e1 m1 a e2 m2 x,
+  eval_expr ge sp le e1 m1 a e2 m2 (Vfloat x) ->
+  eval_expr ge sp le e1 m1 (singleoffloat a) e2 m2 (Vfloat (Float.singleoffloat x)).
+Proof. 
+  intros until x; unfold singleoffloat; case (singleoffloat_match a); intros.
+  InvEval H. FuncInv. EvalOp. subst x. rewrite Float.singleoffloat_idem. reflexivity.
+  EvalOp.
+Qed.
+
 Theorem eval_cmp:
   forall sp le c e1 m1 a e2 m2 x b e3 m3 y,
   eval_expr ge sp le e1 m1 a e2 m2 (Vint x) ->