source: src/common/GenMem.ma @ 2457

Last change on this file since 2457 was 2332, checked in by garnier, 7 years ago

Some progress on switch removal. Small fix in the definition of free, in GenMem?.ma.

File size: 7.3 KB
Line 
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
21include "utilities/extralib.ma".
22include "common/Pointers.ma".
23include "common/ByteValues.ma".
24
25definition 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   
29lemma 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 …) //;
34qed.
35
36lemma 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 ?);//;
42qed.
43
44(* FIXME: workaround for lack of nunfold *)
45lemma 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
48definition 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   
52lemma 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 //
57qed.
58
59lemma 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 ?);//;
65qed.
66
67(* FIXME: workaround for lack of nunfold *)
68lemma 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
74definition 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
79record 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
89record mem : Type[0] ≝ {
90  blocks: block -> block_contents;
91  nextblock: Z;
92  nextblock_pos: OZ < nextblock
93}.
94
95(* The initial store. *)
96
97definition oneZ ≝ pos one.
98
99lemma one_pos: OZ < oneZ.
100//;
101qed.
102
103definition empty_block : Z → Z → block_contents ≝
104  λlo,hi.mk_block_contents lo hi (λy. BVundef).
105
106definition 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
114lemma succ_nextblock_pos:
115  ∀m. OZ < Zsucc (nextblock m).
116#m lapply (nextblock_pos … m);normalize;
117cases (nextblock … m);//;
118#n cases n;//;
119qed.
120
121let rec alloc (m:mem) (lo:Z) (hi:Z) (r:region) on m : mem × Σb:block. block_region b = r ≝
122  let b ≝ mk_block r (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
138definition 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
147definition free_list ≝
148  λm,l.foldr ?? (λb,m.free m b) m l.
149
150(* XXX hack for lack of reduction with restricted unfolding *)
151lemma unfold_free_list :
152 ∀m,h,t. free_list m (h::t) = free … (free_list … m t) h.
153normalize; //; 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
158definition low_bound : mem → block → Z ≝
159  λm,b.low … (blocks … m b).
160definition high_bound : mem → block → Z ≝
161  λm,b.high … (blocks … m b).
162definition 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? *)
169definition valid_block : mem → block → Prop ≝
170  λm,b.block_id b < nextblock … m.
171
172(* FIXME: hacks to get around lack of nunfold *)
173lemma unfold_low_bound : ∀m,b. low_bound m b = low … (blocks … m b).
174//; qed.
175lemma unfold_high_bound : ∀m,b. high_bound m b = high … (blocks … m b).
176//; qed.
177lemma 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 *)
185definition 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
199definition beloadv: ∀m:mem. ∀ptr:pointer. option beval ≝
200 λm,ptr. do_if_in_bounds … m ptr (λb,content,off. contents … content off).
201
202definition 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)).
Note: See TracBrowser for help on using the repository browser.