helm/software/matita/contribs/ng_assembly/emulator/memory/memory_abs.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* ********************************************************************** *)
  16 (*                          Progetto FreeScale                            *)
  17 (*                                                                        *)
  18 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
  19 (*   Sviluppo: 2008-2010                                                  *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "emulator/memory/memory_func.ma".
  24 include "emulator/memory/memory_trees.ma".
  25 include "emulator/memory/memory_bits.ma".
  26
  27 (* ********************************************* *)
  28 (* ASTRAZIONE DALL'IMPLEMENTAZIONE DELLA MEMORIA *)
  29 (* ********************************************* *)
  30
  31 (* tipi di implementazione della memoria *)
  32 ninductive memory_impl : Type ≝
  33   MEM_FUNC: memory_impl
  34 | MEM_TREE: memory_impl
  35 | MEM_BITS: memory_impl.
  36
  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)
  43  ].
  44
  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)
  51  ].
  52
  53 (* unificazione di out_of_bound_memory *)
  54 ndefinition out_of_bound_memory ≝
  55 λt:memory_impl.
  56  match t
  57   return λt.aux_chk_type t
  58  with
  59   [ MEM_FUNC ⇒ mf_out_of_bound_memory
  60   | MEM_TREE ⇒ mt_out_of_bound_memory
  61   | MEM_BITS ⇒ mb_out_of_bound_memory
  62   ].
  63
  64 (* unificazione di zero_memory *)
  65 ndefinition zero_memory ≝
  66 λt:memory_impl.
  67  match t
  68   return λt.aux_mem_type t
  69  with
  70   [ MEM_FUNC ⇒ mf_zero_memory
  71   | MEM_TREE ⇒ mt_zero_memory
  72   | MEM_BITS ⇒ mb_zero_memory
  73   ].
  74
  75 (* unificazione della lettura senza chk: mem_read_abs mem addr *)
  76 ndefinition mem_read_abs ≝
  77 λt:memory_impl.
  78  match t
  79   return λt.aux_mem_type t → word32 → byte8
  80  with
  81   [ MEM_FUNC ⇒ λm:aux_mem_type MEM_FUNC.
  82                λaddr:word32.
  83                m addr
  84   | MEM_TREE ⇒ λm:aux_mem_type MEM_TREE.
  85                λaddr:word32.
  86                mt_visit ? m addr
  87   | MEM_BITS ⇒ λm:aux_mem_type MEM_BITS.
  88                λaddr:word32.
  89                byte8_of_bits (mt_visit ? m addr)
  90   ].
  91
  92 (* unificazione del chk *)
  93 ndefinition chk_get ≝
  94 λt:memory_impl.
  95  match t
  96   return λt.aux_chk_type t → word32 → Array8T memory_type
  97  with
  98   [ MEM_FUNC ⇒ λc:aux_chk_type MEM_FUNC.λaddr:word32.
  99    match c addr with
 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
 103     ]
 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
 109     ]
 110   | MEM_BITS ⇒ λc:aux_chk_type MEM_BITS.λaddr:word32.
 111    mt_visit ? c addr
 112   ].
 113
 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.
 117  match t
 118   return λt.aux_mem_type t → aux_chk_type t → word32 → option byte8
 119  with
 120   [ MEM_FUNC ⇒ mf_mem_read
 121   | MEM_TREE ⇒ mt_mem_read
 122   | MEM_BITS ⇒ mb_mem_read
 123   ] m c addr.
 124
 125 (* unificazione della lettura di bit con chk: mem_read mem chk addr sub *)
 126 ndefinition mem_read_bit ≝
 127 λt:memory_impl.
 128  match t
 129   return λt.aux_mem_type t → aux_chk_type t → word32 → oct → option bool
 130  with
 131   [ MEM_FUNC ⇒ λm:aux_mem_type MEM_FUNC.
 132                λc:aux_chk_type MEM_FUNC.
 133                λaddr:word32.
 134                λo:oct.
 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.
 139                λaddr:word32.
 140                λo:oct.
 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.
 145                λaddr:word32.
 146                λo:oct.
 147                mb_mem_read_bit m c addr o
 148   ].
 149
 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.
 153  match t
 154   return λt.aux_mem_type t → aux_chk_type t → word32 → byte8 → option (aux_mem_type t)
 155  with
 156   [ MEM_FUNC ⇒ mf_mem_update
 157   | MEM_TREE ⇒ mt_mem_update
 158   | MEM_BITS ⇒ mb_mem_update
 159   ] m c addr v.
 160
 161 (* unificazione della scrittura di bit con chk: mem_update mem chk addr sub val *)
 162 ndefinition mem_update_bit ≝
 163 λt:memory_impl.
 164  match t
 165   return λt.aux_mem_type t → aux_chk_type t → word32 → oct → bool → option (aux_mem_type t)
 166  with
 167   [ MEM_FUNC ⇒ λm:aux_mem_type MEM_FUNC.
 168                λc:aux_chk_type MEM_FUNC.
 169                λaddr:word32.
 170                λo:oct.
 171                λv:bool.
 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.
 175                λaddr:word32.
 176                λo:oct.
 177                λv:bool.
 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.
 181                λaddr:word32.
 182                λo:oct.
 183                λv:bool.
 184                mb_mem_update_bit m c addr o v
 185   ].
 186
 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.
 190  match t
 191   return λt.aux_mem_type t → list byte8 → word32 → aux_mem_type t
 192  with
 193   [ MEM_FUNC ⇒ mf_load_from_source_at
 194   | MEM_TREE ⇒ mt_load_from_source_at
 195   | MEM_BITS ⇒ mb_load_from_source_at
 196   ] m l addr.
 197
 198 (* unificazione dell'impostazione della memoria: chk_update_ranged chk inf sup v *)
 199 ndefinition check_update_ranged ≝
 200 λt:memory_impl.
 201  match t
 202   return λt.aux_chk_type t → word32 → word16 → memory_type → aux_chk_type t
 203  with
 204   [ MEM_FUNC ⇒ λc:aux_chk_type MEM_FUNC.
 205                λaddr:word32.
 206                λrange:word16.
 207                λv:memory_type.
 208                mf_check_update_ranged c addr range v
 209   | MEM_TREE ⇒ λc:aux_chk_type MEM_TREE.
 210                λaddr:word32.
 211                λrange:word16.
 212                λv:memory_type.
 213                mt_update_ranged ? c addr ? (w16_to_recw16 range) v
 214   | MEM_BITS ⇒ λc:aux_chk_type MEM_BITS.
 215                λaddr:word32.
 216                λrange:word16.
 217                λv:memory_type.
 218                mt_update_ranged ? c addr ? (w16_to_recw16 range) (mk_Array8T ? v v v v v v v v)
 219   ].
 220
 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 ≝
 224 λt:memory_impl.
 225  match t
 226   return λt.aux_chk_type t → word32 → oct → memory_type → aux_chk_type t
 227  with
 228   [ MEM_FUNC ⇒ λc:aux_chk_type MEM_FUNC.
 229                λaddr:word32.
 230                λo:oct.
 231                λv:memory_type.
 232                c
 233   | MEM_TREE ⇒ λc:aux_chk_type MEM_TREE.
 234                λaddr:word32.
 235                λo:oct.
 236                λv:memory_type.
 237                c
 238   | MEM_BITS ⇒ λc:aux_chk_type MEM_BITS.
 239                λaddr:word32.
 240                λo:oct.
 241                λv:memory_type.
 242                mb_chk_update_bit c addr o v
 243   ].