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 set "baseuri" "cic:/matita/freescale/memory_abs/".
29 (*include "/media/VIRTUOSO/freescale/memory_func.ma".*)
30 include "freescale/memory_func.ma".
31 (*include "/media/VIRTUOSO/freescale/memory_trees.ma".*)
32 include "freescale/memory_trees.ma".
33 (*include "/media/VIRTUOSO/freescale/memory_bits.ma".*)
34 include "freescale/memory_bits.ma".
36 (* ********************************************* *)
37 (* ASTRAZIONE DALL'IMPLEMENTAZIONE DELLA MEMORIA *)
38 (* ********************************************* *)
40 (* tipi di implementazione della memoria *)
41 inductive memory_impl : Type ≝
43 | MEM_TREE: memory_impl
44 | MEM_BITS: memory_impl.
46 (* ausiliario per il tipo della memoria *)
47 definition aux_mem_type ≝
48 λt:memory_impl.match t with
49 [ MEM_FUNC ⇒ word16 → byte8
50 | MEM_TREE ⇒ Prod16T (Prod16T (Prod16T (Prod16T byte8)))
51 | MEM_BITS ⇒ Prod16T (Prod16T (Prod16T (Prod16T (Prod8T bool))))
54 (* ausiliario per il tipo del checker *)
55 definition aux_chk_type ≝
56 λt:memory_impl.match t with
57 [ MEM_FUNC ⇒ word16 → memory_type
58 | MEM_TREE ⇒ Prod16T (Prod16T (Prod16T (Prod16T memory_type)))
59 | MEM_BITS ⇒ Prod16T (Prod16T (Prod16T (Prod16T (Prod8T memory_type))))
62 (* unificazione di out_of_bound_memory *)
63 definition out_of_bound_memory ≝
66 return λt.aux_chk_type t
68 [ MEM_FUNC ⇒ mf_out_of_bound_memory
69 | MEM_TREE ⇒ mt_out_of_bound_memory
70 | MEM_BITS ⇒ mb_out_of_bound_memory
73 (* unificazione di zero_memory *)
74 definition zero_memory ≝
77 return λt.aux_mem_type t
79 [ MEM_FUNC ⇒ mf_zero_memory
80 | MEM_TREE ⇒ mt_zero_memory
81 | MEM_BITS ⇒ mb_zero_memory
84 (* unificazione della lettura senza chk: mem_read_abs mem addr *)
85 definition mem_read_abs ≝
88 return λt.aux_mem_type t → word16 → byte8
90 [ MEM_FUNC ⇒ λm:aux_mem_type MEM_FUNC.
93 | MEM_TREE ⇒ λm:aux_mem_type MEM_TREE.
96 | MEM_BITS ⇒ λm:aux_mem_type MEM_BITS.
98 byte8_of_bits (mt_visit (Prod8T bool) m addr)
101 (* unificazione della lettura con chk: mem_read mem chk addr *)
102 definition mem_read ≝
105 return λt.aux_mem_type t → aux_chk_type t → word16 → option byte8
107 [ MEM_FUNC ⇒ λm:aux_mem_type MEM_FUNC.
108 λc:aux_chk_type MEM_FUNC.
111 | MEM_TREE ⇒ λm:aux_mem_type MEM_TREE.
112 λc:aux_chk_type MEM_TREE.
115 | MEM_BITS ⇒ λm:aux_mem_type MEM_BITS.
116 λc:aux_chk_type MEM_BITS.
121 (* unificazione della lettura di bit con chk: mem_read mem chk addr sub *)
122 definition mem_read_bit ≝
125 return λt.aux_mem_type t → aux_chk_type t → word16 → oct → option bool
127 [ MEM_FUNC ⇒ λm:aux_mem_type MEM_FUNC.
128 λc:aux_chk_type MEM_FUNC.
131 opt_map ?? (mf_mem_read m c addr)
132 (λb.Some ? (getn_array8T o bool (bits_of_byte8 b)))
133 | MEM_TREE ⇒ λm:aux_mem_type MEM_TREE.
134 λc:aux_chk_type MEM_TREE.
137 opt_map ?? (mt_mem_read m c addr)
138 (λb.Some ? (getn_array8T o bool (bits_of_byte8 b)))
139 | MEM_BITS ⇒ λm:aux_mem_type MEM_BITS.
140 λc:aux_chk_type MEM_BITS.
143 mb_mem_read_bit m c addr o
146 (* unificazione della scrittura con chk: mem_update mem chk addr val *)
147 definition mem_update ≝
150 return λt.aux_mem_type t → aux_chk_type t → word16 → byte8 → option (aux_mem_type t)
152 [ MEM_FUNC ⇒ λm:aux_mem_type MEM_FUNC.
153 λc:aux_chk_type MEM_FUNC.
156 mf_mem_update m c addr v
157 | MEM_TREE ⇒ λm:aux_mem_type MEM_TREE.
158 λc:aux_chk_type MEM_TREE.
161 mt_mem_update m c addr v
162 | MEM_BITS ⇒ λm:aux_mem_type MEM_BITS.
163 λc:aux_chk_type MEM_BITS.
166 mb_mem_update m c addr v
169 (* unificazione della scrittura di bit con chk: mem_update mem chk addr sub val *)
170 definition mem_update_bit ≝
173 return λt.aux_mem_type t → aux_chk_type t → word16 → oct → bool → option (aux_mem_type t)
175 [ MEM_FUNC ⇒ λm:aux_mem_type MEM_FUNC.
176 λc:aux_chk_type MEM_FUNC.
180 opt_map ?? (mf_mem_read m c addr)
181 (λb.mf_mem_update m c addr (byte8_of_bits (setn_array8T o bool (bits_of_byte8 b) v)))
182 | MEM_TREE ⇒ λm:aux_mem_type MEM_TREE.
183 λc:aux_chk_type MEM_TREE.
187 opt_map ?? (mt_mem_read m c addr)
188 (λb.mt_mem_update m c addr (byte8_of_bits (setn_array8T o bool (bits_of_byte8 b) v)))
189 | MEM_BITS ⇒ λm:aux_mem_type MEM_BITS.
190 λc:aux_chk_type MEM_BITS.
194 mb_mem_update_bit m c addr o v
197 (* unificazione del caricamento: load_from_source_at old_mem source addr *)
198 definition load_from_source_at ≝
201 return λt.aux_mem_type t → list byte8 → word16 → aux_mem_type t
203 [ MEM_FUNC ⇒ λm:aux_mem_type MEM_FUNC.
206 mf_load_from_source_at m l addr
207 | MEM_TREE ⇒ λm:aux_mem_type MEM_TREE.
210 mt_load_from_source_at m l addr
211 | MEM_BITS ⇒ λm:aux_mem_type MEM_BITS.
214 mb_load_from_source_at m l addr
217 (* unificazione dell'impostazione della memoria: chk_update_ranged chk inf sup v *)
218 definition check_update_ranged ≝
221 return λt.aux_chk_type t → word16 → word16 → memory_type → aux_chk_type t
223 [ MEM_FUNC ⇒ λc:aux_chk_type MEM_FUNC.
226 mf_check_update_ranged c inf sup v
227 | MEM_TREE ⇒ λc:aux_chk_type MEM_TREE.
230 mt_update_ranged memory_type c inf sup v
231 | MEM_BITS ⇒ λc:aux_chk_type MEM_BITS.
234 mt_update_ranged (Prod8T memory_type) c inf sup (array_8T memory_type v v v v v v v v)
237 (* unificazione dell'impostazione dei bit: chk_update_bit chk addr sub v *)
238 (* NB: dove non esiste la granularita' del bit, lascio inalterato *)
239 definition check_update_bit ≝
242 return λt.aux_chk_type t → word16 → oct → memory_type → aux_chk_type t
244 [ MEM_FUNC ⇒ λc:aux_chk_type MEM_FUNC.
249 | MEM_TREE ⇒ λc:aux_chk_type MEM_TREE.
254 | MEM_BITS ⇒ λc:aux_chk_type MEM_BITS.
258 mb_chk_update_bit c addr o v