1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
|
(* *********************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Xavier Leroy, INRIA Paris-Rocquencourt *)
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
(* under the terms of the INRIA Non-Commercial License Agreement. *)
(* *)
(* *********************************************************************)
(** Recognition of tail calls. *)
Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Globalenvs.
Require Import Registers.
Require Import Op.
Require Import RTL.
Require Import 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
&& opt_typ_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.
|
