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_func.ma".
24 include "freescale/memory_trees.ma".
25 include "freescale/memory_bits.ma".
27 (* ********************************************* *)
28 (* ASTRAZIONE DALL'IMPLEMENTAZIONE DELLA MEMORIA *)
29 (* ********************************************* *)
31 (* tipi di implementazione della memoria *)
32 ninductive memory_impl : Type ≝
34 | MEM_TREE: memory_impl
35 | MEM_BITS: memory_impl.
37 (* ausiliario per il tipo della memoria *)
38 ndefinition aux_mem_type ≝
39 λt:memory_impl.match t with
40 [ MEM_FUNC ⇒ word16 → byte8
41 | MEM_TREE ⇒ Array16T (Array16T (Array16T (Array16T byte8)))
42 | MEM_BITS ⇒ Array16T (Array16T (Array16T (Array16T (Array8T bool))))
45 (* ausiliario per il tipo del checker *)
46 ndefinition aux_chk_type ≝
47 λt:memory_impl.match t with
48 [ MEM_FUNC ⇒ word16 → memory_type
49 | MEM_TREE ⇒ Array16T (Array16T (Array16T (Array16T memory_type)))
50 | MEM_BITS ⇒ Array16T (Array16T (Array16T (Array16T (Array8T memory_type))))
53 (* unificazione di out_of_bound_memory *)
54 ndefinition out_of_bound_memory ≝
57 return λt.aux_chk_type t
59 [ MEM_FUNC ⇒ mf_out_of_bound_memory
60 | MEM_TREE ⇒ mt_out_of_bound_memory
61 | MEM_BITS ⇒ mb_out_of_bound_memory
64 (* unificazione di zero_memory *)
65 ndefinition zero_memory ≝
68 return λt.aux_mem_type t
70 [ MEM_FUNC ⇒ mf_zero_memory
71 | MEM_TREE ⇒ mt_zero_memory
72 | MEM_BITS ⇒ mb_zero_memory
75 (* unificazione della lettura senza chk: mem_read_abs mem addr *)
76 ndefinition mem_read_abs ≝
79 return λt.aux_mem_type t → word16 → byte8
81 [ MEM_FUNC ⇒ λm:aux_mem_type MEM_FUNC.
84 | MEM_TREE ⇒ λm:aux_mem_type MEM_TREE.
87 | MEM_BITS ⇒ λm:aux_mem_type MEM_BITS.
89 byte8_of_bits (mt_visit (Array8T bool) m addr)
92 (* unificazione del chk *)
94 λt:memory_impl.λc:aux_chk_type t.λaddr:word16.
96 return λt.aux_chk_type t → word16 → Array8T memory_type
98 [ MEM_FUNC ⇒ mf_chk_get
99 | MEM_TREE ⇒ mt_chk_get
100 | MEM_BITS ⇒ mb_chk_get
103 (* unificazione della lettura con chk: mem_read mem chk addr *)
104 ndefinition mem_read ≝
105 λt:memory_impl.λm:aux_mem_type t.λc:aux_chk_type t.λaddr:word16.
107 return λt.aux_mem_type t → aux_chk_type t → word16 → option byte8
109 [ MEM_FUNC ⇒ mf_mem_read
110 | MEM_TREE ⇒ mt_mem_read
111 | MEM_BITS ⇒ mb_mem_read
114 (* unificazione della lettura di bit con chk: mem_read mem chk addr sub *)
115 ndefinition mem_read_bit ≝
118 return λt.aux_mem_type t → aux_chk_type t → word16 → oct → option bool
120 [ MEM_FUNC ⇒ λm:aux_mem_type MEM_FUNC.
121 λc:aux_chk_type MEM_FUNC.
124 opt_map … (mf_mem_read m c addr)
125 (λb.Some ? (getn_array8T o bool (bits_of_byte8 b)))
126 | MEM_TREE ⇒ λm:aux_mem_type MEM_TREE.
127 λc:aux_chk_type MEM_TREE.
130 opt_map … (mt_mem_read m c addr)
131 (λb.Some ? (getn_array8T o bool (bits_of_byte8 b)))
132 | MEM_BITS ⇒ λm:aux_mem_type MEM_BITS.
133 λc:aux_chk_type MEM_BITS.
136 mb_mem_read_bit m c addr o
139 (* unificazione della scrittura con chk: mem_update mem chk addr val *)
140 ndefinition mem_update ≝
141 λt:memory_impl.λm:aux_mem_type t.λc:aux_chk_type t.λaddr:word16.λv:byte8.
143 return λt.aux_mem_type t → Array8T memory_type → word16 → byte8 → option (aux_mem_type t)
145 [ MEM_FUNC ⇒ mf_mem_update
146 | MEM_TREE ⇒ mt_mem_update
147 | MEM_BITS ⇒ mb_mem_update
148 ] m (chk_get t c addr) addr v.
150 (* unificazione della scrittura di bit con chk: mem_update mem chk addr sub val *)
151 ndefinition mem_update_bit ≝
154 return λt.aux_mem_type t → aux_chk_type t → word16 → oct → bool → option (aux_mem_type t)
156 [ MEM_FUNC ⇒ λm:aux_mem_type MEM_FUNC.
157 λc:aux_chk_type MEM_FUNC.
161 opt_map … (mf_mem_read m c addr)
162 (λb.mf_mem_update m (chk_get MEM_FUNC c addr) addr (byte8_of_bits (setn_array8T o bool (bits_of_byte8 b) v)))
163 | MEM_TREE ⇒ λm:aux_mem_type MEM_TREE.
164 λc:aux_chk_type MEM_TREE.
168 opt_map … (mt_mem_read m c addr)
169 (λb.mt_mem_update m (chk_get MEM_TREE c addr) addr (byte8_of_bits (setn_array8T o bool (bits_of_byte8 b) v)))
170 | MEM_BITS ⇒ λm:aux_mem_type MEM_BITS.
171 λc:aux_chk_type MEM_BITS.
175 mb_mem_update_bit m c addr o v
178 (* unificazione del caricamento: load_from_source_at old_mem source addr *)
179 ndefinition load_from_source_at ≝
180 λt:memory_impl.λm:aux_mem_type t.λl:list byte8.λaddr:word16.
182 return λt.aux_mem_type t → list byte8 → word16 → aux_mem_type t
184 [ MEM_FUNC ⇒ mf_load_from_source_at
185 | MEM_TREE ⇒ mt_load_from_source_at
186 | MEM_BITS ⇒ mb_load_from_source_at
189 (* unificazione dell'impostazione della memoria: chk_update_ranged chk inf sup v *)
190 ndefinition check_update_ranged ≝
193 return λt.aux_chk_type t → word16 → word16 → memory_type → aux_chk_type t
195 [ MEM_FUNC ⇒ λc:aux_chk_type MEM_FUNC.
198 mf_check_update_ranged c inf sup v
199 | MEM_TREE ⇒ λc:aux_chk_type MEM_TREE.
202 mt_update_ranged memory_type c inf sup v
203 | MEM_BITS ⇒ λc:aux_chk_type MEM_BITS.
206 mt_update_ranged (Array8T memory_type) c inf sup (array_8T memory_type v v v v v v v v)
209 (* unificazione dell'impostazione dei bit: chk_update_bit chk addr sub v *)
210 (* NB: dove non esiste la granularita' del bit, lascio inalterato *)
211 ndefinition check_update_bit ≝
214 return λt.aux_chk_type t → word16 → oct → memory_type → aux_chk_type t
216 [ MEM_FUNC ⇒ λc:aux_chk_type MEM_FUNC.
221 | MEM_TREE ⇒ λc:aux_chk_type MEM_TREE.
226 | MEM_BITS ⇒ λc:aux_chk_type MEM_BITS.
230 mb_chk_update_bit c addr o v