source: extracted/lINToASM.ml @ 3019

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

New extraction after ERTLptr abortion.

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