From 47f63df0a43209570de224f28cf53da6a758df16 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 22 May 2017 14:03:37 +0200 Subject: 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. --- cfrontend/SimplExpr.v | 18 ++++++++++++++++-- cfrontend/SimplExprproof.v | 43 ++++++++++++++++++++++++++++++++++++++++--- cfrontend/SimplExprspec.v | 6 +++--- 3 files changed, 59 insertions(+), 8 deletions(-) diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v index a5306b4b..0a191f29 100644 --- a/cfrontend/SimplExpr.v +++ b/cfrontend/SimplExpr.v @@ -121,6 +121,20 @@ Function makeif (a: expr) (s1 s2: statement) : statement := | None => Sifthenelse a s1 s2 end. +(** Smart constructors for [&] and [*]. They optimize away [&*] and [*&] sequences. *) + +Definition Ederef' (a: expr) (t: type) : expr := + match a with + | Eaddrof a' t' => if type_eq t (typeof a') then a' else Ederef a t + | _ => Ederef a t + end. + +Definition Eaddrof' (a: expr) (t: type) : expr := + match a with + | Ederef a' t' => if type_eq t (typeof a') then a' else Eaddrof a t + | _ => Eaddrof a t + end. + (** Translation of pre/post-increment/decrement. *) Definition transl_incrdecr (id: incr_or_decr) (a: expr) (ty: type) : expr := @@ -220,7 +234,7 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement ret (finish dst nil (Evar x ty)) | Csyntax.Ederef r ty => do (sl, a) <- transl_expr For_val r; - ret (finish dst sl (Ederef a ty)) + ret (finish dst sl (Ederef' a ty)) | Csyntax.Efield r f ty => do (sl, a) <- transl_expr For_val r; ret (finish dst sl (Efield a f ty)) @@ -244,7 +258,7 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement ret (finish dst (sl1 ++ sl2) a2) | Csyntax.Eaddrof l ty => do (sl, a) <- transl_expr For_val l; - ret (finish dst sl (Eaddrof a ty)) + ret (finish dst sl (Eaddrof' a ty)) | Csyntax.Eunop op r1 ty => do (sl1, a1) <- transl_expr For_val r1; ret (finish dst sl1 (Eunop op a1 ty)) 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. diff --git a/cfrontend/SimplExprspec.v b/cfrontend/SimplExprspec.v index e317a728..37e2cd96 100644 --- a/cfrontend/SimplExprspec.v +++ b/cfrontend/SimplExprspec.v @@ -55,7 +55,7 @@ Inductive tr_expr: temp_env -> destination -> Csyntax.expr -> list statement -> | tr_deref: forall le dst e1 ty sl1 a1 tmp, tr_expr le For_val e1 sl1 a1 tmp -> tr_expr le dst (Csyntax.Ederef e1 ty) - (sl1 ++ final dst (Ederef a1 ty)) (Ederef a1 ty) tmp + (sl1 ++ final dst (Ederef' a1 ty)) (Ederef' a1 ty) tmp | tr_field: forall le dst e1 f ty sl1 a1 tmp, tr_expr le For_val e1 sl1 a1 tmp -> tr_expr le dst (Csyntax.Efield e1 f ty) @@ -94,8 +94,8 @@ Inductive tr_expr: temp_env -> destination -> Csyntax.expr -> list statement -> | tr_addrof: forall le dst e1 ty tmp sl1 a1, tr_expr le For_val e1 sl1 a1 tmp -> tr_expr le dst (Csyntax.Eaddrof e1 ty) - (sl1 ++ final dst (Eaddrof a1 ty)) - (Eaddrof a1 ty) tmp + (sl1 ++ final dst (Eaddrof' a1 ty)) + (Eaddrof' a1 ty) tmp | tr_unop: forall le dst op e1 ty tmp sl1 a1, tr_expr le For_val e1 sl1 a1 tmp -> tr_expr le dst (Csyntax.Eunop op e1 ty) -- cgit