helm/software/matita/contribs/ng_assembly/freescale/memory_trees.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_struct.ma".
  28 include "freescale/word16.ma".
  29 include "freescale/option.ma".
  30 include "freescale/theory.ma".
  31
  32 (* ********************* *)
  33 (* MEMORIA E DESCRITTORE *)
  34 (* ********************* *)
  35
  36 (* tutta la memoria non installata *)
  37 ndefinition mt_out_of_bound_memory ≝
  38 let lev4 ≝ array_16T ?
  39            MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND
  40            MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND
  41            MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND
  42            MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND
  43            in
  44 let lev3 ≝ array_16T ?
  45            lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4
  46            lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4
  47            in
  48 let lev2 ≝ array_16T ?
  49            lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3
  50            lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3
  51            in
  52 let lev1 ≝ array_16T ?
  53            lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2
  54            lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2
  55            in
  56 lev1.
  57
  58 (* tutta la memoria a 0 *)
  59 ndefinition mt_zero_memory ≝
  60 let lev4 ≝ array_16T ?
  61            (mk_byte8 x0 x0) (mk_byte8 x0 x0) (mk_byte8 x0 x0) (mk_byte8 x0 x0)
  62            (mk_byte8 x0 x0) (mk_byte8 x0 x0) (mk_byte8 x0 x0) (mk_byte8 x0 x0)
  63            (mk_byte8 x0 x0) (mk_byte8 x0 x0) (mk_byte8 x0 x0) (mk_byte8 x0 x0)
  64            (mk_byte8 x0 x0) (mk_byte8 x0 x0) (mk_byte8 x0 x0) (mk_byte8 x0 x0)
  65            in
  66 let lev3 ≝ array_16T ?
  67            lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4
  68            lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4
  69            in
  70 let lev2 ≝ array_16T ?
  71            lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3
  72            lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3
  73            in
  74 let lev1 ≝ array_16T ?
  75            lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2
  76            lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2
  77            in
  78 lev1.
  79
  80 (* visita di un albero da 64KB di elementi: ln16(65536)=4 passaggi *)
  81 ndefinition mt_visit ≝
  82 λT:Type.λdata:Array16T (Array16T (Array16T (Array16T T))).λaddr:word16.
  83  match addr with
  84   [ mk_word16 wh wl ⇒
  85  getn_array16T (b8l wl) ?
  86   (getn_array16T (b8h wl) ?
  87    (getn_array16T (b8l wh) ?
  88     (getn_array16T (b8h wh) ? data))) ].
  89
  90 (* scrittura di un elemento in un albero da 64KB *)
  91 ndefinition mt_update ≝
  92 λT:Type.λdata:Array16T (Array16T (Array16T (Array16T T))).λaddr:word16.λv:T.
  93  match addr with
  94   [ mk_word16 wh wl ⇒
  95  let lev2 ≝ getn_array16T (b8h wh) ? data in
  96  let lev3 ≝ getn_array16T (b8l wh) ? lev2 in
  97  let lev4 ≝ getn_array16T (b8h wl) ? lev3 in
  98  setn_array16T (b8h wh) ? data
  99   (setn_array16T (b8l wh) ? lev2
 100    (setn_array16T (b8h wl) ? lev3
 101     (setn_array16T (b8l wl) T lev4 v))) ].
 102
 103 (* scrittura di un range in un albero da 64KB *)
 104 ndefinition mt_update_ranged ≝
 105 λT:Type.λdata:Array16T (Array16T (Array16T (Array16T T))).λi,s:word16.λv:T.
 106  (* ok i≤s *)
 107  match le_w16 i s with
 108   [ true ⇒
 109  match i with
 110   [ mk_word16 ih il ⇒
 111  match s with
 112   [ mk_word16 sh sl ⇒
 113  let aux_4 ≝ Array16T T in
 114  let aux_3 ≝ Array16T (Array16T T) in
 115  let aux_2 ≝ Array16T (Array16T (Array16T T)) in
 116
 117  let ilev2 ≝ getn_array16T (b8h ih) aux_2 data in
 118  let ilev3 ≝ getn_array16T (b8l ih) aux_3 ilev2 in
 119  let ilev4 ≝ getn_array16T (b8h il) aux_4 ilev3 in
 120
 121  let slev2 ≝ getn_array16T (b8h sh) aux_2 data in
 122  let slev3 ≝ getn_array16T (b8l sh) aux_3 slev2 in
 123  let slev4 ≝ getn_array16T (b8h sl) aux_4 slev3 in
 124
 125  let vlev4 ≝ array_16T T v v v v v v v v v v v v v v v v in
 126  let vlev3 ≝ array_16T aux_4 vlev4 vlev4 vlev4 vlev4 vlev4 vlev4 vlev4 vlev4
 127                              vlev4 vlev4 vlev4 vlev4 vlev4 vlev4 vlev4 vlev4 in
 128  let vlev2 ≝ array_16T aux_3 vlev3 vlev3 vlev3 vlev3 vlev3 vlev3 vlev3 vlev3
 129                              vlev3 vlev3 vlev3 vlev3 vlev3 vlev3 vlev3 vlev3 in
 130
 131  match eq_ex (b8h ih) (b8h sh) with
 132   [ true ⇒ match eq_ex (b8l ih) (b8l sh) with
 133    [ true ⇒ match eq_ex (b8h il) (b8h sl) with
 134     (* caso 0x...(X) a 0x...(Y) *)
 135     [ true ⇒ setn_array16T (b8h ih) aux_2 data
 136               (setn_array16T (b8l ih) aux_3 ilev2
 137                (setn_array16T (b8h il) aux_4 ilev3
 138                 (* cambio a partire da livello 4 *)
 139                 (setmn_array16T (b8l il) (b8l sl) T ilev4 v))) (* ...X,...Y *)
 140     (* caso 0x..(X1)(X2) a 0x..(Y1)(Y2) *)
 141     | false ⇒ setn_array16T (b8h ih) aux_2 data
 142                (setn_array16T (b8l ih) aux_3 ilev2
 143                 (* cambio a partire da livello 3 *)
 144                 (setn_array16T (b8h sl) aux_4 (* ..(Y1)0,..(Y1)(Y2) *)
 145                  (setmn_array16T_succ_pred (b8h il) (b8h sl) aux_4 (* ..(X1+1).,..(Y1-1). *)
 146                   (setn_array16T (b8h il) aux_4 ilev3
 147                    (setmn_array16T (b8l il) xF T ilev4 v)) (* ..(X1)(X2),..(X1)F *)
 148                   vlev4)
 149                  (setmn_array16T x0 (b8l sl) T slev4 v))) ]
 150    (* caso 0x.(X1)(X2)(X3) a 0x..(Y1)(Y2)(Y3) *)
 151    | false ⇒ setn_array16T (b8h ih) aux_2 data
 152               (* cambio a partire da livello 2 *)
 153               (setn_array16T (b8l sh) aux_3
 154                (setmn_array16T_succ_pred (b8l ih) (b8l sh) aux_3 (* .(X1+1)..,.(Y1-1).. *)
 155                 (setn_array16T (b8l ih) aux_3 ilev2
 156                  (setmn_array16T_succ (b8h il) aux_4 (* .(X1)(X2+1).,.(X1)F. *)
 157                   (setn_array16T (b8h il) aux_4 ilev3
 158                    (setmn_array16T (b8l il) xF T ilev4 v)) (* .(X1)(X2)(X3),.(X1)(X2)F *)
 159                   vlev4))
 160                 vlev3)
 161                (setmn_array16T_pred (b8h sl) aux_4 (* .(Y1)0.,.(Y1)(Y2-1). *)
 162                 (setn_array16T (b8h sl) aux_4 slev3
 163                  (setmn_array16T x0 (b8l sl) T slev4 v)) (* .(Y1)(Y2)0,.(Y1)(Y2)(Y3) *)
 164                 vlev4))
 165    ]
 166   (* caso 0x(X1)(X2)(X3)(X4) a 0x(Y1)(Y2)(Y3)(Y4) *)
 167   | false ⇒ setn_array16T (b8h sh) aux_2
 168              (setmn_array16T_succ_pred (b8h ih) (b8h sh) aux_2 (* (X+1)...,(Y-1)... *)
 169               (setn_array16T (b8h ih) aux_2 data
 170                (setmn_array16T_succ (b8l ih) aux_3 (* (X1)(X2+1)..,(X1)F.. *)
 171                 (setn_array16T (b8l ih) aux_3 ilev2
 172                  (setmn_array16T_succ (b8h il) aux_4 (* (X1)(X2)(X3+1).,(X1)(X2)F. *)
 173                   (setn_array16T (b8h il) aux_4 ilev3
 174                    (setmn_array16T (b8l il) xF T ilev4 v)) (* (X1)(X2)(X3)(X4),(X1)(X2)(X3)F *)
 175                   vlev4))
 176                 vlev3))
 177                vlev2)
 178              (setmn_array16T_pred (b8l sh) aux_3 (* (Y1)0..,(Y1)(Y2-1).. *)
 179               (setn_array16T (b8l sh) aux_3 slev2
 180                (setmn_array16T_pred (b8h sl) aux_4 (* (Y1)(Y2)0.,(Y1)(Y2)(Y3-1). *)
 181                 (setn_array16T (b8h sl) aux_4 slev3
 182                  (setmn_array16T x0 (b8l sl) T slev4 v)) (* (Y1)(Y2)(Y3)0,(Y1)(Y2)(Y3)(Y4) *)
 183                 vlev4))
 184               vlev3) ]]]
 185  (* no i>s *)
 186  | false ⇒ data
 187  ].
 188
 189 ndefinition mt_chk_get ≝
 190 λchk:Array16T (Array16T (Array16T (Array16T memory_type))).λaddr:word16.
 191  match mt_visit ? chk addr with
 192  [ MEM_READ_ONLY ⇒ array_8T ? MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY
 193  | MEM_READ_WRITE ⇒ array_8T ? MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE
 194  | MEM_OUT_OF_BOUND ⇒ array_8T ? 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
 195  ].
 196
 197 (* scrivi controllando il tipo di memoria *)
 198 ndefinition mt_mem_update ≝
 199 λmem:Array16T (Array16T (Array16T (Array16T byte8))).
 200 λchk:Array8T memory_type.
 201 λaddr:word16.λv:byte8.
 202  match getn_array8T o0 ? chk with
 203   (* ROM? ok, ma il valore viene perso *)
 204   [ MEM_READ_ONLY ⇒ Some ? mem
 205   (* RAM? ok *)
 206   | MEM_READ_WRITE ⇒ Some ? (mt_update ? mem addr v)
 207   (* NON INSTALLATA? no *)
 208   | MEM_OUT_OF_BOUND ⇒ None ? ].
 209
 210 (* leggi controllando il tipo di memoria *)
 211 ndefinition mt_mem_read ≝
 212 λmem:Array16T (Array16T (Array16T (Array16T byte8))).
 213 λchk:Array16T (Array16T (Array16T (Array16T memory_type))).
 214 λaddr:word16.
 215  match  mt_visit ? chk addr with
 216   [ MEM_READ_ONLY ⇒ Some ? (mt_visit ? mem addr)
 217   | MEM_READ_WRITE ⇒ Some ? (mt_visit ? mem addr)
 218   | MEM_OUT_OF_BOUND ⇒ None ? ].
 219
 220 (* ************************** *)
 221 (* CARICAMENTO PROGRAMMA/DATI *)
 222 (* ************************** *)
 223
 224 (* carica a paratire da addr, scartando source (pescando da old_mem) se si supera 0xFFFF... *)
 225 nlet rec mt_load_from_source_at (old_mem:Array16T (Array16T (Array16T (Array16T byte8))))
 226                                (source:list byte8) (addr:word16) on source ≝
 227 match source with
 228  (* fine di source: carica da old_mem *)
 229  [ nil ⇒ old_mem
 230  | cons hd tl ⇒ match lt_w16 addr 〈〈xF,xF〉:〈xF,xF〉〉 with
 231   (* non supera 0xFFFF, ricorsione *)
 232   [ true ⇒ mt_load_from_source_at (mt_update ? old_mem addr hd) tl (plus_w16_d_d addr 〈〈x0,x0〉:〈x0,x1〉〉)
 233   (* supera 0xFFFF, niente ricorsione *)
 234   | false ⇒ mt_update ? old_mem addr hd
 235   ]].