blob: 7dd0914e93c60c73b3eb71e2da4bd857745ab6c9 (
plain)
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
|
(* *************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* David Monniaux CNRS, VERIMAG *)
(* *)
(* Copyright VERIMAG. All rights reserved. *)
(* This file is distributed under the terms of the INRIA *)
(* Non-Commercial License Agreement. *)
(* *)
(* *************************************************************)
Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
Require Import AST Linking.
Require Import Memory Registers Op RTL Maps.
Require Import Globalenvs Values.
Require Import Linking Values Memory Globalenvs Events Smallstep.
Require Import Registers Op RTL.
Require Import CSE2 CSE2deps.
Require Import Lia.
Lemma ptrofs_size :
Ptrofs.wordsize = 32%nat.
Proof.
unfold Ptrofs.wordsize.
unfold Wordsize_Ptrofs.wordsize.
trivial.
Qed.
Lemma ptrofs_modulus :
Ptrofs.modulus = 4294967296.
Proof.
unfold Ptrofs.modulus.
rewrite ptrofs_size.
destruct Archi.ptr64; reflexivity.
Qed.
Section SOUNDNESS.
Variable F V : Type.
Variable genv: Genv.t F V.
Variable sp : val.
Section MEMORY_WRITE.
Variable m m2 : mem.
Variable chunkw chunkr : memory_chunk.
Variable base : val.
Variable addrw addrr valw : val.
Hypothesis STORE : Mem.storev chunkw m addrw valw = Some m2.
Section INDEXED_AWAY.
Variable ofsw ofsr : int.
Hypothesis ADDRW : eval_addressing genv sp
(Aindexed ofsw) (base :: nil) = Some addrw.
Hypothesis ADDRR : eval_addressing genv sp
(Aindexed ofsr) (base :: nil) = Some addrr.
Lemma load_store_away1 :
forall RANGEW : 0 <= Int.unsigned ofsw <= Ptrofs.modulus - largest_size_chunk,
forall RANGER : 0 <= Int.unsigned ofsr <= Ptrofs.modulus - largest_size_chunk,
forall SWAPPABLE : Int.unsigned ofsw + size_chunk chunkw <= Int.unsigned ofsr
\/ Int.unsigned ofsr + size_chunk chunkr <= Int.unsigned ofsw,
Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr.
Proof.
intros.
pose proof (max_size_chunk chunkr) as size_chunkr_bounded.
pose proof (max_size_chunk chunkw) as size_chunkw_bounded.
unfold largest_size_chunk in *.
rewrite ptrofs_modulus in *.
simpl in *.
inv ADDRR.
inv ADDRW.
destruct base; try discriminate.
eapply Mem.load_store_other with (chunk := chunkw) (v := valw) (b := b).
exact STORE.
right.
all: try (destruct (Ptrofs.unsigned_add_either i (Ptrofs.of_int ofsr)) as [OFSR | OFSR];
rewrite OFSR).
all: try (destruct (Ptrofs.unsigned_add_either i (Ptrofs.of_int ofsw)) as [OFSW | OFSW];
rewrite OFSW).
all: try rewrite ptrofs_modulus in *.
all: unfold Ptrofs.of_int.
all: repeat rewrite Ptrofs.unsigned_repr by (change Ptrofs.max_unsigned with 4294967295; lia).
all: intuition lia.
Qed.
Theorem load_store_away :
can_swap_accesses_ofs (Int.unsigned ofsr) chunkr (Int.unsigned ofsw) chunkw = true ->
Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr.
Proof.
intro SWAP.
unfold can_swap_accesses_ofs in SWAP.
repeat rewrite andb_true_iff in SWAP.
repeat rewrite orb_true_iff in SWAP.
repeat rewrite Z.leb_le in SWAP.
apply load_store_away1.
all: tauto.
Qed.
End INDEXED_AWAY.
End MEMORY_WRITE.
Section STACK_WRITE.
Variable m m2 : mem.
Variable chunkw chunkr : memory_chunk.
Variable addrw addrr valw : val.
Hypothesis STORE : Mem.storev chunkw m addrw valw = Some m2.
Section INDEXED_AWAY.
Variable ofsw ofsr : ptrofs.
Hypothesis ADDRW : eval_addressing genv sp
(Ainstack ofsw) nil = Some addrw.
Hypothesis ADDRR : eval_addressing genv sp
(Ainstack ofsr) nil = Some addrr.
Lemma stack_load_store_away1 :
forall RANGEW : 0 <= Ptrofs.unsigned ofsw <= Ptrofs.modulus - largest_size_chunk,
forall RANGER : 0 <= Ptrofs.unsigned ofsr <= Ptrofs.modulus - largest_size_chunk,
forall SWAPPABLE : Ptrofs.unsigned ofsw + size_chunk chunkw <= Ptrofs.unsigned ofsr
\/ Ptrofs.unsigned ofsr + size_chunk chunkr <= Ptrofs.unsigned ofsw,
Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr.
Proof.
intros.
pose proof (max_size_chunk chunkr) as size_chunkr_bounded.
pose proof (max_size_chunk chunkw) as size_chunkw_bounded.
unfold largest_size_chunk in *.
rewrite ptrofs_modulus in *.
simpl in *.
inv ADDRR.
inv ADDRW.
destruct sp; try discriminate.
eapply Mem.load_store_other with (chunk := chunkw) (v := valw) (b := b).
exact STORE.
right.
all: try (destruct (Ptrofs.unsigned_add_either i ofsr) as [OFSR | OFSR];
rewrite OFSR).
all: try (destruct (Ptrofs.unsigned_add_either i ofsw) as [OFSW | OFSW];
rewrite OFSW).
all: try rewrite ptrofs_modulus in *.
all: intuition lia.
Qed.
Theorem stack_load_store_away :
can_swap_accesses_ofs (Ptrofs.unsigned ofsr) chunkr (Ptrofs.unsigned ofsw) chunkw = true ->
Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr.
Proof.
intro SWAP.
unfold can_swap_accesses_ofs in SWAP.
repeat rewrite andb_true_iff in SWAP.
repeat rewrite orb_true_iff in SWAP.
repeat rewrite Z.leb_le in SWAP.
apply stack_load_store_away1.
all: tauto.
Qed.
End INDEXED_AWAY.
End STACK_WRITE.
End SOUNDNESS.
Section SOUNDNESS.
Variable F V : Type.
Variable genv: Genv.t F V.
Variable sp : val.
Lemma may_overlap_sound:
forall m m' : mem,
forall chunk addr args chunk' addr' args' v a a' rs,
(eval_addressing genv sp addr (rs ## args)) = Some a ->
(eval_addressing genv sp addr' (rs ## args')) = Some a' ->
(may_overlap chunk addr args chunk' addr' args') = false ->
(Mem.storev chunk m a v) = Some m' ->
(Mem.loadv chunk' m' a') = (Mem.loadv chunk' m a').
Proof.
intros until rs.
intros ADDR ADDR' OVERLAP STORE.
destruct addr; destruct addr'; try discriminate.
- (* Aindexed / Aindexed *)
destruct args as [ | base [ | ]]. 1,3: discriminate.
destruct args' as [ | base' [ | ]]. 1,3: discriminate.
simpl in OVERLAP.
destruct (peq base base'). 2: discriminate.
subst base'.
destruct (can_swap_accesses_ofs (Int.unsigned i0) chunk' (Int.unsigned i) chunk) eqn:SWAP.
2: discriminate.
simpl in *.
eapply load_store_away with (F:=F) (V:=V) (genv:=genv) (sp:=sp); eassumption.
- (* Ainstack / Ainstack *)
destruct args. 2: discriminate.
destruct args'. 2: discriminate.
cbn in OVERLAP.
destruct (can_swap_accesses_ofs (Ptrofs.unsigned i0) chunk' (Ptrofs.unsigned i) chunk) eqn:SWAP.
2: discriminate.
cbn in *.
eapply stack_load_store_away with (F:=F) (V:=V) (genv:=genv) (sp:=sp); eassumption.
Qed.
End SOUNDNESS.
|
