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: Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
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 ndefinition memory_impl_ind : ΠP:memory_impl → Prop.P MEM_FUNC → P MEM_TREE → P MEM_BITS → Πm:memory_impl.P m ≝
38 λP:memory_impl → Prop.λp:P MEM_FUNC.λp1:P MEM_TREE.λp2:P MEM_BITS.λm:memory_impl.
39 match m with [ MEM_FUNC ⇒ p | MEM_TREE ⇒ p1 | MEM_BITS ⇒ p2 ].
41 ndefinition memory_impl_rec : ΠP:memory_impl → Set.P MEM_FUNC → P MEM_TREE → P MEM_BITS → Πm:memory_impl.P m ≝
42 λP:memory_impl → Set.λ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_rect : ΠP:memory_impl → Type.P MEM_FUNC → P MEM_TREE → P MEM_BITS → Πm:memory_impl.P m ≝
46 λP:memory_impl → Type.λ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 (* ausiliario per il tipo della memoria *)
50 ndefinition aux_mem_type ≝
51 λt:memory_impl.match t with
52 [ MEM_FUNC ⇒ word16 → byte8
53 | MEM_TREE ⇒ Array16T (Array16T (Array16T (Array16T byte8)))
54 | MEM_BITS ⇒ Array16T (Array16T (Array16T (Array16T (Array8T bool))))
57 (* ausiliario per il tipo del checker *)
58 ndefinition aux_chk_type ≝
59 λt:memory_impl.match t with
60 [ MEM_FUNC ⇒ word16 → memory_type
61 | MEM_TREE ⇒ Array16T (Array16T (Array16T (Array16T memory_type)))
62 | MEM_BITS ⇒ Array16T (Array16T (Array16T (Array16T (Array8T memory_type))))
65 (* unificazione di out_of_bound_memory *)
66 ndefinition out_of_bound_memory ≝
69 return λt.aux_chk_type t
71 [ MEM_FUNC ⇒ mf_out_of_bound_memory
72 | MEM_TREE ⇒ mt_out_of_bound_memory
73 | MEM_BITS ⇒ mb_out_of_bound_memory
76 (* unificazione di zero_memory *)
77 ndefinition zero_memory ≝
80 return λt.aux_mem_type t
82 [ MEM_FUNC ⇒ mf_zero_memory
83 | MEM_TREE ⇒ mt_zero_memory
84 | MEM_BITS ⇒ mb_zero_memory
87 (* unificazione della lettura senza chk: mem_read_abs mem addr *)
88 ndefinition mem_read_abs ≝
91 return λt.aux_mem_type t → word16 → byte8
93 [ MEM_FUNC ⇒ λm:aux_mem_type MEM_FUNC.
96 | MEM_TREE ⇒ λm:aux_mem_type MEM_TREE.
99 | MEM_BITS ⇒ λm:aux_mem_type MEM_BITS.
101 byte8_of_bits (mt_visit (Array8T bool) m addr)
104 (* unificazione del chk *)
105 ndefinition chk_get ≝
106 λt:memory_impl.λc:aux_chk_type t.λaddr:word16.
108 return λt.aux_chk_type t → word16 → Array8T memory_type
110 [ MEM_FUNC ⇒ mf_chk_get
111 | MEM_TREE ⇒ mt_chk_get
112 | MEM_BITS ⇒ mb_chk_get
115 (* unificazione della lettura con chk: mem_read mem chk addr *)
116 ndefinition mem_read ≝
117 λt:memory_impl.λm:aux_mem_type t.λc:aux_chk_type t.λaddr:word16.
119 return λt.aux_mem_type t → aux_chk_type t → word16 → option byte8
121 [ MEM_FUNC ⇒ mf_mem_read
122 | MEM_TREE ⇒ mt_mem_read
123 | MEM_BITS ⇒ mb_mem_read
126 (* unificazione della lettura di bit con chk: mem_read mem chk addr sub *)
127 ndefinition mem_read_bit ≝
130 return λt.aux_mem_type t → aux_chk_type t → word16 → oct → option bool
132 [ MEM_FUNC ⇒ λm:aux_mem_type MEM_FUNC.
133 λc:aux_chk_type MEM_FUNC.
136 opt_map ?? (mf_mem_read m c addr)
137 (λb.Some ? (getn_array8T o bool (bits_of_byte8 b)))
138 | MEM_TREE ⇒ λm:aux_mem_type MEM_TREE.
139 λc:aux_chk_type MEM_TREE.
142 opt_map ?? (mt_mem_read m c addr)
143 (λb.Some ? (getn_array8T o bool (bits_of_byte8 b)))
144 | MEM_BITS ⇒ λm:aux_mem_type MEM_BITS.
145 λc:aux_chk_type MEM_BITS.
148 mb_mem_read_bit m c addr o
151 (* unificazione della scrittura con chk: mem_update mem chk addr val *)
152 ndefinition mem_update ≝
153 λt:memory_impl.λm:aux_mem_type t.λc:aux_chk_type t.λaddr:word16.λv:byte8.
155 return λt.aux_mem_type t → Array8T memory_type → word16 → byte8 → option (aux_mem_type t)
157 [ MEM_FUNC ⇒ mf_mem_update
158 | MEM_TREE ⇒ mt_mem_update
159 | MEM_BITS ⇒ mb_mem_update
160 ] m (chk_get t c addr) addr v.
162 (* unificazione della scrittura di bit con chk: mem_update mem chk addr sub val *)
163 ndefinition mem_update_bit ≝
166 return λt.aux_mem_type t → aux_chk_type t → word16 → oct → bool → option (aux_mem_type t)
168 [ MEM_FUNC ⇒ λm:aux_mem_type MEM_FUNC.
169 λc:aux_chk_type MEM_FUNC.
173 opt_map ?? (mf_mem_read m c addr)
174 (λb.mf_mem_update m (chk_get MEM_FUNC c addr) addr (byte8_of_bits (setn_array8T o bool (bits_of_byte8 b) v)))
175 | MEM_TREE ⇒ λm:aux_mem_type MEM_TREE.
176 λc:aux_chk_type MEM_TREE.
180 opt_map ?? (mt_mem_read m c addr)
181 (λb.mt_mem_update m (chk_get MEM_TREE c addr) addr (byte8_of_bits (setn_array8T o bool (bits_of_byte8 b) v)))
182 | MEM_BITS ⇒ λm:aux_mem_type MEM_BITS.
183 λc:aux_chk_type MEM_BITS.
187 mb_mem_update_bit m c addr o v
190 (* unificazione del caricamento: load_from_source_at old_mem source addr *)
191 ndefinition load_from_source_at ≝
192 λt:memory_impl.λm:aux_mem_type t.λl:list byte8.λaddr:word16.
194 return λt.aux_mem_type t → list byte8 → word16 → aux_mem_type t
196 [ MEM_FUNC ⇒ mf_load_from_source_at
197 | MEM_TREE ⇒ mt_load_from_source_at
198 | MEM_BITS ⇒ mb_load_from_source_at
201 (* unificazione dell'impostazione della memoria: chk_update_ranged chk inf sup v *)
202 ndefinition check_update_ranged ≝
205 return λt.aux_chk_type t → word16 → word16 → memory_type → aux_chk_type t
207 [ MEM_FUNC ⇒ λc:aux_chk_type MEM_FUNC.
210 mf_check_update_ranged c inf sup v
211 | MEM_TREE ⇒ λc:aux_chk_type MEM_TREE.
214 mt_update_ranged memory_type c inf sup v
215 | MEM_BITS ⇒ λc:aux_chk_type MEM_BITS.
218 mt_update_ranged (Array8T memory_type) c inf sup (array_8T memory_type v v v v v v v v)
221 (* unificazione dell'impostazione dei bit: chk_update_bit chk addr sub v *)
222 (* NB: dove non esiste la granularita' del bit, lascio inalterato *)
223 ndefinition check_update_bit ≝
226 return λt.aux_chk_type t → word16 → oct → memory_type → aux_chk_type t
228 [ MEM_FUNC ⇒ λc:aux_chk_type MEM_FUNC.
233 | MEM_TREE ⇒ λc:aux_chk_type MEM_TREE.
238 | MEM_BITS ⇒ λc:aux_chk_type MEM_BITS.
242 mb_chk_update_bit c addr o v