Module Tailcall

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.

If the current function had a non-empty stack block, it could be that the called function accesses it, for instance if a pointer into the stack block is passed as an argument. In this case, it would be semantically incorrect to deallocate the stack block before the call, as Itailcall does. Therefore, the optimization can only be performed if the stack block of the current function is empty, in which case it makes no semantic difference to deallocate it before or after the call. Another complication is that the Ireturn instruction does not, in general, follow immediately the Icall instruction: the RTL code generator can have inserted moves and no-ops between these instructions. The general pattern we recognize is therefore:

       r1 <- call(....)
       nop
       r2 <- r1
       r3 <- r2
       return r3

The 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.