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
|
(* *********************************************************************)
(* *)
(* 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. *)
(* *)
(* *********************************************************************)
(** Predictor for return addresses in generated PPC code.
The [return_address_offset] predicate defined here is used in the
semantics for Mach (module [Machsem]) to determine the
return addresses that are stored in activation records. *)
Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Memory.
Require Import Globalenvs.
Require Import Op.
Require Import Locations.
Require Import Mach.
Require Import Asm.
Require Import Asmgen.
(** The ``code tail'' of an instruction list [c] is the list of instructions
starting at PC [pos]. *)
Inductive code_tail: Z -> code -> code -> Prop :=
| code_tail_0: forall c,
code_tail 0 c c
| code_tail_S: forall pos i c1 c2,
code_tail pos c1 c2 ->
code_tail (pos + 1) (i :: c1) c2.
Lemma code_tail_pos:
forall pos c1 c2, code_tail pos c1 c2 -> pos >= 0.
Proof.
induction 1. omega. omega.
Qed.
(** Consider a Mach function [f] and a sequence [c] of Mach instructions
representing the Mach code that remains to be executed after a
function call returns. The predicate [return_address_offset f c ofs]
holds if [ofs] is the integer offset of the PPC instruction
following the call in the PPC code obtained by translating the
code of [f]. Graphically:
<<
Mach function f |--------- Mcall ---------|
Mach code c | |--------|
| \ \
| \ \
| \ \
PPC code | |--------|
PPC function |--------------- Pbl ---------|
<-------- ofs ------->
>>
*)
Inductive return_address_offset: Mach.function -> Mach.code -> int -> Prop :=
| return_address_offset_intro:
forall c f ofs,
code_tail ofs (transl_function f) (transl_code f c) ->
return_address_offset f c (Int.repr ofs).
(** We now show that such an offset always exists if the Mach code [c]
is a suffix of [f.(fn_code)]. This holds because the translation
from Mach to PPC is compositional: each Mach instruction becomes
zero, one or several PPC instructions, but the order of instructions
is preserved. *)
Lemma is_tail_code_tail:
forall c1 c2, is_tail c1 c2 -> exists ofs, code_tail ofs c2 c1.
Proof.
induction 1. exists 0; constructor.
destruct IHis_tail as [ofs CT]. exists (ofs + 1); constructor; auto.
Qed.
Hint Resolve is_tail_refl: ppcretaddr.
Ltac IsTail :=
auto with ppcretaddr;
match goal with
| [ |- is_tail _ (_ :: _) ] => constructor; IsTail
| [ |- is_tail _ (match ?x with true => _ | false => _ end) ] => destruct x; IsTail
| [ |- is_tail _ (match ?x with left _ => _ | right _ => _ end) ] => destruct x; IsTail
| [ |- is_tail _ (match ?x with nil => _ | _ :: _ => _ end) ] => destruct x; IsTail
| [ |- is_tail _ (match ?x with Tint => _ | Tfloat => _ end) ] => destruct x; IsTail
| [ |- is_tail _ (?f _ _ _ _ _ _ ?k) ] => apply is_tail_trans with k; IsTail
| [ |- is_tail _ (?f _ _ _ _ _ ?k) ] => apply is_tail_trans with k; IsTail
| [ |- is_tail _ (?f _ _ _ _ ?k) ] => apply is_tail_trans with k; IsTail
| [ |- is_tail _ (?f _ _ _ ?k) ] => apply is_tail_trans with k; IsTail
| [ |- is_tail _ (?f _ _ ?k) ] => apply is_tail_trans with k; IsTail
| _ => idtac
end.
Lemma loadimm_tail:
forall r n k, is_tail k (loadimm r n k).
Proof. unfold loadimm; intros; IsTail. Qed.
Hint Resolve loadimm_tail: ppcretaddr.
Lemma addimm_tail:
forall r1 r2 n k, is_tail k (addimm r1 r2 n k).
Proof. unfold addimm; intros; IsTail. Qed.
Hint Resolve addimm_tail: ppcretaddr.
Lemma andimm_base_tail:
forall r1 r2 n k, is_tail k (andimm_base r1 r2 n k).
Proof. unfold andimm_base; intros; IsTail. Qed.
Hint Resolve andimm_base_tail: ppcretaddr.
Lemma andimm_tail:
forall r1 r2 n k, is_tail k (andimm r1 r2 n k).
Proof. unfold andimm; intros; IsTail. Qed.
Hint Resolve andimm_tail: ppcretaddr.
Lemma orimm_tail:
forall r1 r2 n k, is_tail k (orimm r1 r2 n k).
Proof. unfold orimm; intros; IsTail. Qed.
Hint Resolve orimm_tail: ppcretaddr.
Lemma xorimm_tail:
forall r1 r2 n k, is_tail k (xorimm r1 r2 n k).
Proof. unfold xorimm; intros; IsTail. Qed.
Hint Resolve xorimm_tail: ppcretaddr.
Lemma rolm_tail:
forall r1 r2 amount mask k, is_tail k (rolm r1 r2 amount mask k).
Proof. unfold rolm; intros; IsTail. Qed.
Hint Resolve rolm_tail: ppcretaddr.
Lemma loadind_tail:
forall base ofs ty dst k, is_tail k (loadind base ofs ty dst k).
Proof. unfold loadind; intros. destruct ty; IsTail. Qed.
Hint Resolve loadind_tail: ppcretaddr.
Lemma storeind_tail:
forall src base ofs ty k, is_tail k (storeind src base ofs ty k).
Proof. unfold storeind; intros. destruct ty; IsTail. Qed.
Hint Resolve storeind_tail: ppcretaddr.
Lemma floatcomp_tail:
forall cmp r1 r2 k, is_tail k (floatcomp cmp r1 r2 k).
Proof. unfold floatcomp; intros; destruct cmp; IsTail. Qed.
Hint Resolve floatcomp_tail: ppcretaddr.
Lemma transl_cond_tail:
forall cond args k, is_tail k (transl_cond cond args k).
Proof. unfold transl_cond; intros; destruct cond; IsTail. Qed.
Hint Resolve transl_cond_tail: ppcretaddr.
Lemma transl_cond_op_tail:
forall cond args r k, is_tail k (transl_cond_op cond args r k).
Proof.
unfold transl_cond_op; intros.
destruct (classify_condition cond args); IsTail.
Qed.
Hint Resolve transl_cond_op_tail: ppcretaddr.
Lemma transl_op_tail:
forall op args r k, is_tail k (transl_op op args r k).
Proof.
unfold transl_op; intros; destruct op; IsTail.
Qed.
Hint Resolve transl_op_tail: ppcretaddr.
Lemma transl_load_store_tail:
forall mk1 mk2 addr args temp k,
is_tail k (transl_load_store mk1 mk2 addr args temp k).
Proof. unfold transl_load_store; intros; destruct addr; IsTail. Qed.
Hint Resolve transl_load_store_tail: ppcretaddr.
Lemma transl_instr_tail:
forall f i k, is_tail k (transl_instr f i k).
Proof.
unfold transl_instr; intros; destruct i; IsTail.
destruct m; IsTail.
destruct m; IsTail.
destruct s0; IsTail.
destruct s0; IsTail.
Qed.
Hint Resolve transl_instr_tail: ppcretaddr.
Lemma transl_code_tail:
forall f c1 c2, is_tail c1 c2 -> is_tail (transl_code f c1) (transl_code f c2).
Proof.
induction 1; simpl. constructor. eapply is_tail_trans; eauto with ppcretaddr.
Qed.
Lemma return_address_exists:
forall f sg ros c, is_tail (Mcall sg ros :: c) f.(fn_code) ->
exists ra, return_address_offset f c ra.
Proof.
intros. assert (is_tail (transl_code f c) (transl_function f)).
unfold transl_function. IsTail. apply transl_code_tail; eauto with coqlib.
destruct (is_tail_code_tail _ _ H0) as [ofs A].
exists (Int.repr ofs). constructor. auto.
Qed.
|
