source: Deliverables/D4.1/Matita/ASM.ma @ 264

Last change on this file since 264 was 264, checked in by sacerdot, 9 years ago
  • new axiomatic data type for Strings
  • new file for Assembly
File size: 7.5 KB
Line 
1include "Either.ma".
2include "BitVectorTrie.ma".
3include "String.ma".
4
5interpretation "Cartesian" 'product A B = (Cartesian A B).
6notation "hvbox(a break ⊎ b)"
7 left associative with precedence 50
8for @{ 'disjoint_union $a $b }.
9interpretation "Either" 'disjoint_union A B = (Either A B).
10interpretation "Bool" 'or a b = (inclusive_disjunction a b).
11
12ninductive addressing_mode: Type[0] ≝
13  DIRECT: Byte → addressing_mode
14| INDIRECT: Bit → addressing_mode
15| EXT_INDIRECT: Bit → addressing_mode
16| REGISTER: Bit → Bit → Bit → addressing_mode
17| ACC_A: addressing_mode
18| ACC_B: addressing_mode
19| DPTR: addressing_mode
20| DATA: Byte → addressing_mode
21| DATA16: Word → addressing_mode
22| ACC_DPTR: addressing_mode
23| ACC_PC: addressing_mode
24| EXT_INDIRECT_DPTR: addressing_mode
25| INDIRECT_DPTR: addressing_mode
26| CARRY: addressing_mode
27| BIT_ADDR: Bit → addressing_mode
28| N_BIT_ADDR: Bit → addressing_mode
29| RELATIVE: Byte → addressing_mode
30| ADDR11: Word11 → addressing_mode
31| ADDR16: Word → addressing_mode.
32
33ninductive addressing_mode_tag : Type[0] ≝
34  direct: addressing_mode_tag
35| indirect: addressing_mode_tag
36| ext_indirect: addressing_mode_tag
37| register: addressing_mode_tag
38| acc_a: addressing_mode_tag
39| acc_b: addressing_mode_tag
40| dptr: addressing_mode_tag
41| data: addressing_mode_tag
42| data16: addressing_mode_tag
43| acc_dptr: addressing_mode_tag
44| acc_pc: addressing_mode_tag
45| ext_indirect_dptr: addressing_mode_tag
46| indirect_dptr: addressing_mode_tag
47| carry: addressing_mode_tag
48| bit_addr: addressing_mode_tag
49| n_bit_addr: addressing_mode_tag
50| relative: addressing_mode_tag
51| addr11: addressing_mode_tag
52| addr16: addressing_mode_tag.
53
54(* to avoid expansion... *)
55nlet rec is_a (d:addressing_mode_tag) (A:addressing_mode) on d ≝
56  match d with
57   [ direct ⇒ match A with [ DIRECT _ ⇒ true | _ ⇒ false ]
58   | indirect ⇒ match A with [ INDIRECT _ ⇒ true | _ ⇒ false ]
59   | ext_indirect ⇒ match A with [ EXT_INDIRECT _ ⇒ true | _ ⇒ false ]
60   | register ⇒ match A with [ REGISTER _ _ _ ⇒ true | _ ⇒ false ]
61   | acc_a ⇒ match A with [ ACC_A ⇒ true | _ ⇒ false ]
62   | acc_b ⇒ match A with [ ACC_B ⇒ true | _ ⇒ false ]
63   | dptr ⇒ match A with [ DPTR ⇒ true | _ ⇒ false ]
64   | data ⇒ match A with [ DATA _ ⇒ true | _ ⇒ false ]
65   | data16 ⇒ match A with [ DATA16 _ ⇒ true | _ ⇒ false ]
66   | acc_dptr ⇒ match A with [ ACC_DPTR ⇒ true | _ ⇒ false ]
67   | acc_pc ⇒ match A with [ ACC_PC ⇒ true | _ ⇒ false ]
68   | ext_indirect_dptr ⇒ match A with [ EXT_INDIRECT_DPTR ⇒ true | _ ⇒ false ]
69   | indirect_dptr ⇒ match A with [ INDIRECT_DPTR ⇒ true | _ ⇒ false ]
70   | carry ⇒ match A with [ CARRY ⇒ true | _ ⇒ false ]
71   | bit_addr ⇒ match A with [ BIT_ADDR _ ⇒ true | _ ⇒ false ]
72   | n_bit_addr ⇒ match A with [ N_BIT_ADDR _ ⇒ true | _ ⇒ false ]
73   | relative ⇒ match A with [ RELATIVE _ ⇒ true | _ ⇒ false ]
74   | addr11 ⇒ match A with [ ADDR11 _ ⇒ true | _ ⇒ false ]
75   | addr16 ⇒ match A with [ ADDR16 _ ⇒ true | _ ⇒ false ]].
76
77nlet rec is_in n (l: Vector addressing_mode_tag (S n)) (A:addressing_mode) on l : Bool ≝
78 match l return λm.λ_:Vector addressing_mode_tag m .∀K:m=S n.Bool with
79  [ Empty ⇒ λK.⊥
80  | Cons m he (tl: Vector addressing_mode_tag m) ⇒ λ_.
81     match m return λz.m = z → Bool with
82      [ Z ⇒ λ_.is_a he A
83      | S p ⇒ λK.is_a he A ∨ is_in p (? tl) A] (?: m=m)] (?: S n = S n).
84(* CSC: cast not working here: why? *)
85##[##4: #x; ncases K; napply x ]
86//; ndestruct.
87nqed.
88
89ndefinition bool_to_Prop ≝
90 λb. match b with [ true ⇒ True | false ⇒ False ].
91
92nrecord subaddressing_mode (n) (l: Vector addressing_mode_tag (S n)) : Type[0] ≝
93 { subaddressing_modeel:> addressing_mode;
94   subaddressing_modein: bool_to_Prop (is_in ? l subaddressing_modeel)
95 }.
96
97ncoercion subaddressing_mode : ∀n.∀l:Vector addressing_mode_tag (S n).Type[0]
98 ≝ subaddressing_mode on _l: Vector addressing_mode_tag (S ?) to Type[0].
99
100ncoercion mk_subaddressing_mode :
101 ∀n.∀l:Vector addressing_mode_tag (S n).∀a:addressing_mode.
102  ∀p:bool_to_Prop (is_in ? l a).subaddressing_mode n l
103 ≝ mk_subaddressing_mode on a:addressing_mode to subaddressing_mode ? ?.
104
105ninductive jump (A: Type[0]): Type[0] ≝
106  JC: A → jump A
107| JNC: A → jump A
108| JB: Bit → A → jump A
109| JNB: Bit → A → jump A
110| JBC: Bit → A → jump A
111| JZ: A → jump A
112| JNZ: A → jump A
113| CJNE:
114   [[acc_a]] × [[direct; data]] ⊎
115   [[register; indirect]] × [[data]] → A → jump A
116| DJNZ: [[register ; direct]] → A → jump A.
117
118ninductive preinstruction (A: Type[0]) : Type[0] ≝
119   ADD: [[acc_a]] × [[ register ; direct ; indirect ; data ]] -> preinstruction A
120 | ADDC: [[acc_a]] × [[ register ; direct ; indirect ; data ]] -> preinstruction A
121 | SUBB: [[acc_a]] × [[ register ; direct ; indirect ; data ]] -> preinstruction A
122 | INC: [[ acc_a ; register ; direct ; indirect ; dptr ]] -> preinstruction A
123 | DEC: [[ acc_a ; register ; direct ; indirect ]] -> preinstruction A
124 | MUL: [[acc_a]] × [[acc_b]] -> preinstruction A
125 | DIV: [[acc_a]] × [[acc_b]] -> preinstruction A
126 | DA: [[acc_a]] -> preinstruction A
127
128 (* logical operations *)
129 | ANL:
130   [[acc_a]] × [[ register ; direct ; indirect ; data ]] ⊎
131   [[direct]] × [[ acc_a ; data ]] ⊎
132   [[carry]] × [[ bit_addr ; n_bit_addr]] -> preinstruction A
133 | ORL:
134   [[acc_a]] × [[ register ; data ; direct ; indirect ]] ⊎
135   [[direct]] × [[ acc_a ; data ]] ⊎
136   [[carry]] × [[ bit_addr ; n_bit_addr]] -> preinstruction A
137 | XRL:
138   [[acc_a]] × [[ data ; register ; direct ; indirect ]] ⊎
139   [[direct]] × [[ acc_a ; data ]] -> preinstruction A
140 | CLR: [[ acc_a ; carry ; bit_addr ]] -> preinstruction A
141 | CPL: [[ acc_a ; carry ; bit_addr ]] -> preinstruction A
142 | RL: [[acc_a]] -> preinstruction A
143 | RLC: [[acc_a]] -> preinstruction A
144 | RR: [[acc_a]] -> preinstruction A
145 | RRC: [[acc_a]] -> preinstruction A
146 | SWAP: [[acc_a]] -> preinstruction A
147
148 (* data transfer *)
149 | MOV:
150    [[acc_a]] × [[ register ; direct ; indirect ; data ]] ⊎
151    [[ register ; indirect ]] × [[ acc_a ; direct ; data ]] ⊎
152    [[direct]] × [[ acc_a ; register ; direct ; indirect ; data ]] ⊎
153    [[dptr]] × [[data16]] ⊎
154    [[carry]] × [[bit_addr]] ⊎
155    [[bit_addr]] × [[carry]] -> preinstruction A
156 | MOVC: [[acc_a]] × [[ acc_dptr ; acc_pc ]] -> preinstruction A
157 | MOVX:
158    [[acc_a]] × [[ ext_indirect ; ext_indirect_dptr ]] ⊎
159    [[ ext_indirect ; ext_indirect_dptr ]] × [[acc_a]] -> preinstruction A
160 | SETB: [[ carry ; bit_addr ]] -> preinstruction A
161 | PUSH: [[direct]] -> preinstruction A
162 | POP: [[direct]] -> preinstruction A
163 | XCH: [[acc_a]] × [[ register ; direct ; indirect ]] -> preinstruction A
164 | XCHD: [[acc_a]] × [[indirect]] -> preinstruction A
165
166 (* program branching *)
167 | Jump: jump A → preinstruction A
168 | ACALL: [[addr11]] -> preinstruction A
169 | LCALL: [[addr16]] -> preinstruction A
170 | RET: preinstruction A
171 | RETI: preinstruction A
172 | AJMP: [[addr11]] -> preinstruction A
173 | LJMP: [[addr16]] -> preinstruction A
174 | SJMP: [[relative]] -> preinstruction A
175 | JMP: [[indirect_dptr]] -> preinstruction A
176 | NOP: preinstruction A.
177
178ndefinition instruction ≝ preinstruction [[relative]].
179
180ninductive labelled_instruction: Type[0] ≝
181   Instruction: instruction → labelled_instruction
182 | Cost: String → labelled_instruction
183 | Jmp: String → labelled_instruction
184 | Call: String → labelled_instruction
185 | Mov: [[dptr]] × String → labelled_instruction
186 | WithLabel: preinstruction String → labelled_instruction.
187
188ndefinition preamble ≝ List (String × Nat).
189
190ndefinition assembly_program ≝ preamble × (List labelled_instruction).
Note: See TracBrowser for help on using the repository browser.