diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-08-18 09:06:55 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-08-18 09:06:55 +0000 |
commit | a15858a0a8fcea82db02fe8c9bd2ed912210419f (patch) | |
tree | 5c0c19439f0d0f9e8873ce0dad2034cb9cafc4ba /backend/RTLgen.v | |
parent | adedca3a1ff17ff8ac66eb2bcd533a50df0927a0 (diff) | |
download | compcert-a15858a0a8fcea82db02fe8c9bd2ed912210419f.tar.gz compcert-a15858a0a8fcea82db02fe8c9bd2ed912210419f.zip |
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
Diffstat (limited to 'backend/RTLgen.v')
-rw-r--r-- | backend/RTLgen.v | 40 |
1 files changed, 17 insertions, 23 deletions
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 |