matita/matita/contribs/assembly/freescale/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:                                                         *)
  19 (*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
  20 (*                                                                        *)
  21 (* Questo materiale fa parte della tesi:                                  *)
  22 (*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
  23 (*                                                                        *)
  24 (*                    data ultima modifica 15/11/2007                     *)
  25 (* ********************************************************************** *)
  26
  27 include "freescale/memory_func.ma".
  28 include "freescale/memory_trees.ma".
  29 include "freescale/memory_bits.ma".
  30
  31 (* ********************************************* *)
  32 (* ASTRAZIONE DALL'IMPLEMENTAZIONE DELLA MEMORIA *)
  33 (* ********************************************* *)
  34
  35 (* tipi di implementazione della memoria *)
  36 inductive memory_impl : Type ≝
  37   MEM_FUNC: memory_impl
  38 | MEM_TREE: memory_impl
  39 | MEM_BITS: memory_impl.
  40
  41 (* ausiliario per il tipo della memoria *)
  42 definition aux_mem_type ≝
  43 λt:memory_impl.match t with
  44  [ MEM_FUNC ⇒ word16 → byte8
  45  | MEM_TREE ⇒ Prod16T (Prod16T (Prod16T (Prod16T byte8)))
  46  | MEM_BITS ⇒ Prod16T (Prod16T (Prod16T (Prod16T (Prod8T bool))))
  47  ].
  48
  49 (* ausiliario per il tipo del checker *)
  50 definition aux_chk_type ≝
  51 λt:memory_impl.match t with
  52  [ MEM_FUNC ⇒ word16 → memory_type
  53  | MEM_TREE ⇒ Prod16T (Prod16T (Prod16T (Prod16T memory_type)))
  54  | MEM_BITS ⇒ Prod16T (Prod16T (Prod16T (Prod16T (Prod8T memory_type))))
  55  ].
  56
  57 (* unificazione di out_of_bound_memory *)
  58 definition out_of_bound_memory ≝
  59 λt:memory_impl.
  60  match t
  61   return λt.aux_chk_type t
  62  with
  63   [ MEM_FUNC ⇒ mf_out_of_bound_memory
  64   | MEM_TREE ⇒ mt_out_of_bound_memory
  65   | MEM_BITS ⇒ mb_out_of_bound_memory
  66   ].
  67
  68 (* unificazione di zero_memory *)
  69 definition zero_memory ≝
  70 λt:memory_impl.
  71  match t
  72   return λt.aux_mem_type t
  73  with
  74   [ MEM_FUNC ⇒ mf_zero_memory
  75   | MEM_TREE ⇒ mt_zero_memory
  76   | MEM_BITS ⇒ mb_zero_memory
  77   ].
  78
  79 (* unificazione della lettura senza chk: mem_read_abs mem addr *)
  80 definition mem_read_abs ≝
  81 λt:memory_impl.
  82  match t
  83   return λt.aux_mem_type t → word16 → byte8
  84  with
  85   [ MEM_FUNC ⇒ λm:aux_mem_type MEM_FUNC.
  86                λaddr:word16.
  87                m addr
  88   | MEM_TREE ⇒ λm:aux_mem_type MEM_TREE.
  89                λaddr:word16.
  90                mt_visit byte8 m addr
  91   | MEM_BITS ⇒ λm:aux_mem_type MEM_BITS.
  92                λaddr:word16.
  93                byte8_of_bits (mt_visit (Prod8T bool) m addr)
  94   ].
  95
  96 (* unificazione del chk *)
  97 definition chk_get ≝
  98 λt:memory_impl.λc:aux_chk_type t.λaddr:word16.
  99  match t
 100   return λt.aux_chk_type t → word16 → Prod8T memory_type
 101  with
 102   [ MEM_FUNC ⇒ mf_chk_get
 103   | MEM_TREE ⇒ mt_chk_get
 104   | MEM_BITS ⇒ mb_chk_get
 105   ] c addr.
 106
 107 (* unificazione della lettura con chk: mem_read mem chk addr *)
 108 definition mem_read ≝
 109 λt:memory_impl.λm:aux_mem_type t.λc:aux_chk_type t.λaddr:word16.
 110  match t
 111   return λt.aux_mem_type t → aux_chk_type t → word16 → option byte8
 112  with
 113   [ MEM_FUNC ⇒ mf_mem_read
 114   | MEM_TREE ⇒ mt_mem_read
 115   | MEM_BITS ⇒ mb_mem_read
 116   ] m c addr.
 117
 118 (* unificazione della lettura di bit con chk: mem_read mem chk addr sub *)
 119 definition mem_read_bit ≝
 120 λt:memory_impl.
 121  match t
 122   return λt.aux_mem_type t → aux_chk_type t → word16 → oct → option bool
 123  with
 124   [ MEM_FUNC ⇒ λm:aux_mem_type MEM_FUNC.
 125                λc:aux_chk_type MEM_FUNC.
 126                λaddr:word16.
 127                λo:oct.
 128                opt_map ?? (mf_mem_read m c addr)
 129                 (λb.Some ? (getn_array8T o bool (bits_of_byte8 b)))
 130   | MEM_TREE ⇒ λm:aux_mem_type MEM_TREE.
 131                λc:aux_chk_type MEM_TREE.
 132                λaddr:word16.
 133                λo:oct.
 134                opt_map ?? (mt_mem_read m c addr)
 135                 (λb.Some ? (getn_array8T o bool (bits_of_byte8 b)))
 136   | MEM_BITS ⇒ λm:aux_mem_type MEM_BITS.
 137                λc:aux_chk_type MEM_BITS.
 138                λaddr:word16.
 139                λo:oct.
 140                mb_mem_read_bit m c addr o
 141   ].
 142
 143 (* unificazione della scrittura con chk: mem_update mem chk addr val *)
 144 definition mem_update ≝
 145 λt:memory_impl.λm:aux_mem_type t.λc:aux_chk_type t.λaddr:word16.λv:byte8.
 146  match t
 147   return λt.aux_mem_type t → Prod8T memory_type → word16 → byte8 → option (aux_mem_type t)
 148  with
 149   [ MEM_FUNC ⇒ mf_mem_update
 150   | MEM_TREE ⇒ mt_mem_update
 151   | MEM_BITS ⇒ mb_mem_update
 152   ] m (chk_get t c addr) addr v.
 153
 154 (* unificazione della scrittura di bit con chk: mem_update mem chk addr sub val *)
 155 definition mem_update_bit ≝
 156 λt:memory_impl.
 157  match t
 158   return λt.aux_mem_type t → aux_chk_type t → word16 → oct → bool → option (aux_mem_type t)
 159  with
 160   [ MEM_FUNC ⇒ λm:aux_mem_type MEM_FUNC.
 161                λc:aux_chk_type MEM_FUNC.
 162                λaddr:word16.
 163                λo:oct.
 164                λv:bool.
 165                opt_map ?? (mf_mem_read m c addr)
 166                 (λb.mf_mem_update m (chk_get MEM_FUNC c addr) addr (byte8_of_bits (setn_array8T o bool (bits_of_byte8 b) v)))
 167   | MEM_TREE ⇒ λm:aux_mem_type MEM_TREE.
 168                λc:aux_chk_type MEM_TREE.
 169                λaddr:word16.
 170                λo:oct.
 171                λv:bool.
 172                opt_map ?? (mt_mem_read m c addr)
 173                 (λb.mt_mem_update m (chk_get MEM_TREE c addr) addr (byte8_of_bits (setn_array8T o bool (bits_of_byte8 b) v)))
 174   | MEM_BITS ⇒ λm:aux_mem_type MEM_BITS.
 175                λc:aux_chk_type MEM_BITS.
 176                λaddr:word16.
 177                λo:oct.
 178                λv:bool.
 179                mb_mem_update_bit m c addr o v
 180   ].
 181
 182 (* unificazione del caricamento: load_from_source_at old_mem source addr *)
 183 definition load_from_source_at ≝
 184 λt:memory_impl.λm:aux_mem_type t.λl:list byte8.λaddr:word16.
 185  match t
 186   return λt.aux_mem_type t → list byte8 → word16 → aux_mem_type t
 187  with
 188   [ MEM_FUNC ⇒ mf_load_from_source_at
 189   | MEM_TREE ⇒ mt_load_from_source_at
 190   | MEM_BITS ⇒ mb_load_from_source_at
 191   ] m l addr.
 192
 193 (* unificazione dell'impostazione della memoria: chk_update_ranged chk inf sup v *)
 194 definition check_update_ranged ≝
 195 λt:memory_impl.
 196  match t
 197   return λt.aux_chk_type t → word16 → word16 → memory_type → aux_chk_type t
 198  with
 199   [ MEM_FUNC ⇒ λc:aux_chk_type MEM_FUNC.
 200                λinf,sup:word16.
 201                λv:memory_type.
 202                mf_check_update_ranged c inf sup v
 203   | MEM_TREE ⇒ λc:aux_chk_type MEM_TREE.
 204                λinf,sup:word16.
 205                λv:memory_type.
 206                mt_update_ranged memory_type c inf sup v
 207   | MEM_BITS ⇒ λc:aux_chk_type MEM_BITS.
 208                λinf,sup:word16.
 209                λv:memory_type.
 210                mt_update_ranged (Prod8T memory_type) c inf sup (array_8T memory_type v v v v v v v v)
 211   ].
 212
 213 (* unificazione dell'impostazione dei bit: chk_update_bit chk addr sub v *)
 214 (* NB: dove non esiste la granularita' del bit, lascio inalterato *)
 215 definition check_update_bit ≝
 216 λt:memory_impl.
 217  match t
 218   return λt.aux_chk_type t → word16 → oct → memory_type → aux_chk_type t
 219  with
 220   [ MEM_FUNC ⇒ λc:aux_chk_type MEM_FUNC.
 221                λaddr:word16.
 222                λo:oct.
 223                λv:memory_type.
 224                c
 225   | MEM_TREE ⇒ λc:aux_chk_type MEM_TREE.
 226                λaddr:word16.
 227                λo:oct.
 228                λv:memory_type.
 229                c
 230   | MEM_BITS ⇒ λc:aux_chk_type MEM_BITS.
 231                λaddr:word16.
 232                λo:oct.
 233                λv:memory_type.
 234                mb_chk_update_bit c addr o v
 235   ].