From 0899bd69f402eb68d55297afe7131dbc539b693a Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Tue, 8 Jan 2013 09:46:59 +0000
Subject: Avoid generating some obviously useless casts.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2093 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 cfrontend/SimplLocals.v      | 15 ++++++++++++++-
 cfrontend/SimplLocalsproof.v | 23 ++++++++++++++++++++++-
 2 files changed, 36 insertions(+), 2 deletions(-)

(limited to 'cfrontend')

diff --git a/cfrontend/SimplLocals.v b/cfrontend/SimplLocals.v
index 2a472f7f..18eeea29 100644
--- a/cfrontend/SimplLocals.v
+++ b/cfrontend/SimplLocals.v
@@ -39,6 +39,19 @@ Definition is_liftable_var (cenv: compilenv) (a: expr) : option ident :=
   | _ => None
   end.
 
+(** Smart constructor for casts *)
+
+Definition make_cast (a: expr) (tto: type) : expr :=
+  match classify_cast (typeof a) tto with
+  | cast_case_neutral => a
+  | cast_case_i2i I32 _ => a
+  | cast_case_f2f F64 => a
+  | cast_case_struct _ _ _ _ => a
+  | cast_case_union _ _ _ _ => a
+  | cast_case_void => a
+  | _ => Ecast a tto
+  end.
+
 (** Rewriting of expressions and statements. *)
 
 Fixpoint simpl_expr (cenv: compilenv) (a: expr) : expr :=
@@ -75,7 +88,7 @@ Fixpoint simpl_stmt (cenv: compilenv) (s: statement) : res statement :=
   | Sassign a1 a2 =>
       match is_liftable_var cenv a1 with
       | Some id =>
-          OK (Sset id (Ecast (simpl_expr cenv a2) (typeof a1)))
+          OK (Sset id (make_cast (simpl_expr cenv a2) (typeof a1)))
       | None =>
           OK (Sassign (simpl_expr cenv a1) (simpl_expr cenv a2))
       end
diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v
index e08ae49b..f58a2130 100644
--- a/cfrontend/SimplLocalsproof.v
+++ b/cfrontend/SimplLocalsproof.v
@@ -340,6 +340,27 @@ Proof.
   destruct a as [id ty]. inv H. constructor; auto. 
 Qed.
 
+(** Correctness of [make_cast] *)
+
+Lemma make_cast_correct:
+  forall e le m a v1 tto v2,
+  eval_expr tge e le m a v1 ->
+  sem_cast v1 (typeof a) tto = Some v2 ->
+  eval_expr tge e le m (make_cast a tto) v2.
+Proof.
+  intros.
+  assert (DFL: eval_expr tge e le m (Ecast a tto) v2).
+    econstructor; eauto.
+  unfold sem_cast, make_cast in *. 
+  destruct (classify_cast (typeof a) tto); auto.
+  destruct v1; inv H0; auto.
+  destruct sz2; auto. destruct v1; inv H0; auto.
+  destruct sz2; auto. destruct v1; inv H0; auto.
+  destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H0; auto.
+  destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H0; auto.
+  inv H0; auto.
+Qed.
+
 (** Preservation by assignment to lifted variable. *)
 
 Lemma match_envs_assign_lifted:
@@ -2009,7 +2030,7 @@ Proof.
   inv H.
   (* local variable *)
   econstructor; split. 
-  apply plus_one. econstructor. econstructor. eexact A. rewrite typeof_simpl_expr. eexact C.
+  apply plus_one. econstructor. eapply make_cast_correct. eexact A. rewrite typeof_simpl_expr. eexact C.
   econstructor; eauto with compat. 
   eapply match_envs_assign_lifted; eauto. eapply cast_val_is_casted; eauto.
   eapply match_cont_assign_loc; eauto. exploit me_range; eauto. omega.
-- 
cgit