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
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
|
(*
* Vericert: Verified high-level synthesis.
* Copyright (C) 2023 Yann Herklotz <yann@yannherklotz.com>
*
* This program is free software: you can redistribute it and/or modify
* it under the terms of the GNU General Public License as published by
* the Free Software Foundation, either version 3 of the License, or
* (at your option) any later version.
*
* This program is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details.
*
* You should have received a copy of the GNU General Public License
* along with this program. If not, see <https://www.gnu.org/licenses/>.
*)
Require Import Coq.micromega.Lia.
Require Import compcert.lib.Maps.
Require Import compcert.common.Errors.
Require Import compcert.common.Globalenvs.
Require compcert.backend.Registers.
Require Import compcert.common.Linking.
Require Import compcert.common.Memory.
Require compcert.common.Globalenvs.
Require Import compcert.lib.Integers.
Require Import compcert.common.AST.
Require Import vericert.common.IntegerExtra.
Require Import vericert.common.Vericertlib.
Require Import vericert.common.ZExtra.
Require Import vericert.hls.Gible.
Require Import vericert.hls.GiblePar.
Require Import vericert.hls.GibleSubPar.
Require Import vericert.hls.GibleSubPargen.
Require Import vericert.hls.Predicate.
Require Import vericert.common.Errormonad.
Import ErrorMonad.
Import ErrorMonadExtra.
Require Import Lia.
Inductive match_stackframe : GiblePar.stackframe -> GibleSubPar.stackframe -> Prop :=
| match_stackframe_init : forall r f tf sp n rs ps
(TF: transl_function f = OK tf),
match_stackframe (GiblePar.Stackframe r f sp n rs ps)
(Stackframe r tf sp n rs ps).
Variant match_states : GiblePar.state -> GibleSubPar.state -> Prop :=
| match_state :
forall stk stk' f tf sp pc rs m ps
(HSTACK: Forall2 match_stackframe stk stk')
(TF: transl_function f = OK tf),
match_states (GiblePar.State stk f sp pc rs ps m)
(State stk' tf sp pc rs ps m)
| match_callstate :
forall cs cs' f tf args m
(TF: transl_fundef f = OK tf)
(STK: Forall2 match_stackframe cs cs'),
match_states (GiblePar.Callstate cs f args m) (Callstate cs' tf args m)
| match_returnstate :
forall cs cs' v m
(STK: Forall2 match_stackframe cs cs'),
match_states (GiblePar.Returnstate cs v m) (Returnstate cs' v m).
Definition match_prog (p: GiblePar.program) (tp: GibleSubPar.program) :=
Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp.
Section CORRECTNESS.
Context (prog : GiblePar.program).
Context (tprog : GibleSubPar.program).
Let ge : GiblePar.genv := Globalenvs.Genv.globalenv prog.
Let tge : GibleSubPar.genv := Globalenvs.Genv.globalenv tprog.
Context (TRANSL : match_prog prog tprog).
Lemma symbols_preserved:
forall (s: AST.ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
Proof using TRANSL. intros. eapply (Genv.find_symbol_match TRANSL). Qed.
Lemma senv_preserved:
Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge).
Proof using TRANSL. intros; eapply (Genv.senv_transf_partial TRANSL). Qed.
#[local] Hint Resolve senv_preserved : rtlbg.
Lemma function_ptr_translated:
forall b f,
Genv.find_funct_ptr ge b = Some f ->
exists tf, Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = OK tf.
Proof (Genv.find_funct_ptr_transf_partial TRANSL).
Lemma sig_transl_function:
forall (f: GiblePar.fundef) (tf: GibleSubPar.fundef),
transl_fundef f = OK tf ->
GibleSubPar.funsig tf = GiblePar.funsig f.
Proof using.
unfold transl_fundef. unfold transf_partial_fundef.
intros. destruct_match. unfold Errors.bind in *. destruct_match; try discriminate.
inv H. cbn. unfold transl_function in Heqr; unfold bind in *.
repeat (destruct_match; try discriminate). inv Heqr. auto.
inv H; auto.
Qed.
Lemma stacksize_equal:
forall f f0,
transl_function f = OK f0 ->
f0.(fn_stacksize) = f.(GiblePar.fn_stacksize).
Proof.
unfold transl_function, bind; intros. destruct_match; [|discriminate].
inv H. auto.
Qed.
Lemma entrypoint_equal:
forall f f0,
transl_function f = OK f0 ->
f0.(fn_entrypoint) = f.(GiblePar.fn_entrypoint).
Proof.
unfold transl_function, bind; intros. destruct_match; [|discriminate].
inv H. auto.
Qed.
Lemma params_equal:
forall f f0,
transl_function f = OK f0 ->
f0.(fn_params) = f.(GiblePar.fn_params).
Proof.
unfold transl_function, bind; intros. destruct_match; [|discriminate].
inv H. auto.
Qed.
Lemma mfold_left_error:
forall A B f l m, @mfold_left A B f l (Error m) = Error m.
Proof. now induction l. Qed.
Lemma mfold_left_cons:
forall A B f a l x y,
@mfold_left A B f (a :: l) x = OK y ->
exists x' y', @mfold_left A B f l (OK y') = OK y /\ f x' a = OK y' /\ x = OK x'.
Proof.
intros.
destruct x; [|now rewrite mfold_left_error in H].
cbn in H.
replace (fold_left (fun (a : mon A) (b : B) => bind (fun a' : A => f a' b) a) l (f a0 a) = OK y) with
(mfold_left f l (f a0 a) = OK y) in H by auto.
destruct (f a0 a) eqn:?; [|now rewrite mfold_left_error in H].
eauto.
Qed.
Lemma step_cf_instr_pc_ind :
forall s f sp rs' pr' m' pc pc' cf t state,
GiblePar.step_cf_instr ge (GiblePar.State s f sp pc rs' pr' m') cf t state ->
GiblePar.step_cf_instr ge (GiblePar.State s f sp pc' rs' pr' m') cf t state.
Proof. destruct cf; intros; inv H; econstructor; eauto. Qed.
Lemma step_list_inter_not_term :
forall A step_i sp i cf l i' cf',
@step_list_inter A step_i sp (Iterm i cf) l (Iterm i' cf') ->
i = i' /\ cf = cf'.
Proof. now inversion 1. Qed.
Lemma step_list_inter_not_exec :
forall A step_i sp i cf l i',
~ @step_list_inter A step_i sp (Iterm i cf) l (Iexec i').
Proof. now inversion 1. Qed.
Lemma step_instr_seq_with_exit:
forall sp a rs pr m rs' pr' m' pc,
ParBB.step_instr_seq ge sp
(Iexec {| is_rs := rs; is_ps := pr; is_mem := m |}) a
(Iexec {| is_rs := rs'; is_ps := pr'; is_mem := m' |}) ->
SubParBB.step_instr_seq tge sp
(Iexec {| is_rs := rs; is_ps := pr; is_mem := m |}) (a ++ ((RBexit None (RBgoto pc) :: nil) :: nil))
(Iterm {| is_rs := rs'; is_ps := pr'; is_mem := m' |} (RBgoto pc)).
Proof.
induction a; intros.
- cbn in *. inv H. eapply exec_RBterm. repeat econstructor.
- cbn in *. inv H. destruct i1. destruct i. econstructor; eauto.
Admitted.
Lemma step_instr_seq_with_exit':
forall sp a rs pr m rs' pr' m' pc cf,
ParBB.step_instr_seq ge sp
(Iexec {| is_rs := rs; is_ps := pr; is_mem := m |}) a
(Iterm {| is_rs := rs'; is_ps := pr'; is_mem := m' |} cf) ->
SubParBB.step_instr_seq tge sp
(Iexec {| is_rs := rs; is_ps := pr; is_mem := m |}) (a ++ ((RBexit None (RBgoto pc) :: nil) :: nil))
(Iterm {| is_rs := rs'; is_ps := pr'; is_mem := m' |} cf).
Proof.
induction a; intros.
- cbn in *. inv H.
Admitted.
Lemma transl_spec_not_in':
forall bb pc fresh code_start fresh' code_end pc' y,
transl_block (fresh, code_start) (pc', bb) = OK (fresh', code_end) ->
code_start ! pc = Some y ->
code_end ! pc = Some y.
Proof.
induction bb; unfold transl_block; intros; cbn in *.
- inv H; auto.
- remember (
match code_start ! pc' with
| Some _ => Error (msg "GibleSubPargen: Overlapping blocks in translation")
| None =>
OK (fresh, (Pos.succ fresh, PTree.set pc' (a ++ (RBexit None (RBgoto fresh) :: nil) :: nil) code_start))
end) as trans. setoid_rewrite <- Heqtrans in H.
replace (fold_left
(fun (a : mon (positive * (positive * code))) (b : SubParBB.t) =>
bind (fun a' : positive * (positive * code) => transl_block' a' b) a) bb trans) with
(mfold_left transl_block' bb trans) in H by auto.
destruct trans; [|rewrite mfold_left_error in H; cbn in *; inversion H].
repeat (destruct_match; try discriminate; []).
inversion Heqtrans as []. rewrite H1 in H.
exploit IHbb; eauto.
destruct (peq pc pc').
+ subst. rewrite Heqo in H0. discriminate.
+ rewrite PTree.gso by auto; auto.
Qed.
Lemma transl_spec_not_in:
forall l pc fresh code_start fresh' code_end y,
mfold_left transl_block l (OK (fresh, code_start)) = OK (fresh', code_end) ->
code_start ! pc = Some y ->
code_end ! pc = Some y.
Proof.
induction l; cbn in *; [inversion 1; auto|].
intros * HFOLD HNOT.
remember (transl_block (fresh, code_start) a) as tblock.
replace (fold_left
(fun (a : mon (positive * code)) (b : positive * ParBB.t) =>
bind (fun a' : positive * code => transl_block a' b) a) l tblock) with
(mfold_left transl_block l tblock) in HFOLD by auto.
destruct tblock; [|rewrite mfold_left_error in HFOLD; discriminate].
symmetry in Heqtblock. destruct p, a. eapply transl_spec_not_in' in Heqtblock; eauto.
Qed.
Lemma transl_plus_correct:
forall f sp bb pc pc' fresh fresh' code code' s rs pr m rs' pr' m' cf t state0 s' tf,
ParBB.step (Smallstep.globalenv (GiblePar.semantics prog)) sp (Iexec {| is_rs := rs; is_ps := pr; is_mem := m |})
bb (Iterm {| is_rs := rs'; is_ps := pr'; is_mem := m' |} cf) ->
GiblePar.step_cf_instr (Smallstep.globalenv (GiblePar.semantics prog)) (GiblePar.State s f sp pc rs' pr' m') cf t
state0 ->
mfold_left transl_block' bb (OK (pc, (fresh, code))) = OK (pc', (fresh', code')) ->
(forall x y, code' ! x = Some y -> (fn_code tf) ! x = Some y) ->
match_states (GiblePar.State s f sp pc rs pr m) (State s' tf sp pc rs pr m) ->
exists s2' : Smallstep.state (semantics tprog),
Smallstep.plus (Smallstep.step (semantics tprog)) (Smallstep.globalenv (semantics tprog)) (State s' tf sp pc rs pr m) t s2' /\
match_states state0 s2'.
Proof.
induction bb; [inversion 1|].
intros. exploit mfold_left_cons; eauto.
intros (ytemp & (pc_mid & (fresh_mid & code_mid)) & HFOLD & HTRANSL & HOK).
inv HOK. inv H.
- destruct state'. exploit IHbb. eauto. eapply step_cf_instr_pc_ind; eauto.
eauto. eauto. inv H3. econstructor; eauto.
intros (s2' & HPLUS & HMATCH).
unfold transl_block' in HTRANSL. repeat (destruct_match; try discriminate; []).
inv HTRANSL.
exploit transl_spec_not_in'. unfold transl_block.
rewrite HFOLD. cbn. eauto. rewrite PTree.gss. eauto.
intros. eapply H2 in H.
econstructor. split.
eapply Smallstep.plus_left'. econstructor. eauto. cbn. eapply step_instr_seq_with_exit.
eauto. econstructor. eauto. eauto. eauto.
- cbn in HTRANSL. repeat (destruct_match; try discriminate). inv HTRANSL.
exploit transl_spec_not_in'. unfold transl_block. rewrite HFOLD. cbn. eauto.
rewrite PTree.gss. eauto. intros. eapply H2 in H.
econstructor. split.
+ apply Smallstep.plus_one. econstructor; eauto.
eapply step_instr_seq_with_exit'; eauto.
Admitted.
Lemma transl_spec':
forall l fresh fresh' code_start code_end pc bb,
mfold_left transl_block l (OK (fresh, code_start)) = OK (fresh', code_end) ->
In (pc, bb) l ->
exists (code0 code' : code) (fresh fresh' : positive),
transl_block (fresh, code0) (pc, bb) = OK (fresh', code') /\
(forall (x : positive) (y : SubParBB.t), code' ! x = Some y -> code_end ! x = Some y).
Proof.
induction l; [inversion 2|].
intros * HFOLD HIN.
cbn in *.
remember (transl_block (fresh, code_start) a) as HTRANSL.
replace (fold_left
(fun (a : mon (positive * code)) (b : positive * ParBB.t) =>
bind (fun a' : positive * code => transl_block a' b) a) l HTRANSL) with
(mfold_left transl_block l HTRANSL) in HFOLD by auto.
destruct HTRANSL;
[|erewrite mfold_left_error in HFOLD; discriminate].
destruct p as [fresh_mid code_mid].
symmetry in HeqHTRANSL.
inv HIN; eauto.
exists code_start, code_mid, fresh, fresh_mid; split; auto.
intros. eapply transl_spec_not_in; eauto.
Qed.
Lemma transl_spec:
forall f tf pc bb,
transl_function f = OK tf ->
f.(GiblePar.fn_code) ! pc = Some bb ->
exists code code' fresh fresh',
transl_block (fresh, code) (pc, bb) = OK (fresh', code')
/\ (forall x y, code' ! x = Some y -> tf.(fn_code) ! x = Some y).
Proof.
unfold transl_function, bind; intros. destruct_match; [|discriminate].
inversion_clear H as []. cbn -[transl_block] in *.
destruct p.
eapply transl_spec'; eauto.
now apply PTree.elements_correct.
Qed.
Lemma transl_plus_step:
forall (s1 : Smallstep.state (GiblePar.semantics prog)) (t : Events.trace)
(s1' : Smallstep.state (GiblePar.semantics prog)),
Smallstep.step (GiblePar.semantics prog) (Smallstep.globalenv (GiblePar.semantics prog)) s1 t s1' ->
forall s2 : Smallstep.state (semantics tprog),
match_states s1 s2 ->
exists s2' : Smallstep.state (semantics tprog),
Smallstep.plus (Smallstep.step (semantics tprog)) (Smallstep.globalenv (semantics tprog)) s2 t s2' /\
match_states s1' s2'.
Proof.
induction 1.
- inversion 1; subst. exploit transl_spec; eauto.
intros (code0 & code' & fresh & fresh' & HFOLD & HIN).
unfold transl_block in HFOLD.
unfold map in HFOLD. repeat (destruct_match; try discriminate). destruct p. destruct p0.
inv HFOLD. eapply transl_plus_correct; eauto.
- eauto. intros * HMATCH. inv HMATCH. cbn in TF. unfold Errors.bind in TF. destruct_match; [|discriminate].
inv TF. econstructor. split.
+ apply Smallstep.plus_one. econstructor. erewrite stacksize_equal by eauto. eauto.
+ erewrite params_equal by eauto. erewrite entrypoint_equal by eauto. now econstructor.
- cbn in *. intros * HMATCH. inv HMATCH. cbn in *. inv TF.
econstructor. split.
+ apply Smallstep.plus_one. econstructor. eapply Events.external_call_symbols_preserved; eauto.
eapply senv_preserved.
+ now constructor.
- cbn in *. intros * HMATCH. inv HMATCH. inv STK. inv H1.
econstructor; split.
+ apply Smallstep.plus_one. econstructor.
+ now constructor.
Qed.
Lemma transl_initial_states:
forall S,
GiblePar.initial_state prog S ->
exists R, GibleSubPar.initial_state tprog R /\ match_states S R.
Proof.
induction 1.
exploit function_ptr_translated; eauto. intros [tf [A B]].
econstructor; split.
econstructor. apply (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.
eexact A.
rewrite <- H2. apply sig_transl_function; auto.
constructor. auto. constructor.
Qed.
Lemma transl_final_states:
forall S R r,
match_states S R -> GiblePar.final_state S r -> GibleSubPar.final_state R r.
Proof. intros. inv H0. inv H. inv STK. constructor. Qed.
Theorem transl_program_correct:
Smallstep.forward_simulation (GiblePar.semantics prog) (semantics tprog).
Proof using TRANSL.
eapply Smallstep.forward_simulation_plus.
- apply senv_preserved.
- apply transl_initial_states.
- apply transl_final_states.
- apply transl_plus_step.
Qed.
End CORRECTNESS.
|
