1 | open Preamble |
---|
2 | |
---|
3 | open Deqsets |
---|
4 | |
---|
5 | open Setoids |
---|
6 | |
---|
7 | open Monad |
---|
8 | |
---|
9 | open Option |
---|
10 | |
---|
11 | open Extranat |
---|
12 | |
---|
13 | open Vector |
---|
14 | |
---|
15 | open Div_and_mod |
---|
16 | |
---|
17 | open Jmeq |
---|
18 | |
---|
19 | open Russell |
---|
20 | |
---|
21 | open List |
---|
22 | |
---|
23 | open Util |
---|
24 | |
---|
25 | open FoldStuff |
---|
26 | |
---|
27 | open Bool |
---|
28 | |
---|
29 | open Relations |
---|
30 | |
---|
31 | open Nat |
---|
32 | |
---|
33 | open BitVector |
---|
34 | |
---|
35 | open Hints_declaration |
---|
36 | |
---|
37 | open Core_notation |
---|
38 | |
---|
39 | open Pts |
---|
40 | |
---|
41 | open Logic |
---|
42 | |
---|
43 | open Types |
---|
44 | |
---|
45 | open BitVectorTrie |
---|
46 | |
---|
47 | open BitVectorTrieSet |
---|
48 | |
---|
49 | open State |
---|
50 | |
---|
51 | open String |
---|
52 | |
---|
53 | open Exp |
---|
54 | |
---|
55 | open Arithmetic |
---|
56 | |
---|
57 | open Integers |
---|
58 | |
---|
59 | open AST |
---|
60 | |
---|
61 | open LabelledObjects |
---|
62 | |
---|
63 | open Proper |
---|
64 | |
---|
65 | open PositiveMap |
---|
66 | |
---|
67 | open ErrorMessages |
---|
68 | |
---|
69 | open PreIdentifiers |
---|
70 | |
---|
71 | open Errors |
---|
72 | |
---|
73 | open Extralib |
---|
74 | |
---|
75 | open Lists |
---|
76 | |
---|
77 | open Positive |
---|
78 | |
---|
79 | open Identifiers |
---|
80 | |
---|
81 | open CostLabel |
---|
82 | |
---|
83 | open ASM |
---|
84 | |
---|
85 | open Extra_bool |
---|
86 | |
---|
87 | open Coqlib |
---|
88 | |
---|
89 | open Values |
---|
90 | |
---|
91 | open FrontEndVal |
---|
92 | |
---|
93 | open GenMem |
---|
94 | |
---|
95 | open FrontEndMem |
---|
96 | |
---|
97 | open Globalenvs |
---|
98 | |
---|
99 | open Sets |
---|
100 | |
---|
101 | open Listb |
---|
102 | |
---|
103 | open Graphs |
---|
104 | |
---|
105 | open I8051 |
---|
106 | |
---|
107 | open Order |
---|
108 | |
---|
109 | open Registers |
---|
110 | |
---|
111 | open Hide |
---|
112 | |
---|
113 | open Division |
---|
114 | |
---|
115 | open Z |
---|
116 | |
---|
117 | open BitVectorZ |
---|
118 | |
---|
119 | open Pointers |
---|
120 | |
---|
121 | open ByteValues |
---|
122 | |
---|
123 | open BackEndOps |
---|
124 | |
---|
125 | open Joint |
---|
126 | |
---|
127 | open Joint_LTL_LIN |
---|
128 | |
---|
129 | open LIN |
---|
130 | |
---|
131 | type aSM_universe = { id_univ : Identifiers.universe; |
---|
132 | current_funct : AST.ident; |
---|
133 | ident_map : ASM.identifier Identifiers.identifier_map; |
---|
134 | label_map : ASM.identifier Identifiers.identifier_map |
---|
135 | Identifiers.identifier_map; |
---|
136 | address_map : BitVector.word Identifiers.identifier_map; |
---|
137 | fresh_cost_label : Positive.pos } |
---|
138 | |
---|
139 | (** val aSM_universe_rect_Type4 : |
---|
140 | AST.ident List.list -> (Identifiers.universe -> AST.ident -> |
---|
141 | ASM.identifier Identifiers.identifier_map -> ASM.identifier |
---|
142 | Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word |
---|
143 | Identifiers.identifier_map -> __ -> Positive.pos -> 'a1) -> aSM_universe |
---|
144 | -> 'a1 **) |
---|
145 | let rec aSM_universe_rect_Type4 globals h_mk_ASM_universe x_3 = |
---|
146 | let { id_univ = id_univ0; current_funct = current_funct0; ident_map = |
---|
147 | ident_map0; label_map = label_map0; address_map = address_map0; |
---|
148 | fresh_cost_label = fresh_cost_label0 } = x_3 |
---|
149 | in |
---|
150 | h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0 |
---|
151 | address_map0 __ fresh_cost_label0 |
---|
152 | |
---|
153 | (** val aSM_universe_rect_Type5 : |
---|
154 | AST.ident List.list -> (Identifiers.universe -> AST.ident -> |
---|
155 | ASM.identifier Identifiers.identifier_map -> ASM.identifier |
---|
156 | Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word |
---|
157 | Identifiers.identifier_map -> __ -> Positive.pos -> 'a1) -> aSM_universe |
---|
158 | -> 'a1 **) |
---|
159 | let rec aSM_universe_rect_Type5 globals h_mk_ASM_universe x_5 = |
---|
160 | let { id_univ = id_univ0; current_funct = current_funct0; ident_map = |
---|
161 | ident_map0; label_map = label_map0; address_map = address_map0; |
---|
162 | fresh_cost_label = fresh_cost_label0 } = x_5 |
---|
163 | in |
---|
164 | h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0 |
---|
165 | address_map0 __ fresh_cost_label0 |
---|
166 | |
---|
167 | (** val aSM_universe_rect_Type3 : |
---|
168 | AST.ident List.list -> (Identifiers.universe -> AST.ident -> |
---|
169 | ASM.identifier Identifiers.identifier_map -> ASM.identifier |
---|
170 | Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word |
---|
171 | Identifiers.identifier_map -> __ -> Positive.pos -> 'a1) -> aSM_universe |
---|
172 | -> 'a1 **) |
---|
173 | let rec aSM_universe_rect_Type3 globals h_mk_ASM_universe x_7 = |
---|
174 | let { id_univ = id_univ0; current_funct = current_funct0; ident_map = |
---|
175 | ident_map0; label_map = label_map0; address_map = address_map0; |
---|
176 | fresh_cost_label = fresh_cost_label0 } = x_7 |
---|
177 | in |
---|
178 | h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0 |
---|
179 | address_map0 __ fresh_cost_label0 |
---|
180 | |
---|
181 | (** val aSM_universe_rect_Type2 : |
---|
182 | AST.ident List.list -> (Identifiers.universe -> AST.ident -> |
---|
183 | ASM.identifier Identifiers.identifier_map -> ASM.identifier |
---|
184 | Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word |
---|
185 | Identifiers.identifier_map -> __ -> Positive.pos -> 'a1) -> aSM_universe |
---|
186 | -> 'a1 **) |
---|
187 | let rec aSM_universe_rect_Type2 globals h_mk_ASM_universe x_9 = |
---|
188 | let { id_univ = id_univ0; current_funct = current_funct0; ident_map = |
---|
189 | ident_map0; label_map = label_map0; address_map = address_map0; |
---|
190 | fresh_cost_label = fresh_cost_label0 } = x_9 |
---|
191 | in |
---|
192 | h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0 |
---|
193 | address_map0 __ fresh_cost_label0 |
---|
194 | |
---|
195 | (** val aSM_universe_rect_Type1 : |
---|
196 | AST.ident List.list -> (Identifiers.universe -> AST.ident -> |
---|
197 | ASM.identifier Identifiers.identifier_map -> ASM.identifier |
---|
198 | Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word |
---|
199 | Identifiers.identifier_map -> __ -> Positive.pos -> 'a1) -> aSM_universe |
---|
200 | -> 'a1 **) |
---|
201 | let rec aSM_universe_rect_Type1 globals h_mk_ASM_universe x_11 = |
---|
202 | let { id_univ = id_univ0; current_funct = current_funct0; ident_map = |
---|
203 | ident_map0; label_map = label_map0; address_map = address_map0; |
---|
204 | fresh_cost_label = fresh_cost_label0 } = x_11 |
---|
205 | in |
---|
206 | h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0 |
---|
207 | address_map0 __ fresh_cost_label0 |
---|
208 | |
---|
209 | (** val aSM_universe_rect_Type0 : |
---|
210 | AST.ident List.list -> (Identifiers.universe -> AST.ident -> |
---|
211 | ASM.identifier Identifiers.identifier_map -> ASM.identifier |
---|
212 | Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word |
---|
213 | Identifiers.identifier_map -> __ -> Positive.pos -> 'a1) -> aSM_universe |
---|
214 | -> 'a1 **) |
---|
215 | let rec aSM_universe_rect_Type0 globals h_mk_ASM_universe x_13 = |
---|
216 | let { id_univ = id_univ0; current_funct = current_funct0; ident_map = |
---|
217 | ident_map0; label_map = label_map0; address_map = address_map0; |
---|
218 | fresh_cost_label = fresh_cost_label0 } = x_13 |
---|
219 | in |
---|
220 | h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0 |
---|
221 | address_map0 __ fresh_cost_label0 |
---|
222 | |
---|
223 | (** val id_univ : |
---|
224 | AST.ident List.list -> aSM_universe -> Identifiers.universe **) |
---|
225 | let rec id_univ globals xxx = |
---|
226 | xxx.id_univ |
---|
227 | |
---|
228 | (** val current_funct : AST.ident List.list -> aSM_universe -> AST.ident **) |
---|
229 | let rec current_funct globals xxx = |
---|
230 | xxx.current_funct |
---|
231 | |
---|
232 | (** val ident_map : |
---|
233 | AST.ident List.list -> aSM_universe -> ASM.identifier |
---|
234 | Identifiers.identifier_map **) |
---|
235 | let rec ident_map globals xxx = |
---|
236 | xxx.ident_map |
---|
237 | |
---|
238 | (** val label_map : |
---|
239 | AST.ident List.list -> aSM_universe -> ASM.identifier |
---|
240 | Identifiers.identifier_map Identifiers.identifier_map **) |
---|
241 | let rec label_map globals xxx = |
---|
242 | xxx.label_map |
---|
243 | |
---|
244 | (** val address_map : |
---|
245 | AST.ident List.list -> aSM_universe -> BitVector.word |
---|
246 | Identifiers.identifier_map **) |
---|
247 | let rec address_map globals xxx = |
---|
248 | xxx.address_map |
---|
249 | |
---|
250 | (** val fresh_cost_label : |
---|
251 | AST.ident List.list -> aSM_universe -> Positive.pos **) |
---|
252 | let rec fresh_cost_label globals xxx = |
---|
253 | xxx.fresh_cost_label |
---|
254 | |
---|
255 | (** val aSM_universe_inv_rect_Type4 : |
---|
256 | AST.ident List.list -> aSM_universe -> (Identifiers.universe -> AST.ident |
---|
257 | -> ASM.identifier Identifiers.identifier_map -> ASM.identifier |
---|
258 | Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word |
---|
259 | Identifiers.identifier_map -> __ -> Positive.pos -> __ -> 'a1) -> 'a1 **) |
---|
260 | let aSM_universe_inv_rect_Type4 x1 hterm h1 = |
---|
261 | let hcut = aSM_universe_rect_Type4 x1 h1 hterm in hcut __ |
---|
262 | |
---|
263 | (** val aSM_universe_inv_rect_Type3 : |
---|
264 | AST.ident List.list -> aSM_universe -> (Identifiers.universe -> AST.ident |
---|
265 | -> ASM.identifier Identifiers.identifier_map -> ASM.identifier |
---|
266 | Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word |
---|
267 | Identifiers.identifier_map -> __ -> Positive.pos -> __ -> 'a1) -> 'a1 **) |
---|
268 | let aSM_universe_inv_rect_Type3 x1 hterm h1 = |
---|
269 | let hcut = aSM_universe_rect_Type3 x1 h1 hterm in hcut __ |
---|
270 | |
---|
271 | (** val aSM_universe_inv_rect_Type2 : |
---|
272 | AST.ident List.list -> aSM_universe -> (Identifiers.universe -> AST.ident |
---|
273 | -> ASM.identifier Identifiers.identifier_map -> ASM.identifier |
---|
274 | Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word |
---|
275 | Identifiers.identifier_map -> __ -> Positive.pos -> __ -> 'a1) -> 'a1 **) |
---|
276 | let aSM_universe_inv_rect_Type2 x1 hterm h1 = |
---|
277 | let hcut = aSM_universe_rect_Type2 x1 h1 hterm in hcut __ |
---|
278 | |
---|
279 | (** val aSM_universe_inv_rect_Type1 : |
---|
280 | AST.ident List.list -> aSM_universe -> (Identifiers.universe -> AST.ident |
---|
281 | -> ASM.identifier Identifiers.identifier_map -> ASM.identifier |
---|
282 | Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word |
---|
283 | Identifiers.identifier_map -> __ -> Positive.pos -> __ -> 'a1) -> 'a1 **) |
---|
284 | let aSM_universe_inv_rect_Type1 x1 hterm h1 = |
---|
285 | let hcut = aSM_universe_rect_Type1 x1 h1 hterm in hcut __ |
---|
286 | |
---|
287 | (** val aSM_universe_inv_rect_Type0 : |
---|
288 | AST.ident List.list -> aSM_universe -> (Identifiers.universe -> AST.ident |
---|
289 | -> ASM.identifier Identifiers.identifier_map -> ASM.identifier |
---|
290 | Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word |
---|
291 | Identifiers.identifier_map -> __ -> Positive.pos -> __ -> 'a1) -> 'a1 **) |
---|
292 | let aSM_universe_inv_rect_Type0 x1 hterm h1 = |
---|
293 | let hcut = aSM_universe_rect_Type0 x1 h1 hterm in hcut __ |
---|
294 | |
---|
295 | (** val aSM_universe_jmdiscr : |
---|
296 | AST.ident List.list -> aSM_universe -> aSM_universe -> __ **) |
---|
297 | let aSM_universe_jmdiscr a1 x y = |
---|
298 | Logic.eq_rect_Type2 x |
---|
299 | (let { id_univ = a0; current_funct = a10; ident_map = a2; label_map = a3; |
---|
300 | address_map = a4; fresh_cost_label = a6 } = x |
---|
301 | in |
---|
302 | Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __)) y |
---|
303 | |
---|
304 | (** val report_cost : |
---|
305 | AST.ident List.list -> CostLabel.costlabel -> Types.unit0 |
---|
306 | Monad.smax_def__o__monad **) |
---|
307 | let report_cost globals cl = |
---|
308 | Obj.magic (fun u -> |
---|
309 | let clw = Identifiers.word_of_identifier PreIdentifiers.CostTag cl in |
---|
310 | (match Positive.leb u.fresh_cost_label clw with |
---|
311 | | Bool.True -> |
---|
312 | { Types.fst = { id_univ = u.id_univ; current_funct = u.current_funct; |
---|
313 | ident_map = u.ident_map; label_map = u.label_map; address_map = |
---|
314 | u.address_map; fresh_cost_label = (Positive.succ clw) }; Types.snd = |
---|
315 | Types.It } |
---|
316 | | Bool.False -> { Types.fst = u; Types.snd = Types.It })) |
---|
317 | |
---|
318 | (** val new_ASM_universe : Joint.joint_program -> aSM_universe **) |
---|
319 | let new_ASM_universe p = |
---|
320 | let globals_addr_internal = fun res_offset x_size -> |
---|
321 | let { Types.fst = res; Types.snd = offset } = res_offset in |
---|
322 | let { Types.fst = eta6; Types.snd = data } = x_size in |
---|
323 | let { Types.fst = x; Types.snd = region } = eta6 in |
---|
324 | { Types.fst = |
---|
325 | (Identifiers.add PreIdentifiers.SymbolTag res x |
---|
326 | (BitVectorZ.bitvector_of_Z (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
327 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
328 | Nat.O)))))))))))))))) offset)); Types.snd = |
---|
329 | (Z.zplus offset (Z.z_of_nat (Globalenvs.size_init_data_list data))) } |
---|
330 | in |
---|
331 | let addresses = |
---|
332 | Util.foldl globals_addr_internal { Types.fst = |
---|
333 | (Identifiers.empty_map PreIdentifiers.SymbolTag); Types.snd = |
---|
334 | (Z.zopp |
---|
335 | (Z.z_of_nat |
---|
336 | (Joint.globals_stacksize (Joint.lin_params_to_params LIN.lIN) p))) } |
---|
337 | p.Joint.joint_prog.AST.prog_vars |
---|
338 | in |
---|
339 | { id_univ = Positive.One; current_funct = Positive.One; ident_map = |
---|
340 | (Identifiers.empty_map PreIdentifiers.SymbolTag); label_map = |
---|
341 | (Identifiers.empty_map PreIdentifiers.SymbolTag); address_map = |
---|
342 | addresses.Types.fst; fresh_cost_label = Positive.One } |
---|
343 | |
---|
344 | (** val identifier_of_label : |
---|
345 | AST.ident List.list -> Graphs.label -> ASM.identifier |
---|
346 | Monad.smax_def__o__monad **) |
---|
347 | let identifier_of_label g l = |
---|
348 | Obj.magic (fun u -> |
---|
349 | let current = u.current_funct in |
---|
350 | let lmap = |
---|
351 | Identifiers.lookup_def PreIdentifiers.SymbolTag u.label_map current |
---|
352 | (Identifiers.empty_map PreIdentifiers.LabelTag) |
---|
353 | in |
---|
354 | let { Types.fst = eta7; Types.snd = lmap0 } = |
---|
355 | match Identifiers.lookup PreIdentifiers.LabelTag lmap l with |
---|
356 | | Types.None -> |
---|
357 | let { Types.fst = id; Types.snd = univ } = |
---|
358 | Identifiers.fresh PreIdentifiers.ASMTag u.id_univ |
---|
359 | in |
---|
360 | { Types.fst = { Types.fst = id; Types.snd = univ }; Types.snd = |
---|
361 | (Identifiers.add PreIdentifiers.LabelTag lmap l id) } |
---|
362 | | Types.Some id -> |
---|
363 | { Types.fst = { Types.fst = id; Types.snd = u.id_univ }; Types.snd = |
---|
364 | lmap } |
---|
365 | in |
---|
366 | let { Types.fst = id; Types.snd = univ } = eta7 in |
---|
367 | { Types.fst = { id_univ = univ; current_funct = current; ident_map = |
---|
368 | u.ident_map; label_map = |
---|
369 | (Identifiers.add PreIdentifiers.SymbolTag u.label_map current lmap0); |
---|
370 | address_map = u.address_map; fresh_cost_label = u.fresh_cost_label }; |
---|
371 | Types.snd = id }) |
---|
372 | |
---|
373 | (** val identifier_of_ident : |
---|
374 | AST.ident List.list -> AST.ident -> ASM.identifier |
---|
375 | Monad.smax_def__o__monad **) |
---|
376 | let identifier_of_ident g i = |
---|
377 | Obj.magic (fun u -> |
---|
378 | let imap = u.ident_map in |
---|
379 | let { Types.fst = eta8; Types.snd = imap0 } = |
---|
380 | match Identifiers.lookup PreIdentifiers.SymbolTag imap i with |
---|
381 | | Types.None -> |
---|
382 | let { Types.fst = id; Types.snd = univ } = |
---|
383 | Identifiers.fresh PreIdentifiers.ASMTag u.id_univ |
---|
384 | in |
---|
385 | { Types.fst = { Types.fst = id; Types.snd = univ }; Types.snd = |
---|
386 | (Identifiers.add PreIdentifiers.SymbolTag imap i id) } |
---|
387 | | Types.Some id -> |
---|
388 | { Types.fst = { Types.fst = id; Types.snd = u.id_univ }; Types.snd = |
---|
389 | imap } |
---|
390 | in |
---|
391 | let { Types.fst = id; Types.snd = univ } = eta8 in |
---|
392 | { Types.fst = { id_univ = univ; current_funct = u.current_funct; |
---|
393 | ident_map = imap0; label_map = u.label_map; address_map = u.address_map; |
---|
394 | fresh_cost_label = u.fresh_cost_label }; Types.snd = id }) |
---|
395 | |
---|
396 | (** val start_funct_translation : |
---|
397 | AST.ident List.list -> (AST.ident, Joint.joint_function) Types.prod -> |
---|
398 | Types.unit0 Monad.smax_def__o__monad **) |
---|
399 | let start_funct_translation g id_f = |
---|
400 | Obj.magic (fun u -> { Types.fst = { id_univ = u.id_univ; current_funct = |
---|
401 | id_f.Types.fst; ident_map = u.ident_map; label_map = u.label_map; |
---|
402 | address_map = u.address_map; fresh_cost_label = u.fresh_cost_label }; |
---|
403 | Types.snd = Types.It }) |
---|
404 | |
---|
405 | (** val address_of_ident : |
---|
406 | __ List.list -> __ -> ASM.subaddressing_mode Monad.smax_def__o__monad **) |
---|
407 | let address_of_ident globals i = |
---|
408 | Obj.magic (fun u -> { Types.fst = u; Types.snd = (ASM.DATA16 |
---|
409 | (Identifiers.lookup_safe PreIdentifiers.SymbolTag u.address_map |
---|
410 | (Obj.magic i))) }) |
---|
411 | |
---|
412 | (** val aSM_fresh : |
---|
413 | AST.ident List.list -> ASM.identifier Monad.smax_def__o__monad **) |
---|
414 | let aSM_fresh g = |
---|
415 | Obj.magic (fun u -> |
---|
416 | let { Types.fst = id; Types.snd = univ } = |
---|
417 | Identifiers.fresh PreIdentifiers.ASMTag u.id_univ |
---|
418 | in |
---|
419 | { Types.fst = { id_univ = univ; current_funct = u.current_funct; |
---|
420 | ident_map = u.ident_map; label_map = u.label_map; address_map = |
---|
421 | u.address_map; fresh_cost_label = u.fresh_cost_label }; Types.snd = id }) |
---|
422 | |
---|
423 | (** val register_address : I8051.register -> ASM.subaddressing_mode **) |
---|
424 | let register_address r = |
---|
425 | (match r with |
---|
426 | | I8051.Register00 -> |
---|
427 | (fun _ -> ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, |
---|
428 | (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O, |
---|
429 | Bool.False, Vector.VEmpty))))))) |
---|
430 | | I8051.Register01 -> |
---|
431 | (fun _ -> ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, |
---|
432 | (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O, |
---|
433 | Bool.True, Vector.VEmpty))))))) |
---|
434 | | I8051.Register02 -> |
---|
435 | (fun _ -> ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, |
---|
436 | (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, |
---|
437 | Bool.False, Vector.VEmpty))))))) |
---|
438 | | I8051.Register03 -> |
---|
439 | (fun _ -> ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, |
---|
440 | (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, |
---|
441 | Bool.True, Vector.VEmpty))))))) |
---|
442 | | I8051.Register04 -> |
---|
443 | (fun _ -> ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, |
---|
444 | (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O, |
---|
445 | Bool.False, Vector.VEmpty))))))) |
---|
446 | | I8051.Register05 -> |
---|
447 | (fun _ -> ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, |
---|
448 | (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O, |
---|
449 | Bool.True, Vector.VEmpty))))))) |
---|
450 | | I8051.Register06 -> |
---|
451 | (fun _ -> ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, |
---|
452 | (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, |
---|
453 | Bool.False, Vector.VEmpty))))))) |
---|
454 | | I8051.Register07 -> |
---|
455 | (fun _ -> ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, |
---|
456 | (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, |
---|
457 | Bool.True, Vector.VEmpty))))))) |
---|
458 | | I8051.Register10 -> |
---|
459 | (fun _ -> ASM.DIRECT |
---|
460 | (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
461 | (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r))) |
---|
462 | | I8051.Register11 -> |
---|
463 | (fun _ -> ASM.DIRECT |
---|
464 | (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
465 | (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r))) |
---|
466 | | I8051.Register12 -> |
---|
467 | (fun _ -> ASM.DIRECT |
---|
468 | (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
469 | (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r))) |
---|
470 | | I8051.Register13 -> |
---|
471 | (fun _ -> ASM.DIRECT |
---|
472 | (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
473 | (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r))) |
---|
474 | | I8051.Register14 -> |
---|
475 | (fun _ -> ASM.DIRECT |
---|
476 | (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
477 | (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r))) |
---|
478 | | I8051.Register15 -> |
---|
479 | (fun _ -> ASM.DIRECT |
---|
480 | (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
481 | (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r))) |
---|
482 | | I8051.Register16 -> |
---|
483 | (fun _ -> ASM.DIRECT |
---|
484 | (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
485 | (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r))) |
---|
486 | | I8051.Register17 -> |
---|
487 | (fun _ -> ASM.DIRECT |
---|
488 | (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
489 | (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r))) |
---|
490 | | I8051.Register20 -> |
---|
491 | (fun _ -> ASM.DIRECT |
---|
492 | (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
493 | (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r))) |
---|
494 | | I8051.Register21 -> |
---|
495 | (fun _ -> ASM.DIRECT |
---|
496 | (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
497 | (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r))) |
---|
498 | | I8051.Register22 -> |
---|
499 | (fun _ -> ASM.DIRECT |
---|
500 | (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
501 | (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r))) |
---|
502 | | I8051.Register23 -> |
---|
503 | (fun _ -> ASM.DIRECT |
---|
504 | (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
505 | (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r))) |
---|
506 | | I8051.Register24 -> |
---|
507 | (fun _ -> ASM.DIRECT |
---|
508 | (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
509 | (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r))) |
---|
510 | | I8051.Register25 -> |
---|
511 | (fun _ -> ASM.DIRECT |
---|
512 | (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
513 | (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r))) |
---|
514 | | I8051.Register26 -> |
---|
515 | (fun _ -> ASM.DIRECT |
---|
516 | (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
517 | (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r))) |
---|
518 | | I8051.Register27 -> |
---|
519 | (fun _ -> ASM.DIRECT |
---|
520 | (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
521 | (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r))) |
---|
522 | | I8051.Register30 -> |
---|
523 | (fun _ -> ASM.DIRECT |
---|
524 | (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
525 | (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r))) |
---|
526 | | I8051.Register31 -> |
---|
527 | (fun _ -> ASM.DIRECT |
---|
528 | (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
529 | (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r))) |
---|
530 | | I8051.Register32 -> |
---|
531 | (fun _ -> ASM.DIRECT |
---|
532 | (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
533 | (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r))) |
---|
534 | | I8051.Register33 -> |
---|
535 | (fun _ -> ASM.DIRECT |
---|
536 | (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
537 | (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r))) |
---|
538 | | I8051.Register34 -> |
---|
539 | (fun _ -> ASM.DIRECT |
---|
540 | (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
541 | (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r))) |
---|
542 | | I8051.Register35 -> |
---|
543 | (fun _ -> ASM.DIRECT |
---|
544 | (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
545 | (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r))) |
---|
546 | | I8051.Register36 -> |
---|
547 | (fun _ -> ASM.DIRECT |
---|
548 | (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
549 | (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r))) |
---|
550 | | I8051.Register37 -> |
---|
551 | (fun _ -> ASM.DIRECT |
---|
552 | (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
553 | (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r))) |
---|
554 | | I8051.RegisterA -> (fun _ -> ASM.ACC_A) |
---|
555 | | I8051.RegisterB -> |
---|
556 | (fun _ -> ASM.DIRECT |
---|
557 | (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
558 | (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
559 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
560 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
561 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
562 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
563 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
564 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
565 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
566 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
567 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
568 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
569 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
570 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
571 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
572 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
573 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
574 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
575 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
576 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
577 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
578 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
579 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
580 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
581 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
582 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
583 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
584 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
585 | (Nat.S |
---|
586 | Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) |
---|
587 | | I8051.RegisterDPL -> |
---|
588 | (fun _ -> ASM.DIRECT |
---|
589 | (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
590 | (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
591 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
592 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
593 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
594 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
595 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
596 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
597 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
598 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
599 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
600 | Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) |
---|
601 | | I8051.RegisterDPH -> |
---|
602 | (fun _ -> ASM.DIRECT |
---|
603 | (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
604 | (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
605 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
606 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
607 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
608 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
609 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
610 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
611 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
612 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
613 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
614 | Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) |
---|
615 | | I8051.RegisterCarry -> |
---|
616 | (fun _ -> ASM.DIRECT |
---|
617 | (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
618 | (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))) __ |
---|
619 | |
---|
620 | (** val vector_cast : |
---|
621 | Nat.nat -> Nat.nat -> 'a1 -> 'a1 Vector.vector -> 'a1 Vector.vector **) |
---|
622 | let vector_cast n m dflt v = |
---|
623 | Util.if_then_else_safe (Nat.leb n m) (fun _ -> |
---|
624 | Vector.append (Nat.minus m n) n (Vector.replicate (Nat.minus m n) dflt) v) |
---|
625 | (fun _ -> (Vector.vsplit (Nat.minus n m) m v).Types.snd) |
---|
626 | |
---|
627 | (** val arg_address : Joint.hdw_argument -> ASM.subaddressing_mode **) |
---|
628 | let arg_address = function |
---|
629 | | Joint.Reg r -> |
---|
630 | let x = |
---|
631 | ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S (Nat.S Nat.O)) |
---|
632 | (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S Nat.O)), |
---|
633 | ASM.Acc_a, (Vector.VCons ((Nat.S Nat.O), ASM.Direct, (Vector.VCons |
---|
634 | (Nat.O, ASM.Registr, Vector.VEmpty)))))) (Vector.VCons ((Nat.S (Nat.S |
---|
635 | (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)), |
---|
636 | ASM.Direct, (Vector.VCons ((Nat.S Nat.O), ASM.Registr, (Vector.VCons |
---|
637 | (Nat.O, ASM.Data, Vector.VEmpty)))))))) (register_address r) |
---|
638 | in |
---|
639 | x |
---|
640 | | Joint.Imm v -> let x = ASM.DATA v in x |
---|
641 | |
---|
642 | type lin_statement = Joint.joint_statement LabelledObjects.labelled_obj |
---|
643 | |
---|
644 | (** val data_of_int : BitVector.byte -> ASM.addressing_mode **) |
---|
645 | let data_of_int bv = |
---|
646 | ASM.DATA bv |
---|
647 | |
---|
648 | (** val data16_of_int : Nat.nat -> ASM.addressing_mode **) |
---|
649 | let data16_of_int bv = |
---|
650 | ASM.DATA16 |
---|
651 | (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
652 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
653 | Nat.O)))))))))))))))) bv) |
---|
654 | |
---|
655 | (** val accumulator_address : ASM.addressing_mode **) |
---|
656 | let accumulator_address = |
---|
657 | ASM.DIRECT |
---|
658 | (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
659 | (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
660 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
661 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
662 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
663 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
664 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
665 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
666 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
667 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
668 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
669 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
670 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
671 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
672 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
673 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
674 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
675 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
676 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
677 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
678 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
679 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
680 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
681 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
682 | Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) |
---|
683 | |
---|
684 | (** val asm_other_bit : ASM.addressing_mode **) |
---|
685 | let asm_other_bit = |
---|
686 | ASM.BIT_ADDR Joint.zero_byte |
---|
687 | |
---|
688 | (** val translate_statements : |
---|
689 | AST.ident List.list -> Joint.joint_statement -> ASM.pseudo_instruction |
---|
690 | Monad.smax_def__o__monad **) |
---|
691 | let translate_statements globals = function |
---|
692 | | Joint.Sequential (instr, x) -> |
---|
693 | (match instr with |
---|
694 | | Joint.COST_LABEL lbl -> |
---|
695 | Monad.m_bind0 (Monad.smax_def State.state_monad) |
---|
696 | (report_cost globals lbl) (fun x0 -> |
---|
697 | Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Cost lbl)) |
---|
698 | | Joint.CALL (f, x0, x1) -> |
---|
699 | (match f with |
---|
700 | | Types.Inl id -> |
---|
701 | Monad.m_bind0 (Monad.smax_def State.state_monad) |
---|
702 | (identifier_of_ident globals id) (fun id' -> |
---|
703 | Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Call |
---|
704 | (ASM.toASM_ident PreIdentifiers.ASMTag id'))) |
---|
705 | | Types.Inr x2 -> |
---|
706 | Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Instruction |
---|
707 | (ASM.JMP ASM.INDIRECT_DPTR))) |
---|
708 | | Joint.COND (x0, lbl) -> |
---|
709 | Monad.m_bind0 (Monad.smax_def State.state_monad) |
---|
710 | (identifier_of_label globals lbl) (fun l -> |
---|
711 | Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Instruction |
---|
712 | (ASM.JNZ l))) |
---|
713 | | Joint.Step_seq instr' -> |
---|
714 | (match instr' with |
---|
715 | | Joint.COMMENT comment -> |
---|
716 | Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Comment |
---|
717 | comment) |
---|
718 | | Joint.MOVE regs -> |
---|
719 | Monad.m_return0 (Monad.smax_def State.state_monad) |
---|
720 | (match Obj.magic regs with |
---|
721 | | Joint_LTL_LIN.From_acc (reg, x0) -> |
---|
722 | (match ASM.subaddressing_modeel (Nat.S (Nat.S Nat.O)) |
---|
723 | (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_a, |
---|
724 | (Vector.VCons ((Nat.S Nat.O), ASM.Direct, (Vector.VCons |
---|
725 | (Nat.O, ASM.Registr, Vector.VEmpty)))))) |
---|
726 | (register_address reg) with |
---|
727 | | ASM.DIRECT d -> |
---|
728 | (fun _ -> ASM.Instruction (ASM.MOV (Types.Inl (Types.Inl |
---|
729 | (Types.Inl (Types.Inr { Types.fst = (ASM.DIRECT d); |
---|
730 | Types.snd = ASM.ACC_A })))))) |
---|
731 | | ASM.INDIRECT x1 -> (fun _ -> assert false (* absurd case *)) |
---|
732 | | ASM.EXT_INDIRECT x1 -> |
---|
733 | (fun _ -> assert false (* absurd case *)) |
---|
734 | | ASM.REGISTER r -> |
---|
735 | (fun _ -> ASM.Instruction (ASM.MOV (Types.Inl (Types.Inl |
---|
736 | (Types.Inl (Types.Inl (Types.Inr { Types.fst = |
---|
737 | (ASM.REGISTER r); Types.snd = ASM.ACC_A }))))))) |
---|
738 | | ASM.ACC_A -> (fun _ -> ASM.Instruction ASM.NOP) |
---|
739 | | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) |
---|
740 | | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) |
---|
741 | | ASM.DATA x1 -> (fun _ -> assert false (* absurd case *)) |
---|
742 | | ASM.DATA16 x1 -> (fun _ -> assert false (* absurd case *)) |
---|
743 | | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *)) |
---|
744 | | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *)) |
---|
745 | | ASM.EXT_INDIRECT_DPTR -> |
---|
746 | (fun _ -> assert false (* absurd case *)) |
---|
747 | | ASM.INDIRECT_DPTR -> |
---|
748 | (fun _ -> assert false (* absurd case *)) |
---|
749 | | ASM.CARRY -> (fun _ -> assert false (* absurd case *)) |
---|
750 | | ASM.BIT_ADDR x1 -> (fun _ -> assert false (* absurd case *)) |
---|
751 | | ASM.N_BIT_ADDR x1 -> |
---|
752 | (fun _ -> assert false (* absurd case *)) |
---|
753 | | ASM.RELATIVE x1 -> (fun _ -> assert false (* absurd case *)) |
---|
754 | | ASM.ADDR11 x1 -> (fun _ -> assert false (* absurd case *)) |
---|
755 | | ASM.ADDR16 x1 -> (fun _ -> assert false (* absurd case *))) |
---|
756 | __ |
---|
757 | | Joint_LTL_LIN.To_acc (x0, reg) -> |
---|
758 | (match ASM.subaddressing_modeel (Nat.S (Nat.S Nat.O)) |
---|
759 | (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_a, |
---|
760 | (Vector.VCons ((Nat.S Nat.O), ASM.Direct, (Vector.VCons |
---|
761 | (Nat.O, ASM.Registr, Vector.VEmpty)))))) |
---|
762 | (register_address reg) with |
---|
763 | | ASM.DIRECT d -> |
---|
764 | (fun _ -> ASM.Instruction (ASM.MOV (Types.Inl (Types.Inl |
---|
765 | (Types.Inl (Types.Inl (Types.Inl { Types.fst = ASM.ACC_A; |
---|
766 | Types.snd = (ASM.DIRECT d) }))))))) |
---|
767 | | ASM.INDIRECT x1 -> (fun _ -> assert false (* absurd case *)) |
---|
768 | | ASM.EXT_INDIRECT x1 -> |
---|
769 | (fun _ -> assert false (* absurd case *)) |
---|
770 | | ASM.REGISTER r -> |
---|
771 | (fun _ -> ASM.Instruction (ASM.MOV (Types.Inl (Types.Inl |
---|
772 | (Types.Inl (Types.Inl (Types.Inl { Types.fst = ASM.ACC_A; |
---|
773 | Types.snd = (ASM.REGISTER r) }))))))) |
---|
774 | | ASM.ACC_A -> (fun _ -> ASM.Instruction ASM.NOP) |
---|
775 | | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) |
---|
776 | | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) |
---|
777 | | ASM.DATA x1 -> (fun _ -> assert false (* absurd case *)) |
---|
778 | | ASM.DATA16 x1 -> (fun _ -> assert false (* absurd case *)) |
---|
779 | | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *)) |
---|
780 | | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *)) |
---|
781 | | ASM.EXT_INDIRECT_DPTR -> |
---|
782 | (fun _ -> assert false (* absurd case *)) |
---|
783 | | ASM.INDIRECT_DPTR -> |
---|
784 | (fun _ -> assert false (* absurd case *)) |
---|
785 | | ASM.CARRY -> (fun _ -> assert false (* absurd case *)) |
---|
786 | | ASM.BIT_ADDR x1 -> (fun _ -> assert false (* absurd case *)) |
---|
787 | | ASM.N_BIT_ADDR x1 -> |
---|
788 | (fun _ -> assert false (* absurd case *)) |
---|
789 | | ASM.RELATIVE x1 -> (fun _ -> assert false (* absurd case *)) |
---|
790 | | ASM.ADDR11 x1 -> (fun _ -> assert false (* absurd case *)) |
---|
791 | | ASM.ADDR16 x1 -> (fun _ -> assert false (* absurd case *))) |
---|
792 | __ |
---|
793 | | Joint_LTL_LIN.Int_to_reg (reg, b) -> |
---|
794 | (match ASM.subaddressing_modeel (Nat.S (Nat.S Nat.O)) |
---|
795 | (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_a, |
---|
796 | (Vector.VCons ((Nat.S Nat.O), ASM.Direct, (Vector.VCons |
---|
797 | (Nat.O, ASM.Registr, Vector.VEmpty)))))) |
---|
798 | (register_address reg) with |
---|
799 | | ASM.DIRECT d -> |
---|
800 | (fun _ -> ASM.Instruction (ASM.MOV (Types.Inl (Types.Inl |
---|
801 | (Types.Inl (Types.Inr { Types.fst = (ASM.DIRECT d); |
---|
802 | Types.snd = (ASM.DATA b) })))))) |
---|
803 | | ASM.INDIRECT x0 -> (fun _ -> assert false (* absurd case *)) |
---|
804 | | ASM.EXT_INDIRECT x0 -> |
---|
805 | (fun _ -> assert false (* absurd case *)) |
---|
806 | | ASM.REGISTER r -> |
---|
807 | (fun _ -> ASM.Instruction (ASM.MOV (Types.Inl (Types.Inl |
---|
808 | (Types.Inl (Types.Inl (Types.Inr { Types.fst = |
---|
809 | (ASM.REGISTER r); Types.snd = (ASM.DATA b) }))))))) |
---|
810 | | ASM.ACC_A -> |
---|
811 | (fun _ -> |
---|
812 | match BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
813 | (Nat.S (Nat.S (Nat.S Nat.O)))))))) |
---|
814 | (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
815 | (Nat.S (Nat.S (Nat.S Nat.O))))))))) b with |
---|
816 | | Bool.True -> ASM.Instruction (ASM.CLR ASM.ACC_A) |
---|
817 | | Bool.False -> |
---|
818 | ASM.Instruction (ASM.MOV (Types.Inl (Types.Inl (Types.Inl |
---|
819 | (Types.Inl (Types.Inl { Types.fst = ASM.ACC_A; |
---|
820 | Types.snd = (ASM.DATA b) }))))))) |
---|
821 | | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) |
---|
822 | | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) |
---|
823 | | ASM.DATA x0 -> (fun _ -> assert false (* absurd case *)) |
---|
824 | | ASM.DATA16 x0 -> (fun _ -> assert false (* absurd case *)) |
---|
825 | | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *)) |
---|
826 | | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *)) |
---|
827 | | ASM.EXT_INDIRECT_DPTR -> |
---|
828 | (fun _ -> assert false (* absurd case *)) |
---|
829 | | ASM.INDIRECT_DPTR -> |
---|
830 | (fun _ -> assert false (* absurd case *)) |
---|
831 | | ASM.CARRY -> (fun _ -> assert false (* absurd case *)) |
---|
832 | | ASM.BIT_ADDR x0 -> (fun _ -> assert false (* absurd case *)) |
---|
833 | | ASM.N_BIT_ADDR x0 -> |
---|
834 | (fun _ -> assert false (* absurd case *)) |
---|
835 | | ASM.RELATIVE x0 -> (fun _ -> assert false (* absurd case *)) |
---|
836 | | ASM.ADDR11 x0 -> (fun _ -> assert false (* absurd case *)) |
---|
837 | | ASM.ADDR16 x0 -> (fun _ -> assert false (* absurd case *))) |
---|
838 | __ |
---|
839 | | Joint_LTL_LIN.Int_to_acc (x0, b) -> |
---|
840 | (match BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
841 | (Nat.S (Nat.S Nat.O)))))))) |
---|
842 | (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
843 | (Nat.S (Nat.S (Nat.S Nat.O))))))))) b with |
---|
844 | | Bool.True -> ASM.Instruction (ASM.CLR ASM.ACC_A) |
---|
845 | | Bool.False -> |
---|
846 | ASM.Instruction (ASM.MOV (Types.Inl (Types.Inl (Types.Inl |
---|
847 | (Types.Inl (Types.Inl { Types.fst = ASM.ACC_A; Types.snd = |
---|
848 | (ASM.DATA b) })))))))) |
---|
849 | | Joint.POP x0 -> |
---|
850 | Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Instruction |
---|
851 | (ASM.POP accumulator_address)) |
---|
852 | | Joint.PUSH x0 -> |
---|
853 | Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Instruction |
---|
854 | (ASM.PUSH accumulator_address)) |
---|
855 | | Joint.ADDRESS (addr, x0, x1) -> |
---|
856 | Monad.m_bind0 (Monad.smax_def State.state_monad) |
---|
857 | (address_of_ident (Obj.magic globals) (Obj.magic addr)) |
---|
858 | (fun addr' -> |
---|
859 | Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Instruction |
---|
860 | (ASM.MOV (Types.Inl (Types.Inl (Types.Inr { Types.fst = ASM.DPTR; |
---|
861 | Types.snd = addr' })))))) |
---|
862 | | Joint.OPACCS (accs, x0, x1, x2, x3) -> |
---|
863 | Monad.m_return0 (Monad.smax_def State.state_monad) |
---|
864 | (match accs with |
---|
865 | | BackEndOps.Mul -> |
---|
866 | ASM.Instruction (ASM.MUL (ASM.ACC_A, ASM.ACC_B)) |
---|
867 | | BackEndOps.DivuModu -> |
---|
868 | ASM.Instruction (ASM.DIV (ASM.ACC_A, ASM.ACC_B))) |
---|
869 | | Joint.OP1 (op1, x0, x1) -> |
---|
870 | Monad.m_return0 (Monad.smax_def State.state_monad) |
---|
871 | (match op1 with |
---|
872 | | BackEndOps.Cmpl -> ASM.Instruction (ASM.CPL ASM.ACC_A) |
---|
873 | | BackEndOps.Inc -> ASM.Instruction (ASM.INC ASM.ACC_A) |
---|
874 | | BackEndOps.Rl -> ASM.Instruction (ASM.RL ASM.ACC_A)) |
---|
875 | | Joint.OP2 (op2, x0, x1, reg) -> |
---|
876 | Monad.m_return0 (Monad.smax_def State.state_monad) |
---|
877 | ((match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) |
---|
878 | (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a, |
---|
879 | (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Direct, |
---|
880 | (Vector.VCons ((Nat.S Nat.O), ASM.Registr, (Vector.VCons |
---|
881 | (Nat.O, ASM.Data, Vector.VEmpty)))))))) |
---|
882 | (arg_address (Obj.magic reg)) with |
---|
883 | | ASM.DIRECT d -> |
---|
884 | (fun _ -> |
---|
885 | match op2 with |
---|
886 | | BackEndOps.Add -> |
---|
887 | ASM.Instruction (ASM.ADD (ASM.ACC_A, (ASM.DIRECT d))) |
---|
888 | | BackEndOps.Addc -> |
---|
889 | ASM.Instruction (ASM.ADDC (ASM.ACC_A, (ASM.DIRECT d))) |
---|
890 | | BackEndOps.Sub -> |
---|
891 | ASM.Instruction (ASM.SUBB (ASM.ACC_A, (ASM.DIRECT d))) |
---|
892 | | BackEndOps.And -> |
---|
893 | ASM.Instruction (ASM.ANL (Types.Inl (Types.Inl |
---|
894 | { Types.fst = ASM.ACC_A; Types.snd = (ASM.DIRECT d) }))) |
---|
895 | | BackEndOps.Or -> |
---|
896 | ASM.Instruction (ASM.ORL (Types.Inl (Types.Inl |
---|
897 | { Types.fst = ASM.ACC_A; Types.snd = (ASM.DIRECT d) }))) |
---|
898 | | BackEndOps.Xor -> |
---|
899 | ASM.Instruction (ASM.XRL (Types.Inl { Types.fst = |
---|
900 | ASM.ACC_A; Types.snd = (ASM.DIRECT d) }))) |
---|
901 | | ASM.INDIRECT x2 -> (fun _ -> assert false (* absurd case *)) |
---|
902 | | ASM.EXT_INDIRECT x2 -> |
---|
903 | (fun _ -> assert false (* absurd case *)) |
---|
904 | | ASM.REGISTER r -> |
---|
905 | (fun _ -> |
---|
906 | match op2 with |
---|
907 | | BackEndOps.Add -> |
---|
908 | ASM.Instruction (ASM.ADD (ASM.ACC_A, (ASM.REGISTER r))) |
---|
909 | | BackEndOps.Addc -> |
---|
910 | ASM.Instruction (ASM.ADDC (ASM.ACC_A, (ASM.REGISTER r))) |
---|
911 | | BackEndOps.Sub -> |
---|
912 | ASM.Instruction (ASM.SUBB (ASM.ACC_A, (ASM.REGISTER r))) |
---|
913 | | BackEndOps.And -> |
---|
914 | ASM.Instruction (ASM.ANL (Types.Inl (Types.Inl |
---|
915 | { Types.fst = ASM.ACC_A; Types.snd = (ASM.REGISTER |
---|
916 | r) }))) |
---|
917 | | BackEndOps.Or -> |
---|
918 | ASM.Instruction (ASM.ORL (Types.Inl (Types.Inl |
---|
919 | { Types.fst = ASM.ACC_A; Types.snd = (ASM.REGISTER |
---|
920 | r) }))) |
---|
921 | | BackEndOps.Xor -> |
---|
922 | ASM.Instruction (ASM.XRL (Types.Inl { Types.fst = |
---|
923 | ASM.ACC_A; Types.snd = (ASM.REGISTER r) }))) |
---|
924 | | ASM.ACC_A -> |
---|
925 | (fun _ -> |
---|
926 | match op2 with |
---|
927 | | BackEndOps.Add -> |
---|
928 | ASM.Instruction (ASM.ADD (ASM.ACC_A, accumulator_address)) |
---|
929 | | BackEndOps.Addc -> |
---|
930 | ASM.Instruction (ASM.ADDC (ASM.ACC_A, accumulator_address)) |
---|
931 | | BackEndOps.Sub -> |
---|
932 | ASM.Instruction (ASM.SUBB (ASM.ACC_A, accumulator_address)) |
---|
933 | | BackEndOps.And -> ASM.Instruction ASM.NOP |
---|
934 | | BackEndOps.Or -> ASM.Instruction ASM.NOP |
---|
935 | | BackEndOps.Xor -> ASM.Instruction (ASM.CLR ASM.ACC_A)) |
---|
936 | | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) |
---|
937 | | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) |
---|
938 | | ASM.DATA b -> |
---|
939 | (fun _ -> |
---|
940 | match op2 with |
---|
941 | | BackEndOps.Add -> |
---|
942 | ASM.Instruction (ASM.ADD (ASM.ACC_A, (ASM.DATA b))) |
---|
943 | | BackEndOps.Addc -> |
---|
944 | ASM.Instruction (ASM.ADDC (ASM.ACC_A, (ASM.DATA b))) |
---|
945 | | BackEndOps.Sub -> |
---|
946 | ASM.Instruction (ASM.SUBB (ASM.ACC_A, (ASM.DATA b))) |
---|
947 | | BackEndOps.And -> |
---|
948 | ASM.Instruction (ASM.ANL (Types.Inl (Types.Inl |
---|
949 | { Types.fst = ASM.ACC_A; Types.snd = (ASM.DATA b) }))) |
---|
950 | | BackEndOps.Or -> |
---|
951 | ASM.Instruction (ASM.ORL (Types.Inl (Types.Inl |
---|
952 | { Types.fst = ASM.ACC_A; Types.snd = (ASM.DATA b) }))) |
---|
953 | | BackEndOps.Xor -> |
---|
954 | ASM.Instruction (ASM.XRL (Types.Inl { Types.fst = |
---|
955 | ASM.ACC_A; Types.snd = (ASM.DATA b) }))) |
---|
956 | | ASM.DATA16 x2 -> (fun _ -> assert false (* absurd case *)) |
---|
957 | | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *)) |
---|
958 | | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *)) |
---|
959 | | ASM.EXT_INDIRECT_DPTR -> |
---|
960 | (fun _ -> assert false (* absurd case *)) |
---|
961 | | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *)) |
---|
962 | | ASM.CARRY -> (fun _ -> assert false (* absurd case *)) |
---|
963 | | ASM.BIT_ADDR x2 -> (fun _ -> assert false (* absurd case *)) |
---|
964 | | ASM.N_BIT_ADDR x2 -> (fun _ -> assert false (* absurd case *)) |
---|
965 | | ASM.RELATIVE x2 -> (fun _ -> assert false (* absurd case *)) |
---|
966 | | ASM.ADDR11 x2 -> (fun _ -> assert false (* absurd case *)) |
---|
967 | | ASM.ADDR16 x2 -> (fun _ -> assert false (* absurd case *))) __) |
---|
968 | | Joint.CLEAR_CARRY -> |
---|
969 | Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Instruction |
---|
970 | (ASM.CLR ASM.CARRY)) |
---|
971 | | Joint.SET_CARRY -> |
---|
972 | Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Instruction |
---|
973 | (ASM.SETB ASM.CARRY)) |
---|
974 | | Joint.LOAD (x0, x1, x2) -> |
---|
975 | Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Instruction |
---|
976 | (ASM.MOVX (Types.Inl { Types.fst = ASM.ACC_A; Types.snd = |
---|
977 | ASM.EXT_INDIRECT_DPTR }))) |
---|
978 | | Joint.STORE (x0, x1, x2) -> |
---|
979 | Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Instruction |
---|
980 | (ASM.MOVX (Types.Inr { Types.fst = ASM.EXT_INDIRECT_DPTR; |
---|
981 | Types.snd = ASM.ACC_A }))) |
---|
982 | | Joint.Extension_seq ext -> |
---|
983 | (match Obj.magic ext with |
---|
984 | | Joint_LTL_LIN.SAVE_CARRY -> |
---|
985 | Monad.m_return0 (Monad.smax_def State.state_monad) |
---|
986 | (ASM.Instruction (ASM.MOV (Types.Inr { Types.fst = |
---|
987 | asm_other_bit; Types.snd = ASM.CARRY }))) |
---|
988 | | Joint_LTL_LIN.RESTORE_CARRY -> |
---|
989 | Monad.m_return0 (Monad.smax_def State.state_monad) |
---|
990 | (ASM.Instruction (ASM.MOV (Types.Inl (Types.Inr { Types.fst = |
---|
991 | ASM.CARRY; Types.snd = asm_other_bit })))) |
---|
992 | | Joint_LTL_LIN.LOW_ADDRESS (reg, lbl) -> |
---|
993 | Monad.m_bind0 (Monad.smax_def State.state_monad) |
---|
994 | (identifier_of_label globals lbl) (fun lbl' -> |
---|
995 | Monad.m_return0 (Monad.smax_def State.state_monad) |
---|
996 | (ASM.MovSuccessor ((register_address reg), ASM.LOW, lbl'))) |
---|
997 | | Joint_LTL_LIN.HIGH_ADDRESS (reg, lbl) -> |
---|
998 | Monad.m_bind0 (Monad.smax_def State.state_monad) |
---|
999 | (identifier_of_label globals lbl) (fun lbl' -> |
---|
1000 | Monad.m_return0 (Monad.smax_def State.state_monad) |
---|
1001 | (ASM.MovSuccessor ((register_address reg), ASM.HIGH, lbl')))))) |
---|
1002 | | Joint.Final instr -> |
---|
1003 | (match instr with |
---|
1004 | | Joint.GOTO lbl -> |
---|
1005 | Monad.m_bind0 (Monad.smax_def State.state_monad) |
---|
1006 | (identifier_of_label globals lbl) (fun lbl' -> |
---|
1007 | Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Jmp |
---|
1008 | (ASM.toASM_ident PreIdentifiers.LabelTag lbl))) |
---|
1009 | | Joint.RETURN -> |
---|
1010 | Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Instruction |
---|
1011 | ASM.RET) |
---|
1012 | | Joint.TAILCALL (x, x0) -> assert false (* absurd case *)) |
---|
1013 | | Joint.FCOND (x0, lbl_true, lbl_false) -> |
---|
1014 | Monad.m_bind0 (Monad.smax_def State.state_monad) |
---|
1015 | (identifier_of_label globals lbl_true) (fun l1 -> |
---|
1016 | Monad.m_bind0 (Monad.smax_def State.state_monad) |
---|
1017 | (identifier_of_label globals lbl_false) (fun l2 -> |
---|
1018 | Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Jnz (ASM.ACC_A, |
---|
1019 | l1, l2)))) |
---|
1020 | |
---|
1021 | (** val build_translated_statement : |
---|
1022 | AST.ident List.list -> lin_statement -> __ **) |
---|
1023 | let build_translated_statement globals statement = |
---|
1024 | Monad.m_bind0 (Monad.smax_def State.state_monad) |
---|
1025 | (translate_statements globals statement.Types.snd) (fun stmt -> |
---|
1026 | match statement.Types.fst with |
---|
1027 | | Types.None -> |
---|
1028 | Monad.m_return0 (Monad.smax_def State.state_monad) { Types.fst = |
---|
1029 | Types.None; Types.snd = stmt } |
---|
1030 | | Types.Some lbl -> |
---|
1031 | Monad.m_bind0 (Monad.smax_def State.state_monad) |
---|
1032 | (identifier_of_label globals lbl) (fun lbl' -> |
---|
1033 | Monad.m_return0 (Monad.smax_def State.state_monad) { Types.fst = |
---|
1034 | (Types.Some lbl'); Types.snd = stmt })) |
---|
1035 | |
---|
1036 | (** val translate_code : |
---|
1037 | AST.ident List.list -> lin_statement List.list -> __ **) |
---|
1038 | let translate_code globals code = |
---|
1039 | Monad.m_list_map (Monad.smax_def State.state_monad) |
---|
1040 | (build_translated_statement globals) code |
---|
1041 | |
---|
1042 | (** val translate_fun_def : |
---|
1043 | AST.ident List.list -> (AST.ident, Joint.joint_function) Types.prod -> __ **) |
---|
1044 | let translate_fun_def globals id_def = |
---|
1045 | Monad.m_bind0 (Monad.smax_def State.state_monad) |
---|
1046 | (start_funct_translation globals id_def) (fun x -> |
---|
1047 | match id_def.Types.snd with |
---|
1048 | | AST.Internal int -> |
---|
1049 | let code = (Types.pi1 int).Joint.joint_if_code in |
---|
1050 | Monad.m_bind0 (Monad.smax_def State.state_monad) |
---|
1051 | (identifier_of_ident globals id_def.Types.fst) (fun id -> |
---|
1052 | Monad.m_bind0 (Monad.smax_def State.state_monad) |
---|
1053 | (translate_code globals (Obj.magic code)) (fun code' -> |
---|
1054 | match code' with |
---|
1055 | | List.Nil -> |
---|
1056 | Monad.m_return0 (Monad.smax_def State.state_monad) (List.Cons |
---|
1057 | ({ Types.fst = (Types.Some id); Types.snd = (ASM.Instruction |
---|
1058 | ASM.RET) }, List.Nil)) |
---|
1059 | | List.Cons (hd, tl) -> |
---|
1060 | (match hd.Types.fst with |
---|
1061 | | Types.None -> |
---|
1062 | Monad.m_return0 (Monad.smax_def State.state_monad) (List.Cons |
---|
1063 | ({ Types.fst = (Types.Some id); Types.snd = hd.Types.snd }, |
---|
1064 | tl)) |
---|
1065 | | Types.Some x0 -> |
---|
1066 | Monad.m_return0 (Monad.smax_def State.state_monad) (List.Cons |
---|
1067 | ({ Types.fst = (Types.Some id); Types.snd = (ASM.Instruction |
---|
1068 | ASM.NOP) }, (List.Cons (hd, tl))))))) |
---|
1069 | | AST.External x0 -> |
---|
1070 | Monad.m_return0 (Monad.smax_def State.state_monad) List.Nil) |
---|
1071 | |
---|
1072 | (** val store_bytes : |
---|
1073 | BitVector.byte List.list -> ASM.labelled_instruction List.list **) |
---|
1074 | let store_bytes bytes = |
---|
1075 | List.fold List.append List.Nil (fun by -> Bool.True) (fun by -> List.Cons |
---|
1076 | ({ Types.fst = Types.None; Types.snd = (ASM.Instruction (ASM.MOV |
---|
1077 | (Types.Inl (Types.Inl (Types.Inl (Types.Inl (Types.Inl { Types.fst = |
---|
1078 | ASM.ACC_A; Types.snd = (ASM.DATA by) }))))))) }, (List.Cons |
---|
1079 | ({ Types.fst = Types.None; Types.snd = (ASM.Instruction (ASM.MOVX |
---|
1080 | (Types.Inr { Types.fst = ASM.EXT_INDIRECT_DPTR; Types.snd = |
---|
1081 | ASM.ACC_A }))) }, (List.Cons ({ Types.fst = Types.None; Types.snd = |
---|
1082 | (ASM.Instruction (ASM.INC ASM.DPTR)) }, List.Nil)))))) bytes |
---|
1083 | |
---|
1084 | (** val do_store_init_data : |
---|
1085 | AST.ident List.list -> aSM_universe -> Z.z -> AST.init_data -> |
---|
1086 | ASM.labelled_instruction List.list **) |
---|
1087 | let do_store_init_data globals u nxt_dptr = function |
---|
1088 | | AST.Init_int8 n -> store_bytes (List.Cons (n, List.Nil)) |
---|
1089 | | AST.Init_int16 n -> |
---|
1090 | let { Types.fst = by0; Types.snd = by1 } = |
---|
1091 | Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
1092 | Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
1093 | Nat.O)))))))) n |
---|
1094 | in |
---|
1095 | store_bytes (List.Cons (by0, (List.Cons (by1, List.Nil)))) |
---|
1096 | | AST.Init_int32 n -> |
---|
1097 | let { Types.fst = by0; Types.snd = n0 } = |
---|
1098 | Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
1099 | Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
1100 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
1101 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))))))))))) |
---|
1102 | n |
---|
1103 | in |
---|
1104 | let { Types.fst = by1; Types.snd = n1 } = |
---|
1105 | Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
1106 | Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
1107 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
1108 | Nat.O)))))))))))))))) n0 |
---|
1109 | in |
---|
1110 | let { Types.fst = by2; Types.snd = by3 } = |
---|
1111 | Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
1112 | Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
1113 | Nat.O)))))))) n1 |
---|
1114 | in |
---|
1115 | store_bytes (List.Cons (by0, (List.Cons (by1, (List.Cons (by2, (List.Cons |
---|
1116 | (by3, List.Nil)))))))) |
---|
1117 | | AST.Init_space n -> |
---|
1118 | (match n with |
---|
1119 | | Nat.O -> List.Nil |
---|
1120 | | Nat.S k -> |
---|
1121 | (match k with |
---|
1122 | | Nat.O -> |
---|
1123 | List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Instruction |
---|
1124 | (ASM.INC ASM.DPTR)) }, List.Nil) |
---|
1125 | | Nat.S x -> |
---|
1126 | List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Instruction |
---|
1127 | (ASM.MOV (Types.Inl (Types.Inl (Types.Inr { Types.fst = ASM.DPTR; |
---|
1128 | Types.snd = (ASM.DATA16 |
---|
1129 | (BitVectorZ.bitvector_of_Z (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
1130 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
1131 | (Nat.S (Nat.S Nat.O)))))))))))))))) nxt_dptr)) }))))) }, |
---|
1132 | List.Nil))) |
---|
1133 | | AST.Init_null -> |
---|
1134 | store_bytes (List.Cons |
---|
1135 | ((BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
1136 | Nat.O))))))))), (List.Cons |
---|
1137 | ((BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
1138 | Nat.O))))))))), List.Nil)))) |
---|
1139 | | AST.Init_addrof (symb, ofs) -> |
---|
1140 | let addr = |
---|
1141 | match Identifiers.lookup PreIdentifiers.SymbolTag u.address_map symb with |
---|
1142 | | Types.None -> |
---|
1143 | BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
1144 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
1145 | Nat.O)))))))))))))))) |
---|
1146 | | Types.Some x -> |
---|
1147 | BitVectorZ.bitvector_of_Z (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
1148 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
1149 | Nat.O)))))))))))))))) |
---|
1150 | (Z.zplus |
---|
1151 | (BitVectorZ.z_of_unsigned_bitvector (Nat.S (Nat.S (Nat.S (Nat.S |
---|
1152 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
1153 | (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) x) (Z.z_of_nat ofs)) |
---|
1154 | in |
---|
1155 | let { Types.fst = by1; Types.snd = by0 } = |
---|
1156 | Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
1157 | Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
1158 | Nat.O)))))))) addr |
---|
1159 | in |
---|
1160 | store_bytes (List.Cons (by0, (List.Cons (by1, List.Nil)))) |
---|
1161 | |
---|
1162 | (** val do_store_init_data_list : |
---|
1163 | AST.ident List.list -> aSM_universe -> Z.z -> AST.init_data List.list -> |
---|
1164 | ASM.labelled_instruction List.list **) |
---|
1165 | let do_store_init_data_list globals u start_dptr data = |
---|
1166 | let f = fun data0 dptr_acc -> |
---|
1167 | let { Types.fst = dptr; Types.snd = acc } = dptr_acc in |
---|
1168 | let nxt_dptr = |
---|
1169 | Z.zplus dptr (Z.z_of_nat (Globalenvs.size_init_data data0)) |
---|
1170 | in |
---|
1171 | { Types.fst = nxt_dptr; Types.snd = |
---|
1172 | (List.append (do_store_init_data globals u nxt_dptr data0) acc) } |
---|
1173 | in |
---|
1174 | List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Instruction (ASM.MOV |
---|
1175 | (Types.Inl (Types.Inl (Types.Inr { Types.fst = ASM.DPTR; Types.snd = |
---|
1176 | (ASM.DATA16 |
---|
1177 | (BitVectorZ.bitvector_of_Z (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
1178 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
1179 | Nat.O)))))))))))))))) start_dptr)) }))))) }, |
---|
1180 | (List.foldr f { Types.fst = start_dptr; Types.snd = List.Nil } data).Types.snd) |
---|
1181 | |
---|
1182 | (** val translate_initialization : |
---|
1183 | LIN.lin_program -> ASM.labelled_instruction List.list |
---|
1184 | Monad.smax_def__o__monad **) |
---|
1185 | let translate_initialization p = |
---|
1186 | Obj.magic (fun u -> |
---|
1187 | let start_sp = |
---|
1188 | Z.zopp |
---|
1189 | (Z.z_of_nat |
---|
1190 | (Joint.globals_stacksize (Joint.lin_params_to_params LIN.lIN) p)) |
---|
1191 | in |
---|
1192 | let { Types.fst = sph; Types.snd = spl } = |
---|
1193 | Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
1194 | Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
1195 | Nat.O)))))))) |
---|
1196 | (BitVectorZ.bitvector_of_Z |
---|
1197 | (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
1198 | Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
1199 | (Nat.S Nat.O))))))))) start_sp) |
---|
1200 | in |
---|
1201 | let data = |
---|
1202 | List.flatten |
---|
1203 | (List.map (fun x -> x.Types.snd) p.Joint.joint_prog.AST.prog_vars) |
---|
1204 | in |
---|
1205 | let init_isp = ASM.DATA |
---|
1206 | (Vector.append (Nat.S (Nat.S Nat.O)) |
---|
1207 | (Nat.plus (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S |
---|
1208 | Nat.O))))) (BitVector.zero (Nat.S (Nat.S Nat.O))) |
---|
1209 | (Vector.append (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S |
---|
1210 | Nat.O)))) (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons |
---|
1211 | (Nat.O, Bool.False, Vector.VEmpty)))) |
---|
1212 | (BitVector.maximum (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))) |
---|
1213 | in |
---|
1214 | let isp_direct = ASM.DIRECT |
---|
1215 | (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
1216 | Nat.O))))))) (Nat.S Nat.O) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S |
---|
1217 | (Nat.S (Nat.S Nat.O)))))), Bool.True, |
---|
1218 | (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
1219 | Nat.O))))))))) (Vector.VCons (Nat.O, Bool.True, Vector.VEmpty))) |
---|
1220 | in |
---|
1221 | let reg_spl = ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)), |
---|
1222 | Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons |
---|
1223 | (Nat.O, Bool.False, Vector.VEmpty)))))) |
---|
1224 | in |
---|
1225 | let reg_sph = ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)), |
---|
1226 | Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons |
---|
1227 | (Nat.O, Bool.True, Vector.VEmpty)))))) |
---|
1228 | in |
---|
1229 | { Types.fst = u; Types.snd = |
---|
1230 | (List.append (List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Cost |
---|
1231 | p.Joint.init_cost_label) }, (List.Cons ({ Types.fst = Types.None; |
---|
1232 | Types.snd = (ASM.Instruction (ASM.MOV (Types.Inl (Types.Inl (Types.Inl |
---|
1233 | (Types.Inr { Types.fst = isp_direct; Types.snd = init_isp })))))) }, |
---|
1234 | (List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Instruction |
---|
1235 | (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inl (Types.Inr |
---|
1236 | { Types.fst = reg_spl; Types.snd = (ASM.DATA spl) }))))))) }, |
---|
1237 | (List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Instruction |
---|
1238 | (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inl (Types.Inr |
---|
1239 | { Types.fst = reg_sph; Types.snd = (ASM.DATA sph) }))))))) }, |
---|
1240 | List.Nil)))))))) |
---|
1241 | (do_store_init_data_list (AST.prog_var_names p.Joint.joint_prog) u |
---|
1242 | start_sp data)) }) |
---|
1243 | |
---|
1244 | (** val get_symboltable : |
---|
1245 | AST.ident List.list -> (ASM.identifier, AST.ident) Types.prod List.list |
---|
1246 | Monad.smax_def__o__monad **) |
---|
1247 | let get_symboltable globals = |
---|
1248 | Obj.magic (fun u -> |
---|
1249 | let imap = u.ident_map in |
---|
1250 | let f = fun iold inew x -> List.Cons ({ Types.fst = inew; Types.snd = |
---|
1251 | iold }, x) |
---|
1252 | in |
---|
1253 | { Types.fst = u; Types.snd = |
---|
1254 | (Identifiers.foldi PreIdentifiers.SymbolTag f imap List.Nil) }) |
---|
1255 | |
---|
1256 | (** val lin_to_asm : |
---|
1257 | LIN.lin_program -> ASM.pseudo_assembly_program Types.option **) |
---|
1258 | let lin_to_asm p = |
---|
1259 | State.state_run (new_ASM_universe p) |
---|
1260 | (let add_translation = fun acc id_def -> |
---|
1261 | Monad.m_bind0 (Monad.smax_def State.state_monad) |
---|
1262 | (translate_fun_def |
---|
1263 | (List.map (fun x -> x.Types.fst.Types.fst) |
---|
1264 | p.Joint.joint_prog.AST.prog_vars) id_def) (fun code -> |
---|
1265 | Monad.m_bind0 (Monad.smax_def State.state_monad) acc (fun acc0 -> |
---|
1266 | Monad.m_return0 (Monad.smax_def State.state_monad) |
---|
1267 | (List.append code acc0))) |
---|
1268 | in |
---|
1269 | Monad.m_bind0 (Monad.smax_def State.state_monad) |
---|
1270 | (Util.foldl add_translation |
---|
1271 | (Monad.m_return0 (Monad.smax_def State.state_monad) List.Nil) |
---|
1272 | p.Joint.joint_prog.AST.prog_funct) (fun code -> |
---|
1273 | Monad.m_bind0 (Monad.smax_def State.state_monad) |
---|
1274 | (aSM_fresh (AST.prog_var_names p.Joint.joint_prog)) |
---|
1275 | (fun exit_label -> |
---|
1276 | Monad.m_bind0 (Monad.smax_def State.state_monad) |
---|
1277 | (identifier_of_ident (AST.prog_var_names p.Joint.joint_prog) |
---|
1278 | p.Joint.joint_prog.AST.prog_main) (fun main -> |
---|
1279 | Monad.m_bind0 (Monad.smax_def State.state_monad) |
---|
1280 | (get_symboltable (AST.prog_var_names p.Joint.joint_prog)) |
---|
1281 | (fun symboltable -> |
---|
1282 | Monad.m_bind0 (Monad.smax_def State.state_monad) |
---|
1283 | (translate_initialization p) (fun init -> |
---|
1284 | Monad.m_bind0 (Monad.smax_def State.state_monad) |
---|
1285 | State.state_get (fun u -> |
---|
1286 | Monad.m_return0 (Monad.smax_def State.state_monad) |
---|
1287 | (let code0 = |
---|
1288 | List.append init (List.Cons ({ Types.fst = Types.None; |
---|
1289 | Types.snd = (ASM.Call main) }, (List.Cons |
---|
1290 | ({ Types.fst = (Types.Some exit_label); Types.snd = |
---|
1291 | (ASM.Cost u.fresh_cost_label) }, (List.Cons |
---|
1292 | ({ Types.fst = Types.None; Types.snd = (ASM.Jmp |
---|
1293 | exit_label) }, code)))))) |
---|
1294 | in |
---|
1295 | Monad.m_bind0 (Monad.max_def Option.option) |
---|
1296 | (Obj.magic (ASM.code_size_opt code0)) (fun _ -> |
---|
1297 | Monad.m_return0 (Monad.max_def Option.option) |
---|
1298 | { ASM.preamble = List.Nil; ASM.code = code0; |
---|
1299 | ASM.renamed_symbols = symboltable; ASM.final_label = |
---|
1300 | exit_label }))))))))) |
---|
1301 | |
---|