source: src/common/GenMem.ma @ 1516

Last change on this file since 1516 was 1516, checked in by sacerdot, 6 years ago

Ported to syntax of Matita 0.99.1.

File size: 6.6 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. Actually, it is so tiny that
19     the functions defined here could be put elsewhere.
20*)
21
22include "utilities/extralib.ma".
23include "common/Pointers.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
74record contentT: Type[1] ≝
75 { contentcarr:> Type[0]
76 ; undef: contentcarr
77 }.
78
79definition 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
84record 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
94record 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
102definition oneZ ≝ pos one.
103
104lemma one_pos: OZ < oneZ.
105//;
106qed.
107
108definition empty_block : ∀content. Z → Z → block_contents content ≝
109  λcontent,lo,hi.mk_block_contents content lo hi (λy. undef content).
110
111definition empty: ∀content. mem content ≝
112 λcontent.mk_mem content (λx.empty_block content OZ OZ) (pos one) one_pos.
113
114definition 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
121lemma succ_nextblock_pos:
122  ∀content.∀m. OZ < Zsucc (nextblock content m).
123#content #m lapply (nextblock_pos … m);normalize;
124cases (nextblock … m);//;
125#n cases n;//;
126qed.
127
128definition alloc : ∀content. mem content → Z → Z → ∀r:region. mem content × Σb:block. block_region b = r ≝
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〉.
138% qed.
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
146definition 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
155definition 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 *)
159lemma unfold_free_list :
160 ∀content,m,h,t. free_list content m (h::t) = free … (free_list … m t) h.
161normalize; //; 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
166definition low_bound : ∀content. mem content → block → Z ≝
167  λcontent,m,b.low … (blocks … m b).
168definition high_bound : ∀content. mem content → block → Z ≝
169  λcontent,m,b.high … (blocks … m b).
170definition 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? *)
177definition 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 *)
181lemma unfold_low_bound : ∀content,m,b. low_bound content m b = low … (blocks … m b).
182//; qed.
183lemma unfold_high_bound : ∀content,m,b. high_bound content m b = high … (blocks … m b).
184//; qed.
185lemma unfold_valid_block : ∀content,m,b. (valid_block content m b) = (block_id b < nextblock … m).
186//; qed.
Note: See TracBrowser for help on using the repository browser.