-
Notifications
You must be signed in to change notification settings - Fork 1
/
AssnState.v
1565 lines (1481 loc) · 55.8 KB
/
AssnState.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 syntax.
Require Import alist.
Require Import FMapWeakList.
Require Import sflib.
Require Import Coqlib.
Require Import infrastructure.
Require Import Metatheory.
Require Import vellvm.
Require Import memory_props.
Import Opsem.
Require Import Exprs.
Require Import Hints.
Require Import GenericValues.
Require Import Inject.
Require AssnMem.
Require Import TODO.
Require Import paco.
Require Import TODOProof.
Require Import OpsemAux.
Set Implicit Arguments.
Inductive valid_conf
(m_src m_tgt:module)
(conf_src conf_tgt:Config): Prop :=
| valid_conf_intro
(INJECT: inject_conf conf_src conf_tgt)
.
Ltac solve_bool_true :=
repeat
(try match goal with
| [H: andb ?a ?b = true |- _] =>
apply andb_true_iff in H; des
| [H: orb ?a ?b = true |- _] =>
apply orb_true_iff in H; des
| [H: proj_sumbool (?dec ?a ?b) = true |- _] =>
destruct (dec a b)
end;
try subst; ss; unfold is_true in *; unfold sflib.is_true in *).
Lemma get_lhs_in_spec
ld (rhs: Expr.t) x
(LHS: ExprPairSet.In x (Assertion.get_lhs ld rhs)):
(snd x) = rhs /\ ExprPairSet.In x ld.
Proof.
unfold Assertion.get_lhs, flip in *.
rewrite ExprPairSetFacts.filter_iff in LHS; cycle 1.
{ solve_compat_bool. solve_leibniz. ss. }
des. des_sumbool. ss.
Qed.
Lemma get_rhs_in_spec
ld (lhs: Expr.t) x
(RHS: ExprPairSet.In x (Assertion.get_rhs ld lhs)):
(fst x) = lhs /\ ExprPairSet.In x ld.
Proof.
unfold Assertion.get_rhs, flip in *.
rewrite ExprPairSetFacts.filter_iff in RHS; cycle 1.
{ solve_compat_bool. solve_leibniz. ss. }
des. des_sumbool. ss.
Qed.
Lemma get_rhs_in_spec2
(ld: ExprPairSet.t) (lhs: Expr.t) (x: Expr.t * Expr.t)
(LHS: fst x = lhs)
(IN: ExprPairSet.In x ld)
: ExprPairSet.In x (Assertion.get_rhs ld lhs).
Proof.
i. des.
unfold Assertion.get_rhs, flip.
apply ExprPairSet.filter_3.
{ solve_compat_bool. solve_leibniz. ss. }
- subst.
unfold proj_sumbool.
des_ifs.
- subst.
unfold proj_sumbool.
des_ifs.
Qed.
Module Unary.
Structure t := mk {
previous: GVsMap;
ghost: GVsMap;
}.
Definition update_previous f x :=
(mk (f x.(previous)) x.(ghost)).
Definition update_ghost f x :=
(mk x.(previous) (f x.(ghost))).
Definition update_both f x :=
update_ghost f (update_previous f x).
Definition clear_idt (idt0: IdT.t) (invst: t): t :=
match idt0 with
| (Tag.physical, id0) => invst
| (Tag.previous, id0) => (mk (filter_AL_atom (fun x => negb (id_dec id0 x)) invst.(previous))
invst.(ghost))
| (Tag.ghost, id0) => (mk (invst.(previous))
(filter_AL_atom (fun x => negb (id_dec id0 x)) invst.(ghost)))
end
.
Definition sem_tag (st:State) (invst:t) (tag:Tag.t): GVsMap :=
match tag with
| Tag.physical => st.(EC).(Locals)
| Tag.previous => invst.(previous)
| Tag.ghost => invst.(ghost)
end.
Definition sem_idT (st:State) (invst:t) (id:IdT.t): option GenericValue :=
lookupAL _ (sem_tag st invst id.(fst)) id.(snd).
Definition sem_valueT (conf:Config) (st:State) (invst:t) (v:ValueT.t): option GenericValue :=
match v with
| ValueT.id id => sem_idT st invst id
| ValueT.const c => const2GV conf.(CurTargetData) conf.(Globals) c
end.
Fixpoint sem_list_valueT (conf:Config) (st:State) (invst:t) (lv:list (sz * ValueT.t)): option (list GenericValue) :=
match lv with
| nil => Some nil
| (_, v) :: lv' =>
match sem_valueT conf st invst v, sem_list_valueT conf st invst lv' with
| Some GV, Some GVs => Some (GV::GVs)
| _, _ => None
end
end.
Definition sem_expr (conf:Config) (st:State) (invst:t) (e:Expr.t): option GenericValue :=
match e with
| Expr.bop op bsz v1 v2 =>
match sem_valueT conf st invst v1,
sem_valueT conf st invst v2 with
| Some gv1, Some gv2 =>
mbop conf.(CurTargetData) op bsz gv1 gv2
| _, _ => None
end
| Expr.fbop op fp v1 v2 =>
match sem_valueT conf st invst v1,
sem_valueT conf st invst v2 with
| Some gv1, Some gv2 =>
mfbop conf.(CurTargetData) op fp gv1 gv2
| _, _ => None
end
| Expr.extractvalue ty1 v1 lc ty2 =>
match sem_valueT conf st invst v1 with
| Some gv1 =>
extractGenericValue conf.(CurTargetData) ty1 gv1 lc
| None => None
end
| Expr.insertvalue ty1 v1 ty2 v2 lc =>
match sem_valueT conf st invst v1,
sem_valueT conf st invst v2 with
| Some gv1, Some gv2 =>
insertGenericValue conf.(CurTargetData) ty1 gv1 lc ty2 gv2
| _, _ => None
end
| Expr.gep inb ty1 v1 lsv ty2 =>
match sem_valueT conf st invst v1, sem_list_valueT conf st invst lsv with
| Some gv1, Some glsv =>
gep conf.(CurTargetData) ty1 glsv inb ty2 gv1
| _, _ => None
end
| Expr.trunc op ty1 v ty2 =>
match sem_valueT conf st invst v with
| Some gv =>
mtrunc conf.(CurTargetData) op ty1 ty2 gv
| _ => None
end
| Expr.ext eop ty1 v ty2 =>
match sem_valueT conf st invst v with
| Some gv =>
mext conf.(CurTargetData) eop ty1 ty2 gv
| None => None
end
| Expr.cast cop ty1 v ty2 =>
match sem_valueT conf st invst v with
| Some gv => mcast conf.(CurTargetData) cop ty1 ty2 gv
| None => None
end
| Expr.icmp c ty v1 v2 =>
match sem_valueT conf st invst v1,
sem_valueT conf st invst v2 with
| Some gv1, Some gv2 =>
micmp conf.(CurTargetData) c ty gv1 gv2
| _, _ => None
end
| Expr.fcmp fc fp v1 v2 =>
match sem_valueT conf st invst v1,
sem_valueT conf st invst v2 with
| Some gv1, Some gv2 =>
mfcmp conf.(CurTargetData) fc fp gv1 gv2
| _, _ => None
end
| Expr.select v0 ty v1 v2 =>
match sem_valueT conf st invst v0,
sem_valueT conf st invst v1,
sem_valueT conf st invst v2 with
| Some gv0, Some gv1, Some gv2 =>
mselect conf.(CurTargetData) ty gv0 gv1 gv2
| _, _, _ => None
end
| Expr.value v =>
sem_valueT conf st invst v
| Expr.load v ty a =>
match sem_valueT conf st invst v with
| Some gvp =>
mload conf.(CurTargetData) st.(Mem) gvp ty a
| None => None
end
end.
Definition sem_lessdef (conf:Config) (st:State) (invst:t) (es:ExprPair.t): Prop :=
forall val1 (VAL1: sem_expr conf st invst es.(fst) = Some val1),
exists val2,
<<VAL2: sem_expr conf st invst es.(snd) = Some val2>> /\
<<VAL: GVs.lessdef val1 val2>>.
Lemma sem_lessdef_trans
conf st invst e0 e1 e2
(LD01: Unary.sem_lessdef conf st invst (e0, e1))
(LD12: Unary.sem_lessdef conf st invst (e1, e2))
:
<<LD12: Unary.sem_lessdef conf st invst (e0, e2)>>
.
Proof.
ii. expl LD01. expl LD12. ss. esplits; eauto.
eapply GVs.lessdef_trans; eauto.
Qed.
Definition sem_diffblock (conf:Config) (val1 val2:GenericValue): Prop :=
list_disjoint (GV2blocks val1) (GV2blocks val2).
Definition sem_noalias (conf:Config) (val1 val2:GenericValue) (ty1 ty2:typ): Prop :=
list_disjoint (GV2blocks val1) (GV2blocks val2).
Lemma diffblock_comm
conf gv1 gv2
(DIFFBLOCK: sem_diffblock conf gv1 gv2)
: sem_diffblock conf gv2 gv1.
Proof.
eapply list_disjoint_comm; eauto.
Qed.
Lemma undef_diffblock
conf (gv1: GenericValue) gv2
(* (UNDEF: List.Forall (fun x => x.(fst) = Vundef) gv1) *)
(UNDEF: forall v mc, In (v, mc) gv1 -> v = Vundef)
:
<<DIFFBLOCK: sem_diffblock conf gv1 gv2>>.
Proof.
induction gv2; ii; des; ss.
cut(GV2blocks gv1 = []).
{ clarify. ii. rewrite H1 in *. ss. }
clear - UNDEF.
induction gv1; ii; ss.
destruct a; ss.
exploit UNDEF; eauto; []; ii; des.
subst.
exploit IHgv1; eauto.
Qed.
Lemma noalias_comm
conf gv1 gv2 ty1 ty2
(NOALIAS: sem_noalias conf gv1 gv2 ty1 ty2)
: sem_noalias conf gv2 gv1 ty2 ty1.
Proof.
eapply list_disjoint_comm; eauto.
Qed.
Inductive sem_alias (conf:Config) (st:State) (invst:t) (arel:Assertion.aliasrel): Prop :=
| sem_alias_intro
(DIFFBLOCK:
forall val1 gval1
val2 gval2
(MEM: ValueTPairSet.mem (val1, val2) arel.(Assertion.diffblock))
(VAL1: sem_valueT conf st invst val1 = Some gval1)
(VAL2: sem_valueT conf st invst val2 = Some gval2),
sem_diffblock conf gval1 gval2)
(NOALIAS:
forall ptr1 gptr1
ptr2 gptr2
(MEM: PtrPairSet.mem (ptr1, ptr2) arel.(Assertion.noalias))
(VAL1: sem_valueT conf st invst ptr1.(fst) = Some gptr1)
(VAL2: sem_valueT conf st invst ptr2.(fst) = Some gptr2),
sem_noalias conf gptr1 gptr2 ptr1.(snd) ptr2.(snd))
.
Inductive sem_unique (conf:Config) (st:State) (gmax:positive) (a:atom) : Prop :=
| sem_unique_intro
val
(VAL: lookupAL _ st.(EC).(Locals) a = Some val)
(LOCALS: forall reg val'
(REG: a <> reg)
(VAL': lookupAL _ st.(EC).(Locals) reg = Some val'),
sem_diffblock conf val val')
(MEM:
forall mptr typ align val'
(LOAD: mload conf.(CurTargetData) st.(Mem) mptr typ align = Some val'),
sem_diffblock conf val val')
(GLOBALS:
forall b
(GV2BLOCKS: In b (GV2blocks val)),
(gmax < b)%positive)
.
Definition sem_private (conf:Config) (st:State) (invst:t)
(private_parent:list mblock) (public:mblock -> Prop) (a:IdT.t): Prop :=
forall b val
(VAL: sem_idT st invst a = Some val)
(IN: In b (GV2blocks val)),
<<PRIVATE_BLOCK: AssnMem.private_block st.(Mem) public b>> /\
<<PARENT_DISJOINT: ~ In b private_parent>>
.
(* In b private. *)
(* match GV2ptr conf.(CurTargetData) (getPointerSize conf.(CurTargetData)) val with *)
(* | ret Vptr b _ => In b private *)
(* | _ => False *)
(* end. *)
Inductive sem (conf:Config) (st:State) (invst:t) (assnmem:AssnMem.Unary.t) (gmax:positive) (public:mblock -> Prop) (inv:Assertion.unary): Prop :=
| sem_intro
(LESSDEF: ExprPairSet.For_all (sem_lessdef conf st invst) inv.(Assertion.lessdef))
(NOALIAS: sem_alias conf st invst inv.(Assertion.alias))
(UNIQUE: AtomSetImpl.For_all (sem_unique conf st gmax) inv.(Assertion.unique))
(PRIVATE: IdTSet.For_all (sem_private conf st invst assnmem.(AssnMem.Unary.private_parent) public) inv.(Assertion.private))
(ALLOCAS_PARENT: list_disjoint st.(EC).(Allocas) assnmem.(AssnMem.Unary.private_parent))
(ALLOCAS_VALID: List.Forall (Mem.valid_block st.(Mem)) st.(EC).(Allocas))
(WF_LOCAL: MemProps.wf_lc st.(Mem) st.(EC).(Locals))
(WF_PREVIOUS: MemProps.wf_lc st.(Mem) invst.(previous))
(WF_GHOST: MemProps.wf_lc st.(Mem) invst.(ghost))
(UNIQUE_PARENT_LOCAL:
forall x ptr
(PTR:lookupAL _ st.(EC).(Locals) x = Some ptr),
AssnMem.gv_diffblock_with_blocks conf ptr assnmem.(AssnMem.Unary.unique_parent))
(WF_FDEF: wf_fdef conf.(CurSystem) conf st.(EC).(CurFunction))
(WF_EC: wf_EC st.(EC))
.
Lemma sem_valueT_physical
conf st inv val:
sem_valueT conf st inv (Exprs.ValueT.lift Exprs.Tag.physical val) =
getOperandValue conf.(CurTargetData) val st.(EC).(Locals) conf.(Globals).
Proof. destruct val; ss. Qed.
End Unary.
Module Rel.
Structure t := mk {
src: Unary.t;
tgt: Unary.t;
}.
Definition update_src f x :=
(mk (f x.(src)) x.(tgt)).
Definition update_tgt f x :=
(mk x.(src) (f x.(tgt))).
Definition update_both f x :=
update_src f (update_tgt f x).
Definition clear_idt (idt0: IdT.t) (invst: t): t :=
mk (Unary.clear_idt idt0 invst.(src)) (Unary.clear_idt idt0 invst.(tgt))
.
Definition sem_inject (st_src st_tgt:State) (invst:t) (inject:meminj) (id:IdT.t): Prop :=
forall val_src (VAL_SRC: Unary.sem_idT st_src invst.(src) id = Some val_src),
exists val_tgt,
<<VAL_TGT: Unary.sem_idT st_tgt invst.(tgt) id = Some val_tgt>> /\
<<VAL: genericvalues_inject.gv_inject inject val_src val_tgt>>
.
Inductive inject_allocas (f: meminj): list mblock -> list mblock -> Prop :=
| inject_allocas_nil: inject_allocas f [] []
| inject_allocas_alloca_nop
al
(PRIVATE: f al = None)
als_src als_tgt
(INJECT: inject_allocas f als_src als_tgt)
:
inject_allocas f (al :: als_src) als_tgt
| inject_allocas_nop_alloca
al
(PRIVATE: forall b ofs, f b <> Some (al, ofs))
als_src als_tgt
(INJECT: inject_allocas f als_src als_tgt)
:
inject_allocas f als_src (al :: als_tgt)
| inject_allocas_alloca_alloca
al_src al_tgt
(PUBLIC: f al_src = Some (al_tgt, 0))
als_src als_tgt
(INJECT: inject_allocas f als_src als_tgt)
:
inject_allocas f (al_src :: als_src) (al_tgt :: als_tgt)
.
Definition sem_inject_expr (conf_src conf_tgt: Config)
(st_src st_tgt:State) (invst:t) (inject:meminj) (expr:Expr.t): Prop :=
forall val_src (VAL_SRC: Unary.sem_expr conf_src st_src invst.(src) expr = Some val_src),
exists val_tgt,
<<VAL_TGT: Unary.sem_expr conf_tgt st_tgt invst.(tgt) expr = Some val_tgt>> /\
<<VAL: genericvalues_inject.gv_inject inject val_src val_tgt>>.
Inductive sem (conf_src conf_tgt:Config) (st_src st_tgt:State) (invst:t) (assnmem:AssnMem.Rel.t) (inv:Assertion.t): Prop :=
| sem_intro
(SRC: Unary.sem conf_src st_src invst.(src) assnmem.(AssnMem.Rel.src) assnmem.(AssnMem.Rel.gmax) (AssnMem.Rel.public_src assnmem.(AssnMem.Rel.inject)) inv.(Assertion.src))
(TGT: Unary.sem conf_tgt st_tgt invst.(tgt) assnmem.(AssnMem.Rel.tgt) assnmem.(AssnMem.Rel.gmax) (AssnMem.Rel.public_tgt assnmem.(AssnMem.Rel.inject)) inv.(Assertion.tgt))
(TGT_NOUNIQ: AtomSetImpl.Empty (inv.(Assertion.tgt).(Assertion.unique)))
(MAYDIFF:
forall id (NOTIN: (IdTSet.mem id inv.(Assertion.maydiff)) = false),
sem_inject st_src st_tgt invst assnmem.(AssnMem.Rel.inject) id)
(ALLOCAS:
inject_allocas assnmem.(AssnMem.Rel.inject) st_src.(EC).(Allocas) st_tgt.(EC).(Allocas))
.
Lemma inject_allocas_preserved_aux
assnmem0
als_src als_tgt
(INJECT: inject_allocas assnmem0.(AssnMem.Rel.inject) als_src als_tgt)
assnmem1
(INJECT_INCR: inject_incr assnmem0.(AssnMem.Rel.inject) assnmem1.(AssnMem.Rel.inject))
bd_src bd_tgt
(FROZEN: AssnMem.Rel.frozen assnmem0.(AssnMem.Rel.inject) assnmem1.(AssnMem.Rel.inject)
bd_src bd_tgt)
(VALID_SRC: List.Forall (fun x => (x < bd_src)%positive) als_src)
(VALID_TGT: List.Forall (fun x => (x < bd_tgt)%positive) als_tgt)
:
<<INJECT: inject_allocas assnmem1.(AssnMem.Rel.inject) als_src als_tgt>>
.
Proof.
ginduction INJECT; ii; ss.
- econs; eauto.
- inv VALID_SRC.
econs; eauto.
+ erewrite <- AssnMem.Rel.frozen_preserves_src; eauto.
+ eapply IHINJECT; eauto.
- inv VALID_TGT.
econs; eauto.
+ ii.
exploit AssnMem.Rel.frozen_preserves_tgt; eauto; []; i; des.
exploit PRIVATE; eauto.
+ eapply IHINJECT; eauto.
- inv VALID_SRC. inv VALID_TGT.
econs 4; eauto.
+ eapply IHINJECT; eauto.
Qed.
Lemma inject_allocas_preserved_le
assnmem0
als_src als_tgt
(INJECT: inject_allocas assnmem0.(AssnMem.Rel.inject) als_src als_tgt)
assnmem1
(LE: AssnMem.Rel.le assnmem0 assnmem1)
(VALID_SRC: List.Forall
(Mem.valid_block assnmem0.(AssnMem.Rel.src).(AssnMem.Unary.mem_parent)) als_src)
(VALID_TGT: List.Forall
(Mem.valid_block assnmem0.(AssnMem.Rel.tgt).(AssnMem.Unary.mem_parent)) als_tgt)
:
<<INJECT: inject_allocas assnmem1.(AssnMem.Rel.inject) als_src als_tgt>>
.
Proof.
eapply inject_allocas_preserved_aux; try exact INJECT; try eassumption.
{ apply LE. }
{ apply LE. }
Qed.
Lemma inject_allocas_preserved_le_lift
m_src0 m_tgt0 assnmem0
als_src als_tgt
(INJECT: inject_allocas assnmem0.(AssnMem.Rel.inject) als_src als_tgt)
assnmem1
arg0 arg1 arg2 arg3
(LE: AssnMem.Rel.le (AssnMem.Rel.lift m_src0 m_tgt0 arg0 arg1 arg2 arg3 assnmem0) assnmem1)
(VALID_SRC: List.Forall (Mem.valid_block m_src0) als_src)
(VALID_TGT: List.Forall (Mem.valid_block m_tgt0) als_tgt)
(PARENT_LE_SRC: ((Mem.nextblock (AssnMem.Unary.mem_parent (AssnMem.Rel.src assnmem0)) <=
Mem.nextblock (AssnMem.Unary.mem_parent (AssnMem.Rel.src assnmem1))))%positive)
(PARENT_LE_TGT: ((Mem.nextblock (AssnMem.Unary.mem_parent (AssnMem.Rel.tgt assnmem0)) <=
Mem.nextblock (AssnMem.Unary.mem_parent (AssnMem.Rel.tgt assnmem1))))%positive)
:
<<INJECT: inject_allocas assnmem1.(AssnMem.Rel.inject) als_src als_tgt>>
.
Proof.
eapply inject_allocas_preserved_aux; try exact INJECT; try eassumption.
{ apply LE. }
{ inv LE; ss. }
Qed.
Lemma const2GV_gv_inject_refl
TD globals cnst gv meminj
(CONST: const2GV TD globals cnst = ret gv)
gmax mem_src mem_tgt
(WASABI: genericvalues_inject.wf_sb_mi gmax meminj mem_src mem_tgt)
(WF_GLOBALS: genericvalues_inject.wf_globals gmax globals)
:
<<REFL: genericvalues_inject.gv_inject meminj gv gv>>.
Proof.
eapply const2GV_inject; eauto.
Qed.
Lemma not_in_maydiff_value_spec
inv assnmem invst
m_src conf_src st_src
m_tgt conf_tgt st_tgt
val gv_val_src
(CONF: valid_conf m_src m_tgt conf_src conf_tgt)
(NIMD: Assertion.not_in_maydiff inv val = true)
(MAYDIFF: forall id : Tag.t * id,
IdTSet.mem id (Assertion.maydiff inv) = false ->
sem_inject st_src st_tgt invst (AssnMem.Rel.inject assnmem) id)
(VAL_SRC: Unary.sem_valueT conf_src st_src (src invst) val = ret gv_val_src)
(MEM: AssnMem.Rel.sem conf_src conf_tgt st_src.(Mem) st_tgt.(Mem) assnmem)
:
exists gv_val_tgt, Unary.sem_valueT conf_tgt st_tgt (tgt invst) val = ret gv_val_tgt /\
genericvalues_inject.gv_inject (AssnMem.Rel.inject assnmem) gv_val_src gv_val_tgt.
Proof.
inv CONF. inv INJECT.
destruct val; repeat (ss; des_bool; des).
- exploit MAYDIFF; eauto.
- esplits.
+ rewrite <- TARGETDATA, <- GLOBALS. eauto.
+ eapply const2GV_gv_inject_refl; eauto.
apply MEM.
apply MEM.
Qed.
Lemma not_in_maydiff_list_value_spec
inv assnmem invst
m_src conf_src st_src
m_tgt conf_tgt st_tgt
vals gv_vals_src
(CONF: valid_conf m_src m_tgt conf_src conf_tgt)
(NIMD: forallb (Assertion.not_in_maydiff inv) (List.map snd vals) = true)
(MAYDIFF: forall id : Tag.t * id,
IdTSet.mem id (Assertion.maydiff inv) = false ->
sem_inject st_src st_tgt invst (AssnMem.Rel.inject assnmem) id)
(VAL_SRC: Unary.sem_list_valueT conf_src st_src (src invst) vals = ret gv_vals_src)
(MEM: AssnMem.Rel.sem conf_src conf_tgt st_src.(Mem) st_tgt.(Mem) assnmem)
:
exists gv_vals_tgt,
Unary.sem_list_valueT conf_tgt st_tgt (tgt invst) vals = ret gv_vals_tgt /\
list_forall2 (genericvalues_inject.gv_inject assnmem.(AssnMem.Rel.inject)) gv_vals_src gv_vals_tgt.
Proof.
revert gv_vals_src VAL_SRC.
induction vals; ss; i; inv VAL_SRC.
- esplits; eauto. econs.
- destruct a. simtac.
exploit not_in_maydiff_value_spec; eauto. i. des.
exploit IHvals; eauto. i. des.
rewrite H0, H3. esplits; eauto. econs; eauto.
Qed.
(* company-coq extracted *)
(* C-c C-a C-x *)
Lemma not_in_maydiff_load:
forall (inv : Assertion.t) (assnmem : AssnMem.Rel.t) (invst : t)
(m_src : module) (conf_src : Config) (st_src : State)
(m_tgt : module) (conf_tgt : Config) (st_tgt : State)
(v : ValueT.t) (t0 : typ) (a : align) (gv_expr_src : GenericValue),
valid_conf m_src m_tgt conf_src conf_tgt ->
Assertion.not_in_maydiff inv v = true ->
(forall id : Tag.t * id,
IdTSet.mem id (Assertion.maydiff inv) = false ->
sem_inject st_src st_tgt invst (AssnMem.Rel.inject assnmem) id) ->
forall g0 : GenericValue,
Unary.sem_valueT conf_src st_src (src invst) v = ret g0 ->
mload (CurTargetData conf_tgt) (Mem st_src) g0 t0 a = ret gv_expr_src ->
AssnMem.Rel.sem conf_src conf_tgt (Mem st_src) (Mem st_tgt) assnmem ->
CurTargetData conf_src = CurTargetData conf_tgt ->
Globals conf_src = Globals conf_tgt ->
forall g : GenericValue,
Unary.sem_valueT conf_tgt st_tgt (tgt invst) v = ret g ->
genericvalues_inject.gv_inject (AssnMem.Rel.inject assnmem) g0 g ->
exists gv_expr_tgt : GenericValue,
mload (CurTargetData conf_tgt) (Mem st_tgt) g t0 a = ret gv_expr_tgt /\
genericvalues_inject.gv_inject (AssnMem.Rel.inject assnmem) gv_expr_src
gv_expr_tgt.
Proof.
intros inv assnmem invst m_src conf_src st_src m_tgt conf_tgt st_tgt v t0 a
gv_expr_src CONF NIMD MAYDIFF g0 Heq0 VAL_SRC MEM
TARGETDATA GLOBALS g H H0.
eapply mload_inv in VAL_SRC; eauto; []; ii; des.
clarify.
inv MEM. clear SRC TGT.
rename b into __b__.
inv H0. inv H6.
destruct assnmem. cbn in *.
inv H5. cbn in *.
exploit genericvalues_inject.simulation_mload_aux;
try apply VAL_SRC; eauto; []; ii; des; eauto.
esplits; eauto.
clear CHUNK.
des_ifs. rewrite <- H0.
(* not to spill inv contents outside of assertion proof *)
replace delta with 0 in *; cycle 1.
{
(* really weird *)
inv WF.
exploit mi_range_block; eauto.
}
replace (Int.signed 31 (Int.add 31 ofs (Int.repr 31 0)))
with (Int.signed 31 ofs + 0); ss.
clear - ofs.
rewrite Z.add_comm. ss.
apply int_add_0.
Qed.
Lemma inject_expr_load
(m_src : module)
(conf_src : Config)
(st_src : State)
(v : ValueT.t)
(m_tgt : module)
(conf_tgt : Config)
(st_tgt : State)
(v0 : ValueT.t)
(t1 : typ)
(a0 : align)
(invst : t)
(assnmem : AssnMem.Rel.t)
(inv : Assertion.t)
(gval_src : GenericValue)
(STATE : sem conf_src conf_tgt st_src st_tgt invst assnmem inv)
(MEM : AssnMem.Rel.sem conf_src conf_tgt (Mem st_src) (Mem st_tgt) assnmem)
(INJECT0 : Assertion.inject_value inv v v0 = true)
(g0 : GenericValue)
(Heq0 : Unary.sem_valueT conf_src st_src (src invst) v = ret g0)
(CONF_DUP : valid_conf m_src m_tgt conf_src conf_tgt)
(TARGETDATA : CurTargetData conf_src = CurTargetData conf_tgt)
(GLOBALS : Globals conf_src = Globals conf_tgt)
(EQB_SPEC : forall c1 c2 : const, Decs.const_eqb c1 c2 -> c1 = c2)
(g : GenericValue)
(VAL_SRC : mload (CurTargetData conf_src) (Mem st_src) g0 t1 a0 = ret gval_src)
(VAL_TGT : Unary.sem_valueT conf_tgt st_tgt (tgt invst) v0 = ret g)
(INJECT : genericvalues_inject.gv_inject (AssnMem.Rel.inject assnmem) g0 g)
:
exists gval_tgt : GenericValue,
(<<VAL_TGT: mload (CurTargetData conf_src) (Mem st_tgt) g t1 a0 = ret gval_tgt >>) /\
(<<INJECT: genericvalues_inject.gv_inject (AssnMem.Rel.inject assnmem)
gval_src gval_tgt >>)
.
Proof.
eapply mload_inv in VAL_SRC; eauto; []; ii; des.
clarify.
inv MEM. clear SRC TGT.
rename b into __b__.
inv INJECT. inv H4.
destruct assnmem. cbn in *.
inv H3. cbn in *.
exploit genericvalues_inject.simulation_mload_aux;
try apply VAL_SRC; eauto; []; ii; des; eauto.
esplits; eauto.
clear CHUNK.
des_ifs. rewrite <- H.
(* not to spill inv contents outside of assertion proof *)
replace delta with 0 in *; cycle 1.
{
(* really weird *)
inv WF.
exploit mi_range_block; eauto.
}
replace (Int.signed 31 (Int.add 31 ofs (Int.repr 31 0)))
with (Int.signed 31 ofs + 0); ss.
clear - ofs.
rewrite Z.add_comm. ss.
apply int_add_0.
Qed.
(* TODO move lemma position to definition point *)
Lemma forall_gv_inject_gvs_inject
assnmem l0 l1
(INJECT: list_forall2
(genericvalues_inject.gv_inject
(AssnMem.Rel.inject assnmem)) l0 l1)
:
<<INJECTS: genericvalues_inject.gvs_inject
(AssnMem.Rel.inject assnmem) l0 l1>>
.
Proof.
generalize dependent l1.
induction l0; ii; ss; des; ss.
- inv INJECT. ss.
- destruct l1; ss.
{ inv INJECT. }
inv INJECT.
exploit IHl0; eauto.
Qed.
Lemma not_in_maydiff_expr_spec
inv assnmem invst
m_src conf_src st_src
m_tgt conf_tgt st_tgt
expr gv_expr_src
(CONF: valid_conf m_src m_tgt conf_src conf_tgt)
(NIMD: Assertion.not_in_maydiff_expr inv expr = true)
(MAYDIFF: forall id : Tag.t * id,
IdTSet.mem id (Assertion.maydiff inv) = false ->
sem_inject st_src st_tgt invst (AssnMem.Rel.inject assnmem) id)
(VAL_SRC: Unary.sem_expr conf_src st_src (src invst) expr
= ret gv_expr_src)
(MEM: AssnMem.Rel.sem conf_src conf_tgt st_src.(Mem) st_tgt.(Mem) assnmem)
:
exists gv_expr_tgt,
(Unary.sem_expr conf_tgt st_tgt (tgt invst) expr = ret gv_expr_tgt)
/\ (genericvalues_inject.gv_inject
(AssnMem.Rel.inject assnmem) gv_expr_src gv_expr_tgt)
.
Proof.
inversion CONF. inv INJECT.
unfold Assertion.not_in_maydiff_expr in *.
Ltac exploit_not_in_maydiff_value_spec_with x :=
match (type of x) with
| (Unary.sem_valueT _ _ _ _ = Some _) =>
(exploit not_in_maydiff_value_spec; [| | | exact x | |]; eauto; ii; des; [])
end.
Ltac exploit_not_in_maydiff_list_value_spec_with x :=
match (type of x) with
| (Unary.sem_list_valueT _ _ _ _ = Some _) =>
(exploit not_in_maydiff_list_value_spec; [| | | exact x | |]; eauto; ii; des; [])
end.
Ltac exploit_GV2int :=
let tmp := fresh in
match goal with
| [ H1: GV2int ?conf_x _ ?x = _,
H2: GV2int ?conf_y _ ?y = _,
TRGTDATA: ?conf_x = ?conf_y,
INJ: genericvalues_inject.gv_inject _ ?x ?y |- _ ] =>
exploit genericvalues_inject.simulation__GV2int; try eapply INJ; eauto; []; intro tmp; des;
rewrite TRGTDATA in tmp; rewrite H2 in tmp; clarify
end.
Time destruct expr; ss; repeat (des_bool; des);
des_ifs; (all_once exploit_not_in_maydiff_value_spec_with); clarify;
(all_once exploit_not_in_maydiff_list_value_spec_with); clarify;
try rewrite TARGETDATA in VAL_SRC;
try exploit_GV2int.
(* Finished transaction in 39.843 secs (39.67u,0.194s) (successful) *)
- exploit genericvalues_inject.simulation__mbop; try apply VAL_SRC; eauto; ii; des; eauto.
- exploit genericvalues_inject.simulation__mfbop; try apply VAL_SRC; eauto; ii; des; eauto.
- exploit genericvalues_inject.simulation__extractGenericValue; try apply VAL_SRC; eauto; ii; des; eauto.
- exploit genericvalues_inject.simulation__insertGenericValue; try apply VAL_SRC; eauto; ii; des; eauto.
- inv MEM.
exploit genericvalues_inject.simulation__GEP; try apply VAL_SRC; eauto; ii; des; eauto.
apply forall_gv_inject_gvs_inject; ss.
(* exploit genericvalues_inject.simulation__mgep; try apply VAL_SRC; eauto; ii; des; eauto. *)
- exploit genericvalues_inject.simulation__mtrunc; try apply VAL_SRC; eauto; ii; des; eauto.
- exploit genericvalues_inject.simulation__mext; try apply VAL_SRC; eauto; ii; des; eauto.
- exploit genericvalues_inject.simulation__mcast; try apply VAL_SRC; eauto; ii; des; eauto.
- exploit genericvalues_inject.simulation__micmp; try apply VAL_SRC; eauto; ii; des; eauto.
- exploit genericvalues_inject.simulation__mfcmp; try apply VAL_SRC; eauto; ii; des; eauto.
- exploit genericvalues_inject.simulation__mselect; try apply VAL_SRC; eauto; ii; des; eauto.
- eapply not_in_maydiff_value_spec; eauto.
- eapply not_in_maydiff_load; eauto.
Qed.
Lemma lessdef_expr_spec
invst assnmem inv
conf st gmax public
e1 e2 gv1
(SEM: Unary.sem conf st invst assnmem gmax public inv)
(E: ExprPairSet.mem (e1, e2) inv.(Assertion.lessdef))
(E1: Unary.sem_expr conf st invst e1 = ret gv1):
exists gv2,
<<E2: Unary.sem_expr conf st invst e2 = ret gv2>> /\
<<GV: GVs.lessdef gv1 gv2>>.
Proof.
inv SEM. exploit LESSDEF.
- apply ExprPairSetFacts.mem_iff. eauto.
- eauto.
- eauto.
Qed.
Lemma lessdef_list_value_spec
conf st invst assnmem gmax public inv
(STATE: Unary.sem conf st invst assnmem gmax public inv)
lsv0 lsv1
(LD_EXPR0: List.map fst lsv0 = List.map fst lsv1)
(LD_EXPR1: list_forallb2
(fun v1 v2 => ExprPairSet.mem
(Expr.value v1, Expr.value v2) (Assertion.lessdef inv))
(List.map snd lsv0) (List.map snd lsv1) = true)
l0
(SEM: Unary.sem_list_valueT conf st invst lsv0 = ret l0)
:
exists l1,
<<SEM: Unary.sem_list_valueT conf st invst lsv1 = ret l1>> /\
<<GV: List.Forall2 GVs.lessdef l0 l1>>
.
Proof.
ginduction lsv0; ii; ss; des_ifs_safe; clarify.
{ destruct lsv1; ss.
esplits; eauto. }
ss. destruct lsv1; ss.
clarify. ss.
des_ifs_safe. ss.
des_bool. des.
exploit lessdef_expr_spec; eauto. i; des. ss.
des_ifs_safe.
exploit IHlsv0; eauto. i; des.
des_ifs_safe.
esplits; eauto.
Qed.
Lemma lessdef_list_value_spec'
conf st invst
lsv0 lsv1
(LD_EXPR0: List.map fst lsv0 = List.map fst lsv1)
(LD_EXPR1: Forall2
(fun v1 v2 : ValueT.t =>
Unary.sem_lessdef conf st invst
(Expr.value v1, Expr.value v2)) (List.map snd lsv0)
(List.map snd lsv1))
l0
(SEM: Unary.sem_list_valueT conf st invst lsv0 = ret l0)
:
exists l1,
<<SEM: Unary.sem_list_valueT conf st invst lsv1 = ret l1>> /\
<<GV: List.Forall2 GVs.lessdef l0 l1>>
.
Proof.
ginduction lsv0; ii; ss; des_ifs_safe; clarify.
{ destruct lsv1; ss.
esplits; eauto. }
ss. destruct lsv1; ss.
clarify. inv LD_EXPR1.
des_ifs_safe. ss.
des_bool.
exploit H3; eauto. i; des. ss.
des_ifs_safe.
exploit IHlsv0; eauto. i; des.
des_ifs_safe.
esplits; eauto.
Qed.
Lemma lessdef_GV2val
TD gv0 gv1
(GV: GVs.lessdef gv0 gv1)
:
TODO.lift2_option Val.lessdef (GV2val TD gv0) (GV2val TD gv1)
.
Proof.
inv GV; ss.
des; ss. destruct a1, b1; ss. clarify.
inv H; ss.
- des_ifs; ss; try (by inv H0).
- des_ifs; ss; try (by inv H0).
Qed.
Lemma lessdef_mc2undefs
gv0 mcs0
(CHUNK: gv_chunks_match_typb_aux gv0 mcs0)
:
<<LD: GVs.lessdef (mc2undefs mcs0) gv0>>
.
Proof.
ginduction gv0; ii; ss.
- des_ifs. ss. econs; eauto.
- des_ifs. ss.
apply memory_chunk_eq_prop in H0. clarify.
econs; ss; eauto.
eapply IHgv0; eauto.
Qed.
Lemma lessdef_gundef
TD ty gv0
(UNDEF: gundef TD ty = ret gv0)
gv1
(CHUNK: gv_chunks_match_typb TD gv1 ty)
:
<<LD: GVs.lessdef gv0 gv1>>
.
Proof.
red.
unfold gundef, gv_chunks_match_typb in *. des_ifs.
eapply lessdef_mc2undefs; eauto.
Qed.
(* Vellvm: mbop_is_total *)
(* Just drag wf condition? *)
Lemma mbop_total
TD b0 s0 gva0 gvb0
:
exists val0, <<MBOP: mbop TD b0 s0 gva0 gvb0 = ret val0>> /\
<<CHUNK: gv_chunks_match_typb TD val0 (typ_int (Size.to_nat s0))>>
.
Proof.
assert(MBOP: exists val0, mbop TD b0 s0 gva0 gvb0 = ret val0).
{ unfold mbop.
des_ifs; try by (unfold gundef, flatten_typ; ss; esplits; eauto; des_ifs).
}
des.
expl mbop_matches_chunks.
esplits; eauto.
unfold Size.to_nat.
apply OpsemPP.gv_chunks_match_typ__gv_chunks_match_typb. auto.
Qed.
Lemma lessdef_mbop
b0 s0 val0 gva0 gva1 gvb0 gvb1
TD
(MBOP0: mbop TD b0 s0 gva0 gvb0 = ret val0)
(GVA: GVs.lessdef gva0 gva1)
(GVB: GVs.lessdef gvb0 gvb1)
:
exists val1, <<MBOP: mbop TD b0 s0 gva1 gvb1 = ret val1 >> /\ <<LD: GVs.lessdef val0 val1>>
.
Proof.
exploit lessdef_GV2val; try apply GVA; eauto.
instantiate (1:= TD).
intro VA.
exploit lessdef_GV2val; try apply GVB; eauto.
instantiate (1:= TD).
intro VB.
clear GVA GVB.
generalize (mbop_total TD b0 s0 gva1 gvb1); intro MBOP1. des.
esplits; eauto.
unfold mbop in *.
abstr (GV2val TD gva0) va0.
abstr (GV2val TD gva1) va1.
abstr (GV2val TD gvb0) vb0.
abstr (GV2val TD gvb1) vb1.
destruct va0, va1; ss; [|]; cycle 1.
{ rewrite MBOP in *. clarify. eapply GVs.lessdef_refl; eauto. }
destruct vb0, vb1; ss; [|]; cycle 1.
{ des_ifs; try rewrite MBOP in *; clarify; eapply GVs.lessdef_refl; eauto. }
inv VA; ss; cycle 1.
{ eapply lessdef_gundef; eauto. }
inv VB; ss; cycle 1.
{ assert(UNDEF: gundef TD (typ_int (Size.to_nat s0)) = ret val0).
{ destruct v0; ss. }
clear MBOP0.
eapply lessdef_gundef; eauto.
}
{ assert(val0 = val1).
{ des_ifs. }
clarify.
eapply GVs.lessdef_refl.
}
Qed.
Lemma int32_unsigned_repr_eq
(i0: int32)
:
<<EQ: i0 = (Int.repr 31 (Int.unsigned 31 i0))>>
.
Proof.
red.
destruct i0; ss.
unfold Int.repr.
apply Int.mkint_eq.
rewrite Int.Z_mod_modulus_eq.
rewrite Z.mod_small; ss.
omega.
Qed.
Lemma lessdef_inject_identity
gv0 gv1
:
genericvalues_inject.gv_inject inject_id gv0 gv1 <->
GVs.lessdef gv0 gv1
.
Proof.
split; i.
- ginduction H; ii; ss.
{ econs; eauto; ss. }
econs; eauto; ss.
splits; ss.
inv H; ss. clear CHUNK.
unfold inject_id in *. clarify.
unfold Int.add. ss.
rewrite Z.add_0_r.
rewrite <- int32_unsigned_repr_eq.
econs; eauto.
- ginduction H; ii; ss.
destruct a1, b1; ss.
des; clarify; ss.
econs; eauto.
inv H; ss.
destruct v0; ss.
econs; eauto.
{ unfold inject_id. ss. }
unfold Int.add. ss.
rewrite Z.add_0_r.
rewrite <- int32_unsigned_repr_eq.
ss.
Qed.
Lemma lessdef_inject_identity_list
l0 l1
(LD: Forall2 GVs.lessdef l0 l1)
:
<<INJ: genericvalues_inject.gvs_inject inject_id l0 l1>>