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/SimplExpr.v | |
| parent | 3a37afef5420ac20b39bfd48c2aeeac915385d5f (diff) | |
| download | compcert-kvx-47f63df0a43209570de224f28cf53da6a758df16.tar.gz compcert-kvx-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/SimplExpr.v')
| -rw-r--r-- | cfrontend/SimplExpr.v | 18 |
1 files changed, 16 insertions, 2 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)) |