matita/contribs/assembly/freescale/translation.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/table_HC05.ma".
  28 include "freescale/table_HC08.ma".
  29 include "freescale/table_HCS08.ma".
  30 include "freescale/table_RS08.ma".
  31
  32 (* ***************************** *)
  33 (* TRADUZIONE ESADECIMALE → INFO *)
  34 (* ***************************** *)
  35
  36 (* accesso alla tabella della ALU prescelta *)
  37 definition opcode_table ≝
  38 λm:mcu_type.
  39  match m
  40   return λm:mcu_type.list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)
  41  with
  42   [ HC05  ⇒ opcode_table_HC05
  43   | HC08  ⇒ opcode_table_HC08
  44   | HCS08 ⇒ opcode_table_HCS08
  45   | RS08  ⇒ opcode_table_RS08
  46  ].
  47
  48 (* traduzione mcu+esadecimale → info *)
  49 (* NB: la ricerca per byte non matcha con una word con lo stesso byte superiore uguale *)
  50 (* NB: per matchare una word (precode+code) bisogna passare una word *)
  51 (* NB: il risultato e' sempre un'opzione, NON esiste un dummy opcode tipo UNKNOWN/ILLEGAL *)
  52 definition full_info_of_word16 ≝
  53 λm:mcu_type.λborw:byte8_or_word16.
  54  let rec aux param ≝ match param with
  55   [ nil ⇒ None ?
  56   | cons hd tl ⇒
  57    match thd4T ???? hd with
  58     [ Byte b ⇒ match borw with
  59      [ Byte borw' ⇒ match eq_b8 borw' b with
  60       [ true ⇒ Some ? hd | false ⇒ aux tl ]
  61      | Word _ ⇒ aux tl ]
  62     | Word w ⇒ match borw with
  63      [ Byte _ ⇒ aux tl
  64      | Word borw' ⇒ match eq_w16 borw' w with
  65       [ true ⇒ Some ? hd | false ⇒ aux tl ]
  66     ]]] in aux (opcode_table m).
  67
  68 (* ******************************************************* *)
  69 (* TRADUZIONE MCU+OPCODE+MODALITA'+ARGOMENTI → ESADECIMALE *)
  70 (* ******************************************************* *)
  71
  72 (* introduzione di un tipo byte8 dipendente dall'mcu_type (phantom type) *)
  73 inductive t_byte8 (m:mcu_type) : Type ≝
  74  TByte : byte8 → t_byte8 m.
  75
  76 coercion cic:/matita/freescale/translation/t_byte8.ind#xpointer(1/1/1).
  77
  78 (* introduzione di un tipo dipendente (dalla modalita') per gli argomenti *)
  79 inductive MA_check : instr_mode → Type ≝
  80   maINH              : MA_check MODE_INH
  81 | maINHA             : MA_check MODE_INHA
  82 | maINHX             : MA_check MODE_INHX
  83 | maINHH             : MA_check MODE_INHH
  84 | maINHX0ADD         : MA_check MODE_INHX0ADD
  85 | maINHX1ADD         : byte8 → MA_check MODE_INHX1ADD
  86 | maINHX2ADD         : word16 → MA_check MODE_INHX2ADD
  87 | maIMM1             : byte8  → MA_check MODE_IMM1
  88 | maIMM1EXT          : byte8  → MA_check MODE_IMM1EXT
  89 | maIMM2             : word16 → MA_check MODE_IMM2
  90 | maDIR1             : byte8  → MA_check MODE_DIR1
  91 | maDIR2             : word16 → MA_check MODE_DIR2
  92 | maIX0              : MA_check MODE_IX0
  93 | maIX1              : byte8  → MA_check MODE_IX1
  94 | maIX2              : word16 → MA_check MODE_IX2
  95 | maSP1              : byte8  → MA_check MODE_SP1
  96 | maSP2              : word16 → MA_check MODE_SP2
  97 | maDIR1_to_DIR1     : byte8 → byte8 → MA_check MODE_DIR1_to_DIR1
  98 | maIMM1_to_DIR1     : byte8 → byte8 → MA_check MODE_IMM1_to_DIR1
  99 | maIX0p_to_DIR1     : byte8 → MA_check MODE_IX0p_to_DIR1
 100 | maDIR1_to_IX0p     : byte8 → MA_check MODE_DIR1_to_IX0p
 101 | maINHA_and_IMM1    : byte8 → MA_check MODE_INHA_and_IMM1
 102 | maINHX_and_IMM1    : byte8 → MA_check MODE_INHX_and_IMM1
 103 | maIMM1_and_IMM1    : byte8 → byte8 → MA_check MODE_IMM1_and_IMM1
 104 | maDIR1_and_IMM1    : byte8 → byte8 → MA_check MODE_DIR1_and_IMM1
 105 | maIX0_and_IMM1     : byte8 → MA_check MODE_IX0_and_IMM1
 106 | maIX0p_and_IMM1    : byte8 → MA_check MODE_IX0p_and_IMM1
 107 | maIX1_and_IMM1     : byte8 → byte8 → MA_check MODE_IX1_and_IMM1
 108 | maIX1p_and_IMM1    : byte8 → byte8 → MA_check MODE_IX1p_and_IMM1
 109 | maSP1_and_IMM1     : byte8 → byte8 → MA_check MODE_SP1_and_IMM1
 110 | maDIRn             : ∀o.byte8 → MA_check (MODE_DIRn o)
 111 | maDIRn_and_IMM1    : ∀o.byte8 → byte8 → MA_check (MODE_DIRn_and_IMM1 o)
 112 | maTNY              : ∀e.MA_check (MODE_TNY e)
 113 | maSRT              : ∀t.MA_check (MODE_SRT t)
 114 .
 115
 116 (* tipo istruzione per unificare in una lista omogenea il sorgente *)
 117 inductive instruction : Type ≝
 118 instr: ∀i:instr_mode.opcode → MA_check i → instruction.
 119
 120 coercion cic:/matita/freescale/translation/instruction.ind#xpointer(1/1/1).
 121
 122 (* picker: trasforma l'argomento necessario in input a bytes_of_pseudo_instr_mode_param:
 123    MA_check i → list (t_byte8 m) *)
 124 definition args_picker ≝
 125 λm:mcu_type.λi:instr_mode.λargs:MA_check i.
 126  match args with
 127   (* inherent: legale se nessun operando *)
 128   [ maINH    ⇒ nil ?
 129   | maINHA   ⇒ nil ?
 130   | maINHX   ⇒ nil ?
 131   | maINHH   ⇒ nil ?
 132   (* inherent address: legale se nessun operando/1 byte/1 word *)
 133   | maINHX0ADD ⇒ nil ?
 134   | maINHX1ADD b ⇒ [ TByte m b ]
 135   | maINHX2ADD w ⇒ [ TByte m (w16h w); TByte m (w16l w) ]
 136   (* _0/1/2: legale se nessun operando/1 byte/1 word *)
 137   | maIMM1 b ⇒ [ TByte m b ]
 138   | maIMM1EXT b ⇒ [ TByte m b ]
 139   | maIMM2 w ⇒ [ TByte m (w16h w); TByte m (w16l w) ]
 140   | maDIR1 b ⇒ [ TByte m b ]
 141   | maDIR2 w ⇒ [ TByte m (w16h w); TByte m (w16l w) ]
 142   | maIX0    ⇒ nil ?
 143   | maIX1 b  ⇒ [ TByte m b ]
 144   | maIX2 w  ⇒ [ TByte m (w16h w); TByte m (w16l w) ]
 145   | maSP1 b  ⇒ [ TByte m b ]
 146   | maSP2 w  ⇒ [ TByte m (w16h w); TByte m (w16l w) ]
 147   (* movimento: legale se 2 operandi byte *)
 148   | maDIR1_to_DIR1 b1 b2  ⇒ [ TByte m b1 ; TByte m b2 ]
 149   | maIMM1_to_DIR1 b1 b2  ⇒ [ TByte m b1 ; TByte m b2 ]
 150   | maIX0p_to_DIR1 b      ⇒ [ TByte m b]
 151   | maDIR1_to_IX0p b      ⇒ [ TByte m b]
 152   (* cbeq/dbnz: legale se 1/2 operandi byte *)
 153   | maINHA_and_IMM1 b     ⇒ [ TByte m b]
 154   | maINHX_and_IMM1 b     ⇒ [ TByte m b]
 155   | maIMM1_and_IMM1 b1 b2 ⇒ [ TByte m b1 ; TByte m b2 ]
 156   | maDIR1_and_IMM1 b1 b2 ⇒ [ TByte m b1 ; TByte m b2 ]
 157   | maIX0_and_IMM1  b     ⇒ [ TByte m b]
 158   | maIX0p_and_IMM1 b     ⇒ [ TByte m b]
 159   | maIX1_and_IMM1  b1 b2 ⇒ [ TByte m b1 ; TByte m b2 ]
 160   | maIX1p_and_IMM1 b1 b2 ⇒ [ TByte m b1 ; TByte m b2 ]
 161   | maSP1_and_IMM1  b1 b2 ⇒ [ TByte m b1 ; TByte m b2 ]
 162   (* DIRn: legale se 1 operando byte *)
 163   | maDIRn _ b ⇒ [ TByte m b]
 164   (* DIRn_and_IMM1: legale se 2 operandi byte *)
 165   | maDIRn_and_IMM1 _ b1 b2 ⇒ [ TByte m b1 ; TByte m b2 ]
 166   (* TNY: legale se nessun operando *)
 167   | maTNY _ ⇒ nil ?
 168   (* SRT: legale se nessun operando *)
 169   | maSRT _ ⇒ nil ?
 170   ].
 171
 172 (* trasformatore finale: mcu+opcode+instr_mode+args → list (t_byte8 m) *)
 173 definition bytes_of_pseudo_instr_mode_param ≝
 174 λm:mcu_type.λo:any_opcode m.λi:instr_mode.λp:MA_check i.
 175 let rec aux param  ≝ match param with
 176  [ nil ⇒ None ? | cons hd tl ⇒
 177   match (eqop m o (fst4T ???? hd)) ⊗ (eqim i (snd4T ???? hd)) with
 178    [ true ⇒ match thd4T ???? hd with
 179     [ Byte isab ⇒
 180      Some ? ([ (TByte m isab) ]@(args_picker m i p))
 181     | Word isaw ⇒
 182      Some ? ([ (TByte m (w16h isaw)) ; (TByte m (w16l isaw)) ]@(args_picker m i p))
 183     ]
 184    | false ⇒ aux tl ]] in aux (opcode_table m).
 185
 186 (* tipatore degli opcode generici *)
 187 definition opcode_to_any ≝ λm:mcu_type.λo:opcode.anyOP m o.
 188
 189 (* ****************************** *)
 190 (* APPROCCIO COMPILAZIONE AL VOLO *)
 191 (* ****************************** *)
 192
 193 (* ausiliario di compile *)
 194 definition defined ≝
 195  λT:Type.λo:option T.
 196   match o with
 197    [ None ⇒ False
 198    | Some _ ⇒ True
 199    ].
 200
 201 (* compila solo se l'intera istruzione+modalita'+argomenti ha riscontro nelle tabelle *)
 202 definition compile ≝
 203 λmcu:mcu_type.λi:instr_mode.λop:opcode.λarg:MA_check i.
 204  let res ≝ bytes_of_pseudo_instr_mode_param mcu (opcode_to_any mcu op) i arg in
 205   λp:defined ? res.
 206    let value ≝
 207     match res return λres: option (list (t_byte8 mcu)).defined ? res → ? with
 208     [ None ⇒ λp:defined (list (t_byte8 mcu)) (None ?).
 209        False_rect ? p
 210     | Some v ⇒ λ_:defined ? (Some ? v).v
 211     ] p in value.
 212
 213 (* detipatore del compilato: (t_byte8 m) → byte8 *)
 214 definition source_to_byte8 ≝
 215 λmcu:mcu_type.
 216  match mcu
 217   return λmcu:mcu_type.list (t_byte8 mcu) → list byte8 with
 218   [ HC05 ⇒ λl:list (t_byte8 HC05).
 219    let rec aux (p1:list (t_byte8 HC05)) (p2:list byte8) ≝ match p1 with
 220     [ nil ⇒ p2 | cons hd tl ⇒ match hd with [ TByte b ⇒ aux tl (p2@[b]) ]] in aux l ([])
 221   | HC08 ⇒ λl:list (t_byte8 HC08).
 222    let rec aux (p1:list (t_byte8 HC08)) (p2:list byte8) ≝ match p1 with
 223     [ nil ⇒ p2 | cons hd tl ⇒ match hd with [ TByte b ⇒ aux tl (p2@[b]) ]] in aux l ([])
 224   | HCS08 ⇒ λl:list (t_byte8 HCS08).
 225    let rec aux (p1:list (t_byte8 HCS08)) (p2:list byte8) ≝ match p1 with
 226     [ nil ⇒ p2 | cons hd tl ⇒ match hd with [ TByte b ⇒ aux tl (p2@[b]) ]] in aux l ([])
 227   | RS08 ⇒ λl:list (t_byte8 RS08).
 228    let rec aux (p1:list (t_byte8 RS08)) (p2:list byte8) ≝ match p1 with
 229     [ nil ⇒ p2 | cons hd tl ⇒ match hd with [ TByte b ⇒ aux tl (p2@[b]) ]] in aux l ([])
 230   ].
 231
 232 (* esempio da riciclare su come scrivere un sorgente *)
 233 (*
 234 definition source_example_of_correct_HC08: list byte8 ≝
 235 let m ≝ HC08 in
 236  source_to_byte8 m (
 237   (compile m ? CLR maINHA I) @
 238   (compile m ? NOP maINH I) @
 239   (compile m ? BRSETn (maDIRn_and_IMM1 x1 〈x1,x2〉 〈x3,x4〉) I) @
 240   (compile m ? ADD maIX0 I) @
 241   (compile m ? ADD (maIX1 〈x1,x2〉) I) @
 242   (compile m ? ADD (maSP2 〈〈x1,x2〉:〈x3,x4〉〉) I)
 243  ).
 244 *)