[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 |
---|
| 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. |
---|
[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 | |
---|
| 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 | |
---|
[1395] | 128 | definition alloc : ∀content. mem content → Z → Z → ∀r:region. mem content × Σb:block. block_region b = r ≝ |
---|
[1213] | 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〉. |
---|
[1395] | 138 | % qed. |
---|
[1213] | 139 | |
---|
| 140 | (* Freeing a block. Return the updated memory state where the given |
---|
| 141 | block address has been invalidated: future reads and writes to this |
---|
| 142 | address will fail. Note that we make no attempt to return the block |
---|
| 143 | to an allocation pool: the given block address will never be allocated |
---|
| 144 | later. *) |
---|
| 145 | |
---|
| 146 | definition free ≝ |
---|
| 147 | λcontent,m,b.mk_mem content (update_block … b |
---|
| 148 | (empty_block … OZ OZ) |
---|
| 149 | (blocks … m)) |
---|
| 150 | (nextblock … m) |
---|
| 151 | (nextblock_pos … m). |
---|
| 152 | |
---|
| 153 | (* Freeing of a list of blocks. *) |
---|
| 154 | |
---|
| 155 | definition free_list ≝ |
---|
| 156 | λcontent,m,l.foldr ?? (λb,m.free content m b) m l. |
---|
| 157 | |
---|
| 158 | (* XXX hack for lack of reduction with restricted unfolding *) |
---|
| 159 | lemma unfold_free_list : |
---|
| 160 | ∀content,m,h,t. free_list content m (h::t) = free … (free_list … m t) h. |
---|
| 161 | normalize; //; qed. |
---|
| 162 | |
---|
| 163 | (* Return the low and high bounds for the given block address. |
---|
| 164 | Those bounds are 0 for freed or not yet allocated address. *) |
---|
| 165 | |
---|
| 166 | definition low_bound : ∀content. mem content → block → Z ≝ |
---|
| 167 | λcontent,m,b.low … (blocks … m b). |
---|
| 168 | definition high_bound : ∀content. mem content → block → Z ≝ |
---|
| 169 | λcontent,m,b.high … (blocks … m b). |
---|
| 170 | definition block_region: ∀content. mem content → block → region ≝ |
---|
| 171 | λcontent,m,b.block_region b. (* TODO: should I keep the mem argument for uniformity, or get rid of it? *) |
---|
| 172 | |
---|
| 173 | (* A block address is valid if it was previously allocated. It remains valid |
---|
| 174 | even after being freed. *) |
---|
| 175 | |
---|
| 176 | (* TODO: should this check for region? *) |
---|
| 177 | definition valid_block : ∀content. mem content → block → Prop ≝ |
---|
| 178 | λcontent,m,b.block_id b < nextblock … m. |
---|
| 179 | |
---|
| 180 | (* FIXME: hacks to get around lack of nunfold *) |
---|
| 181 | lemma unfold_low_bound : ∀content,m,b. low_bound content m b = low … (blocks … m b). |
---|
| 182 | //; qed. |
---|
| 183 | lemma unfold_high_bound : ∀content,m,b. high_bound content m b = high … (blocks … m b). |
---|
| 184 | //; qed. |
---|
| 185 | lemma unfold_valid_block : ∀content,m,b. (valid_block content m b) = (block_id b < nextblock … m). |
---|
| 186 | //; qed. |
---|