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. Actually, it is so tiny that |
---|
19 | the functions defined here could be put elsewhere. |
---|
20 | *) |
---|
21 | |
---|
22 | include "utilities/extralib.ma". |
---|
23 | include "common/Pointers.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 | record contentT: Type[1] ≝ |
---|
75 | { contentcarr:> Type[0] |
---|
76 | ; undef: contentcarr |
---|
77 | }. |
---|
78 | |
---|
79 | definition contentmap: contentT → Type[0] ≝ λcontent. Z → content. |
---|
80 | |
---|
81 | (* A memory block comprises the dimensions of the block (low and high bounds) |
---|
82 | plus a mapping from byte offsets to contents. *) |
---|
83 | |
---|
84 | record block_contents (content:contentT) : Type[0] ≝ { |
---|
85 | low: Z; |
---|
86 | high: Z; |
---|
87 | contents: contentmap content |
---|
88 | }. |
---|
89 | |
---|
90 | (* A memory state is a mapping from block addresses (represented by memory |
---|
91 | regions and integers) to blocks. We also maintain the address of the next |
---|
92 | unallocated block, and a proof that this address is positive. *) |
---|
93 | |
---|
94 | record mem (content:contentT): Type[0] ≝ { |
---|
95 | blocks: block -> block_contents content; |
---|
96 | nextblock: Z; |
---|
97 | nextblock_pos: OZ < nextblock |
---|
98 | }. |
---|
99 | |
---|
100 | (* The initial store. *) |
---|
101 | |
---|
102 | definition oneZ ≝ pos one. |
---|
103 | |
---|
104 | lemma one_pos: OZ < oneZ. |
---|
105 | //; |
---|
106 | qed. |
---|
107 | |
---|
108 | definition empty_block : ∀content. Z → Z → block_contents content ≝ |
---|
109 | λcontent,lo,hi.mk_block_contents content lo hi (λy. undef content). |
---|
110 | |
---|
111 | definition empty: ∀content. mem content ≝ |
---|
112 | λcontent.mk_mem content (λx.empty_block content OZ OZ) (pos one) one_pos. |
---|
113 | |
---|
114 | definition nullptr: block ≝ mk_block Any OZ. |
---|
115 | |
---|
116 | (* Allocation of a fresh block with the given bounds. Return an updated |
---|
117 | memory state and the address of the fresh block, which initially contains |
---|
118 | undefined cells. Note that allocation never fails: we model an |
---|
119 | infinite memory. *) |
---|
120 | |
---|
121 | lemma succ_nextblock_pos: |
---|
122 | ∀content.∀m. OZ < Zsucc (nextblock content m). |
---|
123 | #content #m lapply (nextblock_pos … m);normalize; |
---|
124 | cases (nextblock … m);//; |
---|
125 | #n cases n;//; |
---|
126 | qed. |
---|
127 | |
---|
128 | definition alloc : ∀content. mem content → Z → Z → region → mem content × block ≝ |
---|
129 | λcontent,m,lo,hi,r. |
---|
130 | let b ≝ mk_block r (nextblock … m) in |
---|
131 | 〈mk_mem content |
---|
132 | (update_block … b |
---|
133 | (empty_block … lo hi) |
---|
134 | (blocks … m)) |
---|
135 | (Zsucc (nextblock … m)) |
---|
136 | (succ_nextblock_pos … m), |
---|
137 | b〉. |
---|
138 | |
---|
139 | (* Freeing a block. Return the updated memory state where the given |
---|
140 | block address has been invalidated: future reads and writes to this |
---|
141 | address will fail. Note that we make no attempt to return the block |
---|
142 | to an allocation pool: the given block address will never be allocated |
---|
143 | later. *) |
---|
144 | |
---|
145 | definition free ≝ |
---|
146 | λcontent,m,b.mk_mem content (update_block … b |
---|
147 | (empty_block … OZ OZ) |
---|
148 | (blocks … m)) |
---|
149 | (nextblock … m) |
---|
150 | (nextblock_pos … m). |
---|
151 | |
---|
152 | (* Freeing of a list of blocks. *) |
---|
153 | |
---|
154 | definition free_list ≝ |
---|
155 | λcontent,m,l.foldr ?? (λb,m.free content m b) m l. |
---|
156 | |
---|
157 | (* XXX hack for lack of reduction with restricted unfolding *) |
---|
158 | lemma unfold_free_list : |
---|
159 | ∀content,m,h,t. free_list content m (h::t) = free … (free_list … m t) h. |
---|
160 | normalize; //; qed. |
---|
161 | |
---|
162 | (* Return the low and high bounds for the given block address. |
---|
163 | Those bounds are 0 for freed or not yet allocated address. *) |
---|
164 | |
---|
165 | definition low_bound : ∀content. mem content → block → Z ≝ |
---|
166 | λcontent,m,b.low … (blocks … m b). |
---|
167 | definition high_bound : ∀content. mem content → block → Z ≝ |
---|
168 | λcontent,m,b.high … (blocks … m b). |
---|
169 | definition block_region: ∀content. mem content → block → region ≝ |
---|
170 | λcontent,m,b.block_region b. (* TODO: should I keep the mem argument for uniformity, or get rid of it? *) |
---|
171 | |
---|
172 | (* A block address is valid if it was previously allocated. It remains valid |
---|
173 | even after being freed. *) |
---|
174 | |
---|
175 | (* TODO: should this check for region? *) |
---|
176 | definition valid_block : ∀content. mem content → block → Prop ≝ |
---|
177 | λcontent,m,b.block_id b < nextblock … m. |
---|
178 | |
---|
179 | (* FIXME: hacks to get around lack of nunfold *) |
---|
180 | lemma unfold_low_bound : ∀content,m,b. low_bound content m b = low … (blocks … m b). |
---|
181 | //; qed. |
---|
182 | lemma unfold_high_bound : ∀content,m,b. high_bound content m b = high … (blocks … m b). |
---|
183 | //; qed. |
---|
184 | lemma unfold_valid_block : ∀content,m,b. (valid_block content m b) = (block_id b < nextblock … m). |
---|
185 | //; qed. |
---|