source: src/ASM/ASM.ma @ 714

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

Work on translation from LTL to LIN.

File size: 8.3 KB
Line 
1include "common/AST.ma".
2
3inductive addressing_mode: Type[0] ≝
4  DIRECT: Byte → addressing_mode
5| INDIRECT: Bit → addressing_mode
6| EXT_INDIRECT: Bit → addressing_mode
7| REGISTER: BitVector 3 → addressing_mode
8| ACC_A: addressing_mode
9| ACC_B: addressing_mode
10| DPTR: addressing_mode
11| DATA: Byte → addressing_mode
12| DATA16: Word → addressing_mode
13| ACC_DPTR: addressing_mode
14| ACC_PC: addressing_mode
15| EXT_INDIRECT_DPTR: addressing_mode
16| INDIRECT_DPTR: addressing_mode
17| CARRY: addressing_mode
18| BIT_ADDR: Byte → addressing_mode
19| N_BIT_ADDR: Byte → addressing_mode
20| RELATIVE: Byte → addressing_mode
21| ADDR11: Word11 → addressing_mode
22| ADDR16: Word → addressing_mode.
23
24inductive addressing_mode_tag : Type[0] ≝
25  direct: addressing_mode_tag
26| indirect: addressing_mode_tag
27| ext_indirect: addressing_mode_tag
28| register: addressing_mode_tag
29| acc_a: addressing_mode_tag
30| acc_b: addressing_mode_tag
31| dptr: addressing_mode_tag
32| data: addressing_mode_tag
33| data16: addressing_mode_tag
34| acc_dptr: addressing_mode_tag
35| acc_pc: addressing_mode_tag
36| ext_indirect_dptr: addressing_mode_tag
37| indirect_dptr: addressing_mode_tag
38| carry: addressing_mode_tag
39| bit_addr: addressing_mode_tag
40| n_bit_addr: addressing_mode_tag
41| relative: addressing_mode_tag
42| addr11: addressing_mode_tag
43| addr16: addressing_mode_tag.
44
45definition eq_a ≝
46  λa, b: addressing_mode_tag.
47    match a with
48      [ direct ⇒ match b with [ direct ⇒ true | _ ⇒ false ]
49      | indirect ⇒ match b with [ indirect ⇒ true | _ ⇒ false ]
50      | ext_indirect ⇒ match b with [ ext_indirect ⇒ true | _ ⇒ false ]
51      | register ⇒ match b with [ register ⇒ true | _ ⇒ false ]
52      | acc_a ⇒ match b with [ acc_a ⇒ true | _ ⇒ false ]
53      | acc_b ⇒ match b with [ acc_b ⇒ true | _ ⇒ false ]
54      | dptr ⇒ match b with [ dptr ⇒ true | _ ⇒ false ]
55      | data ⇒ match b with [ data ⇒ true | _ ⇒ false ]
56      | data16 ⇒ match b with [ data16 ⇒ true | _ ⇒ false ]
57      | acc_dptr ⇒ match b with [ acc_dptr ⇒ true | _ ⇒ false ]
58      | acc_pc ⇒ match b with [ acc_pc ⇒ true | _ ⇒ false ]
59      | ext_indirect_dptr ⇒ match b with [ ext_indirect_dptr ⇒ true | _ ⇒ false ]
60      | indirect_dptr ⇒ match b with [ indirect_dptr ⇒ true | _ ⇒ false ]
61      | carry ⇒ match b with [ carry ⇒ true | _ ⇒ false ]
62      | bit_addr ⇒ match b with [ bit_addr ⇒ true | _ ⇒ false ]
63      | n_bit_addr ⇒ match b with [ n_bit_addr ⇒ true | _ ⇒ false ]
64      | relative ⇒ match b with [ relative ⇒ true | _ ⇒ false ]
65      | addr11 ⇒ match b with [ addr11 ⇒ true | _ ⇒ false ]
66      | addr16 ⇒ match b with [ addr16 ⇒ true | _ ⇒ false ]
67      ].
68
69(* to avoid expansion... *)
70let rec is_a (d:addressing_mode_tag) (A:addressing_mode) on d ≝
71  match d with
72   [ direct ⇒ match A with [ DIRECT _ ⇒ true | _ ⇒ false ]
73   | indirect ⇒ match A with [ INDIRECT _ ⇒ true | _ ⇒ false ]
74   | ext_indirect ⇒ match A with [ EXT_INDIRECT _ ⇒ true | _ ⇒ false ]
75   | register ⇒ match A with [ REGISTER _ ⇒ true | _ ⇒ false ]
76   | acc_a ⇒ match A with [ ACC_A ⇒ true | _ ⇒ false ]
77   | acc_b ⇒ match A with [ ACC_B ⇒ true | _ ⇒ false ]
78   | dptr ⇒ match A with [ DPTR ⇒ true | _ ⇒ false ]
79   | data ⇒ match A with [ DATA _ ⇒ true | _ ⇒ false ]
80   | data16 ⇒ match A with [ DATA16 _ ⇒ true | _ ⇒ false ]
81   | acc_dptr ⇒ match A with [ ACC_DPTR ⇒ true | _ ⇒ false ]
82   | acc_pc ⇒ match A with [ ACC_PC ⇒ true | _ ⇒ false ]
83   | ext_indirect_dptr ⇒ match A with [ EXT_INDIRECT_DPTR ⇒ true | _ ⇒ false ]
84   | indirect_dptr ⇒ match A with [ INDIRECT_DPTR ⇒ true | _ ⇒ false ]
85   | carry ⇒ match A with [ CARRY ⇒ true | _ ⇒ false ]
86   | bit_addr ⇒ match A with [ BIT_ADDR _ ⇒ true | _ ⇒ false ]
87   | n_bit_addr ⇒ match A with [ N_BIT_ADDR _ ⇒ true | _ ⇒ false ]
88   | relative ⇒ match A with [ RELATIVE _ ⇒ true | _ ⇒ false ]
89   | addr11 ⇒ match A with [ ADDR11 _ ⇒ true | _ ⇒ false ]
90   | addr16 ⇒ match A with [ ADDR16 _ ⇒ true | _ ⇒ false ]].
91
92
93let rec is_in n (l: Vector addressing_mode_tag n) (A:addressing_mode) on l : bool ≝
94 match l return λm.λ_:Vector addressing_mode_tag m.bool with
95  [ VEmpty ⇒ false
96  | VCons m he (tl: Vector addressing_mode_tag m) ⇒
97     is_a he A ∨ is_in ? tl A ].
98
99record subaddressing_mode (n) (l: Vector addressing_mode_tag (S n)) : Type[0] ≝
100{
101  subaddressing_modeel:> addressing_mode;
102  subaddressing_modein: bool_to_Prop (is_in ? l subaddressing_modeel)
103}.
104
105coercion subaddressing_mode : ∀n.∀l:Vector addressing_mode_tag (S n).Type[0]
106 ≝ subaddressing_mode on _l: Vector addressing_mode_tag (S ?) to Type[0].
107
108coercion mk_subaddressing_mode :
109 ∀n.∀l:Vector addressing_mode_tag (S n).∀a:addressing_mode.
110  ∀p:bool_to_Prop (is_in ? l a).subaddressing_mode n l
111 ≝ mk_subaddressing_mode on a:addressing_mode to subaddressing_mode ? ?.
112
113inductive jump (A: Type[0]): Type[0] ≝
114  JC: A → jump A
115| JNC: A → jump A
116| JB: [[bit_addr]] → A → jump A
117| JNB: [[bit_addr]] → A → jump A
118| JBC: [[bit_addr]] → A → jump A
119| JZ: A → jump A
120| JNZ: A → jump A
121| CJNE:
122   [[acc_a]] × [[direct; data]] ⊎ [[register; indirect]] × [[data]] → A → jump A
123| DJNZ: [[register ; direct]] → A → jump A.
124
125inductive preinstruction (A: Type[0]) : Type[0] ≝
126  ADD: [[acc_a]] → [[ register ; direct ; indirect ; data ]] → preinstruction A
127| ADDC: [[acc_a]] → [[ register ; direct ; indirect ; data ]] → preinstruction A
128| SUBB: [[acc_a]] → [[ register ; direct ; indirect ; data ]] → preinstruction A
129| INC: [[ acc_a ; register ; direct ; indirect ; dptr ]] → preinstruction A
130| DEC: [[ acc_a ; register ; direct ; indirect ]] → preinstruction A
131| MUL: [[acc_a]] → [[acc_b]] → preinstruction A
132| DIV: [[acc_a]] → [[acc_b]] → preinstruction A
133| DA: [[acc_a]] → preinstruction A
134
135 (* logical operations *)
136| ANL:
137   [[acc_a]] × [[ register ; direct ; indirect ; data ]] ⊎
138   [[direct]] × [[ acc_a ; data ]] ⊎
139   [[carry]] × [[ bit_addr ; n_bit_addr]] → preinstruction A
140| ORL:
141   [[acc_a]] × [[ register ; data ; direct ; indirect ]] ⊎
142   [[direct]] × [[ acc_a ; data ]] ⊎
143   [[carry]] × [[ bit_addr ; n_bit_addr]] → preinstruction A
144| XRL:
145   [[acc_a]] × [[ data ; register ; direct ; indirect ]] ⊎
146   [[direct]] × [[ acc_a ; data ]] → preinstruction A
147| CLR: [[ acc_a ; carry ; bit_addr ]] → preinstruction A
148| CPL: [[ acc_a ; carry ; bit_addr ]] → preinstruction A
149| RL: [[acc_a]] → preinstruction A
150| RLC: [[acc_a]] → preinstruction A
151| RR: [[acc_a]] → preinstruction A
152| RRC: [[acc_a]] → preinstruction A
153| SWAP: [[acc_a]] → preinstruction A
154
155 (* data transfer *)
156| MOV:
157    [[acc_a]] × [[ register ; direct ; indirect ; data ]] ⊎
158    [[ register ; indirect ]] × [[ acc_a ; direct ; data ]] ⊎
159    [[direct]] × [[ acc_a ; register ; direct ; indirect ; data ]] ⊎
160    [[dptr]] × [[data16]] ⊎
161    [[carry]] × [[bit_addr]] ⊎
162    [[bit_addr]] × [[carry]] → preinstruction A
163| MOVC: [[acc_a]] → [[ acc_dptr ; acc_pc ]] → preinstruction A
164| MOVX:
165    [[acc_a]] × [[ ext_indirect ; ext_indirect_dptr ]] ⊎
166    [[ ext_indirect ; ext_indirect_dptr ]] × [[acc_a]] → preinstruction A
167| SETB: [[ carry ; bit_addr ]] → preinstruction A
168| PUSH: [[direct]] → preinstruction A
169| POP: [[direct]] → preinstruction A
170| XCH: [[acc_a]] → [[ register ; direct ; indirect ]] → preinstruction A
171| XCHD: [[acc_a]] → [[indirect]] → preinstruction A
172
173 (* program branching *)
174| Jump: jump A → preinstruction A
175| ACALL: [[addr11]] → preinstruction A
176| LCALL: [[addr16]] → preinstruction A
177| RET: preinstruction A
178| RETI: preinstruction A
179| AJMP: [[addr11]] → preinstruction A
180| LJMP: [[addr16]] → preinstruction A
181| SJMP: [[relative]] → preinstruction A
182| JMP: [[indirect_dptr]] → preinstruction A
183| NOP: preinstruction A.
184
185definition instruction ≝ preinstruction [[relative]].
186
187inductive labelled_instruction: Type[0] ≝
188  Instruction: instruction → labelled_instruction
189| Cost: Identifier → labelled_instruction
190| Jmp: Identifier → labelled_instruction
191| Call: Identifier → labelled_instruction
192| Mov: [[dptr]] → Identifier → labelled_instruction
193| Label: Identifier → labelled_instruction
194| WithLabel: jump Identifier → labelled_instruction.
195
196definition preamble ≝ list (Identifier × nat).
197
198definition assembly_program ≝ preamble × (list labelled_instruction).
Note: See TracBrowser for help on using the repository browser.