source: src/joint/BEMem.ma @ 2217

Last change on this file since 2217 was 2185, checked in by campbell, 8 years ago

Use bitvectors for offsets.

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