source: extracted/lINToASM.ml @ 2979

Last change on this file since 2979 was 2979, checked in by sacerdot, 8 years ago
  1. LINToASM: new extraction (fix deletion backtracked)
  2. translateUtils: hand-made patch waiting for the new extraction
File size: 59.2 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_3 =
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_3
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_5 =
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_5
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_7 =
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_7
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_9 =
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_9
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_11 =
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_11
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_13 =
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_13
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 = eta6; Types.snd = data } = x_size in
323    let { Types.fst = x; Types.snd = region } = eta6 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      p.Joint.joint_prog.AST.prog_vars
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 = eta7; 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 } = eta7 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 = eta8; 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 } = eta8 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
1072(** val store_bytes :
1073    BitVector.byte List.list -> ASM.labelled_instruction List.list **)
1074let store_bytes bytes =
1075  List.fold List.append List.Nil (fun by -> Bool.True) (fun by -> List.Cons
1076    ({ Types.fst = Types.None; Types.snd = (ASM.Instruction (ASM.MOV
1077    (Types.Inl (Types.Inl (Types.Inl (Types.Inl (Types.Inl { Types.fst =
1078    ASM.ACC_A; Types.snd = (ASM.DATA by) }))))))) }, (List.Cons
1079    ({ Types.fst = Types.None; Types.snd = (ASM.Instruction (ASM.MOVX
1080    (Types.Inr { Types.fst = ASM.EXT_INDIRECT_DPTR; Types.snd =
1081    ASM.ACC_A }))) }, (List.Cons ({ Types.fst = Types.None; Types.snd =
1082    (ASM.Instruction (ASM.INC ASM.DPTR)) }, List.Nil)))))) bytes
1083
1084(** val do_store_init_data :
1085    AST.ident List.list -> aSM_universe -> Z.z -> AST.init_data ->
1086    ASM.labelled_instruction List.list **)
1087let do_store_init_data globals u nxt_dptr = function
1088| AST.Init_int8 n -> store_bytes (List.Cons (n, List.Nil))
1089| AST.Init_int16 n ->
1090  let { Types.fst = by0; Types.snd = by1 } =
1091    Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1092      Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1093      Nat.O)))))))) n
1094  in
1095  store_bytes (List.Cons (by0, (List.Cons (by1, List.Nil))))
1096| AST.Init_int32 n ->
1097  let { Types.fst = by0; Types.snd = n0 } =
1098    Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1099      Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1100      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1101      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))))))))))
1102      n
1103  in
1104  let { Types.fst = by1; Types.snd = n1 } =
1105    Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1106      Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1107      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1108      Nat.O)))))))))))))))) n0
1109  in
1110  let { Types.fst = by2; Types.snd = by3 } =
1111    Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1112      Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1113      Nat.O)))))))) n1
1114  in
1115  store_bytes (List.Cons (by0, (List.Cons (by1, (List.Cons (by2, (List.Cons
1116    (by3, List.Nil))))))))
1117| AST.Init_space n ->
1118  (match n with
1119   | Nat.O -> List.Nil
1120   | Nat.S k ->
1121     (match k with
1122      | Nat.O ->
1123        List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Instruction
1124          (ASM.INC ASM.DPTR)) }, List.Nil)
1125      | Nat.S x ->
1126        List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Instruction
1127          (ASM.MOV (Types.Inl (Types.Inl (Types.Inr { Types.fst = ASM.DPTR;
1128          Types.snd = (ASM.DATA16
1129          (BitVectorZ.bitvector_of_Z (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1130            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1131            (Nat.S (Nat.S Nat.O)))))))))))))))) nxt_dptr)) }))))) },
1132          List.Nil)))
1133| AST.Init_null ->
1134  store_bytes (List.Cons
1135    ((BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1136       Nat.O))))))))), (List.Cons
1137    ((BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1138       Nat.O))))))))), List.Nil))))
1139| AST.Init_addrof (symb, ofs) ->
1140  let addr =
1141    match Identifiers.lookup PreIdentifiers.SymbolTag u.address_map symb with
1142    | Types.None ->
1143      BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1144        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1145        Nat.O))))))))))))))))
1146    | Types.Some x ->
1147      BitVectorZ.bitvector_of_Z (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1148        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1149        Nat.O))))))))))))))))
1150        (Z.zplus
1151          (BitVectorZ.z_of_unsigned_bitvector (Nat.S (Nat.S (Nat.S (Nat.S
1152            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1153            (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) x) (Z.z_of_nat ofs))
1154  in
1155  let { Types.fst = by1; Types.snd = by0 } =
1156    Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1157      Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1158      Nat.O)))))))) addr
1159  in
1160  store_bytes (List.Cons (by0, (List.Cons (by1, List.Nil))))
1161
1162(** val do_store_init_data_list :
1163    AST.ident List.list -> aSM_universe -> Z.z -> AST.init_data List.list ->
1164    ASM.labelled_instruction List.list **)
1165let do_store_init_data_list globals u start_dptr data =
1166  let f = fun data0 dptr_acc ->
1167    let { Types.fst = dptr; Types.snd = acc } = dptr_acc in
1168    let nxt_dptr =
1169      Z.zplus dptr (Z.z_of_nat (Globalenvs.size_init_data data0))
1170    in
1171    { Types.fst = nxt_dptr; Types.snd =
1172    (List.append (do_store_init_data globals u nxt_dptr data0) acc) }
1173  in
1174  List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Instruction (ASM.MOV
1175  (Types.Inl (Types.Inl (Types.Inr { Types.fst = ASM.DPTR; Types.snd =
1176  (ASM.DATA16
1177  (BitVectorZ.bitvector_of_Z (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1178    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1179    Nat.O)))))))))))))))) start_dptr)) }))))) },
1180  (List.foldr f { Types.fst = start_dptr; Types.snd = List.Nil } data).Types.snd)
1181
1182(** val translate_initialization :
1183    LIN.lin_program -> ASM.labelled_instruction List.list
1184    Monad.smax_def__o__monad **)
1185let translate_initialization p =
1186  Obj.magic (fun u ->
1187    let start_sp =
1188      Z.zopp
1189        (Z.z_of_nat
1190          (Joint.globals_stacksize (Joint.lin_params_to_params LIN.lIN) p))
1191    in
1192    let { Types.fst = sph; Types.snd = spl } =
1193      Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1194        Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1195        Nat.O))))))))
1196        (BitVectorZ.bitvector_of_Z
1197          (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1198            Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1199            (Nat.S Nat.O))))))))) start_sp)
1200    in
1201    let data =
1202      List.flatten
1203        (List.map (fun x -> x.Types.snd) p.Joint.joint_prog.AST.prog_vars)
1204    in
1205    let init_isp = ASM.DATA
1206      (Vector.append (Nat.S (Nat.S Nat.O))
1207        (Nat.plus (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S
1208          Nat.O))))) (BitVector.zero (Nat.S (Nat.S Nat.O)))
1209        (Vector.append (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S
1210          Nat.O)))) (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons
1211          (Nat.O, Bool.False, Vector.VEmpty))))
1212          (BitVector.maximum (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))
1213    in
1214    let isp_direct = ASM.DIRECT
1215      (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1216        Nat.O))))))) (Nat.S Nat.O) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1217        (Nat.S (Nat.S Nat.O)))))), Bool.True,
1218        (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1219          Nat.O))))))))) (Vector.VCons (Nat.O, Bool.True, Vector.VEmpty)))
1220    in
1221    let reg_spl = ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1222      Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons
1223      (Nat.O, Bool.False, Vector.VEmpty))))))
1224    in
1225    let reg_sph = ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1226      Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons
1227      (Nat.O, Bool.True, Vector.VEmpty))))))
1228    in
1229    { Types.fst = u; Types.snd =
1230    (List.append (List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Cost
1231      p.Joint.init_cost_label) }, (List.Cons ({ Types.fst = Types.None;
1232      Types.snd = (ASM.Instruction (ASM.MOV (Types.Inl (Types.Inl (Types.Inl
1233      (Types.Inr { Types.fst = isp_direct; Types.snd = init_isp })))))) },
1234      (List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Instruction
1235      (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inl (Types.Inr
1236      { Types.fst = reg_spl; Types.snd = (ASM.DATA spl) }))))))) },
1237      (List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Instruction
1238      (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inl (Types.Inr
1239      { Types.fst = reg_sph; Types.snd = (ASM.DATA sph) }))))))) },
1240      List.Nil))))))))
1241      (do_store_init_data_list (AST.prog_var_names p.Joint.joint_prog) u
1242        start_sp data)) })
1243
1244(** val get_symboltable :
1245    AST.ident List.list -> (ASM.identifier, AST.ident) Types.prod List.list
1246    Monad.smax_def__o__monad **)
1247let get_symboltable globals =
1248  Obj.magic (fun u ->
1249    let imap = u.ident_map in
1250    let f = fun iold inew x -> List.Cons ({ Types.fst = inew; Types.snd =
1251      iold }, x)
1252    in
1253    { Types.fst = u; Types.snd =
1254    (Identifiers.foldi PreIdentifiers.SymbolTag f imap List.Nil) })
1255
1256(** val lin_to_asm :
1257    LIN.lin_program -> ASM.pseudo_assembly_program Types.option **)
1258let lin_to_asm p =
1259  State.state_run (new_ASM_universe p)
1260    (let add_translation = fun acc id_def ->
1261       Monad.m_bind0 (Monad.smax_def State.state_monad)
1262         (translate_fun_def
1263           (List.map (fun x -> x.Types.fst.Types.fst)
1264             p.Joint.joint_prog.AST.prog_vars) id_def) (fun code ->
1265         Monad.m_bind0 (Monad.smax_def State.state_monad) acc (fun acc0 ->
1266           Monad.m_return0 (Monad.smax_def State.state_monad)
1267             (List.append code acc0)))
1268     in
1269    Monad.m_bind0 (Monad.smax_def State.state_monad)
1270      (Util.foldl add_translation
1271        (Monad.m_return0 (Monad.smax_def State.state_monad) List.Nil)
1272        p.Joint.joint_prog.AST.prog_funct) (fun code ->
1273      Monad.m_bind0 (Monad.smax_def State.state_monad)
1274        (aSM_fresh (AST.prog_var_names p.Joint.joint_prog))
1275        (fun exit_label ->
1276        Monad.m_bind0 (Monad.smax_def State.state_monad)
1277          (identifier_of_ident (AST.prog_var_names p.Joint.joint_prog)
1278            p.Joint.joint_prog.AST.prog_main) (fun main ->
1279          Monad.m_bind0 (Monad.smax_def State.state_monad)
1280            (get_symboltable (AST.prog_var_names p.Joint.joint_prog))
1281            (fun symboltable ->
1282            Monad.m_bind0 (Monad.smax_def State.state_monad)
1283              (translate_initialization p) (fun init ->
1284              Monad.m_bind0 (Monad.smax_def State.state_monad)
1285                State.state_get (fun u ->
1286                Monad.m_return0 (Monad.smax_def State.state_monad)
1287                  (let code0 =
1288                     List.append init (List.Cons ({ Types.fst = Types.None;
1289                       Types.snd = (ASM.Call main) }, (List.Cons
1290                       ({ Types.fst = (Types.Some exit_label); Types.snd =
1291                       (ASM.Cost u.fresh_cost_label) }, (List.Cons
1292                       ({ Types.fst = Types.None; Types.snd = (ASM.Jmp
1293                       exit_label) }, code))))))
1294                   in
1295                  Monad.m_bind0 (Monad.max_def Option.option)
1296                    (Obj.magic (ASM.code_size_opt code0)) (fun _ ->
1297                    Monad.m_return0 (Monad.max_def Option.option)
1298                      { ASM.preamble = List.Nil; ASM.code = code0;
1299                      ASM.renamed_symbols = symboltable; ASM.final_label =
1300                      exit_label })))))))))
1301
Note: See TracBrowser for help on using the repository browser.