From 0cb770c9d2dcad16afdd8129558e356f31202803 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 2 May 2010 07:43:49 +0000 Subject: In compilation of Sassign, avoid systematic move from a fresh temp. Those moves are not always coalesced during coloring. The resulting smaller RTL code also reduces the load on the rest of the back-end. RTLgenspec.v: use spiffy saturateTrans tactic to speed up proof search. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1330 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/RTLgen.v | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'backend/RTLgen.v') diff --git a/backend/RTLgen.v b/backend/RTLgen.v index 942dc50b..ff4f81c5 100644 --- a/backend/RTLgen.v +++ b/backend/RTLgen.v @@ -524,9 +524,8 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node) | Sskip => ret nd | Sassign v b => - do rt <- alloc_reg map b; - do no <- store_var map rt v nd; - transl_expr map b rt no + do r <- find_var map v; + transl_expr map b r nd | Sstore chunk addr al b => do rl <- alloc_regs map al; do r <- alloc_reg map b; -- cgit