1 | (* *********************************************************************) |
---|
2 | (* *) |
---|
3 | (* The Compcert verified compiler *) |
---|
4 | (* *) |
---|
5 | (* Xavier Leroy, INRIA Paris-Rocquencourt *) |
---|
6 | (* Sandrine Blazy, ENSIIE and INRIA Paris-Rocquencourt *) |
---|
7 | (* *) |
---|
8 | (* Copyright Institut National de Recherche en Informatique et en *) |
---|
9 | (* Automatique. All rights reserved. This file is distributed *) |
---|
10 | (* under the terms of the GNU General Public License as published by *) |
---|
11 | (* the Free Software Foundation, either version 2 of the License, or *) |
---|
12 | (* (at your option) any later version. This file is also distributed *) |
---|
13 | (* under the terms of the INRIA Non-Commercial License Agreement. *) |
---|
14 | (* *) |
---|
15 | (* *********************************************************************) |
---|
16 | |
---|
17 | (* * This file describes the part of the memory model that is in common |
---|
18 | between the front-end and the back-end. |
---|
19 | *) |
---|
20 | |
---|
21 | include "utilities/extralib.ma". |
---|
22 | include "common/Pointers.ma". |
---|
23 | include "common/ByteValues.ma". |
---|
24 | |
---|
25 | definition update : ∀A: Type[0]. ∀x: Z. ∀v: A. ∀f: Z → A. Z → A ≝ |
---|
26 | λA,x,v,f. |
---|
27 | λy.match eqZb y x with [ true ⇒ v | false ⇒ f y ]. |
---|
28 | |
---|
29 | lemma update_s: |
---|
30 | ∀A: Type[0]. ∀x: Z. ∀v: A. ∀f: Z -> A. |
---|
31 | update … x v f x = v. |
---|
32 | #A #x #v #f whd in ⊢ (??%?); |
---|
33 | >(eqZb_z_z …) //; |
---|
34 | qed. |
---|
35 | |
---|
36 | lemma update_o: |
---|
37 | ∀A: Type[0]. ∀x: Z. ∀v: A. ∀f: Z -> A. ∀y: Z. |
---|
38 | x ≠ y → update … x v f y = f y. |
---|
39 | #A #x #v #f #y #H whd in ⊢ (??%?); |
---|
40 | @eqZb_elim //; |
---|
41 | #H2 cases H;#H3 elim (H3 ?);//; |
---|
42 | qed. |
---|
43 | |
---|
44 | (* FIXME: workaround for lack of nunfold *) |
---|
45 | lemma unfold_update : ∀A,x,v,f,y. update A x v f y = match eqZb y x with [ true ⇒ v | false ⇒ f y ]. |
---|
46 | //; qed. |
---|
47 | |
---|
48 | definition update_block : ∀A: Type[0]. ∀x: block. ∀v: A. ∀f: block → A. block → A ≝ |
---|
49 | λA,x,v,f. |
---|
50 | λy.match eq_block y x with [ true ⇒ v | false ⇒ f y ]. |
---|
51 | |
---|
52 | lemma update_block_s: |
---|
53 | ∀A: Type[0]. ∀x: block. ∀v: A. ∀f: block -> A. |
---|
54 | update_block … x v f x = v. |
---|
55 | #A * #ix #v #f whd in ⊢ (??%?); |
---|
56 | >eq_block_b_b // |
---|
57 | qed. |
---|
58 | |
---|
59 | lemma update_block_o: |
---|
60 | ∀A: Type[0]. ∀x: block. ∀v: A. ∀f: block -> A. ∀y: block. |
---|
61 | x ≠ y → update_block … x v f y = f y. |
---|
62 | #A #x #v #f #y #H whd in ⊢ (??%?); |
---|
63 | @eq_block_elim //; |
---|
64 | #H2 cases H;#H3 elim (H3 ?);//; |
---|
65 | qed. |
---|
66 | |
---|
67 | (* FIXME: workaround for lack of nunfold *) |
---|
68 | lemma unfold_update_block : ∀A,x,v,f,y. |
---|
69 | update_block A x v f y = match eq_block y x with [ true ⇒ v | false ⇒ f y ]. |
---|
70 | //; qed. |
---|
71 | |
---|
72 | (***************************************) |
---|
73 | |
---|
74 | definition contentmap: Type[0] ≝ Z → beval. |
---|
75 | |
---|
76 | (* A memory block comprises the dimensions of the block (low and high bounds) |
---|
77 | plus a mapping from byte offsets to contents. *) |
---|
78 | |
---|
79 | record block_contents : Type[0] ≝ { |
---|
80 | low: Z; |
---|
81 | high: Z; |
---|
82 | contents: contentmap |
---|
83 | }. |
---|
84 | |
---|
85 | (* A memory state is a mapping from block addresses (represented by memory |
---|
86 | regions and integers) to blocks. We also maintain the address of the next |
---|
87 | unallocated block, and a proof that this address is positive. *) |
---|
88 | |
---|
89 | record mem : Type[0] ≝ { |
---|
90 | blocks: block -> block_contents; |
---|
91 | nextblock: Z; |
---|
92 | nextblock_pos: OZ < nextblock |
---|
93 | }. |
---|
94 | |
---|
95 | (* The initial store. *) |
---|
96 | |
---|
97 | definition oneZ ≝ pos one. |
---|
98 | |
---|
99 | lemma one_pos: OZ < oneZ. |
---|
100 | //; |
---|
101 | qed. |
---|
102 | |
---|
103 | definition empty_block : Z → Z → block_contents ≝ |
---|
104 | λlo,hi.mk_block_contents lo hi (λy. BVundef). |
---|
105 | |
---|
106 | definition empty: mem ≝ |
---|
107 | mk_mem (λx.empty_block OZ OZ) (pos one) one_pos. |
---|
108 | |
---|
109 | (* Allocation of a fresh block with the given bounds. Return an updated |
---|
110 | memory state and the address of the fresh block, which initially contains |
---|
111 | undefined cells. Note that allocation never fails: we model an |
---|
112 | infinite memory. *) |
---|
113 | |
---|
114 | lemma succ_nextblock_pos: |
---|
115 | ∀m. OZ < Zsucc (nextblock m). |
---|
116 | #m lapply (nextblock_pos … m);normalize; |
---|
117 | cases (nextblock … m);//; |
---|
118 | #n cases n;//; |
---|
119 | qed. |
---|
120 | |
---|
121 | let rec alloc (m:mem) (lo:Z) (hi:Z) (*(r:region)*) on m : mem × block (*Σb:block. block_region b = r *) ≝ |
---|
122 | let b ≝ mk_block (nextblock … m) in |
---|
123 | 〈mk_mem |
---|
124 | (update_block … b |
---|
125 | (empty_block … lo hi) |
---|
126 | (blocks … m)) |
---|
127 | (Zsucc (nextblock … m)) |
---|
128 | (succ_nextblock_pos … m), |
---|
129 | b〉. |
---|
130 | (* % qed. *) |
---|
131 | |
---|
132 | (* Freeing a block. Return the updated memory state where the given |
---|
133 | block address has been invalidated: future reads and writes to this |
---|
134 | address will fail. Note that we make no attempt to return the block |
---|
135 | to an allocation pool: the given block address will never be allocated |
---|
136 | later. We make sure that no valid_pointer can exist towards this block. *) |
---|
137 | |
---|
138 | definition free ≝ |
---|
139 | λm,b.mk_mem (update_block … b |
---|
140 | (empty_block … (pos one) OZ) |
---|
141 | (blocks … m)) |
---|
142 | (nextblock … m) |
---|
143 | (nextblock_pos … m). |
---|
144 | |
---|
145 | (* Freeing of a list of blocks. *) |
---|
146 | |
---|
147 | definition free_list ≝ |
---|
148 | λm,l.foldr ?? (λb,m.free m b) m l. |
---|
149 | |
---|
150 | (* XXX hack for lack of reduction with restricted unfolding *) |
---|
151 | lemma unfold_free_list : |
---|
152 | ∀m,h,t. free_list m (h::t) = free … (free_list … m t) h. |
---|
153 | normalize; //; qed. |
---|
154 | |
---|
155 | (* Return the low and high bounds for the given block address. |
---|
156 | Those bounds are 0 for freed or not yet allocated address. *) |
---|
157 | |
---|
158 | definition low_bound : mem → block → Z ≝ |
---|
159 | λm,b.low … (blocks … m b). |
---|
160 | definition high_bound : mem → block → Z ≝ |
---|
161 | λm,b.high … (blocks … m b). |
---|
162 | definition block_region: mem → block → region ≝ |
---|
163 | λm,b.block_region b. (* TODO: should I keep the mem argument for uniformity, or get rid of it? *) |
---|
164 | |
---|
165 | (* A block address is valid if it was previously allocated. It remains valid |
---|
166 | even after being freed. *) |
---|
167 | |
---|
168 | (* TODO: should this check for region? *) |
---|
169 | definition valid_block : mem → block → Prop ≝ |
---|
170 | λm,b.block_id b < nextblock … m. |
---|
171 | |
---|
172 | (* FIXME: hacks to get around lack of nunfold *) |
---|
173 | lemma unfold_low_bound : ∀m,b. low_bound m b = low … (blocks … m b). |
---|
174 | //; qed. |
---|
175 | lemma unfold_high_bound : ∀m,b. high_bound m b = high … (blocks … m b). |
---|
176 | //; qed. |
---|
177 | lemma unfold_valid_block : ∀m,b. (valid_block m b) = (block_id b < nextblock … m). |
---|
178 | //; qed. |
---|
179 | |
---|
180 | (* XXX note that this won't allow access to negative offsets, and we don't |
---|
181 | currently provide any other means to access them. We could choose to get |
---|
182 | rid of them entirely. *) |
---|
183 | |
---|
184 | (* This function should be moved to common/GenMem.ma and replaces in_bounds *) |
---|
185 | definition do_if_in_bounds: |
---|
186 | ∀A:Type[0]. mem → pointer → (block → block_contents → Z → A) → option A ≝ |
---|
187 | λS,m,ptr,F. |
---|
188 | let b ≝ pblock ptr in |
---|
189 | if Zltb (block_id b) (nextblock … m) then |
---|
190 | let content ≝ blocks … m b in |
---|
191 | let off ≝ Z_of_unsigned_bitvector … (offv (poff ptr)) in |
---|
192 | if andb (Zleb (low … content) off) (Zltb off (high … content)) then |
---|
193 | Some … (F b content off) |
---|
194 | else |
---|
195 | None ? |
---|
196 | else |
---|
197 | None ?. |
---|
198 | |
---|
199 | definition beloadv: ∀m:mem. ∀ptr:pointer. option beval ≝ |
---|
200 | λm,ptr. do_if_in_bounds … m ptr (λb,content,off. contents … content off). |
---|
201 | |
---|
202 | definition bestorev: ∀m:mem. ∀ptr:pointer. beval → option mem ≝ |
---|
203 | λm,ptr,v. do_if_in_bounds … m ptr |
---|
204 | (λb,content,off. |
---|
205 | let contents ≝ update … off v (contents … content) in |
---|
206 | let content ≝ mk_block_contents (low … content) (high … content) contents in |
---|
207 | let blocks ≝ update_block … b content (blocks … m) in |
---|
208 | mk_mem … blocks (nextblock … m) (nextblock_pos … m)). |
---|
209 | |
---|
210 | (* Axiom of extensional equality for the memory *) |
---|
211 | axiom mem_ext_eq : |
---|
212 | ∀m1,m2 : mem. |
---|
213 | (∀b.let bc1 ≝ blocks m1 b in |
---|
214 | let bc2 ≝ blocks m2 b in |
---|
215 | low bc1 = low bc2 ∧ high bc1 = high bc2 ∧ |
---|
216 | ∀z.contents bc1 z = contents bc2 z) → |
---|
217 | nextblock m1 = nextblock m2 → m1 = m2. |
---|
218 | |
---|