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
|
Require Import Coqlib Maps.
Require Import AST Integers Values Events Memory Globalenvs Smallstep.
Require Import RTL Op Registers OptionMonad BTL.
Require Import Errors Linking BTLtoRTL.
(*****************************)
(* Put this in an other file *)
Require Import Linking.
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.
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: program) (tp: RTL.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 RTL_SIMULATES_BTL.
Variable prog: program.
Variable tprog: RTL.program.
Hypothesis TRANSL: match_prog prog tprog.
Let ge := Genv.globalenv prog.
Let tge := Genv.globalenv tprog.
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: 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 -> RTL.funsig tf = 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:
initial_state prog s1 ->
exists s2, RTL.initial_state tprog s2 /\ match_states s1 s2.
Proof.
intros. inv H.
exploit function_ptr_translated; eauto. intros (tf & FIND & TRANSF).
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 s1 s2 r:
match_states s1 s2 -> final_state s1 r -> RTL.final_state s2 r.
Proof.
intros. inv H0. inv H. inv STACKS. constructor.
Qed.
(* suggestion *)
Lemma iblock_stepi_simulation sp dupmap stack' f' rs0 m0 ib rs1 m1 ofin
(IBIS: iblock_istep ge sp rs0 m0 ib rs1 m1 ofin):
forall cfg' pc0 opc isfst
(MIB: match_iblock dupmap cfg' isfst pc0 ib opc)
,
match ofin with
| None => exists pc1,(opc = Some pc1) /\ plus RTL.step tge (RTL.State stack' f' sp pc0 rs0 m0) E0 (RTL.State stack' f' sp pc1 rs1 m1)
| Some fin => True (* TODO: A CHANGER *)
end.
Proof.
induction IBIS; simpl; auto.
Admitted.
Inductive iblock_istep_gen sp dupmap stack f pc0 cfg ib: trace -> bool -> option final -> option node -> Prop :=
| ibis_synced opc pc1
(HOPC: opc = Some pc1)
(MIB : match_iblock dupmap cfg true pc0 ib opc)
: iblock_istep_gen sp dupmap stack f pc0 cfg ib E0 true None opc
| ibis_stutter rs1 m1 fin ofin s t
(HFIN: ofin = Some fin)
(MIB : match_iblock dupmap cfg false pc0 ib None)
(FS : final_step ge stack f sp rs1 m1 fin t s)
: iblock_istep_gen sp dupmap stack f pc0 cfg ib t false ofin None.
Lemma iblock_step_simulation
sp dupmap stack stack' f f' rs0 m0 rs1 m1 ib ofin pc0 opc t s isfst
(STACKS: list_forall2 match_stackframes stack stack')
(TRANSF: match_function dupmap f f')
(IBIS: iblock_istep ge sp rs0 m0 ib rs1 m1 ofin)
(*(MIB : match_iblock dupmap cfg' isfst pc0 ib opc)*)
(*(FS : final_step ge stack f sp rs1 m1 fin t s)*)
(*FNC : (fn_code f) ! pc = Some ib*)
(IBGEN: iblock_istep_gen sp dupmap stack f pc0 (RTL.fn_code f') ib t isfst ofin opc)
:exists s', (if isfst then plus RTL.step else star RTL.step) tge (RTL.State stack' f' sp pc0 rs0 m0) t s' /\ match_states s s'.
Proof.
(* TODO: généraliser ce lemme pour pouvoir le prouver par induction sur IBIS:
=> il faut en particulier généraliser l'hypothèse MIB qui relie le iblock_istep ib en cours d'exécution.
avec le code RTL à partir de pc0.
=> ici, le "isfst" a déjà été généralisé: quand il vaut "false", ça veut dire qu'on a le droit de faire du "stuttering" côté RTL.
=> il reste à comprendre comment généraliser le "None" en "opc"
ainsi que l'hypothese OFIN pour autoriser le cas "ofin=None" (nécessaire pour l'induction).
Idée: si "ofin = None" alors il y a un pc1 tq "opc = Some pc1" qui permet d'exécuter la suite du bloc...
Au final, il faut sans doute introduire un "Inductive" pour capturer ces idées dans un prédicat "lisible"/"manipulable"...
*)
(* XXX keep IBIS, MIB, and FS ? *)
induction IBIS.
- (* exec_final *)
try_simplify_someHyps. (* TODO: introduire un lemme pour ce cas specifique ? *)
admit.
- inversion IBGEN; subst; try_simplify_someHyps.
inv MIB.
eexists. split. apply plus_one.
eapply exec_Inop; eauto.
try_simplify_someHyps.
admit.
- (* exec_op *)
admit. (* cas absurde car hypothese OFIN trop restrictive *)
- (* exec_load_TRAP *)
admit. (* cas absurde car hypothese OFIN trop restrictive *)
- (* exec_load_store *)
admit. (* cas absurde car hypothese OFIN trop restrictive *)
- (* exec_seq_stop *)
(*inv MIB.*)
eapply IHIBIS; eauto.
(* TODO: c'est ici qu'on voit que l'hypothèse MIB est trop restrictive actuellement
normalement, l'hypothèse d'induction IHIBIS devrait permettre de conclure quasi-directement ici.
*)
admit.
- (* exec_seq_continue *)
(* TODO: ici l'hypothèse d'induction IHIBIS1 n'est pas utilisable à cause de OFIN trop restrictive *)
try_simplify_someHyps.
(*inv MIB.*)
admit.
- (* exec_cond *)
try_simplify_someHyps.
(*inv MIB.*)
admit.
Admitted.
Theorem plus_simulation s1 t s1':
step ge s1 t s1' ->
forall s2 (MS: match_states s1 s2),
exists s2',
plus RTL.step tge s2 t s2'
/\ match_states s1' s2'.
Proof.
destruct 1; intros; inv MS.
- eapply dupmap_correct in DUPLIC; eauto.
destruct DUPLIC as (ib' & FNC & MIB).
try_simplify_someHyps. destruct STEP as (rs' & m' & fin & IBIS & FS).
admit.
(*intros; exploit iblock_step_simulation; eauto.*)
(* exec_function_internal *)
- inversion TRANSF as [dupmap f0 f0' MATCHF|]; subst. eexists. split.
+ eapply plus_one. apply RTL.exec_function_internal.
erewrite <- preserv_fnstacksize; eauto.
+ erewrite <- preserv_fnparams; eauto.
eapply match_states_intro; eauto.
apply dupmap_entrypoint. assumption.
(* exec_function_external *)
- inversion TRANSF as [|]; subst. eexists. split.
+ eapply plus_one. econstructor.
eapply external_call_symbols_preserved; eauto. apply senv_preserved.
+ constructor. assumption.
(* exec_return *)
- inversion STACKS as [|a1 al b1 bl H1 HL]; subst.
destruct b1 as [res' f' sp' pc' rs'].
eexists. split.
+ eapply plus_one. constructor.
+ inv H1. econstructor; eauto.
(*Qed.*)
Admitted.
Theorem transf_program_correct:
forward_simulation (semantics prog) (RTL.semantics tprog).
Proof.
eapply forward_simulation_plus with match_states.
- eapply senv_preserved.
- eapply transf_initial_states.
- eapply transf_final_states.
- eapply plus_simulation.
Qed.
End RTL_SIMULATES_BTL.
|
