source: src/joint/BEMem.ma @ 1882

Last change on this file since 1882 was 1882, checked in by tranquil, 8 years ago

big update, alas incomplete:
joint changed a bit, and all BE languages need to be updated
started development of blocks to aid preservation results, but still incomplete
if it breaks too many things, feel free to roll back

File size: 7.3 KB
Line 
1(* Memory model used in the dynamic semantics of the back-end intermediate
2   languages. Inspired by common/Mem.ma, adapted from Compcert *)
3
4(* * This file develops the memory model that is used in the dynamic
5  semantics of all the languages used in the compiler.
6  It defines a type [mem] of memory states, the following 4 basic
7  operations over memory states, and their properties:
8- [load]: read a memory chunk at a given address;
9- [store]: store a memory chunk at a given address;
10- [alloc]: allocate a fresh memory block;
11- [free]: invalidate a memory block.
12*)
13
14include "joint/BEValues.ma".
15include "common/GenMem.ma".
16
17definition becontentT ≝ mk_contentT beval BVundef.
18definition bemem ≝ mem becontentT.
19
20(* This function should be moved to common/GenMem.ma and replaces in_bounds *)
21definition do_if_in_bounds:
22 ∀A:Type[0]. bemem → pointer → (block → block_contents becontentT → Z → A) → option A ≝
23 λS,m,ptr,F.
24  let b ≝ pblock ptr in
25  if Zltb (block_id b) (nextblock … m) then
26   let content ≝ blocks … m b in
27   let off ≝ offv (poff ptr) in
28   if andb (Zleb (low … content) off) (Zleb off (high … content)) then
29    Some … (F b content off)
30   else
31    None ?
32  else
33   None ?.
34
35definition beloadv: ∀m:bemem. ∀ptr:pointer. option beval ≝
36 λm,ptr. do_if_in_bounds … m ptr (λb,content,off. contents … content off).
37
38definition bestorev: ∀m:bemem. ∀ptr:pointer. beval → option bemem ≝
39 λm,ptr,v. do_if_in_bounds … m ptr
40  (λb,content,off.
41    let contents ≝ update … off v (contents … content) in
42    let content ≝ mk_block_contents (mk_contentT beval BVundef) (low … content) (high … content) contents in
43    let blocks ≝ update_block … b content (blocks … m) in
44     mk_mem … blocks (nextblock … m) (nextblock_pos … m)).
45
46definition is_addressable : region → bool ≝ λr.match r with
47  [ XData ⇒ true | Code ⇒ true | _ ⇒ false ].
48
49
50definition is_address : (beval × beval) → Prop ≝ λa.
51  ∃p : Σp.bool_to_Prop (is_addressable (ptype p)).∃p0,p1.
52    \fst a = BVptr p p0 ∧ part_no ? p0 = 0 ∧
53    \snd a = BVptr p p1 ∧ part_no ? p1 = 1.
54
55definition is_addressb : (beval × beval) → bool ≝ λa.
56  match a with
57  [ mk_Prod a0 a1 ⇒
58    match a0 with
59    [ BVptr p0 part0 ⇒
60      is_addressable (ptype p0) ∧ eqb part0 0 ∧
61        match a1 with
62        [ BVptr p1 part1 ⇒
63          eq_pointer p0 p1 ∧ eqb part1 1
64        | _ ⇒ false
65        ]
66    | _ ⇒ false
67    ]
68  ].
69
70lemma is_addressb_elim : ∀P : bool → Prop.∀a : beval × beval.
71  (is_address a → P true) → (¬is_address a → P false) → P (is_addressb a).
72#P * *
73[4:|*: [|#b0|#r0#part0] #a1 #_ #Pfalse @Pfalse % * #x * #p0 * #p1 *** #EQ destruct(EQ)]
74#p0 #part0 #a1
75whd in match is_addressb; normalize nodelta
76elim (true_or_false_Prop (is_addressable (ptype p0)))
77#H >H
78[ @(eqb_elim part0 0) #Heq
79  [ cases a1 [|#b0|#r0#part0|#p1#part1] whd in match (?∧?);
80    [4: @eq_pointer_elim #Heq'
81      [ @(eqb_elim part1 1) #Heq''
82        [ #Ptrue #_ @Ptrue destruct
83          %{p1} [assumption] %{part0} %{part1}
84          % [ % [ % ]] try % assumption
85        ]
86      ]
87    ]
88  ]
89]
90#_ #Pfalse @Pfalse % ** #p0' #H' * #part0' * #part1' ***
91#H0 #H1 #H2 #H3 destruct /2 by absurd/
92qed.
93
94(* CSC: only pointers to XRAM or code memory ATM *)
95definition address ≝ beval × beval.
96definition safe_address ≝ Sig address is_address.
97unification hint 0 ≔ ;
98P ≟ Prod beval beval
99(*------------------*)⊢
100safe_address ≡ Sig P is_address.
101
102definition eq_address: address → address → bool ≝
103 λaddr1,addr2.
104  eq_beval (\fst addr1) (\fst addr2) ∧ eq_beval (\snd addr1) (\snd addr2).
105
106definition pointer_of_address: address → res pointer ≝
107 λp. let 〈v1,v2〉 ≝ p in pointer_of_bevals [v1;v2].
108 
109definition pointer_of_address_safe : safe_address → pointer ≝
110  λp.match \fst p return λx.\fst p = x → ? with
111    [ BVptr ptr _ ⇒ λ_.ptr
112    | _ ⇒ λabs.⊥
113    ] (refl …).
114lapply abs -abs cases p
115* #a0 #a1 * #x * #p0 * #p1 *** #H0 #H1 #H2 #H3 #H4
116destruct(H0 H4)
117qed.
118
119definition pointer_compat' ≝ λb,r.
120  match b with
121  [ mk_block r' z ⇒
122    if eq_region r' r then True
123    else
124      match r with
125      [ Any ⇒ True
126      | XData ⇒ match r' with
127        [ PData ⇒ True
128        | _ ⇒ False
129        ]
130      | _ ⇒ False
131      ]
132   ].
133
134lemma pointer_compat_to_ind : ∀b,r.pointer_compat' b r → pointer_compat b r.
135** #z ** //
136qed.
137
138lemma pointer_compat_from_ind : ∀b,r.pointer_compat b r → pointer_compat' b r.
139#b #r #H inversion H
140[ #s #id #EQ1 #EQ2 #EQ3 whd >reflexive_eq_region %
141| #id #EQ1 #EQ2 #EQ3 %
142| #r #id #EQ1 #EQ2 #EQ3 whd @eq_region_elim #EQ4 destruct(EQ4) %
143]
144qed.
145
146lemma pointer_of_address_is_safe : ∀a : safe_address.pointer_of_address a = OK … (pointer_of_address_safe a).
147** #a0 #a1 ***** #r #z #Hr #o * lapply (pointer_compat_from_ind ?? Hr)
148cases r in Hr ⊢ %; #Hr *
149** #part0 #H0 ** #part1 #H1 *** #EQa0 #EQpart0 #EQa1 #EQpart1
150destruct normalize
151@eqZb_elim [2,4,6: * #ABS elim (ABS (refl …))]
152@eqZb_elim [2,4,6: * #ABS elim (ABS (refl …))]
153#_ #_ normalize %
154qed.
155   
156definition address_of_pointer : pointer → res address ≝ beval_pair_of_pointer.
157
158example address_of_pointer_OK_to_safe :
159  ∀p,a.address_of_pointer p = OK … a → is_address a.
160#p
161lapply (refl … p)
162generalize in match p in ⊢ (???%→%); **
163whd in match (address_of_pointer ?);
164#b #H #o #EQp * #a0 #a1
165normalize #EQ destruct(EQ)
166%{p} >EQp [1,3: %]
167% [2,4: % [2,4: % [1,3: % [1,3: %]]]] %
168qed.
169
170definition safe_address_of_pointer: pointer → res safe_address ≝ λp.
171  do a as EQ ← address_of_pointer p ; return «a ,address_of_pointer_OK_to_safe ?? EQ».
172
173lemma address_of_pointer_is_safe :
174  ∀p.address_of_pointer p = ! a ← safe_address_of_pointer p ; return (a : address).
175****#z #H
176lapply (pointer_compat_from_ind ?? H) * #o
177normalize %
178qed.
179
180definition code_pointer_of_address: address → res (Σp:pointer. ptype p = Code) ≝
181code_pointer_of_beval_pair.
182
183definition address_of_code_pointer: (Σp:pointer. ptype p = Code) → address ≝ beval_pair_of_code_pointer.
184
185definition safe_address_of_code_pointer: (Σp:pointer. ptype p = Code) → safe_address ≝ address_of_code_pointer.
186cases H -H * #r #b #H #o #EQ destruct(EQ) normalize lapply H
187lapply (pointer_compat_from_ind … H) -H cases b * #z * #H
188%{«mk_pointer ? (mk_block Code z) H o,I»}
189% [2: % [2: % [ % [ % ]] % |]|]
190qed.
191
192(* Paolo: why only code pointers and not XRAM too? *)
193definition addr_add: address → nat → res address ≝
194 λaddr,n.
195  do ptr ← code_pointer_of_address addr ;
196  OK … (address_of_code_pointer (shift_pointer 16 ptr (bitvector_of_nat … n))).
197normalize cases ptr #p #E @E
198qed.
199
200definition safe_addr_add: safe_address → nat → res safe_address ≝
201 λaddr,n.
202  do ptr ← code_pointer_of_address addr ;
203  OK … (safe_address_of_code_pointer (shift_pointer 16 ptr (bitvector_of_nat … n))).
204normalize cases ptr #p #E @E
205qed.
206
207definition addr_sub: address → nat → res address ≝
208 λaddr,n.
209  do ptr ← code_pointer_of_address addr ;
210  OK … (address_of_code_pointer (neg_shift_pointer 16 ptr (bitvector_of_nat … n))).
211normalize cases ptr #p #E @E
212qed.
213
214definition safe_addr_sub: safe_address → nat → res safe_address ≝
215 λaddr,n.
216  do ptr ← code_pointer_of_address addr ;
217  OK … (safe_address_of_code_pointer (neg_shift_pointer 16 ptr (bitvector_of_nat … n))).
218normalize cases ptr #p #E @E
219qed.
Note: See TracBrowser for help on using the repository browser.