source: Deliverables/D4.2-4.3/LIN/LinToAsm.ma @ 683

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

Changes from working on my PC.

File size: 5.8 KB
Line 
1include "cerco/Util.ma".
2include "cerco-intermediate-languages/utilities/BitVectorTrieSet.ma".
3include "cerco-intermediate-languages/LIN/LIN.ma".
4
5definition statement_labels ≝
6  λg: list (Identifier × nat).
7  λs: LINStatement g.
8  match s with
9  [ LIN_St_Goto lbl ⇒ set_insert ? lbl (set_empty ?)
10  | LIN_St_Label lbl ⇒ set_insert ? lbl (set_empty ?)
11  | LIN_St_CostLabel lbl ⇒ set_insert ? lbl (set_empty ?)
12  | LIN_St_CondAcc lbl ⇒ set_insert ? lbl (set_empty ?)
13  | _ ⇒ set_empty ?
14  ].
15
16definition function_labels_internal ≝
17  λglobals: list (Identifier × nat).
18  λlabels: BitVectorTrieSet 8.
19  λstatement: LINStatement globals.
20    set_union ? labels (statement_labels globals statement).
21
22(* dpm: A = Identifier *)
23definition function_labels: ∀A. ∀globals. ∀f. BitVectorTrieSet 8 ≝
24  λA: Type[0].
25  λglobals: list (Identifier × nat).
26  λf: A × (LINFunctionDefinition globals).
27  let 〈ignore, fun_def〉 ≝ f in
28  match fun_def return λ_. BitVectorTrieSet 8 with
29  [ LIN_Fu_Internal stmts ⇒
30      foldl ? ? (function_labels_internal globals) (set_empty 8) stmts
31  | LIN_Fu_External _ ⇒ set_empty ?
32  ].
33 
34definition program_labels_internal: ∀A. ∀globals. ∀labels. ∀funct. BitVectorTrieSet 8 ≝
35  λA: Type[0].
36  λglobals: list (Identifier × nat).
37  λlabels: BitVectorTrieSet 8.
38  λfunct: A × (LINFunctionDefinition globals).
39    set_union ? labels (function_labels ? globals funct).
40   
41definition program_labels ≝
42  λglobals: list (Identifier × nat).
43  λprogram.
44    foldl ? ? (program_labels_internal ? globals)
45              (set_empty 8) (LIN_Pr_funs globals program).
46   
47definition data_of_int ≝ λbv. DATA bv.
48definition data16_of_int ≝ λbv. DATA16 bv.
49definition accumulator_address ≝ register_address RegisterA.
50
51axiom ImplementedInRuntime: False.
52
53definition translate_statements ≝
54  λglobals: list (Identifier × nat).
55  λlin_statement: LINStatement globals.
56  match lin_statement with
57  [ LIN_St_Goto lbl ⇒ Some ? [ Jmp lbl ]
58  | LIN_St_Label lbl ⇒ Some ? [ Label lbl ]
59  | LIN_St_Comment _ ⇒ Some ? [ ]
60  | LIN_St_CostLabel lbl ⇒ Some ? [ Cost lbl ]
61  | LIN_St_Pop ⇒ Some ? [ Instruction (POP ? accumulator_address) ]
62  | LIN_St_Push ⇒ Some ? [ Instruction (PUSH ? accumulator_address) ]
63  | LIN_St_ClearCarry ⇒ Some ? [ Instruction (CLR ? CARRY) ]
64  | LIN_St_Return ⇒ Some ? [ Instruction (RET ?) ]
65  | LIN_St_CallId f ⇒ Some ? [ Call f ]
66  | LIN_St_OpAccs accs ⇒
67    match accs with
68    [ Mul ⇒ Some ? [ Instruction (MUL ? ACC_A ACC_B) ]
69    | Divu ⇒ Some ? [ Instruction (DIV ? ACC_A ACC_B) ]
70    | Modu ⇒ ?
71    ]
72  | LIN_St_Op1 op1 ⇒
73    match op1 with
74    [ Cmpl ⇒ Some ? [ Instruction (CPL ? ACC_A) ]
75    | Inc ⇒ Some ? [ Instruction (INC ? ACC_A) ]
76    ]
77  | LIN_St_Op2 op2 reg ⇒
78    match op2 with
79    [ Add ⇒ Some ? [ Instruction (ADD ? ACC_A (register_address reg)) ]
80    | Addc ⇒ Some ? [ Instruction (ADDC ? ACC_A (register_address reg)) ]
81    | Sub ⇒ Some ? [ Instruction (SUBB ? ACC_A (register_address reg)) ]
82    | And ⇒ Some ? [ Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, (register_address reg)〉))) ]
83    | Or ⇒ Some ? [ Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, (register_address reg)〉))) ]
84    | Xor ⇒ Some ? [ Instruction (XRL ? (inl ? ? 〈ACC_A, (register_address reg)〉)) ]
85    ]
86  | LIN_St_Int reg byte ⇒
87    let reg' ≝ register_address reg in
88      match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
89                                                    register;
90                                                    direct ]] x) → ? with
91      [ REGISTER _ ⇒ λreg: True.
92        Some ? [ Instruction (MOV ? (inl ? ? 〈register, (data_of_int byte)〉)) ]
93      | _ ⇒ ?
94      ] (subaddressing_modein … reg')
95  | _ ⇒ ?
96  ].
97
98      | DIRECT _ ⇒ λdirect: True.
99        Some ? [ Instruction (MOV ? (inr ? ? (inr ? ? 〈register, (data_of_int byte)〉))) ]
100      | ACC_A ⇒ λacc_a: True.
101        Some ? [ Instruction (MOV ? (inl ? ? 〈ACC_A, (data_of_int byte)〉)) ]
102      | _ ⇒ λother: False. ⊥
103      ] (subaddressing_modein … reg')
104
105  | LIN_St_FromAcc reg ⇒ ? (*
106    let reg' ≝ register_address reg in
107      match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
108                                                    register;
109                                                    direct ]] x) → ? with
110      [ REGISTER _ ⇒ λreg: True.
111        Some ? [ Instruction (MOV ? (inr ? ? 〈reg', ACC_A〉)) ]
112      | DIRECT _ ⇒ λdirect: True.
113        Some ? [ Instruction (MOV ? (inr ? ? 〈reg', ACC_A〉)) ]
114      | ACC_A ⇒ λacc_a: True.
115        Some ? [ Instruction (MOV ? (inr ? ? 〈reg', ACC_A〉)) ]
116      | _ ⇒ λother: False. ⊥
117      ] (subaddressing_modein … reg') *)
118  | LIN_St_ToAcc reg ⇒ ? (*
119    let reg' ≝ register_address reg in
120      match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
121                                                    register;
122                                                    direct ]] x) → ? with
123      [ REGISTER _ ⇒ λreg: True.
124        Some ? [ Instruction (MOV ? (inr ? ? 〈ACC_A, reg'〉)) ]
125      | DIRECT _ ⇒ λdirect: True.
126        Some ? [ Instruction (MOV ? (inr ? ? 〈ACC_A, reg'〉)) ]
127      | ACC_A ⇒ λacc_a: True.
128        Some ? [ Instruction (MOV ? (inr ? ? 〈ACC_A, reg'〉)) ]
129      | _ ⇒ λother: False. ⊥
130      ] (subaddressing_modein … reg') *)
131  | LIN_St_Address addr ⇒ ? (*
132    let look ≝ association ? ? eq_v addr global_addresses in
133    match look with
134    [ None ⇒ None
135    | Some look' ⇒
136      Some ? [ Instruction (MOV ? (inr ? ? (inr ? ? 〈DPTR, (data16_of_int look')〉))) ]
137    ] *)
138  | LIN_St_Load ⇒ Some ? [ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉)) ]
139  | LIN_St_Store ⇒ Some ? [ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉)) ]
140  | LIN_St_CondAcc lbl ⇒ ?
141  ].
Note: See TracBrowser for help on using the repository browser.