blob: bdc4c8b65fa9c7323147563de85f2ec058d40712 (
plain)
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
|
(* *********************************************************************)
(* *)
(* 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. *)
Lemma loc_arguments_acceptable_2:
forall s l,
In l (regs_of_rpairs (loc_arguments s)) -> loc_argument_acceptable l.
Proof.
intros until l. generalize (loc_arguments_acceptable s). generalize (loc_arguments s).
induction l0 as [ | p pl]; simpl; intros.
- contradiction.
- rewrite in_app_iff in H0. destruct H0.
exploit H; eauto. destruct p; simpl in *; intuition congruence.
apply IHpl; auto.
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 (rpair loc) :=
List.map (map_rpair parameter_of_argument) (loc_arguments s).
Lemma incoming_slot_in_parameters:
forall ofs ty sg,
In (S Incoming ofs ty) (regs_of_rpairs (loc_parameters sg)) ->
In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments sg)).
Proof.
intros.
replace (regs_of_rpairs (loc_parameters sg)) with (List.map parameter_of_argument (regs_of_rpairs (loc_arguments sg))) 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_2; eauto. unfold loc_argument_acceptable; intros.
destruct x; simpl in A; try discriminate.
destruct sl; try contradiction.
inv A. auto.
unfold loc_parameters. generalize (loc_arguments sg). induction l as [ | p l]; simpl; intros.
auto.
rewrite map_app. f_equal; auto. destruct p; auto.
Qed.
(** * Tail calls *)
(** A tail-call is possible for a signature if the corresponding
arguments are all passed in registers. *)
(** 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 (regs_of_rpairs (loc_arguments s)) ->
match l with R _ => True | S _ _ _ => False end.
(** Decide whether a tailcall is possible. *)
Definition tailcall_is_possible (sg: signature) : bool :=
List.forallb
(fun l => match l with R _ => true | S _ _ _ => false end)
(regs_of_rpairs (loc_arguments sg)).
Lemma tailcall_is_possible_correct:
forall s, tailcall_is_possible s = true -> tailcall_possible s.
Proof.
unfold tailcall_is_possible; intros. rewrite forallb_forall in H.
red; intros. apply H in H0. destruct l; [auto|discriminate].
Qed.
Lemma zero_size_arguments_tailcall_possible:
forall sg, size_arguments sg = 0 -> tailcall_possible sg.
Proof.
intros; red; intros. exploit loc_arguments_acceptable_2; eauto.
unfold loc_argument_acceptable.
destruct l; intros. auto. destruct sl; try contradiction. destruct H1.
generalize (loc_arguments_bounded _ _ _ H0).
generalize (typesize_pos ty). omega.
Qed.
|
