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_func.ma".
24 include "emulator/memory/memory_trees.ma".
25 include "emulator/memory/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 ⇒ word32 → byte8
41 | MEM_TREE ⇒ aux_32B_type byte8
42 | MEM_BITS ⇒ aux_32B_type (Array8T bool)
45 (* ausiliario per il tipo del checker *)
46 ndefinition aux_chk_type ≝
47 λt:memory_impl.match t with
48 [ MEM_FUNC ⇒ word32 → memory_type
49 | MEM_TREE ⇒ aux_32B_type memory_type
50 | MEM_BITS ⇒ aux_32B_type (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 → word32 → 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 ? m addr)
92 (* unificazione del chk *)
96 return λt.aux_chk_type t → word32 → Array8T memory_type
98 [ MEM_FUNC ⇒ λc:aux_chk_type MEM_FUNC.λaddr:word32.
100 [ MEM_READ_ONLY ⇒ mk_Array8T ? MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY
101 | MEM_READ_WRITE ⇒ mk_Array8T ? MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE
102 | MEM_OUT_OF_BOUND ⇒ mk_Array8T ? MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND
104 | MEM_TREE ⇒ λc:aux_chk_type MEM_TREE.λaddr:word32.
105 match mt_visit ? c addr with
106 [ MEM_READ_ONLY ⇒ mk_Array8T ? MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY
107 | MEM_READ_WRITE ⇒ mk_Array8T ? MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE
108 | MEM_OUT_OF_BOUND ⇒ mk_Array8T ? MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND
110 | MEM_BITS ⇒ λc:aux_chk_type MEM_BITS.λaddr:word32.
114 (* unificazione della lettura con chk: mem_read mem chk addr *)
115 ndefinition mem_read ≝
116 λt:memory_impl.λm:aux_mem_type t.λc:aux_chk_type t.λaddr:word32.
118 return λt.aux_mem_type t → aux_chk_type t → word32 → option byte8
120 [ MEM_FUNC ⇒ mf_mem_read
121 | MEM_TREE ⇒ mt_mem_read
122 | MEM_BITS ⇒ mb_mem_read
125 (* unificazione della lettura di bit con chk: mem_read mem chk addr sub *)
126 ndefinition mem_read_bit ≝
129 return λt.aux_mem_type t → aux_chk_type t → word32 → oct → option bool
131 [ MEM_FUNC ⇒ λm:aux_mem_type MEM_FUNC.
132 λc:aux_chk_type MEM_FUNC.
135 opt_map … (mf_mem_read m c addr)
136 (λb.Some ? (getn_array8T o bool (bits_of_byte8 b)))
137 | MEM_TREE ⇒ λm:aux_mem_type MEM_TREE.
138 λc:aux_chk_type MEM_TREE.
141 opt_map … (mt_mem_read m c addr)
142 (λb.Some ? (getn_array8T o bool (bits_of_byte8 b)))
143 | MEM_BITS ⇒ λm:aux_mem_type MEM_BITS.
144 λc:aux_chk_type MEM_BITS.
147 mb_mem_read_bit m c addr o
150 (* unificazione della scrittura con chk: mem_update mem chk addr val *)
151 ndefinition mem_update ≝
152 λt:memory_impl.λm:aux_mem_type t.λc:aux_chk_type t.λaddr:word32.λv:byte8.
154 return λt.aux_mem_type t → aux_chk_type t → word32 → byte8 → option (aux_mem_type t)
156 [ MEM_FUNC ⇒ mf_mem_update
157 | MEM_TREE ⇒ mt_mem_update
158 | MEM_BITS ⇒ mb_mem_update
161 (* unificazione della scrittura di bit con chk: mem_update mem chk addr sub val *)
162 ndefinition mem_update_bit ≝
165 return λt.aux_mem_type t → aux_chk_type t → word32 → oct → bool → option (aux_mem_type t)
167 [ MEM_FUNC ⇒ λm:aux_mem_type MEM_FUNC.
168 λc:aux_chk_type MEM_FUNC.
172 mf_mem_update m c addr (byte8_of_bits (setn_array8T o bool (bits_of_byte8 (m addr)) v))
173 | MEM_TREE ⇒ λm:aux_mem_type MEM_TREE.
174 λc:aux_chk_type MEM_TREE.
178 mt_mem_update m c addr (byte8_of_bits (setn_array8T o bool (bits_of_byte8 (mt_visit ? m addr)) v))
179 | MEM_BITS ⇒ λm:aux_mem_type MEM_BITS.
180 λc:aux_chk_type MEM_BITS.
184 mb_mem_update_bit m c addr o v
187 (* unificazione del caricamento: load_from_source_at old_mem source addr *)
188 ndefinition load_from_source_at ≝
189 λt:memory_impl.λm:aux_mem_type t.λl:list byte8.λaddr:word32.
191 return λt.aux_mem_type t → list byte8 → word32 → aux_mem_type t
193 [ MEM_FUNC ⇒ mf_load_from_source_at
194 | MEM_TREE ⇒ mt_load_from_source_at
195 | MEM_BITS ⇒ mb_load_from_source_at
198 (* unificazione dell'impostazione della memoria: chk_update_ranged chk inf sup v *)
199 ndefinition check_update_ranged ≝
202 return λt.aux_chk_type t → word32 → word16 → memory_type → aux_chk_type t
204 [ MEM_FUNC ⇒ λc:aux_chk_type MEM_FUNC.
208 mf_check_update_ranged c addr range v
209 | MEM_TREE ⇒ λc:aux_chk_type MEM_TREE.
213 mt_update_ranged ? c addr ? (w16_to_recw16 range) v
214 | MEM_BITS ⇒ λc:aux_chk_type MEM_BITS.
218 mt_update_ranged ? c addr ? (w16_to_recw16 range) (mk_Array8T ? 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 → word32 → 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