-
Notifications
You must be signed in to change notification settings - Fork 256
Expand file tree
/
Copy pathMemory.v
More file actions
4567 lines (4164 loc) · 142 KB
/
Memory.v
File metadata and controls
4567 lines (4164 loc) · 142 KB
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 *)
(* Sandrine Blazy, ENSIIE and INRIA Paris-Rocquencourt *)
(* with contributions from Andrew Appel, Rob Dockins, *)
(* and Gordon Stewart (Princeton University) *)
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
(* under the terms of the GNU General Public License as published by *)
(* the Free Software Foundation, either version 2 of the License, or *)
(* (at your option) any later version. This file is also distributed *)
(* under the terms of the INRIA Non-Commercial License Agreement. *)
(* *)
(* *********************************************************************)
(** This file develops the memory model that is used in the dynamic
semantics of all the languages used in the compiler.
It defines a type [mem] of memory states, the following 4 basic
operations over memory states, and their properties:
- [load]: read a memory chunk at a given address;
- [store]: store a memory chunk at a given address;
- [alloc]: allocate a fresh memory block;
- [free]: invalidate a memory block.
*)
Require Import Eqdep_dec.
Require Import Zwf.
Require Import Axioms.
Require Import Coqlib.
Require Intv.
Require Import Maps.
Require Archi.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Export Memdata.
Require Export Memtype.
(* To avoid useless definitions of inductors in extracted code. *)
Local Unset Elimination Schemes.
Local Unset Case Analysis Schemes.
Local Notation "a # b" := (PMap.get b a) (at level 1).
Module Mem <: MEM.
Definition perm_order' (po: option permission) (p: permission) :=
match po with
| Some p' => perm_order p' p
| None => False
end.
Lemma perm_order'_irr p1 p2 (po1 po2: perm_order' p1 p2): po1 = po2.
Proof.
destruct p1 as [p1|];[apply perm_order_irr|elim po1].
Qed.
Definition perm_order'' (po1 po2: option permission) :=
match po1, po2 with
| Some p1, Some p2 => perm_order p1 p2
| _, None => True
| None, Some _ => False
end.
Lemma perm_order''_irr p1 p2 (po1 po2: perm_order'' p1 p2): po1 = po2.
Proof.
destruct p1 as [p1|];destruct p2 as [p2|]; try apply perm_order_irr;
destruct po1; destruct po2; reflexivity.
Qed.
Record mem' : Type := mkmem {
mem_contents: PMap.t (ZMap.t memval); (**r [block -> offset -> memval] *)
mem_access: PMap.t (Z -> perm_kind -> option permission);
(**r [block -> offset -> kind -> option permission] *)
nextblock: block;
access_max:
forall b ofs, perm_order'' (mem_access#b ofs Max) (mem_access#b ofs Cur);
nextblock_noaccess:
forall b ofs k, ~(Plt b nextblock) -> mem_access#b ofs k = None;
contents_default:
forall b, fst mem_contents#b = Undef
}.
Definition mem := mem'.
Lemma mkmem_ext:
forall cont1 cont2 acc1 acc2 next1 next2 a1 a2 b1 b2 c1 c2,
cont1=cont2 -> acc1=acc2 -> next1=next2 ->
mkmem cont1 acc1 next1 a1 b1 c1 = mkmem cont2 acc2 next2 a2 b2 c2.
Proof.
intros. subst. f_equal; repeat (apply functional_extensionality_dep; intro).
- apply perm_order''_irr.
- apply UIP_dec. repeat decide equality.
- apply UIP_dec. apply memval_dec.
Qed.
(** * Validity of blocks and accesses *)
(** A block address is valid if it was previously allocated. It remains valid
even after being freed. *)
Definition valid_block (m: mem) (b: block) := Plt b (nextblock m).
Theorem valid_not_valid_diff:
forall m b b', valid_block m b -> ~(valid_block m b') -> b <> b'.
Proof.
intros; red; intros. subst b'. contradiction.
Qed.
Local Hint Resolve valid_not_valid_diff: mem.
(** Permissions *)
Definition perm (m: mem) (b: block) (ofs: Z) (k: perm_kind) (p: permission) : Prop :=
perm_order' (m.(mem_access)#b ofs k) p.
Theorem perm_implies:
forall m b ofs k p1 p2, perm m b ofs k p1 -> perm_order p1 p2 -> perm m b ofs k p2.
Proof.
unfold perm, perm_order'; intros.
destruct (m.(mem_access)#b ofs k); auto.
eapply perm_order_trans; eauto.
Qed.
Local Hint Resolve perm_implies: mem.
Theorem perm_cur_max:
forall m b ofs p, perm m b ofs Cur p -> perm m b ofs Max p.
Proof.
assert (forall po1 po2 p,
perm_order' po2 p -> perm_order'' po1 po2 -> perm_order' po1 p).
unfold perm_order', perm_order''. intros.
destruct po2; try contradiction.
destruct po1; try contradiction.
eapply perm_order_trans; eauto.
unfold perm; intros.
generalize (access_max m b ofs). eauto.
Qed.
Theorem perm_cur:
forall m b ofs k p, perm m b ofs Cur p -> perm m b ofs k p.
Proof.
intros. destruct k; auto. apply perm_cur_max. auto.
Qed.
Theorem perm_max:
forall m b ofs k p, perm m b ofs k p -> perm m b ofs Max p.
Proof.
intros. destruct k; auto. apply perm_cur_max. auto.
Qed.
Local Hint Resolve perm_cur perm_max: mem.
Theorem perm_valid_block:
forall m b ofs k p, perm m b ofs k p -> valid_block m b.
Proof.
unfold perm; intros.
destruct (plt b m.(nextblock)).
auto.
assert (m.(mem_access)#b ofs k = None).
eapply nextblock_noaccess; eauto.
rewrite H0 in H.
contradiction.
Qed.
Local Hint Resolve perm_valid_block: mem.
Remark perm_order_dec:
forall p1 p2, {perm_order p1 p2} + {~perm_order p1 p2}.
Proof.
intros. destruct p1; destruct p2; (left; constructor) || (right; intro PO; inversion PO).
Defined.
Remark perm_order'_dec:
forall op p, {perm_order' op p} + {~perm_order' op p}.
Proof.
intros. destruct op; unfold perm_order'.
apply perm_order_dec.
right; tauto.
Defined.
Theorem perm_dec:
forall m b ofs k p, {perm m b ofs k p} + {~ perm m b ofs k p}.
Proof.
unfold perm; intros.
apply perm_order'_dec.
Defined.
Definition range_perm (m: mem) (b: block) (lo hi: Z) (k: perm_kind) (p: permission) : Prop :=
forall ofs, lo <= ofs < hi -> perm m b ofs k p.
Theorem range_perm_implies:
forall m b lo hi k p1 p2,
range_perm m b lo hi k p1 -> perm_order p1 p2 -> range_perm m b lo hi k p2.
Proof.
unfold range_perm; intros; eauto with mem.
Qed.
Theorem range_perm_cur:
forall m b lo hi k p,
range_perm m b lo hi Cur p -> range_perm m b lo hi k p.
Proof.
unfold range_perm; intros; eauto with mem.
Qed.
Theorem range_perm_max:
forall m b lo hi k p,
range_perm m b lo hi k p -> range_perm m b lo hi Max p.
Proof.
unfold range_perm; intros; eauto with mem.
Qed.
Local Hint Resolve range_perm_implies range_perm_cur range_perm_max: mem.
Lemma range_perm_dec:
forall m b lo hi k p, {range_perm m b lo hi k p} + {~ range_perm m b lo hi k p}.
Proof.
intros.
induction lo using (well_founded_induction_type (Zwf_up_well_founded hi)).
destruct (zlt lo hi).
destruct (perm_dec m b lo k p).
destruct (H (lo + 1)). red. omega.
left; red; intros. destruct (zeq lo ofs). congruence. apply r. omega.
right; red; intros. elim n. red; intros; apply H0; omega.
right; red; intros. elim n. apply H0. omega.
left; red; intros. omegaContradiction.
Defined.
(** [valid_access m chunk b ofs p] holds if a memory access
of the given chunk is possible in [m] at address [b, ofs]
with current permissions [p].
This means:
- The range of bytes accessed all have current permission [p].
- The offset [ofs] is aligned.
*)
Definition valid_access (m: mem) (chunk: memory_chunk) (b: block) (ofs: Z) (p: permission): Prop :=
range_perm m b ofs (ofs + size_chunk chunk) Cur p
/\ (align_chunk chunk | ofs).
Theorem valid_access_implies:
forall m chunk b ofs p1 p2,
valid_access m chunk b ofs p1 -> perm_order p1 p2 ->
valid_access m chunk b ofs p2.
Proof.
intros. inv H. constructor; eauto with mem.
Qed.
Theorem valid_access_freeable_any:
forall m chunk b ofs p,
valid_access m chunk b ofs Freeable ->
valid_access m chunk b ofs p.
Proof.
intros.
eapply valid_access_implies; eauto. constructor.
Qed.
Local Hint Resolve valid_access_implies: mem.
Theorem valid_access_valid_block:
forall m chunk b ofs,
valid_access m chunk b ofs Nonempty ->
valid_block m b.
Proof.
intros. destruct H.
assert (perm m b ofs Cur Nonempty).
apply H. generalize (size_chunk_pos chunk). omega.
eauto with mem.
Qed.
Local Hint Resolve valid_access_valid_block: mem.
Lemma valid_access_perm:
forall m chunk b ofs k p,
valid_access m chunk b ofs p ->
perm m b ofs k p.
Proof.
intros. destruct H. apply perm_cur. apply H. generalize (size_chunk_pos chunk). omega.
Qed.
Lemma valid_access_compat:
forall m chunk1 chunk2 b ofs p,
size_chunk chunk1 = size_chunk chunk2 ->
align_chunk chunk2 <= align_chunk chunk1 ->
valid_access m chunk1 b ofs p->
valid_access m chunk2 b ofs p.
Proof.
intros. inv H1. rewrite H in H2. constructor; auto.
eapply Z.divide_trans; eauto. eapply align_le_divides; eauto.
Qed.
Lemma valid_access_dec:
forall m chunk b ofs p,
{valid_access m chunk b ofs p} + {~ valid_access m chunk b ofs p}.
Proof.
intros.
destruct (range_perm_dec m b ofs (ofs + size_chunk chunk) Cur p).
destruct (Zdivide_dec (align_chunk chunk) ofs (align_chunk_pos chunk)).
left; constructor; auto.
right; red; intro V; inv V; contradiction.
right; red; intro V; inv V; contradiction.
Defined.
(** [valid_pointer m b ofs] returns [true] if the address [b, ofs]
is nonempty in [m] and [false] if it is empty. *)
Definition valid_pointer (m: mem) (b: block) (ofs: Z): bool :=
perm_dec m b ofs Cur Nonempty.
Theorem valid_pointer_nonempty_perm:
forall m b ofs,
valid_pointer m b ofs = true <-> perm m b ofs Cur Nonempty.
Proof.
intros. unfold valid_pointer.
destruct (perm_dec m b ofs Cur Nonempty); simpl;
intuition congruence.
Qed.
Theorem valid_pointer_valid_access:
forall m b ofs,
valid_pointer m b ofs = true <-> valid_access m Mint8unsigned b ofs Nonempty.
Proof.
intros. rewrite valid_pointer_nonempty_perm.
split; intros.
split. simpl; red; intros. replace ofs0 with ofs by omega. auto.
simpl. apply Z.divide_1_l.
destruct H. apply H. simpl. omega.
Qed.
(** C allows pointers one past the last element of an array. These are not
valid according to the previously defined [valid_pointer]. The property
[weak_valid_pointer m b ofs] holds if address [b, ofs] is a valid pointer
in [m], or a pointer one past a valid block in [m]. *)
Definition weak_valid_pointer (m: mem) (b: block) (ofs: Z) :=
valid_pointer m b ofs || valid_pointer m b (ofs - 1).
Lemma weak_valid_pointer_spec:
forall m b ofs,
weak_valid_pointer m b ofs = true <->
valid_pointer m b ofs = true \/ valid_pointer m b (ofs - 1) = true.
Proof.
intros. unfold weak_valid_pointer. now rewrite orb_true_iff.
Qed.
Lemma valid_pointer_implies:
forall m b ofs,
valid_pointer m b ofs = true -> weak_valid_pointer m b ofs = true.
Proof.
intros. apply weak_valid_pointer_spec. auto.
Qed.
(** * Operations over memory stores *)
(** The initial store *)
Program Definition empty: mem :=
mkmem (PMap.init (ZMap.init Undef))
(PMap.init (fun ofs k => None))
1%positive _ _ _.
Next Obligation.
repeat rewrite PMap.gi. red; auto.
Qed.
Next Obligation.
rewrite PMap.gi. auto.
Qed.
Next Obligation.
rewrite PMap.gi. auto.
Qed.
(** Allocation of a fresh block with the given bounds. Return an updated
memory state and the address of the fresh block, which initially contains
undefined cells. Note that allocation never fails: we model an
infinite memory. *)
Program Definition alloc (m: mem) (lo hi: Z) :=
(mkmem (PMap.set m.(nextblock)
(ZMap.init Undef)
m.(mem_contents))
(PMap.set m.(nextblock)
(fun ofs k => if zle lo ofs && zlt ofs hi then Some Freeable else None)
m.(mem_access))
(Pos.succ m.(nextblock))
_ _ _,
m.(nextblock)).
Next Obligation.
repeat rewrite PMap.gsspec. destruct (peq b (nextblock m)).
subst b. destruct (zle lo ofs && zlt ofs hi); red; auto with mem.
apply access_max.
Qed.
Next Obligation.
rewrite PMap.gsspec. destruct (peq b (nextblock m)).
subst b. elim H. apply Plt_succ.
apply nextblock_noaccess. red; intros; elim H.
apply Plt_trans_succ; auto.
Qed.
Next Obligation.
rewrite PMap.gsspec. destruct (peq b (nextblock m)). auto. apply contents_default.
Qed.
(** Freeing a block between the given bounds.
Return the updated memory state where the given range of the given block
has been invalidated: future reads and writes to this
range will fail. Requires freeable permission on the given range. *)
Program Definition unchecked_free (m: mem) (b: block) (lo hi: Z): mem :=
mkmem m.(mem_contents)
(PMap.set b
(fun ofs k => if zle lo ofs && zlt ofs hi then None else m.(mem_access)#b ofs k)
m.(mem_access))
m.(nextblock) _ _ _.
Next Obligation.
repeat rewrite PMap.gsspec. destruct (peq b0 b).
destruct (zle lo ofs && zlt ofs hi). red; auto. apply access_max.
apply access_max.
Qed.
Next Obligation.
repeat rewrite PMap.gsspec. destruct (peq b0 b). subst.
destruct (zle lo ofs && zlt ofs hi). auto. apply nextblock_noaccess; auto.
apply nextblock_noaccess; auto.
Qed.
Next Obligation.
apply contents_default.
Qed.
Definition free (m: mem) (b: block) (lo hi: Z): option mem :=
if range_perm_dec m b lo hi Cur Freeable
then Some(unchecked_free m b lo hi)
else None.
Fixpoint free_list (m: mem) (l: list (block * Z * Z)) {struct l}: option mem :=
match l with
| nil => Some m
| (b, lo, hi) :: l' =>
match free m b lo hi with
| None => None
| Some m' => free_list m' l'
end
end.
(** Memory reads. *)
(** Reading N adjacent bytes in a block content. *)
Fixpoint getN (n: nat) (p: Z) (c: ZMap.t memval) {struct n}: list memval :=
match n with
| O => nil
| S n' => ZMap.get p c :: getN n' (p + 1) c
end.
(** [load chunk m b ofs] perform a read in memory state [m], at address
[b] and offset [ofs]. It returns the value of the memory chunk
at that address. [None] is returned if the accessed bytes
are not readable. *)
Definition load (chunk: memory_chunk) (m: mem) (b: block) (ofs: Z): option val :=
if valid_access_dec m chunk b ofs Readable
then Some(decode_val chunk (getN (size_chunk_nat chunk) ofs (m.(mem_contents)#b)))
else None.
(** [loadv chunk m addr] is similar, but the address and offset are given
as a single value [addr], which must be a pointer value. *)
Definition loadv (chunk: memory_chunk) (m: mem) (addr: val) : option val :=
match addr with
| Vptr b ofs => load chunk m b (Ptrofs.unsigned ofs)
| _ => None
end.
(** [loadbytes m b ofs n] reads [n] consecutive bytes starting at
location [(b, ofs)]. Returns [None] if the accessed locations are
not readable. *)
Definition loadbytes (m: mem) (b: block) (ofs n: Z): option (list memval) :=
if range_perm_dec m b ofs (ofs + n) Cur Readable
then Some (getN (nat_of_Z n) ofs (m.(mem_contents)#b))
else None.
(** Memory stores. *)
(** Writing N adjacent bytes in a block content. *)
Fixpoint setN (vl: list memval) (p: Z) (c: ZMap.t memval) {struct vl}: ZMap.t memval :=
match vl with
| nil => c
| v :: vl' => setN vl' (p + 1) (ZMap.set p v c)
end.
Remark setN_other:
forall vl c p q,
(forall r, p <= r < p + Z.of_nat (length vl) -> r <> q) ->
ZMap.get q (setN vl p c) = ZMap.get q c.
Proof.
induction vl; intros; simpl.
auto.
simpl length in H. rewrite Nat2Z.inj_succ in H.
transitivity (ZMap.get q (ZMap.set p a c)).
apply IHvl. intros. apply H. omega.
apply ZMap.gso. apply not_eq_sym. apply H. omega.
Qed.
Remark setN_outside:
forall vl c p q,
q < p \/ q >= p + Z.of_nat (length vl) ->
ZMap.get q (setN vl p c) = ZMap.get q c.
Proof.
intros. apply setN_other.
intros. omega.
Qed.
Remark getN_setN_same:
forall vl p c,
getN (length vl) p (setN vl p c) = vl.
Proof.
induction vl; intros; simpl.
auto.
decEq.
rewrite setN_outside. apply ZMap.gss. omega.
apply IHvl.
Qed.
Remark getN_exten:
forall c1 c2 n p,
(forall i, p <= i < p + Z.of_nat n -> ZMap.get i c1 = ZMap.get i c2) ->
getN n p c1 = getN n p c2.
Proof.
induction n; intros. auto. rewrite Nat2Z.inj_succ in H. simpl. decEq.
apply H. omega. apply IHn. intros. apply H. omega.
Qed.
Remark getN_setN_disjoint:
forall vl q c n p,
Intv.disjoint (p, p + Z.of_nat n) (q, q + Z.of_nat (length vl)) ->
getN n p (setN vl q c) = getN n p c.
Proof.
intros. apply getN_exten. intros. apply setN_other.
intros; red; intros; subst r. eelim H; eauto.
Qed.
Remark getN_setN_outside:
forall vl q c n p,
p + Z.of_nat n <= q \/ q + Z.of_nat (length vl) <= p ->
getN n p (setN vl q c) = getN n p c.
Proof.
intros. apply getN_setN_disjoint. apply Intv.disjoint_range. auto.
Qed.
Remark setN_default:
forall vl q c, fst (setN vl q c) = fst c.
Proof.
induction vl; simpl; intros. auto. rewrite IHvl. auto.
Qed.
(** [store chunk m b ofs v] perform a write in memory state [m].
Value [v] is stored at address [b] and offset [ofs].
Return the updated memory store, or [None] if the accessed bytes
are not writable. *)
Program Definition store (chunk: memory_chunk) (m: mem) (b: block) (ofs: Z) (v: val): option mem :=
if valid_access_dec m chunk b ofs Writable then
Some (mkmem (PMap.set b
(setN (encode_val chunk v) ofs (m.(mem_contents)#b))
m.(mem_contents))
m.(mem_access)
m.(nextblock)
_ _ _)
else
None.
Next Obligation. apply access_max. Qed.
Next Obligation. apply nextblock_noaccess; auto. Qed.
Next Obligation.
rewrite PMap.gsspec. destruct (peq b0 b).
rewrite setN_default. apply contents_default.
apply contents_default.
Qed.
(** [storev chunk m addr v] is similar, but the address and offset are given
as a single value [addr], which must be a pointer value. *)
Definition storev (chunk: memory_chunk) (m: mem) (addr v: val) : option mem :=
match addr with
| Vptr b ofs => store chunk m b (Ptrofs.unsigned ofs) v
| _ => None
end.
(** [storebytes m b ofs bytes] stores the given list of bytes [bytes]
starting at location [(b, ofs)]. Returns updated memory state
or [None] if the accessed locations are not writable. *)
Program Definition storebytes (m: mem) (b: block) (ofs: Z) (bytes: list memval) : option mem :=
if range_perm_dec m b ofs (ofs + Z.of_nat (length bytes)) Cur Writable then
Some (mkmem
(PMap.set b (setN bytes ofs (m.(mem_contents)#b)) m.(mem_contents))
m.(mem_access)
m.(nextblock)
_ _ _)
else
None.
Next Obligation. apply access_max. Qed.
Next Obligation. apply nextblock_noaccess; auto. Qed.
Next Obligation.
rewrite PMap.gsspec. destruct (peq b0 b).
rewrite setN_default. apply contents_default.
apply contents_default.
Qed.
(** [drop_perm m b lo hi p] sets the max permissions of the byte range
[(b, lo) ... (b, hi - 1)] to [p]. These bytes must have current permissions
[Freeable] in the initial memory state [m].
Returns updated memory state, or [None] if insufficient permissions. *)
Program Definition drop_perm (m: mem) (b: block) (lo hi: Z) (p: permission): option mem :=
if range_perm_dec m b lo hi Cur Freeable then
Some (mkmem m.(mem_contents)
(PMap.set b
(fun ofs k => if zle lo ofs && zlt ofs hi then Some p else m.(mem_access)#b ofs k)
m.(mem_access))
m.(nextblock) _ _ _)
else None.
Next Obligation.
repeat rewrite PMap.gsspec. destruct (peq b0 b). subst b0.
destruct (zle lo ofs && zlt ofs hi). red; auto with mem. apply access_max.
apply access_max.
Qed.
Next Obligation.
specialize (nextblock_noaccess m b0 ofs k H0). intros.
rewrite PMap.gsspec. destruct (peq b0 b). subst b0.
destruct (zle lo ofs). destruct (zlt ofs hi).
assert (perm m b ofs k Freeable). apply perm_cur. apply H; auto.
unfold perm in H2. rewrite H1 in H2. contradiction.
auto. auto. auto.
Qed.
Next Obligation.
apply contents_default.
Qed.
(** * Properties of the memory operations *)
(** Properties of the empty store. *)
Theorem nextblock_empty: nextblock empty = 1%positive.
Proof. reflexivity. Qed.
Theorem perm_empty: forall b ofs k p, ~perm empty b ofs k p.
Proof.
intros. unfold perm, empty; simpl. rewrite PMap.gi. simpl. tauto.
Qed.
Theorem valid_access_empty: forall chunk b ofs p, ~valid_access empty chunk b ofs p.
Proof.
intros. red; intros. elim (perm_empty b ofs Cur p). apply H.
generalize (size_chunk_pos chunk); omega.
Qed.
(** ** Properties related to [load] *)
Theorem valid_access_load:
forall m chunk b ofs,
valid_access m chunk b ofs Readable ->
exists v, load chunk m b ofs = Some v.
Proof.
intros. econstructor. unfold load. rewrite pred_dec_true; eauto.
Qed.
Theorem load_valid_access:
forall m chunk b ofs v,
load chunk m b ofs = Some v ->
valid_access m chunk b ofs Readable.
Proof.
intros until v. unfold load.
destruct (valid_access_dec m chunk b ofs Readable); intros.
auto.
congruence.
Qed.
Lemma load_result:
forall chunk m b ofs v,
load chunk m b ofs = Some v ->
v = decode_val chunk (getN (size_chunk_nat chunk) ofs (m.(mem_contents)#b)).
Proof.
intros until v. unfold load.
destruct (valid_access_dec m chunk b ofs Readable); intros.
congruence.
congruence.
Qed.
Local Hint Resolve load_valid_access valid_access_load: mem.
Theorem load_type:
forall m chunk b ofs v,
load chunk m b ofs = Some v ->
Val.has_type v (type_of_chunk chunk).
Proof.
intros. exploit load_result; eauto; intros. rewrite H0.
apply decode_val_type.
Qed.
Theorem load_cast:
forall m chunk b ofs v,
load chunk m b ofs = Some v ->
match chunk with
| Mint8signed => v = Val.sign_ext 8 v
| Mint8unsigned => v = Val.zero_ext 8 v
| Mint16signed => v = Val.sign_ext 16 v
| Mint16unsigned => v = Val.zero_ext 16 v
| _ => True
end.
Proof.
intros. exploit load_result; eauto.
set (l := getN (size_chunk_nat chunk) ofs m.(mem_contents)#b).
intros. subst v. apply decode_val_cast.
Qed.
Theorem load_int8_signed_unsigned:
forall m b ofs,
load Mint8signed m b ofs = option_map (Val.sign_ext 8) (load Mint8unsigned m b ofs).
Proof.
intros. unfold load.
change (size_chunk_nat Mint8signed) with (size_chunk_nat Mint8unsigned).
set (cl := getN (size_chunk_nat Mint8unsigned) ofs m.(mem_contents)#b).
destruct (valid_access_dec m Mint8signed b ofs Readable).
rewrite pred_dec_true; auto. unfold decode_val.
destruct (proj_bytes cl); auto.
simpl. decEq. decEq. rewrite Int.sign_ext_zero_ext. auto. compute; auto.
rewrite pred_dec_false; auto.
Qed.
Theorem load_int16_signed_unsigned:
forall m b ofs,
load Mint16signed m b ofs = option_map (Val.sign_ext 16) (load Mint16unsigned m b ofs).
Proof.
intros. unfold load.
change (size_chunk_nat Mint16signed) with (size_chunk_nat Mint16unsigned).
set (cl := getN (size_chunk_nat Mint16unsigned) ofs m.(mem_contents)#b).
destruct (valid_access_dec m Mint16signed b ofs Readable).
rewrite pred_dec_true; auto. unfold decode_val.
destruct (proj_bytes cl); auto.
simpl. decEq. decEq. rewrite Int.sign_ext_zero_ext. auto. compute; auto.
rewrite pred_dec_false; auto.
Qed.
(** ** Properties related to [loadbytes] *)
Theorem range_perm_loadbytes:
forall m b ofs len,
range_perm m b ofs (ofs + len) Cur Readable ->
exists bytes, loadbytes m b ofs len = Some bytes.
Proof.
intros. econstructor. unfold loadbytes. rewrite pred_dec_true; eauto.
Qed.
Theorem loadbytes_range_perm:
forall m b ofs len bytes,
loadbytes m b ofs len = Some bytes ->
range_perm m b ofs (ofs + len) Cur Readable.
Proof.
intros until bytes. unfold loadbytes.
destruct (range_perm_dec m b ofs (ofs + len) Cur Readable). auto. congruence.
Qed.
Theorem loadbytes_load:
forall chunk m b ofs bytes,
loadbytes m b ofs (size_chunk chunk) = Some bytes ->
(align_chunk chunk | ofs) ->
load chunk m b ofs = Some(decode_val chunk bytes).
Proof.
unfold loadbytes, load; intros.
destruct (range_perm_dec m b ofs (ofs + size_chunk chunk) Cur Readable);
try congruence.
inv H. rewrite pred_dec_true. auto.
split; auto.
Qed.
Theorem load_loadbytes:
forall chunk m b ofs v,
load chunk m b ofs = Some v ->
exists bytes, loadbytes m b ofs (size_chunk chunk) = Some bytes
/\ v = decode_val chunk bytes.
Proof.
intros. exploit load_valid_access; eauto. intros [A B].
exploit load_result; eauto. intros.
exists (getN (size_chunk_nat chunk) ofs m.(mem_contents)#b); split.
unfold loadbytes. rewrite pred_dec_true; auto.
auto.
Qed.
Lemma getN_length:
forall c n p, length (getN n p c) = n.
Proof.
induction n; simpl; intros. auto. decEq; auto.
Qed.
Theorem loadbytes_length:
forall m b ofs n bytes,
loadbytes m b ofs n = Some bytes ->
length bytes = nat_of_Z n.
Proof.
unfold loadbytes; intros.
destruct (range_perm_dec m b ofs (ofs + n) Cur Readable); try congruence.
inv H. apply getN_length.
Qed.
Theorem loadbytes_empty:
forall m b ofs n,
n <= 0 -> loadbytes m b ofs n = Some nil.
Proof.
intros. unfold loadbytes. rewrite pred_dec_true. rewrite nat_of_Z_neg; auto.
red; intros. omegaContradiction.
Qed.
Lemma getN_concat:
forall c n1 n2 p,
getN (n1 + n2)%nat p c = getN n1 p c ++ getN n2 (p + Z.of_nat n1) c.
Proof.
induction n1; intros.
simpl. decEq. omega.
rewrite Nat2Z.inj_succ. simpl. decEq.
replace (p + Z.succ (Z.of_nat n1)) with ((p + 1) + Z.of_nat n1) by omega.
auto.
Qed.
Theorem loadbytes_concat:
forall m b ofs n1 n2 bytes1 bytes2,
loadbytes m b ofs n1 = Some bytes1 ->
loadbytes m b (ofs + n1) n2 = Some bytes2 ->
n1 >= 0 -> n2 >= 0 ->
loadbytes m b ofs (n1 + n2) = Some(bytes1 ++ bytes2).
Proof.
unfold loadbytes; intros.
destruct (range_perm_dec m b ofs (ofs + n1) Cur Readable); try congruence.
destruct (range_perm_dec m b (ofs + n1) (ofs + n1 + n2) Cur Readable); try congruence.
rewrite pred_dec_true. rewrite nat_of_Z_plus; auto.
rewrite getN_concat. rewrite nat_of_Z_eq; auto.
congruence.
red; intros.
assert (ofs0 < ofs + n1 \/ ofs0 >= ofs + n1) by omega.
destruct H4. apply r; omega. apply r0; omega.
Qed.
Theorem loadbytes_split:
forall m b ofs n1 n2 bytes,
loadbytes m b ofs (n1 + n2) = Some bytes ->
n1 >= 0 -> n2 >= 0 ->
exists bytes1, exists bytes2,
loadbytes m b ofs n1 = Some bytes1
/\ loadbytes m b (ofs + n1) n2 = Some bytes2
/\ bytes = bytes1 ++ bytes2.
Proof.
unfold loadbytes; intros.
destruct (range_perm_dec m b ofs (ofs + (n1 + n2)) Cur Readable);
try congruence.
rewrite nat_of_Z_plus in H; auto. rewrite getN_concat in H.
rewrite nat_of_Z_eq in H; auto.
repeat rewrite pred_dec_true.
econstructor; econstructor.
split. reflexivity. split. reflexivity. congruence.
red; intros; apply r; omega.
red; intros; apply r; omega.
Qed.
Theorem load_rep:
forall ch m1 m2 b ofs v1 v2,
(forall z, 0 <= z < size_chunk ch -> ZMap.get (ofs + z) m1.(mem_contents)#b = ZMap.get (ofs + z) m2.(mem_contents)#b) ->
load ch m1 b ofs = Some v1 ->
load ch m2 b ofs = Some v2 ->
v1 = v2.
Proof.
intros.
apply load_result in H0.
apply load_result in H1.
subst.
f_equal.
rewrite size_chunk_conv in H.
remember (size_chunk_nat ch) as n; clear Heqn.
revert ofs H; induction n; intros; simpl; auto.
f_equal.
rewrite Nat2Z.inj_succ in H.
replace ofs with (ofs+0) by omega.
apply H; omega.
apply IHn.
intros.
rewrite <- Z.add_assoc.
apply H.
rewrite Nat2Z.inj_succ. omega.
Qed.
Theorem load_int64_split:
forall m b ofs v,
load Mint64 m b ofs = Some v -> Archi.ptr64 = false ->
exists v1 v2,
load Mint32 m b ofs = Some (if Archi.big_endian then v1 else v2)
/\ load Mint32 m b (ofs + 4) = Some (if Archi.big_endian then v2 else v1)
/\ Val.lessdef v (Val.longofwords v1 v2).
Proof.
intros.
exploit load_valid_access; eauto. intros [A B]. simpl in *.
exploit load_loadbytes. eexact H. simpl. intros [bytes [LB EQ]].
change 8 with (4 + 4) in LB.
exploit loadbytes_split. eexact LB. omega. omega.
intros (bytes1 & bytes2 & LB1 & LB2 & APP).
change 4 with (size_chunk Mint32) in LB1.
exploit loadbytes_load. eexact LB1.
simpl. apply Zdivides_trans with 8; auto. exists 2; auto.
intros L1.
change 4 with (size_chunk Mint32) in LB2.
exploit loadbytes_load. eexact LB2.
simpl. apply Z.divide_add_r. apply Zdivides_trans with 8; auto. exists 2; auto. exists 1; auto.
intros L2.
exists (decode_val Mint32 (if Archi.big_endian then bytes1 else bytes2));
exists (decode_val Mint32 (if Archi.big_endian then bytes2 else bytes1)).
split. destruct Archi.big_endian; auto.
split. destruct Archi.big_endian; auto.
rewrite EQ. rewrite APP. apply decode_val_int64; auto.
erewrite loadbytes_length; eauto. reflexivity.
erewrite loadbytes_length; eauto. reflexivity.
Qed.
Lemma addressing_int64_split:
forall i,
Archi.ptr64 = false ->
(8 | Ptrofs.unsigned i) ->
Ptrofs.unsigned (Ptrofs.add i (Ptrofs.of_int (Int.repr 4))) = Ptrofs.unsigned i + 4.
Proof.
intros.
rewrite Ptrofs.add_unsigned.
replace (Ptrofs.unsigned (Ptrofs.of_int (Int.repr 4))) with (Int.unsigned (Int.repr 4))
by (symmetry; apply Ptrofs.agree32_of_int; auto).
change (Int.unsigned (Int.repr 4)) with 4.
apply Ptrofs.unsigned_repr.
exploit (Zdivide_interval (Ptrofs.unsigned i) Ptrofs.modulus 8).
omega. apply Ptrofs.unsigned_range. auto.
exists (two_p (Ptrofs.zwordsize - 3)).
unfold Ptrofs.modulus, Ptrofs.zwordsize, Ptrofs.wordsize.
unfold Wordsize_Ptrofs.wordsize. destruct Archi.ptr64; reflexivity.
unfold Ptrofs.max_unsigned. omega.
Qed.
Theorem loadv_int64_split:
forall m a v,
loadv Mint64 m a = Some v -> Archi.ptr64 = false ->
exists v1 v2,
loadv Mint32 m a = Some (if Archi.big_endian then v1 else v2)
/\ loadv Mint32 m (Val.add a (Vint (Int.repr 4))) = Some (if Archi.big_endian then v2 else v1)
/\ Val.lessdef v (Val.longofwords v1 v2).
Proof.
intros. destruct a; simpl in H; inv H.
exploit load_int64_split; eauto. intros (v1 & v2 & L1 & L2 & EQ).
unfold Val.add; rewrite H0.
assert (NV: Ptrofs.unsigned (Ptrofs.add i (Ptrofs.of_int (Int.repr 4))) = Ptrofs.unsigned i + 4).
{ apply addressing_int64_split; auto.
exploit load_valid_access. eexact H2. intros [P Q]. auto. }
exists v1, v2.
Opaque Ptrofs.repr.
split. auto.
split. simpl. rewrite NV. auto.
auto.
Qed.
(** ** Properties related to [store] *)
Theorem valid_access_store:
forall m1 chunk b ofs v,
valid_access m1 chunk b ofs Writable ->
{ m2: mem | store chunk m1 b ofs v = Some m2 }.
Proof.
intros.
unfold store.
destruct (valid_access_dec m1 chunk b ofs Writable).
eauto.
contradiction.
Defined.
Local Hint Resolve valid_access_store: mem.
Section STORE.
Variable chunk: memory_chunk.
Variable m1: mem.
Variable b: block.
Variable ofs: Z.
Variable v: val.
Variable m2: mem.
Hypothesis STORE: store chunk m1 b ofs v = Some m2.
Lemma store_access: mem_access m2 = mem_access m1.
Proof.
unfold store in STORE. destruct ( valid_access_dec m1 chunk b ofs Writable); inv STORE.
auto.
Qed.
Lemma store_mem_contents:
mem_contents m2 = PMap.set b (setN (encode_val chunk v) ofs m1.(mem_contents)#b) m1.(mem_contents).
Proof.
unfold store in STORE. destruct (valid_access_dec m1 chunk b ofs Writable); inv STORE.
auto.
Qed.
Theorem perm_store_1:
forall b' ofs' k p, perm m1 b' ofs' k p -> perm m2 b' ofs' k p.