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/SimplExprspec.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'cfrontend/SimplExprspec.v') 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