helm/software/matita/contribs/ng_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 ninductive memory_impl : Type ≝
  37   MEM_FUNC: memory_impl
  38 | MEM_TREE: memory_impl
  39 | MEM_BITS: memory_impl.
  40
  41 ndefinition memory_impl_ind : ΠP:memory_impl → Prop.P MEM_FUNC → P MEM_TREE → P MEM_BITS → Πm:memory_impl.P m ≝
  42 λP:memory_impl → Prop.λ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 ].
  44
  45 ndefinition memory_impl_rec : ΠP:memory_impl → Set.P MEM_FUNC → P MEM_TREE → P MEM_BITS → Πm:memory_impl.P m ≝
  46 λP:memory_impl → Set.λ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 ].
  48
  49 ndefinition memory_impl_rect : ΠP:memory_impl → Type.P MEM_FUNC → P MEM_TREE → P MEM_BITS → Πm:memory_impl.P m ≝
  50 λP:memory_impl → Type.λp:P MEM_FUNC.λp1:P MEM_TREE.λp2:P MEM_BITS.λm:memory_impl.
  51  match m with [ MEM_FUNC ⇒ p | MEM_TREE ⇒ p1 | MEM_BITS ⇒ p2 ].
  52
  53 (* ausiliario per il tipo della memoria *)
  54 ndefinition aux_mem_type ≝
  55 λt:memory_impl.match t with
  56  [ MEM_FUNC ⇒ word16 → byte8
  57  | MEM_TREE ⇒ Array16T (Array16T (Array16T (Array16T byte8)))
  58  | MEM_BITS ⇒ Array16T (Array16T (Array16T (Array16T (Array8T bool))))
  59  ].
  60
  61 (* ausiliario per il tipo del checker *)
  62 ndefinition aux_chk_type ≝
  63 λt:memory_impl.match t with
  64  [ MEM_FUNC ⇒ word16 → memory_type
  65  | MEM_TREE ⇒ Array16T (Array16T (Array16T (Array16T memory_type)))
  66  | MEM_BITS ⇒ Array16T (Array16T (Array16T (Array16T (Array8T memory_type))))
  67  ].
  68
  69 (* unificazione di out_of_bound_memory *)
  70 ndefinition out_of_bound_memory ≝
  71 λt:memory_impl.
  72  match t
  73   return λt.aux_chk_type t
  74  with
  75   [ MEM_FUNC ⇒ mf_out_of_bound_memory
  76   | MEM_TREE ⇒ mt_out_of_bound_memory
  77   | MEM_BITS ⇒ mb_out_of_bound_memory
  78   ].
  79
  80 (* unificazione di zero_memory *)
  81 ndefinition zero_memory ≝
  82 λt:memory_impl.
  83  match t
  84   return λt.aux_mem_type t
  85  with
  86   [ MEM_FUNC ⇒ mf_zero_memory
  87   | MEM_TREE ⇒ mt_zero_memory
  88   | MEM_BITS ⇒ mb_zero_memory
  89   ].
  90
  91 (* unificazione della lettura senza chk: mem_read_abs mem addr *)
  92 ndefinition mem_read_abs ≝
  93 λt:memory_impl.
  94  match t
  95   return λt.aux_mem_type t → word16 → byte8
  96  with
  97   [ MEM_FUNC ⇒ λm:aux_mem_type MEM_FUNC.
  98                λaddr:word16.
  99                m addr
 100   | MEM_TREE ⇒ λm:aux_mem_type MEM_TREE.
 101                λaddr:word16.
 102                mt_visit byte8 m addr
 103   | MEM_BITS ⇒ λm:aux_mem_type MEM_BITS.
 104                λaddr:word16.
 105                byte8_of_bits (mt_visit (Array8T bool) m addr)
 106   ].
 107
 108 (* unificazione del chk *)
 109 ndefinition chk_get ≝
 110 λt:memory_impl.λc:aux_chk_type t.λaddr:word16.
 111  match t
 112   return λt.aux_chk_type t → word16 → Array8T memory_type
 113  with
 114   [ MEM_FUNC ⇒ mf_chk_get
 115   | MEM_TREE ⇒ mt_chk_get
 116   | MEM_BITS ⇒ mb_chk_get
 117   ] c addr.
 118
 119 (* unificazione della lettura con chk: mem_read mem chk addr *)
 120 ndefinition mem_read ≝
 121 λt:memory_impl.λm:aux_mem_type t.λc:aux_chk_type t.λaddr:word16.
 122  match t
 123   return λt.aux_mem_type t → aux_chk_type t → word16 → option byte8
 124  with
 125   [ MEM_FUNC ⇒ mf_mem_read
 126   | MEM_TREE ⇒ mt_mem_read
 127   | MEM_BITS ⇒ mb_mem_read
 128   ] m c addr.
 129
 130 (* unificazione della lettura di bit con chk: mem_read mem chk addr sub *)
 131 ndefinition mem_read_bit ≝
 132 λt:memory_impl.
 133  match t
 134   return λt.aux_mem_type t → aux_chk_type t → word16 → oct → option bool
 135  with
 136   [ MEM_FUNC ⇒ λm:aux_mem_type MEM_FUNC.
 137                λc:aux_chk_type MEM_FUNC.
 138                λaddr:word16.
 139                λo:oct.
 140                opt_map ?? (mf_mem_read m c addr)
 141                 (λb.Some ? (getn_array8T o bool (bits_of_byte8 b)))
 142   | MEM_TREE ⇒ λm:aux_mem_type MEM_TREE.
 143                λc:aux_chk_type MEM_TREE.
 144                λaddr:word16.
 145                λo:oct.
 146                opt_map ?? (mt_mem_read m c addr)
 147                 (λb.Some ? (getn_array8T o bool (bits_of_byte8 b)))
 148   | MEM_BITS ⇒ λm:aux_mem_type MEM_BITS.
 149                λc:aux_chk_type MEM_BITS.
 150                λaddr:word16.
 151                λo:oct.
 152                mb_mem_read_bit m c addr o
 153   ].
 154
 155 (* unificazione della scrittura con chk: mem_update mem chk addr val *)
 156 ndefinition mem_update ≝
 157 λt:memory_impl.λm:aux_mem_type t.λc:aux_chk_type t.λaddr:word16.λv:byte8.
 158  match t
 159   return λt.aux_mem_type t → Array8T memory_type → word16 → byte8 → option (aux_mem_type t)
 160  with
 161   [ MEM_FUNC ⇒ mf_mem_update
 162   | MEM_TREE ⇒ mt_mem_update
 163   | MEM_BITS ⇒ mb_mem_update
 164   ] m (chk_get t c addr) addr v.
 165
 166 (* unificazione della scrittura di bit con chk: mem_update mem chk addr sub val *)
 167 ndefinition mem_update_bit ≝
 168 λt:memory_impl.
 169  match t
 170   return λt.aux_mem_type t → aux_chk_type t → word16 → oct → bool → option (aux_mem_type t)
 171  with
 172   [ MEM_FUNC ⇒ λm:aux_mem_type MEM_FUNC.
 173                λc:aux_chk_type MEM_FUNC.
 174                λaddr:word16.
 175                λo:oct.
 176                λv:bool.
 177                opt_map ?? (mf_mem_read m c addr)
 178                 (λb.mf_mem_update m (chk_get MEM_FUNC c addr) addr (byte8_of_bits (setn_array8T o bool (bits_of_byte8 b) v)))
 179   | MEM_TREE ⇒ λm:aux_mem_type MEM_TREE.
 180                λc:aux_chk_type MEM_TREE.
 181                λaddr:word16.
 182                λo:oct.
 183                λv:bool.
 184                opt_map ?? (mt_mem_read m c addr)
 185                 (λb.mt_mem_update m (chk_get MEM_TREE c addr) addr (byte8_of_bits (setn_array8T o bool (bits_of_byte8 b) v)))
 186   | MEM_BITS ⇒ λm:aux_mem_type MEM_BITS.
 187                λc:aux_chk_type MEM_BITS.
 188                λaddr:word16.
 189                λo:oct.
 190                λv:bool.
 191                mb_mem_update_bit m c addr o v
 192   ].
 193
 194 (* unificazione del caricamento: load_from_source_at old_mem source addr *)
 195 ndefinition load_from_source_at ≝
 196 λt:memory_impl.λm:aux_mem_type t.λl:list byte8.λaddr:word16.
 197  match t
 198   return λt.aux_mem_type t → list byte8 → word16 → aux_mem_type t
 199  with
 200   [ MEM_FUNC ⇒ mf_load_from_source_at
 201   | MEM_TREE ⇒ mt_load_from_source_at
 202   | MEM_BITS ⇒ mb_load_from_source_at
 203   ] m l addr.
 204
 205 (* unificazione dell'impostazione della memoria: chk_update_ranged chk inf sup v *)
 206 ndefinition check_update_ranged ≝
 207 λt:memory_impl.
 208  match t
 209   return λt.aux_chk_type t → word16 → word16 → memory_type → aux_chk_type t
 210  with
 211   [ MEM_FUNC ⇒ λc:aux_chk_type MEM_FUNC.
 212                λinf,sup:word16.
 213                λv:memory_type.
 214                mf_check_update_ranged c inf sup v
 215   | MEM_TREE ⇒ λc:aux_chk_type MEM_TREE.
 216                λinf,sup:word16.
 217                λv:memory_type.
 218                mt_update_ranged memory_type c inf sup v
 219   | MEM_BITS ⇒ λc:aux_chk_type MEM_BITS.
 220                λinf,sup:word16.
 221                λv:memory_type.
 222                mt_update_ranged (Array8T memory_type) c inf sup (array_8T memory_type v v v v v v v v)
 223   ].
 224
 225 (* unificazione dell'impostazione dei bit: chk_update_bit chk addr sub v *)
 226 (* NB: dove non esiste la granularita' del bit, lascio inalterato *)
 227 ndefinition check_update_bit ≝
 228 λt:memory_impl.
 229  match t
 230   return λt.aux_chk_type t → word16 → oct → memory_type → aux_chk_type t
 231  with
 232   [ MEM_FUNC ⇒ λc:aux_chk_type MEM_FUNC.
 233                λaddr:word16.
 234                λo:oct.
 235                λv:memory_type.
 236                c
 237   | MEM_TREE ⇒ λc:aux_chk_type MEM_TREE.
 238                λaddr:word16.
 239                λo:oct.
 240                λv:memory_type.
 241                c
 242   | MEM_BITS ⇒ λc:aux_chk_type MEM_BITS.
 243                λaddr:word16.
 244                λo:oct.
 245                λv:memory_type.
 246                mb_chk_update_bit c addr o v
 247   ].