source: src/ASM/ASM.ma @ 1975

Last change on this file since 1975 was 1882, checked in by tranquil, 8 years ago

big update, alas incomplete:
joint changed a bit, and all BE languages need to be updated
started development of blocks to aid preservation results, but still incomplete
if it breaks too many things, feel free to roll back

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