diff options
Diffstat (limited to 'backend/RTLgen.v')
| -rw-r--r-- | backend/RTLgen.v | 41 |
1 files changed, 10 insertions, 31 deletions
diff --git a/backend/RTLgen.v b/backend/RTLgen.v index 007191a..f5e34e4 100644 --- a/backend/RTLgen.v +++ b/backend/RTLgen.v @@ -362,18 +362,6 @@ Fixpoint alloc_regs (map: mapping) (al: exprlist) ret (r :: rl) end. -(** A variant of [alloc_regs] for two-address instructions: - reuse the result register as destination for the first argument. *) - -Definition alloc_regs_2addr (map: mapping) (al: exprlist) (rd: reg) - : mon (list reg) := - match al with - | Enil => - ret nil - | Econs a bl => - do rl <- alloc_regs map bl; ret (rd :: 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. *) @@ -406,9 +394,7 @@ Fixpoint transl_expr (map: mapping) (a: expr) (rd: reg) (nd: node) | Evar v => do r <- find_var map v; add_move r rd nd | Eop op al => - do rl <- if two_address_op op - then alloc_regs_2addr map al rd - else alloc_regs map al; + do rl <- alloc_regs map al; do no <- add_instr (Iop op rl rd nd); transl_exprlist map al rl no | Eload chunk addr al => @@ -427,6 +413,14 @@ Fixpoint transl_expr (map: mapping) (a: expr) (rd: reg) (nd: node) transl_expr map b r nc | Eletvar n => do r <- find_letvar map n; add_move r rd nd + | Ebuiltin ef al => + do rl <- alloc_regs map al; + do no <- add_instr (Ibuiltin ef rl rd nd); + transl_exprlist map al rl no + | Eexternal id sg al => + do rl <- alloc_regs map al; + do no <- add_instr (Icall sg (inr id) rl rd nd); + transl_exprlist map al rl no end (** Translation of a list of expressions. The expressions are evaluated @@ -495,16 +489,6 @@ Fixpoint transl_switch (r: reg) (nexits: list node) (t: comptree) add_instr (Iop op (r :: nil) rt n3) end. -(** Detect a two-address operator at the top of an expression. *) - -Fixpoint expr_is_2addr_op (e: expr) : bool := - match e with - | Eop op _ => two_address_op op - | Econdition cond el e2 e3 => expr_is_2addr_op e2 || expr_is_2addr_op e3 - | Elet e1 e2 => expr_is_2addr_op e2 - | _ => false - end. - (** Translation of statements. [transl_stmt map s nd nexits nret rret] enriches the current CFG with the RTL instructions necessary to execute the CminorSel statement [s], and returns the node of the first @@ -524,12 +508,7 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node) ret nd | Sassign v b => do r <- find_var map v; - if expr_is_2addr_op b then - do rd <- new_reg; - do n1 <- add_move rd r nd; - transl_expr map b rd n1 - else - transl_expr map b r nd + transl_expr map b r nd | Sstore chunk addr al b => do rl <- alloc_regs map al; do r <- alloc_reg map b; |