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_func.ma".
28 include "freescale/memory_trees.ma".
29 include "freescale/memory_bits.ma".
31 (* ********************************************* *)
32 (* ASTRAZIONE DALL'IMPLEMENTAZIONE DELLA MEMORIA *)
33 (* ********************************************* *)
35 (* tipi di implementazione della memoria *)
36 ninductive memory_impl : Type ≝
38 | MEM_TREE: memory_impl
39 | MEM_BITS: memory_impl.
41 ndefinition memory_impl_ind : ΠP:memory_impl → Prop.P MEM_FUNC → P MEM_TREE → P MEM_BITS → Πm:memory_impl.P m ≝
42 λP:memory_impl → Prop.λp:P MEM_FUNC.λp1:P MEM_TREE.λp2:P MEM_BITS.λm:memory_impl.
43 match m with [ MEM_FUNC ⇒ p | MEM_TREE ⇒ p1 | MEM_BITS ⇒ p2 ].
45 ndefinition memory_impl_rec : ΠP:memory_impl → Set.P MEM_FUNC → P MEM_TREE → P MEM_BITS → Πm:memory_impl.P m ≝
46 λP:memory_impl → Set.λp:P MEM_FUNC.λp1:P MEM_TREE.λp2:P MEM_BITS.λm:memory_impl.
47 match m with [ MEM_FUNC ⇒ p | MEM_TREE ⇒ p1 | MEM_BITS ⇒ p2 ].
49 ndefinition memory_impl_rect : ΠP:memory_impl → Type.P MEM_FUNC → P MEM_TREE → P MEM_BITS → Πm:memory_impl.P m ≝
50 λP:memory_impl → Type.λp:P MEM_FUNC.λp1:P MEM_TREE.λp2:P MEM_BITS.λm:memory_impl.
51 match m with [ MEM_FUNC ⇒ p | MEM_TREE ⇒ p1 | MEM_BITS ⇒ p2 ].
53 (* ausiliario per il tipo della memoria *)
54 ndefinition aux_mem_type ≝
55 λt:memory_impl.match t with
56 [ MEM_FUNC ⇒ word16 → byte8
57 | MEM_TREE ⇒ Array16T (Array16T (Array16T (Array16T byte8)))
58 | MEM_BITS ⇒ Array16T (Array16T (Array16T (Array16T (Array8T bool))))
61 (* ausiliario per il tipo del checker *)
62 ndefinition aux_chk_type ≝
63 λt:memory_impl.match t with
64 [ MEM_FUNC ⇒ word16 → memory_type
65 | MEM_TREE ⇒ Array16T (Array16T (Array16T (Array16T memory_type)))
66 | MEM_BITS ⇒ Array16T (Array16T (Array16T (Array16T (Array8T memory_type))))
69 (* unificazione di out_of_bound_memory *)
70 ndefinition out_of_bound_memory ≝
73 return λt.aux_chk_type t
75 [ MEM_FUNC ⇒ mf_out_of_bound_memory
76 | MEM_TREE ⇒ mt_out_of_bound_memory
77 | MEM_BITS ⇒ mb_out_of_bound_memory
80 (* unificazione di zero_memory *)
81 ndefinition zero_memory ≝
84 return λt.aux_mem_type t
86 [ MEM_FUNC ⇒ mf_zero_memory
87 | MEM_TREE ⇒ mt_zero_memory
88 | MEM_BITS ⇒ mb_zero_memory
91 (* unificazione della lettura senza chk: mem_read_abs mem addr *)
92 ndefinition mem_read_abs ≝
95 return λt.aux_mem_type t → word16 → byte8
97 [ MEM_FUNC ⇒ λm:aux_mem_type MEM_FUNC.
100 | MEM_TREE ⇒ λm:aux_mem_type MEM_TREE.
102 mt_visit byte8 m addr
103 | MEM_BITS ⇒ λm:aux_mem_type MEM_BITS.
105 byte8_of_bits (mt_visit (Array8T bool) m addr)
108 (* unificazione del chk *)
109 ndefinition chk_get ≝
110 λt:memory_impl.λc:aux_chk_type t.λaddr:word16.
112 return λt.aux_chk_type t → word16 → Array8T memory_type
114 [ MEM_FUNC ⇒ mf_chk_get
115 | MEM_TREE ⇒ mt_chk_get
116 | MEM_BITS ⇒ mb_chk_get
119 (* unificazione della lettura con chk: mem_read mem chk addr *)
120 ndefinition mem_read ≝
121 λt:memory_impl.λm:aux_mem_type t.λc:aux_chk_type t.λaddr:word16.
123 return λt.aux_mem_type t → aux_chk_type t → word16 → option byte8
125 [ MEM_FUNC ⇒ mf_mem_read
126 | MEM_TREE ⇒ mt_mem_read
127 | MEM_BITS ⇒ mb_mem_read
130 (* unificazione della lettura di bit con chk: mem_read mem chk addr sub *)
131 ndefinition mem_read_bit ≝
134 return λt.aux_mem_type t → aux_chk_type t → word16 → oct → option bool
136 [ MEM_FUNC ⇒ λm:aux_mem_type MEM_FUNC.
137 λc:aux_chk_type MEM_FUNC.
140 opt_map ?? (mf_mem_read m c addr)
141 (λb.Some ? (getn_array8T o bool (bits_of_byte8 b)))
142 | MEM_TREE ⇒ λm:aux_mem_type MEM_TREE.
143 λc:aux_chk_type MEM_TREE.
146 opt_map ?? (mt_mem_read m c addr)
147 (λb.Some ? (getn_array8T o bool (bits_of_byte8 b)))
148 | MEM_BITS ⇒ λm:aux_mem_type MEM_BITS.
149 λc:aux_chk_type MEM_BITS.
152 mb_mem_read_bit m c addr o
155 (* unificazione della scrittura con chk: mem_update mem chk addr val *)
156 ndefinition mem_update ≝
157 λt:memory_impl.λm:aux_mem_type t.λc:aux_chk_type t.λaddr:word16.λv:byte8.
159 return λt.aux_mem_type t → Array8T memory_type → word16 → byte8 → option (aux_mem_type t)
161 [ MEM_FUNC ⇒ mf_mem_update
162 | MEM_TREE ⇒ mt_mem_update
163 | MEM_BITS ⇒ mb_mem_update
164 ] m (chk_get t c addr) addr v.
166 (* unificazione della scrittura di bit con chk: mem_update mem chk addr sub val *)
167 ndefinition mem_update_bit ≝
170 return λt.aux_mem_type t → aux_chk_type t → word16 → oct → bool → option (aux_mem_type t)
172 [ MEM_FUNC ⇒ λm:aux_mem_type MEM_FUNC.
173 λc:aux_chk_type MEM_FUNC.
177 opt_map ?? (mf_mem_read m c addr)
178 (λb.mf_mem_update m (chk_get MEM_FUNC c addr) addr (byte8_of_bits (setn_array8T o bool (bits_of_byte8 b) v)))
179 | MEM_TREE ⇒ λm:aux_mem_type MEM_TREE.
180 λc:aux_chk_type MEM_TREE.
184 opt_map ?? (mt_mem_read m c addr)
185 (λb.mt_mem_update m (chk_get MEM_TREE c addr) addr (byte8_of_bits (setn_array8T o bool (bits_of_byte8 b) v)))
186 | MEM_BITS ⇒ λm:aux_mem_type MEM_BITS.
187 λc:aux_chk_type MEM_BITS.
191 mb_mem_update_bit m c addr o v
194 (* unificazione del caricamento: load_from_source_at old_mem source addr *)
195 ndefinition load_from_source_at ≝
196 λt:memory_impl.λm:aux_mem_type t.λl:list byte8.λaddr:word16.
198 return λt.aux_mem_type t → list byte8 → word16 → aux_mem_type t
200 [ MEM_FUNC ⇒ mf_load_from_source_at
201 | MEM_TREE ⇒ mt_load_from_source_at
202 | MEM_BITS ⇒ mb_load_from_source_at
205 (* unificazione dell'impostazione della memoria: chk_update_ranged chk inf sup v *)
206 ndefinition check_update_ranged ≝
209 return λt.aux_chk_type t → word16 → word16 → memory_type → aux_chk_type t
211 [ MEM_FUNC ⇒ λc:aux_chk_type MEM_FUNC.
214 mf_check_update_ranged c inf sup v
215 | MEM_TREE ⇒ λc:aux_chk_type MEM_TREE.
218 mt_update_ranged memory_type c inf sup v
219 | MEM_BITS ⇒ λc:aux_chk_type MEM_BITS.
222 mt_update_ranged (Array8T memory_type) c inf sup (array_8T memory_type v v v v v v v v)
225 (* unificazione dell'impostazione dei bit: chk_update_bit chk addr sub v *)
226 (* NB: dove non esiste la granularita' del bit, lascio inalterato *)
227 ndefinition check_update_bit ≝
230 return λt.aux_chk_type t → word16 → oct → memory_type → aux_chk_type t
232 [ MEM_FUNC ⇒ λc:aux_chk_type MEM_FUNC.
237 | MEM_TREE ⇒ λc:aux_chk_type MEM_TREE.
242 | MEM_BITS ⇒ λc:aux_chk_type MEM_BITS.
246 mb_chk_update_bit c addr o v