diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2017-05-22 14:03:37 +0200 |
---|---|---|
committer | Bernhard Schommer <bschommer@users.noreply.github.com> | 2017-05-29 15:11:43 +0200 |
commit | 47f63df0a43209570de224f28cf53da6a758df16 (patch) | |
tree | d89860b525b7e0abf0fc473914707b4324f963cc /cfrontend/SimplExprproof.v | |
parent | 3a37afef5420ac20b39bfd48c2aeeac915385d5f (diff) | |
download | compcert-47f63df0a43209570de224f28cf53da6a758df16.tar.gz compcert-47f63df0a43209570de224f28cf53da6a758df16.zip |
Early optimization of redundant *& and &* addressings
Particularly annoying was the `*&x` sequence where `x` is a local variable, which would force stack-allocation of `x` early, generating extra loads and stores that could not always be optimized later (in CSE and Deadcode).
The `*&` sequences and, by symmetry, the `&*` sequences are now eliminated early during Clight generation, via smart constructors.
Diffstat (limited to 'cfrontend/SimplExprproof.v')
-rw-r--r-- | cfrontend/SimplExprproof.v | 43 |
1 files changed, 40 insertions, 3 deletions
diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v index 191a10de..d85fb271 100644 --- a/cfrontend/SimplExprproof.v +++ b/cfrontend/SimplExprproof.v @@ -97,6 +97,42 @@ Proof. intros. inv H; auto. Qed. +(** Properties of smart constructors. *) + +Lemma eval_Ederef': + forall ge e le m a t l ofs, + eval_expr ge e le m a (Vptr l ofs) -> + eval_lvalue ge e le m (Ederef' a t) l ofs. +Proof. + intros. unfold Ederef'; destruct a; auto using eval_Ederef. + destruct (type_eq t (typeof a)); auto using eval_Ederef. + inv H. +- auto. +- inv H0. +Qed. + +Lemma typeof_Ederef': + forall a t, typeof (Ederef' a t) = t. +Proof. + unfold Ederef'; intros; destruct a; auto. destruct (type_eq t (typeof a)); auto. +Qed. + +Lemma eval_Eaddrof': + forall ge e le m a t l ofs, + eval_lvalue ge e le m a l ofs -> + eval_expr ge e le m (Eaddrof' a t) (Vptr l ofs). +Proof. + intros. unfold Eaddrof'; destruct a; auto using eval_Eaddrof. + destruct (type_eq t (typeof a)); auto using eval_Eaddrof. + inv H; auto. +Qed. + +Lemma typeof_Eaddrof': + forall a t, typeof (Eaddrof' a t) = t. +Proof. + unfold Eaddrof'; intros; destruct a; auto. destruct (type_eq t (typeof a)); auto. +Qed. + (** Translation of simple expressions. *) Lemma tr_simple_nil: @@ -214,8 +250,9 @@ Opaque makeif. (* addrof *) exploit H0; eauto. intros [A [B C]]. subst sl1; simpl. - assert (eval_expr tge e le m (Eaddrof a1 ty) (Vptr b ofs)). econstructor; eauto. - destruct dst; auto. simpl; econstructor; eauto. + assert (eval_expr tge e le m (Eaddrof' a1 ty) (Vptr b ofs)) by (apply eval_Eaddrof'; auto). + assert (typeof (Eaddrof' a1 ty) = ty) by (apply typeof_Eaddrof'). + destruct dst; auto. simpl; econstructor; eauto. (* unop *) exploit H0; eauto. intros [A [B C]]. subst sl1; simpl. @@ -251,7 +288,7 @@ Opaque makeif. rewrite symbols_preserved; auto. (* deref *) exploit H0; eauto. intros [A [B C]]. subst sl1. - split; auto. split; auto. constructor; auto. + split; auto. split. rewrite typeof_Ederef'; auto. apply eval_Ederef'; auto. (* field struct *) rewrite <- comp_env_preserved in *. exploit H0; eauto. intros [A [B C]]. subst sl1. |