source: src/LIN/LINToASM.ma @ 698

Last change on this file since 698 was 698, checked in by mulligan, 9 years ago

Commit with changes to files to get our files to typecheck.

File size: 11.0 KB
Line 
1include "ASM/Util.ma".
2include "utilities/BitVectorTrieSet.ma".
3include "LIN/LIN.ma".
4 
5let rec association (i: Identifier) (l: list (Identifier × nat))
6                    on l: member i (eq_bv ?) l → nat ≝
7  match l return λl. member i (eq_bv ?) l → nat with
8  [ nil ⇒ λabsd. ?
9  | cons hd tl ⇒
10    λprf: member i (eq_bv ?) (cons ? hd tl).
11      (match eq_bv ? (\fst hd) i return λb. eq_bv ? (\fst hd) i = b → nat with
12      [ true ⇒ λeq_prf. \snd hd
13      | false ⇒ λeq_prf. association i tl ?
14      ]) (refl ? (eq_bv ? (\fst hd) i))
15  ].
16  [ cases absd
17  | cases prf
18    [ > eq_prf
19      # H
20      cases H
21    | # H
22      assumption
23    ]
24  ]
25qed.
26
27definition statement_labels ≝
28  λg: list (Identifier × nat).
29  λs: LINStatement g.
30  match s with
31  [ LIN_St_Goto lbl ⇒ set_insert ? lbl (set_empty ?)
32  | LIN_St_Label lbl ⇒ set_insert ? lbl (set_empty ?)
33  | LIN_St_CostLabel lbl ⇒ set_insert ? lbl (set_empty ?)
34  | LIN_St_CondAcc lbl ⇒ set_insert ? lbl (set_empty ?)
35  | _ ⇒ set_empty ?
36  ].
37
38definition function_labels_internal ≝
39  λglobals: list (Identifier × nat).
40  λlabels: BitVectorTrieSet 8.
41  λstatement: LINStatement globals.
42    set_union ? labels (statement_labels globals statement).
43
44(* dpm: A = Identifier *)
45definition function_labels: ∀A. ∀globals. ∀f. BitVectorTrieSet 8 ≝
46  λA: Type[0].
47  λglobals: list (Identifier × nat).
48  λf: A × (LINFunctionDefinition globals).
49  let 〈ignore, fun_def〉 ≝ f in
50  match fun_def return λ_. BitVectorTrieSet 8 with
51  [ LIN_Fu_Internal stmts ⇒
52      foldl ? ? (function_labels_internal globals) (set_empty 8) stmts
53  | LIN_Fu_External _ ⇒ set_empty ?
54  ].
55 
56definition program_labels_internal: ∀A. ∀globals. ∀labels. ∀funct. BitVectorTrieSet 8 ≝
57  λA: Type[0].
58  λglobals: list (Identifier × nat).
59  λlabels: BitVectorTrieSet 8.
60  λfunct: A × (LINFunctionDefinition globals).
61    set_union ? labels (function_labels ? globals funct).
62   
63definition program_labels ≝
64  λglobals: list (Identifier × nat).
65  λprogram.
66    foldl ? ? (program_labels_internal ? globals)
67              (set_empty 8) (LIN_Pr_funs globals program).
68   
69definition data_of_int ≝ λbv. DATA bv.
70definition data16_of_int ≝ λbv. DATA16 (bitvector_of_nat 16 bv).
71definition accumulator_address ≝ DIRECT (bitvector_of_nat 8 224).
72
73axiom ImplementedInRuntime: False.
74
75definition translate_statements ≝
76  λglobals: list (Identifier × nat).
77  λlin_statement: LINStatement globals.
78  match lin_statement with
79  [ LIN_St_Goto lbl ⇒ [ Jmp lbl ]
80  | LIN_St_Label lbl ⇒ [ Label lbl ]
81  | LIN_St_Comment _ ⇒ [ ]
82  | LIN_St_CostLabel lbl ⇒ [ Cost lbl ]
83  | LIN_St_Pop ⇒ [ Instruction (POP ? accumulator_address) ]
84  | LIN_St_Push ⇒ [ Instruction (PUSH ? accumulator_address) ]
85  | LIN_St_ClearCarry ⇒ [ Instruction (CLR ? CARRY) ]
86  | LIN_St_Return ⇒ [ Instruction (RET ?) ]
87  | LIN_St_CallId f ⇒ [ Call f ]
88  | LIN_St_OpAccs accs ⇒
89    match accs with
90    [ Mul ⇒ [ Instruction (MUL ? ACC_A ACC_B) ]
91    | Divu ⇒ [ Instruction (DIV ? ACC_A ACC_B) ]
92    | Modu ⇒ ?
93    ]
94  | LIN_St_Op1 op1 ⇒
95    match op1 with
96    [ Cmpl ⇒ [ Instruction (CPL ? ACC_A) ]
97    | Inc ⇒ [ Instruction (INC ? ACC_A) ]
98    ]
99  | LIN_St_Op2 op2 reg ⇒
100    match op2 with
101    [ Add ⇒
102      let reg' ≝ register_address reg in
103      match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
104                                                     direct;
105                                                     register ]] x) → ? with
106      [ ACC_A ⇒ λacc_a: True.
107        [ Instruction (ADD ? ACC_A accumulator_address) ]
108      | DIRECT d ⇒ λdirect1: True.
109        [ Instruction (ADD ? ACC_A (DIRECT d)) ]
110      | REGISTER r ⇒ λregister1: True.
111        [ Instruction (ADD ? ACC_A (REGISTER r)) ]
112      | _ ⇒ λother: False. ⊥
113      ] (subaddressing_modein … reg')
114    | Addc ⇒
115      let reg' ≝ register_address reg in
116      match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
117                                                     direct;
118                                                     register ]] x) → ? with
119      [ ACC_A ⇒ λacc_a: True.
120        [ Instruction (ADDC ? ACC_A accumulator_address) ]
121      | DIRECT d ⇒ λdirect2: True.
122        [ Instruction (ADDC ? ACC_A (DIRECT d)) ]
123      | REGISTER r ⇒ λregister2: True.
124        [ Instruction (ADDC ? ACC_A (REGISTER r)) ]
125      | _ ⇒ λother: False. ⊥
126      ] (subaddressing_modein … reg')
127    | Sub ⇒
128      let reg' ≝ register_address reg in
129      match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
130                                                     direct;
131                                                     register ]] x) → ? with
132      [ ACC_A ⇒ λacc_a: True.
133        [ Instruction (SUBB ? ACC_A accumulator_address) ]
134      | DIRECT d ⇒ λdirect3: True.
135        [ Instruction (SUBB ? ACC_A (DIRECT d)) ]
136      | REGISTER r ⇒ λregister3: True.
137        [ Instruction (SUBB ? ACC_A (REGISTER r)) ]
138      | _ ⇒ λother: False. ⊥
139      ] (subaddressing_modein … reg')
140    | And ⇒
141      let reg' ≝ register_address reg in
142      match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
143                                                     direct;
144                                                     register ]] x) → ? with
145      [ ACC_A ⇒ λacc_a: True.
146        [ Instruction (NOP ?) ]
147      | DIRECT d ⇒ λdirect4: True.
148        [ Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))) ]
149      | REGISTER r ⇒ λregister4: True.
150        [ Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))) ]
151      | _ ⇒ λother: False. ⊥
152      ] (subaddressing_modein … reg')
153    | Or ⇒
154      let reg' ≝ register_address reg in
155      match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
156                                                     direct;
157                                                     register ]] x) → ? with
158      [ ACC_A ⇒ λacc_a: True.
159        [ Instruction (NOP ?) ]
160      | DIRECT d ⇒ λdirect5: True.
161        [ Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))) ]
162      | REGISTER r ⇒ λregister5: True.
163        [ Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))) ]
164      | _ ⇒ λother: False. ⊥
165      ] (subaddressing_modein … reg')
166    | Xor ⇒
167      let reg' ≝ register_address reg in
168      match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
169                                                     direct;
170                                                     register ]] x) → ? with
171      [ ACC_A ⇒ λacc_a: True.
172        [ Instruction (XRL ? (inr ? ? 〈accumulator_address, ACC_A〉)) ]
173      | DIRECT d ⇒ λdirect6: True.
174        [ Instruction (XRL ? (inl ? ? 〈ACC_A, DIRECT d〉)) ]
175      | REGISTER r ⇒ λregister6: True.
176        [ Instruction (XRL ? (inl ? ? 〈ACC_A, REGISTER r〉)) ]
177      | _ ⇒ λother: False. ⊥
178      ] (subaddressing_modein … reg')
179    ]
180  | LIN_St_Int reg byte ⇒
181    let reg' ≝ register_address reg in
182      match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
183                                                     direct;
184                                                     register ]] x) → ? with
185      [ REGISTER r ⇒ λregister7: True.
186        [ Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, (data_of_int byte)〉)))))) ]
187      | ACC_A ⇒ λacc: True.
188        [ Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, (data_of_int byte)〉)))))) ]
189      | DIRECT d ⇒ λdirect7: True.
190        [ Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, (data_of_int byte)〉))))) ]
191      | _ ⇒ λother: False. ⊥
192      ] (subaddressing_modein … reg')
193  | LIN_St_FromAcc reg ⇒
194    let reg' ≝ register_address reg in
195      match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
196                                                     direct;
197                                                     register ]] x) → ? with
198      [ REGISTER r ⇒ λregister8: True.
199        [ Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, ACC_A〉)))))) ]
200      | ACC_A ⇒ λacc: True.
201        [ Instruction (NOP ?) ]
202      | DIRECT d ⇒ λdirect8: True.
203        [ Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, ACC_A〉))))) ]
204      | _ ⇒ λother: False. ⊥
205      ] (subaddressing_modein … reg')
206  | LIN_St_ToAcc reg ⇒
207    let reg' ≝ register_address reg in
208      match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
209                                                     direct;
210                                                     register ]] x) → ? with
211      [ REGISTER r ⇒ λregister9: True.
212        [ Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))))) ]
213      | DIRECT d ⇒ λdirect9: True.
214        [ Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))))) ]
215      | ACC_A ⇒ λacc_a: True.
216        [ Instruction (NOP ?) ]
217      | _ ⇒ λother: False. ⊥
218      ] (subaddressing_modein … reg')
219  | LIN_St_Load ⇒ [ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉)) ]
220  | LIN_St_Store ⇒ [ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉)) ]
221  | LIN_St_Address addr proof ⇒
222    let look ≝ association addr globals proof in
223      [ Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉))))) ]
224  | LIN_St_CondAcc lbl ⇒
225    (* dpm: this should be handled in translate_code! *)
226    [ WithLabel (JNZ ? lbl) ]
227  ].
228  try assumption
229  try @ I
230  cases ImplementedInRuntime
231qed.
232
233definition translate_code ≝
234  λglobals: list (Identifier × nat).
235  λcode: list (LINStatement globals).
236    flatten ? (map ? ? (translate_statements globals) code).
237   
238definition translate_fun_def ≝
239  λglobals.
240  λid_def.
241    let 〈id, def〉 ≝ id_def in
242    match def with
243    [ LIN_Fu_Internal code ⇒ (Label id) :: (translate_code globals code)
244    | _ ⇒ [ ]
245    ].
246   
247definition translate_functs ≝
248  λglobals.
249  λexit_label.
250  λmain.
251  λfuncts.
252  let preamble ≝
253    match main with
254    [ None ⇒ [ ]
255    | Some main' ⇒ [ Call main' ; Label exit_label ; Jmp exit_label ]
256    ] in
257      preamble @ (flatten ? (map ? ? (translate_fun_def globals) functs)).
258
259definition globals_addr_internal ≝
260  λres_offset.
261  λx_size: Identifier × nat.
262    let 〈res, offset〉 ≝ res_offset in
263    let 〈x, size〉 ≝ x_size in
264      〈〈x, offset〉 :: res, offset + size〉.
265
266definition globals_addr ≝
267  λl.
268    foldl ? ? globals_addr_internal 〈[ ], 0〉 l.
269     
270(*   
271definition translate ≝
272  λp.
273  let prog_lbls ≝ program_labels p in
274  let exit_label ≝
275   
276let translate p =
277  let prog_lbls = prog_labels p in
278  let exit_label = Label.Gen.fresh_prefix prog_lbls "_exit" in
279  let glbls_addr = globals_addr p.LIN.vars in
280  let p =
281    { ASM.ppreamble = p.LIN.vars ;
282      ASM.pexit_label = exit_label ;
283      ASM.pcode =
284        translate_functs glbls_addr exit_label p.LIN.main p.LIN.functs ;
285      ASM.phas_main = p.LIN.main <> None } in
286  ASMInterpret.assembly p
287  *)
Note: See TracBrowser for help on using the repository browser.