From a15858a0a8fcea82db02fe8c9bd2ed912210419f Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 18 Aug 2010 09:06:55 +0000 Subject: 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 --- backend/RTLgen.v | 40 +++++++++++++++++----------------------- 1 file changed, 17 insertions(+), 23 deletions(-) (limited to 'backend/RTLgen.v') diff --git a/backend/RTLgen.v b/backend/RTLgen.v index aec2c867..b728829f 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 -- cgit