[1213] | 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 |
---|
[1988] | 18 | between the front-end and the back-end. |
---|
[1213] | 19 | *) |
---|
| 20 | |
---|
| 21 | include "utilities/extralib.ma". |
---|
| 22 | include "common/Pointers.ma". |
---|
[1988] | 23 | include "common/ByteValues.ma". |
---|
[1213] | 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 ]. |
---|
[2608] | 51 | |
---|
[1213] | 52 | lemma update_block_s: |
---|
| 53 | ∀A: Type[0]. ∀x: block. ∀v: A. ∀f: block -> A. |
---|
| 54 | update_block … x v f x = v. |
---|
[2608] | 55 | #A * #ix #v #f whd in ⊢ (??%?); |
---|
[1213] | 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 | |
---|
[1988] | 74 | definition contentmap: Type[0] ≝ Z → beval. |
---|
[1213] | 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 | |
---|
[1988] | 79 | record block_contents : Type[0] ≝ { |
---|
[1213] | 80 | low: Z; |
---|
| 81 | high: Z; |
---|
[1988] | 82 | contents: contentmap |
---|
[1213] | 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 | |
---|
[1988] | 89 | record mem : Type[0] ≝ { |
---|
| 90 | blocks: block -> block_contents; |
---|
[1213] | 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 | |
---|
[1988] | 103 | definition empty_block : Z → Z → block_contents ≝ |
---|
| 104 | λlo,hi.mk_block_contents lo hi (λy. BVundef). |
---|
[1213] | 105 | |
---|
[1988] | 106 | definition empty: mem ≝ |
---|
| 107 | mk_mem (λx.empty_block OZ OZ) (pos one) one_pos. |
---|
[1213] | 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: |
---|
[1988] | 115 | ∀m. OZ < Zsucc (nextblock m). |
---|
| 116 | #m lapply (nextblock_pos … m);normalize; |
---|
[1213] | 117 | cases (nextblock … m);//; |
---|
| 118 | #n cases n;//; |
---|
| 119 | qed. |
---|
| 120 | |
---|
[2608] | 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 |
---|
[1988] | 123 | 〈mk_mem |
---|
[1213] | 124 | (update_block … b |
---|
| 125 | (empty_block … lo hi) |
---|
| 126 | (blocks … m)) |
---|
| 127 | (Zsucc (nextblock … m)) |
---|
| 128 | (succ_nextblock_pos … m), |
---|
| 129 | b〉. |
---|
[2608] | 130 | (* % qed. *) |
---|
[1213] | 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 |
---|
[2332] | 136 | later. We make sure that no valid_pointer can exist towards this block. *) |
---|
[1213] | 137 | |
---|
| 138 | definition free ≝ |
---|
[1988] | 139 | λm,b.mk_mem (update_block … b |
---|
[2332] | 140 | (empty_block … (pos one) OZ) |
---|
[1988] | 141 | (blocks … m)) |
---|
[1213] | 142 | (nextblock … m) |
---|
| 143 | (nextblock_pos … m). |
---|
| 144 | |
---|
| 145 | (* Freeing of a list of blocks. *) |
---|
| 146 | |
---|
| 147 | definition free_list ≝ |
---|
[1988] | 148 | λm,l.foldr ?? (λb,m.free m b) m l. |
---|
[1213] | 149 | |
---|
| 150 | (* XXX hack for lack of reduction with restricted unfolding *) |
---|
| 151 | lemma unfold_free_list : |
---|
[1988] | 152 | ∀m,h,t. free_list m (h::t) = free … (free_list … m t) h. |
---|
[1213] | 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 | |
---|
[1988] | 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? *) |
---|
[1213] | 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? *) |
---|
[1988] | 169 | definition valid_block : mem → block → Prop ≝ |
---|
| 170 | λm,b.block_id b < nextblock … m. |
---|
[1213] | 171 | |
---|
| 172 | (* FIXME: hacks to get around lack of nunfold *) |
---|
[1988] | 173 | lemma unfold_low_bound : ∀m,b. low_bound m b = low … (blocks … m b). |
---|
[1213] | 174 | //; qed. |
---|
[1988] | 175 | lemma unfold_high_bound : ∀m,b. high_bound m b = high … (blocks … m b). |
---|
[1213] | 176 | //; qed. |
---|
[1988] | 177 | lemma unfold_valid_block : ∀m,b. (valid_block m b) = (block_id b < nextblock … m). |
---|
[1993] | 178 | //; qed. |
---|
| 179 | |
---|
[2185] | 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. *) |
---|
[1993] | 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 |
---|
[2185] | 191 | let off ≝ Z_of_unsigned_bitvector … (offv (poff ptr)) in |
---|
[2180] | 192 | if andb (Zleb (low … content) off) (Zltb off (high … content)) then |
---|
[1993] | 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)). |
---|
[2783] | 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 | |
---|