source: extracted/lINToASM.ml @ 2731

Last change on this file since 2731 was 2730, checked in by sacerdot, 7 years ago

Exported again.

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