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

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

Initial commit of (part)-formalisation of LIN intermediate language.

File size: 4.1 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  λs: LINStatement.
7  match s with
8  [ LIN_St_Goto lbl ⇒ set_insert ? lbl (set_empty ?)
9  | LIN_St_Label lbl ⇒ set_insert ? lbl (set_empty ?)
10  | LIN_St_CostLabel lbl ⇒ set_insert ? lbl (set_empty ?)
11  | LIN_St_CondAcc lbl ⇒ set_insert ? lbl (set_empty ?)
12  | _ ⇒ set_empty ?
13  ].
14
15definition function_labels_internal: BitVectorTrieSet 8 → LINStatement → BitVectorTrieSet 8 ≝
16  λlabels: BitVectorTrieSet 8.
17  λstatement: LINStatement.
18    set_union ? labels (statement_labels statement).
19
20(* dpm: A = Identifier *)
21definition function_labels: ∀A. ∀f. BitVectorTrieSet 8 ≝
22  λA: Type[0].
23  λf: A × LINFunctionDefinition.
24  let 〈ignore, fun_def〉 ≝ f in
25  match fun_def return λ_. BitVectorTrieSet 8 with
26  [ LIN_Fu_Internal stmts ⇒
27      foldl ? ? function_labels_internal (set_empty 8) stmts
28  | LIN_Fu_External _ ⇒ set_empty ?
29  ].
30 
31definition program_labels_internal: ∀A. ∀labels. ∀funct. BitVectorTrieSet 8 ≝
32  λA: Type[0].
33  λlabels: BitVectorTrieSet 8.
34  λfunct: A × LINFunctionDefinition.
35    set_union ? labels (function_labels ? funct).
36   
37definition program_labels ≝
38  λprogram.
39    foldl ? ? (program_labels_internal ?) (set_empty 8) (LIN_Pr_funs program).
40   
41definition data_of_int ≝ λbv. DATA bv.
42definition data16_of_int ≝ λbv. DATA16 bv.
43definition accumulator_address ≝ register_address RegisterA.
44
45axiom ImplementedInRuntime: False.
46
47definition translate_statements ≝
48  λglobal_addresses.
49  λlin_statement.
50  match lin_statement with
51  [ LIN_St_Goto lbl ⇒ [ Jmp lbl ]
52  | LIN_St_Label lbl ⇒ [ Label lbl ]
53  | LIN_St_Comment _ ⇒ [ ]
54  | LIN_St_CostLabel lbl ⇒ [ Cost lbl ]
55  | LIN_St_Pop ⇒ [ Instruction (POP ? accumulator_address) ]
56  | LIN_St_Push ⇒ [ Instruction (PUSH ? accumulator_address) ]
57  | LIN_St_ClearCarry ⇒ [ Instruction (CLR ? CARRY) ]
58  | LIN_St_Return ⇒ [ Instruction (RET ?) ]
59  | LIN_St_CallId f ⇒ [ Call f ]
60  | LIN_St_OpAccs accs ⇒
61    match accs with
62    [ Mul ⇒ [ Instruction (MUL ? ACC_A ACC_B) ]
63    | Divu ⇒ [ Instruction (DIV ? ACC_A ACC_B) ]
64    | Modu ⇒ ?
65    ]
66  | LIN_St_Op1 op1 ⇒
67    match op1 with
68    [ Cmpl ⇒ [ Instruction (CPL ? ACC_A) ]
69    | Inc ⇒ [ Instruction (INC ? ACC_A) ]
70    ]
71  | LIN_St_Op2 op2 reg ⇒
72    match op2 with
73    [ Add ⇒ [ Instruction (ADD ? ACC_A (register_address reg)) ]
74    | Addc ⇒ [ Instruction (ADDC ? ACC_A (register_address reg)) ]
75    | Sub ⇒ [ Instruction (SUBB ? ACC_A (register_address reg)) ]
76    | And ⇒ [ Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, (register_address reg)〉))) ]
77    | Or ⇒ [ Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, (register_address reg)〉))) ]
78    | Xor ⇒ [ Instruction (XRL ? (inl ? ? 〈ACC_A, (register_address reg)〉)) ]
79    ]
80  | LIN_St_Int reg byte ⇒
81    let reg ≝ register_address reg in
82      match reg return λx. bool_to_Prop (is_in … [[ acc_a;
83                                                    register;
84                                                    direct ]] x) → ? with
85      [ REGISTER _ ⇒ λreg: True.
86        [ Instruction (MOV ? (inr ? ? 〈register, (data_of_int byte)〉)) ]
87      | DIRECT _ ⇒ λdirect: True.
88        [ Instruction (MOV ? (inr ? ? (inr ? ? 〈register, (data_of_int byte)〉))) ]
89      | ACC_A ⇒ λacc_a: True.
90        [ Instruction (MOV ? (inl ? ? 〈ACC_A, (data_of_int byte)〉)) ]
91      | _ ⇒ λother: False. ⊥
92      ] (subaddressing_modein … reg)
93  | LIN_St_FromAcc reg ⇒ [ Instruction (MOV ? (inr ? ? 〈(register_address reg), ACC_A〉)) ]
94  | LIN_St_ToAcc reg ⇒ [ Instruction (MOV ? (inl ? ? 〈ACC_A, (register_address reg)〉)) ]
95  | LIN_St_Address addr ⇒
96    let lookup ≝ association ? ? global_addresses addr in
97      [ Instruction (MOV ? (inr ? ? (inr ? ? 〈DPTR, (data16_of_int lookup)〉))) ]
98  | LIN_St_Load ⇒ [ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉)) ]
99  | LIN_St_Store ⇒ [ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉)) ]
100  | LIN_St_CondAcc lbl ⇒ ?
101  ].
Note: See TracBrowser for help on using the repository browser.