source: src/common/GenMem.ma @ 1993

Last change on this file since 1993 was 1993, checked in by campbell, 7 years ago

Make front-end memory model only depend on the general definitions by
moving a few definitions from the back-end one. Give the front-end
model a more descriptive name.

File size: 7.1 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
109definition 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
116lemma succ_nextblock_pos:
117  ∀m. OZ < Zsucc (nextblock m).
118#m lapply (nextblock_pos … m);normalize;
119cases (nextblock … m);//;
120#n cases n;//;
121qed.
122
123definition alloc : mem → Z → Z → ∀r:region. mem × Σb:block. block_region b = r ≝
124  λm,lo,hi,r.
125  let b ≝ mk_block r (nextblock … m) in
126  〈mk_mem
127    (update_block … b
128      (empty_block … lo hi)
129      (blocks … m))
130    (Zsucc (nextblock … m))
131    (succ_nextblock_pos … m),
132    b〉.
133% qed.
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
141definition free ≝
142  λm,b.mk_mem (update_block … b
143              (empty_block … OZ OZ)
144              (blocks … m))
145        (nextblock … m)
146        (nextblock_pos … m).
147
148(* Freeing of a list of blocks. *)
149
150definition free_list ≝
151  λm,l.foldr ?? (λb,m.free m b) m l.
152
153(* XXX hack for lack of reduction with restricted unfolding *)
154lemma unfold_free_list :
155 ∀m,h,t. free_list m (h::t) = free … (free_list … m t) h.
156normalize; //; 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
161definition low_bound : mem → block → Z ≝
162  λm,b.low … (blocks … m b).
163definition high_bound : mem → block → Z ≝
164  λm,b.high … (blocks … m b).
165definition 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? *)
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? *)
172definition valid_block : mem → block → Prop ≝
173  λm,b.block_id b < nextblock … m.
174
175(* FIXME: hacks to get around lack of nunfold *)
176lemma unfold_low_bound : ∀m,b. low_bound m b = low … (blocks … m b).
177//; qed.
178lemma unfold_high_bound : ∀m,b. high_bound m b = high … (blocks … m b).
179//; qed.
180lemma unfold_valid_block : ∀m,b. (valid_block m b) = (block_id b < nextblock … m).
181//; qed.
182
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 ≝ offv (poff ptr) in
192   if andb (Zleb (low … content) off) (Zleb 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.