source: extracted/lINToASM.ml @ 2797

Last change on this file since 2797 was 2797, checked in by sacerdot, 8 years ago

Extracted again after James's cleanup and the implementation of the
new testing function to be used in the untrusted code.

File size: 49.0 KB
Line 
1open Preamble
2
3open Deqsets
4
5open Setoids
6
7open Monad
8
9open Option
10
11open Extranat
12
13open Vector
14
15open Div_and_mod
16
17open Jmeq
18
19open Russell
20
21open List
22
23open Util
24
25open FoldStuff
26
27open Bool
28
29open Relations
30
31open Nat
32
33open BitVector
34
35open Hints_declaration
36
37open Core_notation
38
39open Pts
40
41open Logic
42
43open Types
44
45open BitVectorTrie
46
47open BitVectorTrieSet
48
49open State
50
51open String
52
53open Exp
54
55open Arithmetic
56
57open Integers
58
59open AST
60
61open LabelledObjects
62
63open Proper
64
65open PositiveMap
66
67open ErrorMessages
68
69open PreIdentifiers
70
71open Errors
72
73open Extralib
74
75open Lists
76
77open Positive
78
79open Identifiers
80
81open CostLabel
82
83open ASM
84
85open Sets
86
87open Listb
88
89open Graphs
90
91open I8051
92
93open Order
94
95open Registers
96
97open Hide
98
99open Division
100
101open Z
102
103open BitVectorZ
104
105open Pointers
106
107open ByteValues
108
109open BackEndOps
110
111open Joint
112
113open Joint_LTL_LIN
114
115open LIN
116
117type aSM_universe = { id_univ : Identifiers.universe;
118                      current_funct : AST.ident;
119                      ident_map : ASM.identifier Identifiers.identifier_map;
120                      label_map : ASM.identifier 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.identifier Identifiers.identifier_map -> ASM.identifier
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_24287 =
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_24287
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.identifier Identifiers.identifier_map -> ASM.identifier
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_24289 =
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_24289
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.identifier Identifiers.identifier_map -> ASM.identifier
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_24291 =
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_24291
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.identifier Identifiers.identifier_map -> ASM.identifier
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_24293 =
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_24293
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.identifier Identifiers.identifier_map -> ASM.identifier
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_24295 =
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_24295
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.identifier Identifiers.identifier_map -> ASM.identifier
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_24297 =
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_24297
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.identifier
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.identifier
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.identifier Identifiers.identifier_map -> ASM.identifier
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.identifier Identifiers.identifier_map -> ASM.identifier
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.identifier Identifiers.identifier_map -> ASM.identifier
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.identifier Identifiers.identifier_map -> ASM.identifier
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.identifier Identifiers.identifier_map -> ASM.identifier
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 = res; Types.snd = offset } = res_offset in
282    let { Types.fst = eta29046; Types.snd = size } = x_size in
283    let { Types.fst = x; Types.snd = region } = eta29046 in
284    { Types.fst =
285    (Identifiers.add PreIdentifiers.SymbolTag res 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)))))))))))))))) offset)); Types.snd =
289    (Z.zplus offset (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.identifier
303    Monad.smax_def__o__monad **)
304let identifier_of_label g 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 = eta29047; Types.snd = lmap0 } =
312      match Identifiers.lookup 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 } = eta29047 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.identifier
331    Monad.smax_def__o__monad **)
332let identifier_of_ident g i =
333  Obj.magic (fun u ->
334    let imap = u.ident_map in
335    let { Types.fst = eta29048; Types.snd = imap0 } =
336      match Identifiers.lookup 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 } = eta29048 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 g 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.identifier Monad.smax_def__o__monad **)
369let aSM_fresh g =
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.append (Nat.minus m n) n (Vector.replicate (Nat.minus m n) dflt) v)
580    (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 (op1, x0, x1) ->
823        Monad.m_return0 (Monad.smax_def State.state_monad)
824          (match op1 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 (op2, 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 op2 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 op2 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 op2 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 op2 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 int ->
1002      let code = (Types.pi1 int).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 (hd, tl) ->
1013            (match hd.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 = hd.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 (hd, tl)))))))
1022    | AST.External x0 ->
1023      Monad.m_return0 (Monad.smax_def State.state_monad) List.Nil)
1024
1025(** val get_symboltable :
1026    AST.ident List.list -> (ASM.identifier, AST.ident) Types.prod List.list
1027    Monad.smax_def__o__monad **)
1028let get_symboltable globals =
1029  Obj.magic (fun u ->
1030    let imap = u.ident_map in
1031    let f = fun iold inew x -> List.Cons ({ Types.fst = inew; Types.snd =
1032      iold }, x)
1033    in
1034    { Types.fst = u; Types.snd =
1035    (Identifiers.foldi PreIdentifiers.SymbolTag f imap List.Nil) })
1036
1037(** val lin_to_asm :
1038    LIN.lin_program -> ASM.pseudo_assembly_program Types.option **)
1039let lin_to_asm p =
1040  State.state_run (new_ASM_universe p)
1041    (let add_translation = fun acc id_def ->
1042       Monad.m_bind0 (Monad.smax_def State.state_monad)
1043         (translate_fun_def
1044           (List.map (fun x -> x.Types.fst.Types.fst) p.AST.prog_vars)
1045           id_def) (fun code ->
1046         Monad.m_bind0 (Monad.smax_def State.state_monad) acc (fun acc0 ->
1047           Monad.m_return0 (Monad.smax_def State.state_monad)
1048             (List.append code acc0)))
1049     in
1050    Monad.m_bind0 (Monad.smax_def State.state_monad)
1051      (Util.foldl add_translation
1052        (Monad.m_return0 (Monad.smax_def State.state_monad) List.Nil)
1053        p.AST.prog_funct) (fun code ->
1054      Monad.m_bind0 (Monad.smax_def State.state_monad)
1055        (aSM_fresh
1056          (List.map (fun x -> x.Types.fst.Types.fst) p.AST.prog_vars))
1057        (fun exit_label ->
1058        Monad.m_bind0 (Monad.smax_def State.state_monad)
1059          (identifier_of_ident
1060            (List.map (fun x -> x.Types.fst.Types.fst) p.AST.prog_vars)
1061            p.AST.prog_main) (fun main ->
1062          Monad.m_bind0 (Monad.smax_def State.state_monad)
1063            (get_symboltable
1064              (List.map (fun x -> x.Types.fst.Types.fst) p.AST.prog_vars))
1065            (fun symboltable ->
1066            Monad.m_return0 (Monad.smax_def State.state_monad)
1067              (let code0 = List.Cons ({ Types.fst = Types.None; Types.snd =
1068                 (ASM.Call main) }, (List.Cons ({ Types.fst = (Types.Some
1069                 exit_label); Types.snd = (ASM.Jmp exit_label) }, code)))
1070               in
1071              Monad.m_bind0 (Monad.max_def Option.option)
1072                (Obj.magic (ASM.code_size_opt code0)) (fun _ ->
1073                Monad.m_return0 (Monad.max_def Option.option)
1074                  { ASM.preamble = List.Nil; ASM.code = code0;
1075                  ASM.renamed_symbols = symboltable; ASM.final_label =
1076                  exit_label })))))))
1077
Note: See TracBrowser for help on using the repository browser.