Merge of branches/full-expr-4:

- Csyntax, Csem: source C language has side-effects within expressions,
  performs implicit casts, and has nondeterministic reduction semantics
  for expressions
- Cstrategy: deterministic red. sem. for the above
- Clight: the previous source C language, with pure expressions.
  Added: temporary variables + implicit casts.
- New pass SimplExpr to pull side-effects out of expressions
  (previously done in untrusted Caml code in cparser/)
- Csharpminor: added temporary variables to match Clight.
- Cminorgen: adapted, removed cast optimization (moved to back-end)
- CastOptim: RTL-level optimization of casts
- cparser: transformations Bitfields, StructByValue and StructAssign
  now work on non-simplified expressions
- Added pretty-printers for several intermediate languages,
  and matching -dxxx command-line flags.



git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1467 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 17 insertions, 23 deletions

diff --git a/backend/RTLgen.v b/backend/RTLgen.v
index aec2c86..b728829 100644
--- a/backend/RTLgen.v
+++ b/backend/RTLgen.v
@@ -363,6 +363,16 @@ Fixpoint alloc_regs (map: mapping) (al: exprlist)
       ret (r :: rl)
   end.
 
+(** [alloc_optreg] is used for function calls.  If a destination is
+  specified for the call, it is returned.  Otherwise, a fresh
+  register is returned. *)
+
+Definition alloc_optreg (map: mapping) (dest: option ident) : mon reg :=
+  match dest with
+  | Some id => find_var map id
+  | None => new_reg
+  end.
+
 (** * RTL generation **)
 
 (** Insertion of a register-to-register move instruction. *)
@@ -440,20 +450,6 @@ with transl_exprlist (map: mapping) (al: exprlist) (rl: list reg) (nd: node)
       error (Errors.msg "RTLgen.transl_exprlist")
   end.
 
-(** Generation of code for variable assignments. *)
-
-Definition store_var
-       (map: mapping) (rs: reg) (id: ident) (nd: node) : mon node :=
-  do rv <- find_var map id;
-  add_move rs rv nd.
-
-Definition store_optvar
-       (map: mapping) (rs: reg) (optid: option ident) (nd: node) : mon node :=
-  match optid with
-  | None => ret nd
-  | Some id => store_var map rs id nd
-  end.
-
 (** Auxiliary for branch prediction.  When compiling an if/then/else
   statement, we have a choice between translating the ``then'' branch
   first or the ``else'' branch first.  Linearization of RTL control-flow
@@ -535,11 +531,10 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node)
   | Scall optid sig b cl =>
       do rf <- alloc_reg map b;
       do rargs <- alloc_regs map cl;
-      do r <- new_reg;
-      do n1 <- store_optvar map r optid nd;
-      do n2 <- add_instr (Icall sig (inl _ rf) rargs r n1);
-      do n3 <- transl_exprlist map cl rargs n2;
-         transl_expr map b rf n3
+      do r <- alloc_optreg map optid;
+      do n1 <- add_instr (Icall sig (inl _ rf) rargs r nd);
+      do n2 <- transl_exprlist map cl rargs n1;
+         transl_expr map b rf n2
   | Stailcall sig b cl =>
       do rf <- alloc_reg map b;
       do rargs <- alloc_regs map cl;
@@ -548,10 +543,9 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node)
          transl_expr map b rf n2
   | Sbuiltin optid ef al =>
       do rargs <- alloc_regs map al;
-      do r <- new_reg;
-      do n1 <- store_optvar map r optid nd;
-      do n2 <- add_instr (Ibuiltin ef rargs r n1);
-      transl_exprlist map al rargs n2
+      do r <- alloc_optreg map optid;
+      do n1 <- add_instr (Ibuiltin ef rargs r nd);
+         transl_exprlist map al rargs n1
   | Sseq s1 s2 =>
       do ns <- transl_stmt map s2 nd nexits ngoto nret rret;
       transl_stmt map s1 ns nexits ngoto nret rret