1 | include "ASM/ASM.ma". |
---|
2 | include "ASM/Arithmetic.ma". |
---|
3 | include "ASM/Fetch.ma". |
---|
4 | include "ASM/Interpret.ma". |
---|
5 | |
---|
6 | inductive instruction_nature: Type[0] ≝ |
---|
7 | | goto: Word → instruction_nature |
---|
8 | | branch: Word → instruction_nature |
---|
9 | | direct_fun_call: Word → instruction_nature |
---|
10 | | ret: instruction_nature |
---|
11 | | other: instruction_nature. |
---|
12 | |
---|
13 | definition addr16_of_addr11: Word → Word11 → Word ≝ |
---|
14 | λpc: Word. |
---|
15 | λa: Word11. |
---|
16 | let 〈pc_upper, ignore〉 ≝ split … 8 8 pc in |
---|
17 | let 〈n1, n2〉 ≝ split … 4 4 pc_upper in |
---|
18 | let 〈b123, b〉 ≝ split … 3 8 a in |
---|
19 | let b1 ≝ get_index_v … b123 0 ? in |
---|
20 | let b2 ≝ get_index_v … b123 1 ? in |
---|
21 | let b3 ≝ get_index_v … b123 2 ? in |
---|
22 | let p5 ≝ get_index_v … n2 0 ? in |
---|
23 | (n1 @@ [[ p5; b1; b2; b3 ]]) @@ b. |
---|
24 | // |
---|
25 | qed. |
---|
26 | |
---|
27 | definition instruction_info: |
---|
28 | BitVectorTrie Byte 16 → Word → ? ≝ |
---|
29 | λmem. |
---|
30 | λpc. |
---|
31 | let 〈inst, next_pc, inst_cost〉 ≝ fetch mem pc in |
---|
32 | let 〈nature, next_pcs〉 ≝ |
---|
33 | match inst with |
---|
34 | [ RealInstruction ri ⇒ |
---|
35 | match ri with |
---|
36 | [ RET ⇒ 〈ret, [ ]〉 |
---|
37 | | RETI ⇒ 〈ret, [ ]〉 |
---|
38 | | JC addr ⇒ |
---|
39 | match addr return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with |
---|
40 | [ RELATIVE addr ⇒ λ_. |
---|
41 | let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in |
---|
42 | 〈branch addr, [ next_pc; addr ]〉 |
---|
43 | | _ ⇒ λp. match p in False with [ ] |
---|
44 | ] (subaddressing_modein … addr) |
---|
45 | | JNC addr ⇒ |
---|
46 | match addr return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with |
---|
47 | [ RELATIVE addr ⇒ λ_. |
---|
48 | let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in |
---|
49 | 〈branch addr, [ next_pc; addr ]〉 |
---|
50 | | _ ⇒ λp. match p in False with [ ] |
---|
51 | ] (subaddressing_modein … addr) |
---|
52 | | JZ addr ⇒ |
---|
53 | match addr return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with |
---|
54 | [ RELATIVE addr ⇒ λ_. |
---|
55 | let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in |
---|
56 | 〈branch addr, [ next_pc; addr ]〉 |
---|
57 | | _ ⇒ λp. match p in False with [ ] |
---|
58 | ] (subaddressing_modein … addr) |
---|
59 | | JNZ addr ⇒ |
---|
60 | match addr return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with |
---|
61 | [ RELATIVE addr ⇒ λ_. |
---|
62 | let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in |
---|
63 | 〈branch addr, [ next_pc; addr ]〉 |
---|
64 | | _ ⇒ λp. match p in False with [ ] |
---|
65 | ] (subaddressing_modein … addr) |
---|
66 | | JB addr1 addr2 ⇒ |
---|
67 | match addr2 return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with |
---|
68 | [ RELATIVE addr ⇒ λ_. |
---|
69 | let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in |
---|
70 | 〈branch addr, [ next_pc; addr ]〉 |
---|
71 | | _ ⇒ λp. match p in False with [ ] |
---|
72 | ] (subaddressing_modein … addr2) |
---|
73 | | JNB addr1 addr2 ⇒ |
---|
74 | match addr2 return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with |
---|
75 | [ RELATIVE addr ⇒ λ_. |
---|
76 | let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in |
---|
77 | 〈branch addr, [ next_pc; addr ]〉 |
---|
78 | | _ ⇒ λp. match p in False with [ ] |
---|
79 | ] (subaddressing_modein … addr2) |
---|
80 | | JBC addr1 addr2 ⇒ |
---|
81 | match addr2 return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with |
---|
82 | [ RELATIVE addr ⇒ λ_. |
---|
83 | let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in |
---|
84 | 〈branch addr, [ next_pc; addr ]〉 |
---|
85 | | _ ⇒ λp. match p in False with [ ] |
---|
86 | ] (subaddressing_modein … addr2) |
---|
87 | | DJNZ addr1 addr2 ⇒ |
---|
88 | match addr2 return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with |
---|
89 | [ RELATIVE addr ⇒ λ_. |
---|
90 | let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in |
---|
91 | 〈branch addr, [ next_pc; addr ]〉 |
---|
92 | | _ ⇒ λp. match p in False with [ ] |
---|
93 | ] (subaddressing_modein … addr2) |
---|
94 | | CJNE addr1 addr2 ⇒ |
---|
95 | match addr2 return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with |
---|
96 | [ RELATIVE addr ⇒ λ_. |
---|
97 | let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in |
---|
98 | 〈branch addr, [ next_pc; addr ]〉 |
---|
99 | | _ ⇒ λp. match p in False with [ ] |
---|
100 | ] (subaddressing_modein … addr2) |
---|
101 | | _ ⇒ 〈other, [ next_pc ]〉 |
---|
102 | ] |
---|
103 | | ACALL addr ⇒ |
---|
104 | match addr return λx. bool_to_Prop (is_in ? [[ addr11 ]] x) → ? with |
---|
105 | [ ADDR11 addr ⇒ λ_. |
---|
106 | let addr ≝ addr16_of_addr11 pc addr in |
---|
107 | 〈direct_fun_call addr, [ next_pc ]〉 |
---|
108 | | _ ⇒ λp. match p in False with [ ] |
---|
109 | ] (subaddressing_modein … addr) |
---|
110 | | LCALL addr ⇒ |
---|
111 | match addr return λx. bool_to_Prop (is_in ? [[ addr16 ]] x) → ? with |
---|
112 | [ ADDR16 addr ⇒ λ_. 〈direct_fun_call addr, [ next_pc ]〉 |
---|
113 | | _ ⇒ λp. match p in False with [ ] |
---|
114 | ] (subaddressing_modein … addr) |
---|
115 | | AJMP addr ⇒ |
---|
116 | match addr return λx. bool_to_Prop (is_in ? [[ addr11 ]] x) → ? with |
---|
117 | [ ADDR11 addr ⇒ λ_. |
---|
118 | let addr ≝ addr16_of_addr11 pc addr in |
---|
119 | 〈goto addr, [ addr ]〉 |
---|
120 | | _ ⇒ λp. match p in False with [ ] |
---|
121 | ] (subaddressing_modein … addr) |
---|
122 | | LJMP addr ⇒ |
---|
123 | match addr return λx. bool_to_Prop (is_in ? [[ addr16 ]] x) → ? with |
---|
124 | [ ADDR16 addr ⇒ λ_. 〈goto addr, [ addr ]〉 |
---|
125 | | _ ⇒ λp. match p in False with [ ] |
---|
126 | ] (subaddressing_modein … addr) |
---|
127 | | SJMP addr ⇒ |
---|
128 | match addr return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with |
---|
129 | [ RELATIVE addr ⇒ λ_. |
---|
130 | let 〈carry, addr〉 ≝ half_add 16 next_pc (sign_extend 8 8 addr) in |
---|
131 | 〈goto addr, [ addr ]〉 |
---|
132 | | _ ⇒ λp. match p in False with [ ] |
---|
133 | ] (subaddressing_modein … addr) |
---|
134 | | JMP addr ⇒ 〈other, [ next_pc ]〉 |
---|
135 | | MOVC acc_a addr ⇒ 〈other, [ next_pc ]〉 |
---|
136 | ] |
---|
137 | in |
---|
138 | 〈nature, next_pc, next_pcs, inst_cost〉. |
---|
139 | |
---|
140 | let rec compare |
---|
141 | (a: Type[0]) (the_list: list (a × nat)) |
---|
142 | on the_list: nat ≝ |
---|
143 | match the_list with |
---|
144 | [ nil ⇒ ⊥ (* XXX: was assert false *) |
---|
145 | | cons hd tl ⇒ |
---|
146 | match tl with |
---|
147 | [ nil ⇒ |
---|
148 | let 〈pc, cost〉 ≝ hd in |
---|
149 | cost |
---|
150 | | cons hd' tl' ⇒ |
---|
151 | let 〈pc1, cost1〉 ≝ hd in |
---|
152 | let 〈pc2, cost2〉 ≝ hd' in |
---|
153 | match eq_nat cost1 cost2 with |
---|
154 | [ true ⇒ max cost1 (compare … tl) |
---|
155 | | false ⇒ compare … tl' |
---|
156 | ] |
---|
157 | ] |
---|
158 | ]. |
---|
159 | cases daemon |
---|
160 | qed. |
---|
161 | |
---|
162 | let rec block_cost |
---|
163 | (mem: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie Byte 16) |
---|
164 | (the_list: list Word) (program_size: nat) |
---|
165 | on program_size: nat ≝ |
---|
166 | match program_size with |
---|
167 | [ O ⇒ 0 (* XXX: empty program *) |
---|
168 | | S program_size ⇒ |
---|
169 | match the_list with |
---|
170 | [ nil ⇒ 0 (* XXX: should be empty program *) |
---|
171 | | cons pc tl ⇒ |
---|
172 | match tl with |
---|
173 | [ nil ⇒ |
---|
174 | match lookup_opt … pc cost_labels with |
---|
175 | [ None ⇒ |
---|
176 | let 〈ignore, ignore, next_pcs, cost〉 ≝ instruction_info mem pc in |
---|
177 | let tail ≝ block_cost mem cost_labels next_pcs program_size in |
---|
178 | cost + tail |
---|
179 | | Some _ ⇒ O |
---|
180 | ] |
---|
181 | | _ ⇒ compare ? (map … (λpc. 〈pc, block_cost mem cost_labels [pc] program_size〉) the_list) |
---|
182 | ] |
---|
183 | ] |
---|
184 | ]. |
---|
185 | |
---|
186 | let rec traverse_code_internal |
---|
187 | (program: list Byte) (mem: BitVectorTrie Byte 16) |
---|
188 | (cost_labels: BitVectorTrie Byte 16) (pc: Word) (program_size: nat) |
---|
189 | on program: BitVectorTrie nat 8 ≝ |
---|
190 | let 〈ignore, newpc, ignore, ignore〉 ≝ instruction_info mem pc in |
---|
191 | match program with |
---|
192 | [ nil ⇒ Stub … |
---|
193 | | cons hd tl ⇒ |
---|
194 | match lookup_opt … pc cost_labels with |
---|
195 | [ None ⇒ traverse_code_internal tl mem cost_labels newpc program_size |
---|
196 | | Some lbl ⇒ |
---|
197 | let cost ≝ block_cost mem cost_labels [ pc ] program_size in |
---|
198 | let cost_mapping ≝ traverse_code_internal tl mem cost_labels newpc program_size in |
---|
199 | insert … lbl cost cost_mapping |
---|
200 | ] |
---|
201 | ]. |
---|
202 | |
---|
203 | definition traverse_code ≝ |
---|
204 | λprogram: list Byte. |
---|
205 | λmem: BitVectorTrie Byte 16. |
---|
206 | λcost_labels. |
---|
207 | λprogram_size: nat. |
---|
208 | traverse_code_internal program mem cost_labels (zero …) program_size. |
---|
209 | |
---|
210 | let rec first_cost_label_internal |
---|
211 | (mem: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie Byte 16) |
---|
212 | (program_size: nat) (oldpc: Word) |
---|
213 | on program_size: (Byte × nat) ≝ |
---|
214 | match program_size with |
---|
215 | [ O ⇒ ⊥ (* XXX: ummm ... ? *) |
---|
216 | | S program_size ⇒ |
---|
217 | match lookup_opt … oldpc cost_labels with |
---|
218 | [ None ⇒ |
---|
219 | let 〈nature, pc, ignore, inst_cost〉 ≝ instruction_info mem oldpc in |
---|
220 | match nature with |
---|
221 | [ direct_fun_call addr ⇒ |
---|
222 | let 〈lbl, cost〉 ≝ first_cost_label_internal mem cost_labels program_size addr in |
---|
223 | 〈lbl, inst_cost + cost〉 |
---|
224 | | other ⇒ |
---|
225 | let 〈lbl, cost〉 ≝ first_cost_label_internal mem cost_labels program_size pc in |
---|
226 | 〈lbl, inst_cost + cost〉 |
---|
227 | | _ ⇒ ⊥ (* XXX: was assert false in o'caml *) |
---|
228 | ] |
---|
229 | | Some cost ⇒ 〈cost, 0〉 |
---|
230 | ] |
---|
231 | ]. |
---|
232 | cases daemon |
---|
233 | qed. |
---|
234 | |
---|
235 | definition first_cost_label ≝ |
---|
236 | λmem: BitVectorTrie Byte 16. |
---|
237 | λcost_labels: BitVectorTrie Byte 16. |
---|
238 | λprogram_size: nat. |
---|
239 | first_cost_label_internal mem cost_labels program_size (zero …). |
---|
240 | |
---|
241 | definition initialize_costs ≝ |
---|
242 | λmem: BitVectorTrie Byte 16. |
---|
243 | λcost_labels: BitVectorTrie Byte 16. |
---|
244 | λcost_mapping: BitVectorTrie nat 8. |
---|
245 | λprogram_size: nat. |
---|
246 | let 〈lbl, cost〉 ≝ first_cost_label mem cost_labels program_size in |
---|
247 | let old_cost ≝ |
---|
248 | match lookup_opt … lbl cost_mapping with |
---|
249 | [ None ⇒ 0 |
---|
250 | | Some cost ⇒ cost |
---|
251 | ] |
---|
252 | in |
---|
253 | let new_cost ≝ old_cost + cost in |
---|
254 | insert … lbl new_cost cost_mapping. |
---|
255 | |
---|
256 | definition compute_costs ≝ |
---|
257 | λprogram: list Byte. |
---|
258 | λcost_labels: BitVectorTrie Byte 16. |
---|
259 | λhas_main: bool. |
---|
260 | let program_size ≝ |program| in |
---|
261 | let memory ≝ load_code_memory program in |
---|
262 | let costs_mapping ≝ traverse_code program memory cost_labels program_size in |
---|
263 | match has_main with |
---|
264 | [ true ⇒ |
---|
265 | initialize_costs memory cost_labels costs_mapping program_size |
---|
266 | | false ⇒ costs_mapping |
---|
267 | ]. |
---|