matita/matita/contribs/ng_assembly/emulator/memory/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: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
  19 (*   Sviluppo: 2008-2010                                                  *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "emulator/memory/memory_struct.ma".
  24 include "num/word32.ma".
  25 include "common/option.ma".
  26 include "common/list.ma".
  27
  28 (* ********************* *)
  29 (* MEMORIA E DESCRITTORE *)
  30 (* ********************* *)
  31
  32 ndefinition aux_32B_filler ≝
  33 λT:Type.λel:T.
  34 let lev8 ≝ mk_Array16T T el el el el el el el el el el el el el el el el in
  35 let lev7 ≝ mk_Array16T ?
  36            lev8 lev8 lev8 lev8 lev8 lev8 lev8 lev8
  37            lev8 lev8 lev8 lev8 lev8 lev8 lev8 lev8
  38            in
  39 let lev6 ≝ mk_Array16T ?
  40            lev7 lev7 lev7 lev7 lev7 lev7 lev7 lev7
  41            lev7 lev7 lev7 lev7 lev7 lev7 lev7 lev7
  42            in
  43 let lev5 ≝ mk_Array16T ?
  44            lev6 lev6 lev6 lev6 lev6 lev6 lev6 lev6
  45            lev6 lev6 lev6 lev6 lev6 lev6 lev6 lev6
  46            in
  47 let lev4 ≝ mk_Array16T ?
  48            lev5 lev5 lev5 lev5 lev5 lev5 lev5 lev5
  49            lev5 lev5 lev5 lev5 lev5 lev5 lev5 lev5
  50            in
  51 let lev3 ≝ mk_Array16T ?
  52            lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4
  53            lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4
  54            in
  55 let lev2 ≝ mk_Array16T ?
  56            lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3
  57            lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3
  58            in
  59 let lev1 ≝ mk_Array16T ?
  60            lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2
  61            lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2
  62            in
  63 lev1.
  64
  65 ndefinition aux_32B_type ≝
  66 λT:Type.Array16T (Array16T (Array16T (Array16T (Array16T (Array16T (Array16T (Array16T T))))))).
  67
  68 (* tutta la memoria non installata *)
  69 ndefinition mt_out_of_bound_memory ≝ aux_32B_filler ? MEM_OUT_OF_BOUND.
  70
  71 (* tutta la memoria a 0 *)
  72 ndefinition mt_zero_memory ≝ aux_32B_filler ? 〈x0,x0〉.
  73
  74 (* visita di un albero da 4GB di elementi: ln16(4GB)=8 passaggi *)
  75 ndefinition mt_visit ≝
  76 λT:Type.λdata:aux_32B_type T.λaddr:word32.
  77  getn_array16T (cnL ? (cnL ? (cnL ? addr))) ?
  78   (getn_array16T (cnH ? (cnL ? (cnL ? addr))) ?
  79    (getn_array16T (cnL ? (cnH ? (cnL ? addr))) ?
  80     (getn_array16T (cnH ? (cnH ? (cnL ? addr))) ?
  81      (getn_array16T (cnL ? (cnL ? (cnH ? addr))) ?
  82       (getn_array16T (cnH ? (cnL ? (cnH ? addr))) ?
  83        (getn_array16T (cnL ? (cnH ? (cnH ? addr))) ?
  84         (getn_array16T (cnH ? (cnH ? (cnH ? addr))) ? data))))))).
  85
  86 (* scrittura di un elemento in un albero da 4GB *)
  87 ndefinition mt_update ≝
  88 λT:Type.λdata:aux_32B_type T.λaddr:word32.λv:T.
  89  let lev2 ≝ getn_array16T (cnH ? (cnH ? (cnH ? addr))) ? data in
  90  let lev3 ≝ getn_array16T (cnL ? (cnH ? (cnH ? addr))) ? lev2 in
  91  let lev4 ≝ getn_array16T (cnH ? (cnL ? (cnH ? addr))) ? lev3 in
  92  let lev5 ≝ getn_array16T (cnL ? (cnL ? (cnH ? addr))) ? lev4 in
  93  let lev6 ≝ getn_array16T (cnH ? (cnH ? (cnL ? addr))) ? lev5 in
  94  let lev7 ≝ getn_array16T (cnL ? (cnH ? (cnL ? addr))) ? lev6 in
  95  let lev8 ≝ getn_array16T (cnH ? (cnL ? (cnL ? addr))) ? lev7 in
  96
  97  setn_array16T (cnH ? (cnH ? (cnH ? addr))) ? data
  98   (setn_array16T (cnL ? (cnH ? (cnH ? addr))) ? lev2
  99    (setn_array16T (cnH ? (cnL ? (cnH ? addr))) ? lev3
 100     (setn_array16T (cnL ? (cnL ? (cnH ? addr))) ? lev4
 101      (setn_array16T (cnH ? (cnH ? (cnL ? addr))) ? lev5
 102       (setn_array16T (cnL ? (cnH ? (cnL ? addr))) ? lev6
 103        (setn_array16T (cnH ? (cnL ? (cnL ? addr))) ? lev7
 104         (setn_array16T (cnL ? (cnL ? (cnL ? addr))) T lev8 v))))))).
 105
 106 (* scrittura di un range (max 64KB) in un albero da 4GB *)
 107 nlet rec mt_update_ranged (T:Type) (data:aux_32B_type T) (addr:word32) (w:word16) (rw:rec_word16 w) (v:T) on rw ≝
 108  match rw with
 109   [ w16_O ⇒ data
 110   | w16_S w' rw' ⇒ mt_update_ranged T (mt_update T data addr v)
 111                                     (succ_w32 addr) w' rw' v
 112   ].
 113
 114 (* scrivi controllando il tipo di memoria *)
 115 ndefinition mt_mem_update ≝
 116 λmem:aux_32B_type byte8.
 117 λchk:aux_32B_type memory_type.
 118 λaddr:word32.λv:byte8.
 119  match mt_visit ? chk addr with
 120   (* ROM? ok, ma il valore viene perso *)
 121   [ MEM_READ_ONLY ⇒ Some ? mem
 122   (* RAM? ok *)
 123   | MEM_READ_WRITE ⇒ Some ? (mt_update ? mem addr v)
 124   (* NON INSTALLATA? no *)
 125   | MEM_OUT_OF_BOUND ⇒ None ? ].
 126
 127 (* leggi controllando il tipo di memoria *)
 128 ndefinition mt_mem_read ≝
 129 λmem:aux_32B_type byte8.
 130 λchk:aux_32B_type memory_type.
 131 λaddr:word32.
 132  match mt_visit ? chk addr with
 133   [ MEM_READ_ONLY ⇒ Some ? (mt_visit ? mem addr)
 134   | MEM_READ_WRITE ⇒ Some ? (mt_visit ? mem addr)
 135   | MEM_OUT_OF_BOUND ⇒ None ? ].
 136
 137 (* ************************** *)
 138 (* CARICAMENTO PROGRAMMA/DATI *)
 139 (* ************************** *)
 140
 141 (* carica a paratire da addr, overflow se si supera 0xFFFF... *)
 142 nlet rec mt_load_from_source_at (old_mem:aux_32B_type byte8)
 143                                 (src:list byte8) (addr:word32) on src ≝
 144  match src with
 145   (* fine di source: carica da old_mem *)
 146   [ nil ⇒ old_mem
 147   | cons hd tl ⇒ mt_load_from_source_at (mt_update ? old_mem addr hd) tl (succ_w32 addr)
 148   ].