1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
19 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
21 (* Questo materiale fa parte della tesi: *)
22 (* "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale" *)
24 (* data ultima modifica 15/11/2007 *)
25 (* ********************************************************************** *)
27 include "freescale/memory_struct.ma".
29 (* ********************* *)
30 (* MEMORIA E DESCRITTORE *)
31 (* ********************* *)
33 (* tutta la memoria non installata *)
34 definition mt_out_of_bound_memory ≝
35 let lev4 ≝ array_16T ?
36 MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND
37 MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND
38 MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND
39 MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND
41 let lev3 ≝ array_16T ?
42 lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4
43 lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4
45 let lev2 ≝ array_16T ?
46 lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3
47 lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3
49 let lev1 ≝ array_16T ?
50 lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2
51 lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2
55 (* tutta la memoria a 0 *)
56 definition mt_zero_memory ≝
57 let lev4 ≝ array_16T ?
58 (mk_byte8 x0 x0) (mk_byte8 x0 x0) (mk_byte8 x0 x0) (mk_byte8 x0 x0)
59 (mk_byte8 x0 x0) (mk_byte8 x0 x0) (mk_byte8 x0 x0) (mk_byte8 x0 x0)
60 (mk_byte8 x0 x0) (mk_byte8 x0 x0) (mk_byte8 x0 x0) (mk_byte8 x0 x0)
61 (mk_byte8 x0 x0) (mk_byte8 x0 x0) (mk_byte8 x0 x0) (mk_byte8 x0 x0)
63 let lev3 ≝ array_16T ?
64 lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4
65 lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4
67 let lev2 ≝ array_16T ?
68 lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3
69 lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3
71 let lev1 ≝ array_16T ?
72 lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2
73 lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2
77 (* visita di un albero da 64KB di elementi: ln16(65536)=4 passaggi *)
79 λT:Type.λdata:Prod16T (Prod16T (Prod16T (Prod16T T))).λaddr:word16.
82 getn_array16T (b8l wl) ?
83 (getn_array16T (b8h wl) ?
84 (getn_array16T (b8l wh) ?
85 (getn_array16T (b8h wh) ? data))) ].
87 (* scrittura di un elemento in un albero da 64KB *)
88 definition mt_update ≝
89 λT:Type.λdata:Prod16T (Prod16T (Prod16T (Prod16T T))).λaddr:word16.λv:T.
92 let lev2 ≝ getn_array16T (b8h wh) ? data in
93 let lev3 ≝ getn_array16T (b8l wh) ? lev2 in
94 let lev4 ≝ getn_array16T (b8h wl) ? lev3 in
95 setn_array16T (b8h wh) ? data
96 (setn_array16T (b8l wh) ? lev2
97 (setn_array16T (b8h wl) ? lev3
98 (setn_array16T (b8l wl) T lev4 v))) ].
100 (* scrittura di un range in un albero da 64KB *)
101 definition mt_update_ranged ≝
102 λT:Type.λdata:Prod16T (Prod16T (Prod16T (Prod16T T))).λi,s:word16.λv:T.
104 match le_w16 i s with
110 let aux_4 ≝ Prod16T T in
111 let aux_3 ≝ Prod16T (Prod16T T) in
112 let aux_2 ≝ Prod16T (Prod16T (Prod16T T)) in
114 let ilev2 ≝ getn_array16T (b8h ih) aux_2 data in
115 let ilev3 ≝ getn_array16T (b8l ih) aux_3 ilev2 in
116 let ilev4 ≝ getn_array16T (b8h il) aux_4 ilev3 in
118 let slev2 ≝ getn_array16T (b8h sh) aux_2 data in
119 let slev3 ≝ getn_array16T (b8l sh) aux_3 slev2 in
120 let slev4 ≝ getn_array16T (b8h sl) aux_4 slev3 in
122 let vlev4 ≝ array_16T T v v v v v v v v v v v v v v v v in
123 let vlev3 ≝ array_16T aux_4 vlev4 vlev4 vlev4 vlev4 vlev4 vlev4 vlev4 vlev4
124 vlev4 vlev4 vlev4 vlev4 vlev4 vlev4 vlev4 vlev4 in
125 let vlev2 ≝ array_16T aux_3 vlev3 vlev3 vlev3 vlev3 vlev3 vlev3 vlev3 vlev3
126 vlev3 vlev3 vlev3 vlev3 vlev3 vlev3 vlev3 vlev3 in
128 match eq_ex (b8h ih) (b8h sh) with
129 [ true ⇒ match eq_ex (b8l ih) (b8l sh) with
130 [ true ⇒ match eq_ex (b8h il) (b8h sl) with
131 (* caso 0x...(X) a 0x...(Y) *)
132 [ true ⇒ setn_array16T (b8h ih) aux_2 data
133 (setn_array16T (b8l ih) aux_3 ilev2
134 (setn_array16T (b8h il) aux_4 ilev3
135 (* cambio a partire da livello 4 *)
136 (setmn_array16T (b8l il) (b8l sl) T ilev4 v))) (* ...X,...Y *)
137 (* caso 0x..(X1)(X2) a 0x..(Y1)(Y2) *)
138 | false ⇒ setn_array16T (b8h ih) aux_2 data
139 (setn_array16T (b8l ih) aux_3 ilev2
140 (* cambio a partire da livello 3 *)
141 (setn_array16T (b8h sl) aux_4 (* ..(Y1)0,..(Y1)(Y2) *)
142 (setmn_array16T_succ_pred (b8h il) (b8h sl) aux_4 (* ..(X1+1).,..(Y1-1). *)
143 (setn_array16T (b8h il) aux_4 ilev3
144 (setmn_array16T (b8l il) xF T ilev4 v)) (* ..(X1)(X2),..(X1)F *)
146 (setmn_array16T x0 (b8l sl) T slev4 v))) ]
147 (* caso 0x.(X1)(X2)(X3) a 0x..(Y1)(Y2)(Y3) *)
148 | false ⇒ setn_array16T (b8h ih) aux_2 data
149 (* cambio a partire da livello 2 *)
150 (setn_array16T (b8l sh) aux_3
151 (setmn_array16T_succ_pred (b8l ih) (b8l sh) aux_3 (* .(X1+1)..,.(Y1-1).. *)
152 (setn_array16T (b8l ih) aux_3 ilev2
153 (setmn_array16T_succ (b8h il) aux_4 (* .(X1)(X2+1).,.(X1)F. *)
154 (setn_array16T (b8h il) aux_4 ilev3
155 (setmn_array16T (b8l il) xF T ilev4 v)) (* .(X1)(X2)(X3),.(X1)(X2)F *)
158 (setmn_array16T_pred (b8h sl) aux_4 (* .(Y1)0.,.(Y1)(Y2-1). *)
159 (setn_array16T (b8h sl) aux_4 slev3
160 (setmn_array16T x0 (b8l sl) T slev4 v)) (* .(Y1)(Y2)0,.(Y1)(Y2)(Y3) *)
163 (* caso 0x(X1)(X2)(X3)(X4) a 0x(Y1)(Y2)(Y3)(Y4) *)
164 | false ⇒ setn_array16T (b8h sh) aux_2
165 (setmn_array16T_succ_pred (b8h ih) (b8h sh) aux_2 (* (X+1)...,(Y-1)... *)
166 (setn_array16T (b8h ih) aux_2 data
167 (setmn_array16T_succ (b8l ih) aux_3 (* (X1)(X2+1)..,(X1)F.. *)
168 (setn_array16T (b8l ih) aux_3 ilev2
169 (setmn_array16T_succ (b8h il) aux_4 (* (X1)(X2)(X3+1).,(X1)(X2)F. *)
170 (setn_array16T (b8h il) aux_4 ilev3
171 (setmn_array16T (b8l il) xF T ilev4 v)) (* (X1)(X2)(X3)(X4),(X1)(X2)(X3)F *)
175 (setmn_array16T_pred (b8l sh) aux_3 (* (Y1)0..,(Y1)(Y2-1).. *)
176 (setn_array16T (b8l sh) aux_3 slev2
177 (setmn_array16T_pred (b8h sl) aux_4 (* (Y1)(Y2)0.,(Y1)(Y2)(Y3-1). *)
178 (setn_array16T (b8h sl) aux_4 slev3
179 (setmn_array16T x0 (b8l sl) T slev4 v)) (* (Y1)(Y2)(Y3)0,(Y1)(Y2)(Y3)(Y4) *)
186 definition mt_chk_get ≝
187 λchk:Prod16T (Prod16T (Prod16T (Prod16T memory_type))).λaddr:word16.
188 match mt_visit ? chk addr with
189 [ MEM_READ_ONLY ⇒ array_8T ? MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY
190 | MEM_READ_WRITE ⇒ array_8T ? MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE
191 | MEM_OUT_OF_BOUND ⇒ array_8T ? MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND
194 (* scrivi controllando il tipo di memoria *)
195 definition mt_mem_update ≝
196 λmem:Prod16T (Prod16T (Prod16T (Prod16T byte8))).
197 λchk:Prod8T memory_type.
198 λaddr:word16.λv:byte8.
199 match getn_array8T o0 ? chk with
200 (* ROM? ok, ma il valore viene perso *)
201 [ MEM_READ_ONLY ⇒ Some ? mem
203 | MEM_READ_WRITE ⇒ Some ? (mt_update ? mem addr v)
204 (* NON INSTALLATA? no *)
205 | MEM_OUT_OF_BOUND ⇒ None ? ].
207 (* leggi controllando il tipo di memoria *)
208 definition mt_mem_read ≝
209 λmem:Prod16T (Prod16T (Prod16T (Prod16T byte8))).
210 λchk:Prod16T (Prod16T (Prod16T (Prod16T memory_type))).
212 match mt_visit ? chk addr with
213 [ MEM_READ_ONLY ⇒ Some ? (mt_visit ? mem addr)
214 | MEM_READ_WRITE ⇒ Some ? (mt_visit ? mem addr)
215 | MEM_OUT_OF_BOUND ⇒ None ? ].
217 (* ************************** *)
218 (* CARICAMENTO PROGRAMMA/DATI *)
219 (* ************************** *)
221 (* carica a paratire da addr, scartando source (pescando da old_mem) se si supera 0xFFFF... *)
222 let rec mt_load_from_source_at (old_mem:Prod16T (Prod16T (Prod16T (Prod16T byte8))))
223 (source:list byte8) (addr:word16) on source ≝
225 (* fine di source: carica da old_mem *)
227 | cons hd tl ⇒ match lt_w16 addr 〈〈xF,xF〉:〈xF,xF〉〉 with
228 (* non supera 0xFFFF, ricorsione *)
229 [ true ⇒ mt_load_from_source_at (mt_update ? old_mem addr hd) tl (plus_w16nc addr 〈〈x0,x0〉:〈x0,x1〉〉)
230 (* supera 0xFFFF, niente ricorsione *)
231 | false ⇒ mt_update ? old_mem addr hd
234 (* ********************** *)
235 (* TEOREMI/LEMMMI/ASSIOMI *)
236 (* ********************** *)
238 (* lettura da locazione diversa da quella in cui scrivo e' vecchio *)
239 (* NB: sembra corretto, ma 2^32 casi!!! *)
242 forall_word16 (λaddr1.
243 forall_word16 (λaddr2.
244 (eq_w16 addr1 addr2) ⊙
245 (eq_b8 (mt_visit ? (mt_update ? mt_zero_memory addr1 〈xF,xF〉) addr2)
252 (* verifica scrittura di range *)
253 (* NB: sembra corretto, ma 2^48 casi!!! *)
255 lemma ok_mt_update_ranged :
256 forall_word16 (λaddr1.
257 forall_word16 (λaddr2.
258 forall_word16 (λaddr3.
259 (in_range addr3 addr1 addr2) ⊙
260 (eq_b8 (mt_visit ? (mt_update_ranged ? mt_zero_memory addr1 addr2 〈xF,xF〉) addr3)