-
Notifications
You must be signed in to change notification settings - Fork 5
/
UpperBound_B.v
1396 lines (1313 loc) · 57 KB
/
UpperBound_B.v
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
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
Require Import CoqlibC Maps.
Require Import ASTC Integers Floats Values MemoryC EventsC GlobalenvsC Smallstep.
Require Import Locations Stacklayout Conventions Linking.
(** newly added **)
Require Export Csem Cop Ctypes Ctyping Csyntax Cexec.
Require Import Simulation Memory ValuesC.
Require Import Skeleton ModSem Mod sflib SemProps.
Require Import CtypesC CsemC Sem Syntax LinkingC Program.
Require Import BehaviorsC.
Require Import CtypingC.
Set Implicit Arguments.
Local Opaque Z.mul.
Definition is_external (ge: genv) (s:Csem.state) : Prop :=
match s with
| Csem.Callstate fptr ty args k m =>
match Genv.find_funct ge fptr with
| Some f =>
match f with
| External ef targs tres cconv => is_external_ef ef = true
| _ => False
end
| None => False
end
| _ => False
end.
Definition internal_function_state (ge: genv) (s: Csem.state) : Prop :=
match s with
| Csem.Callstate fptr ty args k m =>
match Genv.find_funct ge fptr with
| Some f =>
match f with
| Internal func => type_of_fundef f = Tfunction Tnil type_int32s cc_default
| _ => False
end
| None => False
end
| _ => False
end.
Section PRESERVATION.
Inductive my_eq {A: Type} (x: A): A -> Prop :=
| my_eq_refl: my_eq x x.
Notation "a m= b" := (my_eq a b) (at level 10).
Ltac Eq :=
match goal with
| [ H1: ?a = ?b, H2: ?a = ?c |- _ ] =>
rewrite H1 in H2; inv H2; Eq
| [ H1: ?a m= ?b, H2: ?a m= ?c |- _ ] =>
rewrite H1 in H2; inv H2; Eq
| _ => idtac
end.
Section PLANB0.
(** ********************* linking *********************************)
Variable prog: Csyntax.program.
Let tprog : Syntax.program := List.map CsemC.module [prog].
(** ********************* genv *********************************)
Variable sk_tgt: Sk.t.
Hypothesis LINK_SK_TGT: link_sk tprog = Some sk_tgt.
Let skenv_link := Sk.load_skenv sk_tgt.
Hypothesis WTSK: Sk.wf sk_tgt.
Let SKEWF: SkEnv.wf skenv_link.
Proof.
eapply SkEnv.load_skenv_wf; et.
Qed.
Let ge := globalenv prog.
Let tge_ce : composite_env := prog_comp_env prog.
Let tge := load_genv tprog skenv_link.
Hypothesis MAIN_INTERNAL: forall st_src, Csem.initial_state prog st_src -> internal_function_state ge st_src.
Hypothesis WTPROG: wt_program prog.
Hypothesis WT_EXTERNAL:
forall id ef args res cc vargs m t vres m',
In (id, Gfun (External ef args res cc)) prog.(prog_defs) ->
external_call ef skenv_link vargs m t vres m' ->
wt_retval vres res.
Hypothesis CSTYLE_EXTERN:
forall id ef tyargs ty cc,
In (id, (Gfun (Ctypes.External ef tyargs ty cc))) prog.(prog_defs) ->
(ef_sig ef).(sig_cstyle).
Definition local_genv (p : Csyntax.program) :=
(SkEnv.revive ((SkEnv.project skenv_link) (CSk.of_program signature_of_function p))) p.
Inductive match_states : Csem.state -> Sem.state -> nat -> Prop :=
| match_states_intro
fr (st: Csem.state)
(FRAME: fr = Frame.mk (CsemC.modsem skenv_link prog) st):
match_states st (Sem.State [fr]) 1
| match_states_call
fptr tyf vargs k m args fr (st: Csem.state) cconv tres targs n
(STATE: st = (Csem.Callstate fptr tyf vargs k m))
(FRAME: fr = Frame.mk (CsemC.modsem skenv_link prog) st)
(SIG: exists skd, (Genv.find_funct skenv_link) fptr = Some skd
/\ Some (signature_of_type targs tres cconv) = Sk.get_csig skd)
(FPTR: (Args.fptr args) = fptr)
(ARGS: (Args.vs args) = vargs)
(MEM: (Args.m args) = m)
(NOTPROG: Genv.find_funct (local_genv prog) (Args.fptr args) = None)
(ORD: n = 0%nat):
match_states (Csem.Callstate fptr tyf vargs k m) (Callstate args [fr]) n
| match_states_init
st_src st_tgt
(INITSRC: Csem.initial_state prog st_src)
(INITTGT: initial_state tprog st_tgt):
match_states st_src st_tgt 0.
Let INCL: SkEnv.includes (Sk.load_skenv (CSk.of_program signature_of_function prog)) (CSk.of_program signature_of_function prog).
Proof. eapply includes_refl. Qed.
(** ********************* init_memory *********************************)
Variable m_init : mem.
Hypothesis INIT_MEM: (Sk.load_mem sk_tgt) = Some m_init.
Definition m_src_init := m_init.
Lemma prog_sk_tgt:
CSk.of_program signature_of_function prog = sk_tgt.
Proof.
unfold skenv_link, link_sk, link_list in LINK_SK_TGT; inversion LINK_SK_TGT. auto.
Qed.
Lemma SRC_INIT_MEM: Genv.init_mem prog = Some m_src_init.
Proof.
Local Transparent Linker_prog.
unfold Sk.load_mem in *.
eapply Genv.init_mem_match
with (ctx := tt) (match_fundef := top3) (match_varinfo := top2);
[| eapply INIT_MEM]. econs.
- rewrite <- prog_sk_tgt. ss.
remember (prog_defs prog) as l. clear Heql.
ginduction l; ss; ii; econs.
+ destruct a; ss; econs; eauto.
destruct g; ss; des_ifs; try (by (econs; eauto; econs)).
{ econs. ss. destruct v. ss. }
+ exploit IHl; eauto.
- split.
+ subst tprog; ss.
unfold link_sk, link_list in *; ss; unfold link_prog in *. des_ifs.
+ subst tprog.
unfold link_sk, link_list in *; ss; unfold link_prog in *. des_ifs.
Unshelve. all: econs.
Qed.
Lemma skenv_link_wf:
SkEnv.wf skenv_link.
Proof.
clear INIT_MEM. (unfold skenv_link; eapply SkEnv.load_skenv_wf). ss.
Qed.
Lemma proj_wf:
SkEnv.project_spec skenv_link (CSk.of_program signature_of_function prog) (SkEnv.project skenv_link (CSk.of_program signature_of_function prog)).
Proof.
eapply SkEnv.project_impl_spec.
unfold skenv_link.
rpapply link_includes; et.
{ unfold tprog. rewrite in_map_iff. esplits; et. ss. left; et. }
ss.
Qed.
Lemma match_ge_skenv_link :
Genv.match_genvs (fun fdef skdef => skdef_of_gdef signature_of_function ((globdef_of_globdef (V:=type)) fdef) = skdef) ge skenv_link.
Proof.
unfold ge, skenv_link. rewrite <- prog_sk_tgt. unfold Sk.load_skenv, Genv.globalenv. ss.
eapply Genv.add_globals_match; cycle 1.
{ econs; ss.
i. do 2 rewrite PTree.gempty. econs. }
ss. clear.
remember (prog_defs prog) as l.
clear Heql.
ginduction l; ss.
- econs.
- ii. destruct a. ss. econs; ss.
eapply IHl; eauto.
Qed.
Lemma symb_preserved id:
Senv.public_symbol (symbolenv (sem tprog)) id =
Senv.public_symbol (symbolenv (semantics prog)) id.
Proof.
destruct match_ge_skenv_link. ss.
unfold symbolenv. ss.
unfold Genv.public_symbol, proj_sumbool.
unfold Sk.load_skenv in *. ss.
unfold Genv.find_symbol in *. ss.
rewrite <- mge_symb. unfold skenv_link.
rewrite <- prog_sk_tgt. ss.
des_ifs.
unfold Genv.globalenv in *. ss. erewrite Genv.genv_public_add_globals in *. ss.
unfold Genv.globalenv in *. ss. erewrite Genv.genv_public_add_globals in *. ss.
Qed.
Lemma transf_initial_states:
forall st1, Csem.initial_state prog st1 ->
exists st2, Sem.initial_state tprog st2 /\ match_states st1 st2 0.
Proof.
destruct match_ge_skenv_link. destruct skenv_link_wf.
i. inversion H; subst.
assert (ge = ge0).
{ unfold ge, ge0. auto. }
subst ge0.
unfold tge, skenv_link, link_sk, link_list in *; inversion LINK_SK_TGT.
assert (Genv.find_funct (Sk.load_skenv sk_tgt) (Genv.symbol_address (Sk.load_skenv sk_tgt) (AST.prog_main sk_tgt) Ptrofs.zero) =
Some (AST.Internal signature_main)).
{ dup H.
eapply MAIN_INTERNAL in H.
ss. des_ifs.
unfold Genv.symbol_address.
unfold Genv.find_symbol in *.
unfold fundef in *. ss.
des_ifs; cycle 1.
{ rewrite <- mge_symb in H1.
unfold skenv_link in H1.
rewrite H1 in Heq0. clarify. }
ss. des_ifs. rewrite Genv.find_funct_ptr_iff in *.
unfold Genv.find_def in *.
rewrite mge_symb in Heq0.
assert (b = b0).
{ Eq. auto. } subst.
specialize (mge_defs b0). inv mge_defs.
{ rewrite Heq in H7. clarify. }
Eq. rewrite Heq in H6. inv H6. ss.
destruct f0; ss. unfold type_of_function in H. ss. inv H. destruct fn_params; ss.
destruct p. inv H8. }
esplits; eauto.
{ econs; et. i. ss. des; ss. clarify. }
{ econs; et. econs; et. i. ss. des; ss. clarify. }
Qed.
(** ********************* transf step *********************************)
Inductive valid_owner fptr (p: Csyntax.program) : Prop :=
| valid_owner_intro
fd
(MSFIND: tge.(Ge.find_fptr_owner) fptr (CsemC.modsem skenv_link p))
(FINDF: Genv.find_funct (local_genv p) fptr = Some (Internal fd)).
Lemma find_fptr_owner_determ
fptr ms0 ms1
(FIND0: Ge.find_fptr_owner tge fptr ms0)
(FIND1: Ge.find_fptr_owner tge fptr ms1):
ms0 = ms1.
Proof.
eapply SemProps.find_fptr_owner_determ; ss;
try rewrite LINK_SK_TGT; eauto.
{ ii. ss. des; ss. clarify. ss. unfold link_sk, link_list in *. ss. clarify. }
Qed.
Lemma alloc_variables_determ
g e m
vars e2 m2
e2' m2'
(ALLOCV1: alloc_variables g e m vars e2 m2)
(ALLOCV2: alloc_variables g e m vars e2' m2'):
e2' = e2 /\ m2' = m2.
Proof.
generalize dependent g.
generalize dependent e2'.
generalize dependent m2'.
induction 1; i; inv ALLOCV2; auto.
rewrite H in H7. inv H7. eapply IHALLOCV1 in H8. auto.
Qed.
Notation "'assign_loc'" := (assign_loc skenv_link) (only parsing).
Notation "'bind_parameters'" := (bind_parameters skenv_link) (only parsing).
Notation "'rred'" := (rred skenv_link) (only parsing).
Notation "'estep'" := (estep skenv_link) (only parsing).
Lemma assign_loc_determ
g ty m b
ofs v tr m1 m1'
(ASSIGN1: assign_loc g ty m b ofs v tr m1)
(ASSIGN2: assign_loc g ty m b ofs v tr m1'):
m1 = m1'.
Proof.
generalize dependent g.
generalize dependent m1'.
induction 1; i; inv ASSIGN2; f_equal; Eq; auto.
inv H1; inv H4. inv H5; inv H15; try congruence. Eq. auto.
Qed.
Lemma bind_parameters_determ
g env m l vl m1 m1'
(BIND1: bind_parameters g env m l vl m1)
(BIND2: bind_parameters g env m l vl m1'):
m1 = m1'.
Proof.
generalize dependent g.
generalize dependent m1'.
induction 1; i; inv BIND2; f_equal; Eq; auto.
determ_tac assign_loc_determ.
eapply IHBIND1; eauto.
Qed.
(** ********************* aux lemmas *********************************)
Lemma senv_equiv_ge_link:
Senv.equiv (Genv.globalenv prog) skenv_link.
Proof.
destruct match_ge_skenv_link.
econs; ss; splits.
- unfold skenv_link in *. unfold Genv.public_symbol in *. des_ifs; ss.
rewrite <- prog_sk_tgt in *.
i. des_ifs; ss; unfold Genv.find_symbol in *;
rewrite <- mge_symb in *; rewrite Heq0 in Heq; clarify.
unfold Genv.public_symbol in *. des_ifs; ss.
repeat rewrite Genv.globalenv_public in *. ss.
- unfold Genv.block_is_volatile in *. i.
des_ifs.
+ rewrite Genv.find_var_info_iff in *.
unfold skenv_link in *. rewrite <- prog_sk_tgt in *. ss.
unfold Genv.find_def in *;
specialize (mge_defs b); inv mge_defs; symmetry in H, H0; Eq; ss.
inv H2. destruct g0; ss.
+ unfold Genv.find_var_info in *.
des_ifs;
unfold Genv.find_def in *;
destruct (mge_defs b); clarify; des_ifs.
+ unfold Genv.find_var_info in *.
des_ifs;
unfold Genv.find_def in *;
destruct (mge_defs b); clarify; des_ifs.
Qed.
Lemma id_in_prog id:
defs prog id <-> In id (prog_defs_names prog).
Proof.
split; i; unfold defs, in_dec, ident_eq in *; destruct (prog_defs_names prog); ss; des_ifs; eauto.
inv H; clarify.
Qed.
Lemma id_not_in_prog id:
~ defs prog id <-> ~ In id (prog_defs_names prog).
Proof.
split; i; unfold not; i.
- rewrite <- id_in_prog in H0. clarify.
- rewrite id_in_prog in H0. clarify.
Qed.
Lemma not_prog_defmap_spec F V p id:
~ In id (prog_defs_names p) <-> ~ (exists g : globdef F V, (prog_defmap p) ! id = Some g).
Proof.
split; i; unfold not; i.
- des. eapply H. rewrite prog_defmap_spec. eauto.
- eapply H. rewrite prog_defmap_spec in H0. des. eauto.
Qed.
Lemma var_info_same
blk g
(VAR: Genv.find_var_info (Genv.globalenv prog) blk = Some g):
Genv.find_var_info (local_genv prog) blk = Some g
.
Proof.
destruct match_ge_skenv_link.
destruct skenv_link_wf. destruct proj_wf.
rewrite Genv.find_var_info_iff in *.
unfold Genv.find_def in *. ss.
repeat rewrite MapsC.PTree_filter_map_spec.
rewrite o_bind_ignore.
specialize (mge_defs blk). inv mge_defs.
{ rewrite VAR in H0. inv H0. }
symmetry in H0.
eapply DEFSYMB in H0. des. des_ifs.
- destruct (Genv.invert_symbol (SkEnv.project skenv_link (CSk.of_program signature_of_function prog)) blk) eqn:SYMINV; ss; cycle 1.
+ assert ((prog_defmap prog) ! id = Some x).
{ rewrite Genv.find_def_symbol. exists blk. splits.
unfold Genv.find_symbol in *. rewrite <- mge_symb. ss.
unfold Genv.find_def. ss. }
exploit SYMBKEEP; eauto.
{ instantiate (1 := id). rewrite CSk.of_program_defs.
rewrite id_in_prog. rewrite prog_defmap_spec. eauto. }
i. rewrite <- H2 in H0.
eapply Genv.find_invert_symbol in H0. clarify.
+ unfold o_bind; ss.
assert ((prog_defmap prog) ! id = Some x).
{ rewrite Genv.find_def_symbol. exists blk. splits.
unfold Genv.find_symbol in *. rewrite <- mge_symb. ss.
unfold Genv.find_def. ss. }
exploit SYMBKEEP; eauto.
{ instantiate (1 := id).
rewrite CSk.of_program_defs.
rewrite id_in_prog. rewrite prog_defmap_spec. eauto. } i. des.
rewrite <- H2 in H0.
exploit Genv.find_invert_symbol; eauto. i. rewrite H3 in SYMINV. inv SYMINV.
rewrite H1. ss. rewrite VAR in H. inv H. ss.
- unfold o_bind in Heq; ss.
exploit Genv.find_invert_symbol; eauto. i. rewrite H1 in Heq. ss.
rewrite VAR in *. clarify. des_ifs.
{ uo. unfold internals in *. des_ifs. }
unfold Genv.find_symbol in *. rewrite mge_symb in H0.
assert ((prog_defmap prog) ! id = Some (Gvar g)).
{ rewrite Genv.find_def_symbol. exists blk. splits; eauto. }
assert (In id (prog_defs_names prog)).
{ rewrite prog_defmap_spec. exists (Gvar g). auto. }
rewrite <- id_in_prog in H2. rewrite CSk.of_program_internals in *. unfold internals in Heq0. des_ifs.
Qed.
Lemma var_info_same'
blk g
(VAR: Genv.find_var_info (local_genv prog) blk = Some g):
Genv.find_var_info (Genv.globalenv prog) blk = Some g.
Proof.
destruct match_ge_skenv_link.
destruct skenv_link_wf. destruct proj_wf.
rewrite Genv.find_var_info_iff in *. dup VAR.
unfold Genv.find_def in VAR. ss.
repeat rewrite MapsC.PTree_filter_map_spec in VAR.
rewrite o_bind_ignore in VAR. des_ifs.
destruct ((Genv.genv_defs skenv_link) ! blk) eqn:LINKDEF; cycle 1.
{ unfold o_bind in *; ss. }
unfold o_bind in Heq; ss.
destruct (Genv.invert_symbol skenv_link blk) eqn:LINKINV; cycle 1; ss. des_ifs.
exploit Genv.invert_find_symbol; eauto. i.
exploit SYMBKEEP; eauto. { eapply internals_defs; et. } i. rewrite <- H0 in H.
exploit Genv.find_invert_symbol; eauto. i.
rewrite H1 in VAR. unfold o_bind in VAR; ss.
assert (defs prog i).
{ eapply internals_defs; et. erewrite <- CSk.of_program_internals; et. }
rewrite id_in_prog in H2. rewrite prog_defmap_spec in H2. des.
rewrite H2 in VAR. ss. des_ifs. ss.
exploit DEFKEEP; eauto. i. rewrite Genv.find_def_symbol in H2. des.
rewrite H in H0. unfold Genv.find_symbol in *. rewrite mge_symb in H0. rewrite <- H0 in H2. inv H2.
clarify.
Qed.
Lemma volatile_block_same
blk b
(VOLATILE: Genv.block_is_volatile (local_genv prog) blk = b):
Genv.block_is_volatile (Genv.globalenv prog) blk = b.
Proof.
destruct match_ge_skenv_link.
destruct skenv_link_wf. destruct proj_wf.
ss. unfold Genv.block_is_volatile in *. des_ifs; try (by (exploit var_info_same; eauto; i; clarify)).
exploit var_info_same'; eauto. i. rewrite H in Heq. clarify.
Qed.
Lemma volatile_block_same'
blk b
(VOLATILE: Genv.block_is_volatile (Genv.globalenv prog) blk = b):
Genv.block_is_volatile (local_genv prog) blk = b.
Proof.
destruct match_ge_skenv_link.
destruct skenv_link_wf. destruct proj_wf.
unfold Genv.block_is_volatile in *.
des_ifs.
- exploit var_info_same; eauto. i. Eq. clarify.
- exploit var_info_same'; eauto. i. rewrite Heq0 in H. clarify.
- exploit var_info_same; eauto. i. rewrite H in Heq. clarify.
Qed.
Lemma symbol_same id:
Genv.find_symbol (local_genv prog) id = Genv.find_symbol (Genv.globalenv prog) id.
Proof.
destruct match_ge_skenv_link.
destruct skenv_link_wf. destruct proj_wf.
unfold Genv.find_symbol; ss.
rewrite MapsC.PTree_filter_key_spec. des_ifs; ss.
destruct ((Genv.genv_symb (Genv.globalenv prog)) ! id) eqn:SYMB; ss.
exploit mge_symb. i. rewrite SYMB in H.
exploit SYMBDEF; eauto. i. des.
specialize (mge_defs b). inv mge_defs.
{ unfold Genv.find_def in H0. rewrite H0 in H3. clarify. }
assert (~ defs prog id).
{ rewrite CSk.of_program_defs in *. unfold not. i. inv H. clarify. }
exfalso. apply H3.
rewrite id_in_prog. rewrite prog_defmap_spec. exists x.
rewrite Genv.find_def_symbol. exists b. split; eauto.
Qed.
Lemma public_same id:
Genv.public_symbol {| genv_genv := (local_genv prog); genv_cenv := prog_comp_env prog |} id =
Genv.public_symbol (Genv.globalenv prog) id.
Proof.
destruct match_ge_skenv_link.
destruct skenv_link_wf. destruct proj_wf.
unfold Genv.public_symbol in *. des_ifs; ss.
- rewrite Genv.globalenv_public. ss.
- rewrite symbol_same in Heq. rewrite Heq in Heq0. clarify.
- rewrite symbol_same in Heq. rewrite Heq in Heq0. clarify.
Qed.
Lemma Senv_equiv1:
Senv.equiv (Genv.globalenv prog) {| genv_genv := (local_genv prog); genv_cenv := prog_comp_env prog |}.
Proof.
econs; splits.
- eapply symbol_same.
- eapply public_same.
- i. destruct (Senv.block_is_volatile (Genv.globalenv prog) b) eqn:VOLA;
eapply volatile_block_same'; eauto.
Qed.
Lemma Senv_equiv2:
Senv.equiv {| genv_genv := (local_genv prog); genv_cenv := prog_comp_env prog |} (Genv.globalenv prog).
Proof.
econs; splits; symmetry.
- eapply symbol_same.
- eapply public_same.
- i. destruct (Senv.block_is_volatile (Genv.globalenv prog) b) eqn:VOLA;
eapply volatile_block_same'; eauto.
Qed.
Lemma volatile_load_same chunk m' b ofs tr v:
volatile_load {| genv_genv := (local_genv prog); genv_cenv := prog_comp_env prog |} chunk
m' b ofs tr v
<-> volatile_load (globalenv prog) chunk m' b ofs tr v.
Proof.
split; i;
exploit volatile_load_preserved; eauto. eapply Senv_equiv2. eapply Senv_equiv1.
Qed.
Lemma deref_loc_same ty m' b ofs tr v:
deref_loc {| genv_genv := (local_genv prog); genv_cenv := prog_comp_env prog |} ty m' b ofs tr v
<-> deref_loc (globalenv prog) ty m' b ofs tr v.
Proof.
destruct match_ge_skenv_link.
split; intro DEREF;
inv DEREF; try (by econs; eauto);
econs 2; eauto.
- rewrite <- volatile_load_same; eauto.
- rewrite volatile_load_same; eauto.
Qed.
Lemma volatile_store_same chunk m b ofs v tr m':
volatile_store
{| genv_genv := (local_genv prog);
genv_cenv := prog_comp_env prog |} chunk m b ofs v tr m'
<-> volatile_store (globalenv prog) chunk m b ofs v tr m'.
Proof.
split; i;
exploit volatile_store_preserved; eauto. eapply Senv_equiv2. eapply Senv_equiv1.
Qed.
Lemma assign_loc_same ty m b ofs v tr m':
assign_loc
{| genv_genv := (local_genv prog);
genv_cenv := prog_comp_env prog |} ty m b ofs v tr m'
<-> assign_loc (globalenv prog) ty m b ofs v tr m'.
Proof.
destruct match_ge_skenv_link.
split; intro ASSIGN;
inv ASSIGN; try (by econs; eauto);
econs 2; eauto.
Qed.
Lemma bind_parameters_same e m1 params vl m2:
bind_parameters {| genv_genv := local_genv prog;
genv_cenv := prog_comp_env prog |} e m1 params vl m2
<-> bind_parameters (globalenv prog) e m1 params vl m2.
Proof.
destruct match_ge_skenv_link.
split; intro BPARAM.
- induction BPARAM; try econs; eauto.
rewrite assign_loc_same in H0. eauto.
- induction BPARAM; try econs; eauto.
rewrite <- assign_loc_same in H0. eauto.
Qed.
Lemma lred_same e a m a' m':
lred {| genv_genv := (local_genv prog); genv_cenv := prog_comp_env prog |} e a m a' m'
<-> lred (globalenv prog) e a m a' m'.
Proof.
destruct match_ge_skenv_link.
split; intro LRED;
inv LRED; try (by econs; eauto); econs 2; eauto.
- rewrite <- symbol_same; auto.
- rewrite symbol_same; auto.
Qed.
Lemma rred_same
a m tr a' m'
:
rred {| genv_genv := (local_genv prog); genv_cenv := prog_comp_env prog |} a m tr a' m'
<-> rred (globalenv prog) a m tr a' m'.
Proof.
destruct match_ge_skenv_link.
split; intro RRED.
- inv RRED; try (by econs); ss
; try (by (econs; eauto; rewrite <- deref_loc_same; eauto)).
+ econs; eauto. rewrite <- assign_loc_same; eauto.
- inv RRED; try (by econs); ss
; try (by (econs; eauto; rewrite deref_loc_same; eauto)).
+ econs; eauto. rewrite assign_loc_same; eauto.
Qed.
Lemma estep_same
st_src tr st0
(ESTEP: estep
{| genv_genv := (local_genv prog); genv_cenv := prog_comp_env prog |}
st_src tr st0):
estep (globalenv prog) st_src tr st0.
Proof.
destruct match_ge_skenv_link.
inv ESTEP; ss; try (by econs; eauto).
- econs; eauto.
rewrite <- lred_same; eauto.
- econs 2; eauto.
rewrite <- rred_same; eauto.
- econs; eauto.
unfold not in *. i. eapply H0.
inv H1; try (by econs); ss.
+ econs; eauto.
rewrite lred_same; eauto.
+ econs 4; eauto.
rewrite rred_same; eauto.
+ econs 5; eauto.
Qed.
Ltac o_bind_b :=
match goal with
| [ H : (do id <- ?stmt; ?next) = Some ?f |- _ ] => destruct stmt eqn:SYMB; clarify; unfold o_bind in *; ss
end.
Lemma def_same
b f
(DEF: Genv.find_def
{| genv_genv := (local_genv prog);
genv_cenv := prog_comp_env prog |} b = Some f):
Genv.find_def ge b = Some f.
Proof.
destruct match_ge_skenv_link.
destruct proj_wf. destruct skenv_link_wf.
ss. unfold Genv.find_def in DEF. ss.
repeat rewrite MapsC.PTree_filter_map_spec in DEF.
rewrite o_bind_ignore in DEF.
des_ifs. o_bind_b.
destruct ((prog_defmap prog)! i) eqn:PROGDEF; ss. des_ifs. ss.
exploit (SYMBKEEP i).
rewrite CSk.of_program_defs.
rewrite id_in_prog. rewrite prog_defmap_spec.
eauto. i.
exploit Genv.invert_find_symbol; eauto; i. Eq.
rewrite H in H0. exploit SYMBDEF; eauto. i. des.
rewrite Genv.find_def_symbol in PROGDEF. des.
unfold Genv.find_symbol in *. rewrite mge_symb in H0. Eq.
auto.
Qed.
Lemma function_find_same
fptr f
(FUNC: Genv.find_funct (local_genv prog) fptr = Some f):
Genv.find_funct ge fptr = Some f.
Proof.
unfold Genv.find_funct in FUNC. des_ifs.
rewrite Genv.find_funct_ptr_iff in FUNC.
exploit def_same; eauto. i. ss. des_ifs.
rewrite Genv.find_funct_ptr_iff. auto.
Qed.
Definition is_external_fd :=
fun (F : Type) (f : fundef) =>
match f with
| Internal _ => false
| External ef _ _ _ => is_external_ef ef
end.
Lemma not_external_function_find_same
f fptr
(INTERN : is_external_fd function f = false)
(FUNC : Genv.find_funct (Genv.globalenv prog) fptr = Some f):
Genv.find_funct (local_genv prog) fptr = Some f.
Proof.
destruct match_ge_skenv_link.
destruct proj_wf. destruct skenv_link_wf.
ss. unfold Genv.find_funct. des_ifs; cycle 1.
{ ss. des_ifs. }
ss. des_ifs.
rewrite Genv.find_funct_ptr_iff in *.
unfold Genv.find_def in *. ss.
specialize (mge_defs b). inv mge_defs.
{ rewrite FUNC in H0. clarify. }
repeat rewrite MapsC.PTree_filter_map_spec.
rewrite o_bind_ignore. des_ifs; cycle 1.
{ rewrite FUNC in H. inv H. rewrite <- H0 in Heq.
unfold o_bind in Heq; ss.
destruct (Genv.invert_symbol skenv_link b) eqn:SYMB; ss.
- assert (~ defs prog i).
{ des_ifs_safe; ss. ii. rewrite CSk.of_program_internals in *. unfold internals, defs in *. des_sumbool.
apply prog_defmap_spec in H. des. des_ifs_safe. ss.
destruct (is_external_gd g) eqn:ISEXT; ss; cycle 1.
{ uo. generalize (CSk.of_program_prog_defmap prog signature_of_function i). intro REL.
inv REL; ss; try congruence. des_ifs. }
apply Genv.find_def_symbol in Heq0. des. uge. clarify.
apply Genv.invert_find_symbol in SYMB. uge.
assert(b0 = b).
{ rewrite mge_symb in *. clarify. }
clarify.
clear - INTERN ISEXT. bsimpl. ss. destruct f; ss. clarify. }
exploit Genv.invert_find_symbol; eauto. i.
unfold Genv.find_symbol in *. rewrite mge_symb in H1.
assert ((prog_defmap prog) ! i = Some (Gfun f)).
{ rewrite Genv.find_def_symbol. exists b.
splits. unfold Genv.find_symbol in *. auto.
auto. }
rewrite id_not_in_prog in H. rewrite not_prog_defmap_spec in H.
exfalso. apply H. exists (Gfun f). auto.
- exploit DEFSYMB; eauto. i. des.
exploit Genv.find_invert_symbol; eauto. i. Eq. }
rewrite <- H0 in Heq. unfold o_bind in Heq. ss.
dup H.
rewrite FUNC in H. inv H.
exploit DEFSYMB; eauto. i. des.
exploit Genv.find_invert_symbol; eauto. i. rewrite H2 in Heq. ss.
assert (defs prog id).
{ rewrite CSk.of_program_internals in *. des_ifs_safe. eapply internals_defs; et. }
exploit (SYMBKEEP id); ss. { rewrite CSk.of_program_defs; ss. } i.
dup H. rewrite <- H4 in H.
exploit Genv.find_invert_symbol. eapply H. i. rewrite H6.
unfold o_bind. ss. rewrite id_in_prog in H3. rewrite prog_defmap_spec in H3. des.
rewrite H3. ss.
assert ((prog_defmap prog) ! id = Some (Gfun f)).
{ rewrite Genv.find_def_symbol. exists b.
splits. unfold Genv.find_symbol in *. rewrite <- mge_symb. auto.
auto. }
Eq. ss.
Qed.
Notation "'sstep'" := (sstep skenv_link) (only parsing).
Lemma sstep_same
st_src tr st0
(SSTEP: sstep
{| genv_genv := (local_genv prog); genv_cenv := prog_comp_env prog |}
st_src tr st0):
sstep (globalenv prog) st_src tr st0.
Proof.
inv SSTEP; ss; try (by econs; eauto).
- (* internal call *)
econs; eauto.
+ exploit function_find_same; eauto.
+ instantiate (1 := m1).
clear -H0. induction H0; try (by econs).
econs; eauto.
+ induction H1; try (by econs).
econs; eauto.
rewrite assign_loc_same in H2. eauto.
rewrite bind_parameters_same in H3. eauto.
- (* external call *)
econs; eauto; ss.
exploit function_find_same; eauto.
Qed.
Lemma cstep_same
st_src tr st0
(STEP: Csem.step skenv_link
{| genv_genv := (local_genv prog); genv_cenv := prog_comp_env prog |}
st_src tr st0):
Csem.step skenv_link (globalenv prog) st_src tr st0.
Proof.
inv STEP.
- econs. exploit estep_same; eauto.
- econs 2. exploit sstep_same; eauto.
Qed.
Lemma system_internal
ptr fn_sig f
(SYSCALL: Genv.find_funct (System.skenv skenv_link) ptr = Some (AST.Internal fn_sig))
(INTERNAL: Genv.find_funct ge ptr = Some (Internal f)):
False.
Proof.
destruct match_ge_skenv_link.
unfold System.skenv in SYSCALL. ss. unfold skenv_link in *.
unfold Genv.find_funct in *. des_ifs. rewrite Genv.find_funct_ptr_iff in *.
unfold Genv.find_def in *. ss. rewrite MapsC.PTree_filter_map_spec in SYSCALL.
specialize (mge_defs b). inv mge_defs; unfold fundef in *.
{ rewrite INTERNAL in H0. clarify. }
rewrite INTERNAL in H. inv H. ss. rewrite <- H0 in SYSCALL. ss.
Qed.
Lemma estep_progress
st_src tr st0
(ESTEP: estep (globalenv prog) st_src tr st0):
estep
{| genv_genv := (local_genv prog); genv_cenv := prog_comp_env prog |}
st_src tr st0.
Proof.
destruct match_ge_skenv_link.
inv ESTEP; try (by econs; eauto).
- econs; eauto.
rewrite lred_same; eauto.
- econs 2; eauto.
rewrite rred_same; eauto.
- econs; eauto.
unfold not in *. i. eapply H0.
inv H1; try (by econs); ss.
+ econs; eauto.
rewrite <- lred_same; eauto.
+ econs 4; eauto.
rewrite <- rred_same; eauto.
+ econs 5; eauto.
Qed.
Lemma sstep_progress
st_src tr st0
(INTERN: ~ is_external ge st_src)
(SSTEP: sstep (globalenv prog) st_src tr st0):
sstep
{| genv_genv := (local_genv prog); genv_cenv := prog_comp_env prog |}
st_src tr st0.
Proof.
destruct match_ge_skenv_link.
inv SSTEP; try (by econs; eauto).
- eapply step_internal_function; eauto.
+ exploit not_external_function_find_same; eauto. ss.
+ instantiate (1 := m1).
clear -H0. induction H0; try (by econs).
econs; eauto.
+ induction H1; try (by econs).
exploit bind_parameters_same. i.
rewrite H4. ss. econs; eauto.
- econs; eauto; ss.
+ des_ifs.
exploit not_external_function_find_same; eauto.
ss. destruct ef; ss.
Unshelve. all: auto.
Qed.
Lemma senv_same : ((Genv.globalenv prog): Senv.t) = (skenv_link: Senv.t).
Proof.
generalize match_ge_skenv_link; intro MGE.
clear - skenv_link LINK_SK_TGT MGE.
subst skenv_link. ss. unfold Sk.load_skenv in *. subst tprog. unfold link_sk in *. ss.
unfold link_list in *. ss. clarify.
inv MGE. apply senv_eta; ss.
- uge. apply func_ext1. i. ss.
- unfold Genv.public_symbol. uge. apply func_ext1. i. specialize (mge_symb x0). rewrite mge_symb. des_ifs.
rewrite mge_pubs. ss.
- apply func_ext1. i.
destruct (Genv.invert_symbol (Genv.globalenv prog) x0) eqn:T.
+ apply Genv.invert_find_symbol in T. symmetry. apply Genv.find_invert_symbol. uge. rewrite mge_symb. ss.
+ destruct (Genv.invert_symbol (Genv.globalenv (CSk.of_program signature_of_function prog)) x0) eqn:U; ss.
apply Genv.invert_find_symbol in U. specialize (mge_symb i). uge. rewrite mge_symb in *.
apply Genv.find_invert_symbol in U. congruence.
- unfold Genv.block_is_volatile, Genv.find_var_info. apply func_ext1. i.
specialize (mge_defs x0). uge. inv mge_defs; ss.
destruct x; ss. des_ifs.
Qed.
Lemma progress_step
st_src frs n t st_src'
(INTERN: ~ is_external ge st_src)
(MTCHST : match_states st_src (State frs) n)
(STEP: Step (semantics prog) st_src t st_src'):
exists (tr : trace) (st_tgt1 : Smallstep.state (sem tprog)), Step (sem tprog) (State frs) tr st_tgt1.
Proof.
inv MTCHST; inv STEP; ss; exists t.
- esplits. econs; ss. econs 1. exploit estep_progress; eauto. rewrite <- senv_same. eauto.
- esplits. econs; ss. econs 2. exploit sstep_progress; eauto. rewrite <- senv_same. eauto.
- inv INITSRC; inv INITTGT; inv H.
- inv INITSRC; inv INITTGT; inv H.
Qed.
Lemma init_case st args frs fptr tr st_src st_src'
(STATE: st = Callstate args frs)
(FPTR: fptr = (Args.fptr args))
(MTCHST: match_states st_src st 0)
(SAFESRC: Step (semantics prog) st_src tr st_src'):
(<<CMOD: valid_owner fptr prog>>) \/
(<<SYSMOD: tge.(Ge.find_fptr_owner)
fptr (System.modsem skenv_link)>>).
Proof.
subst.
destruct (classic (valid_owner (Args.fptr args) prog)); eauto.
right. inv MTCHST.
(* syscall *)
- inv SAFESRC; inv H0.
+ ss. exploit not_external_function_find_same; eauto. ss.
i. unfold local_genv in *. Eq.
+ econs.
* unfold tge. ss. left. eauto.
* destruct match_ge_skenv_link.
ss. des.
unfold local_genv in NOTPROG.
unfold System.skenv.
unfold Genv.find_funct in *. des_ifs.
rewrite Genv.find_funct_ptr_iff in *.
specialize (mge_defs b).
inv mge_defs; unfold Genv.find_def in *; unfold fundef in *.
{ rewrite FPTR in H1. clarify. }
rewrite FPTR in H0. inv H0. ss. rewrite SIG in H1. inv H1.
rewrite MapsC.PTree_filter_map_spec. rewrite SIG.
unfold o_bind. ss.
(* initial state *)
- inv INITTGT; ss.
assert (SAME: sk_link = sk_tgt).
{ rewrite LINK_SK_TGT in INITSK. clarify. }
clear INITSK.
destruct proj_wf. destruct match_ge_skenv_link.
exploit MAIN_INTERNAL; eauto. intros MAIN_INTERN.
inv INITSRC; inv SAFESRC; inv H4.
+ exploit not_external_function_find_same; eauto. ss. i.
ss. des_ifs. exfalso. eapply H.
unfold Genv.symbol_address in *.
repeat (ss; des_ifs).
assert (b = b0).
{ unfold Genv.find_symbol in *. unfold skenv_link in *.
rewrite <- mge_symb in H1. rewrite <- prog_sk_tgt in *. ss.
rewrite Heq0 in H1. inversion H1. auto. } subst b0.
assert (Genv.find_funct_ptr (Genv.globalenv prog) b = Some (Internal f)
<-> Genv.find_funct (SkEnv.project skenv_link (CSk.of_program signature_of_function prog))
(Genv.symbol_address (Sk.load_skenv sk_tgt) (AST.prog_main sk_tgt) Ptrofs.zero)
= Some (AST.Internal signature_main)).
{ i. ss. des_ifs.
unfold Genv.symbol_address in *.
des_ifs.
unfold Genv.find_funct in *. des_ifs. rewrite Genv.find_funct_ptr_iff in *.
unfold Genv.find_symbol in *. unfold skenv_link in *.
assert (PROGDEF: defs prog (prog_main prog)).
{ rewrite id_in_prog. rewrite prog_defmap_spec. ss.
eexists. erewrite Genv.find_def_symbol. esplits; eauto. }
exploit DEFKEEP; eauto.
{ exploit Genv.find_invert_symbol. unfold Genv.find_symbol. eapply Heq1.
rewrite <- prog_sk_tgt in *. ss. eauto. }
{ rewrite CSk.of_program_internals. unfold internals. rename b into bb.
hexploit (Genv.find_def_symbol prog (prog_main prog) (Gfun (Internal f))); et. intro T; des.
exploit T0; et. i. des_ifs. }
i. unfold Genv.find_funct_ptr. des. rewrite DEFSMALL. inv LO; ss. inv H7; ss.
}
econs; i; eauto.
econs; i; ss; eauto. des_ifs.
unfold Genv.symbol_address in *.
des_ifs. erewrite <- H5. eauto.
+ set (if_sig := (mksignature (typlist_of_typelist targs) (Some (typ_of_type tres)) cc true)).
econs; ss; auto.
instantiate (1:= if_sig). des_ifs.
Qed.
Lemma prog_precise:
SkEnv.genv_precise (SkEnv.revive (SkEnv.project skenv_link (CSk.of_program signature_of_function prog)) prog) prog.
Proof.
eapply CSkEnv.project_revive_precise; eauto.
exploit SkEnv.project_impl_spec. eauto. ii. red in H. unfold skenv_link. rewrite <- prog_sk_tgt. eauto.
Qed.
Lemma preservation_prog
st0 tr st1
(WT: wt_state prog ge st0)
(STEP: Csem.step skenv_link ge st0 tr st1):
<<WT: wt_state prog ge st1>>.
Proof.
eapply Ctyping.preservation; try apply STEP; try refl; eauto; et; destruct prog_precise.
- ii. eapply Genv.find_def_symbol. esplits; eauto.
- i. rewrite Genv.find_def_symbol in MAP. des; eauto.
- i.
destruct match_ge_skenv_link.
specialize (mge_defs blk). inv mge_defs; unfold Genv.find_def in *.
+ unfold ge in DEF. unfold fundef in *.
symmetry in H0. unfold fundef, genv_genv in *. ss. Eq.
+ unfold ge in DEF. unfold fundef in *.
symmetry in H. unfold fundef, genv_genv in *. ss.
Eq. symmetry in H0.
destruct SKEWF.
exploit DEFSYMB; eauto. i. des.
unfold Genv.find_symbol in *. rewrite mge_symb in H. eauto.
Qed.
Lemma match_state_xsim:
forall st_src st_tgt n (MTCHST: match_states st_src st_tgt n),
xsim (Csem.semantics prog) (Sem.sem tprog) lt (wt_state prog ge) top1 n%nat st_src st_tgt.
Proof.
pcofix CIH. i. pfold.
destruct match_ge_skenv_link.
destruct st_tgt.
(* call state *)
- inversion MTCHST; subst.
(* syscall *)
+ left. right. econs; i. econs; i; cycle 1.
* inv FINALSRC.
* econs; i.
(* step *)
-- exploit init_case; eauto. i. des.
{ inv CMOD. clarify. }
assert (CSTYLEARGS: exists fptr vs m, args = Args.Cstyle fptr vs m).
{ inv SYSMOD; ss. destruct args; ss. eauto. }
des; subst args; econs; i.
esplits.
++ left. split; cycle 1. {
(* receptive *)
-- econs.
++ i. inv H; inv H1; ss; clarify.
{ inv H0. eexists. econs 2.
eapply step_internal_function; eauto. }
{ exploit external_call_receptive; eauto. i. des.
eexists. econs 2.
eapply step_external_function; eauto. }