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 (* Sviluppo: 2008-2010 *)
21 (* ********************************************************************** *)
23 include "emulator/memory/memory_struct.ma".
24 include "num/word32.ma".
25 include "common/option.ma".
26 include "common/list.ma".
28 (* ********************* *)
29 (* MEMORIA E DESCRITTORE *)
30 (* ********************* *)
32 ndefinition aux_32B_filler ≝
34 let lev8 ≝ mk_Array16T T el el el el el el el el el el el el el el el el in
35 let lev7 ≝ mk_Array16T ?
36 lev8 lev8 lev8 lev8 lev8 lev8 lev8 lev8
37 lev8 lev8 lev8 lev8 lev8 lev8 lev8 lev8
39 let lev6 ≝ mk_Array16T ?
40 lev7 lev7 lev7 lev7 lev7 lev7 lev7 lev7
41 lev7 lev7 lev7 lev7 lev7 lev7 lev7 lev7
43 let lev5 ≝ mk_Array16T ?
44 lev6 lev6 lev6 lev6 lev6 lev6 lev6 lev6
45 lev6 lev6 lev6 lev6 lev6 lev6 lev6 lev6
47 let lev4 ≝ mk_Array16T ?
48 lev5 lev5 lev5 lev5 lev5 lev5 lev5 lev5
49 lev5 lev5 lev5 lev5 lev5 lev5 lev5 lev5
51 let lev3 ≝ mk_Array16T ?
52 lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4
53 lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4
55 let lev2 ≝ mk_Array16T ?
56 lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3
57 lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3
59 let lev1 ≝ mk_Array16T ?
60 lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2
61 lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2
65 ndefinition aux_32B_type ≝
66 λT:Type.Array16T (Array16T (Array16T (Array16T (Array16T (Array16T (Array16T (Array16T T))))))).
68 (* tutta la memoria non installata *)
69 ndefinition mt_out_of_bound_memory ≝ aux_32B_filler ? MEM_OUT_OF_BOUND.
71 (* tutta la memoria a 0 *)
72 ndefinition mt_zero_memory ≝ aux_32B_filler ? 〈x0,x0〉.
74 (* visita di un albero da 4GB di elementi: ln16(4GB)=8 passaggi *)
75 ndefinition mt_visit ≝
76 λT:Type.λdata:aux_32B_type T.λaddr:word32.
77 getn_array16T (cnL ? (cnL ? (cnL ? addr))) ?
78 (getn_array16T (cnH ? (cnL ? (cnL ? addr))) ?
79 (getn_array16T (cnL ? (cnH ? (cnL ? addr))) ?
80 (getn_array16T (cnH ? (cnH ? (cnL ? addr))) ?
81 (getn_array16T (cnL ? (cnL ? (cnH ? addr))) ?
82 (getn_array16T (cnH ? (cnL ? (cnH ? addr))) ?
83 (getn_array16T (cnL ? (cnH ? (cnH ? addr))) ?
84 (getn_array16T (cnH ? (cnH ? (cnH ? addr))) ? data))))))).
86 (* scrittura di un elemento in un albero da 4GB *)
87 ndefinition mt_update ≝
88 λT:Type.λdata:aux_32B_type T.λaddr:word32.λv:T.
89 let lev2 ≝ getn_array16T (cnH ? (cnH ? (cnH ? addr))) ? data in
90 let lev3 ≝ getn_array16T (cnL ? (cnH ? (cnH ? addr))) ? lev2 in
91 let lev4 ≝ getn_array16T (cnH ? (cnL ? (cnH ? addr))) ? lev3 in
92 let lev5 ≝ getn_array16T (cnL ? (cnL ? (cnH ? addr))) ? lev4 in
93 let lev6 ≝ getn_array16T (cnH ? (cnH ? (cnL ? addr))) ? lev5 in
94 let lev7 ≝ getn_array16T (cnL ? (cnH ? (cnL ? addr))) ? lev6 in
95 let lev8 ≝ getn_array16T (cnH ? (cnL ? (cnL ? addr))) ? lev7 in
97 setn_array16T (cnH ? (cnH ? (cnH ? addr))) ? data
98 (setn_array16T (cnL ? (cnH ? (cnH ? addr))) ? lev2
99 (setn_array16T (cnH ? (cnL ? (cnH ? addr))) ? lev3
100 (setn_array16T (cnL ? (cnL ? (cnH ? addr))) ? lev4
101 (setn_array16T (cnH ? (cnH ? (cnL ? addr))) ? lev5
102 (setn_array16T (cnL ? (cnH ? (cnL ? addr))) ? lev6
103 (setn_array16T (cnH ? (cnL ? (cnL ? addr))) ? lev7
104 (setn_array16T (cnL ? (cnL ? (cnL ? addr))) T lev8 v))))))).
106 (* scrittura di un range (max 64KB) in un albero da 4GB *)
107 nlet rec mt_update_ranged (T:Type) (data:aux_32B_type T) (addr:word32) (w:word16) (rw:rec_word16 w) (v:T) on rw ≝
110 | w16_S w' rw' ⇒ mt_update_ranged T (mt_update T data addr v)
111 (succ_w32 addr) w' rw' v
114 (* scrivi controllando il tipo di memoria *)
115 ndefinition mt_mem_update ≝
116 λmem:aux_32B_type byte8.
117 λchk:aux_32B_type memory_type.
118 λaddr:word32.λv:byte8.
119 match mt_visit ? chk addr with
120 (* ROM? ok, ma il valore viene perso *)
121 [ MEM_READ_ONLY ⇒ Some ? mem
123 | MEM_READ_WRITE ⇒ Some ? (mt_update ? mem addr v)
124 (* NON INSTALLATA? no *)
125 | MEM_OUT_OF_BOUND ⇒ None ? ].
127 (* leggi controllando il tipo di memoria *)
128 ndefinition mt_mem_read ≝
129 λmem:aux_32B_type byte8.
130 λchk:aux_32B_type memory_type.
132 match mt_visit ? chk addr with
133 [ MEM_READ_ONLY ⇒ Some ? (mt_visit ? mem addr)
134 | MEM_READ_WRITE ⇒ Some ? (mt_visit ? mem addr)
135 | MEM_OUT_OF_BOUND ⇒ None ? ].
137 (* ************************** *)
138 (* CARICAMENTO PROGRAMMA/DATI *)
139 (* ************************** *)
141 (* carica a paratire da addr, overflow se si supera 0xFFFF... *)
142 nlet rec mt_load_from_source_at (old_mem:aux_32B_type byte8)
143 (src:list byte8) (addr:word32) on src ≝
145 (* fine di source: carica da old_mem *)
147 | cons hd tl ⇒ mt_load_from_source_at (mt_update ? old_mem addr hd) tl (succ_w32 addr)