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
|
Require Import Coqlib Maps.
Require Import AST Integers Values Events Memory Globalenvs Smallstep.
Require Import RTL Op Registers OptionMonad BTL.
Require Import Errors Linking RTLtoBTL.
Require Import Linking.
Record match_function dupmap (f:RTL.function) (tf: BTL.function): Prop := {
dupmap_correct: match_cfg dupmap (fn_code tf) (RTL.fn_code f);
dupmap_entrypoint: dupmap!(fn_entrypoint tf) = Some (RTL.fn_entrypoint f);
code_right_assoc: forall pc ib, (fn_code tf)!pc=Some ib -> is_right_assoc ib.(entry);
preserv_fnsig: fn_sig tf = RTL.fn_sig f;
preserv_fnparams: fn_params tf = RTL.fn_params f;
preserv_fnstacksize: fn_stacksize tf = RTL.fn_stacksize f
}.
Inductive match_fundef: RTL.fundef -> fundef -> Prop :=
| match_Internal dupmap f tf: match_function dupmap f tf -> match_fundef (Internal f) (Internal tf)
| match_External ef: match_fundef (External ef) (External ef).
Inductive match_stackframes: RTL.stackframe -> stackframe -> Prop :=
| match_stackframe_intro
dupmap res f sp pc rs f' pc'
(TRANSF: match_function dupmap f f')
(DUPLIC: dupmap!pc' = Some pc)
: match_stackframes (RTL.Stackframe res f sp pc rs) (Stackframe res f' sp pc' rs).
Lemma verify_function_correct dupmap f f' tt:
verify_function dupmap f' f = OK tt ->
fn_sig f' = RTL.fn_sig f ->
fn_params f' = RTL.fn_params f ->
fn_stacksize f' = RTL.fn_stacksize f ->
(forall pc ib, (fn_code f')!pc=Some ib -> is_right_assoc ib.(entry)) ->
match_function dupmap f f'.
Proof.
unfold verify_function; intro VERIF. monadInv VERIF.
constructor; eauto.
- eapply verify_cfg_correct; eauto.
- eapply verify_is_copy_correct; eauto.
Qed.
Lemma transf_function_correct f f':
transf_function f = OK f' -> exists dupmap, match_function dupmap f f'.
Proof.
unfold transf_function; unfold bind. repeat autodestruct.
intros H _ _ X. inversion X; subst; clear X.
eexists; eapply verify_function_correct; simpl; eauto.
eapply right_assoc_code_correct; eauto.
Qed.
Lemma transf_fundef_correct f f':
transf_fundef f = OK f' -> match_fundef f f'.
Proof.
intros TRANSF; destruct f; simpl; monadInv TRANSF.
+ exploit transf_function_correct; eauto.
intros (dupmap & MATCH_F).
eapply match_Internal; eauto.
+ eapply match_External.
Qed.
Definition match_prog (p: RTL.program) (tp: program) :=
match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp.
Lemma transf_program_match:
forall prog tprog, transf_program prog = OK tprog -> match_prog prog tprog.
Proof.
intros. eapply match_transform_partial_program_contextual; eauto.
Qed.
Section BTL_SIMULATES_RTL.
Variable prog: RTL.program.
Variable tprog: program.
Hypothesis TRANSL: match_prog prog tprog.
Let ge := Genv.globalenv prog.
Let tge := Genv.globalenv tprog.
Local Open Scope nat_scope.
(* TODO:
Le (option iblock) en paramètre représente l'état de l'exécution côté BTL
depuis le début de l'exécution du block
faire un dessin ASCII art de la simulation avec match_states_intro
*)
Inductive match_states: (option iblock) -> RTL.state -> state -> Prop :=
| match_states_intro (* TODO: LES DETAILS SONT SANS DOUTE A REVOIR !!! *)
ib dupmap st f sp pc rs m st' f' pc0' pc0 rs0 m0 isfst ib0
(STACKS: list_forall2 match_stackframes st st')
(TRANSF: match_function dupmap f f')
(ATpc0: (fn_code f')!pc0' = Some ib0)
(DUPLIC: dupmap!pc0' = Some pc0)
(MIB: match_iblock dupmap (RTL.fn_code f) isfst pc ib None)
(RIGHTA: is_right_assoc ib)
(RTL_RUN: star RTL.step ge (RTL.State st f sp pc0 rs0 m0) E0 (RTL.State st f sp pc rs m))
(BTL_RUN: iblock_istep_run tge sp ib0.(entry) rs0 m0 = iblock_istep_run tge sp ib rs m)
: match_states (Some ib) (RTL.State st f sp pc rs m) (State st' f' sp pc0' rs0 m0)
| match_states_call
st st' f f' args m
(STACKS: list_forall2 match_stackframes st st')
(TRANSF: match_fundef f f')
: match_states None (RTL.Callstate st f args m) (Callstate st' f' args m)
| match_states_return
st st' v m
(STACKS: list_forall2 match_stackframes st st')
: match_states None (RTL.Returnstate st v m) (Returnstate st' v m)
.
Lemma symbols_preserved s: Genv.find_symbol tge s = Genv.find_symbol ge s.
Proof.
rewrite <- (Genv.find_symbol_match TRANSL). reflexivity.
Qed.
Lemma senv_preserved: Senv.equiv ge tge.
Proof.
eapply (Genv.senv_match TRANSL).
Qed.
Lemma functions_translated (v: val) (f: RTL.fundef):
Genv.find_funct ge v = Some f ->
exists tf cunit, transf_fundef f = OK tf /\ Genv.find_funct tge v = Some tf /\ linkorder cunit prog.
Proof.
intros. exploit (Genv.find_funct_match TRANSL); eauto.
intros (cu & tf & A & B & C).
repeat eexists; intuition eauto.
+ unfold incl; auto.
+ eapply linkorder_refl.
Qed.
Lemma function_ptr_translated v f:
Genv.find_funct_ptr ge v = Some f ->
exists tf,
Genv.find_funct_ptr tge v = Some tf /\ transf_fundef f = OK tf.
Proof.
intros.
exploit (Genv.find_funct_ptr_transf_partial TRANSL); eauto.
Qed.
Lemma function_sig_translated f tf: transf_fundef f = OK tf -> funsig tf = RTL.funsig f.
Proof.
intros H; apply transf_fundef_correct in H; destruct H; simpl; eauto.
erewrite preserv_fnsig; eauto.
Qed.
Lemma transf_initial_states s1:
RTL.initial_state prog s1 ->
exists ib s2, initial_state tprog s2 /\ match_states ib s1 s2.
Proof.
intros. inv H.
exploit function_ptr_translated; eauto. intros (tf & FIND & TRANSF).
eexists. eexists. split.
- econstructor; eauto.
+ eapply (Genv.init_mem_transf_partial TRANSL); eauto.
+ replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved. eauto.
symmetry. eapply match_program_main. eauto.
+ erewrite function_sig_translated; eauto.
- constructor; eauto.
constructor.
apply transf_fundef_correct; auto.
Qed.
Lemma transf_final_states ib s1 s2 r:
match_states ib s1 s2 -> RTL.final_state s1 r -> final_state s2 r.
Proof.
intros. inv H0. inv H. inv STACKS. constructor.
Qed.
Lemma find_function_preserved ri rs0 fd
(FIND : RTL.find_function ge ri rs0 = Some fd)
: exists fd', find_function tge ri rs0 = Some fd'
/\ transf_fundef fd = OK fd'.
Proof.
pose symbols_preserved as SYMPRES.
destruct ri.
+ simpl in FIND; apply functions_translated in FIND.
destruct FIND as (tf & cunit & TFUN & GFIND & LO).
eexists; split. eauto. assumption.
+ simpl in FIND. destruct (Genv.find_symbol _ _) eqn:GFS; try discriminate.
apply function_ptr_translated in FIND. destruct FIND as (tf & GFF & TF).
eexists; split. simpl. rewrite symbols_preserved.
rewrite GFS. eassumption. assumption.
Qed.
(* Inspired from Duplicateproof.v *)
Lemma list_nth_z_dupmap:
forall dupmap ln ln' (pc pc': node) val,
list_nth_z ln val = Some pc ->
list_forall2 (fun n n' => dupmap!n = Some n') ln ln' ->
exists (pc': node),
list_nth_z ln' val = Some pc'
/\ dupmap!pc = Some pc'.
Proof.
induction ln; intros until val; intros LNZ LFA.
- inv LNZ.
- inv LNZ. destruct (zeq val 0) eqn:ZEQ.
+ inv H0. destruct ln'; inv LFA.
simpl. exists n. split; auto.
+ inv LFA. simpl. rewrite ZEQ. exploit IHln. 2: eapply H0. all: eauto.
Qed.
(* TODO: definir une measure sur les iblocks.
Cette mesure décroit strictement quand on exécute un "petit-pas" de iblock.
Par exemple, le nombre de noeuds (ou d'instructions "RTL") dans le iblock devrait convenir.
La hauteur de l'arbre aussi.
*)
Parameter measure: iblock -> nat.
Definition omeasure (oib: option iblock): nat :=
match oib with
| None => 0
| Some ib => measure ib
end.
Theorem opt_simu s1 t s1' oib s2:
RTL.step ge s1 t s1' ->
match_states oib s1 s2 ->
exists (oib' : option iblock),
(exists s2', step tge s2 t s2' /\ match_states oib' s1' s2')
\/ (omeasure oib' < omeasure oib /\ t=E0 /\ match_states oib' s1' s2)
.
Admitted.
Local Hint Resolve plus_one star_refl: core.
Theorem transf_program_correct:
forward_simulation (RTL.semantics prog) (BTL.semantics tprog).
Proof.
eapply (Forward_simulation (L1:=RTL.semantics prog) (L2:=semantics tprog) (ltof _ omeasure) match_states).
constructor 1; simpl.
- apply well_founded_ltof.
- eapply transf_initial_states.
- eapply transf_final_states.
- intros s1 t s1' STEP i s2 MATCH. exploit opt_simu; eauto. clear MATCH STEP.
destruct 1 as (oib' & [ (s2' & STEP & MATCH) | (MEASURE & TRACE & MATCH) ]).
+ repeat eexists; eauto.
+ subst. repeat eexists; eauto.
- eapply senv_preserved.
Qed.
End BTL_SIMULATES_RTL.
|
