source: extracted/lINToASM.ml @ 2960

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

New extraction, it diverges in RTL execution now.

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