forked from SJTU-PLV/direct-refinement-popl24-artifact
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Deadcodeproof.v
1928 lines (1829 loc) · 77.7 KB
/
Deadcodeproof.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
(* *********************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Xavier Leroy, INRIA Paris-Rocquencourt *)
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
(* under the terms of the INRIA Non-Commercial License Agreement. *)
(* *)
(* *********************************************************************)
(** Elimination of unneeded computations over RTL: correctness proof. *)
Require Import FunInd.
Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
Require Import AST Linking.
Require Import Values Memory Globalenvs Events Smallstep.
Require Import LanguageInterface Invariant Inject InjectFootprint.
Require Import Registers Op RTL.
Require Import ValueDomain ValueAnalysis NeedDomain NeedOp Deadcode.
Definition match_prog (prog tprog: RTL.program) :=
match_program (fun _ f tf => transf_fundef (romem_for prog) f = OK tf) eq prog tprog.
Lemma transf_program_match:
forall prog tprog, transf_program prog = OK tprog -> match_prog prog tprog.
Proof.
intros. eapply match_transform_partial_program_contextual; eauto.
Qed.
(** * Relating the memory states *)
(** The [magree] predicate is a variant of [Mem.inject] where we
allow the contents of the two memory states to differ arbitrarily
on some locations. The predicate [P] is true on the locations whose
contents must be in the [inject] relation. *)
Definition locset := block -> Z -> Prop.
Record magree (f:meminj) (m1 m2: mem) (P: locset) : Prop := mk_magree {
ma_perm:
forall b1 b2 ofs delta k p,
f b1 = Some (b2,delta) -> Mem.perm m1 b1 ofs k p -> Mem.perm m2 b2 (ofs + delta) k p;
ma_align:
forall b1 b2 delta ofs chunk p,
f b1 = Some (b2, delta) ->
Mem.range_perm m1 b1 ofs (ofs + size_chunk chunk) Max p -> (align_chunk chunk | delta);
ma_perm_inv:
forall b1 b2 delta ofs k p, f b1 = Some (b2, delta) ->
Mem.perm m2 b2 (ofs + delta) k p -> Mem.perm m1 b1 ofs k p \/ ~Mem.perm m1 b1 ofs Max Nonempty;
ma_memval:
forall b1 b2 delta ofs, f b1 = Some (b2, delta) ->
Mem.perm m1 b1 ofs Cur Readable ->
P b1 ofs ->
memval_inject f (ZMap.get ofs (NMap.get _ b1 (Mem.mem_contents m1)))
(ZMap.get (ofs + delta) (NMap.get _ b2 (Mem.mem_contents m2)));
ma_freeblocks:
forall b, ~ Mem.valid_block m1 b -> f b = None;
ma_mappedblocks:
forall b b' delta, f b = Some (b', delta) -> Mem.valid_block m2 b';
ma_no_overlap : Mem.meminj_no_overlap f m1;
ma_representable : forall b b' delta ofs, f b = Some (b', delta) ->
Mem.perm m1 b (Ptrofs.unsigned ofs) Max Nonempty \/
Mem.perm m1 b (Ptrofs.unsigned ofs - 1) Max Nonempty ->
delta >= 0 /\ 0 <= Ptrofs.unsigned ofs + delta <= Ptrofs.max_unsigned;
}.
Lemma magree_monotone:
forall m1 m2 j (P Q: locset),
magree j m1 m2 P ->
(forall b ofs, Q b ofs -> P b ofs) ->
magree j m1 m2 Q.
Proof.
intros. destruct H. constructor; eauto.
Qed.
Lemma minject_agree:
forall j m1 m2 P, Mem.inject j m1 m2 -> magree j m1 m2 P.
Proof.
intros. destruct H. destruct mi_inj. constructor; intros; eauto.
Qed.
Lemma magree_inject:
forall j m1 m2 (P: locset),
(forall b ofs, P b ofs) ->
magree j m1 m2 P -> Mem.inject j m1 m2.
Proof.
intros. destruct H0. constructor; eauto. constructor; eauto.
Qed.
Lemma magree_loadbytes:
forall j m1 m2 P b1 b2 delta ofs n bytes,
magree j m1 m2 P ->
Mem.loadbytes m1 b1 ofs n = Some bytes ->
j b1 = Some (b2,delta) ->
(forall i, ofs <= i < ofs + n -> P b1 i) ->
exists bytes', Mem.loadbytes m2 b2 (ofs + delta) n = Some bytes' /\ list_forall2 (memval_inject j) bytes bytes'.
Proof.
assert (GETN: forall c1 c2 n ofs j delta,
(forall i, ofs <= i < ofs + Z.of_nat n -> memval_inject j (ZMap.get i c1) (ZMap.get (i + delta) c2)) ->
list_forall2 (memval_inject j) (Mem.getN n ofs c1) (Mem.getN n (ofs + delta) c2)).
{
induction n; intros; simpl.
constructor.
rewrite Nat2Z.inj_succ in H. constructor.
apply H. lia.
replace (ofs + delta + 1) with (ofs + 1 + delta) by lia.
apply IHn. intros; apply H; lia.
}
Local Transparent Mem.loadbytes.
unfold Mem.loadbytes; intros. destruct H.
destruct (Mem.range_perm_dec m1 b1 ofs (ofs + n) Cur Readable); inv H0.
rewrite pred_dec_true. econstructor; split; eauto.
apply GETN. intros. rewrite Z_to_nat_max in H.
assert (ofs <= i < ofs + n) by extlia.
apply ma_memval0; auto.
red; intros; eauto.
red in r. replace (ofs0) with ((ofs0 - delta) + delta) by lia.
eapply ma_perm0; eauto. eapply r. lia.
Qed.
Lemma magree_load:
forall j m1 m2 P chunk b1 b2 delta ofs v,
magree j m1 m2 P ->
Mem.load chunk m1 b1 ofs = Some v ->
j b1 = Some (b2, delta) ->
(forall i, ofs <= i < ofs + size_chunk chunk -> P b1 i) ->
exists v', Mem.load chunk m2 b2 (ofs + delta) = Some v' /\ Val.inject j v v'.
Proof.
intros. exploit Mem.load_valid_access; eauto. intros [A B].
exploit Mem.load_loadbytes; eauto. intros [bytes [C D]].
exploit magree_loadbytes; eauto. intros [bytes' [E F]].
exists (decode_val chunk bytes'); split.
apply Mem.loadbytes_load; auto.
apply Z.divide_add_r; eauto.
inv H. eapply ma_align0; eauto with mem.
subst v. apply decode_val_inject; auto.
Qed.
Lemma magree_storebytes_parallel:
forall j m1 m2 (P Q: locset) b1 b2 delta ofs bytes1 m1' bytes2,
magree j m1 m2 P ->
Mem.storebytes m1 b1 ofs bytes1 = Some m1' ->
j b1 = Some (b2,delta) ->
(forall b' i, Q b' i ->
b' <> b1 \/ i < ofs \/ ofs + Z.of_nat (length bytes1) <= i ->
P b' i) ->
list_forall2 (memval_inject j) bytes1 bytes2 ->
exists m2', Mem.storebytes m2 b2 (ofs + delta) bytes2 = Some m2' /\ magree j m1' m2' Q.
Proof.
assert (SETN: forall (access: Z -> Prop) j bytes1 bytes2 delta,
list_forall2 (memval_inject j) bytes1 bytes2 ->
forall p c1 c2,
(forall i, access i -> i < p \/ p + Z.of_nat (length bytes1) <= i -> memval_inject j (ZMap.get i c1) (ZMap.get (i + delta) c2)) ->
forall q, access q ->
memval_inject j (ZMap.get q (Mem.setN bytes1 p c1))
(ZMap.get (q + delta) (Mem.setN bytes2 (p + delta) c2))).
{
induction 1; intros; simpl.
- apply H; auto. simpl. lia.
- simpl length in H1; rewrite Nat2Z.inj_succ in H1.
replace (p + delta + 1) with (p + 1 + delta) by lia.
apply IHlist_forall2; auto.
intros. rewrite ! ZMap.gsspec. destruct (ZIndexed.eq i p).
rewrite pred_dec_true. auto. lia. rewrite pred_dec_false.
eapply H1; auto. unfold ZIndexed.t in *; lia. lia.
}
intros.
destruct (Mem.range_perm_storebytes m2 b2 (ofs + delta) bytes2) as [m2' ST2].
{ erewrite <- list_forall2_length by eauto. red; intros.
replace (ofs0) with ((ofs0 - delta) + delta) by lia.
eapply ma_perm; eauto.
eapply Mem.storebytes_range_perm; eauto. lia. }
exists m2'; split; auto.
constructor; intros.
- eapply Mem.perm_storebytes_1; eauto. eapply ma_perm; eauto.
eapply Mem.perm_storebytes_2; eauto.
- exploit ma_align; eauto. red. eauto using Mem.perm_storebytes_2.
- exploit ma_perm_inv; eauto using Mem.perm_storebytes_2.
intuition eauto using Mem.perm_storebytes_1, Mem.perm_storebytes_2.
- rewrite (Mem.storebytes_mem_contents _ _ _ _ _ H0).
rewrite (Mem.storebytes_mem_contents _ _ _ _ _ ST2).
rewrite ! NMap.gsspec. destruct (NMap.elt_eq b0 b1).
+ subst b0. rewrite H1 in H4. inv H4. rewrite pred_dec_true; auto.
apply SETN with (access := fun ofs => Mem.perm m1' b1 ofs Cur Readable /\ Q b1 ofs); auto.
intros. destruct H4. eapply ma_memval; eauto.
eapply Mem.perm_storebytes_2; eauto.
+ destruct (NMap.elt_eq b3 b2).
* subst. rewrite Mem.setN_other. eapply ma_memval; eauto. eapply Mem.perm_storebytes_2; eauto.
intros. assert (b2 <> b2 \/ ofs0 + delta0 <> (r - delta) + delta).
eapply ma_no_overlap; eauto 6 with mem.
exploit Mem.storebytes_range_perm. eexact H0. instantiate (1:= r - delta).
rewrite (list_forall2_length H3). lia.
eauto with mem. destruct H8. congruence. lia.
* eapply ma_memval; eauto. eapply Mem.perm_storebytes_2; eauto.
- eapply ma_freeblocks; eauto with mem.
- eapply Mem.storebytes_valid_block_1; eauto with mem. eapply ma_mappedblocks; eauto.
- red. intros. eapply ma_no_overlap; eauto with mem.
- eapply ma_representable; eauto with mem.
destruct H5. left. eapply Mem.perm_storebytes_2; eauto.
right. eapply Mem.perm_storebytes_2; eauto.
Qed.
Lemma magree_store_parallel:
forall j m1 m2 (P Q: locset) chunk b1 b2 delta ofs v1 m1' v2,
magree j m1 m2 P ->
Mem.store chunk m1 b1 ofs v1 = Some m1' ->
vagree j v1 v2 (store_argument chunk) ->
j b1 = Some (b2, delta) ->
(forall b' i, Q b' i ->
b' <> b1 \/ i < ofs \/ ofs + size_chunk chunk <= i ->
P b' i) ->
exists m2', Mem.store chunk m2 b2 (ofs + delta) v2 = Some m2' /\ magree j m1' m2' Q.
Proof.
intros.
exploit Mem.store_valid_access_3; eauto. intros [A B].
exploit Mem.store_storebytes; eauto. intros SB1.
exploit magree_storebytes_parallel. eauto. eauto. eauto.
instantiate (1 := Q). intros. rewrite encode_val_length in H5.
rewrite <- size_chunk_conv in H5. apply H3; auto.
eapply store_argument_sound; eauto.
intros [m2' [SB2 AG]].
exists m2'; split; auto.
apply Mem.storebytes_store; auto.
eapply Z.divide_add_r; eauto. eapply ma_align; eauto.
red. intros.
eapply Mem.perm_store_1; eauto.
exploit A; eauto with mem.
Qed.
Lemma magree_storebytes_left:
forall j m1 m2 P b1 ofs bytes1 m1',
magree j m1 m2 P ->
Mem.storebytes m1 b1 ofs bytes1 = Some m1' ->
(forall i, ofs <= i < ofs + Z.of_nat (length bytes1) -> ~(P b1 i)) ->
magree j m1' m2 P.
Proof.
intros. constructor; intros.
- eapply ma_perm; eauto. eapply Mem.perm_storebytes_2; eauto.
- eapply ma_align; eauto. red. intros. eauto using Mem.perm_storebytes_2.
- exploit ma_perm_inv; eauto.
intuition eauto using Mem.perm_storebytes_1, Mem.perm_storebytes_2.
- rewrite (Mem.storebytes_mem_contents _ _ _ _ _ H0).
rewrite NMap.gsspec. destruct (NMap.elt_eq b0 b1).
+ subst b0. rewrite Mem.setN_outside. eapply ma_memval; eauto. eapply Mem.perm_storebytes_2; eauto.
destruct (zlt ofs0 ofs); auto. destruct (zle (ofs + Z.of_nat (length bytes1)) ofs0); try lia.
assert(ofs <= ofs0 < ofs + Z.of_nat(Datatypes.length bytes1)) by lia.
apply H1 in H5. congruence.
+ eapply ma_memval; eauto. eapply Mem.perm_storebytes_2; eauto.
- eapply ma_freeblocks; eauto with mem.
- eapply ma_mappedblocks; eauto with mem.
- red. intros. eapply ma_no_overlap; eauto with mem.
- eapply ma_representable; eauto with mem.
destruct H3. left. eauto with mem. right. eauto with mem.
Qed.
Lemma magree_store_left:
forall j m1 m2 P chunk b1 ofs v1 m1',
magree j m1 m2 P ->
Mem.store chunk m1 b1 ofs v1 = Some m1' ->
(forall i, ofs <= i < ofs + size_chunk chunk -> ~(P b1 i)) ->
magree j m1' m2 P.
Proof.
intros. eapply magree_storebytes_left; eauto.
eapply Mem.store_storebytes; eauto.
intros. rewrite encode_val_length in H2.
rewrite <- size_chunk_conv in H2. apply H1; auto.
Qed.
Lemma magree_free:
forall j m1 m2 (P Q: locset) b1 b2 delta lo hi m1',
magree j m1 m2 P ->
Mem.free m1 b1 lo hi = Some m1' ->
j b1 = Some (b2, delta) ->
(forall b' i, Q b' i ->
b' <> b1 \/ ~(lo <= i < hi) ->
P b' i) ->
exists m2', Mem.free m2 b2 (lo + delta) (hi + delta) = Some m2' /\ magree j m1' m2' Q.
Proof.
intros.
destruct (Mem.range_perm_free m2 b2 (lo + delta) (hi + delta)) as [m2' FREE].
red; intros. replace (ofs) with ((ofs - delta) + delta) by lia.
eapply ma_perm; eauto. eapply Mem.free_range_perm; eauto. lia.
exists m2'; split; auto.
constructor; intros.
- (* permissions *)
assert (Mem.perm m2 b3 (ofs + delta0) k p). { eapply ma_perm; eauto. eapply Mem.perm_free_3; eauto. }
exploit Mem.perm_free_inv; eauto. intros [[A B] | A]; auto.
subst b3. exfalso. destruct (eq_block b0 b1). subst.
rewrite H1 in H3. inv H3.
eelim Mem.perm_free_2. eexact H0. 2: eauto. lia.
exploit ma_no_overlap; eauto. eapply Mem.perm_free_3; eauto with mem.
instantiate (1:= ofs + delta0 - delta).
apply Mem.free_range_perm in H0. red in H0. exploit H0; eauto with mem. lia.
intros [|]. eauto. extlia.
- eapply ma_align; eauto. red. eauto using Mem.perm_free_3; eauto.
- (* inverse permissions *)
exploit ma_perm_inv; eauto using Mem.perm_free_3. intros [A|A].
eapply Mem.perm_free_inv in A; eauto. destruct A as [[A B] | A]; auto.
subst b0; right; eapply Mem.perm_free_2; eauto.
right; intuition eauto using Mem.perm_free_3.
- (* contents *)
rewrite (Mem.free_result _ _ _ _ _ H0).
rewrite (Mem.free_result _ _ _ _ _ FREE).
simpl. eapply ma_memval; eauto. eapply Mem.perm_free_3; eauto.
apply H2; auto. destruct (eq_block b0 b1); auto.
subst b0. right. red; intros. eelim Mem.perm_free_2. eexact H0. eauto. eauto.
- eapply ma_freeblocks; eauto with mem.
- eapply Mem.valid_block_free_1; eauto with mem. eapply ma_mappedblocks; eauto.
- red. intros. eapply ma_no_overlap; eauto with mem.
- eapply ma_representable; eauto with mem.
destruct H4; eauto with mem.
Qed.
Lemma magree_valid_access:
forall j m1 m2 (P: locset) chunk b1 b2 delta ofs p,
magree j m1 m2 P ->
j b1 = Some (b2, delta) ->
Mem.valid_access m1 chunk b1 ofs p ->
Mem.valid_access m2 chunk b2 (ofs + delta) p.
Proof.
intros. destruct H1; split; auto.
red; intros. replace ofs0 with ((ofs0 - delta) + delta) by lia.
eapply ma_perm; eauto. eapply H1; eauto. lia.
apply Z.divide_add_r; eauto.
eapply ma_align; eauto. red. intros. eauto with mem.
Qed.
(** * Properties of the need environment *)
Lemma add_need_all_eagree:
forall j e e' r ne,
eagree j e e' (add_need_all r ne) -> eagree j e e' ne.
Proof.
intros; red; intros. generalize (H r0). unfold add_need_all.
rewrite NE.gsspec. destruct (peq r0 r); auto with na.
Qed.
Lemma add_need_all_inject:
forall j e e' r ne,
eagree j e e' (add_need_all r ne) -> Val.inject j e#r e'#r.
Proof.
intros. generalize (H r); unfold add_need_all.
rewrite NE.gsspec, peq_true. auto with na.
Qed.
Lemma add_need_eagree:
forall j e e' r nv ne,
eagree j e e' (add_need r nv ne) -> eagree j e e' ne.
Proof.
intros; red; intros. generalize (H r0); unfold add_need.
rewrite NE.gsspec. destruct (peq r0 r); auto.
subst r0. intros. eapply nge_agree; eauto. apply nge_lub_r.
Qed.
Lemma add_need_vagree:
forall j e e' r nv ne,
eagree j e e' (add_need r nv ne) -> vagree j e#r e'#r nv.
Proof.
intros. generalize (H r); unfold add_need.
rewrite NE.gsspec, peq_true. intros. eapply nge_agree; eauto. apply nge_lub_l.
Qed.
Lemma add_needs_all_eagree:
forall j rl e e' ne,
eagree j e e' (add_needs_all rl ne) -> eagree j e e' ne.
Proof.
induction rl; simpl; intros.
auto.
apply IHrl. eapply add_need_all_eagree; eauto.
Qed.
Lemma add_needs_all_inject:
forall j rl e e' ne,
eagree j e e' (add_needs_all rl ne) -> Val.inject_list j e##rl e'##rl.
Proof.
induction rl; simpl; intros.
constructor.
constructor. eapply add_need_all_inject; eauto.
eapply IHrl. eapply add_need_all_eagree; eauto.
Qed.
Lemma add_needs_eagree:
forall j rl nvl e e' ne,
eagree j e e' (add_needs rl nvl ne) -> eagree j e e' ne.
Proof.
induction rl; simpl; intros.
auto.
destruct nvl. apply add_needs_all_eagree with (a :: rl); auto.
eapply IHrl. eapply add_need_eagree; eauto.
Qed.
Lemma add_needs_vagree:
forall j rl nvl e e' ne,
eagree j e e' (add_needs rl nvl ne) -> vagree_list j e##rl e'##rl nvl.
Proof.
induction rl; simpl; intros.
constructor.
destruct nvl.
apply vagree_inject_list. eapply add_needs_all_inject with (rl := a :: rl); eauto.
constructor. eapply add_need_vagree; eauto.
eapply IHrl. eapply add_need_eagree; eauto.
Qed.
Lemma add_ros_need_eagree:
forall j e e' ros ne, eagree j e e' (add_ros_need_all ros ne) -> eagree j e e' ne.
Proof.
intros. destruct ros; simpl in *. eapply add_need_all_eagree; eauto. auto.
Qed.
Global Hint Resolve add_need_all_eagree add_need_all_inject
add_need_eagree add_need_vagree
add_needs_all_eagree add_needs_all_inject
add_needs_eagree add_needs_vagree
add_ros_need_eagree: na.
Lemma eagree_init_regs:
forall j rl vl1 vl2 ne,
Val.inject_list j vl1 vl2 ->
eagree j (init_regs vl1 rl) (init_regs vl2 rl) ne.
Proof.
induction rl; intros until ne; intros LD; simpl.
- red; auto with na.
- inv LD.
+ red; auto with na.
+ apply eagree_update; auto with na.
Qed.
(** * Basic properties of the translation *)
Section PRESERVATION.
Variable prog: program.
Variable tprog: program.
Variables se tse: Genv.symtbl.
Variable m0: mem.
Variable w : inj_world.
Hypothesis SUPm0: injw_sup_l w = Mem.support m0.
Hypothesis GE: inj_stbls w se tse.
Hypothesis SEVALID: Genv.valid_for (erase_program prog) se.
Hypothesis TRANSF: match_prog prog tprog.
Let ge := Genv.globalenv se prog.
Let tge := Genv.globalenv tse tprog.
(*
Lemma match_stbls_incr: forall w',
inj_incr w w' -> inj_stbls w' se tse.
Proof.
intros.
exploit inj_stbls_subrel; eauto.
Qed.
*)
Lemma functions_translated:
forall (j: meminj) (v tv: val) (f: RTL.fundef),
Genv.match_stbls j se tse ->
Genv.find_funct ge v = Some f ->
Val.inject j v tv ->
exists tf,
Genv.find_funct tge tv = Some tf /\ transf_fundef (romem_for prog) f = OK tf.
Proof.
intros. eapply Genv.find_funct_transf_partial; eauto.
Qed.
Lemma sig_function_translated:
forall rm f tf,
transf_fundef rm f = OK tf ->
funsig tf = funsig f.
Proof.
intros; destruct f; monadInv H.
unfold transf_function in EQ.
destruct (analyze (ValueAnalysis.analyze rm f) f); inv EQ; auto.
auto.
Qed.
Lemma stacksize_translated:
forall rm f tf,
transf_function rm f = OK tf -> tf.(fn_stacksize) = f.(fn_stacksize).
Proof.
unfold transf_function; intros. destruct (analyze (ValueAnalysis.analyze rm f) f); inv H; auto.
Qed.
Definition vanalyze (cu: program) (f: function) :=
ValueAnalysis.analyze (romem_for cu) f.
Lemma transf_function_at:
forall cu f tf an pc instr,
transf_function (romem_for cu) f = OK tf ->
analyze (vanalyze cu f) f = Some an ->
f.(fn_code)!pc = Some instr ->
tf.(fn_code)!pc = Some(transf_instr (vanalyze cu f) an pc instr).
Proof.
intros. unfold transf_function in H. unfold vanalyze in H0. rewrite H0 in H. inv H; simpl.
rewrite PTree.gmap. rewrite H1; auto.
Qed.
Lemma is_dead_sound_1:
forall nv, is_dead nv = true -> nv = Nothing.
Proof.
destruct nv; simpl; congruence.
Qed.
Lemma is_dead_sound_2:
forall nv, is_dead nv = false -> nv <> Nothing.
Proof.
intros; red; intros. subst nv; discriminate.
Qed.
Hint Resolve is_dead_sound_1 is_dead_sound_2: na.
Lemma is_int_zero_sound:
forall nv, is_int_zero nv = true -> nv = I Int.zero.
Proof.
unfold is_int_zero; destruct nv; try discriminate.
predSpec Int.eq Int.eq_spec m Int.zero; congruence.
Qed.
Lemma ros_address_translated:
forall j ros rs trs ne,
Genv.match_stbls j se tse ->
eagree j rs trs (add_ros_need_all ros ne) ->
Val.inject j (ros_address ge ros rs) (ros_address tge ros trs).
Proof.
intros. unfold ros_address, Genv.find_funct. destruct ros; auto.
specialize (H0 r). unfold NE.get in H0. cbn in H0. rewrite PTree.gss in H0. auto.
eapply symbol_address_inject; eauto.
Qed.
(** * Semantic invariant *)
Inductive match_stackframes (j:meminj): stackframe -> stackframe -> Prop :=
| match_stackframes_intro:
forall res f sp sp' pc e tf te an
(FUN: transf_function (romem_for prog) f = OK tf)
(ANL: analyze (vanalyze prog f) f = Some an)
(RES: forall v tv,
Val.inject j v tv ->
eagree j (e#res <- v) (te#res<- tv)
(fst (transfer f (vanalyze prog f) pc an!!pc)))
(PC: j sp = Some (sp',0)),
match_stackframes j (Stackframe res f (Vptr sp Ptrofs.zero) pc e)
(Stackframe res tf (Vptr sp' Ptrofs.zero) pc te).
Lemma vagree_incr: forall j j' v w x, vagree j v w x -> inject_incr j j' -> vagree j' v w x.
Proof.
intros. destruct x; simpl in *; eauto.
Qed.
Lemma eagree_incr : forall j j' rs rs' x,
eagree j rs rs' x -> inject_incr j j' -> eagree j' rs rs' x.
Proof.
intros. red. intros.
eapply vagree_incr; eauto.
Qed.
Lemma match_stackframes_incr : forall j j' s s',
list_forall2 (match_stackframes j) s s' ->
inject_incr j j' ->
list_forall2 (match_stackframes j') s s'.
Proof.
induction 1; intros.
- constructor.
- constructor; eauto. inv H.
econstructor; eauto. intros. red.
intros. simpl. destruct (peq r res).
+ subst. rewrite !Regmap.gss. eapply vagree_inject; eauto.
+ rewrite !Regmap.gso; eauto.
eapply vagree_incr; eauto.
assert (Val.inject j Vundef Vundef). constructor.
apply RES in H2. red in H2. generalize (H2 r).
rewrite !Regmap.gso; eauto.
Qed.
Inductive match_states: state -> state -> Prop :=
| match_regular_states:
forall s f sp pc e m ts tf te tm an j sp'
(STACKS: list_forall2 (match_stackframes j) s ts)
(FUN: transf_function (romem_for prog) f = OK tf)
(ANL: analyze (vanalyze prog f) f = Some an)
(ENV: eagree j e te (fst (transfer f (vanalyze prog f) pc an!!pc)))
(MEM: magree j m tm (nlive ge sp (snd (transfer f (vanalyze prog f) pc an!!pc))))
(SP: j sp = Some (sp',0))
(RO: ro_acc m0 m)
(INCR: inj_incr w (injw j (Mem.support m) (Mem.support tm))),
match_states (State s f (Vptr sp Ptrofs.zero) pc e m)
(State ts tf (Vptr sp' Ptrofs.zero) pc te tm)
| match_call_states:
forall s vf args m ts tvf targs tm j
(STACKS: list_forall2 (match_stackframes j) s ts)
(VF: Val.inject j vf tvf)
(ARGS: Val.inject_list j args targs)
(MEM: Mem.inject j m tm)
(RO: ro_acc m0 m)
(INCR: inj_incr w (injw j (Mem.support m) (Mem.support tm))),
match_states (Callstate s vf args m)
(Callstate ts tvf targs tm)
| match_return_states:
forall s v m ts tv tm j
(STACKS: list_forall2 (match_stackframes j) s ts)
(RES: Val.inject j v tv)
(MEM: Mem.inject j m tm)
(RO: ro_acc m0 m)
(INCR: inj_incr w (injw j (Mem.support m) (Mem.support tm))),
match_states (Returnstate s v m)
(Returnstate ts tv tm).
(** [match_states] and CFG successors *)
Lemma analyze_successors:
forall cu f an pc instr pc',
analyze (vanalyze cu f) f = Some an ->
f.(fn_code)!pc = Some instr ->
In pc' (successors_instr instr) ->
NA.ge an!!pc (transfer f (vanalyze cu f) pc' an!!pc').
Proof.
intros. eapply DS.fixpoint_solution; eauto.
intros. unfold transfer; rewrite H2. destruct a. apply DS.L.eq_refl.
Qed.
Lemma match_succ_states:
forall s f sp pc e m ts tf te tm an pc' instr ne nm j sp'
(STACKS: list_forall2 (match_stackframes j) s ts)
(FUN: transf_function (romem_for prog) f = OK tf)
(ANL: analyze (vanalyze prog f) f = Some an)
(INSTR: f.(fn_code)!pc = Some instr)
(SUCC: In pc' (successors_instr instr))
(ANPC: an!!pc = (ne, nm))
(ENV: eagree j e te ne)
(MEM: magree j m tm (nlive ge sp nm))
(SP: j sp = Some (sp',0))
(RO: ro_acc m0 m)
(INCR: inj_incr w (injw j (Mem.support m) (Mem.support tm))),
match_states (State s f (Vptr sp Ptrofs.zero) pc' e m)
(State ts tf (Vptr sp' Ptrofs.zero) pc' te tm).
Proof.
intros. exploit analyze_successors; eauto. rewrite ANPC; simpl. intros [A B].
econstructor; eauto.
eapply eagree_ge; eauto.
eapply magree_monotone; eauto.
Qed.
(** Builtin arguments and results *)
Lemma eagree_set_res:
forall j e1 e2 v1 v2 res ne,
Val.inject j v1 v2 ->
eagree j e1 e2 (kill_builtin_res res ne) ->
eagree j (regmap_setres res v1 e1) (regmap_setres res v2 e2) ne.
Proof.
intros. destruct res; simpl in *; auto.
apply eagree_update; eauto. apply vagree_inject; auto.
Qed.
Lemma transfer_builtin_arg_sound:
forall bc e e' sp m m' a v j sp',
eval_builtin_arg ge (fun r => e#r) (Vptr sp Ptrofs.zero) m a v ->
forall nv ne1 nm1 ne2 nm2,
transfer_builtin_arg nv (ne1, nm1) a = (ne2, nm2) ->
eagree j e e' ne2 ->
magree j m m' (nlive ge sp nm2) ->
Genv.match_stbls j se tse ->
genv_match bc ge ->
bc sp = BCstack ->
j sp = Some (sp',0) ->
exists v',
eval_builtin_arg tge (fun r => e'#r) (Vptr sp' Ptrofs.zero) m' a v'
/\ vagree j v v' nv
/\ eagree j e e' ne1
/\ magree j m m' (nlive ge sp nm1).
Proof.
induction 1; simpl; intros until nm2; intros TR EA MA MSTB GM SPM SPJ; inv TR.
- exists e'#x; intuition auto. constructor. eauto 2 with na. eauto 2 with na.
- exists (Vint n); intuition auto. constructor. apply vagree_inject. constructor.
- exists (Vlong n); intuition auto. constructor. apply vagree_inject. constructor.
- exists (Vfloat n); intuition auto. constructor. apply vagree_inject. constructor.
- exists (Vsingle n); intuition auto. constructor. apply vagree_inject. constructor.
- simpl in H. exploit magree_load; eauto.
intros. eapply nlive_add; eauto with va. rewrite Ptrofs.add_zero_l in H0; auto.
intros (v' & A & B). rewrite Z.add_0_r in A.
exists v'; intuition auto. constructor; auto. apply vagree_inject; auto.
eapply magree_monotone; eauto. intros; eapply incl_nmem_add; eauto.
- exists (Vptr sp' (Ptrofs.add Ptrofs.zero ofs)); intuition auto with na. constructor.
eapply vagree_inject. econstructor; eauto. rewrite Ptrofs.add_zero. reflexivity.
- unfold Genv.symbol_address in H; simpl in H.
destruct (Genv.find_symbol se id) as [b|] eqn:FS; simpl in H; try discriminate.
eapply Genv.find_symbol_match in FS as FS'; eauto. destruct FS' as [tb [MAP FS']].
exploit magree_load; eauto.
intros. eapply nlive_add; eauto. constructor. apply GM; auto.
intros (v' & A & B). rewrite Z.add_0_r in A.
exists v'; intuition auto.
constructor. simpl. unfold Genv.symbol_address. rewrite FS'; auto.
apply vagree_inject; auto.
eapply magree_monotone; eauto. intros; eapply incl_nmem_add; eauto.
- exists (Genv.symbol_address tse id ofs); intuition auto with na. constructor.
eapply vagree_inject. apply symbol_address_inject; eauto.
- destruct (transfer_builtin_arg All (ne1, nm1) hi) as [ne' nm'] eqn:TR.
exploit IHeval_builtin_arg2; eauto. intros (vlo' & A & B & C & D).
exploit IHeval_builtin_arg1; eauto. intros (vhi' & P & Q & R & S).
exists (Val.longofwords vhi' vlo'); intuition auto.
constructor; auto.
apply vagree_inject.
apply Val.longofwords_inject; apply inject_vagree; auto.
- destruct (transfer_builtin_arg All (ne1, nm1) a1) as [ne' nm'] eqn:TR.
exploit IHeval_builtin_arg2; eauto. intros (v2' & A & B & C & D).
exploit IHeval_builtin_arg1; eauto. intros (v1' & P & Q & R & S).
econstructor; intuition auto.
econstructor; eauto.
destruct Archi.ptr64; auto using Val.add_inject, Val.addl_inject, vagree_inject, inject_vagree.
Qed.
Lemma transfer_builtin_args_sound:
forall e sp m e' m' bc al vl j sp',
eval_builtin_args ge (fun r => e#r) (Vptr sp Ptrofs.zero) m al vl ->
forall ne1 nm1 ne2 nm2,
transfer_builtin_args (ne1, nm1) al = (ne2, nm2) ->
eagree j e e' ne2 ->
magree j m m' (nlive ge sp nm2) ->
Genv.match_stbls j se tse ->
genv_match bc ge ->
bc sp = BCstack ->
j sp = Some (sp',0) ->
exists vl',
eval_builtin_args tge (fun r => e'#r) (Vptr sp' Ptrofs.zero) m' al vl'
/\ Val.inject_list j vl vl'
/\ eagree j e e' ne1
/\ magree j m m' (nlive ge sp nm1).
Proof.
Local Opaque transfer_builtin_arg.
induction 1; simpl; intros.
- inv H. exists (@nil val); intuition auto. constructor.
- destruct (transfer_builtin_arg All (ne1, nm1) a1) as [ne' nm'] eqn:TR.
exploit IHlist_forall2; eauto. intros (vs' & A1 & B1 & C1 & D1).
exploit transfer_builtin_arg_sound; eauto. intros (v1' & A2 & B2 & C2 & D2).
exists (v1' :: vs'); intuition auto. constructor; auto.
Qed.
Lemma address_inject:
forall j m1 m2 b1 ofs1 b2 delta p P,
magree j m1 m2 P ->
Mem.perm m1 b1 (Ptrofs.unsigned ofs1) Cur p ->
j b1 = Some (b2, delta) ->
Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta)) = Ptrofs.unsigned ofs1 + delta.
Proof.
intros.
assert (Mem.perm m1 b1 (Ptrofs.unsigned ofs1) Max Nonempty) by eauto with mem.
exploit ma_representable; eauto. intros [A B].
assert (0 <= delta <= Ptrofs.max_unsigned).
generalize (Ptrofs.unsigned_range ofs1). lia.
unfold Ptrofs.add. repeat rewrite Ptrofs.unsigned_repr; lia.
Qed.
Lemma can_eval_builtin_arg:
forall j sp e m e' m' P sp',
magree j m m' P ->
j sp = Some (sp',0) ->
Genv.match_stbls j se tse ->
forall a v,
eval_builtin_arg ge (fun r => e#r) (Vptr sp Ptrofs.zero) m a v ->
exists v', eval_builtin_arg tge (fun r => e'#r) (Vptr sp' Ptrofs.zero) m' a v'.
Proof.
intros until sp'; intros MA JSP MSTB.
assert (LD: forall chunk addr v addr',
Mem.loadv chunk m addr = Some v ->
Val.inject j addr addr' ->
exists v', Mem.loadv chunk m' addr' = Some v').
{
intros. destruct addr; simpl in H; try discriminate. inv H0. simpl.
eapply Mem.valid_access_load. erewrite address_inject; eauto with mem.
eapply magree_valid_access; eauto.
eapply Mem.load_valid_access; eauto. }
induction 1; try (econstructor; now constructor).
- exploit LD; eauto. econstructor; eauto.
intros (v' & A). rewrite Ptrofs.add_zero in A. exists v'; constructor; auto.
- exploit LD; eauto. eapply symbol_address_inject; eauto.
intros (v' & A). exists v'; constructor; auto.
- destruct IHeval_builtin_arg1 as (v1' & A1).
destruct IHeval_builtin_arg2 as (v2' & A2).
exists (Val.longofwords v1' v2'); constructor; auto.
- destruct IHeval_builtin_arg1 as (v1' & A1).
destruct IHeval_builtin_arg2 as (v2' & A2).
econstructor; econstructor; eauto.
Qed.
Lemma can_eval_builtin_args:
forall sp e m e' m' P j sp',
magree j m m' P ->
j sp = Some (sp',0) ->
Genv.match_stbls j se tse ->
forall al vl,
eval_builtin_args ge (fun r => e#r) (Vptr sp Ptrofs.zero) m al vl ->
exists vl', eval_builtin_args tge (fun r => e'#r) (Vptr sp' Ptrofs.zero) m' al vl'.
Proof.
induction 4.
- exists (@nil val); constructor.
- exploit can_eval_builtin_arg; eauto. intros (v' & A).
destruct IHlist_forall2 as (vl' & B).
exists (v' :: vl'); constructor; eauto.
Qed.
(** Properties of volatile memory accesses *)
Lemma match_symbols_inject:
forall j, Genv.match_stbls j se tse -> symbols_inject j se tse.
Proof.
intros. inv H. constructor.
- eauto.
- repeat apply conj.
+ intros. exploit mge_dom; eauto. eapply Genv.genv_symb_range.
eauto. intros [x A]. rewrite H in A. inv A. split. reflexivity.
eapply mge_symb in H0; eauto.
+ intros. exploit mge_dom; eauto. eapply Genv.genv_symb_range; eauto.
intros [b2 A]. exists b2. split; eauto.
eapply mge_symb in H0; eauto.
+ intros. unfold Genv.block_is_volatile. erewrite mge_info; eauto.
Qed.
Lemma transf_volatile_store:
forall j v1 v2 v1' v2' m tm chunk sp nm t v m',
volatile_store_sem chunk ge (v1::v2::nil) m t v m' ->
Val.inject j v1 v1' ->
vagree j v2 v2' (store_argument chunk) ->
magree j m tm (nlive ge sp nm) ->
Genv.match_stbls j se tse ->
v = Vundef /\
exists tm', volatile_store_sem chunk tge (v1'::v2'::nil) tm t Vundef tm'
/\ magree j m' tm' (nlive ge sp nm).
Proof.
intros. inv H. split; auto.
inv H0. inv H10.
- (* volatile *)
exists tm; split; auto. econstructor.
eapply Genv.find_symbol_match in H0 as FS'; eauto. destruct FS' as [tb [MAP FS']].
rewrite H5 in MAP. inv MAP. rewrite Ptrofs.add_zero.
econstructor; eauto. unfold Genv.block_is_volatile in *.
inv H3. erewrite <- mge_info; eauto.
eapply eventval_match_inject; eauto.
eapply match_symbols_inject; eauto.
apply store_argument_load_result; auto.
- (* not volatile *)
exploit magree_store_parallel. eauto. eauto. eauto. eauto.
instantiate (1 := nlive ge sp nm). auto.
intros (tm' & P & Q).
exists tm'; split. econstructor. econstructor; eauto.
unfold Genv.block_is_volatile in *. inv H3. erewrite <- mge_info; eauto.
erewrite address_inject; eauto with mem. auto.
Qed.
Lemma eagree_set_undef:
forall j e1 e2 ne r, eagree j e1 e2 ne -> eagree j (e1#r <- Vundef) e2 ne.
Proof.
intros; red; intros. rewrite PMap.gsspec. destruct (peq r0 r); auto with na.
Qed.
Theorem disjoint_or_equal_inject:
forall f m b1 b1' delta1 b2 b2' delta2 ofs1 ofs2 sz,
Mem.meminj_no_overlap f m ->
f b1 = Some(b1', delta1) ->
f b2 = Some(b2', delta2) ->
Mem.range_perm m b1 ofs1 (ofs1 + sz) Max Nonempty ->
Mem.range_perm m b2 ofs2 (ofs2 + sz) Max Nonempty ->
sz > 0 ->
b1 <> b2 \/ ofs1 = ofs2 \/ ofs1 + sz <= ofs2 \/ ofs2 + sz <= ofs1 ->
b1' <> b2' \/ ofs1 + delta1 = ofs2 + delta2
\/ ofs1 + delta1 + sz <= ofs2 + delta2
\/ ofs2 + delta2 + sz <= ofs1 + delta1.
Proof.
intros.
destruct (eq_block b1 b2).
assert (b1' = b2') by congruence. assert (delta1 = delta2) by congruence. subst.
destruct H5. congruence. right. destruct H5. left; congruence. right. lia.
destruct (eq_block b1' b2'); auto. subst. right. right.
set (i1 := (ofs1 + delta1, ofs1 + delta1 + sz)).
set (i2 := (ofs2 + delta2, ofs2 + delta2 + sz)).
change (snd i1 <= fst i2 \/ snd i2 <= fst i1).
apply Intv.range_disjoint'; simpl; try lia.
unfold Intv.disjoint, Intv.In; simpl; intros. red; intros.
exploit H; eauto.
instantiate (1 := x - delta1). apply H2. lia.
instantiate (1 := x - delta2). apply H3. lia.
intuition.
Qed.
Lemma valid_access_inject:
forall f m1 m2 chunk b1 ofs b2 delta p x,
f b1 = Some(b2, delta) ->
magree f m1 m2 x ->
Mem.valid_access m1 chunk b1 ofs p ->
Mem.valid_access m2 chunk b2 (ofs + delta) p.
Proof.
intros. red. red in H1. destruct H1.
split. red. intros. replace (ofs0) with (ofs0 - delta + delta) by lia.
eapply ma_perm; eauto. eapply H1. lia.
apply Z.divide_add_r. eauto. eapply ma_align; eauto.
eapply Mem.range_perm_max; eauto.
Qed.
Theorem aligned_area_inject:
forall f m m' b ofs al sz b' delta x,
magree f m m' x ->
al = 1 \/ al = 2 \/ al = 4 \/ al = 8 -> sz > 0 ->
(al | sz) ->
Mem.range_perm m b ofs (ofs + sz) Cur Nonempty ->
(al | ofs) ->
f b = Some(b', delta) ->
(al | ofs + delta).
Proof.
intros.
assert (P: al > 0) by lia.
assert (Q: Z.abs al <= Z.abs sz). apply Zdivide_bounds; auto. lia.
rewrite Z.abs_eq in Q; try lia. rewrite Z.abs_eq in Q; try lia.
assert (R: exists chunk, al = align_chunk chunk /\ al = size_chunk chunk).
destruct H0. subst; exists Mint8unsigned; auto.
destruct H0. subst; exists Mint16unsigned; auto.
destruct H0. subst; exists Mint32; auto.
subst; exists Mint64; auto.
destruct R as [chunk [A B]].
assert (Mem.valid_access m chunk b ofs Nonempty).
split. red; intros; apply H3. lia. congruence.
exploit valid_access_inject; eauto. intros [C D].
congruence.
Qed.
(** * The simulation diagram *)
Theorem step_simulation:
forall S1 t S2, step ge S1 t S2 ->
forall S1', match_states S1 S1' -> sound_state prog se S1 ->
exists S2', step tge S1' t S2' /\ match_states S2 S2'.
Proof.
Ltac TransfInstr :=
match goal with
| [INSTR: (fn_code _)!_ = Some _,
FUN: transf_function _ _ = OK _,
ANL: analyze _ _ = Some _ |- _ ] =>
generalize (transf_function_at _ _ _ _ _ _ FUN ANL INSTR);
let TI := fresh "TI" in
intro TI; unfold transf_instr in TI
end.
Ltac UseTransfer :=
match goal with
| [INSTR: (fn_code _)!?pc = Some _,
ANL: analyze _ _ = Some ?an |- _ ] =>
destruct (an!!pc) as [ne nm] eqn:ANPC;
unfold transfer in *;
rewrite INSTR in *;
simpl in *
end.
induction 1; intros S1' MS SS; inv MS.
- (* nop *)
TransfInstr; UseTransfer.
econstructor; split.
eapply exec_Inop; eauto.
eapply match_succ_states; eauto. simpl; auto.
- (* op *)
TransfInstr; UseTransfer.
destruct (is_dead (nreg ne res)) eqn:DEAD;
[idtac|destruct (is_int_zero (nreg ne res)) eqn:INTZERO;
[idtac|destruct (operation_is_redundant op (nreg ne res)) eqn:REDUNDANT]].
+ (* dead instruction, turned into a nop *)
econstructor; split.
eapply exec_Inop; eauto.
eapply match_succ_states; eauto. simpl; auto.
apply eagree_update_dead; auto with na.
+ (* instruction with needs = [I Int.zero], turned into a load immediate of zero. *)
econstructor; split.
eapply exec_Iop with (v := Vint Int.zero); eauto.
eapply match_succ_states; eauto. simpl; auto.
apply eagree_update; auto.
rewrite is_int_zero_sound by auto.
destruct v; simpl; auto. apply iagree_zero.
+ (* redundant operation *)
destruct args.
* (* kept as is because no arguments -- should never happen *)
simpl in *. exploit inj_stbls_subrel; eauto. intro GE'. inv GE'.
exploit needs_of_operation_sound; eauto.
eapply symbol_address_inject; eauto.
intros. eapply ma_perm; eauto. eapply ma_representable; eauto. eapply ma_no_overlap; eauto.
eauto. instantiate (1 := nreg ne res). eauto with na. eauto with na. intros [tv [A B]].
econstructor; split.
eapply exec_Iop with (v := tv); eauto.
eapply match_succ_states; eauto. simpl; auto.
apply eagree_update; auto.
* (* turned into a move *)
unfold fst in ENV. unfold snd in MEM. simpl in H0.
assert (VA: vagree j v te#r (nreg ne res)).
{ eapply operation_is_redundant_sound with (arg1' := te#r) (args' := te##args).
eauto. eauto. exploit add_needs_vagree; eauto. }
econstructor; split.
eapply exec_Iop; eauto. simpl; reflexivity.
eapply match_succ_states; eauto. simpl; auto.
eapply eagree_update; eauto 2 with na.
+ (* preserved operation *)
simpl in *. exploit inj_stbls_subrel; eauto. intro GE'. inv GE'.
exploit needs_of_operation_sound; eauto.