1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
19 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
21 (* Questo materiale fa parte della tesi: *)
22 (* "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale" *)
24 (* data ultima modifica 15/11/2007 *)
25 (* ********************************************************************** *)
27 include "freescale/table_HC05.ma".
28 include "freescale/table_HC08.ma".
29 include "freescale/table_HCS08.ma".
30 include "freescale/table_RS08.ma".
32 (* ***************************** *)
33 (* TRADUZIONE ESADECIMALE → INFO *)
34 (* ***************************** *)
36 (* accesso alla tabella della ALU prescelta *)
37 definition opcode_table ≝
40 return λm:mcu_type.list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)
42 [ HC05 ⇒ opcode_table_HC05
43 | HC08 ⇒ opcode_table_HC08
44 | HCS08 ⇒ opcode_table_HCS08
45 | RS08 ⇒ opcode_table_RS08
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
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 ]
62 | Word w ⇒ match borw with
64 | Word borw' ⇒ match eq_w16 borw' w with
65 [ true ⇒ Some ? hd | false ⇒ aux tl ]
66 ]]] in aux (opcode_table m).
68 (* ******************************************************* *)
69 (* TRADUZIONE MCU+OPCODE+MODALITA'+ARGOMENTI → ESADECIMALE *)
70 (* ******************************************************* *)
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.
76 coercion cic:/matita/freescale/translation/t_byte8.ind#xpointer(1/1/1).
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)
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.
120 coercion cic:/matita/freescale/translation/instruction.ind#xpointer(1/1/1).
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.
127 (* inherent: legale se nessun operando *)
132 (* inherent address: legale se nessun operando/1 byte/1 word *)
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) ]
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 *)
168 (* SRT: legale se nessun operando *)
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
180 Some ? ([ (TByte m isab) ]@(args_picker m i p))
182 Some ? ([ (TByte m (w16h isaw)) ; (TByte m (w16l isaw)) ]@(args_picker m i p))
184 | false ⇒ aux tl ]] in aux (opcode_table m).
186 (* tipatore degli opcode generici *)
187 definition opcode_to_any ≝ λm:mcu_type.λo:opcode.anyOP m o.
189 (* ****************************** *)
190 (* APPROCCIO COMPILAZIONE AL VOLO *)
191 (* ****************************** *)
193 (* ausiliario di compile *)
201 (* compila solo se l'intera istruzione+modalita'+argomenti ha riscontro nelle tabelle *)
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
207 match res return λres: option (list (t_byte8 mcu)).defined ? res → ? with
208 [ None ⇒ λp:defined (list (t_byte8 mcu)) (None ?).
210 | Some v ⇒ λ_:defined ? (Some ? v).v
213 (* detipatore del compilato: (t_byte8 m) → byte8 *)
214 definition source_to_byte8 ≝
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 ([])
232 (* esempio da riciclare su come scrivere un sorgente *)
234 definition source_example_of_correct_HC08: list byte8 ≝
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)