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 *)
18 (* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
21 (* ********************************************************************** *)
23 include "freescale/table_HC05.ma".
24 include "freescale/table_HC08.ma".
25 include "freescale/table_HCS08.ma".
26 include "freescale/table_RS08.ma".
27 include "freescale/option.ma".
29 (* ***************************** *)
30 (* TRADUZIONE ESADECIMALE → INFO *)
31 (* ***************************** *)
33 (* accesso alla tabella della ALU prescelta *)
34 ndefinition opcode_table ≝
37 return λm:mcu_type.list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)
39 [ HC05 ⇒ opcode_table_HC05
40 | HC08 ⇒ opcode_table_HC08
41 | HCS08 ⇒ opcode_table_HCS08
42 | RS08 ⇒ opcode_table_RS08
45 (* traduzione mcu+esadecimale → info *)
46 (* NB: la ricerca per byte non matcha con una word con lo stesso byte superiore uguale *)
47 (* NB: per matchare una word (precode+code) bisogna passare una word *)
48 (* NB: il risultato e' sempre un'opzione, NON esiste un dummy opcode tipo UNKNOWN/ILLEGAL *)
49 nlet rec full_info_of_word16_aux (m:mcu_type) (borw:byte8_or_word16)
50 (param:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on param ≝
55 [ Byte b ⇒ match borw with
56 [ Byte borw' ⇒ match eq_b8 borw' b with
58 | false ⇒ full_info_of_word16_aux m borw tl ]
59 | Word _ ⇒ full_info_of_word16_aux m borw tl ]
60 | Word w ⇒ match borw with
61 [ Byte _ ⇒ full_info_of_word16_aux m borw tl
62 | Word borw' ⇒ match eq_w16 borw' w with
64 | false ⇒ full_info_of_word16_aux m borw tl ]
67 ndefinition full_info_of_word16 ≝
68 λm:mcu_type.λborw:byte8_or_word16.
69 full_info_of_word16_aux m borw (opcode_table m).
71 (* ******************************************************* *)
72 (* TRADUZIONE MCU+OPCODE+MODALITA'+ARGOMENTI → ESADECIMALE *)
73 (* ******************************************************* *)
75 (* introduzione di un tipo byte8 dipendente dall'mcu_type (phantom type) *)
76 ninductive t_byte8 (m:mcu_type) : Type ≝
77 TByte : byte8 → t_byte8 m.
79 nlemma tbyte8_destruct : ∀m,b1,b2.TByte m b1 = TByte m b2 → b1 = b2.
81 nchange with (match TByte m b2 with [ TByte a ⇒ b1 = a ]);
87 (* introduzione di un tipo dipendente (dalla modalita') per gli argomenti *)
88 ninductive MA_check : instr_mode → Type ≝
89 maINH : MA_check MODE_INH
90 | maINHA : MA_check MODE_INHA
91 | maINHX : MA_check MODE_INHX
92 | maINHH : MA_check MODE_INHH
93 | maINHX0ADD : MA_check MODE_INHX0ADD
94 | maINHX1ADD : byte8 → MA_check MODE_INHX1ADD
95 | maINHX2ADD : word16 → MA_check MODE_INHX2ADD
96 | maIMM1 : byte8 → MA_check MODE_IMM1
97 | maIMM1EXT : byte8 → MA_check MODE_IMM1EXT
98 | maIMM2 : word16 → MA_check MODE_IMM2
99 | maDIR1 : byte8 → MA_check MODE_DIR1
100 | maDIR2 : word16 → MA_check MODE_DIR2
101 | maIX0 : MA_check MODE_IX0
102 | maIX1 : byte8 → MA_check MODE_IX1
103 | maIX2 : word16 → MA_check MODE_IX2
104 | maSP1 : byte8 → MA_check MODE_SP1
105 | maSP2 : word16 → MA_check MODE_SP2
106 | maDIR1_to_DIR1 : byte8 → byte8 → MA_check MODE_DIR1_to_DIR1
107 | maIMM1_to_DIR1 : byte8 → byte8 → MA_check MODE_IMM1_to_DIR1
108 | maIX0p_to_DIR1 : byte8 → MA_check MODE_IX0p_to_DIR1
109 | maDIR1_to_IX0p : byte8 → MA_check MODE_DIR1_to_IX0p
110 | maINHA_and_IMM1 : byte8 → MA_check MODE_INHA_and_IMM1
111 | maINHX_and_IMM1 : byte8 → MA_check MODE_INHX_and_IMM1
112 | maIMM1_and_IMM1 : byte8 → byte8 → MA_check MODE_IMM1_and_IMM1
113 | maDIR1_and_IMM1 : byte8 → byte8 → MA_check MODE_DIR1_and_IMM1
114 | maIX0_and_IMM1 : byte8 → MA_check MODE_IX0_and_IMM1
115 | maIX0p_and_IMM1 : byte8 → MA_check MODE_IX0p_and_IMM1
116 | maIX1_and_IMM1 : byte8 → byte8 → MA_check MODE_IX1_and_IMM1
117 | maIX1p_and_IMM1 : byte8 → byte8 → MA_check MODE_IX1p_and_IMM1
118 | maSP1_and_IMM1 : byte8 → byte8 → MA_check MODE_SP1_and_IMM1
119 | maDIRn : ∀n.byte8 → MA_check (MODE_DIRn n)
120 | maDIRn_and_IMM1 : ∀n.byte8 → byte8 → MA_check (MODE_DIRn_and_IMM1 n)
121 | maTNY : ∀e.MA_check (MODE_TNY e)
122 | maSRT : ∀t.MA_check (MODE_SRT t)
125 (* picker: trasforma l'argomento necessario in input a bytes_of_pseudo_instr_mode_param:
126 MA_check i → list (t_byte8 m) *)
127 ndefinition args_picker ≝
128 λm:mcu_type.λi:instr_mode.λargs:MA_check i.
130 (* inherent: legale se nessun operando *)
135 (* inherent address: legale se nessun operando/1 byte/1 word *)
137 | maINHX1ADD b ⇒ [ TByte m b ]
138 | maINHX2ADD w ⇒ [ TByte m (w16h w); TByte m (w16l w) ]
139 (* _0/1/2: legale se nessun operando/1 byte/1 word *)
140 | maIMM1 b ⇒ [ TByte m b ]
141 | maIMM1EXT b ⇒ [ TByte m b ]
142 | maIMM2 w ⇒ [ TByte m (w16h w); TByte m (w16l w) ]
143 | maDIR1 b ⇒ [ TByte m b ]
144 | maDIR2 w ⇒ [ TByte m (w16h w); TByte m (w16l w) ]
146 | maIX1 b ⇒ [ TByte m b ]
147 | maIX2 w ⇒ [ TByte m (w16h w); TByte m (w16l w) ]
148 | maSP1 b ⇒ [ TByte m b ]
149 | maSP2 w ⇒ [ TByte m (w16h w); TByte m (w16l w) ]
150 (* movimento: legale se 2 operandi byte *)
151 | maDIR1_to_DIR1 b1 b2 ⇒ [ TByte m b1 ; TByte m b2 ]
152 | maIMM1_to_DIR1 b1 b2 ⇒ [ TByte m b1 ; TByte m b2 ]
153 | maIX0p_to_DIR1 b ⇒ [ TByte m b]
154 | maDIR1_to_IX0p b ⇒ [ TByte m b]
155 (* cbeq/dbnz: legale se 1/2 operandi byte *)
156 | maINHA_and_IMM1 b ⇒ [ TByte m b]
157 | maINHX_and_IMM1 b ⇒ [ TByte m b]
158 | maIMM1_and_IMM1 b1 b2 ⇒ [ TByte m b1 ; TByte m b2 ]
159 | maDIR1_and_IMM1 b1 b2 ⇒ [ TByte m b1 ; TByte m b2 ]
160 | maIX0_and_IMM1 b ⇒ [ TByte m b]
161 | maIX0p_and_IMM1 b ⇒ [ TByte m b]
162 | maIX1_and_IMM1 b1 b2 ⇒ [ TByte m b1 ; TByte m b2 ]
163 | maIX1p_and_IMM1 b1 b2 ⇒ [ TByte m b1 ; TByte m b2 ]
164 | maSP1_and_IMM1 b1 b2 ⇒ [ TByte m b1 ; TByte m b2 ]
165 (* DIRn: legale se 1 operando byte *)
166 | maDIRn _ b ⇒ [ TByte m b]
167 (* DIRn_and_IMM1: legale se 2 operandi byte *)
168 | maDIRn_and_IMM1 _ b1 b2 ⇒ [ TByte m b1 ; TByte m b2 ]
169 (* TNY: legale se nessun operando *)
171 (* SRT: legale se nessun operando *)
175 (* trasformatore finale: mcu+opcode+instr_mode+args → list (t_byte8 m) *)
176 nlet rec bytes_of_pseudo_instr_mode_param_aux (m:mcu_type) (o:any_opcode m) (i:instr_mode) (p:MA_check i)
177 (param:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on param ≝
179 [ nil ⇒ None ? | cons hd tl ⇒
180 match (eq_anyop m o (fst4T … hd)) ⊗ (eq_instrmode i (snd4T … hd)) with
181 [ true ⇒ match thd4T … hd with
183 Some ? ([ (TByte m isab) ]@(args_picker m i p))
185 Some ? ([ (TByte m (w16h isaw)) ; (TByte m (w16l isaw)) ]@(args_picker m i p))
187 | false ⇒ bytes_of_pseudo_instr_mode_param_aux m o i p tl ]].
189 ndefinition bytes_of_pseudo_instr_mode_param ≝
190 λm:mcu_type.λo:any_opcode m.λi:instr_mode.λp:MA_check i.
191 bytes_of_pseudo_instr_mode_param_aux m o i p (opcode_table m).
193 (* ****************************** *)
194 (* APPROCCIO COMPILAZIONE AL VOLO *)
195 (* ****************************** *)
197 (* ausiliario di compile *)
198 ndefinition defined_option ≝
205 (* compila solo se l'intera istruzione+modalita'+argomenti ha riscontro nelle tabelle *)
206 ndefinition compile ≝
207 λmcu:mcu_type.λi:instr_mode.λop:opcode.λarg:MA_check i.
208 match bytes_of_pseudo_instr_mode_param mcu (anyOP mcu op) i arg
209 return λres:option ?.defined_option ? res → ?
211 [ None ⇒ λp:defined_option ? (None ?).False_rect_Type0 ? p
212 | Some x ⇒ λp:defined_option ? (Some ? x).x
215 (* detipatore del compilato: (t_byte8 m) → byte8 *)
216 nlet rec source_to_byte8_HC05_aux (p1:list (t_byte8 HC05)) (p2:list byte8) ≝
219 | cons hd tl ⇒ match hd with [ TByte b ⇒ source_to_byte8_HC05_aux tl (p2@[b]) ]
222 nlet rec source_to_byte8_HC08_aux (p1:list (t_byte8 HC08)) (p2:list byte8) ≝
225 | cons hd tl ⇒ match hd with [ TByte b ⇒ source_to_byte8_HC08_aux tl (p2@[b]) ]
228 nlet rec source_to_byte8_HCS08_aux (p1:list (t_byte8 HCS08)) (p2:list byte8) ≝
231 | cons hd tl ⇒ match hd with [ TByte b ⇒ source_to_byte8_HCS08_aux tl (p2@[b]) ]
234 nlet rec source_to_byte8_RS08_aux (p1:list (t_byte8 RS08)) (p2:list byte8) ≝
237 | cons hd tl ⇒ match hd with [ TByte b ⇒ source_to_byte8_RS08_aux tl (p2@[b]) ]
240 ndefinition source_to_byte8 ≝
243 return λm:mcu_type.list (t_byte8 m) → list byte8
245 [ HC05 ⇒ λl:list (t_byte8 HC05).source_to_byte8_HC05_aux l []
246 | HC08 ⇒ λl:list (t_byte8 HC08).source_to_byte8_HC08_aux l []
247 | HCS08 ⇒ λl:list (t_byte8 HCS08).source_to_byte8_HCS08_aux l []
248 | RS08 ⇒ λl:list (t_byte8 RS08).source_to_byte8_RS08_aux l []