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
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
|
(* *********************************************************************)
(* *)
(* 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. *)
(* *)
(* *********************************************************************)
(** Function calling conventions and other conventions regarding the use of
machine registers and stack slots. *)
Require Import Coqlib.
Require Import AST.
Require Import Locations.
Require Export Conventions1.
(** The processor-dependent and EABI-dependent definitions are in
[arch/abi/Conventions1.v]. This file adds various processor-independent
definitions and lemmas. *)
(** * Acceptable locations for register allocation *)
(** The following predicate describes the locations that can be assigned
to an RTL pseudo-register during register allocation: a non-temporary
machine register or a [Local] stack slot are acceptable. *)
Definition loc_acceptable (l: loc) : Prop :=
match l with
| R r => ~(In l temporaries)
| S (Local ofs ty) => ofs >= 0
| S (Incoming _ _) => False
| S (Outgoing _ _) => False
end.
Definition locs_acceptable (ll: list loc) : Prop :=
forall l, In l ll -> loc_acceptable l.
Lemma temporaries_not_acceptable:
forall l, loc_acceptable l -> Loc.notin l temporaries.
Proof.
unfold loc_acceptable; destruct l.
simpl. intuition congruence.
destruct s; try contradiction.
intro. simpl. tauto.
Qed.
Hint Resolve temporaries_not_acceptable: locs.
Lemma locs_acceptable_disj_temporaries:
forall ll, locs_acceptable ll -> Loc.disjoint ll temporaries.
Proof.
intros. apply Loc.notin_disjoint. intros.
apply temporaries_not_acceptable. auto.
Qed.
Lemma loc_acceptable_noteq_diff:
forall l1 l2,
loc_acceptable l1 -> l1 <> l2 -> Loc.diff l1 l2.
Proof.
unfold loc_acceptable, Loc.diff; destruct l1; destruct l2;
try (destruct s); try (destruct s0); intros; auto; try congruence.
case (zeq z z0); intro.
compare t t0; intro.
subst z0; subst t0; tauto.
tauto. tauto.
contradiction. contradiction.
Qed.
Lemma loc_acceptable_notin_notin:
forall r ll,
loc_acceptable r ->
~(In r ll) -> Loc.notin r ll.
Proof.
induction ll; simpl; intros.
auto.
split. apply loc_acceptable_noteq_diff. assumption.
apply sym_not_equal. tauto.
apply IHll. assumption. tauto.
Qed.
(** * Additional properties of result and argument locations *)
(** The result location is not a callee-save register. *)
Lemma loc_result_not_callee_save:
forall (s: signature),
~(In (loc_result s) int_callee_save_regs \/ In (loc_result s) float_callee_save_regs).
Proof.
intros. generalize (loc_result_caller_save s).
generalize (int_callee_save_not_destroyed (loc_result s)).
generalize (float_callee_save_not_destroyed (loc_result s)).
tauto.
Qed.
(** Callee-save registers do not overlap with argument locations. *)
Lemma arguments_not_preserved:
forall sig l,
Loc.notin l destroyed_at_call -> loc_acceptable l ->
Loc.notin l (loc_arguments sig).
Proof.
intros. destruct l; red in H0.
apply Loc.reg_notin. red; intros.
exploit Loc.notin_not_in; eauto. eapply arguments_caller_save; eauto.
destruct s; try contradiction.
unfold loc_arguments. apply loc_arguments_rec_notin_local.
Qed.
(** There is no partial overlap between arguments and acceptable locations. *)
Lemma no_overlap_arguments:
forall args sg,
locs_acceptable args ->
Loc.no_overlap args (loc_arguments sg).
Proof.
unfold Loc.no_overlap; intros.
generalize (H r H0).
generalize (loc_arguments_acceptable _ _ H1).
destruct s; destruct r; simpl.
intros. case (mreg_eq m0 m); intro. left; congruence. tauto.
intros. right; destruct s; auto.
intros. right. auto.
destruct s; try tauto. destruct s0; tauto.
Qed.
(** ** Location of function parameters *)
(** A function finds the values of its parameter in the same locations
where its caller stored them, except that the stack-allocated arguments,
viewed as [Outgoing] slots by the caller, are accessed via [Incoming]
slots (at the same offsets and types) in the callee. *)
Definition parameter_of_argument (l: loc) : loc :=
match l with
| S (Outgoing n ty) => S (Incoming n ty)
| _ => l
end.
Definition loc_parameters (s: signature) :=
List.map parameter_of_argument (loc_arguments s).
Lemma loc_parameters_type:
forall sig, List.map Loc.type (loc_parameters sig) = sig.(sig_args).
Proof.
intros. unfold loc_parameters.
rewrite list_map_compose.
rewrite <- loc_arguments_type.
apply list_map_exten.
intros. destruct x; simpl. auto.
destruct s; reflexivity.
Qed.
Lemma loc_parameters_length:
forall sg, List.length (loc_parameters sg) = List.length sg.(sig_args).
Proof.
intros. unfold loc_parameters. rewrite list_length_map.
apply loc_arguments_length.
Qed.
Lemma loc_parameters_not_temporaries:
forall sig, Loc.disjoint (loc_parameters sig) temporaries.
Proof.
intro; red; intros.
unfold loc_parameters in H.
elim (list_in_map_inv _ _ _ H). intros y [EQ IN].
generalize (loc_arguments_not_temporaries sig y x2 IN H0).
subst x1. destruct x2.
destruct y; simpl. auto. destruct s; auto.
byContradiction. generalize H0. simpl. NotOrEq.
Qed.
Lemma no_overlap_parameters:
forall params sg,
locs_acceptable params ->
Loc.no_overlap (loc_parameters sg) params.
Proof.
unfold Loc.no_overlap; intros.
unfold loc_parameters in H0.
elim (list_in_map_inv _ _ _ H0). intros t [EQ IN].
rewrite EQ.
generalize (loc_arguments_acceptable _ _ IN).
generalize (H s H1).
destruct s; destruct t; simpl.
intros. case (mreg_eq m0 m); intro. left; congruence. tauto.
intros. right; destruct s; simpl; auto.
intros; right; auto.
destruct s; try tauto. destruct s0; try tauto.
intros; simpl. tauto.
Qed.
Lemma incoming_slot_in_parameters:
forall ofs ty sg,
In (S (Incoming ofs ty)) (loc_parameters sg) ->
In (S (Outgoing ofs ty)) (loc_arguments sg).
Proof.
intros.
unfold loc_parameters in H.
change (S (Incoming ofs ty)) with (parameter_of_argument (S (Outgoing ofs ty))) in H.
exploit list_in_map_inv. eexact H. intros [x [A B]]. simpl in A.
exploit loc_arguments_acceptable; eauto. unfold loc_argument_acceptable; intros.
destruct x; simpl in A; try discriminate.
destruct s; try contradiction.
inv A. auto.
Qed.
(** * Tail calls *)
(** A tail-call is possible for a signature if the corresponding
arguments are all passed in registers. *)
Definition tailcall_possible (s: signature) : Prop :=
forall l, In l (loc_arguments s) ->
match l with R _ => True | S _ => False end.
(** Decide whether a tailcall is possible. *)
Definition tailcall_is_possible (sg: signature) : bool :=
let fix tcisp (l: list loc) :=
match l with
| nil => true
| R _ :: l' => tcisp l'
| S _ :: l' => false
end
in tcisp (loc_arguments sg).
Lemma tailcall_is_possible_correct:
forall s, tailcall_is_possible s = true -> tailcall_possible s.
Proof.
intro s. unfold tailcall_is_possible, tailcall_possible.
generalize (loc_arguments s). induction l; simpl; intros.
elim H0.
destruct a.
destruct H0. subst l0. auto. apply IHl. auto. auto. discriminate.
Qed.
(** * Counting temporaries *)
(** Given a list [tys] of types representing arguments to an operator,
[arity_ok tys] returns [true] if there are enough temporaries to
reload all arguments into temporaries. *)
Fixpoint arity_ok_rec (tys: list typ) (itmps ftmps: list mreg)
{struct tys} : bool :=
match tys with
| nil => true
| Tint :: ts =>
match itmps with
| nil => false
| it1 :: its => arity_ok_rec ts its ftmps
end
| Tfloat :: ts =>
match ftmps with
| nil => false
| ft1 :: fts => arity_ok_rec ts itmps fts
end
end.
Definition arity_ok (tys: list typ) :=
arity_ok_rec tys int_temporaries float_temporaries.
|
