source: src/common/GenMem.ma @ 1988

Last change on this file since 1988 was 1988, checked in by campbell, 6 years ago

Abstraction of the memory contents in the memory models is no longer
necessary.

File size: 6.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.
Note: See TracBrowser for help on using the repository browser.