source: Deliverables/D3.3/id-lookup-branch/common/GenMem.ma @ 1939

Last change on this file since 1939 was 1311, checked in by campbell, 9 years ago

Merge trunk to invariants branch, sorting out the handling of temporaries
in Clight/toCminor.

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