source: src/LIN/LINToASM.ma @ 699

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

More or less finished formalisation of LIN.

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