source: extracted/lINToASM.ml @ 2746

Last change on this file since 2746 was 2743, checked in by sacerdot, 7 years ago

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

File size: 48.1 KB
Line 
1open Preamble
2
3open Div_and_mod
4
5open Jmeq
6
7open Russell
8
9open Bool
10
11open Relations
12
13open Nat
14
15open Hints_declaration
16
17open Core_notation
18
19open Pts
20
21open Logic
22
23open Types
24
25open List
26
27open Util
28
29open Extranat
30
31open Vector
32
33open FoldStuff
34
35open BitVector
36
37open BitVectorTrie
38
39open BitVectorTrieSet
40
41open String
42
43open Sets
44
45open Listb
46
47open LabelledObjects
48
49open Graphs
50
51open I8051
52
53open Order
54
55open Registers
56
57open CostLabel
58
59open Hide
60
61open Proper
62
63open PositiveMap
64
65open Deqsets
66
67open ErrorMessages
68
69open PreIdentifiers
70
71open Errors
72
73open Extralib
74
75open Setoids
76
77open Monad
78
79open Option
80
81open Lists
82
83open Identifiers
84
85open Integers
86
87open AST
88
89open Division
90
91open Exp
92
93open Arithmetic
94
95open Positive
96
97open Z
98
99open BitVectorZ
100
101open Pointers
102
103open ByteValues
104
105open BackEndOps
106
107open Joint
108
109open Joint_LTL_LIN
110
111open LIN
112
113open ASM
114
115open State
116
117type aSM_universe = { id_univ : Identifiers.universe;
118                      current_funct : AST.ident;
119                      ident_map : ASM.identifier0 Identifiers.identifier_map;
120                      label_map : ASM.identifier0 Identifiers.identifier_map
121                                  Identifiers.identifier_map;
122                      address_map : BitVector.word Identifiers.identifier_map }
123
124(** val aSM_universe_rect_Type4 :
125    AST.ident List.list -> (Identifiers.universe -> AST.ident ->
126    ASM.identifier0 Identifiers.identifier_map -> ASM.identifier0
127    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
128    Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **)
129let rec aSM_universe_rect_Type4 globals h_mk_ASM_universe x_24106 =
130  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
131    ident_map0; label_map = label_map0; address_map = address_map0 } =
132    x_24106
133  in
134  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
135    address_map0 __
136
137(** val aSM_universe_rect_Type5 :
138    AST.ident List.list -> (Identifiers.universe -> AST.ident ->
139    ASM.identifier0 Identifiers.identifier_map -> ASM.identifier0
140    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
141    Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **)
142let rec aSM_universe_rect_Type5 globals h_mk_ASM_universe x_24108 =
143  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
144    ident_map0; label_map = label_map0; address_map = address_map0 } =
145    x_24108
146  in
147  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
148    address_map0 __
149
150(** val aSM_universe_rect_Type3 :
151    AST.ident List.list -> (Identifiers.universe -> AST.ident ->
152    ASM.identifier0 Identifiers.identifier_map -> ASM.identifier0
153    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
154    Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **)
155let rec aSM_universe_rect_Type3 globals h_mk_ASM_universe x_24110 =
156  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
157    ident_map0; label_map = label_map0; address_map = address_map0 } =
158    x_24110
159  in
160  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
161    address_map0 __
162
163(** val aSM_universe_rect_Type2 :
164    AST.ident List.list -> (Identifiers.universe -> AST.ident ->
165    ASM.identifier0 Identifiers.identifier_map -> ASM.identifier0
166    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
167    Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **)
168let rec aSM_universe_rect_Type2 globals h_mk_ASM_universe x_24112 =
169  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
170    ident_map0; label_map = label_map0; address_map = address_map0 } =
171    x_24112
172  in
173  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
174    address_map0 __
175
176(** val aSM_universe_rect_Type1 :
177    AST.ident List.list -> (Identifiers.universe -> AST.ident ->
178    ASM.identifier0 Identifiers.identifier_map -> ASM.identifier0
179    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
180    Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **)
181let rec aSM_universe_rect_Type1 globals h_mk_ASM_universe x_24114 =
182  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
183    ident_map0; label_map = label_map0; address_map = address_map0 } =
184    x_24114
185  in
186  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
187    address_map0 __
188
189(** val aSM_universe_rect_Type0 :
190    AST.ident List.list -> (Identifiers.universe -> AST.ident ->
191    ASM.identifier0 Identifiers.identifier_map -> ASM.identifier0
192    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
193    Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **)
194let rec aSM_universe_rect_Type0 globals h_mk_ASM_universe x_24116 =
195  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
196    ident_map0; label_map = label_map0; address_map = address_map0 } =
197    x_24116
198  in
199  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
200    address_map0 __
201
202(** val id_univ :
203    AST.ident List.list -> aSM_universe -> Identifiers.universe **)
204let rec id_univ globals xxx =
205  xxx.id_univ
206
207(** val current_funct : AST.ident List.list -> aSM_universe -> AST.ident **)
208let rec current_funct globals xxx =
209  xxx.current_funct
210
211(** val ident_map :
212    AST.ident List.list -> aSM_universe -> ASM.identifier0
213    Identifiers.identifier_map **)
214let rec ident_map globals xxx =
215  xxx.ident_map
216
217(** val label_map :
218    AST.ident List.list -> aSM_universe -> ASM.identifier0
219    Identifiers.identifier_map Identifiers.identifier_map **)
220let rec label_map globals xxx =
221  xxx.label_map
222
223(** val address_map :
224    AST.ident List.list -> aSM_universe -> BitVector.word
225    Identifiers.identifier_map **)
226let rec address_map globals xxx =
227  xxx.address_map
228
229(** val aSM_universe_inv_rect_Type4 :
230    AST.ident List.list -> aSM_universe -> (Identifiers.universe -> AST.ident
231    -> ASM.identifier0 Identifiers.identifier_map -> ASM.identifier0
232    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
233    Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1 **)
234let aSM_universe_inv_rect_Type4 x1 hterm h1 =
235  let hcut = aSM_universe_rect_Type4 x1 h1 hterm in hcut __
236
237(** val aSM_universe_inv_rect_Type3 :
238    AST.ident List.list -> aSM_universe -> (Identifiers.universe -> AST.ident
239    -> ASM.identifier0 Identifiers.identifier_map -> ASM.identifier0
240    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
241    Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1 **)
242let aSM_universe_inv_rect_Type3 x1 hterm h1 =
243  let hcut = aSM_universe_rect_Type3 x1 h1 hterm in hcut __
244
245(** val aSM_universe_inv_rect_Type2 :
246    AST.ident List.list -> aSM_universe -> (Identifiers.universe -> AST.ident
247    -> ASM.identifier0 Identifiers.identifier_map -> ASM.identifier0
248    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
249    Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1 **)
250let aSM_universe_inv_rect_Type2 x1 hterm h1 =
251  let hcut = aSM_universe_rect_Type2 x1 h1 hterm in hcut __
252
253(** val aSM_universe_inv_rect_Type1 :
254    AST.ident List.list -> aSM_universe -> (Identifiers.universe -> AST.ident
255    -> ASM.identifier0 Identifiers.identifier_map -> ASM.identifier0
256    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
257    Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1 **)
258let aSM_universe_inv_rect_Type1 x1 hterm h1 =
259  let hcut = aSM_universe_rect_Type1 x1 h1 hterm in hcut __
260
261(** val aSM_universe_inv_rect_Type0 :
262    AST.ident List.list -> aSM_universe -> (Identifiers.universe -> AST.ident
263    -> ASM.identifier0 Identifiers.identifier_map -> ASM.identifier0
264    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
265    Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1 **)
266let aSM_universe_inv_rect_Type0 x1 hterm h1 =
267  let hcut = aSM_universe_rect_Type0 x1 h1 hterm in hcut __
268
269(** val aSM_universe_jmdiscr :
270    AST.ident List.list -> aSM_universe -> aSM_universe -> __ **)
271let aSM_universe_jmdiscr a1 x y =
272  Logic.eq_rect_Type2 x
273    (let { id_univ = a0; current_funct = a10; ident_map = a2; label_map = a3;
274       address_map = a4 } = x
275     in
276    Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y
277
278(** val new_ASM_universe : Joint.joint_program -> aSM_universe **)
279let new_ASM_universe p =
280  let globals_addr_internal = fun res_offset x_size ->
281    let { Types.fst = res1; Types.snd = offset0 } = res_offset in
282    let { Types.fst = eta28996; Types.snd = size } = x_size in
283    let { Types.fst = x; Types.snd = region0 } = eta28996 in
284    { Types.fst =
285    (Identifiers.add PreIdentifiers.SymbolTag res1 x
286      (BitVectorZ.bitvector_of_Z (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
287        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
288        Nat.O)))))))))))))))) offset0)); Types.snd =
289    (Z.zplus offset0 (Z.z_of_nat size)) }
290  in
291  let addresses =
292    Util.foldl globals_addr_internal { Types.fst =
293      (Identifiers.empty_map PreIdentifiers.SymbolTag); Types.snd = Z.OZ }
294      p.AST.prog_vars
295  in
296  { id_univ = Positive.One; current_funct = Positive.One; ident_map =
297  (Identifiers.empty_map PreIdentifiers.SymbolTag); label_map =
298  (Identifiers.empty_map PreIdentifiers.SymbolTag); address_map =
299  addresses.Types.fst }
300
301(** val identifier_of_label :
302    AST.ident List.list -> Graphs.label -> ASM.identifier0
303    Monad.smax_def__o__monad **)
304let identifier_of_label g0 l =
305  Obj.magic (fun u ->
306    let current = u.current_funct in
307    let lmap =
308      Identifiers.lookup_def PreIdentifiers.SymbolTag u.label_map current
309        (Identifiers.empty_map PreIdentifiers.LabelTag)
310    in
311    let { Types.fst = eta28997; Types.snd = lmap0 } =
312      match Identifiers.lookup0 PreIdentifiers.LabelTag lmap l with
313      | Types.None ->
314        let { Types.fst = id; Types.snd = univ } =
315          Identifiers.fresh PreIdentifiers.ASMTag u.id_univ
316        in
317        { Types.fst = { Types.fst = id; Types.snd = univ }; Types.snd =
318        (Identifiers.add PreIdentifiers.LabelTag lmap l id) }
319      | Types.Some id ->
320        { Types.fst = { Types.fst = id; Types.snd = u.id_univ }; Types.snd =
321          lmap }
322    in
323    let { Types.fst = id; Types.snd = univ } = eta28997 in
324    { Types.fst = { id_univ = univ; current_funct = current; ident_map =
325    u.ident_map; label_map =
326    (Identifiers.add PreIdentifiers.SymbolTag u.label_map current lmap0);
327    address_map = u.address_map }; Types.snd = id })
328
329(** val identifier_of_ident :
330    AST.ident List.list -> AST.ident -> ASM.identifier0
331    Monad.smax_def__o__monad **)
332let identifier_of_ident g0 i =
333  Obj.magic (fun u ->
334    let imap = u.ident_map in
335    let { Types.fst = eta28998; Types.snd = imap0 } =
336      match Identifiers.lookup0 PreIdentifiers.SymbolTag imap i with
337      | Types.None ->
338        let { Types.fst = id; Types.snd = univ } =
339          Identifiers.fresh PreIdentifiers.ASMTag u.id_univ
340        in
341        { Types.fst = { Types.fst = id; Types.snd = univ }; Types.snd =
342        (Identifiers.add PreIdentifiers.SymbolTag imap i id) }
343      | Types.Some id ->
344        { Types.fst = { Types.fst = id; Types.snd = u.id_univ }; Types.snd =
345          imap }
346    in
347    let { Types.fst = id; Types.snd = univ } = eta28998 in
348    { Types.fst = { id_univ = univ; current_funct = u.current_funct;
349    ident_map = imap0; label_map = u.label_map; address_map =
350    u.address_map }; Types.snd = id })
351
352(** val start_funct_translation :
353    AST.ident List.list -> (AST.ident, Joint.joint_function) Types.prod ->
354    Types.unit0 Monad.smax_def__o__monad **)
355let start_funct_translation g0 id_f =
356  Obj.magic (fun u -> { Types.fst = { id_univ = u.id_univ; current_funct =
357    id_f.Types.fst; ident_map = u.ident_map; label_map = u.label_map;
358    address_map = u.address_map }; Types.snd = Types.It })
359
360(** val address_of_ident :
361    __ List.list -> __ -> ASM.subaddressing_mode Monad.smax_def__o__monad **)
362let address_of_ident globals i =
363  Obj.magic (fun u -> { Types.fst = u; Types.snd = (ASM.DATA16
364    (Identifiers.lookup_safe PreIdentifiers.SymbolTag u.address_map
365      (Obj.magic i))) })
366
367(** val aSM_fresh :
368    AST.ident List.list -> ASM.identifier0 Monad.smax_def__o__monad **)
369let aSM_fresh g0 =
370  Obj.magic (fun u ->
371    let { Types.fst = id; Types.snd = univ } =
372      Identifiers.fresh PreIdentifiers.ASMTag u.id_univ
373    in
374    { Types.fst = { id_univ = univ; current_funct = u.current_funct;
375    ident_map = u.ident_map; label_map = u.label_map; address_map =
376    u.address_map }; Types.snd = id })
377
378(** val register_address : I8051.register -> ASM.subaddressing_mode **)
379let register_address r =
380  (match r with
381   | I8051.Register00 ->
382     (fun _ -> ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
383       (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O,
384       Bool.False, Vector.VEmpty)))))))
385   | I8051.Register01 ->
386     (fun _ -> ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
387       (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O,
388       Bool.True, Vector.VEmpty)))))))
389   | I8051.Register02 ->
390     (fun _ -> ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
391       (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O,
392       Bool.False, Vector.VEmpty)))))))
393   | I8051.Register03 ->
394     (fun _ -> ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
395       (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O,
396       Bool.True, Vector.VEmpty)))))))
397   | I8051.Register04 ->
398     (fun _ -> ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True,
399       (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O,
400       Bool.False, Vector.VEmpty)))))))
401   | I8051.Register05 ->
402     (fun _ -> ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True,
403       (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O,
404       Bool.True, Vector.VEmpty)))))))
405   | I8051.Register06 ->
406     (fun _ -> ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True,
407       (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O,
408       Bool.False, Vector.VEmpty)))))))
409   | I8051.Register07 ->
410     (fun _ -> ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True,
411       (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O,
412       Bool.True, Vector.VEmpty)))))))
413   | I8051.Register10 ->
414     (fun _ -> ASM.DIRECT
415       (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
416         (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
417   | I8051.Register11 ->
418     (fun _ -> ASM.DIRECT
419       (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
420         (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
421   | I8051.Register12 ->
422     (fun _ -> ASM.DIRECT
423       (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
424         (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
425   | I8051.Register13 ->
426     (fun _ -> ASM.DIRECT
427       (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
428         (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
429   | I8051.Register14 ->
430     (fun _ -> ASM.DIRECT
431       (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
432         (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
433   | I8051.Register15 ->
434     (fun _ -> ASM.DIRECT
435       (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
436         (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
437   | I8051.Register16 ->
438     (fun _ -> ASM.DIRECT
439       (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
440         (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
441   | I8051.Register17 ->
442     (fun _ -> ASM.DIRECT
443       (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
444         (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
445   | I8051.Register20 ->
446     (fun _ -> ASM.DIRECT
447       (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
448         (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
449   | I8051.Register21 ->
450     (fun _ -> ASM.DIRECT
451       (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
452         (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
453   | I8051.Register22 ->
454     (fun _ -> ASM.DIRECT
455       (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
456         (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
457   | I8051.Register23 ->
458     (fun _ -> ASM.DIRECT
459       (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
460         (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
461   | I8051.Register24 ->
462     (fun _ -> ASM.DIRECT
463       (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
464         (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
465   | I8051.Register25 ->
466     (fun _ -> ASM.DIRECT
467       (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
468         (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
469   | I8051.Register26 ->
470     (fun _ -> ASM.DIRECT
471       (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
472         (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
473   | I8051.Register27 ->
474     (fun _ -> ASM.DIRECT
475       (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
476         (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
477   | I8051.Register30 ->
478     (fun _ -> ASM.DIRECT
479       (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
480         (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
481   | I8051.Register31 ->
482     (fun _ -> ASM.DIRECT
483       (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
484         (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
485   | I8051.Register32 ->
486     (fun _ -> ASM.DIRECT
487       (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
488         (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
489   | I8051.Register33 ->
490     (fun _ -> ASM.DIRECT
491       (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
492         (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
493   | I8051.Register34 ->
494     (fun _ -> ASM.DIRECT
495       (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
496         (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
497   | I8051.Register35 ->
498     (fun _ -> ASM.DIRECT
499       (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
500         (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
501   | I8051.Register36 ->
502     (fun _ -> ASM.DIRECT
503       (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
504         (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
505   | I8051.Register37 ->
506     (fun _ -> ASM.DIRECT
507       (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
508         (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))
509   | I8051.RegisterA -> (fun _ -> ASM.ACC_A)
510   | I8051.RegisterB ->
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)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
514         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
515         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
516         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
517         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
518         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
519         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
520         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
521         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
522         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
523         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
524         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
525         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
526         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
527         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
528         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
529         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
530         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
531         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
532         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
533         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
534         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
535         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
536         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
537         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
538         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
539         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
540         (Nat.S
541         Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
542   | I8051.RegisterDPL ->
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)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
546         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
547         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
548         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
549         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
550         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
551         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
552         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
553         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
554         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
555         Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
556   | I8051.RegisterDPH ->
557     (fun _ -> ASM.DIRECT
558       (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
559         (Nat.S (Nat.S Nat.O)))))))) (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
569         Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
570   | I8051.RegisterCarry ->
571     (fun _ -> ASM.DIRECT
572       (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
573         (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))) __
574
575(** val vector_cast :
576    Nat.nat -> Nat.nat -> 'a1 -> 'a1 Vector.vector -> 'a1 Vector.vector **)
577let vector_cast n m dflt v =
578  Util.if_then_else_safe (Nat.leb n m) (fun _ ->
579    Vector.append0 (Nat.minus m n) n (Vector.replicate (Nat.minus m n) dflt)
580      v) (fun _ -> (Vector.vsplit (Nat.minus n m) m v).Types.snd)
581
582(** val arg_address : Joint.hdw_argument -> ASM.subaddressing_mode **)
583let arg_address = function
584| Joint.Reg r ->
585  let x =
586    ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S (Nat.S Nat.O))
587      (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S Nat.O)),
588      ASM.Acc_a, (Vector.VCons ((Nat.S Nat.O), ASM.Direct, (Vector.VCons
589      (Nat.O, ASM.Registr, Vector.VEmpty)))))) (Vector.VCons ((Nat.S (Nat.S
590      (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
591      ASM.Direct, (Vector.VCons ((Nat.S Nat.O), ASM.Registr, (Vector.VCons
592      (Nat.O, ASM.Data, Vector.VEmpty)))))))) (register_address r)
593  in
594  x
595| Joint.Imm v -> let x = ASM.DATA v in x
596
597type lin_statement = Joint.joint_statement LabelledObjects.labelled_obj
598
599(** val data_of_int : BitVector.byte -> ASM.addressing_mode **)
600let data_of_int bv =
601  ASM.DATA bv
602
603(** val data16_of_int : Nat.nat -> ASM.addressing_mode **)
604let data16_of_int bv =
605  ASM.DATA16
606    (Arithmetic.bitvector_of_nat (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 (Nat.S
608      Nat.O)))))))))))))))) bv)
609
610(** val accumulator_address : ASM.addressing_mode **)
611let accumulator_address =
612  ASM.DIRECT
613    (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
614      (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
615      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
616      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
617      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
618      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
619      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
620      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
621      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
622      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
623      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
624      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
625      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
626      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
627      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
628      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
629      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
630      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
631      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
632      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
633      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
634      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
635      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
636      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
637      Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
638
639(** val asm_other_bit : ASM.addressing_mode **)
640let asm_other_bit =
641  ASM.BIT_ADDR Joint.zero_byte
642
643(** val translate_statements :
644    AST.ident List.list -> Joint.joint_statement -> ASM.pseudo_instruction
645    Monad.smax_def__o__monad **)
646let translate_statements globals = function
647| Joint.Sequential (instr, x) ->
648  (match instr with
649   | Joint.COST_LABEL lbl ->
650     Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Cost lbl)
651   | Joint.CALL (f, x0, x1) ->
652     (match f with
653      | Types.Inl id ->
654        Monad.m_bind0 (Monad.smax_def State.state_monad)
655          (identifier_of_ident globals id) (fun id' ->
656          Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Call
657            (ASM.toASM_ident PreIdentifiers.ASMTag id')))
658      | Types.Inr x2 ->
659        Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Instruction
660          (ASM.JMP ASM.INDIRECT_DPTR)))
661   | Joint.COND (x0, lbl) ->
662     Monad.m_bind0 (Monad.smax_def State.state_monad)
663       (identifier_of_label globals lbl) (fun l ->
664       Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Instruction
665         (ASM.JNZ l)))
666   | Joint.Step_seq instr' ->
667     (match instr' with
668      | Joint.COMMENT comment ->
669        Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Comment
670          comment)
671      | Joint.MOVE regs ->
672        Monad.m_return0 (Monad.smax_def State.state_monad)
673          (match Obj.magic regs with
674           | Joint_LTL_LIN.From_acc (reg, x0) ->
675             (match ASM.subaddressing_modeel (Nat.S (Nat.S Nat.O))
676                      (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_a,
677                      (Vector.VCons ((Nat.S Nat.O), ASM.Direct, (Vector.VCons
678                      (Nat.O, ASM.Registr, Vector.VEmpty))))))
679                      (register_address reg) with
680              | ASM.DIRECT d ->
681                (fun _ -> ASM.Instruction (ASM.MOV (Types.Inl (Types.Inl
682                  (Types.Inl (Types.Inr { Types.fst = (ASM.DIRECT d);
683                  Types.snd = ASM.ACC_A }))))))
684              | ASM.INDIRECT x1 -> (fun _ -> assert false (* absurd case *))
685              | ASM.EXT_INDIRECT x1 ->
686                (fun _ -> assert false (* absurd case *))
687              | ASM.REGISTER r ->
688                (fun _ -> ASM.Instruction (ASM.MOV (Types.Inl (Types.Inl
689                  (Types.Inl (Types.Inl (Types.Inr { Types.fst =
690                  (ASM.REGISTER r); Types.snd = ASM.ACC_A })))))))
691              | ASM.ACC_A -> (fun _ -> ASM.Instruction ASM.NOP)
692              | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
693              | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
694              | ASM.DATA x1 -> (fun _ -> assert false (* absurd case *))
695              | ASM.DATA16 x1 -> (fun _ -> assert false (* absurd case *))
696              | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
697              | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
698              | ASM.EXT_INDIRECT_DPTR ->
699                (fun _ -> assert false (* absurd case *))
700              | ASM.INDIRECT_DPTR ->
701                (fun _ -> assert false (* absurd case *))
702              | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
703              | ASM.BIT_ADDR x1 -> (fun _ -> assert false (* absurd case *))
704              | ASM.N_BIT_ADDR x1 ->
705                (fun _ -> assert false (* absurd case *))
706              | ASM.RELATIVE x1 -> (fun _ -> assert false (* absurd case *))
707              | ASM.ADDR11 x1 -> (fun _ -> assert false (* absurd case *))
708              | ASM.ADDR16 x1 -> (fun _ -> assert false (* absurd case *)))
709               __
710           | Joint_LTL_LIN.To_acc (x0, reg) ->
711             (match ASM.subaddressing_modeel (Nat.S (Nat.S Nat.O))
712                      (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_a,
713                      (Vector.VCons ((Nat.S Nat.O), ASM.Direct, (Vector.VCons
714                      (Nat.O, ASM.Registr, Vector.VEmpty))))))
715                      (register_address reg) with
716              | ASM.DIRECT d ->
717                (fun _ -> ASM.Instruction (ASM.MOV (Types.Inl (Types.Inl
718                  (Types.Inl (Types.Inl (Types.Inl { Types.fst = ASM.ACC_A;
719                  Types.snd = (ASM.DIRECT d) })))))))
720              | ASM.INDIRECT x1 -> (fun _ -> assert false (* absurd case *))
721              | ASM.EXT_INDIRECT x1 ->
722                (fun _ -> assert false (* absurd case *))
723              | ASM.REGISTER r ->
724                (fun _ -> ASM.Instruction (ASM.MOV (Types.Inl (Types.Inl
725                  (Types.Inl (Types.Inl (Types.Inl { Types.fst = ASM.ACC_A;
726                  Types.snd = (ASM.REGISTER r) })))))))
727              | ASM.ACC_A -> (fun _ -> ASM.Instruction ASM.NOP)
728              | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
729              | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
730              | ASM.DATA x1 -> (fun _ -> assert false (* absurd case *))
731              | ASM.DATA16 x1 -> (fun _ -> assert false (* absurd case *))
732              | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
733              | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
734              | ASM.EXT_INDIRECT_DPTR ->
735                (fun _ -> assert false (* absurd case *))
736              | ASM.INDIRECT_DPTR ->
737                (fun _ -> assert false (* absurd case *))
738              | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
739              | ASM.BIT_ADDR x1 -> (fun _ -> assert false (* absurd case *))
740              | ASM.N_BIT_ADDR x1 ->
741                (fun _ -> assert false (* absurd case *))
742              | ASM.RELATIVE x1 -> (fun _ -> assert false (* absurd case *))
743              | ASM.ADDR11 x1 -> (fun _ -> assert false (* absurd case *))
744              | ASM.ADDR16 x1 -> (fun _ -> assert false (* absurd case *)))
745               __
746           | Joint_LTL_LIN.Int_to_reg (reg, b) ->
747             (match ASM.subaddressing_modeel (Nat.S (Nat.S Nat.O))
748                      (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_a,
749                      (Vector.VCons ((Nat.S Nat.O), ASM.Direct, (Vector.VCons
750                      (Nat.O, ASM.Registr, Vector.VEmpty))))))
751                      (register_address reg) with
752              | ASM.DIRECT d ->
753                (fun _ -> ASM.Instruction (ASM.MOV (Types.Inl (Types.Inl
754                  (Types.Inl (Types.Inr { Types.fst = (ASM.DIRECT d);
755                  Types.snd = (ASM.DATA b) }))))))
756              | ASM.INDIRECT x0 -> (fun _ -> assert false (* absurd case *))
757              | ASM.EXT_INDIRECT x0 ->
758                (fun _ -> assert false (* absurd case *))
759              | ASM.REGISTER r ->
760                (fun _ -> ASM.Instruction (ASM.MOV (Types.Inl (Types.Inl
761                  (Types.Inl (Types.Inl (Types.Inr { Types.fst =
762                  (ASM.REGISTER r); Types.snd = (ASM.DATA b) })))))))
763              | ASM.ACC_A ->
764                (fun _ ->
765                  match BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
766                          (Nat.S (Nat.S (Nat.S Nat.O))))))))
767                          (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
768                            (Nat.S (Nat.S (Nat.S Nat.O))))))))) b with
769                  | Bool.True -> ASM.Instruction (ASM.CLR ASM.ACC_A)
770                  | Bool.False ->
771                    ASM.Instruction (ASM.MOV (Types.Inl (Types.Inl (Types.Inl
772                      (Types.Inl (Types.Inl { Types.fst = ASM.ACC_A;
773                      Types.snd = (ASM.DATA b) })))))))
774              | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
775              | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
776              | ASM.DATA x0 -> (fun _ -> assert false (* absurd case *))
777              | ASM.DATA16 x0 -> (fun _ -> assert false (* absurd case *))
778              | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
779              | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
780              | ASM.EXT_INDIRECT_DPTR ->
781                (fun _ -> assert false (* absurd case *))
782              | ASM.INDIRECT_DPTR ->
783                (fun _ -> assert false (* absurd case *))
784              | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
785              | ASM.BIT_ADDR x0 -> (fun _ -> assert false (* absurd case *))
786              | ASM.N_BIT_ADDR x0 ->
787                (fun _ -> assert false (* absurd case *))
788              | ASM.RELATIVE x0 -> (fun _ -> assert false (* absurd case *))
789              | ASM.ADDR11 x0 -> (fun _ -> assert false (* absurd case *))
790              | ASM.ADDR16 x0 -> (fun _ -> assert false (* absurd case *)))
791               __
792           | Joint_LTL_LIN.Int_to_acc (x0, b) ->
793             (match BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
794                      (Nat.S (Nat.S Nat.O))))))))
795                      (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
796                        (Nat.S (Nat.S (Nat.S Nat.O))))))))) b with
797              | Bool.True -> ASM.Instruction (ASM.CLR ASM.ACC_A)
798              | Bool.False ->
799                ASM.Instruction (ASM.MOV (Types.Inl (Types.Inl (Types.Inl
800                  (Types.Inl (Types.Inl { Types.fst = ASM.ACC_A; Types.snd =
801                  (ASM.DATA b) }))))))))
802      | Joint.POP x0 ->
803        Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Instruction
804          (ASM.POP accumulator_address))
805      | Joint.PUSH x0 ->
806        Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Instruction
807          (ASM.PUSH accumulator_address))
808      | Joint.ADDRESS (addr, x0, x1) ->
809        Monad.m_bind0 (Monad.smax_def State.state_monad)
810          (address_of_ident (Obj.magic globals) (Obj.magic addr))
811          (fun addr' ->
812          Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Instruction
813            (ASM.MOV (Types.Inl (Types.Inl (Types.Inr { Types.fst = ASM.DPTR;
814            Types.snd = addr' }))))))
815      | Joint.OPACCS (accs, x0, x1, x2, x3) ->
816        Monad.m_return0 (Monad.smax_def State.state_monad)
817          (match accs with
818           | BackEndOps.Mul ->
819             ASM.Instruction (ASM.MUL (ASM.ACC_A, ASM.ACC_B))
820           | BackEndOps.DivuModu ->
821             ASM.Instruction (ASM.DIV (ASM.ACC_A, ASM.ACC_B)))
822      | Joint.OP1 (op4, x0, x1) ->
823        Monad.m_return0 (Monad.smax_def State.state_monad)
824          (match op4 with
825           | BackEndOps.Cmpl -> ASM.Instruction (ASM.CPL ASM.ACC_A)
826           | BackEndOps.Inc -> ASM.Instruction (ASM.INC ASM.ACC_A)
827           | BackEndOps.Rl -> ASM.Instruction (ASM.RL ASM.ACC_A))
828      | Joint.OP2 (op4, x0, x1, reg) ->
829        Monad.m_return0 (Monad.smax_def State.state_monad)
830          ((match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O)))
831                    (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a,
832                    (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Direct,
833                    (Vector.VCons ((Nat.S Nat.O), ASM.Registr, (Vector.VCons
834                    (Nat.O, ASM.Data, Vector.VEmpty))))))))
835                    (arg_address (Obj.magic reg)) with
836            | ASM.DIRECT d ->
837              (fun _ ->
838                match op4 with
839                | BackEndOps.Add ->
840                  ASM.Instruction (ASM.ADD (ASM.ACC_A, (ASM.DIRECT d)))
841                | BackEndOps.Addc ->
842                  ASM.Instruction (ASM.ADDC (ASM.ACC_A, (ASM.DIRECT d)))
843                | BackEndOps.Sub ->
844                  ASM.Instruction (ASM.SUBB (ASM.ACC_A, (ASM.DIRECT d)))
845                | BackEndOps.And ->
846                  ASM.Instruction (ASM.ANL (Types.Inl (Types.Inl
847                    { Types.fst = ASM.ACC_A; Types.snd = (ASM.DIRECT d) })))
848                | BackEndOps.Or ->
849                  ASM.Instruction (ASM.ORL (Types.Inl (Types.Inl
850                    { Types.fst = ASM.ACC_A; Types.snd = (ASM.DIRECT d) })))
851                | BackEndOps.Xor ->
852                  ASM.Instruction (ASM.XRL (Types.Inl { Types.fst =
853                    ASM.ACC_A; Types.snd = (ASM.DIRECT d) })))
854            | ASM.INDIRECT x2 -> (fun _ -> assert false (* absurd case *))
855            | ASM.EXT_INDIRECT x2 ->
856              (fun _ -> assert false (* absurd case *))
857            | ASM.REGISTER r ->
858              (fun _ ->
859                match op4 with
860                | BackEndOps.Add ->
861                  ASM.Instruction (ASM.ADD (ASM.ACC_A, (ASM.REGISTER r)))
862                | BackEndOps.Addc ->
863                  ASM.Instruction (ASM.ADDC (ASM.ACC_A, (ASM.REGISTER r)))
864                | BackEndOps.Sub ->
865                  ASM.Instruction (ASM.SUBB (ASM.ACC_A, (ASM.REGISTER r)))
866                | BackEndOps.And ->
867                  ASM.Instruction (ASM.ANL (Types.Inl (Types.Inl
868                    { Types.fst = ASM.ACC_A; Types.snd = (ASM.REGISTER
869                    r) })))
870                | BackEndOps.Or ->
871                  ASM.Instruction (ASM.ORL (Types.Inl (Types.Inl
872                    { Types.fst = ASM.ACC_A; Types.snd = (ASM.REGISTER
873                    r) })))
874                | BackEndOps.Xor ->
875                  ASM.Instruction (ASM.XRL (Types.Inl { Types.fst =
876                    ASM.ACC_A; Types.snd = (ASM.REGISTER r) })))
877            | ASM.ACC_A ->
878              (fun _ ->
879                match op4 with
880                | BackEndOps.Add ->
881                  ASM.Instruction (ASM.ADD (ASM.ACC_A, accumulator_address))
882                | BackEndOps.Addc ->
883                  ASM.Instruction (ASM.ADDC (ASM.ACC_A, accumulator_address))
884                | BackEndOps.Sub ->
885                  ASM.Instruction (ASM.SUBB (ASM.ACC_A, accumulator_address))
886                | BackEndOps.And -> ASM.Instruction ASM.NOP
887                | BackEndOps.Or -> ASM.Instruction ASM.NOP
888                | BackEndOps.Xor -> ASM.Instruction (ASM.CLR ASM.ACC_A))
889            | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
890            | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
891            | ASM.DATA b ->
892              (fun _ ->
893                match op4 with
894                | BackEndOps.Add ->
895                  ASM.Instruction (ASM.ADD (ASM.ACC_A, (ASM.DATA b)))
896                | BackEndOps.Addc ->
897                  ASM.Instruction (ASM.ADDC (ASM.ACC_A, (ASM.DATA b)))
898                | BackEndOps.Sub ->
899                  ASM.Instruction (ASM.SUBB (ASM.ACC_A, (ASM.DATA b)))
900                | BackEndOps.And ->
901                  ASM.Instruction (ASM.ANL (Types.Inl (Types.Inl
902                    { Types.fst = ASM.ACC_A; Types.snd = (ASM.DATA b) })))
903                | BackEndOps.Or ->
904                  ASM.Instruction (ASM.ORL (Types.Inl (Types.Inl
905                    { Types.fst = ASM.ACC_A; Types.snd = (ASM.DATA b) })))
906                | BackEndOps.Xor ->
907                  ASM.Instruction (ASM.XRL (Types.Inl { Types.fst =
908                    ASM.ACC_A; Types.snd = (ASM.DATA b) })))
909            | ASM.DATA16 x2 -> (fun _ -> assert false (* absurd case *))
910            | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
911            | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
912            | ASM.EXT_INDIRECT_DPTR ->
913              (fun _ -> assert false (* absurd case *))
914            | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
915            | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
916            | ASM.BIT_ADDR x2 -> (fun _ -> assert false (* absurd case *))
917            | ASM.N_BIT_ADDR x2 -> (fun _ -> assert false (* absurd case *))
918            | ASM.RELATIVE x2 -> (fun _ -> assert false (* absurd case *))
919            | ASM.ADDR11 x2 -> (fun _ -> assert false (* absurd case *))
920            | ASM.ADDR16 x2 -> (fun _ -> assert false (* absurd case *))) __)
921      | Joint.CLEAR_CARRY ->
922        Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Instruction
923          (ASM.CLR ASM.CARRY))
924      | Joint.SET_CARRY ->
925        Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Instruction
926          (ASM.SETB ASM.CARRY))
927      | Joint.LOAD (x0, x1, x2) ->
928        Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Instruction
929          (ASM.MOVX (Types.Inl { Types.fst = ASM.ACC_A; Types.snd =
930          ASM.EXT_INDIRECT_DPTR })))
931      | Joint.STORE (x0, x1, x2) ->
932        Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Instruction
933          (ASM.MOVX (Types.Inr { Types.fst = ASM.EXT_INDIRECT_DPTR;
934          Types.snd = ASM.ACC_A })))
935      | Joint.Extension_seq ext ->
936        (match Obj.magic ext with
937         | Joint_LTL_LIN.SAVE_CARRY ->
938           Monad.m_return0 (Monad.smax_def State.state_monad)
939             (ASM.Instruction (ASM.MOV (Types.Inr { Types.fst =
940             asm_other_bit; Types.snd = ASM.CARRY })))
941         | Joint_LTL_LIN.RESTORE_CARRY ->
942           Monad.m_return0 (Monad.smax_def State.state_monad)
943             (ASM.Instruction (ASM.MOV (Types.Inl (Types.Inr { Types.fst =
944             ASM.CARRY; Types.snd = asm_other_bit }))))
945         | Joint_LTL_LIN.LOW_ADDRESS (reg, lbl) ->
946           Monad.m_bind0 (Monad.smax_def State.state_monad)
947             (identifier_of_label globals lbl) (fun lbl' ->
948             Monad.m_return0 (Monad.smax_def State.state_monad)
949               (ASM.MovSuccessor ((register_address reg), ASM.LOW, lbl')))
950         | Joint_LTL_LIN.HIGH_ADDRESS (reg, lbl) ->
951           Monad.m_bind0 (Monad.smax_def State.state_monad)
952             (identifier_of_label globals lbl) (fun lbl' ->
953             Monad.m_return0 (Monad.smax_def State.state_monad)
954               (ASM.MovSuccessor ((register_address reg), ASM.HIGH, lbl'))))))
955| Joint.Final instr ->
956  (match instr with
957   | Joint.GOTO lbl ->
958     Monad.m_bind0 (Monad.smax_def State.state_monad)
959       (identifier_of_label globals lbl) (fun lbl' ->
960       Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Jmp
961         (ASM.toASM_ident PreIdentifiers.LabelTag lbl)))
962   | Joint.RETURN ->
963     Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Instruction
964       ASM.RET)
965   | Joint.TAILCALL (x, x0) -> assert false (* absurd case *))
966| Joint.FCOND (x0, lbl_true, lbl_false) ->
967  Monad.m_bind0 (Monad.smax_def State.state_monad)
968    (identifier_of_label globals lbl_true) (fun l1 ->
969    Monad.m_bind0 (Monad.smax_def State.state_monad)
970      (identifier_of_label globals lbl_false) (fun l2 ->
971      Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Jnz (ASM.ACC_A,
972        l1, l2))))
973
974(** val build_translated_statement :
975    AST.ident List.list -> lin_statement -> __ **)
976let build_translated_statement globals statement =
977  Monad.m_bind0 (Monad.smax_def State.state_monad)
978    (translate_statements globals statement.Types.snd) (fun stmt ->
979    match statement.Types.fst with
980    | Types.None ->
981      Monad.m_return0 (Monad.smax_def State.state_monad) { Types.fst =
982        Types.None; Types.snd = stmt }
983    | Types.Some lbl ->
984      Monad.m_bind0 (Monad.smax_def State.state_monad)
985        (identifier_of_label globals lbl) (fun lbl' ->
986        Monad.m_return0 (Monad.smax_def State.state_monad) { Types.fst =
987          (Types.Some lbl'); Types.snd = stmt }))
988
989(** val translate_code :
990    AST.ident List.list -> lin_statement List.list -> __ **)
991let translate_code globals code =
992  Monad.m_list_map (Monad.smax_def State.state_monad)
993    (build_translated_statement globals) code
994
995(** val translate_fun_def :
996    AST.ident List.list -> (AST.ident, Joint.joint_function) Types.prod -> __ **)
997let translate_fun_def globals id_def =
998  Monad.m_bind0 (Monad.smax_def State.state_monad)
999    (start_funct_translation globals id_def) (fun x ->
1000    match id_def.Types.snd with
1001    | AST.Internal int0 ->
1002      let code = (Types.pi1 int0).Joint.joint_if_code in
1003      Monad.m_bind0 (Monad.smax_def State.state_monad)
1004        (identifier_of_ident globals id_def.Types.fst) (fun id ->
1005        Monad.m_bind0 (Monad.smax_def State.state_monad)
1006          (translate_code globals (Obj.magic code)) (fun code' ->
1007          match code' with
1008          | List.Nil ->
1009            Monad.m_return0 (Monad.smax_def State.state_monad) (List.Cons
1010              ({ Types.fst = (Types.Some id); Types.snd = (ASM.Instruction
1011              ASM.RET) }, List.Nil))
1012          | List.Cons (hd0, tl) ->
1013            (match hd0.Types.fst with
1014             | Types.None ->
1015               Monad.m_return0 (Monad.smax_def State.state_monad) (List.Cons
1016                 ({ Types.fst = (Types.Some id); Types.snd = hd0.Types.snd },
1017                 tl))
1018             | Types.Some x0 ->
1019               Monad.m_return0 (Monad.smax_def State.state_monad) (List.Cons
1020                 ({ Types.fst = (Types.Some id); Types.snd = (ASM.Instruction
1021                 ASM.NOP) }, (List.Cons (hd0, tl)))))))
1022    | AST.External x0 ->
1023      Monad.m_return0 (Monad.smax_def State.state_monad) List.Nil)
1024
1025(** val lin_to_asm : LIN.lin_program -> ASM.pseudo_assembly_program **)
1026let lin_to_asm p =
1027  State.state_run (new_ASM_universe p)
1028    (let add_translation = fun acc id_def ->
1029       Monad.m_bind0 (Monad.smax_def State.state_monad)
1030         (translate_fun_def
1031           (List.map (fun x -> x.Types.fst.Types.fst) p.AST.prog_vars)
1032           id_def) (fun code ->
1033         Monad.m_bind0 (Monad.smax_def State.state_monad) acc (fun acc0 ->
1034           Monad.m_return0 (Monad.smax_def State.state_monad)
1035             (List.append code acc0)))
1036     in
1037    Monad.m_bind0 (Monad.smax_def State.state_monad)
1038      (Util.foldl add_translation
1039        (Monad.m_return0 (Monad.smax_def State.state_monad) List.Nil)
1040        p.AST.prog_funct) (fun code ->
1041      Monad.m_bind0 (Monad.smax_def State.state_monad)
1042        (aSM_fresh
1043          (List.map (fun x -> x.Types.fst.Types.fst) p.AST.prog_vars))
1044        (fun exit_label ->
1045        Monad.m_bind0 (Monad.smax_def State.state_monad)
1046          (identifier_of_ident
1047            (List.map (fun x -> x.Types.fst.Types.fst) p.AST.prog_vars)
1048            p.AST.prog_main) (fun main ->
1049          let code0 = List.Cons ({ Types.fst = Types.None; Types.snd =
1050            (ASM.Call main) }, (List.Cons ({ Types.fst = (Types.Some
1051            exit_label); Types.snd = (ASM.Jmp exit_label) }, code)))
1052          in
1053          Monad.m_return0 (Monad.smax_def State.state_monad) { Types.fst =
1054            List.Nil; Types.snd = code0 }))))
1055
Note: See TracBrowser for help on using the repository browser.