source: src/ASM/ASM.ma @ 1522

Last change on this file since 1522 was 1522, checked in by mulligan, 10 years ago

changes to preamble and lin to asm pass, resolved conflict in interpret

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