-
Notifications
You must be signed in to change notification settings - Fork 5
/
LowerBound.v
2413 lines (2229 loc) · 102 KB
/
LowerBound.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 Events Globalenvs Smallstep.
Require Import Locations Stacklayout Conventions Linking.
(** newly added **)
Require Export Asm.
Require Import Simulation Memory ValuesC.
Require Import Skeleton ModSem Mod sflib StoreArguments StoreArgumentsProps AsmC AsmregsC Sem Syntax LinkingC Program SemProps.
Require Import GlobalenvsC Lia LinkingC2 mktac MemdataC LocationsC AsmStepInj LowerBoundExtra IdSimExtra.
Set Implicit Arguments.
Local Opaque Z.mul.
Record sub_match_genvs A B V W (R: globdef A V -> globdef B W -> Prop)
(ge1: Genv.t A V) (ge2: Genv.t B W): Prop :=
{ sub_mge_next : Ple (Genv.genv_next ge1) (Genv.genv_next ge2);
sub_mge_symb id b (FIND: Genv.find_symbol ge1 id = Some b):
Genv.find_symbol ge2 id = Some b;
sub_mge_defs b d0 (FIND: Genv.find_def ge1 b = Some d0):
exists d1, <<FIND: Genv.find_def ge2 b = Some d1>> /\ <<MATCHDEF: R d0 d1>>; }.
Definition match_prog (sk: Sk.t) (tprog: Asm.program) : Prop
:= @match_program
_ _ _ _ (Linking.Linker_fundef signature) Linker_unit
(fun cu tf f => tf = AST.transf_fundef fn_sig f) eq sk tprog.
Lemma module_match_prog p:
match_prog (AsmC.module p) p.
Proof.
specialize (@match_transform_program _ _ unit _ _ (transf_fundef fn_sig) p).
unfold match_prog.
replace (Mod.sk (module p)) with
(transform_program (transf_fundef fn_sig) p); cycle 1.
{ unfold module, Sk.of_program, transform_program, transf_fundef. ss. f_equal.
unfold skdefs_of_gdefs, skdef_of_gdef, update_snd. f_equal.
extensionality i. destruct i. ss. des_ifs. destruct v. repeat f_equal.
destruct gvar_info. refl. }
generalize (transform_program (transf_fundef fn_sig) p). i.
inv H. des. econs; eauto.
eapply list_forall2_rev. eapply list_forall2_imply; eauto.
i. inv H4. inv H6; splits; eauto; ss.
- econs; eauto.
instantiate (1:=mkprogram nil nil p0.(prog_main)).
econs; splits; eauto; ss.
i. eapply in_prog_defmap in H6. ss.
- econs; eauto. inv H8. ss.
Qed.
Lemma link_success progs sk
(LINK_SK: link_sk (List.map AsmC.module progs) = Some sk):
exists tprog, link_list progs = Some tprog /\ match_prog sk tprog.
Proof.
assert((@link_list _ (@Linker_prog _ _ (Linking.Linker_fundef signature) _)
(map Mod.sk (map module progs))) = Some sk).
{ unfold link_sk, link_list in *. des_ifs_safe.
eapply (@stricter_link_list_aux _ (@Linker_prog (AST.fundef signature) unit (Linking.Linker_fundef signature) Linker_unit) (@Linker_prog (AST.fundef signature) unit Linker_skfundef Linker_unit)) in Heq.
- rewrite Heq. auto.
- clear Heq.
Local Transparent Linker_prog Linker_def Linking.Linker_fundef Linker_skfundef.
i. ss. unfold link_prog, proj_sumbool, andb in *. des_ifs_safe.
assert (FORALL: @PTree_Properties.for_all
_ (prog_defmap x0) (@link_prog_check _ _ (Linking.Linker_fundef signature) _ x0 x1)
= true).
+ rewrite PTree_Properties.for_all_correct in Heq0.
rewrite PTree_Properties.for_all_correct.
i. unfold link_prog_check, proj_sumbool, andb in *. des_ifs_safe.
exploit Heq0; eauto. i. des_ifs.
ss. unfold link_def in *. des_ifs.
ss. unfold link_skfundef, Linking.link_fundef in *. des_ifs.
+ rewrite FORALL. f_equal. f_equal. eapply PTree.elements_extensional.
i. erewrite PTree.gcombine; eauto. erewrite PTree.gcombine; eauto.
rewrite PTree_Properties.for_all_correct in Heq0.
rewrite PTree_Properties.for_all_correct in FORALL.
unfold link_prog_merge. des_ifs.
exploit Heq0; eauto. i. exploit FORALL; eauto. i. clear Heq0 FORALL.
unfold link_prog_check, proj_sumbool, andb in *. des_ifs.
ss. unfold link_def in *. des_ifs.
ss. unfold link_skfundef, Linking.link_fundef in *. des_ifs. }
clear LINK_SK. rename H into LINK_SK.
eapply (@link_list_match (AST.program (AST.fundef signature) unit) Asm.program (@Linker_prog (AST.fundef signature) unit (Linking.Linker_fundef signature) Linker_unit)); eauto.
- eapply (@TransfTotalLink_rev function signature unit Linker_unit fn_sig).
- rewrite list_map_compose. clear LINK_SK.
induction progs; ss.
+ econs.
+ econs; ss.
eapply module_match_prog.
Qed.
Section PRESERVATION.
(** ********************* linking *********************************)
Variable progs : list Asm.program.
Let prog : Syntax.program := List.map AsmC.module progs.
Hypothesis (WFSK: forall md (IN: In md prog), <<WF: Sk.wf md>>).
Variable tprog : Asm.program.
Hypothesis LINK : link_list progs = Some tprog.
(** ********************* genv *********************************)
Variable sk : Sk.t.
Hypothesis LINK_SK : link_sk prog = Some sk.
Let skenv_link := Sk.load_skenv sk.
Let ge := load_genv prog skenv_link.
Let tge := Genv.globalenv tprog.
Let WFSKLINK: Sk.wf sk. eapply link_list_preserves_wf_sk; et. Qed.
Let WFSKELINK: SkEnv.wf skenv_link.
Proof. eapply SkEnv.load_skenv_wf. ss. Qed.
Let ININCL: forall p (IN: In p prog), <<INCL: SkEnv.includes skenv_link p.(Mod.sk)>>.
Proof. eapply link_includes; et. Qed.
Definition local_genv (p : Asm.program) :=
(skenv_link.(SkEnv.project) p.(Sk.of_program fn_sig)).(SkEnv.revive) p.
Lemma match_genvs_sub A B V W R (ge1: Genv.t A V) (ge2: Genv.t B W)
(MATCHGE: Genv.match_genvs R ge1 ge2):
sub_match_genvs R ge1 ge2.
Proof.
inv MATCHGE. econs; i; ss; eauto.
- rewrite mge_next. refl.
- etrans; eauto.
- unfold Genv.find_def in *. specialize (mge_defs b).
inv mge_defs; eq_closure_tac. eauto.
Qed.
Lemma match_genvs_le A B V W R1 R2 (ge1: Genv.t A V) (ge2: Genv.t B W)
(MATCHGE: Genv.match_genvs R1 ge1 ge2)
(LE: R1 <2= R2):
Genv.match_genvs R2 ge1 ge2.
Proof.
inv MATCHGE. econs; i; ss; eauto.
cinv (mge_defs b).
- econs 1.
- econs 2. eapply LE; eauto.
Qed.
Definition genv_le (ge_src ge_tgt: Genv.t fundef unit): Prop :=
sub_match_genvs (@def_match _ _) ge_src ge_tgt.
Lemma skenv_link_public_eq id:
Genv.public_symbol skenv_link id = Senv.public_symbol (symbolenv (sem prog)) id.
Proof.
ss. des_ifs.
Qed.
Lemma MATCH_PROG:
match_prog sk tprog.
Proof. exploit link_success; eauto. i. des. clarify. Qed.
Lemma public_eq:
prog_public sk = prog_public tprog.
Proof. cinv MATCH_PROG. des. eauto. Qed.
Lemma genv_public_eq:
Genv.genv_public skenv_link = Genv.genv_public tge.
Proof.
unfold skenv_link, tge.
repeat rewrite Genv.globalenv_public.
eapply public_eq.
Qed.
Lemma main_eq:
prog_main sk = prog_main tprog.
Proof. cinv MATCH_PROG. des. eauto. Qed.
Lemma match_skenv_link_tge :
Genv.match_genvs (fun skdef fdef => skdef_of_gdef fn_sig fdef = skdef) skenv_link tge.
Proof.
set (Genv.globalenvs_match MATCH_PROG).
eapply match_genvs_le; eauto.
ii. inv PR; ss.
- des_ifs.
- inv H. ss. repeat f_equal. destruct i2. auto.
Qed.
Lemma sub_match_local_genv ge_local
(MATCHGE: genv_le ge_local tge):
sub_match_genvs (fun fdef skdef => def_match (skdef_of_gdef fn_sig fdef) (skdef)) ge_local skenv_link.
Proof.
destruct match_skenv_link_tge. inv MATCHGE.
unfold Genv.find_symbol, Genv.find_def in *. econs.
- rewrite <- mge_next. eauto.
- i. eapply sub_mge_symb0 in FIND.
rewrite mge_symb in FIND. eauto.
- i. eapply sub_mge_defs0 in FIND. des.
specialize (mge_defs b). inv mge_defs.
+ eq_closure_tac.
+ eq_closure_tac. esplits; eauto.
inv MATCHDEF; ss; des_ifs; econs.
Qed.
Inductive valid_owner fptr (p: Asm.program) : Prop :=
| valid_owner_intro
fd
(MSFIND: ge.(Ge.find_fptr_owner) fptr (AsmC.modsem skenv_link p))
(FINDF: Genv.find_funct (local_genv p) fptr = Some (Internal fd))
(PROGIN: In (AsmC.module p) prog).
Lemma owner_genv_le p
(IN: In (AsmC.module p) prog):
genv_le (local_genv p) tge.
Proof.
unfold ge in *.
unfold load_modsems, flip, Mod.modsem, skenv_link, Sk.load_skenv, prog in *. ss.
eapply in_map_iff in IN. des. clarify. apply inj_pair2 in H0. destruct H0. unfold local_genv.
assert(INCL: SkEnv.includes (Genv.globalenv sk) (Sk.of_program fn_sig x)).
{ exploit link_includes; et.
{ rewrite in_map_iff. esplits; et. }
i. ss. }
cinv match_skenv_link_tge.
cinv (@SkEnv.project_impl_spec skenv_link x.(Sk.of_program fn_sig) INCL).
unfold skenv_link in *.
assert (SKWF: SkEnv.wf_proj (SkEnv.project (Genv.globalenv sk) x.(Sk.of_program fn_sig))).
{ eapply SkEnv.project_spec_preserves_wf.
- eapply SkEnv.load_skenv_wf. et.
- eapply SkEnv.project_impl_spec; et. }
exploit SkEnv.project_revive_precise; eauto.
{ eapply SkEnv.project_impl_spec; et. }
i. inv H. econs; ss; i.
- unfold fundef in *. rewrite mge_next. refl.
- unfold Genv.find_symbol in *. rewrite mge_symb.
destruct (classic (defs x id)).
+ exploit SYMBKEEP; et.
{ erewrite Sk.of_program_defs; et. }
i; des. ss. congruence.
+ exploit SYMBDROP; et.
{ erewrite Sk.of_program_defs; et. }
i; des. ss. congruence.
- dup FIND. unfold SkEnv.revive in FIND.
eapply Genv_map_defs_def in FIND. des. gesimpl.
destruct (Genv.invert_symbol skenv_link b) eqn:EQ; cycle 1.
{ eapply DEFORPHAN in EQ. des. clarify. }
exploit GE2P; et. i; des. uo. des_ifs.
assert(TMP: Genv.find_symbol (SkEnv.project (Genv.globalenv sk) (Sk.of_program fn_sig x)) id = Some b).
{ uge. unfold SkEnv.revive in SYMB. ss. }
assert(TMP0: Genv.find_symbol (Genv.globalenv sk) id = Some b).
{ unfold SkEnv.project in TMP. rewrite Genv_map_defs_symb in TMP. ss.
unfold Genv.find_symbol in TMP. ss.
rewrite MapsC.PTree_filter_key_spec in *. des_ifs. }
assert(id = i0).
{ apply Genv.find_invert_symbol in TMP. clarify. } clarify.
assert(i = i0).
{ apply Genv.find_invert_symbol in TMP0. unfold skenv_link in EQ. clarify. } clarify.
hexploit (link_list_linkorder _ LINK); et. intro LO; des. rewrite Forall_forall in *.
specialize (LO x IN0).
Local Transparent Linker_prog. ss.
Local Opaque Linker_prog. des.
exploit LO1; et. i; des.
assert(INT: ~ASTC.is_external d0) by ss.
assert(INT0: ~ASTC.is_external gd2).
{ Local Transparent Linker_def. inv H0.
- inv H2; ss.
- inv H2; ss. }
exists gd2. splits; eauto.
+ apply Genv.find_def_symbol in H. des.
assert(b0 = b).
{ apply Genv.invert_find_symbol in EQ. uge. rewrite mge_symb in H. unfold skenv_link in EQ. clarify. }
clarify.
+ inv H0; ss.
* inv H2; ss.
* inv H2; ss. destruct info1, info2. econs.
Qed.
Lemma symb_preserved id:
Senv.public_symbol (symbolenv (semantics tprog)) id =
Senv.public_symbol (symbolenv (sem prog)) id.
Proof.
rewrite <- skenv_link_public_eq. ss.
unfold Genv.public_symbol in *.
cinv match_skenv_link_tge.
fold tge. ss. unfold fundef.
unfold Genv.find_symbol in *. rewrite mge_symb.
des_ifs. rewrite genv_public_eq. auto.
Qed.
Lemma symb_main :
Genv.find_symbol skenv_link (prog_main sk) =
Genv.find_symbol tge (prog_main tprog).
Proof.
unfold Genv.find_symbol in *.
cinv match_skenv_link_tge.
rewrite mge_symb. f_equal.
eapply main_eq.
Qed.
Lemma local_global_consistent
ge_local
(LE: genv_le ge_local tge)
fptr fd
(LOCAL: Genv.find_funct ge_local fptr = Some (Internal fd))
skd
(GLOBAL: Genv.find_funct skenv_link fptr = Some skd):
Sk.get_sig skd = fd.(fn_sig).
Proof.
inv LE. unfold Genv.find_funct, Genv.find_funct_ptr, Genv.find_def in *. des_ifs.
cset sub_mge_defs0 Heq0. des.
cinv match_skenv_link_tge.
cinv (mge_defs b).
- rewrite Heq in *. clarify.
- rewrite Heq in *. clarify.
unfold skdef_of_gdef, fundef in *. rewrite FIND in *. inv MATCHDEF.
des_ifs.
Qed.
(** ********************* initial memory *********************************)
Variable m_init : mem.
Hypothesis INIT_MEM: sk.(Sk.load_mem) = Some m_init.
Definition m_tgt_init := m_init.
Lemma TGT_INIT_MEM: Genv.init_mem tprog = Some m_tgt_init.
Proof.
Local Transparent Linker_prog.
unfold Sk.load_mem in *.
eapply (Genv.init_mem_match MATCH_PROG). eauto.
Qed.
Definition init_inject := Mem.flat_inj (Mem.nextblock m_init).
Lemma initmem_inject: Mem.inject init_inject m_init m_tgt_init.
Proof.
eapply Genv.initmem_inject. unfold Sk.load_mem in INIT_MEM. eauto.
Qed.
Lemma init_inject_ge :
skenv_inject skenv_link init_inject m_init.
Proof.
unfold init_inject, Mem.flat_inj. econs; i; ss.
- unfold Sk.load_mem in *.
erewrite <- Genv.init_mem_genv_next; eauto.
unfold skenv_link, Sk.load_skenv in *. des_ifs.
- des_ifs; eauto.
Qed.
(* TODO: remove redundancy with from UpperBound_B.v. *)
Lemma senv_same :
(tge: Senv.t) = (skenv_link: Senv.t).
Proof.
generalize match_skenv_link_tge; intro MGE.
clear - MGE.
subst skenv_link. ss. unfold Sk.load_skenv in *. subst tge. unfold link_sk in *. ss.
inv MGE. unfold fundef in *.
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 (AST.fundef function) unit tprog) 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 sk) 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 y; ss. des_ifs.
Qed.
Lemma system_symbols_inject j m
(SKINJ: skenv_inject skenv_link j m):
symbols_inject_weak j (System.globalenv skenv_link) skenv_link m.
Proof.
destruct match_skenv_link_tge. inv SKINJ.
unfold System.globalenv.
rr. esplits; ss.
- i. exploit Genv.genv_symb_range; eauto. intro NB.
exploit DOMAIN; et. i; clarify.
- i. exploit Genv.genv_symb_range; eauto.
- ii. destruct (Genv.block_is_volatile skenv_link b1) eqn:VEQ0.
+ eauto.
+ destruct (Genv.block_is_volatile skenv_link b2) eqn:VEQ1; auto.
right. split; auto. ii.
exploit IMAGE; eauto.
* right. exists ofs. eapply Mem.perm_max.
eapply Mem.perm_implies; eauto. econs.
* i. clarify.
Qed.
Section SYSTEM.
Lemma system_function_ofs j b_src b_tgt delta fd m
(SKINJ: skenv_inject skenv_link j m)
(FIND: Genv.find_funct_ptr (System.globalenv skenv_link) b_src = Some fd)
(INJ: j b_src = Some (b_tgt, delta)):
delta = 0.
Proof.
inv SKINJ. exploit DOMAIN.
- instantiate (1:=b_src). clear - FIND WFSKLINK.
unfold System.globalenv in *.
unfold Genv.find_funct_ptr in *. des_ifs.
assert (SkEnv.wf skenv_link).
{ apply SkEnv.load_skenv_wf; et. }
inv H. unfold Genv.find_symbol in *.
exploit DEFSYMB; eauto. i. des.
eapply Genv.genv_symb_range; eauto.
- i. clarify.
Qed.
Lemma system_sig j b_src b_tgt delta ef m
(SKINJ: skenv_inject skenv_link j m)
(FIND: Genv.find_funct_ptr (System.globalenv skenv_link) b_src = Some (External ef))
(INJ: j b_src = Some (b_tgt, delta)):
Genv.find_funct_ptr tge b_tgt = Some (External ef).
Proof.
unfold System.globalenv in *.
cinv match_skenv_link_tge.
replace b_tgt with b_src; cycle 1.
{ unfold Genv.find_funct_ptr in FIND. des_ifs.
cinv SKINJ. exploit DOMAIN.
- instantiate (1:= b_src).
assert (SkEnv.wf skenv_link).
{ apply SkEnv.load_skenv_wf; et. }
inv H. unfold Genv.find_symbol in *.
exploit DEFSYMB; eauto.
i. des. eapply Genv.genv_symb_range; eauto.
- i. clarify. }
unfold Genv.find_funct_ptr, Genv.find_def, skdef_of_gdef, fundef in *.
cinv (mge_defs b_src); des_ifs.
Qed.
Lemma system_receptive_at st frs:
receptive_at (sem prog)
(State ((Frame.mk (System.modsem skenv_link) st) :: frs)).
Proof.
econs.
- i. Local Opaque symbolenv.
ss. rewrite LINK_SK in *.
inv H; ss.
+ inv STEP. ss.
exploit external_call_receptive; eauto; cycle 1.
* i. des.
eexists. econs; eauto. ss. econs; eauto.
* unfold System.globalenv in *.
unfold SkEnv.t in *.
eapply match_traces_preserved; [| eauto].
i. unfold Senv.public_symbol at 1. ss.
eapply skenv_link_public_eq.
+ inv FINAL. ss. inv H0.
eexists. econs 4; ss; eauto.
- ss. unfold single_events_at. i.
inv H; ss; try lia. inv STEP.
exploit ec_trace_length; eauto.
eapply external_call_spec.
Qed.
End SYSTEM.
Section ASMLEMMAS.
Lemma asm_determinate_at p st:
determinate_at (semantics p) st.
Proof.
generalize (semantics_determinate p); intro P. inv P. econs; ii; ss; eauto. eapply sd_final_nostep; eauto.
Qed.
End ASMLEMMAS.
(** ********************* regset *********************************)
Definition initial_regset : regset :=
(Pregmap.init Vundef)
# PC <- (Genv.symbol_address tge tprog.(prog_main) Ptrofs.zero)
# RA <- Vnullptr
# RSP <- (Vptr 1%positive Ptrofs.zero).
Definition initial_tgt_regset := initial_regset.
Lemma init_mem_nextblock F V (p: AST.program F V) m
(INIT: Genv.init_mem p = Some m):
Plt 1 (Mem.nextblock m).
Proof.
unfold Genv.init_mem in *.
eapply Genv.alloc_globals_unchanged with (P:=top2) in INIT; eauto.
eapply Mem.unchanged_on_nextblock in INIT. ss. xomega.
Qed.
Lemma update_agree j rs_src rs_tgt pr v
(AGREE: agree j rs_src rs_tgt)
(UPDATE: Val.inject j v (rs_tgt # pr)):
agree j (rs_src # pr <- v) rs_tgt.
Proof.
destruct pr; intros pr0; specialize (AGREE pr0); destruct pr0; eauto.
- destruct i, i0; eauto.
- destruct f, f0; eauto.
- destruct c, c0; eauto.
Qed.
Lemma initial_regset_agree: agree init_inject initial_regset initial_tgt_regset.
Proof.
unfold initial_tgt_regset, initial_regset.
repeat eapply agree_step; ss; eauto.
- unfold Genv.symbol_address; des_ifs. econs; eauto.
unfold init_inject, Mem.flat_inj. des_ifs.
exfalso. eapply Genv.genv_symb_range in Heq.
unfold tge in *. erewrite Genv.init_mem_genv_next in Heq. eauto.
apply TGT_INIT_MEM. symmetry. apply Ptrofs.add_zero.
- econs.
- econs.
+ unfold init_inject, Mem.flat_inj; des_ifs.
exfalso. apply n. eapply init_mem_nextblock.
unfold Sk.load_mem in INIT_MEM. apply INIT_MEM.
+ symmetry. apply Ptrofs.add_zero.
Qed.
(** ********************* calee initial *********************************)
Inductive wf_init_rs (j: meminj) (rs_caller rs_callee: regset) : Prop :=
| wf_init_rs_intro
(PCSAME: rs_caller # PC = rs_callee # PC)
(RANOTFPTR: forall blk ofs (RAVAL: rs_callee RA = Vptr blk ofs),
~ Plt blk (Genv.genv_next skenv_link))
(RASAME: inj_same j (rs_caller # RA) (rs_callee # RA))
(RSPSAME: inj_same j (rs_caller # RSP) (rs_callee # RSP))
(CALLEESAVE: forall mr, Conventions1.is_callee_save mr ->
inj_same j (rs_caller (to_preg mr))
(rs_callee (to_preg mr))).
Lemma preg_case pr :
(exists mr, pr = to_preg mr) \/
(pr = PC) \/ (exists c, pr = CR c) \/ (pr = RSP) \/ (pr = RA).
Proof.
destruct (to_mreg pr) eqn:EQ.
- left. exists m. unfold to_mreg in *.
destruct pr; clarify.
destruct i; clarify; auto.
destruct f; clarify; auto.
- right. unfold to_mreg in *.
destruct pr; clarify; eauto.
destruct i; clarify; auto.
destruct f; clarify; auto.
Qed.
Lemma callee_save_agree j rs_caller init_rs rs_callee rs_tgt sg mr rs
(WF: wf_init_rs j rs_caller init_rs)
(AGREE: agree j rs_callee rs_tgt)
(RETV: loc_result sg = One mr)
(CALLEESAVE: forall mr, Conventions1.is_callee_save mr ->
Val.lessdef (init_rs mr.(to_preg)) (rs_callee mr.(to_preg)))
(RSRA: rs_callee # PC = init_rs # RA)
(RSRSP: rs_callee # RSP = init_rs # RSP)
(RS: rs = (set_pair (loc_external_result sg) (rs_callee mr.(to_preg)) (Asm.regset_after_external rs_caller)) #PC <- (rs_caller RA)):
agree j rs rs_tgt.
Proof.
inv WF. clarify.
- unfold loc_external_result. rewrite RETV. ss.
eapply update_agree; eauto; cycle 1.
{ eapply inj_same_inj; eauto. rewrite <- RSRA. auto. }
eapply update_agree; eauto.
unfold Asm.regset_after_external in *. intros pr. specialize (AGREE pr).
destruct (preg_case pr); des; clarify; ss.
+ rewrite to_preg_to_mreg. des_ifs.
specialize (CALLEESAVE mr0). specialize (CALLEESAVE0 mr0).
rewrite Heq in *. eapply inj_same_inj; eauto.
eapply Mem.val_lessdef_inject_compose; try apply CALLEESAVE; eauto.
+ rewrite RSRSP in *. eapply inj_same_inj; eauto.
Qed.
(** ********************* match stack *********************************)
Inductive match_stack (j: meminj) : (Values.block -> Z -> Prop) -> regset -> list Frame.t -> Prop :=
| match_stack_init
init_rs P
(RSRA: init_rs # RA = Vnullptr)
(RSPC: init_rs # PC = Genv.symbol_address tge tprog.(prog_main) Ptrofs.zero)
(SIG: skenv_link.(Genv.find_funct) (Genv.symbol_address tge tprog.(prog_main) Ptrofs.zero) = Some (Internal signature_main)):
match_stack j P init_rs nil
| match_stack_cons
fr frs p st init_rs0 init_rs1 P0 P1 sg blk ofs
(FRAME: fr = Frame.mk (AsmC.modsem skenv_link p) (AsmC.mkstate init_rs1 st))
(STACK: match_stack j P0 init_rs1 frs)
(WF: wf_init_rs j st.(st_rs) init_rs0)
(GELE: genv_le (local_genv p) tge)
(PROGIN: In (AsmC.module p) prog)
(SIG: exists skd, skenv_link.(Genv.find_funct) (init_rs0 # PC)
= Some skd /\ Sk.get_csig skd = Some sg)
(RSPPTR: st.(st_rs) # RSP = Vptr blk ofs)
(RANGE: P0 \2/ (brange blk (Ptrofs.unsigned ofs) (Ptrofs.unsigned ofs + 4 * size_arguments sg)) <2= P1):
match_stack j P1 init_rs0 (fr::frs)
| match_stack_cons_asmstyle
fr frs p st init_rs0 init_rs1 P0
(FRAME: fr = Frame.mk (AsmC.modsem skenv_link p) (AsmC.mkstate init_rs1 st))
(STACK: match_stack j P0 init_rs1 frs)
(WF: inj_same j (st.(st_rs) # RA) (init_rs0 # RA))
(GELE: genv_le (local_genv p) tge)
(PROGIN: In (AsmC.module p) prog)
(SIG: exists skd, skenv_link.(Genv.find_funct) (init_rs0 # PC)
= Some skd /\ Sk.get_csig skd = None):
match_stack j P0 init_rs0 (fr::frs)
.
Inductive match_stack_call (j: meminj) : mem -> (Values.block -> Z -> Prop) -> regset -> list Frame.t -> Prop :=
| match_stack_call_init
init_rs m P
(MEM: m = m_init)
(INITRS: init_rs = initial_regset)
(SIG: skenv_link.(Genv.find_funct) (Genv.symbol_address tge tprog.(prog_main) Ptrofs.zero) = Some (Internal signature_main)):
match_stack_call j m P init_rs nil
| match_stack_call_cons
fr frs p st init_rs0 init_rs1 m P0 P1 sg blk ofs
(FRAME: fr = Frame.mk (AsmC.modsem skenv_link p)
(AsmC.mkstate init_rs1 st))
(INITRS: init_rs0 = st.(st_rs))
(STACK: match_stack j P0 init_rs1 frs)
(MEM: m = st.(st_m))
(GELE: genv_le (local_genv p) tge)
(PROGIN: In (AsmC.module p) prog)
(SIG: exists skd, skenv_link.(Genv.find_funct) (init_rs0 # PC)
= Some skd /\ Sk.get_csig skd = Some sg)
(RSPPTR: init_rs0 # RSP = Vptr blk ofs)
(RANGE: P0 \2/ (brange blk (Ptrofs.unsigned ofs) (Ptrofs.unsigned ofs + 4 * size_arguments sg)) <2= P1):
match_stack_call j m P1 init_rs0 (fr::frs)
| match_stack_call_cons_asmstyle
fr frs p st init_rs0 init_rs1 m P0
(FRAME: fr = Frame.mk (AsmC.modsem skenv_link p)
(AsmC.mkstate init_rs1 st))
(INITRS: init_rs0 = st.(st_rs))
(STACK: match_stack j P0 init_rs1 frs)
(MEM: m = st.(st_m))
(GELE: genv_le (local_genv p) tge)
(PROGIN: In (AsmC.module p) prog)
(SIG: exists skd, skenv_link.(Genv.find_funct) (init_rs0 # PC)
= Some skd /\ Sk.get_csig skd = None):
match_stack_call j m P0 init_rs0 (fr::frs).
Lemma match_stack_incr j1 j2 init_rs l P0 P1
(INCR: inject_incr j1 j2)
(PLE: P0 <2= P1)
(MATCH: match_stack j1 P0 init_rs l):
match_stack j2 P1 init_rs l.
Proof.
revert init_rs INCR P0 P1 PLE MATCH. induction l; ss; ii; inv MATCH.
- econs; ss; eauto.
- econs; ss; auto.
+ eapply IHl; cycle 2; eauto.
+ inv WF. econs; eauto.
* eapply inj_same_incr; eauto.
* eapply inj_same_incr; eauto.
* ii. eapply inj_same_incr; eauto.
+ eauto.
+ eauto.
+ eauto.
- econs 3; ss; eauto. eapply inj_same_incr; eauto.
Qed.
Lemma frame_inj a0 b0 a1 b1
(EQ: Frame.mk a0 b0 = Frame.mk a1 b1):
b0 ~= b1.
Proof. inv EQ. eauto. Qed.
Lemma asm_frame_inj se1 se2 p1 p2 st1 st2
(EQ : Frame.mk (modsem se1 p1) st1 = Frame.mk (modsem se2 p2) st2):
st1 = st2.
Proof. apply frame_inj in EQ. apply JMeq_eq. eauto. Qed.
Lemma asm_frame_inj2 p1 p2 st1 st2
(EQ : Frame.mk (modsem skenv_link p1) st1
= Frame.mk (modsem skenv_link p2) st2):
local_genv p1 = local_genv p2.
Proof.
apply f_equal with (f := Frame.ms) in EQ. ss.
apply f_hequal with (f := ModSem.globalenv) in EQ.
apply JMeq_eq in EQ. ss.
Qed.
Lemma skenv_inject_memory j m m_tgt
(GEINJECT: skenv_inject skenv_link j m)
(INJ: Mem.inject j m m_tgt):
Ple (Genv.genv_next skenv_link) (Mem.nextblock m).
Proof.
assert (~ Plt
(Mem.nextblock m)
(Genv.genv_next skenv_link)); [|xomega].
ii. inv GEINJECT. exploit DOMAIN; eauto. i.
eapply Mem.valid_block_inject_1 in H0; eauto.
eapply Plt_strict; eauto.
Qed.
(** ********************* arguments *********************************)
Program Definition callee_initial_mem' (blk: Values.block) (ofs: ptrofs)
(m0: mem) (m: mem) (sg: signature) (args: list val): mem :=
Mem.mkmem
(PMap.set
(m.(Mem.nextblock))
(_FillArgsParallel.fill_args_src_blk
(m0.(Mem.mem_contents) !! blk)
((fst (Mem.alloc m 0 (4 * size_arguments sg))).(Mem.mem_contents) !! (Mem.nextblock m))
(Ptrofs.unsigned ofs) 0 args (loc_arguments sg)) ((fst (Mem.alloc m 0 (4 * size_arguments sg))).(Mem.mem_contents)))
((fst (Mem.alloc m 0 (4 * size_arguments sg))).(Mem.mem_access))
((fst (Mem.alloc m 0 (4 * size_arguments sg))).(Mem.nextblock)) _ _ _.
Next Obligation.
eapply Mem.access_max; eauto.
Qed.
Next Obligation.
eapply Mem.nextblock_noaccess; eauto.
Qed.
Next Obligation.
rewrite PMap.gsspec. des_ifs.
- rewrite _FillArgsParallel.fill_args_src_blk_default.
eapply Mem.contents_default.
- eapply Mem.contents_default.
Qed.
Definition callee_initial_reg' (sg: signature) (args: list val): Mach.regset :=
fun mr => if extcall_args_reg mr sg
then _FillArgsParallel.fill_args_src_reg args (loc_arguments sg) mr
else Vundef.
Definition callee_initial_inj' (blk: Values.block) (ofs: ptrofs)
(j: meminj) (m_src: mem): meminj :=
fun blk' => if (peq blk' (Mem.nextblock m_src))
then
match (j blk) with
| Some (blk_tgt, delta) => Some (blk_tgt, delta + Ptrofs.unsigned ofs)
| None => None
end
else j blk'.
Lemma typify_list_lessdef args typs
(LEN: Datatypes.length args = Datatypes.length typs):
Val.lessdef_list (typify_list args typs) args.
Proof.
revert typs LEN. induction args; ss. ii. destruct typs; inv LEN.
unfold typify_list, zip, typify. des_ifs; eauto.
Qed.
Lemma asm_extcall_arguments_mach rs m:
Asm.extcall_arguments rs m <2=
Mach.extcall_arguments (AsmregsC.to_mregset rs) m (rs RSP).
Proof.
ii. eapply list_forall2_imply; eauto.
i. inv H1; econs.
- inv H2; econs. ss.
- inv H2; inv H3; econs; ss.
- inv H2; inv H3; econs; ss.
Qed.
Lemma callee_initial_arguments (rs: regset) m0 m1 blk ofs sg args targs
(ARGS: Asm.extcall_arguments rs m0 sg args)
(RSRSP: rs RSP = Vptr blk ofs)
(ARGRANGE: Ptrofs.unsigned ofs + 4 * size_arguments sg <= Ptrofs.max_unsigned)
(TYP: typecheck args sg targs):
Mach.extcall_arguments
(callee_initial_reg' sg targs)
(callee_initial_mem' blk ofs m0 m1 sg targs)
(Vptr (Mem.nextblock m1) Ptrofs.zero) sg targs.
Proof.
inv TYP.
eapply extcall_arguments_same; cycle 1.
{ instantiate (1:=_FillArgsParallel.fill_args_src_reg _ (loc_arguments sg)).
unfold callee_initial_reg'. ii. des_ifs. }
eapply extcall_arg_in_stack_in_reg_extcall_argument; ss; eauto.
- rewrite PMap.gss.
exploit _FillArgsParallel.fill_args_src_blk_args; [..|eauto].
+ apply val_inject_list_lessdef. apply typify_list_lessdef. eauto.
+ eapply loc_arguments_norepet.
+ erewrite typify_list_length; eauto. rewrite LEN. rewrite Nat.min_id. eapply sig_args_length.
+ eapply extcall_arguments_extcall_arg_in_stack; eauto.
* set (Ptrofs.unsigned_range_2 ofs). lia.
* erewrite Ptrofs.repr_unsigned. rewrite <- RSRSP.
eapply asm_extcall_arguments_mach; eauto.
- exploit _FillArgsParallel.fill_args_src_reg_args; [..|eauto].
+ eapply loc_arguments_norepet.
+ eapply loc_arguments_one.
+ erewrite typify_list_length. rewrite LEN. rewrite Nat.min_id. eapply sig_args_length.
- destruct (Mem.alloc m1 0 (4 * size_arguments sg)) eqn:MEQ.
hexploit Mem_alloc_range_perm; eauto. ii. exploit H; eauto. i.
unfold Mem.perm, callee_initial_mem' in *. ss. rewrite MEQ. ss.
eapply Mem.alloc_result in MEQ. clarify.
- set (Ptrofs.unsigned_range_2 ofs). nia.
Qed.
Lemma callee_initial_inj_incr blk ofs j m_src
(NONE: j (Mem.nextblock m_src) = None):
inject_incr j (callee_initial_inj' blk ofs j m_src).
Proof.
ii. unfold callee_initial_inj'. des_ifs; eauto.
Qed.
Lemma callee_initial_mem_nextblock m0 m1 blk ofs sg targs:
Mem.nextblock (callee_initial_mem' blk ofs m0 m1 sg targs) =
Pos.succ (Mem.nextblock m1).
Proof.
unfold callee_initial_mem'. ss.
Qed.
Lemma callee_initial_mem_perm m0 m1 blk ofs sg targs blk' ofs' p k:
Mem.perm (callee_initial_mem' blk ofs m0 m1 sg targs) blk' ofs' p k
<-> if (peq (Mem.nextblock m1) blk')
then (zle 0 ofs' && zlt ofs' (4 * size_arguments sg))
else Mem.perm m1 blk' ofs' p k.
Proof.
unfold callee_initial_mem', Mem.perm. ss.
destruct (Mem.alloc m1 0 (4 * size_arguments sg)) eqn:MEQ.
exploit Mem.alloc_result; eauto. i. clarify.
split; i.
- eapply Mem.perm_alloc_inv in H; eauto. unfold proj_sumbool. des_ifs; lia.
- des_ifs.
+ eapply Mem.perm_cur.
eapply Mem.perm_implies.
* try eapply Mem_alloc_range_perm; eauto.
unfold proj_sumbool in *. des_ifs.
* econs.
+ eapply Mem.perm_alloc_1; eauto.
Qed.
Lemma callee_initial_inject' (rs: regset) m_src0 m_src1 m_tgt j blk ofs sg args targs
(INJECT: Mem.inject j m_src0 m_tgt)
(ARGS: Asm.extcall_arguments rs m_src0 sg args)
(RSRSP: rs RSP = Vptr blk ofs)
(FREE: freed_from m_src0 m_src1 blk ofs.(Ptrofs.unsigned) (ofs.(Ptrofs.unsigned) + 4 * (size_arguments sg)))
(ARGRANGE: Ptrofs.unsigned ofs + 4 * size_arguments sg <= Ptrofs.max_unsigned)
(TYP: typecheck args sg targs)
(ALIGN: forall chunk (CHUNK: size_chunk chunk <= 4 * (size_arguments sg)),
(align_chunk chunk | ofs.(Ptrofs.unsigned))):
Mem.inject
(callee_initial_inj' blk ofs j m_src1)
(callee_initial_mem' blk ofs m_src0 m_src1 sg targs)
m_tgt.
Proof.
inv TYP. dup FREE. inv FREE. inv freed_from_unchanged.
set (ARGRANGE0:= Ptrofs.unsigned_range_2 ofs).
assert (INCR: inject_incr j (callee_initial_inj' blk ofs j m_src1)).
{ eapply callee_initial_inj_incr; eauto. eapply Mem.mi_freeblocks; eauto.
rewrite freed_from_nextblock. apply Plt_strict. }
econs; [econs|..].
- i. eapply callee_initial_mem_perm in H0. unfold proj_sumbool in *.
unfold callee_initial_inj' in H. des_ifs.
+ exploit Mem.mi_perm; eauto.
* apply INJECT.
* eapply freed_from_perm. instantiate (1:=Ptrofs.unsigned ofs + ofs0). lia.
* i. replace (ofs0 + (z + Ptrofs.unsigned ofs)) with (Ptrofs.unsigned ofs + ofs0 + z); try lia.
eapply Mem.perm_cur. eapply Mem.perm_implies; eauto. econs.
+ eapply Mem.perm_inject; eauto.
eapply freed_from_perm_greater; eauto.
- i. unfold callee_initial_inj' in H. des_ifs.
+ unfold Mem.range_perm in H0.
setoid_rewrite callee_initial_mem_perm in H0. des_ifs.
assert (RANGE: 0 <= ofs0 /\ ofs0 + size_chunk chunk <= 4 * size_arguments sg).
{ clear - H0. unfold proj_sumbool in *.
set (size_chunk_pos chunk). split.
- specialize (H0 ofs0). exploit H0; try lia. des_ifs.
- specialize (H0 (ofs0 + size_chunk chunk - 1)).
exploit H0; try lia. des_ifs. i. lia. }
apply Z.divide_add_r.
{ eapply Mem.mi_align; try apply INJECT; eauto.
ii. apply Mem.perm_cur. eapply freed_from_perm.
instantiate (1:=Ptrofs.unsigned ofs) in H. lia. }
{ eapply ALIGN. lia. }
+ unfold Mem.range_perm in H0.
setoid_rewrite callee_initial_mem_perm in H0. des_ifs.
eapply Mem.mi_align; try apply INJECT; eauto.
instantiate (2:=ofs0). ii. specialize (H0 _ H1).
eapply freed_from_perm_greater; eauto.
- i. unfold callee_initial_inj' in H.
rewrite callee_initial_mem_perm in H0. des_ifs.
+ exploit _FillArgsParallel.fill_args_src_blk_inject.
{ apply val_inject_list_lessdef. apply typify_list_lessdef. eauto. }
{ erewrite typify_list_length. rewrite LEN.
rewrite Nat.min_id. eapply sig_args_length. }
{ instantiate (1:=Ptrofs.unsigned ofs).
instantiate (1:=(Mem.mem_contents m_src0) !! blk).
eapply extcall_arguments_extcall_arg_in_stack; eauto.
- lia.
- rewrite Ptrofs.repr_unsigned. rewrite <- RSRSP.
eapply asm_extcall_arguments_mach; eauto. }
{ i. exploit Mem.mi_memval; try apply INJECT; eauto.
- instantiate (1:=ofs0 + Ptrofs.unsigned ofs).
eapply Mem.perm_implies; [try eapply freed_from_perm|econs].
unfold proj_sumbool in *. des_ifs. lia.
- i. replace (callee_initial_inj' blk ofs j m_src0) with
(compose_meminj (fun b => Some (b, 0)) (callee_initial_inj' blk ofs j m_src0)); cycle 1.
{ extensionality b. unfold compose_meminj. des_ifs. }
exploit memval_inject_compose.
+ eapply H.
+ instantiate (1:=(ZMap.get (ofs0 + Ptrofs.unsigned ofs + z) (Mem.mem_contents m_tgt) !! b2)).
instantiate (2:=(callee_initial_inj' blk ofs j m_src1)).
eapply memval_inject_incr.
{ instantiate (1:=ofs0). rpapply H2. f_equal. lia. }
{ eapply callee_initial_inj_incr; eauto. eapply Mem.mi_freeblocks; eauto.
rewrite freed_from_nextblock. apply Plt_strict. }
+ i. unfold callee_initial_mem'. ss. rewrite PMap.gss.
instantiate (1:=0) in H3. zsimpl. clear - H3.
rpapply H3.
* extensionality b. unfold compose_meminj. des_ifs.
* f_equal. f_equal.
Local Transparent Mem.alloc. ss. rewrite PMap.gss. auto.
* f_equal. lia. }
+ eapply memval_inject_incr; eauto.
Local Transparent Mem.alloc.
unfold callee_initial_mem', Mem.alloc. ss. rewrite PMap.gso; eauto.
dup H0. eapply freed_from_perm_greater in H0; eauto.
eapply Mem.mi_memval in H0; try apply INJECT; eauto.
rewrite PMap.gso; eauto. rewrite unchanged_on_contents; eauto.
* des_ifs. ii. eapply freed_from_noperm; eauto. apply Mem.perm_cur.
eapply Mem.perm_implies; eauto. econs.
* eapply freed_from_perm_greater; eauto.
Local Opaque Mem.alloc.
- ii. unfold Mem.valid_block in *. rewrite callee_initial_mem_nextblock in *.
unfold callee_initial_inj'. des_ifs.
+ exfalso. clear - H. xomega.
+ eapply Mem.mi_freeblocks; eauto.
unfold Mem.valid_block. rewrite <- freed_from_nextblock. xomega.
- ii. unfold callee_initial_inj' in H. des_ifs.
+ eapply Mem.mi_mappedblocks; eauto.
+ eapply Mem.mi_mappedblocks; eauto.
- ii. erewrite callee_initial_mem_perm in *. unfold proj_sumbool in *.
unfold callee_initial_inj' in H0, H1. des_ifs.
+ destruct (peq b1 blk); clarify.
{ right. ii. eapply freed_from_noperm.
- instantiate (1:=ofs2 + Ptrofs.unsigned ofs). lia.
- replace (ofs2 + Ptrofs.unsigned ofs) with ofs1; try lia. eauto. }
{ exploit Mem.mi_no_overlap; try apply INJECT; try exact n1; eauto.
- eapply freed_from_perm_greater; eauto.
- instantiate (1:=Ptrofs.unsigned ofs + ofs2).
apply Mem.perm_cur. eapply Mem.perm_implies.
+ eapply freed_from_perm. lia.
+ econs.
- i. des; eauto. right. lia. }
+ destruct (peq blk b2); clarify.
{ right. ii. eapply freed_from_noperm.
- instantiate (1:=ofs1 + Ptrofs.unsigned ofs). lia.
- replace (ofs1 + Ptrofs.unsigned ofs) with ofs2; try lia. eauto. }
{ exploit Mem.mi_no_overlap; try apply INJECT; try exact n1; eauto.
- instantiate (1:=Ptrofs.unsigned ofs + ofs1).
apply Mem.perm_cur. eapply Mem.perm_implies.
+ eapply freed_from_perm. lia.
+ econs.
- eapply freed_from_perm_greater; eauto.
- i. des; eauto. right. lia. }
+ exploit Mem.mi_no_overlap; try apply INJECT; try exact H; eauto.
* eapply freed_from_perm_greater; eauto.
* eapply freed_from_perm_greater; eauto.
- ii. unfold callee_initial_inj' in H.
repeat erewrite callee_initial_mem_perm in *. des_ifs.
+ exploit Mem.mi_representable.
* eauto.
* eauto.
* instantiate (1:=Ptrofs.add ofs ofs0).
unfold proj_sumbool in *. des; des_ifs_safe.
{ left. apply Mem.perm_cur. eapply Mem.perm_implies.
- eapply freed_from_perm. rewrite Ptrofs.add_unsigned.
erewrite Ptrofs.unsigned_repr; lia.
- econs. }
{ right. apply Mem.perm_cur. eapply Mem.perm_implies.
- eapply freed_from_perm. rewrite Ptrofs.add_unsigned.
erewrite Ptrofs.unsigned_repr; lia.
- econs. }
* i. split.
{ set (Ptrofs.unsigned_range_2 ofs). clear - a H. lia. }
{ rewrite Ptrofs.add_unsigned in H.
erewrite Ptrofs.unsigned_repr in H.
- clear - H. lia.
- unfold proj_sumbool in *. des; des_ifs_safe; lia. }
+ eapply Mem.mi_representable; try eapply INJECT; eauto.
des; eapply freed_from_perm_greater in H0; eauto.
- ii. unfold callee_initial_inj' in H.
repeat erewrite callee_initial_mem_perm in *. des_ifs.
+ clear. tauto.
+ exploit Mem.mi_perm_inv; try apply INJECT; eauto.
i. destruct (peq b1 blk); clarify.
{ destruct (zle (Ptrofs.unsigned ofs) ofs0 && zlt ofs0 (Ptrofs.unsigned ofs + 4 * size_arguments sg))
eqn:BOUND; unfold proj_sumbool in *; des_ifs.
- right. eapply freed_from_noperm; eauto.
- repeat erewrite <- unchanged_on_perm; eauto; des_ifs; try lia.
+ eapply Mem.valid_block_inject_1; eauto.
+ eapply Mem.valid_block_inject_1; eauto.
- repeat erewrite <- unchanged_on_perm; eauto; des_ifs; try lia.
+ eapply Mem.valid_block_inject_1; eauto.
+ eapply Mem.valid_block_inject_1; eauto.
- repeat erewrite <- unchanged_on_perm; eauto; des_ifs; try lia.
+ eapply Mem.valid_block_inject_1; eauto.
+ eapply Mem.valid_block_inject_1; eauto. }
{ repeat erewrite <- unchanged_on_perm; eauto; des_ifs.
- eapply Mem.valid_block_inject_1; eauto.
- eapply Mem.valid_block_inject_1; eauto. }