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
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
|
(* *************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Sylvain Boulmé Grenoble-INP, VERIMAG *)
(* Justus Fasse UGA, VERIMAG *)
(* Xavier Leroy INRIA Paris-Rocquencourt *)
(* 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 Errors.
Require Import Integers Floats AST Linking.
Require Import Values Memory Events Globalenvs Smallstep.
Require Import Op Locations Machblock Conventions PseudoAsmblock Asmblock.
Require Machblockgenproof Asmblockgenproof.
Require Import Asmgen.
Module Asmblock_PRESERVATION.
Import Asmblock_TRANSF.
Definition match_prog (p: Asmblock.program) (tp: Asm.program) :=
match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp.
Lemma transf_program_match:
forall p tp, transf_program p = OK tp -> match_prog p tp.
Proof.
intros. eapply match_transform_partial_program; eauto.
Qed.
Section PRESERVATION.
Variable prog: Asmblock.program.
Variable tprog: Asm.program.
Hypothesis TRANSF: match_prog prog tprog.
Let ge := Genv.globalenv prog.
Let tge := Genv.globalenv tprog.
Definition lk :aarch64_linker := {| Asmblock.symbol_low:=Asm.symbol_low tge; Asmblock.symbol_high:=Asm.symbol_high tge|}.
Lemma symbols_preserved:
forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
Proof (Genv.find_symbol_match TRANSF).
Lemma symbol_addresses_preserved:
forall (s: ident) (ofs: ptrofs),
Genv.symbol_address tge s ofs = Genv.symbol_address ge s ofs.
Proof.
intros; unfold Genv.symbol_address; rewrite symbols_preserved; reflexivity.
Qed.
Lemma senv_preserved:
Senv.equiv ge tge.
Proof (Genv.senv_match TRANSF).
Lemma symbol_high_low: forall (id: ident) (ofs: ptrofs),
Val.addl (Asmblock.symbol_high lk id ofs) (Asmblock.symbol_low lk id ofs) = Genv.symbol_address ge id ofs.
Proof.
unfold lk; simpl. intros; rewrite Asm.symbol_high_low; unfold Genv.symbol_address;
rewrite symbols_preserved; reflexivity.
Qed.
Lemma functions_translated:
forall b f,
Genv.find_funct_ptr ge b = Some f ->
exists tf,
Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = OK tf.
Proof (Genv.find_funct_ptr_transf_partial TRANSF).
(* Asmblock and Asm share the same definition of state *)
Definition match_states (s1 s2 : state) := s1 = s2.
Inductive match_internal: forall n, state -> state -> Prop :=
| match_internal_intro n rs1 m1 rs2 m2
(MEM: m1 = m2)
(AG: forall r, r <> PC -> rs1 r = rs2 r)
(AGPC: Val.offset_ptr (rs1 PC) (Ptrofs.repr n) = rs2 PC)
: match_internal n (State rs1 m1) (State rs2 m2).
Lemma match_internal_set_parallel:
forall n rs1 m1 rs2 m2 r val,
match_internal n (State rs1 m1) (State rs2 m2) ->
r <> PC ->
match_internal n (State (rs1#r <- val) m1) (State (rs2#r <- val ) m2).
Proof.
intros n rs1 m1 rs2 m2 r v MI.
inversion MI; constructor; auto.
- intros r' NOTPC.
unfold Pregmap.set; rewrite AG. reflexivity. assumption.
- unfold Pregmap.set; destruct (PregEq.eq PC r); congruence.
Qed.
Lemma agree_match_states:
forall rs1 m1 rs2 m2,
match_states (State rs1 m1) (State rs2 m2) ->
forall r : preg, rs1#r = rs2#r.
Proof.
intros.
unfold match_states in *.
assert (rs1 = rs2) as EQ. { congruence. }
rewrite EQ. reflexivity.
Qed.
Lemma match_states_set_parallel:
forall rs1 m1 rs2 m2 r v,
match_states (State rs1 m1) (State rs2 m2) ->
match_states (State (rs1#r <- v) m1) (State (rs2#r <- v) m2).
Proof.
intros; unfold match_states in *.
assert (rs1 = rs2) as RSEQ. { congruence. }
assert (m1 = m2) as MEQ. { congruence. }
rewrite RSEQ in *; rewrite MEQ in *; unfold Pregmap.set; reflexivity.
Qed.
(* match_internal from match_states *)
Lemma mi_from_ms:
forall rs1 m1 rs2 m2 b ofs,
match_states (State rs1 m1) (State rs2 m2) ->
rs1#PC = Vptr b ofs ->
match_internal 0 (State rs1 m1) (State rs2 m2).
Proof.
intros rs1 m1 rs2 m2 b ofs MS PCVAL.
inv MS; constructor; auto; unfold Val.offset_ptr;
rewrite PCVAL; rewrite Ptrofs.add_zero; reflexivity.
Qed.
Lemma transf_initial_states:
forall s1, Asmblock.initial_state prog s1 ->
exists s2, Asm.initial_state tprog s2 /\ match_states s1 s2.
Proof.
intros ? INIT_s1.
inversion INIT_s1 as (m, ?, ge0, rs). unfold ge0 in *.
econstructor; split.
- econstructor.
eapply (Genv.init_mem_transf_partial TRANSF); eauto.
- rewrite (match_program_main TRANSF); rewrite symbol_addresses_preserved.
unfold rs; reflexivity.
Qed.
Lemma transf_final_states:
forall s1 s2 r,
match_states s1 s2 -> Asmblock.final_state s1 r -> Asm.final_state s2 r.
Proof.
intros s1 s2 r MATCH FINAL_s1.
inv FINAL_s1; inv MATCH; constructor; assumption.
Qed.
Definition max_pos (f : Asm.function) := length f.(Asm.fn_code).
Lemma functions_bound_max_pos: forall fb f tf,
Genv.find_funct_ptr ge fb = Some (Internal f) ->
transf_function f = OK tf ->
Z.of_nat (max_pos tf) <= Ptrofs.max_unsigned.
Proof.
intros fb f tf FINDf TRANSf.
unfold transf_function in TRANSf.
apply bind_inversion in TRANSf.
destruct TRANSf as (c & TRANSf).
destruct TRANSf as (_ & TRANSf).
destruct (zlt Ptrofs.max_unsigned (Z.of_nat (length c))).
- inversion TRANSf.
- unfold max_pos.
assert (Asm.fn_code tf = c) as H. { inversion TRANSf as (H'); auto. }
rewrite H; omega.
Qed.
Lemma one_le_max_unsigned:
1 <= Ptrofs.max_unsigned.
Proof.
unfold Ptrofs.max_unsigned; simpl; unfold Ptrofs.wordsize;
unfold Wordsize_Ptrofs.wordsize; destruct Archi.ptr64; simpl; omega.
Qed.
Lemma match_internal_exec_label:
forall n rs1 m1 rs2 m2 l fb f tf,
Genv.find_funct_ptr ge fb = Some (Internal f) ->
transf_function f = OK tf ->
match_internal n (State rs1 m1) (State rs2 m2) ->
n >= 0 ->
(* There is no step if n is already max_pos *)
n < Z.of_nat (max_pos tf) ->
exists rs2' m2', Asm.exec_instr tge tf (Asm.Plabel l) rs2 m2 = Next rs2' m2'
/\ match_internal (n+1) (State rs1 m1) (State rs2' m2').
Proof.
intros. (* XXX auto generated names *)
unfold Asm.exec_instr.
eexists; eexists; split; eauto.
inversion H1; constructor; auto.
- intros; unfold Asm.nextinstr; unfold Pregmap.set;
destruct (PregEq.eq r PC); auto; contradiction.
- unfold Asm.nextinstr; rewrite Pregmap.gss; unfold Ptrofs.one.
rewrite <- AGPC; rewrite Val.offset_ptr_assoc; unfold Ptrofs.add;
rewrite Ptrofs.unsigned_repr. rewrite Ptrofs.unsigned_repr; trivial.
+ split.
* apply Z.le_0_1.
* apply one_le_max_unsigned.
+ split.
* apply Z.ge_le; assumption.
* rewrite <- functions_bound_max_pos; eauto; omega.
Qed.
Lemma step_simulation s1 t s1':
Asmblock.step lk ge s1 t s1' ->
forall s2, match_states s1 s2 ->
(exists s2', plus Asm.step tge s2 t s2' /\ match_states s1' s2').
Proof.
intros STEP s2 MATCH.
inv STEP; simpl; exploit functions_translated; eauto;
intros (tf0 & FINDtf & TRANSf);
monadInv TRANSf.
- (* internal step *) admit.
- (* external step *)
eexists; split.
+ apply plus_one.
rewrite <- MATCH.
exploit external_call_symbols_preserved; eauto. apply senv_preserved.
intros ?.
eapply Asm.exec_step_external; eauto.
+ econstructor; eauto.
Admitted.
Lemma transf_program_correct:
forward_simulation (Asmblock.semantics lk prog) (Asm.semantics tprog).
Proof.
eapply forward_simulation_plus.
- apply senv_preserved.
- eexact transf_initial_states.
- eexact transf_final_states.
- (* TODO step_simulation *) admit.
Admitted.
End PRESERVATION.
End Asmblock_PRESERVATION.
Local Open Scope linking_scope.
Definition block_passes :=
mkpass Machblockgenproof.match_prog
::: mkpass PseudoAsmblockproof.match_prog
::: mkpass Asmblockgenproof.match_prog
::: mkpass Asmblock_PRESERVATION.match_prog
::: pass_nil _.
Definition match_prog := pass_match (compose_passes block_passes).
Lemma transf_program_match:
forall p tp, Asmgen.transf_program p = OK tp -> match_prog p tp.
Proof.
intros p tp H.
unfold Asmgen.transf_program in H. apply bind_inversion in H. destruct H.
inversion_clear H. apply bind_inversion in H1. destruct H1.
inversion_clear H. inversion H2. remember (Machblockgen.transf_program p) as mbp.
unfold match_prog; simpl.
exists mbp; split. apply Machblockgenproof.transf_program_match; auto.
exists x; split. apply PseudoAsmblockproof.transf_program_match; auto.
exists x0; split. apply Asmblockgenproof.transf_program_match; auto.
exists tp; split. apply Asmblock_PRESERVATION.transf_program_match; auto. auto.
Qed.
(** Return Address Offset *)
Definition return_address_offset: Mach.function -> Mach.code -> ptrofs -> Prop :=
Machblockgenproof.Mach_return_address_offset (PseudoAsmblockproof.rao Asmblockgenproof.next).
Lemma return_address_exists:
forall f sg ros c, is_tail (Mach.Mcall sg ros :: c) f.(Mach.fn_code) ->
exists ra, return_address_offset f c ra.
Proof.
intros; eapply Machblockgenproof.Mach_return_address_exists; eauto.
Admitted.
Section PRESERVATION.
Variable prog: Mach.program.
Variable tprog: Asm.program.
Hypothesis TRANSF: match_prog prog tprog.
Let ge := Genv.globalenv prog.
Let tge := Genv.globalenv tprog.
Theorem transf_program_correct:
forward_simulation (Mach.semantics return_address_offset prog) (Asm.semantics tprog).
Proof.
unfold match_prog in TRANSF. simpl in TRANSF.
inv TRANSF. inv H. inv H1. inv H. inv H2. inv H. inv H3. inv H.
eapply compose_forward_simulations.
{ exploit Machblockgenproof.transf_program_correct; eauto. }
eapply compose_forward_simulations.
+ apply PseudoAsmblockproof.transf_program_correct; eauto.
- intros; apply Asmblockgenproof.next_progress.
- intros; eapply Asmblockgenproof.functions_bound_max_pos; eauto.
{ intros; eapply Asmblock_PRESERVATION.symbol_high_low; eauto. }
+ eapply compose_forward_simulations. apply Asmblockgenproof.transf_program_correct; eauto.
{ intros; eapply Asmblock_PRESERVATION.symbol_high_low; eauto. }
apply Asmblock_PRESERVATION.transf_program_correct. eauto.
Qed.
End PRESERVATION.
Instance TransfAsm: TransfLink match_prog := pass_match_link (compose_passes block_passes).
(*******************************************)
(* Stub actually needed by driver/Compiler *)
Module Asmgenproof0.
Definition return_address_offset := return_address_offset.
End Asmgenproof0.
|
