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 *)
18 (* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Ultima modifica: 05/08/2009 *)
21 (* ********************************************************************** *)
23 include "freescale/memory_struct.ma".
24 include "num/word16.ma".
25 include "common/option.ma".
26 include "common/list.ma".
28 (* ********************* *)
29 (* MEMORIA E DESCRITTORE *)
30 (* ********************* *)
32 (* tutta la memoria non installata *)
33 ndefinition mt_out_of_bound_memory ≝
34 let lev4 ≝ array_16T ?
35 MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND
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
40 let lev3 ≝ array_16T ?
41 lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4
42 lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4
44 let lev2 ≝ array_16T ?
45 lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3
46 lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3
48 let lev1 ≝ array_16T ?
49 lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2
50 lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2
54 (* tutta la memoria a 0 *)
55 ndefinition mt_zero_memory ≝
56 let lev4 ≝ array_16T ?
57 (mk_byte8 x0 x0) (mk_byte8 x0 x0) (mk_byte8 x0 x0) (mk_byte8 x0 x0)
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)
62 let lev3 ≝ array_16T ?
63 lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4
64 lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4
66 let lev2 ≝ array_16T ?
67 lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3
68 lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3
70 let lev1 ≝ array_16T ?
71 lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2
72 lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2
76 (* visita di un albero da 64KB di elementi: ln16(65536)=4 passaggi *)
77 ndefinition mt_visit ≝
78 λT:Type.λdata:Array16T (Array16T (Array16T (Array16T T))).λaddr:word16.
81 getn_array16T (b8l wl) ?
82 (getn_array16T (b8h wl) ?
83 (getn_array16T (b8l wh) ?
84 (getn_array16T (b8h wh) ? data))) ].
86 (* scrittura di un elemento in un albero da 64KB *)
87 ndefinition mt_update ≝
88 λT:Type.λdata:Array16T (Array16T (Array16T (Array16T T))).λaddr:word16.λv:T.
91 let lev2 ≝ getn_array16T (b8h wh) ? data in
92 let lev3 ≝ getn_array16T (b8l wh) ? lev2 in
93 let lev4 ≝ getn_array16T (b8h wl) ? lev3 in
94 setn_array16T (b8h wh) ? data
95 (setn_array16T (b8l wh) ? lev2
96 (setn_array16T (b8h wl) ? lev3
97 (setn_array16T (b8l wl) T lev4 v))) ].
99 (* scrittura di un range in un albero da 64KB *)
100 ndefinition mt_update_ranged ≝
101 λT:Type.λdata:Array16T (Array16T (Array16T (Array16T T))).λi,s:word16.λv:T.
103 match le_w16 i s with
109 let aux_4 ≝ Array16T T in
110 let aux_3 ≝ Array16T (Array16T T) in
111 let aux_2 ≝ Array16T (Array16T (Array16T T)) in
113 let ilev2 ≝ getn_array16T (b8h ih) aux_2 data in
114 let ilev3 ≝ getn_array16T (b8l ih) aux_3 ilev2 in
115 let ilev4 ≝ getn_array16T (b8h il) aux_4 ilev3 in
117 let slev2 ≝ getn_array16T (b8h sh) aux_2 data in
118 let slev3 ≝ getn_array16T (b8l sh) aux_3 slev2 in
119 let slev4 ≝ getn_array16T (b8h sl) aux_4 slev3 in
121 let vlev4 ≝ array_16T T v v v v v v v v v v v v v v v v in
122 let vlev3 ≝ array_16T aux_4 vlev4 vlev4 vlev4 vlev4 vlev4 vlev4 vlev4 vlev4
123 vlev4 vlev4 vlev4 vlev4 vlev4 vlev4 vlev4 vlev4 in
124 let vlev2 ≝ array_16T aux_3 vlev3 vlev3 vlev3 vlev3 vlev3 vlev3 vlev3 vlev3
125 vlev3 vlev3 vlev3 vlev3 vlev3 vlev3 vlev3 vlev3 in
127 match eq_ex (b8h ih) (b8h sh) with
128 [ true ⇒ match eq_ex (b8l ih) (b8l sh) with
129 [ true ⇒ match eq_ex (b8h il) (b8h sl) with
130 (* caso 0x...(X) a 0x...(Y) *)
131 [ true ⇒ setn_array16T (b8h ih) aux_2 data
132 (setn_array16T (b8l ih) aux_3 ilev2
133 (setn_array16T (b8h il) aux_4 ilev3
134 (* cambio a partire da livello 4 *)
135 (setmn_array16T (b8l il) (b8l sl) T ilev4 v))) (* ...X,...Y *)
136 (* caso 0x..(X1)(X2) a 0x..(Y1)(Y2) *)
137 | false ⇒ setn_array16T (b8h ih) aux_2 data
138 (setn_array16T (b8l ih) aux_3 ilev2
139 (* cambio a partire da livello 3 *)
140 (setn_array16T (b8h sl) aux_4 (* ..(Y1)0,..(Y1)(Y2) *)
141 (setmn_array16T_succ_pred (b8h il) (b8h sl) aux_4 (* ..(X1+1).,..(Y1-1). *)
142 (setn_array16T (b8h il) aux_4 ilev3
143 (setmn_array16T (b8l il) xF T ilev4 v)) (* ..(X1)(X2),..(X1)F *)
145 (setmn_array16T x0 (b8l sl) T slev4 v))) ]
146 (* caso 0x.(X1)(X2)(X3) a 0x..(Y1)(Y2)(Y3) *)
147 | false ⇒ setn_array16T (b8h ih) aux_2 data
148 (* cambio a partire da livello 2 *)
149 (setn_array16T (b8l sh) aux_3
150 (setmn_array16T_succ_pred (b8l ih) (b8l sh) aux_3 (* .(X1+1)..,.(Y1-1).. *)
151 (setn_array16T (b8l ih) aux_3 ilev2
152 (setmn_array16T_succ (b8h il) aux_4 (* .(X1)(X2+1).,.(X1)F. *)
153 (setn_array16T (b8h il) aux_4 ilev3
154 (setmn_array16T (b8l il) xF T ilev4 v)) (* .(X1)(X2)(X3),.(X1)(X2)F *)
157 (setmn_array16T_pred (b8h sl) aux_4 (* .(Y1)0.,.(Y1)(Y2-1). *)
158 (setn_array16T (b8h sl) aux_4 slev3
159 (setmn_array16T x0 (b8l sl) T slev4 v)) (* .(Y1)(Y2)0,.(Y1)(Y2)(Y3) *)
162 (* caso 0x(X1)(X2)(X3)(X4) a 0x(Y1)(Y2)(Y3)(Y4) *)
163 | false ⇒ setn_array16T (b8h sh) aux_2
164 (setmn_array16T_succ_pred (b8h ih) (b8h sh) aux_2 (* (X+1)...,(Y-1)... *)
165 (setn_array16T (b8h ih) aux_2 data
166 (setmn_array16T_succ (b8l ih) aux_3 (* (X1)(X2+1)..,(X1)F.. *)
167 (setn_array16T (b8l ih) aux_3 ilev2
168 (setmn_array16T_succ (b8h il) aux_4 (* (X1)(X2)(X3+1).,(X1)(X2)F. *)
169 (setn_array16T (b8h il) aux_4 ilev3
170 (setmn_array16T (b8l il) xF T ilev4 v)) (* (X1)(X2)(X3)(X4),(X1)(X2)(X3)F *)
174 (setmn_array16T_pred (b8l sh) aux_3 (* (Y1)0..,(Y1)(Y2-1).. *)
175 (setn_array16T (b8l sh) aux_3 slev2
176 (setmn_array16T_pred (b8h sl) aux_4 (* (Y1)(Y2)0.,(Y1)(Y2)(Y3-1). *)
177 (setn_array16T (b8h sl) aux_4 slev3
178 (setmn_array16T x0 (b8l sl) T slev4 v)) (* (Y1)(Y2)(Y3)0,(Y1)(Y2)(Y3)(Y4) *)
185 ndefinition mt_chk_get ≝
186 λchk:Array16T (Array16T (Array16T (Array16T memory_type))).λaddr:word16.
187 match mt_visit ? chk addr with
188 [ 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
189 | 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
190 | 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
193 (* scrivi controllando il tipo di memoria *)
194 ndefinition mt_mem_update ≝
195 λmem:Array16T (Array16T (Array16T (Array16T byte8))).
196 λchk:Array8T memory_type.
197 λaddr:word16.λv:byte8.
198 match getn_array8T o0 ? chk with
199 (* ROM? ok, ma il valore viene perso *)
200 [ MEM_READ_ONLY ⇒ Some ? mem
202 | MEM_READ_WRITE ⇒ Some ? (mt_update ? mem addr v)
203 (* NON INSTALLATA? no *)
204 | MEM_OUT_OF_BOUND ⇒ None ? ].
206 (* leggi controllando il tipo di memoria *)
207 ndefinition mt_mem_read ≝
208 λmem:Array16T (Array16T (Array16T (Array16T byte8))).
209 λchk:Array16T (Array16T (Array16T (Array16T memory_type))).
211 match mt_visit ? chk addr with
212 [ MEM_READ_ONLY ⇒ Some ? (mt_visit ? mem addr)
213 | MEM_READ_WRITE ⇒ Some ? (mt_visit ? mem addr)
214 | MEM_OUT_OF_BOUND ⇒ None ? ].
216 (* ************************** *)
217 (* CARICAMENTO PROGRAMMA/DATI *)
218 (* ************************** *)
220 (* carica a paratire da addr, overflow se si supera 0xFFFF... *)
221 nlet rec mt_load_from_source_at (old_mem:Array16T (Array16T (Array16T (Array16T byte8))))
222 (src:list byte8) (addr:word16) on src ≝
224 (* fine di source: carica da old_mem *)
226 | cons hd tl ⇒ mt_load_from_source_at (mt_update ? old_mem addr hd) tl (plus_w16_d_d addr 〈〈x0,x0〉:〈x0,x1〉〉)