source: src/joint/BEMem.ma @ 1988

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

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

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