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.

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)