blob: 5a2f2a612153406ddcb99bacb22d9faf154c1649 (
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
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
|
(* *************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Sylvain Boulmé Grenoble-INP, VERIMAG *)
(* David Monniaux CNRS, VERIMAG *)
(* Cyril Six Kalray *)
(* *)
(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *)
(* This file is distributed under the terms of the INRIA *)
(* Non-Commercial License Agreement. *)
(* *)
(* *************************************************************)
Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Values.
Require Import Memory.
Require Import Globalenvs.
Require Import Events.
Require Import Smallstep.
Require Import Op.
Require Import Locations.
Require Import Conventions.
Require Stacklayout.
Require Import Mach.
Require Import Linking.
Require Import Machblock.
(** * Tail-recursive (greedy) translation from Mach code to Machblock code *)
Inductive Machblock_inst: Type :=
| MB_label (lbl: label)
| MB_basic (bi: basic_inst)
| MB_cfi (cfi: control_flow_inst).
Definition trans_inst (i:Mach.instruction) : Machblock_inst :=
match i with
| Mcall sig ros => MB_cfi (MBcall sig ros)
| Mtailcall sig ros => MB_cfi (MBtailcall sig ros)
| Mbuiltin ef args res => MB_cfi (MBbuiltin ef args res)
| Mgoto lbl => MB_cfi (MBgoto lbl)
| Mcond cond args lbl => MB_cfi (MBcond cond args lbl)
| Mjumptable arg tbl => MB_cfi (MBjumptable arg tbl)
| Mreturn => MB_cfi (MBreturn)
| Mgetstack ofs ty dst => MB_basic (MBgetstack ofs ty dst)
| Msetstack src ofs ty => MB_basic (MBsetstack src ofs ty)
| Mgetparam ofs ty dst => MB_basic (MBgetparam ofs ty dst)
| Mop op args res => MB_basic (MBop op args res)
| Mload trap chunk addr args dst=> MB_basic (MBload trap chunk addr args dst)
| Mstore chunk addr args src => MB_basic (MBstore chunk addr args src)
| Mlabel l => MB_label l
end.
Definition empty_bblock:={| header := nil; body := nil; exit := None |}.
Extraction Inline empty_bblock.
Definition add_label l bb:={| header := l::(header bb); body := (body bb); exit := (exit bb) |}.
Extraction Inline add_label.
Definition add_basic bi bb :={| header := nil; body := bi::(body bb); exit := (exit bb) |}.
Extraction Inline add_basic.
Definition cfi_bblock cfi:={| header := nil; body := nil; exit := Some cfi |}.
Extraction Inline cfi_bblock.
Definition add_to_new_bblock (i:Machblock_inst) : bblock :=
match i with
| MB_label l => add_label l empty_bblock
| MB_basic i => add_basic i empty_bblock
| MB_cfi i => cfi_bblock i
end.
(** Adding an instruction to the beginning of a bblock list by
- either adding the instruction to the head of the list,
- or creating a new bblock with the instruction
*)
Definition add_to_code (i:Machblock_inst) (bl:code) : code :=
match bl with
| bh::bl0 => match i with
| MB_label l => add_label l bh::bl0
| MB_cfi i0 => cfi_bblock i0::bl
| MB_basic i0 => match header bh with
|_::_ => add_basic i0 empty_bblock::bl
| nil => add_basic i0 bh::bl0
end
end
| _ => add_to_new_bblock i::nil
end.
Fixpoint trans_code_rev (c: Mach.code) (bl:code) : code :=
match c with
| nil => bl
| i::c0 =>
trans_code_rev c0 (add_to_code (trans_inst i) bl)
end.
Function trans_code (c: Mach.code) : code :=
trans_code_rev (List.rev_append c nil) nil.
Definition transf_function (f: Mach.function) : function :=
{| fn_sig:=Mach.fn_sig f;
fn_code:=trans_code (Mach.fn_code f);
fn_stacksize := Mach.fn_stacksize f;
fn_link_ofs := Mach.fn_link_ofs f;
fn_retaddr_ofs := Mach.fn_retaddr_ofs f
|}.
Definition transf_fundef (f: Mach.fundef) : fundef :=
transf_fundef transf_function f.
Definition transf_program (src: Mach.program) : program :=
transform_program transf_fundef src.
(** * Abstracting trans_code with a simpler inductive relation *)
Inductive is_end_block: Machblock_inst -> code -> Prop :=
| End_empty mbi: is_end_block mbi nil
| End_basic bi bh bl: header bh <> nil -> is_end_block (MB_basic bi) (bh::bl)
| End_cfi cfi bl: bl <> nil -> is_end_block (MB_cfi cfi) bl.
Local Hint Resolve End_empty End_basic End_cfi: core.
Inductive is_trans_code: Mach.code -> code -> Prop :=
| Tr_nil: is_trans_code nil nil
| Tr_end_block i c bl:
is_trans_code c bl ->
is_end_block (trans_inst i) bl ->
is_trans_code (i::c) (add_to_new_bblock (trans_inst i)::bl)
| Tr_add_label i l bh c bl:
is_trans_code c (bh::bl) ->
i = Mlabel l ->
is_trans_code (i::c) (add_label l bh::bl)
| Tr_add_basic i bi bh c bl:
is_trans_code c (bh::bl) ->
trans_inst i = MB_basic bi ->
header bh = nil ->
is_trans_code (i::c) (add_basic bi bh::bl).
Local Hint Resolve Tr_nil Tr_end_block: core.
Lemma add_to_code_is_trans_code i c bl:
is_trans_code c bl ->
is_trans_code (i::c) (add_to_code (trans_inst i) bl).
Proof.
destruct bl as [|bh0 bl]; cbn.
- intro H. inversion H. subst. eauto.
- remember (trans_inst i) as ti.
destruct ti as [l|bi|cfi].
+ intros; eapply Tr_add_label; eauto. destruct i; cbn in * |- *; congruence.
+ intros. remember (header bh0) as hbh0. destruct hbh0 as [|b].
* eapply Tr_add_basic; eauto.
* replace (add_basic bi empty_bblock) with (add_to_new_bblock (MB_basic bi)); auto.
rewrite Heqti; eapply Tr_end_block; eauto.
rewrite <- Heqti. eapply End_basic. congruence.
+ intros.
replace (cfi_bblock cfi) with (add_to_new_bblock (MB_cfi cfi)); auto.
rewrite Heqti. eapply Tr_end_block; eauto.
rewrite <- Heqti. eapply End_cfi. congruence.
Qed.
Local Hint Resolve add_to_code_is_trans_code: core.
Lemma trans_code_is_trans_code_rev c1: forall c2 mbi,
is_trans_code c2 mbi ->
is_trans_code (rev_append c1 c2) (trans_code_rev c1 mbi).
Proof.
induction c1 as [| i c1]; cbn; auto.
Qed.
Lemma trans_code_is_trans_code c: is_trans_code c (trans_code c).
Proof.
unfold trans_code.
rewrite <- rev_alt.
rewrite <- (rev_involutive c) at 1.
rewrite rev_alt at 1.
apply trans_code_is_trans_code_rev; auto.
Qed.
Lemma add_to_code_is_trans_code_inv i c bl:
is_trans_code (i::c) bl -> exists bl0, is_trans_code c bl0 /\ bl = add_to_code (trans_inst i) bl0.
Proof.
intro H; inversion H as [|H0 H1 bl0| | H0 bi bh H1 bl0]; clear H; subst; (repeat econstructor); eauto.
+ (* case Tr_end_block *) inversion H3; subst; cbn; auto.
* destruct (header bh); congruence.
* destruct bl0; cbn; congruence.
+ (* case Tr_add_basic *) rewrite H3. cbn. destruct (header bh); congruence.
Qed.
Lemma trans_code_is_trans_code_rev_inv c1: forall c2 mbi,
is_trans_code (rev_append c1 c2) mbi ->
exists mbi0, is_trans_code c2 mbi0 /\ mbi=trans_code_rev c1 mbi0.
Proof.
induction c1 as [| i c1]; cbn; eauto.
intros; exploit IHc1; eauto.
intros (mbi0 & H1 & H2); subst.
exploit add_to_code_is_trans_code_inv; eauto.
intros. destruct H0 as [mbi1 [H2 H3]].
exists mbi1. split; congruence.
Qed.
Local Hint Resolve trans_code_is_trans_code: core.
Theorem is_trans_code_inv c bl: is_trans_code c bl <-> bl=(trans_code c).
Proof.
constructor; intros; subst; auto.
unfold trans_code.
exploit (trans_code_is_trans_code_rev_inv (rev_append c nil) nil bl); eauto.
* rewrite <- rev_alt.
rewrite <- rev_alt.
rewrite (rev_involutive c).
apply H.
* intros.
destruct H0 as [mbi [H0 H1]].
inversion H0. subst. reflexivity.
Qed.
|
