]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/assembly/freescale/translation.ma
some corrections ...
[helm.git] / matita / 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 definition c_TByte ≝ TByte.
77
78 coercion c_TByte.
79
80 (* introduzione di un tipo dipendente (dalla modalita') per gli argomenti *)
81 inductive MA_check : instr_mode → Type ≝
82   maINH              : MA_check MODE_INH
83 | maINHA             : MA_check MODE_INHA
84 | maINHX             : MA_check MODE_INHX
85 | maINHH             : MA_check MODE_INHH
86 | maINHX0ADD         : MA_check MODE_INHX0ADD
87 | maINHX1ADD         : byte8 → MA_check MODE_INHX1ADD
88 | maINHX2ADD         : word16 → MA_check MODE_INHX2ADD
89 | maIMM1             : byte8  → MA_check MODE_IMM1
90 | maIMM1EXT          : byte8  → MA_check MODE_IMM1EXT
91 | maIMM2             : word16 → MA_check MODE_IMM2
92 | maDIR1             : byte8  → MA_check MODE_DIR1
93 | maDIR2             : word16 → MA_check MODE_DIR2
94 | maIX0              : MA_check MODE_IX0
95 | maIX1              : byte8  → MA_check MODE_IX1
96 | maIX2              : word16 → MA_check MODE_IX2
97 | maSP1              : byte8  → MA_check MODE_SP1
98 | maSP2              : word16 → MA_check MODE_SP2
99 | maDIR1_to_DIR1     : byte8 → byte8 → MA_check MODE_DIR1_to_DIR1
100 | maIMM1_to_DIR1     : byte8 → byte8 → MA_check MODE_IMM1_to_DIR1
101 | maIX0p_to_DIR1     : byte8 → MA_check MODE_IX0p_to_DIR1
102 | maDIR1_to_IX0p     : byte8 → MA_check MODE_DIR1_to_IX0p
103 | maINHA_and_IMM1    : byte8 → MA_check MODE_INHA_and_IMM1
104 | maINHX_and_IMM1    : byte8 → MA_check MODE_INHX_and_IMM1
105 | maIMM1_and_IMM1    : byte8 → byte8 → MA_check MODE_IMM1_and_IMM1
106 | maDIR1_and_IMM1    : byte8 → byte8 → MA_check MODE_DIR1_and_IMM1
107 | maIX0_and_IMM1     : byte8 → MA_check MODE_IX0_and_IMM1
108 | maIX0p_and_IMM1    : byte8 → MA_check MODE_IX0p_and_IMM1
109 | maIX1_and_IMM1     : byte8 → byte8 → MA_check MODE_IX1_and_IMM1
110 | maIX1p_and_IMM1    : byte8 → byte8 → MA_check MODE_IX1p_and_IMM1
111 | maSP1_and_IMM1     : byte8 → byte8 → MA_check MODE_SP1_and_IMM1
112 | maDIRn             : ∀o.byte8 → MA_check (MODE_DIRn o)
113 | maDIRn_and_IMM1    : ∀o.byte8 → byte8 → MA_check (MODE_DIRn_and_IMM1 o)
114 | maTNY              : ∀e.MA_check (MODE_TNY e)
115 | maSRT              : ∀t.MA_check (MODE_SRT t)
116 .
117
118 (* tipo istruzione per unificare in una lista omogenea il sorgente *)
119 inductive instruction : Type ≝ 
120 instr: ∀i:instr_mode.opcode → MA_check i → instruction.
121
122 definition c_instr ≝ instr.
123
124 coercion c_instr.
125
126 (* picker: trasforma l'argomento necessario in input a bytes_of_pseudo_instr_mode_param:
127    MA_check i → list (t_byte8 m) *)
128 definition args_picker ≝
129 λm:mcu_type.λi:instr_mode.λargs:MA_check i.
130  match args with
131   (* inherent: legale se nessun operando *) 
132   [ maINH    ⇒ nil ? 
133   | maINHA   ⇒ nil ? 
134   | maINHX   ⇒ nil ? 
135   | maINHH   ⇒ nil ?
136   (* inherent address: legale se nessun operando/1 byte/1 word *)
137   | maINHX0ADD ⇒ nil ?
138   | maINHX1ADD b ⇒ [ TByte m b ]
139   | maINHX2ADD w ⇒ [ TByte m (w16h w); TByte m (w16l w) ]    
140   (* _0/1/2: legale se nessun operando/1 byte/1 word *)
141   | maIMM1 b ⇒ [ TByte m b ]
142   | maIMM1EXT b ⇒ [ TByte m b ]
143   | maIMM2 w ⇒ [ TByte m (w16h w); TByte m (w16l w) ]
144   | maDIR1 b ⇒ [ TByte m b ]
145   | maDIR2 w ⇒ [ TByte m (w16h w); TByte m (w16l w) ]
146   | maIX0    ⇒ nil ?
147   | maIX1 b  ⇒ [ TByte m b ]
148   | maIX2 w  ⇒ [ TByte m (w16h w); TByte m (w16l w) ]
149   | maSP1 b  ⇒ [ TByte m b ]
150   | maSP2 w  ⇒ [ TByte m (w16h w); TByte m (w16l w) ]
151   (* movimento: legale se 2 operandi byte *)
152   | maDIR1_to_DIR1 b1 b2  ⇒ [ TByte m b1 ; TByte m b2 ]
153   | maIMM1_to_DIR1 b1 b2  ⇒ [ TByte m b1 ; TByte m b2 ]
154   | maIX0p_to_DIR1 b      ⇒ [ TByte m b]
155   | maDIR1_to_IX0p b      ⇒ [ TByte m b]
156   (* cbeq/dbnz: legale se 1/2 operandi byte *)
157   | maINHA_and_IMM1 b     ⇒ [ TByte m b]
158   | maINHX_and_IMM1 b     ⇒ [ TByte m b]
159   | maIMM1_and_IMM1 b1 b2 ⇒ [ TByte m b1 ; TByte m b2 ]
160   | maDIR1_and_IMM1 b1 b2 ⇒ [ TByte m b1 ; TByte m b2 ]
161   | maIX0_and_IMM1  b     ⇒ [ TByte m b]
162   | maIX0p_and_IMM1 b     ⇒ [ TByte m b]
163   | maIX1_and_IMM1  b1 b2 ⇒ [ TByte m b1 ; TByte m b2 ]
164   | maIX1p_and_IMM1 b1 b2 ⇒ [ TByte m b1 ; TByte m b2 ]
165   | maSP1_and_IMM1  b1 b2 ⇒ [ TByte m b1 ; TByte m b2 ]
166   (* DIRn: legale se 1 operando byte *)
167   | maDIRn _ b ⇒ [ TByte m b]
168   (* DIRn_and_IMM1: legale se 2 operandi byte *)
169   | maDIRn_and_IMM1 _ b1 b2 ⇒ [ TByte m b1 ; TByte m b2 ]
170   (* TNY: legale se nessun operando *)
171   | maTNY _ ⇒ nil ?
172   (* SRT: legale se nessun operando *)
173   | maSRT _ ⇒ nil ?
174   ].
175
176 (* trasformatore finale: mcu+opcode+instr_mode+args → list (t_byte8 m) *)
177 definition bytes_of_pseudo_instr_mode_param ≝
178 λm:mcu_type.λo:any_opcode m.λi:instr_mode.λp:MA_check i.
179 let rec aux param  ≝ match param with
180  [ nil ⇒ None ? | cons hd tl ⇒
181   match (eqop m o (fst4T ???? hd)) ⊗ (eqim i (snd4T ???? hd)) with
182    [ true ⇒ match thd4T ???? hd with 
183     [ Byte isab ⇒ 
184      Some ? ([ (TByte m isab) ]@(args_picker m i p))
185     | Word isaw ⇒
186      Some ? ([ (TByte m (w16h isaw)) ; (TByte m (w16l isaw)) ]@(args_picker m i p))
187     ]
188    | false ⇒ aux tl ]] in aux (opcode_table m).
189
190 (* tipatore degli opcode generici *)
191 definition opcode_to_any ≝ λm:mcu_type.λo:opcode.anyOP m o.
192
193 (* ****************************** *)
194 (* APPROCCIO COMPILAZIONE AL VOLO *)
195 (* ****************************** *)
196
197 (* ausiliario di compile *)
198 definition defined ≝
199  λT:Type.λo:option T.
200   match o with
201    [ None ⇒ False
202    | Some _ ⇒ True
203    ].
204
205 (* compila solo se l'intera istruzione+modalita'+argomenti ha riscontro nelle tabelle *)
206 definition compile ≝
207 λmcu:mcu_type.λi:instr_mode.λop:opcode.λarg:MA_check i.
208  let res ≝ bytes_of_pseudo_instr_mode_param mcu (opcode_to_any mcu op) i arg in
209   λp:defined ? res.
210    let value ≝
211     match res return λres: option (list (t_byte8 mcu)).defined ? res → ? with
212     [ None ⇒ λp:defined (list (t_byte8 mcu)) (None ?).
213        False_rect ? p
214     | Some v ⇒ λ_:defined ? (Some ? v).v
215     ] p in value.
216
217 (* detipatore del compilato: (t_byte8 m) → byte8 *)
218 definition source_to_byte8 ≝
219 λmcu:mcu_type.
220  match mcu
221   return λmcu:mcu_type.list (t_byte8 mcu) → list byte8 with
222   [ HC05 ⇒ λl:list (t_byte8 HC05).
223    let rec aux (p1:list (t_byte8 HC05)) (p2:list byte8) ≝ match p1 with
224     [ nil ⇒ p2 | cons hd tl ⇒ match hd with [ TByte b ⇒ aux tl (p2@[b]) ]] in aux l ([])
225   | HC08 ⇒ λl:list (t_byte8 HC08).
226    let rec aux (p1:list (t_byte8 HC08)) (p2:list byte8) ≝ match p1 with
227     [ nil ⇒ p2 | cons hd tl ⇒ match hd with [ TByte b ⇒ aux tl (p2@[b]) ]] in aux l ([])
228   | HCS08 ⇒ λl:list (t_byte8 HCS08).
229    let rec aux (p1:list (t_byte8 HCS08)) (p2:list byte8) ≝ match p1 with
230     [ nil ⇒ p2 | cons hd tl ⇒ match hd with [ TByte b ⇒ aux tl (p2@[b]) ]] in aux l ([])
231   | RS08 ⇒ λl:list (t_byte8 RS08).
232    let rec aux (p1:list (t_byte8 RS08)) (p2:list byte8) ≝ match p1 with
233     [ nil ⇒ p2 | cons hd tl ⇒ match hd with [ TByte b ⇒ aux tl (p2@[b]) ]] in aux l ([])
234   ].
235
236 (* esempio da riciclare su come scrivere un sorgente *)
237 (*
238 definition source_example_of_correct_HC08: list byte8 ≝
239 let m ≝ HC08 in
240  source_to_byte8 m (
241   (compile m ? CLR maINHA I) @
242   (compile m ? NOP maINH I) @
243   (compile m ? BRSETn (maDIRn_and_IMM1 x1 〈x1,x2〉 〈x3,x4〉) I) @
244   (compile m ? ADD maIX0 I) @
245   (compile m ? ADD (maIX1 〈x1,x2〉) I) @
246   (compile m ? ADD (maSP2 〈〈x1,x2〉:〈x3,x4〉〉) I)
247  ).
248 *)