source: extracted/lINToASM.ml @ 3001

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

New extraction.

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_5553 =
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_5553
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_5555 =
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_5555
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_5557 =
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_5557
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_5559 =
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_5559
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_5561 =
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_5561
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_5563 =
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_5563
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 = eta27394; Types.snd = data } = x_size in
323    let { Types.fst = x; Types.snd = region } = eta27394 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
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 = eta27395; 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 } = eta27395 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 = eta27396; 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 } = eta27396 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 (reg, 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 reg), ASM.LOW, lbl')))
997         | Joint_LTL_LIN.HIGH_ADDRESS (reg, lbl) ->
998           Monad.m_bind0 (Monad.smax_def State.state_monad)
999             (identifier_of_label globals lbl) (fun lbl' ->
1000             Monad.m_return0 (Monad.smax_def State.state_monad)
1001               (ASM.MovSuccessor ((register_address reg), ASM.HIGH, lbl'))))))
1002| Joint.Final instr ->
1003  (match instr with
1004   | Joint.GOTO lbl ->
1005     Monad.m_bind0 (Monad.smax_def State.state_monad)
1006       (identifier_of_label globals lbl) (fun lbl' ->
1007       Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Jmp
1008         (ASM.toASM_ident PreIdentifiers.LabelTag lbl)))
1009   | Joint.RETURN ->
1010     Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Instruction
1011       ASM.RET)
1012   | Joint.TAILCALL (x, x0) -> assert false (* absurd case *))
1013| Joint.FCOND (x0, lbl_true, lbl_false) ->
1014  Monad.m_bind0 (Monad.smax_def State.state_monad)
1015    (identifier_of_label globals lbl_true) (fun l1 ->
1016    Monad.m_bind0 (Monad.smax_def State.state_monad)
1017      (identifier_of_label globals lbl_false) (fun l2 ->
1018      Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Jnz (ASM.ACC_A,
1019        l1, l2))))
1020
1021(** val build_translated_statement :
1022    AST.ident List.list -> lin_statement -> __ **)
1023let build_translated_statement globals statement =
1024  Monad.m_bind0 (Monad.smax_def State.state_monad)
1025    (translate_statements globals statement.Types.snd) (fun stmt ->
1026    match statement.Types.fst with
1027    | Types.None ->
1028      Monad.m_return0 (Monad.smax_def State.state_monad) { Types.fst =
1029        Types.None; Types.snd = stmt }
1030    | Types.Some lbl ->
1031      Monad.m_bind0 (Monad.smax_def State.state_monad)
1032        (identifier_of_label globals lbl) (fun lbl' ->
1033        Monad.m_return0 (Monad.smax_def State.state_monad) { Types.fst =
1034          (Types.Some lbl'); Types.snd = stmt }))
1035
1036(** val translate_code :
1037    AST.ident List.list -> lin_statement List.list -> __ **)
1038let translate_code globals code =
1039  Monad.m_list_map (Monad.smax_def State.state_monad)
1040    (build_translated_statement globals) code
1041
1042(** val translate_fun_def :
1043    AST.ident List.list -> (AST.ident, Joint.joint_function) Types.prod -> __ **)
1044let translate_fun_def globals id_def =
1045  Monad.m_bind0 (Monad.smax_def State.state_monad)
1046    (start_funct_translation globals id_def) (fun x ->
1047    match id_def.Types.snd with
1048    | AST.Internal int ->
1049      let code = (Types.pi1 int).Joint.joint_if_code in
1050      Monad.m_bind0 (Monad.smax_def State.state_monad)
1051        (identifier_of_ident globals id_def.Types.fst) (fun id ->
1052        Monad.m_bind0 (Monad.smax_def State.state_monad)
1053          (translate_code globals (Obj.magic code)) (fun code' ->
1054          match code' with
1055          | List.Nil ->
1056            Monad.m_return0 (Monad.smax_def State.state_monad) (List.Cons
1057              ({ Types.fst = (Types.Some id); Types.snd = (ASM.Instruction
1058              ASM.RET) }, List.Nil))
1059          | List.Cons (hd, tl) ->
1060            (match hd.Types.fst with
1061             | Types.None ->
1062               Monad.m_return0 (Monad.smax_def State.state_monad) (List.Cons
1063                 ({ Types.fst = (Types.Some id); Types.snd = hd.Types.snd },
1064                 tl))
1065             | Types.Some x0 ->
1066               Monad.m_return0 (Monad.smax_def State.state_monad) (List.Cons
1067                 ({ Types.fst = (Types.Some id); Types.snd = (ASM.Instruction
1068                 ASM.NOP) }, (List.Cons (hd, tl)))))))
1069    | AST.External x0 ->
1070      Monad.m_return0 (Monad.smax_def State.state_monad) List.Nil)
1071
1072type init_mutable = { virtual_dptr : Z.z; actual_dptr : Z.z;
1073                      built : ASM.labelled_instruction List.list }
1074
1075(** val init_mutable_rect_Type4 :
1076    (Z.z -> Z.z -> ASM.labelled_instruction List.list -> 'a1) -> init_mutable
1077    -> 'a1 **)
1078let rec init_mutable_rect_Type4 h_mk_init_mutable x_5580 =
1079  let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0; built =
1080    built0 } = x_5580
1081  in
1082  h_mk_init_mutable virtual_dptr0 actual_dptr0 built0
1083
1084(** val init_mutable_rect_Type5 :
1085    (Z.z -> Z.z -> ASM.labelled_instruction List.list -> 'a1) -> init_mutable
1086    -> 'a1 **)
1087let rec init_mutable_rect_Type5 h_mk_init_mutable x_5582 =
1088  let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0; built =
1089    built0 } = x_5582
1090  in
1091  h_mk_init_mutable virtual_dptr0 actual_dptr0 built0
1092
1093(** val init_mutable_rect_Type3 :
1094    (Z.z -> Z.z -> ASM.labelled_instruction List.list -> 'a1) -> init_mutable
1095    -> 'a1 **)
1096let rec init_mutable_rect_Type3 h_mk_init_mutable x_5584 =
1097  let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0; built =
1098    built0 } = x_5584
1099  in
1100  h_mk_init_mutable virtual_dptr0 actual_dptr0 built0
1101
1102(** val init_mutable_rect_Type2 :
1103    (Z.z -> Z.z -> ASM.labelled_instruction List.list -> 'a1) -> init_mutable
1104    -> 'a1 **)
1105let rec init_mutable_rect_Type2 h_mk_init_mutable x_5586 =
1106  let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0; built =
1107    built0 } = x_5586
1108  in
1109  h_mk_init_mutable virtual_dptr0 actual_dptr0 built0
1110
1111(** val init_mutable_rect_Type1 :
1112    (Z.z -> Z.z -> ASM.labelled_instruction List.list -> 'a1) -> init_mutable
1113    -> 'a1 **)
1114let rec init_mutable_rect_Type1 h_mk_init_mutable x_5588 =
1115  let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0; built =
1116    built0 } = x_5588
1117  in
1118  h_mk_init_mutable virtual_dptr0 actual_dptr0 built0
1119
1120(** val init_mutable_rect_Type0 :
1121    (Z.z -> Z.z -> ASM.labelled_instruction List.list -> 'a1) -> init_mutable
1122    -> 'a1 **)
1123let rec init_mutable_rect_Type0 h_mk_init_mutable x_5590 =
1124  let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0; built =
1125    built0 } = x_5590
1126  in
1127  h_mk_init_mutable virtual_dptr0 actual_dptr0 built0
1128
1129(** val virtual_dptr : init_mutable -> Z.z **)
1130let rec virtual_dptr xxx =
1131  xxx.virtual_dptr
1132
1133(** val actual_dptr : init_mutable -> Z.z **)
1134let rec actual_dptr xxx =
1135  xxx.actual_dptr
1136
1137(** val built : init_mutable -> ASM.labelled_instruction List.list **)
1138let rec built xxx =
1139  xxx.built
1140
1141(** val init_mutable_inv_rect_Type4 :
1142    init_mutable -> (Z.z -> Z.z -> ASM.labelled_instruction List.list -> __
1143    -> 'a1) -> 'a1 **)
1144let init_mutable_inv_rect_Type4 hterm h1 =
1145  let hcut = init_mutable_rect_Type4 h1 hterm in hcut __
1146
1147(** val init_mutable_inv_rect_Type3 :
1148    init_mutable -> (Z.z -> Z.z -> ASM.labelled_instruction List.list -> __
1149    -> 'a1) -> 'a1 **)
1150let init_mutable_inv_rect_Type3 hterm h1 =
1151  let hcut = init_mutable_rect_Type3 h1 hterm in hcut __
1152
1153(** val init_mutable_inv_rect_Type2 :
1154    init_mutable -> (Z.z -> Z.z -> ASM.labelled_instruction List.list -> __
1155    -> 'a1) -> 'a1 **)
1156let init_mutable_inv_rect_Type2 hterm h1 =
1157  let hcut = init_mutable_rect_Type2 h1 hterm in hcut __
1158
1159(** val init_mutable_inv_rect_Type1 :
1160    init_mutable -> (Z.z -> Z.z -> ASM.labelled_instruction List.list -> __
1161    -> 'a1) -> 'a1 **)
1162let init_mutable_inv_rect_Type1 hterm h1 =
1163  let hcut = init_mutable_rect_Type1 h1 hterm in hcut __
1164
1165(** val init_mutable_inv_rect_Type0 :
1166    init_mutable -> (Z.z -> Z.z -> ASM.labelled_instruction List.list -> __
1167    -> 'a1) -> 'a1 **)
1168let init_mutable_inv_rect_Type0 hterm h1 =
1169  let hcut = init_mutable_rect_Type0 h1 hterm in hcut __
1170
1171(** val init_mutable_discr : init_mutable -> init_mutable -> __ **)
1172let init_mutable_discr x y =
1173  Logic.eq_rect_Type2 x
1174    (let { virtual_dptr = a0; actual_dptr = a1; built = a2 } = x in
1175    Obj.magic (fun _ dH -> dH __ __ __)) y
1176
1177(** val init_mutable_jmdiscr : init_mutable -> init_mutable -> __ **)
1178let init_mutable_jmdiscr x y =
1179  Logic.eq_rect_Type2 x
1180    (let { virtual_dptr = a0; actual_dptr = a1; built = a2 } = x in
1181    Obj.magic (fun _ dH -> dH __ __ __)) y
1182
1183(** val store_byte : BitVector.byte -> init_mutable -> init_mutable **)
1184let store_byte by mut =
1185  let { virtual_dptr = virt; actual_dptr = act; built = acc } = mut in
1186  let off = Z.zminus virt act in
1187  let pre =
1188    match Z.eqZb off Z.OZ with
1189    | Bool.True -> List.Nil
1190    | Bool.False ->
1191      (match Z.eqZb off (Z.z_of_nat (Nat.S Nat.O)) with
1192       | Bool.True ->
1193         List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Instruction
1194           (ASM.INC ASM.DPTR)) }, List.Nil)
1195       | Bool.False ->
1196         List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Instruction
1197           (ASM.MOV (Types.Inl (Types.Inl (Types.Inr { Types.fst = ASM.DPTR;
1198           Types.snd = (ASM.DATA16
1199           (BitVectorZ.bitvector_of_Z (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1200             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1201             (Nat.S (Nat.S Nat.O)))))))))))))))) virt)) }))))) }, List.Nil))
1202  in
1203  { virtual_dptr = (Z.zsucc virt); actual_dptr = virt; built =
1204  (List.append pre (List.Cons ({ Types.fst = Types.None; Types.snd =
1205    (ASM.Instruction (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inl
1206    (Types.Inl { Types.fst = ASM.ACC_A; Types.snd = (ASM.DATA by) }))))))) },
1207    (List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Instruction
1208    (ASM.MOVX (Types.Inr { Types.fst = ASM.EXT_INDIRECT_DPTR; Types.snd =
1209    ASM.ACC_A }))) }, List.Nil))))) }
1210
1211(** val do_store_init_data :
1212    AST.ident List.list -> aSM_universe -> AST.init_data -> init_mutable ->
1213    init_mutable **)
1214let do_store_init_data globals u = function
1215| AST.Init_int8 n -> store_byte n
1216| AST.Init_int16 n ->
1217  let { Types.fst = by0; Types.snd = by1 } =
1218    Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1219      Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1220      Nat.O)))))))) n
1221  in
1222  Relations.compose (store_byte by1) (store_byte by0)
1223| AST.Init_int32 n ->
1224  let { Types.fst = by0; Types.snd = n0 } =
1225    Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1226      Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1227      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1228      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))))))))))
1229      n
1230  in
1231  let { Types.fst = by1; Types.snd = n1 } =
1232    Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1233      Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1234      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1235      Nat.O)))))))))))))))) n0
1236  in
1237  let { Types.fst = by2; Types.snd = by3 } =
1238    Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1239      Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1240      Nat.O)))))))) n1
1241  in
1242  Relations.compose
1243    (Relations.compose (Relations.compose (store_byte by3) (store_byte by2))
1244      (store_byte by1)) (store_byte by0)
1245| AST.Init_space n ->
1246  (fun mut -> { virtual_dptr = (Z.zplus (Z.z_of_nat n) mut.virtual_dptr);
1247    actual_dptr = mut.actual_dptr; built = mut.built })
1248| AST.Init_null ->
1249  let z =
1250    BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1251      Nat.O))))))))
1252  in
1253  Relations.compose (store_byte z) (store_byte z)
1254| AST.Init_addrof (symb, ofs) ->
1255  let addr =
1256    match Identifiers.lookup PreIdentifiers.SymbolTag u.address_map symb with
1257    | Types.None ->
1258      BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1259        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1260        Nat.O))))))))))))))))
1261    | Types.Some x ->
1262      BitVectorZ.bitvector_of_Z (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1263        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1264        Nat.O))))))))))))))))
1265        (Z.zplus
1266          (BitVectorZ.z_of_unsigned_bitvector (Nat.S (Nat.S (Nat.S (Nat.S
1267            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1268            (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) x) (Z.z_of_nat ofs))
1269  in
1270  let { Types.fst = by1; Types.snd = by0 } =
1271    Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1272      Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1273      Nat.O)))))))) addr
1274  in
1275  Relations.compose (store_byte by1) (store_byte by0)
1276
1277(** val do_store_init_data_list :
1278    AST.ident List.list -> aSM_universe -> Z.z -> AST.init_data List.list ->
1279    ASM.labelled_instruction List.list **)
1280let do_store_init_data_list globals u start_dptr data =
1281  let init = { virtual_dptr = start_dptr; actual_dptr = Z.OZ; built =
1282    List.Nil }
1283  in
1284  (List.foldr (do_store_init_data globals u) init data).built
1285
1286(** val translate_premain :
1287    LIN.lin_program -> ASM.identifier -> ASM.labelled_instruction List.list
1288    Monad.smax_def__o__monad **)
1289let translate_premain p exit_label =
1290  Monad.m_bind0 (Monad.smax_def State.state_monad)
1291    (identifier_of_ident (AST.prog_var_names p.Joint.joint_prog)
1292      (AST.prog_main p.Joint.joint_prog)) (fun main ->
1293    Monad.m_bind0 (Monad.smax_def State.state_monad) State.state_get
1294      (fun u ->
1295      let start_sp =
1296        Z.zopp
1297          (Z.z_of_nat
1298            (Joint.globals_stacksize (Joint.lin_params_to_params LIN.lIN) p))
1299      in
1300      let { Types.fst = sph; Types.snd = spl } =
1301        Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1302          Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1303          (Nat.S Nat.O))))))))
1304          (BitVectorZ.bitvector_of_Z
1305            (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1306              Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1307              (Nat.S Nat.O))))))))) start_sp)
1308      in
1309      let data =
1310        List.flatten
1311          (List.map (fun x -> x.Types.snd)
1312            (AST.prog_vars p.Joint.joint_prog))
1313      in
1314      let init_isp = ASM.DATA
1315        (Vector.append (Nat.S (Nat.S Nat.O))
1316          (Nat.plus (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S
1317            Nat.O))))) (BitVector.zero (Nat.S (Nat.S Nat.O)))
1318          (Vector.append (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S
1319            Nat.O)))) (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons
1320            (Nat.O, Bool.False, Vector.VEmpty))))
1321            (BitVector.maximum (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))
1322      in
1323      let isp_direct = ASM.DIRECT
1324        (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1325          Nat.O))))))) (Nat.S Nat.O) (Vector.VCons ((Nat.S (Nat.S (Nat.S
1326          (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True,
1327          (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1328            Nat.O))))))))) (Vector.VCons (Nat.O, Bool.True, Vector.VEmpty)))
1329      in
1330      let reg_spl = ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1331        Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons
1332        (Nat.O, Bool.False, Vector.VEmpty))))))
1333      in
1334      let reg_sph = ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1335        Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons
1336        (Nat.O, Bool.True, Vector.VEmpty))))))
1337      in
1338      Monad.m_return0 (Monad.smax_def State.state_monad)
1339        (List.append (List.Cons ({ Types.fst = Types.None; Types.snd =
1340          (ASM.Cost p.Joint.init_cost_label) }, (List.Cons ({ Types.fst =
1341          Types.None; Types.snd = (ASM.Instruction (ASM.MOV (Types.Inl
1342          (Types.Inl (Types.Inl (Types.Inr { Types.fst = isp_direct;
1343          Types.snd = init_isp })))))) }, (List.Cons ({ Types.fst =
1344          Types.None; Types.snd = (ASM.Instruction (ASM.MOV (Types.Inl
1345          (Types.Inl (Types.Inl (Types.Inl (Types.Inr { Types.fst = reg_spl;
1346          Types.snd = (ASM.DATA spl) }))))))) }, (List.Cons ({ Types.fst =
1347          Types.None; Types.snd = (ASM.Instruction (ASM.MOV (Types.Inl
1348          (Types.Inl (Types.Inl (Types.Inl (Types.Inr { Types.fst = reg_sph;
1349          Types.snd = (ASM.DATA sph) }))))))) }, List.Nil))))))))
1350          (List.append
1351            (do_store_init_data_list (AST.prog_var_names p.Joint.joint_prog)
1352              u start_sp data) (List.Cons ({ Types.fst = Types.None;
1353            Types.snd = (ASM.Call main) }, (List.Cons ({ Types.fst =
1354            (Types.Some exit_label); Types.snd = (ASM.Cost
1355            u.fresh_cost_label) }, (List.Cons ({ Types.fst = Types.None;
1356            Types.snd = (ASM.Jmp exit_label) }, List.Nil))))))))))
1357
1358(** val get_symboltable :
1359    AST.ident List.list -> (ASM.identifier, AST.ident) Types.prod List.list
1360    Monad.smax_def__o__monad **)
1361let get_symboltable globals =
1362  Obj.magic (fun u ->
1363    let imap = u.ident_map in
1364    let f = fun iold inew x -> List.Cons ({ Types.fst = inew; Types.snd =
1365      iold }, x)
1366    in
1367    { Types.fst = u; Types.snd =
1368    (Identifiers.foldi PreIdentifiers.SymbolTag f imap List.Nil) })
1369
1370(** val lin_to_asm :
1371    LIN.lin_program -> ASM.pseudo_assembly_program Types.option **)
1372let lin_to_asm p =
1373  State.state_run (new_ASM_universe p)
1374    (let add_translation = fun acc id_def ->
1375       Monad.m_bind0 (Monad.smax_def State.state_monad)
1376         (translate_fun_def
1377           (List.map (fun x -> x.Types.fst.Types.fst)
1378             (AST.prog_vars p.Joint.joint_prog)) id_def) (fun code ->
1379         Monad.m_bind0 (Monad.smax_def State.state_monad) acc (fun acc0 ->
1380           Monad.m_return0 (Monad.smax_def State.state_monad)
1381             (List.append code acc0)))
1382     in
1383    Monad.m_bind0 (Monad.smax_def State.state_monad)
1384      (aSM_fresh
1385        (List.map (fun x -> x.Types.fst.Types.fst)
1386          (AST.prog_vars p.Joint.joint_prog))) (fun exit_label ->
1387      Monad.m_bind0 (Monad.smax_def State.state_monad)
1388        (Util.foldl add_translation
1389          (Monad.m_return0 (Monad.smax_def State.state_monad) List.Nil)
1390          (AST.prog_funct p.Joint.joint_prog)) (fun code ->
1391        Monad.m_bind0 (Monad.smax_def State.state_monad)
1392          (get_symboltable (AST.prog_var_names p.Joint.joint_prog))
1393          (fun symboltable ->
1394          Monad.m_bind0 (Monad.smax_def State.state_monad)
1395            (translate_premain p exit_label) (fun init ->
1396            Monad.m_return0 (Monad.smax_def State.state_monad)
1397              (let code0 = List.append init code in
1398              Monad.m_bind0 (Monad.max_def Option.option)
1399                (Obj.magic (ASM.code_size_opt code0)) (fun _ ->
1400                Monad.m_return0 (Monad.max_def Option.option)
1401                  { ASM.preamble = List.Nil; ASM.code = code0;
1402                  ASM.renamed_symbols = symboltable; ASM.final_label =
1403                  exit_label })))))))
1404
Note: See TracBrowser for help on using the repository browser.