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

1 files changed, 2 insertions, 3 deletions

diff --git a/backend/RTLgen.v b/backend/RTLgen.v
index 942dc50..ff4f81c 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;