Recognition of tail calls.

Require Import Coqlib Maps AST Registers Op RTL Conventions.

An Icall instruction that stores its result in register rreg
can be turned into a tail call if:

- its successor is a Ireturn None or Ireturn (Some rreg) instruction;
- the stack block of the current function is empty: stacksize = 0.

r1 <- call(....) nop r2 <- r1 r3 <- r2 return r3The is_return function below recognizes this pattern.

Fixpoint is_return (n: nat) (f: function) (pc: node) (rret: reg)

{struct n}: bool :=

match n with

| O => false

| S n' =>

match f.(fn_code)!pc with

| Some(Ireturn None) => true

| Some(Ireturn (Some r)) => Reg.eq r rret

| Some(Inop s) => is_return n' f s rret

| Some(Iop op args dst s) =>

match is_move_operation op args with

| None => false

| Some src =>

if Reg.eq rret src

then is_return n' f s dst

else false

end

| _ => false

end

end.

To ensure termination, we bound arbitrarily the number of iterations
of the is_return function: we look ahead for a nop/move/return of length
at most niter instructions.

Definition niter := 5%nat.

The code transformation is straightforward: call instructions
followed by an appropriate nop/move/return sequence become
tail calls; other instructions are unchanged.
To ensure that the resulting RTL code is well typed, we
restrict the transformation to the cases where a tail call is
allowed by the calling conventions, and where the result signatures
match.

Definition transf_instr (f: function) (pc: node) (instr: instruction) :=

match instr with

| Icall sig ros args res s =>

if is_return niter f s res

&& tailcall_is_possible sig

&& rettype_eq sig.(sig_res) f.(fn_sig).(sig_res)

then Itailcall sig ros args

else instr

| _ => instr

end.

A function is transformed only if its stack block is empty,
as explained above.

Definition transf_function (f: function) : function :=

if zeq f.(fn_stacksize) 0

then RTL.transf_function (transf_instr f) f

else f.

Definition transf_fundef (fd: fundef) : fundef :=

AST.transf_fundef transf_function fd.

Definition transf_program (p: program) : program :=

transform_program transf_fundef p.