-
Notifications
You must be signed in to change notification settings - Fork 0
/
GVN4.v
1918 lines (1812 loc) · 59.9 KB
/
GVN4.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 Bool.
Require Import Sorting.Permutation.
Require Import Omega.
Require Import sflib.
Require Import Lia.
Require Import Common.
Require Import Value.
Require Import Lang.
Require Import Memory.
Require Import State.
Require Import LoadStore.
Require Import SmallStep.
Require Import SmallStepAux.
Require Import SmallStepWf.
Require Import Refinement.
Require Import SmallStepRefinement.
Require Import Reordering.
Require Import GVN1.
Require Import Utf8.
Module Ir.
Module GVN4.
(**************************************************************
This file proves validity of the fourth GVN optimization case:
4. Either p or q is computed by a series of gep inbounds with
positive offsets, based on the same base pointer.
High-level structure of proof is as follows:
(1) We define the notion of `gepinbs p q p0`, meaning
that p and q have same base pointer p0, and have gep inbounds
with positive offsets.
(2) We show that if p0 is a logical pointer, p and q are the same.
(3) We show that if p0 is a physical pointer,
after calculation, given p=Phy(o1, I1, cid1) and
q=Phy(o2, I2, cid2), min(I1) = min(I2) /\ max(I2) = max(I2)
/\ o1 = o2 /\ cid1 = cid2. This relation is defined as
`phys_minmaxI p q`.
(2) and (3) are shown in `gepinbs_after_icmpeq_true`.
(4) We show that if `phy_minmaxI p q` holds, then refinement
holds for all instructions that has operand p replaced
with q.
**************************************************************)
Definition posofs (ofs:nat) (t:Ir.ty) :=
ofs * Ir.ty_bytesz t < Nat.shiftl 1 (Ir.PTRSZ - 1).
Inductive gepinbs: Ir.Memory.t -> Ir.val -> Ir.val -> Ir.ptrval -> Prop :=
| gi_one: (* should have at least one GEP *)
forall m p0 p q ofs1 ofs2 t1 t2
(HGEP1:p = Ir.SmallStep.gep p0 ofs1 t1 m true)
(HGEP2:q = Ir.SmallStep.gep p0 ofs2 t2 m true)
(HPOS1:posofs ofs1 t1)
(HPOS2:posofs ofs2 t2),
gepinbs m p q p0
| gi_succ_l:
forall m p q p0 ofs p' t
(HBASE:gepinbs m (Ir.ptr p) (Ir.ptr q) p0)
(HGEP1:p' = Ir.SmallStep.gep p ofs t m true)
(HPOS:posofs ofs t),
gepinbs m p' (Ir.ptr q) p0
| gi_succ_r:
forall m p q p0 ofs q' t
(HBASE:gepinbs m (Ir.ptr p) (Ir.ptr q) p0)
(HGEP1:q' = Ir.SmallStep.gep q ofs t m true)
(HPOS:posofs ofs t),
gepinbs m (Ir.ptr p) q' p0.
Definition phys_minmaxI (p q:Ir.ptrval): Prop :=
exists o I1 I2 cid ofsmin ofsmax,
(p = Ir.pphy o I1 cid /\ q = Ir.pphy o I2 cid /\
list_min ofsmin I1 /\ list_min ofsmin I2 /\
list_max ofsmax I1 /\ list_max ofsmax I2).
(*********************************************************
Important property of gepinbs:
If gepinbs p q holds, and `icmp eq p, q` evaluates
to true, then either p = q or phys_minmaxI holds.
*********************************************************)
Lemma gepinbs_log_neverphy:
forall m v1 l o v2 p0
(HP1:Ir.ptr (Ir.plog l o) = v1)
(HGEPINBS:gepinbs m v1 v2 p0),
~ exists o2 I2 cid2, v2 = Ir.ptr (Ir.pphy o2 I2 cid2).
Proof.
intros.
generalize dependent l.
generalize dependent o.
induction HGEPINBS.
{ intros. inv HP1. intros HH. inv HH. inv H0. inv H1.
unfold Ir.SmallStep.gep in *.
des_ifs.
}
{ unfold Ir.SmallStep.gep in HGEP1.
des_ifs. intros. inv HP1.
intros HH. inv HH. inv H. inv H0. inv H.
exploit IHHGEPINBS. ss. eexists. eexists. eexists. ss.
eauto. }
{ intros. intros HH. inv HH. inv H. inv H0.
unfold Ir.SmallStep.gep in H.
des_ifs.
exploit IHHGEPINBS. ss. do 3 eexists. ss. eauto.
exploit IHHGEPINBS. ss. do 3 eexists. ss. eauto.
}
Qed.
Lemma gepinbs_phy_neverlog:
forall m v1 o I cid v2 p0
(HP1:Ir.ptr (Ir.pphy o I cid) = v1)
(HGEPINBS:gepinbs m v1 v2 p0),
~ exists l2 o2, v2 = Ir.ptr (Ir.plog l2 o2).
Proof.
intros.
generalize dependent o.
generalize dependent I.
generalize dependent cid.
induction HGEPINBS.
{ intros. inv HP1. intros HH. inv HH. inv H0. inv H1.
unfold Ir.SmallStep.gep in *. des_ifs.
}
{ intros. intros HH. inv HH. inv H. inv H0.
unfold Ir.SmallStep.gep in HP1.
des_ifs.
exploit IHHGEPINBS. ss. do 3 eexists. ss. eauto.
exploit IHHGEPINBS. ss. do 3 eexists. ss.
}
{ intros. intros HH. inv HH. inv H.
unfold Ir.SmallStep.gep in H0.
des_ifs.
exploit IHHGEPINBS. ss. eexists. eexists. eexists. ss.
}
Qed.
Lemma gepinbs_phy_samecid:
forall m v1 v2 o1 o2 I1 I2 cid1 cid2 p0
(HP1:Ir.ptr (Ir.pphy o1 I1 cid1) = v1)
(HP1:Ir.ptr (Ir.pphy o2 I2 cid2) = v2)
(HGEPINBS:gepinbs m v1 v2 p0),
cid1 = cid2.
Proof.
intros.
generalize dependent o1.
generalize dependent o2.
generalize dependent I1.
generalize dependent I2.
generalize dependent cid1.
generalize dependent cid2.
induction HGEPINBS.
{ intros. inv HP1.
unfold Ir.SmallStep.gep in *. des_ifs.
}
{ intros. inv HP0.
unfold Ir.SmallStep.gep in HP1.
des_ifs.
exploit IHHGEPINBS. ss. ss. eauto.
exploit IHHGEPINBS. ss. ss. eauto.
}
{ intros. inv HP0.
unfold Ir.SmallStep.gep in *. des_ifs.
exploit IHHGEPINBS. ss. ss. eauto.
exploit IHHGEPINBS. ss. ss. eauto.
}
Qed.
Lemma gep_phy_Ilb:
forall o1 o2 I1 I2 cid1 cid2 ofs t m
(HMIN:exists n, list_min n I1)
(HGEP:(Ir.ptr (Ir.pphy o2 I2 cid2)) =
Ir.SmallStep.gep (Ir.pphy o1 I1 cid1) ofs t m true)
(HPOS:posofs ofs t),
exists n, (list_min n (o1::I1) /\ list_min n I2).
Proof.
intros.
unfold Ir.SmallStep.gep in HGEP.
unfold posofs in HPOS.
rewrite <- Nat.ltb_lt in HPOS.
rewrite HPOS in HGEP.
des_ifs.
rewrite Nat.ltb_lt in *.
unfold Ir.SmallStep.twos_compl_add.
unfold Ir.SmallStep.twos_compl.
rewrite Nat.mod_small.
unfold list_min.
simpl.
inv HMIN. inv H.
destruct (x <=? o1) eqn:HEQ.
{ rewrite Nat.leb_le in HEQ.
exists x.
split. split. eauto.
simpl. constructor. ss. ss.
split. do 2 right. ss.
constructor. ss. constructor. lia. ss.
}
{ rewrite Nat.leb_gt in HEQ.
exists o1. split. split. eauto. constructor. ss.
rewrite List.Forall_forall in *. intros. eapply H1 in H. lia.
split. eauto.
constructor. ss. constructor. lia.
rewrite List.Forall_forall in *. intros. eapply H1 in H. lia.
}
rewrite Ir.PTRSZ_MEMSZ.
ss.
Qed.
Lemma gep_phy_Iub:
forall o1 o2 I1 I2 cid1 cid2 ofs t m
(HMAX:list_max o1 I1)
(HGEP:(Ir.ptr (Ir.pphy o2 I2 cid2)) =
Ir.SmallStep.gep (Ir.pphy o1 I1 cid1) ofs t m true)
(HPOS:posofs ofs t),
list_max o2 I2.
Proof.
intros.
unfold Ir.SmallStep.gep in HGEP.
unfold posofs in HPOS.
rewrite <- Nat.ltb_lt in HPOS.
rewrite HPOS in HGEP.
des_ifs.
rewrite Nat.ltb_lt in *.
unfold Ir.SmallStep.twos_compl_add.
unfold Ir.SmallStep.twos_compl.
rewrite Nat.mod_small.
unfold list_max.
simpl.
inv HMAX.
split.
right. left. ss.
constructor. lia. constructor. ss.
rewrite List.Forall_forall in *. intros. apply H0 in H1. lia.
rewrite Ir.PTRSZ_MEMSZ.
ss.
Qed.
Lemma gepinbs_log_sameblk:
forall m v1 l1 o1 l2 o2 v2 p0
(HP1:Ir.ptr (Ir.plog l1 o1) = v1)
(HP2:Ir.ptr (Ir.plog l2 o2) = v2)
(HGEPINBS:gepinbs m v1 v2 p0),
l1 = l2.
Proof.
intros.
generalize dependent l1.
generalize dependent l2.
generalize dependent o1.
generalize dependent o2.
induction HGEPINBS.
{ intros. inv HP2. unfold Ir.SmallStep.gep in *. des_ifs. }
{ intros.
unfold Ir.SmallStep.gep in HGEP1.
des_ifs. exploit IHHGEPINBS. ss. eexists. eauto.
}
{ intros. unfold Ir.SmallStep.gep in HGEP1.
des_ifs.
exploit IHHGEPINBS. ss. do 3 eexists. ss.
}
Qed.
Lemma gepinbs_notnum:
forall m v1 v2 p0
(HGEPINBS:gepinbs m v1 v2 p0),
(~ (exists n1, v1 = Ir.num n1)) /\
(~ (exists n2, v2 = Ir.num n2)).
Proof.
intros.
induction HGEPINBS.
{ split. intros HH. inv HH. unfold Ir.SmallStep.gep in *. des_ifs.
intros HH. inv HH. unfold Ir.SmallStep.gep in *. des_ifs. }
{ inv IHHGEPINBS.
split; try ss.
intros HH.
inv HH.
unfold Ir.SmallStep.gep in H1. des_ifs. }
{ inv IHHGEPINBS.
split; try ss.
intros HH. inv HH.
unfold Ir.SmallStep.gep in H1. des_ifs. }
Qed.
Lemma gepinbs_icmp_det:
forall m v1 v2 p1 p2 p0
(HP1:Ir.ptr p1 = v1)
(HP2:Ir.ptr p2 = v2)
(HGEPINBS:gepinbs m v1 v2 p0),
Ir.SmallStep.icmp_eq_ptr_nondet_cond p1 p2 m = false.
Proof.
intros.
unfold Ir.SmallStep.icmp_eq_ptr_nondet_cond.
destruct v1; try congruence.
destruct p; try (inv HP1; reflexivity).
inv HP1.
destruct p2; try reflexivity.
eapply gepinbs_log_sameblk in HGEPINBS; try reflexivity.
subst b.
rewrite Nat.eqb_refl. simpl. des_ifs.
Qed.
Lemma phys_minmaxI_cons:
forall o I1 I2 cid i
(HPMM:phys_minmaxI (Ir.pphy o I1 cid) (Ir.pphy o I2 cid)),
phys_minmaxI (Ir.pphy o (i::I1) cid) (Ir.pphy o (i::I2) cid).
Proof.
intros.
unfold phys_minmaxI in *.
inv HPMM. inv H. inv H0. inv H. inv H0. inv H.
inv H0. inv H1. inv H2. inv H3. inv H4.
inv H. inv H0.
exploit list_minmax_le.
eapply H1. eapply H3. intros HH.
do 4 eexists.
destruct (x3 <=? i) eqn:HMIN.
{ rewrite Nat.leb_le in HMIN.
destruct (i <? x4) eqn:HMAX.
{ rewrite Nat.ltb_lt in HMAX.
exists x3. exists x4.
split. ss. split. ss.
split. eapply list_min_cons; ss.
split. eapply list_min_cons; ss.
split. eapply list_max_cons. ss. omega.
eapply list_max_cons. ss. omega.
}
{ rewrite Nat.ltb_ge in HMAX.
exists x3. exists i.
split. ss. split. ss.
split. eapply list_min_cons; ss.
split. eapply list_min_cons; ss.
split. eapply list_max_cons2. eassumption. ss.
eapply list_max_cons2. eassumption. omega.
}
}
{ rewrite Nat.leb_gt in HMIN.
destruct (i <? x4) eqn:HMAX.
{ rewrite Nat.ltb_lt in HMAX.
exists i. exists x4.
split. ss. split. ss.
split. eapply list_min_cons2. eassumption. omega.
split. eapply list_min_cons2. eassumption. omega.
split. eapply list_max_cons. ss. omega.
eapply list_max_cons. ss. omega.
}
{ rewrite Nat.ltb_ge in HMAX.
omega.
}
}
Qed.
Lemma phys_minmaxI_refl:
forall o I s i
(HIN:List.In i I),
phys_minmaxI (Ir.pphy o I s) (Ir.pphy o I s).
Proof.
unfold phys_minmaxI.
intros.
destruct I. inv HIN.
assert (HH1 := list_min_exists n I).
assert (HH2 := list_max_exists n I).
inv HH1. inv HH2.
do 6 eexists.
split. ss.
split. ss.
do 4 (split; try eassumption).
Qed.
Lemma twos_compl_add_PTRSZ:
forall o i
(HLE:o + i < Ir.MEMSZ),
Ir.SmallStep.twos_compl_add o i Ir.PTRSZ = o + i.
Proof.
intros.
unfold Ir.SmallStep.twos_compl_add.
unfold Ir.SmallStep.twos_compl.
rewrite Ir.PTRSZ_MEMSZ.
rewrite Nat.mod_small. ss.
ss.
Qed.
Lemma twos_compl_add_PTRSZ':
forall o i
(HLE:o + i <? Ir.MEMSZ = true),
Ir.SmallStep.twos_compl_add o i Ir.PTRSZ = o + i.
Proof.
intros.
apply twos_compl_add_PTRSZ.
rewrite <- Nat.ltb_lt. ss.
Qed.
Lemma gepinbs_phy_Imax:
forall m o I1 cid p1 p2 p0 o0 I0 cid0
(HP1:p1 = (Ir.ptr (Ir.pphy o I1 cid)))
(HP0:p0 = Ir.pphy o0 I0 cid0)
(HGEP:gepinbs m p1 p2 p0),
(exists n, list_max n I1 /\ list_max n I0 /\ o < n) \/
(list_max o I1 /\ (forall n, list_max n I0 -> n <= o)).
Proof.
intros.
generalize dependent o.
generalize dependent I1.
generalize dependent I0.
generalize dependent cid.
induction HGEP.
{ intros. inv HP1.
destruct I0.
{ right.
unfold Ir.SmallStep.gep in *.
unfold posofs in *. rewrite <- Nat.ltb_lt in HPOS1, HPOS2.
des_ifs.
split.
{
split.
{
apply list_max_cons. apply list_max_one.
rewrite twos_compl_add_PTRSZ. lia.
rewrite Nat.ltb_lt in Heq. ss.
}
{
apply list_max_cons. apply list_max_one.
rewrite twos_compl_add_PTRSZ. lia.
rewrite Nat.ltb_lt in Heq. ss.
}
}
{ intros. inv H. inv H0. }
}
assert (HMAX := list_max_exists n I0).
inv HMAX.
destruct (x <=? o) eqn:HLE.
{ right.
split.
{
unfold posofs in *. rewrite <- Nat.ltb_lt in *.
unfold Ir.SmallStep.gep in *.
des_ifs.
split.
apply list_max_cons. eapply list_max_cons2. eapply H0.
rewrite Nat.leb_le in HLE. lia.
rewrite twos_compl_add_PTRSZ. lia.
rewrite Nat.ltb_lt in *. ss.
apply list_max_cons. eapply list_max_cons2. eapply H0.
rewrite Nat.leb_le in HLE. lia.
rewrite twos_compl_add_PTRSZ. lia.
rewrite Nat.ltb_lt in *. ss.
}
{ intros. eapply list_max_inj_l with (n := x) in H1; try ss.
rewrite Nat.leb_le in HLE. omega. }
}
{ left. exists x.
unfold posofs in *. rewrite <- Nat.ltb_lt in *.
unfold Ir.SmallStep.gep in *.
des_ifs.
split.
{
apply list_max_cons. apply list_max_cons. ss.
rewrite Nat.leb_gt in HLE.
omega.
rewrite Nat.leb_gt in HLE.
rewrite twos_compl_add_PTRSZ in HLE. eapply le_trans.
instantiate (1 := o0 + ofs1 * Ir.ty_bytesz t1).
eapply Nat.le_add_r.
rewrite Nat.ltb_lt in Heq. omega.
rewrite Nat.ltb_lt in Heq. ss.
}
{ split. ss.
apply Nat.leb_gt in HLE.
apply Nat.ltb_lt. ss.
}
}
}
{ intros.
inv HP0.
unfold posofs in HPOS.
rewrite <- Nat.ltb_lt in HPOS.
unfold Ir.SmallStep.gep in HP1.
des_ifs.
exploit IHHGEP.
ss. ss. intros HH. inv HH.
{ inv H. inv H0. inv H1. clear IHHGEP.
remember (Ir.SmallStep.twos_compl_add n (ofs * Ir.ty_bytesz t)
Ir.PTRSZ) as n'.
destruct (x <=? n') eqn:HLE.
{ rewrite Nat.leb_le in HLE.
right. split.
apply list_max_cons. eapply list_max_cons2. eapply H. ss.
subst n'.
rewrite twos_compl_add_PTRSZ.
apply Nat.le_add_r. rewrite Nat.ltb_lt in Heq. ss.
intros. apply list_max_inj_l with (n := x) in H1. omega. ss.
}
{ left.
exists x.
split.
{ apply list_max_cons. apply list_max_cons. ss.
subst n'.
rewrite Nat.leb_gt in HLE. rewrite twos_compl_add_PTRSZ in *. omega.
rewrite Nat.ltb_lt in Heq. omega.
rewrite Nat.ltb_lt in Heq. omega.
subst n'.
rewrite Nat.leb_gt in HLE. rewrite twos_compl_add_PTRSZ in *.
lia. rewrite Nat.ltb_lt in Heq. ss.
}
{ split. ss. rewrite Nat.leb_gt in HLE. omega. }
}
}
{ inv H. right.
split.
{ apply list_max_cons. eapply list_max_cons2. eassumption.
rewrite twos_compl_add_PTRSZ.
apply Nat.le_add_r. rewrite Nat.ltb_lt in Heq. ss.
rewrite twos_compl_add_PTRSZ.
apply Nat.le_add_r. rewrite Nat.ltb_lt in Heq. ss.
}
{ intros. apply H1 in H.
rewrite twos_compl_add_PTRSZ'. lia.
ss.
}
}
}
{ intros. inv HP1. eapply IHHGEP. ss. ss. }
Qed.
Lemma gepinbs_sym:
forall m p1 p2 p0
(HGEP:gepinbs m p1 p2 p0),
gepinbs m p2 p1 p0.
Proof.
intros.
induction HGEP.
{ eapply gi_one. eassumption. eassumption. ss. ss. }
{ eapply gi_succ_r. eassumption. eassumption. ss. }
{ eapply gi_succ_l. eassumption. eassumption. ss. }
Qed.
Lemma gepinbs_phy_I_In:
forall m p1 p2 p0 o I cid
(HP1:p1 = Ir.ptr (Ir.pphy o I cid))
(HGEP:gepinbs m p1 p2 p0),
List.In o I.
Proof.
intros.
generalize dependent o.
generalize dependent I.
generalize dependent cid.
induction HGEP.
{ intros. inv HP1. unfold Ir.SmallStep.gep in *.
des_ifs. right. left. ss. right. left. ss. }
{ intros. inv HP1. unfold Ir.SmallStep.gep in *.
des_ifs. right. left. ss. right. left. ss. }
{ intros. eapply IHHGEP. eassumption. }
Qed.
Lemma gepinbs_phy_Imin:
forall m o I1 cid p1 p2 p0 o0 I0
(HP1:p1 = (Ir.ptr (Ir.pphy o I1 cid)))
(HP0:p0 = Ir.pphy o0 I0 cid)
(HGEP:gepinbs m p1 p2 p0),
(exists n, list_min n I1 /\ list_min n I0) \/
list_min o0 I1.
Proof.
intros.
generalize dependent o.
generalize dependent o0.
generalize dependent I1.
generalize dependent I0.
generalize dependent cid.
induction HGEP.
{ intros. inv HP1. unfold Ir.SmallStep.gep in H.
unfold posofs in *. rewrite <- Nat.ltb_lt in HPOS1, HPOS2. des_ifs.
{ destruct I0.
{ right. eapply list_min_cons2.
apply list_min_one.
rewrite twos_compl_add_PTRSZ'. apply Nat.le_add_r.
ss.
}
{ assert (HH := list_min_exists n I0).
inv HH.
destruct (x <? o0) eqn:HLE.
{ left. exists x.
split; try ss.
apply list_min_cons.
apply list_min_cons.
ss.
rewrite twos_compl_add_PTRSZ'. rewrite Nat.ltb_lt in HLE.
lia. ss.
rewrite Nat.ltb_lt in HLE. omega.
}
{ destruct (x <=? Ir.SmallStep.twos_compl_add o0 (ofs1 * Ir.ty_bytesz t1)
Ir.PTRSZ)
eqn:HLE2.
{ right. rewrite Nat.ltb_ge in HLE.
eapply list_min_cons2.
apply list_min_cons.
eassumption.
rewrite Nat.leb_le in HLE2. ss. ss. }
{ rewrite Nat.ltb_ge in HLE. rewrite Nat.leb_gt in HLE2.
right. eapply list_min_cons2.
eapply list_min_cons2.
eassumption.
omega.
rewrite twos_compl_add_PTRSZ'. lia.
ss.
}
}
}
}
}
{ intros. inv HP0. dup HP1.
unfold Ir.SmallStep.gep in HP1. dup HPOS. unfold posofs in HPOS.
rewrite <- Nat.ltb_lt in HPOS.
des_ifs.
exploit IHHGEP. ss. ss. intros HH.
inv HH.
{ inv H. inv H0. left.
symmetry in HP0.
dup HP0.
apply gep_phy_Ilb in HP0.
inv HP0. inv H0.
apply list_min_In in H2.
exists x0.
assert (x = x0).
{ eapply list_min_inj_l. eapply H. eapply H2. }
subst x.
split.
ss. ss. eapply gepinbs_phy_I_In. ss. eassumption.
eexists. eassumption. assumption.
}
{ symmetry in HP0.
apply gep_phy_Ilb in HP0.
inv HP0. inv H0.
apply list_min_In in H1.
assert (x = o0).
{ eapply list_min_inj_l. eapply H1. eassumption. }
subst x.
right. ss.
eapply gepinbs_phy_I_In. ss. eassumption.
eexists. eapply H.
ss.
}
}
{ intros. inv HP0. inv HP1.
exploit IHHGEP. ss. ss. eauto. }
Qed.
Lemma gepinbs_phy_Imin2:
forall m o I1 cid p1 p2 p0 o0 I0 n
(HP1:p1 = (Ir.ptr (Ir.pphy o I1 cid)))
(HP0:p0 = Ir.pphy o0 I0 cid)
(HGEP:gepinbs m p1 p2 p0)
(HMIN:list_min n I1),
n <= o.
Proof.
intros.
generalize dependent o.
generalize dependent o0.
generalize dependent I1.
generalize dependent I0.
generalize dependent cid.
induction HGEP.
{ intros. inv HP1. unfold Ir.SmallStep.gep in H.
unfold posofs in *. rewrite <- Nat.ltb_lt in HPOS1, HPOS2. des_ifs.
inv HMIN. rewrite List.Forall_forall in H0.
exploit H0. right. ss. left. ss.
intros. ss.
}
{ intros. inv HP0.
unfold Ir.SmallStep.gep in HP1. unfold posofs in HPOS.
rewrite <- Nat.ltb_lt in HPOS.
des_ifs.
inv HMIN. rewrite List.Forall_forall in H0.
exploit H0. right. left. ss. intros. omega.
}
{ ss. }
Qed.
Lemma gepinbs_phy_base:
forall m o1 I1 cid p1 p2 p0
(HP1:p1 = (Ir.ptr (Ir.pphy o1 I1 cid)))
(HGEP:gepinbs m p1 p2 p0),
exists o2 I2, p0 = Ir.pphy o2 I2 cid.
Proof.
intros.
generalize dependent o1.
generalize dependent I1.
generalize dependent cid.
induction HGEP.
{ intros. inv HP1. unfold Ir.SmallStep.gep in H.
des_ifs; do 3 eexists; ss.
}
{ intros. inv HP1. unfold Ir.SmallStep.gep in H.
des_ifs.
exploit IHHGEP. ss. eauto.
exploit IHHGEP. ss. eauto.
}
{ ss. }
Qed.
Lemma gepinbs_phy_Imin3:
forall m o1 o2 I1 cid p1 p2 p0 I2
(HP1:p1 = (Ir.ptr (Ir.pphy o1 I1 cid)))
(HP2:p2 = (Ir.ptr (Ir.pphy o2 I2 cid)))
(HGEP:gepinbs m p1 p2 p0),
exists n, list_min n I1 /\ list_min n I2.
Proof.
intros.
generalize dependent o1.
generalize dependent o2.
generalize dependent I1.
generalize dependent I2.
generalize dependent cid.
induction HGEP.
{ intros. inv HP1. inv HP2. unfold Ir.SmallStep.gep in *.
unfold posofs in HPOS1, HPOS2. rewrite <- Nat.ltb_lt in HPOS1, HPOS2. des_ifs.
assert (HH2 := list_min_exists n l).
inv HH2.
exists x. split.
apply list_min_swap.
apply list_min_cons. ss. rewrite twos_compl_add_PTRSZ'.
apply list_min_hd in H. lia.
ss.
apply list_min_swap.
apply list_min_cons. ss.
rewrite twos_compl_add_PTRSZ'. apply list_min_hd in H. lia. ss.
}
{ intros. inv HP1. inv HP2. dup H. dup HPOS.
unfold Ir.SmallStep.gep in H. unfold posofs in HPOS.
rewrite <- Nat.ltb_lt in HPOS.
des_ifs.
exploit IHHGEP. ss. ss. intros HH.
inv HH. inv H.
exists x. split; try assumption.
dup HGEP. eapply gepinbs_phy_base in HGEP0; try reflexivity.
inv HGEP0. inv H.
assert (x <= n).
{ eapply gepinbs_phy_Imin2. ss. ss. eassumption. ss. }
apply list_min_cons; try omega.
apply list_min_cons.
ss.
rewrite twos_compl_add_PTRSZ'. lia. ss.
}
{ intros.
inv HP2. inv HP1.
unfold Ir.SmallStep.gep in H. unfold posofs in HPOS. rewrite <- Nat.ltb_lt in HPOS.
des_ifs.
exploit IHHGEP. ss. ss. intros HH.
inv HH. inv H.
exists x. split; try assumption.
dup HGEP. eapply gepinbs_phy_base in HGEP; try reflexivity.
inv HGEP. inv H.
assert (x <= n).
{ eapply gepinbs_phy_Imin2. ss. ss. apply gepinbs_sym in HGEP0.
eassumption. ss. }
apply list_min_cons; try omega.
apply list_min_cons. ss.
rewrite twos_compl_add_PTRSZ'. lia. ss.
}
Qed.
Lemma gep_phy_Iub2:
forall o I cid o' I' cid' ofs t m
(HGEP:Ir.SmallStep.gep (Ir.pphy o I cid) ofs t m true = Ir.ptr (Ir.pphy o' I' cid'))
(HPOS:posofs ofs t),
list_max o' I' \/ (exists n, list_max n I /\ list_max n I').
Proof.
intros.
destruct I.
{ left.
unfold Ir.SmallStep.gep in HGEP.
unfold posofs in HPOS.
des_ifs.
{ unfold Ir.SmallStep.twos_compl_add.
unfold Ir.SmallStep.twos_compl.
unfold list_max. split.
right. constructor. ss.
constructor. rewrite Nat.mod_small. lia.
rewrite Ir.PTRSZ_MEMSZ. rewrite Nat.ltb_lt in Heq0. ss.
constructor. ss.
constructor.
}
{ rewrite Nat.ltb_ge in Heq. omega. }
}
{ assert (HH := list_max_exists n I).
inv HH.
unfold Ir.SmallStep.gep in HGEP.
des_ifs.
{ destruct (x <=? Ir.SmallStep.twos_compl_add o (ofs * Ir.ty_bytesz t) Ir.PTRSZ)
eqn:HLE.
{ left.
constructor.
right. left. ss.
constructor. rewrite twos_compl_add_PTRSZ. lia.
rewrite Nat.ltb_lt in Heq0. ss.
constructor. ss.
inv H.
rewrite List.Forall_forall in *.
intros. apply H1 in H. rewrite Nat.leb_le in HLE.
rewrite twos_compl_add_PTRSZ. eapply Nat.le_trans. eapply H.
rewrite twos_compl_add_PTRSZ in HLE. ss.
rewrite Nat.ltb_lt in Heq0. ss. rewrite Nat.ltb_lt in Heq0. ss.
}
{ right. exists x.
split. ss.
rewrite Nat.leb_gt in HLE.
rewrite twos_compl_add_PTRSZ in HLE.
constructor. right. right. inv H. ss.
constructor.
lia.
constructor. rewrite twos_compl_add_PTRSZ. lia.
rewrite Nat.ltb_lt in Heq0. lia.
inv H. rewrite List.Forall_forall in *.
intros. apply H1 in H. ss.
rewrite Nat.ltb_lt in Heq0. ss.
}
}
{ unfold posofs in HPOS. rewrite Nat.ltb_ge in Heq. omega. }
}
Qed.
Theorem gepinbs_after_icmpeq_true:
forall md st st' r ptrty op1 op2 v1 v2 e pbase
(HWF:Ir.Config.wf md st)
(HINST:Some (Ir.Inst.iicmp_eq r ptrty op1 op2) = Ir.Config.cur_inst md st)
(HOP1:Some v1 = Ir.Config.get_val st op1)
(HOP2:Some v2 = Ir.Config.get_val st op2)
(* gepinbs holds *)
(HEQPROP:gepinbs (Ir.Config.m st) v1 v2 pbase)
(* have a small step *)
(HSTEP:Ir.SmallStep.sstep md st (Ir.SmallStep.sr_success e st'))
(* p1 == p2 is true *)
(HTRUE:Some (Ir.num 1) = Ir.Config.get_val st' (Ir.opreg r)),
v1 = v2 \/
(exists p1 p2, Ir.ptr p1 = v1 /\ Ir.ptr p2 = v2 /\ phys_minmaxI p1 p2).
Proof.
intros.
inv HSTEP; try congruence.
{ inv HISTEP;try congruence.
{ unfold Ir.SmallStep.inst_det_step in HNEXT. rewrite <- HINST in HNEXT.
rewrite <- HOP1, <- HOP2 in HNEXT.
dup HEQPROP. apply gepinbs_notnum in HEQPROP0.
inv HEQPROP0.
destruct v1.
{ exfalso. eapply H. eexists. ss. }
destruct v2.
{ exfalso. eapply H0. eexists. ss. }
des_ifs.
clear H H0.
destruct p.
{ (* log *)
destruct p0.
{ dup HEQPROP.
eapply gepinbs_log_sameblk in HEQPROP; try reflexivity.
subst b0.
unfold Ir.SmallStep.icmp_eq_ptr in Heq. rewrite Nat.eqb_refl in Heq.
inv Heq.
rewrite Ir.SmallStep.get_val_update_reg_and_incrpc in HTRUE.
unfold Ir.Config.get_val in HTRUE.
rewrite Ir.Config.get_rval_update_rval_id in HTRUE.
unfold Ir.SmallStep.to_num in HTRUE.
des_ifs. rewrite Nat.eqb_eq in Heq. subst n.
left. ss.
{ unfold Ir.Config.cur_inst in HINST.
unfold Ir.Config.cur_fdef_pc in HINST.
des_ifs. }
}
{ (* cannot be phy *)
eapply gepinbs_log_neverphy in HEQPROP; try reflexivity.
exfalso. apply HEQPROP. do 3 eexists. ss.
}
}
{ (* phy *)
destruct p0.
{ (* cannot be log *)
eapply gepinbs_phy_neverlog in HEQPROP; try reflexivity.
exfalso. apply HEQPROP. do 3 eexists.
}
{ right.
unfold Ir.SmallStep.icmp_eq_ptr in Heq.
unfold Ir.SmallStep.p2N in Heq.
rewrite Nat.min_id in Heq.
unfold Ir.SmallStep.twos_compl in Heq.
rewrite Ir.PTRSZ_MEMSZ in Heq.
rewrite Nat.mod_small in Heq.
inv Heq.
rewrite Ir.SmallStep.get_val_update_reg_and_incrpc in HTRUE.
unfold Ir.Config.get_val in HTRUE.
rewrite Ir.Config.get_rval_update_rval_id in HTRUE.
unfold Ir.SmallStep.to_num in HTRUE.
inv HTRUE.
des_ifs.
rewrite Nat.eqb_eq in Heq. subst n.
dup HEQPROP.
eapply gepinbs_phy_samecid in HEQPROP0; try reflexivity.
subst o.
dup HEQPROP. eapply gepinbs_phy_base in HEQPROP0; try reflexivity.
inv HEQPROP0. inv H.
eexists. eexists. split. ss. split. ss.
unfold phys_minmaxI.
dup HEQPROP.
eapply gepinbs_phy_Imin3 in HEQPROP0; try reflexivity.
dup HEQPROP.
eapply gepinbs_phy_Imax in HEQPROP1.
2: ss. 2: ss.
apply gepinbs_sym in HEQPROP.
eapply gepinbs_phy_Imax in HEQPROP.
2:ss. 2:ss.
inv HEQPROP0. inv H.
inv HEQPROP.
{ inv H. inv H3. inv H4.
inv HEQPROP1.
{ inv H4. inv H6. inv H7.
assert (x2 = x3).
{ eapply list_max_inj_l. eapply H3. ss. }
subst x2.
do 6 eexists.
split. ss. split. ss.
split. eassumption.
split. ss.
split. eassumption.
ss.
}
{ inv H4. apply H7 in H3.
omega. }
}
{ inv H.
inv HEQPROP1.
{ inv H. inv H5. inv H6. apply H4 in H5. omega. }
{ inv H.
do 6 eexists.
split. ss. split. ss.
split. eassumption. split. ss.
split. eassumption. ss.
}
}
{ unfold Ir.Config.cur_inst in HINST. unfold Ir.Config.cur_fdef_pc in HINST.
des_ifs.
}
{ inv HWF.
exploit wf_ptr. rewrite <- HOP2. reflexivity.
intros HH.
unfold Ir.Config.ptr_wf in HH.
inv HH. eapply H0. reflexivity.
}
}
}
{ inv HNEXT.
rewrite Ir.SmallStep.get_val_update_reg_and_incrpc in HTRUE.
unfold Ir.Config.get_val in HTRUE.
rewrite Ir.Config.get_rval_update_rval_id in HTRUE.
inv HTRUE.
unfold Ir.Config.cur_inst in HINST. unfold Ir.Config.cur_fdef_pc in HINST.
des_ifs.
}
{ inv HNEXT.
rewrite Ir.SmallStep.get_val_update_reg_and_incrpc in HTRUE.
unfold Ir.Config.get_val in HTRUE.
rewrite Ir.Config.get_rval_update_rval_id in HTRUE.
inv HTRUE.
unfold Ir.Config.cur_inst in HINST. unfold Ir.Config.cur_fdef_pc in HINST.
des_ifs.
}
}
{ eapply gepinbs_icmp_det in HEQPROP.
rewrite HNONDET in HEQPROP. inv HEQPROP.
congruence. congruence.
}
}
{ unfold Ir.SmallStep.t_step in HTSTEP.
apply Ir.Config.cur_inst_not_cur_terminator in HINST.
des_ifs.
}
Qed.
Lemma inbounds_abs_minmax:
forall ofsmin ofsmax mb ofss
(HMIN:list_min ofsmin ofss)
(HMAX:list_max ofsmax ofss)
(HINB:Ir.MemBlock.inbounds_abs ofsmin mb = true)
(HINB:Ir.MemBlock.inbounds_abs ofsmax mb = true),
List.forallb (fun i : nat => Ir.MemBlock.inbounds_abs i mb)
ofss = true.
Proof.
intros.
unfold Ir.MemBlock.inbounds_abs in *.
unfold in_range in *.
rewrite List.forallb_forall.
intros.
repeat (rewrite andb_true_iff in *). repeat (rewrite Nat.leb_le in *).
unfold list_min in HMIN.
unfold list_max in HMAX.
inv HMIN. inv HMAX.
rewrite List.Forall_forall in *.
dup H.
apply H1 in H4. apply H3 in H. omega.
Qed.
Lemma inbounds_blocks2_minmax: