[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 ]. |
---|
| 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. |
---|
[1516] | 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 | definition nullptr: block ≝ mk_block Any OZ. |
---|
| 110 | |
---|
| 111 | (* Allocation of a fresh block with the given bounds. Return an updated |
---|
| 112 | memory state and the address of the fresh block, which initially contains |
---|
| 113 | undefined cells. Note that allocation never fails: we model an |
---|
| 114 | infinite memory. *) |
---|
| 115 | |
---|
| 116 | lemma succ_nextblock_pos: |
---|
[1988] | 117 | ∀m. OZ < Zsucc (nextblock m). |
---|
| 118 | #m lapply (nextblock_pos … m);normalize; |
---|
[1213] | 119 | cases (nextblock … m);//; |
---|
| 120 | #n cases n;//; |
---|
| 121 | qed. |
---|
| 122 | |
---|
[1988] | 123 | definition alloc : mem → Z → Z → ∀r:region. mem × Σb:block. block_region b = r ≝ |
---|
| 124 | λm,lo,hi,r. |
---|
[1213] | 125 | let b ≝ mk_block r (nextblock … m) in |
---|
[1988] | 126 | 〈mk_mem |
---|
[1213] | 127 | (update_block … b |
---|
| 128 | (empty_block … lo hi) |
---|
| 129 | (blocks … m)) |
---|
| 130 | (Zsucc (nextblock … m)) |
---|
| 131 | (succ_nextblock_pos … m), |
---|
| 132 | b〉. |
---|
[1395] | 133 | % qed. |
---|
[1213] | 134 | |
---|
| 135 | (* Freeing a block. Return the updated memory state where the given |
---|
| 136 | block address has been invalidated: future reads and writes to this |
---|
| 137 | address will fail. Note that we make no attempt to return the block |
---|
| 138 | to an allocation pool: the given block address will never be allocated |
---|
| 139 | later. *) |
---|
| 140 | |
---|
| 141 | definition free ≝ |
---|
[1988] | 142 | λm,b.mk_mem (update_block … b |
---|
| 143 | (empty_block … OZ OZ) |
---|
| 144 | (blocks … m)) |
---|
[1213] | 145 | (nextblock … m) |
---|
| 146 | (nextblock_pos … m). |
---|
| 147 | |
---|
| 148 | (* Freeing of a list of blocks. *) |
---|
| 149 | |
---|
| 150 | definition free_list ≝ |
---|
[1988] | 151 | λm,l.foldr ?? (λb,m.free m b) m l. |
---|
[1213] | 152 | |
---|
| 153 | (* XXX hack for lack of reduction with restricted unfolding *) |
---|
| 154 | lemma unfold_free_list : |
---|
[1988] | 155 | ∀m,h,t. free_list m (h::t) = free … (free_list … m t) h. |
---|
[1213] | 156 | normalize; //; qed. |
---|
| 157 | |
---|
| 158 | (* Return the low and high bounds for the given block address. |
---|
| 159 | Those bounds are 0 for freed or not yet allocated address. *) |
---|
| 160 | |
---|
[1988] | 161 | definition low_bound : mem → block → Z ≝ |
---|
| 162 | λm,b.low … (blocks … m b). |
---|
| 163 | definition high_bound : mem → block → Z ≝ |
---|
| 164 | λm,b.high … (blocks … m b). |
---|
| 165 | definition block_region: mem → block → region ≝ |
---|
| 166 | λm,b.block_region b. (* TODO: should I keep the mem argument for uniformity, or get rid of it? *) |
---|
[1213] | 167 | |
---|
| 168 | (* A block address is valid if it was previously allocated. It remains valid |
---|
| 169 | even after being freed. *) |
---|
| 170 | |
---|
| 171 | (* TODO: should this check for region? *) |
---|
[1988] | 172 | definition valid_block : mem → block → Prop ≝ |
---|
| 173 | λm,b.block_id b < nextblock … m. |
---|
[1213] | 174 | |
---|
| 175 | (* FIXME: hacks to get around lack of nunfold *) |
---|
[1988] | 176 | lemma unfold_low_bound : ∀m,b. low_bound m b = low … (blocks … m b). |
---|
[1213] | 177 | //; qed. |
---|
[1988] | 178 | lemma unfold_high_bound : ∀m,b. high_bound m b = high … (blocks … m b). |
---|
[1213] | 179 | //; qed. |
---|
[1988] | 180 | lemma unfold_valid_block : ∀m,b. (valid_block m b) = (block_id b < nextblock … m). |
---|
[1213] | 181 | //; qed. |
---|