source: extracted/eRTLptrToLTL.ml @ 2746

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

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

File size: 35.6 KB
Line 
1open Preamble
2
3open String
4
5open Sets
6
7open Listb
8
9open LabelledObjects
10
11open Graphs
12
13open I8051
14
15open Order
16
17open Registers
18
19open BitVectorTrie
20
21open CostLabel
22
23open Hide
24
25open Proper
26
27open PositiveMap
28
29open Deqsets
30
31open ErrorMessages
32
33open PreIdentifiers
34
35open Errors
36
37open Extralib
38
39open Setoids
40
41open Monad
42
43open Option
44
45open Lists
46
47open Identifiers
48
49open Integers
50
51open AST
52
53open Division
54
55open Exp
56
57open Arithmetic
58
59open Extranat
60
61open Vector
62
63open Div_and_mod
64
65open Jmeq
66
67open Russell
68
69open List
70
71open Util
72
73open FoldStuff
74
75open BitVector
76
77open Types
78
79open Bool
80
81open Relations
82
83open Nat
84
85open Hints_declaration
86
87open Core_notation
88
89open Pts
90
91open Logic
92
93open Positive
94
95open Z
96
97open BitVectorZ
98
99open Pointers
100
101open ByteValues
102
103open BackEndOps
104
105open Joint
106
107open Joint_LTL_LIN
108
109open LTL
110
111open Fixpoints
112
113open Set_adt
114
115open ERTL
116
117open ERTLptr
118
119open Liveness
120
121open Interference
122
123open Deqsets_extra
124
125open State
126
127open Bind_new
128
129open BindLists
130
131open Blocks
132
133open TranslateUtils
134
135(** val dpi1__o__Reg_to_dec__o__inject :
136    (I8051.register, 'a1) Types.dPair -> Interference.decision Types.sig0 **)
137let dpi1__o__Reg_to_dec__o__inject x2 =
138  Interference.Decision_colour x2.Types.dpi1
139
140(** val eject__o__Reg_to_dec__o__inject :
141    I8051.register Types.sig0 -> Interference.decision Types.sig0 **)
142let eject__o__Reg_to_dec__o__inject x2 =
143  Interference.Decision_colour (Types.pi1 x2)
144
145(** val reg_to_dec__o__inject :
146    I8051.register -> Interference.decision Types.sig0 **)
147let reg_to_dec__o__inject x1 =
148  Interference.Decision_colour x1
149
150(** val dpi1__o__Reg_to_dec :
151    (I8051.register, 'a1) Types.dPair -> Interference.decision **)
152let dpi1__o__Reg_to_dec x1 =
153  Interference.Decision_colour x1.Types.dpi1
154
155(** val eject__o__Reg_to_dec :
156    I8051.register Types.sig0 -> Interference.decision **)
157let eject__o__Reg_to_dec x1 =
158  Interference.Decision_colour (Types.pi1 x1)
159
160type arg_decision =
161| Arg_decision_colour of I8051.register
162| Arg_decision_spill of Nat.nat
163| Arg_decision_imm of BitVector.byte
164
165(** val arg_decision_rect_Type4 :
166    (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
167    arg_decision -> 'a1 **)
168let rec arg_decision_rect_Type4 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
169| Arg_decision_colour x_21681 -> h_arg_decision_colour x_21681
170| Arg_decision_spill x_21682 -> h_arg_decision_spill x_21682
171| Arg_decision_imm x_21683 -> h_arg_decision_imm x_21683
172
173(** val arg_decision_rect_Type5 :
174    (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
175    arg_decision -> 'a1 **)
176let rec arg_decision_rect_Type5 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
177| Arg_decision_colour x_21688 -> h_arg_decision_colour x_21688
178| Arg_decision_spill x_21689 -> h_arg_decision_spill x_21689
179| Arg_decision_imm x_21690 -> h_arg_decision_imm x_21690
180
181(** val arg_decision_rect_Type3 :
182    (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
183    arg_decision -> 'a1 **)
184let rec arg_decision_rect_Type3 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
185| Arg_decision_colour x_21695 -> h_arg_decision_colour x_21695
186| Arg_decision_spill x_21696 -> h_arg_decision_spill x_21696
187| Arg_decision_imm x_21697 -> h_arg_decision_imm x_21697
188
189(** val arg_decision_rect_Type2 :
190    (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
191    arg_decision -> 'a1 **)
192let rec arg_decision_rect_Type2 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
193| Arg_decision_colour x_21702 -> h_arg_decision_colour x_21702
194| Arg_decision_spill x_21703 -> h_arg_decision_spill x_21703
195| Arg_decision_imm x_21704 -> h_arg_decision_imm x_21704
196
197(** val arg_decision_rect_Type1 :
198    (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
199    arg_decision -> 'a1 **)
200let rec arg_decision_rect_Type1 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
201| Arg_decision_colour x_21709 -> h_arg_decision_colour x_21709
202| Arg_decision_spill x_21710 -> h_arg_decision_spill x_21710
203| Arg_decision_imm x_21711 -> h_arg_decision_imm x_21711
204
205(** val arg_decision_rect_Type0 :
206    (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
207    arg_decision -> 'a1 **)
208let rec arg_decision_rect_Type0 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
209| Arg_decision_colour x_21716 -> h_arg_decision_colour x_21716
210| Arg_decision_spill x_21717 -> h_arg_decision_spill x_21717
211| Arg_decision_imm x_21718 -> h_arg_decision_imm x_21718
212
213(** val arg_decision_inv_rect_Type4 :
214    arg_decision -> (I8051.register -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1)
215    -> (BitVector.byte -> __ -> 'a1) -> 'a1 **)
216let arg_decision_inv_rect_Type4 hterm h1 h2 h3 =
217  let hcut = arg_decision_rect_Type4 h1 h2 h3 hterm in hcut __
218
219(** val arg_decision_inv_rect_Type3 :
220    arg_decision -> (I8051.register -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1)
221    -> (BitVector.byte -> __ -> 'a1) -> 'a1 **)
222let arg_decision_inv_rect_Type3 hterm h1 h2 h3 =
223  let hcut = arg_decision_rect_Type3 h1 h2 h3 hterm in hcut __
224
225(** val arg_decision_inv_rect_Type2 :
226    arg_decision -> (I8051.register -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1)
227    -> (BitVector.byte -> __ -> 'a1) -> 'a1 **)
228let arg_decision_inv_rect_Type2 hterm h1 h2 h3 =
229  let hcut = arg_decision_rect_Type2 h1 h2 h3 hterm in hcut __
230
231(** val arg_decision_inv_rect_Type1 :
232    arg_decision -> (I8051.register -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1)
233    -> (BitVector.byte -> __ -> 'a1) -> 'a1 **)
234let arg_decision_inv_rect_Type1 hterm h1 h2 h3 =
235  let hcut = arg_decision_rect_Type1 h1 h2 h3 hterm in hcut __
236
237(** val arg_decision_inv_rect_Type0 :
238    arg_decision -> (I8051.register -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1)
239    -> (BitVector.byte -> __ -> 'a1) -> 'a1 **)
240let arg_decision_inv_rect_Type0 hterm h1 h2 h3 =
241  let hcut = arg_decision_rect_Type0 h1 h2 h3 hterm in hcut __
242
243(** val arg_decision_discr : arg_decision -> arg_decision -> __ **)
244let arg_decision_discr x y =
245  Logic.eq_rect_Type2 x
246    (match x with
247     | Arg_decision_colour a0 -> Obj.magic (fun _ dH -> dH __)
248     | Arg_decision_spill a0 -> Obj.magic (fun _ dH -> dH __)
249     | Arg_decision_imm a0 -> Obj.magic (fun _ dH -> dH __)) y
250
251(** val arg_decision_jmdiscr : arg_decision -> arg_decision -> __ **)
252let arg_decision_jmdiscr x y =
253  Logic.eq_rect_Type2 x
254    (match x with
255     | Arg_decision_colour a0 -> Obj.magic (fun _ dH -> dH __)
256     | Arg_decision_spill a0 -> Obj.magic (fun _ dH -> dH __)
257     | Arg_decision_imm a0 -> Obj.magic (fun _ dH -> dH __)) y
258
259(** val dpi1__o__Reg_to_arg_dec__o__inject :
260    (I8051.register, 'a1) Types.dPair -> arg_decision Types.sig0 **)
261let dpi1__o__Reg_to_arg_dec__o__inject x2 =
262  Arg_decision_colour x2.Types.dpi1
263
264(** val eject__o__Reg_to_arg_dec__o__inject :
265    I8051.register Types.sig0 -> arg_decision Types.sig0 **)
266let eject__o__Reg_to_arg_dec__o__inject x2 =
267  Arg_decision_colour (Types.pi1 x2)
268
269(** val reg_to_arg_dec__o__inject :
270    I8051.register -> arg_decision Types.sig0 **)
271let reg_to_arg_dec__o__inject x1 =
272  Arg_decision_colour x1
273
274(** val dpi1__o__Reg_to_arg_dec :
275    (I8051.register, 'a1) Types.dPair -> arg_decision **)
276let dpi1__o__Reg_to_arg_dec x1 =
277  Arg_decision_colour x1.Types.dpi1
278
279(** val eject__o__Reg_to_arg_dec :
280    I8051.register Types.sig0 -> arg_decision **)
281let eject__o__Reg_to_arg_dec x1 =
282  Arg_decision_colour (Types.pi1 x1)
283
284(** val preserve_carry_bit :
285    AST.ident List.list -> Bool.bool -> Joint.joint_seq List.list ->
286    Joint.joint_seq List.list **)
287let preserve_carry_bit globals do_it steps =
288  match do_it with
289  | Bool.True ->
290    List.Cons ((Joint.Extension_seq (Obj.magic Joint_LTL_LIN.SAVE_CARRY)),
291      (List.append steps (List.Cons ((Joint.Extension_seq
292        (Obj.magic Joint_LTL_LIN.RESTORE_CARRY)), List.Nil))))
293  | Bool.False -> steps
294
295(** val a : Types.unit0 **)
296let a =
297  Types.It
298
299(** val dpi1__o__beval_of_byte__o__inject :
300    (BitVector.byte, 'a1) Types.dPair -> ByteValues.beval Types.sig0 **)
301let dpi1__o__beval_of_byte__o__inject x2 =
302  ByteValues.BVByte x2.Types.dpi1
303
304(** val eject__o__beval_of_byte__o__inject :
305    BitVector.byte Types.sig0 -> ByteValues.beval Types.sig0 **)
306let eject__o__beval_of_byte__o__inject x2 =
307  ByteValues.BVByte (Types.pi1 x2)
308
309(** val beval_of_byte__o__inject :
310    BitVector.byte -> ByteValues.beval Types.sig0 **)
311let beval_of_byte__o__inject x1 =
312  ByteValues.BVByte x1
313
314(** val dpi1__o__beval_of_byte :
315    (BitVector.byte, 'a1) Types.dPair -> ByteValues.beval **)
316let dpi1__o__beval_of_byte x1 =
317  ByteValues.BVByte x1.Types.dpi1
318
319(** val eject__o__beval_of_byte :
320    BitVector.byte Types.sig0 -> ByteValues.beval **)
321let eject__o__beval_of_byte x1 =
322  ByteValues.BVByte (Types.pi1 x1)
323
324(** val set_dp_by_offset :
325    AST.ident List.list -> Nat.nat -> Joint.joint_seq List.list **)
326let set_dp_by_offset globals off =
327  List.Cons ((Joint.MOVE
328    (Obj.magic (Joint_LTL_LIN.Int_to_acc (a, (Joint.byte_of_nat off))))),
329    (List.Cons ((Joint.OP2 (BackEndOps.Add, (Obj.magic a), (Obj.magic a),
330    (Obj.magic (Joint.hdw_argument_from_reg I8051.registerSPL)))), (List.Cons
331    ((Joint.MOVE
332    (Obj.magic (Joint_LTL_LIN.From_acc (I8051.RegisterDPL, a)))), (List.Cons
333    ((Joint.MOVE
334    (Obj.magic (Joint_LTL_LIN.Int_to_acc (a, Joint.zero_byte)))), (List.Cons
335    ((Joint.OP2 (BackEndOps.Addc, (Obj.magic a), (Obj.magic a),
336    (Obj.magic (Joint.hdw_argument_from_reg I8051.registerSPH)))), (List.Cons
337    ((Joint.MOVE
338    (Obj.magic (Joint_LTL_LIN.From_acc (I8051.RegisterDPH, a)))),
339    List.Nil)))))))))))
340
341(** val get_stack :
342    AST.ident List.list -> I8051.register -> Nat.nat -> Joint.joint_seq
343    List.list **)
344let get_stack globals r off =
345  List.append (set_dp_by_offset globals off)
346    (List.append (List.Cons ((Joint.LOAD ((Obj.magic a),
347      (Obj.magic Types.It), (Obj.magic Types.It))), List.Nil))
348      (match I8051.eq_Register r I8051.RegisterA with
349       | Bool.True -> List.Nil
350       | Bool.False ->
351         List.Cons ((Joint.MOVE (Obj.magic (Joint_LTL_LIN.From_acc (r, a)))),
352           List.Nil)))
353
354(** val set_stack_not_a :
355    AST.ident List.list -> Nat.nat -> I8051.register -> Joint.joint_seq
356    List.list **)
357let set_stack_not_a globals off r =
358  List.append (set_dp_by_offset globals off) (List.Cons ((Joint.MOVE
359    (Obj.magic (Joint_LTL_LIN.To_acc (a, r)))), (List.Cons ((Joint.STORE
360    ((Obj.magic Types.It), (Obj.magic Types.It), (Obj.magic a))),
361    List.Nil))))
362
363(** val set_stack_a :
364    AST.ident List.list -> Nat.nat -> Joint.joint_seq List.list **)
365let set_stack_a globals off =
366  List.append (List.Cons ((Joint.MOVE
367    (Obj.magic (Joint_LTL_LIN.From_acc (I8051.registerST1, a)))), List.Nil))
368    (set_stack_not_a globals off I8051.registerST1)
369
370(** val set_stack :
371    AST.ident List.list -> Nat.nat -> I8051.register -> Joint.joint_seq
372    List.list **)
373let set_stack globals off r =
374  match I8051.eq_Register r I8051.RegisterA with
375  | Bool.True -> set_stack_a globals off
376  | Bool.False -> set_stack_not_a globals off r
377
378(** val set_stack_int :
379    AST.ident List.list -> Nat.nat -> BitVector.byte -> Joint.joint_seq
380    List.list **)
381let set_stack_int globals off int0 =
382  List.append (set_dp_by_offset globals off) (List.Cons ((Joint.MOVE
383    (Obj.magic (Joint_LTL_LIN.Int_to_acc (a, int0)))), (List.Cons
384    ((Joint.STORE ((Obj.magic Types.It), (Obj.magic Types.It),
385    (Obj.magic a))), List.Nil))))
386
387(** val move :
388    AST.ident List.list -> Bool.bool -> Interference.decision -> arg_decision
389    -> Joint.joint_seq List.list **)
390let move globals carry_lives_after dst src =
391  match dst with
392  | Interference.Decision_spill dsto ->
393    (match src with
394     | Arg_decision_colour srcr ->
395       preserve_carry_bit globals carry_lives_after
396         (set_stack globals dsto srcr)
397     | Arg_decision_spill srco ->
398       (match Nat.eqb srco dsto with
399        | Bool.True -> List.Nil
400        | Bool.False ->
401          preserve_carry_bit globals carry_lives_after
402            (List.append (get_stack globals I8051.RegisterA srco)
403              (set_stack globals dsto I8051.RegisterA)))
404     | Arg_decision_imm int0 ->
405       preserve_carry_bit globals carry_lives_after
406         (set_stack_int globals dsto int0))
407  | Interference.Decision_colour dstr ->
408    (match src with
409     | Arg_decision_colour srcr ->
410       (match I8051.eq_Register dstr srcr with
411        | Bool.True -> List.Nil
412        | Bool.False ->
413          (match I8051.eq_Register dstr I8051.RegisterA with
414           | Bool.True ->
415             List.Cons ((Joint.MOVE
416               (Obj.magic (Joint_LTL_LIN.To_acc (a, srcr)))), List.Nil)
417           | Bool.False ->
418             (match I8051.eq_Register srcr I8051.RegisterA with
419              | Bool.True ->
420                List.Cons ((Joint.MOVE
421                  (Obj.magic (Joint_LTL_LIN.From_acc (dstr, a)))), List.Nil)
422              | Bool.False ->
423                List.Cons ((Joint.MOVE
424                  (Obj.magic (Joint_LTL_LIN.To_acc (a, srcr)))), (List.Cons
425                  ((Joint.MOVE
426                  (Obj.magic (Joint_LTL_LIN.From_acc (dstr, a)))),
427                  List.Nil))))))
428     | Arg_decision_spill srco ->
429       preserve_carry_bit globals carry_lives_after
430         (get_stack globals dstr srco)
431     | Arg_decision_imm int0 ->
432       List.append (List.Cons ((Joint.MOVE
433         (Obj.magic (Joint_LTL_LIN.Int_to_acc (a, int0)))), List.Nil))
434         (match I8051.eq_Register dstr I8051.RegisterA with
435          | Bool.True -> List.Nil
436          | Bool.False ->
437            List.Cons ((Joint.MOVE
438              (Obj.magic (Joint_LTL_LIN.From_acc (dstr, a)))), List.Nil)))
439
440(** val arg_is_spilled : arg_decision -> Bool.bool **)
441let arg_is_spilled = function
442| Arg_decision_colour x0 -> Bool.False
443| Arg_decision_spill x0 -> Bool.True
444| Arg_decision_imm x0 -> Bool.False
445
446(** val is_spilled : Interference.decision -> Bool.bool **)
447let is_spilled = function
448| Interference.Decision_spill x0 -> Bool.True
449| Interference.Decision_colour x0 -> Bool.False
450
451(** val newframe :
452    AST.ident List.list -> Nat.nat -> Joint.joint_seq List.list **)
453let newframe globals stack_sz =
454  List.Cons (Joint.CLEAR_CARRY, (List.Cons ((Joint.MOVE
455    (Obj.magic (Joint_LTL_LIN.To_acc (a, I8051.registerSPL)))), (List.Cons
456    ((Joint.OP2 (BackEndOps.Sub, (Obj.magic a), (Obj.magic a),
457    (Obj.magic (Joint.hdw_argument_from_byte (Joint.byte_of_nat stack_sz))))),
458    (List.Cons ((Joint.MOVE
459    (Obj.magic (Joint_LTL_LIN.From_acc (I8051.registerSPL, a)))), (List.Cons
460    ((Joint.MOVE (Obj.magic (Joint_LTL_LIN.To_acc (a, I8051.registerSPH)))),
461    (List.Cons ((Joint.OP2 (BackEndOps.Sub, (Obj.magic a), (Obj.magic a),
462    (Obj.magic (Joint.hdw_argument_from_byte Joint.zero_byte)))), (List.Cons
463    ((Joint.MOVE
464    (Obj.magic (Joint_LTL_LIN.From_acc (I8051.registerSPH, a)))),
465    List.Nil)))))))))))))
466
467(** val delframe :
468    AST.ident List.list -> Nat.nat -> Joint.joint_seq List.list **)
469let delframe globals stack_sz =
470  List.Cons ((Joint.MOVE
471    (Obj.magic (Joint_LTL_LIN.To_acc (a, I8051.registerSPL)))), (List.Cons
472    ((Joint.OP2 (BackEndOps.Add, (Obj.magic a), (Obj.magic a),
473    (Obj.magic (Joint.hdw_argument_from_byte (Joint.byte_of_nat stack_sz))))),
474    (List.Cons ((Joint.MOVE
475    (Obj.magic (Joint_LTL_LIN.From_acc (I8051.registerSPL, a)))), (List.Cons
476    ((Joint.MOVE (Obj.magic (Joint_LTL_LIN.To_acc (a, I8051.registerSPH)))),
477    (List.Cons ((Joint.OP2 (BackEndOps.Addc, (Obj.magic a), (Obj.magic a),
478    (Obj.magic (Joint.hdw_argument_from_byte Joint.zero_byte)))), (List.Cons
479    ((Joint.MOVE
480    (Obj.magic (Joint_LTL_LIN.From_acc (I8051.registerSPH, a)))),
481    List.Nil)))))))))))
482
483(** val commutative : BackEndOps.op2 -> Bool.bool **)
484let commutative = function
485| BackEndOps.Add -> Bool.True
486| BackEndOps.Addc -> Bool.True
487| BackEndOps.Sub -> Bool.False
488| BackEndOps.And -> Bool.True
489| BackEndOps.Or -> Bool.True
490| BackEndOps.Xor -> Bool.True
491
492(** val uses_carry : BackEndOps.op2 -> Bool.bool **)
493let uses_carry = function
494| BackEndOps.Add -> Bool.False
495| BackEndOps.Addc -> Bool.True
496| BackEndOps.Sub -> Bool.True
497| BackEndOps.And -> Bool.False
498| BackEndOps.Or -> Bool.False
499| BackEndOps.Xor -> Bool.False
500
501(** val sets_carry : BackEndOps.op2 -> Bool.bool **)
502let sets_carry = function
503| BackEndOps.Add -> Bool.True
504| BackEndOps.Addc -> Bool.True
505| BackEndOps.Sub -> Bool.True
506| BackEndOps.And -> Bool.False
507| BackEndOps.Or -> Bool.False
508| BackEndOps.Xor -> Bool.False
509
510(** val translate_op2 :
511    AST.ident List.list -> Bool.bool -> BackEndOps.op2 ->
512    Interference.decision -> arg_decision -> arg_decision -> Joint.joint_seq
513    List.list **)
514let translate_op2 globals carry_lives_after op4 dst arg1 arg2 =
515  List.append
516    (preserve_carry_bit globals
517      (Bool.andb (uses_carry op4)
518        (Bool.orb (arg_is_spilled arg1) (arg_is_spilled arg2)))
519      (List.append
520        (move globals Bool.False (Interference.Decision_colour
521          I8051.RegisterB) arg2)
522        (move globals Bool.False (Interference.Decision_colour
523          I8051.RegisterA) arg1)))
524    (List.append (List.Cons ((Joint.OP2 (op4, (Obj.magic a), (Obj.magic a),
525      (Obj.magic (Joint.hdw_argument_from_reg I8051.RegisterB)))), List.Nil))
526      (move globals (Bool.andb (sets_carry op4) carry_lives_after) dst
527        (Arg_decision_colour I8051.RegisterA)))
528
529(** val translate_op2_smart :
530    AST.ident List.list -> Bool.bool -> BackEndOps.op2 ->
531    Interference.decision -> arg_decision -> arg_decision -> Joint.joint_seq
532    List.list **)
533let translate_op2_smart globals carry_lives_after op4 dst arg1 arg2 =
534  preserve_carry_bit globals
535    (Bool.andb (Bool.andb (Bool.notb (sets_carry op4)) carry_lives_after)
536      (Bool.orb (Bool.orb (arg_is_spilled arg1) (arg_is_spilled arg2))
537        (is_spilled dst)))
538    (match arg2 with
539     | Arg_decision_colour arg2r ->
540       List.append
541         (move globals (uses_carry op4) (Interference.Decision_colour
542           I8051.RegisterA) arg1)
543         (List.append (List.Cons ((Joint.OP2 (op4, (Obj.magic a),
544           (Obj.magic a), (Obj.magic (Joint.hdw_argument_from_reg arg2r)))),
545           List.Nil))
546           (move globals (Bool.andb (sets_carry op4) carry_lives_after) dst
547             (Arg_decision_colour I8051.RegisterA)))
548     | Arg_decision_spill x ->
549       (match commutative op4 with
550        | Bool.True ->
551          (match arg1 with
552           | Arg_decision_colour arg1r ->
553             List.append
554               (move globals (uses_carry op4) (Interference.Decision_colour
555                 I8051.RegisterA) arg2)
556               (List.append (List.Cons ((Joint.OP2 (op4, (Obj.magic a),
557                 (Obj.magic a),
558                 (Obj.magic (Joint.hdw_argument_from_reg arg1r)))),
559                 List.Nil))
560                 (move globals (Bool.andb (sets_carry op4) carry_lives_after)
561                   dst (Arg_decision_colour I8051.RegisterA)))
562           | Arg_decision_spill x0 ->
563             translate_op2 globals carry_lives_after op4 dst arg1 arg2
564           | Arg_decision_imm arg1i ->
565             List.append
566               (move globals (uses_carry op4) (Interference.Decision_colour
567                 I8051.RegisterA) arg2)
568               (List.append (List.Cons ((Joint.OP2 (op4, (Obj.magic a),
569                 (Obj.magic a),
570                 (Obj.magic (Joint.hdw_argument_from_byte arg1i)))),
571                 List.Nil))
572                 (move globals (Bool.andb (sets_carry op4) carry_lives_after)
573                   dst (Arg_decision_colour I8051.RegisterA))))
574        | Bool.False ->
575          translate_op2 globals carry_lives_after op4 dst arg1 arg2)
576     | Arg_decision_imm arg2i ->
577       List.append
578         (move globals (uses_carry op4) (Interference.Decision_colour
579           I8051.RegisterA) arg1)
580         (List.append (List.Cons ((Joint.OP2 (op4, (Obj.magic a),
581           (Obj.magic a), (Obj.magic (Joint.hdw_argument_from_byte arg2i)))),
582           List.Nil))
583           (move globals (Bool.andb (sets_carry op4) carry_lives_after) dst
584             (Arg_decision_colour I8051.RegisterA))))
585
586(** val dec_to_arg_dec : Interference.decision -> arg_decision **)
587let dec_to_arg_dec = function
588| Interference.Decision_spill n -> Arg_decision_spill n
589| Interference.Decision_colour r -> Arg_decision_colour r
590
591(** val reg_to_dec__o__dec_arg_dec__o__inject :
592    I8051.register -> arg_decision Types.sig0 **)
593let reg_to_dec__o__dec_arg_dec__o__inject x0 =
594  dec_to_arg_dec (Interference.Decision_colour x0)
595
596(** val dpi1__o__Reg_to_dec__o__dec_arg_dec__o__inject :
597    (I8051.register, 'a1) Types.dPair -> arg_decision Types.sig0 **)
598let dpi1__o__Reg_to_dec__o__dec_arg_dec__o__inject x2 =
599  dec_to_arg_dec (dpi1__o__Reg_to_dec x2)
600
601(** val eject__o__Reg_to_dec__o__dec_arg_dec__o__inject :
602    I8051.register Types.sig0 -> arg_decision Types.sig0 **)
603let eject__o__Reg_to_dec__o__dec_arg_dec__o__inject x2 =
604  dec_to_arg_dec (eject__o__Reg_to_dec x2)
605
606(** val dpi1__o__dec_arg_dec__o__inject :
607    (Interference.decision, 'a1) Types.dPair -> arg_decision Types.sig0 **)
608let dpi1__o__dec_arg_dec__o__inject x2 =
609  dec_to_arg_dec x2.Types.dpi1
610
611(** val eject__o__dec_arg_dec__o__inject :
612    Interference.decision Types.sig0 -> arg_decision Types.sig0 **)
613let eject__o__dec_arg_dec__o__inject x2 =
614  dec_to_arg_dec (Types.pi1 x2)
615
616(** val dec_arg_dec__o__inject :
617    Interference.decision -> arg_decision Types.sig0 **)
618let dec_arg_dec__o__inject x1 =
619  dec_to_arg_dec x1
620
621(** val reg_to_dec__o__dec_arg_dec : I8051.register -> arg_decision **)
622let reg_to_dec__o__dec_arg_dec x0 =
623  dec_to_arg_dec (Interference.Decision_colour x0)
624
625(** val dpi1__o__Reg_to_dec__o__dec_arg_dec :
626    (I8051.register, 'a1) Types.dPair -> arg_decision **)
627let dpi1__o__Reg_to_dec__o__dec_arg_dec x1 =
628  dec_to_arg_dec (dpi1__o__Reg_to_dec x1)
629
630(** val eject__o__Reg_to_dec__o__dec_arg_dec :
631    I8051.register Types.sig0 -> arg_decision **)
632let eject__o__Reg_to_dec__o__dec_arg_dec x1 =
633  dec_to_arg_dec (eject__o__Reg_to_dec x1)
634
635(** val dpi1__o__dec_arg_dec :
636    (Interference.decision, 'a1) Types.dPair -> arg_decision **)
637let dpi1__o__dec_arg_dec x1 =
638  dec_to_arg_dec x1.Types.dpi1
639
640(** val eject__o__dec_arg_dec :
641    Interference.decision Types.sig0 -> arg_decision **)
642let eject__o__dec_arg_dec x1 =
643  dec_to_arg_dec (Types.pi1 x1)
644
645(** val translate_op1 :
646    AST.ident List.list -> Bool.bool -> BackEndOps.op1 ->
647    Interference.decision -> Interference.decision -> Joint.joint_seq
648    List.list **)
649let translate_op1 globals carry_lives_after op4 dst arg =
650  let preserve_carry =
651    Bool.andb carry_lives_after (Bool.orb (is_spilled dst) (is_spilled arg))
652  in
653  preserve_carry_bit globals preserve_carry
654    (List.append
655      (move globals Bool.False (Interference.Decision_colour I8051.RegisterA)
656        (dec_to_arg_dec arg)) (List.Cons ((Joint.OP1 (op4,
657      (Obj.magic Types.It), (Obj.magic Types.It))),
658      (move globals Bool.False dst (Arg_decision_colour I8051.RegisterA)))))
659
660(** val translate_opaccs :
661    AST.ident List.list -> Bool.bool -> BackEndOps.opAccs ->
662    Interference.decision -> Interference.decision -> arg_decision ->
663    arg_decision -> Joint.joint_seq List.list **)
664let translate_opaccs globals carry_lives_after op4 dst1 dst2 arg1 arg2 =
665  List.append
666    (move globals Bool.False (Interference.Decision_colour I8051.RegisterB)
667      arg2)
668    (List.append
669      (move globals Bool.False (Interference.Decision_colour I8051.RegisterA)
670        arg1) (List.Cons ((Joint.OPACCS (op4, (Obj.magic Types.It),
671      (Obj.magic Types.It), (Obj.magic Types.It), (Obj.magic Types.It))),
672      (List.append
673        (move globals Bool.False dst1 (Arg_decision_colour I8051.RegisterA))
674        (List.append
675          (move globals Bool.False dst2 (Arg_decision_colour
676            I8051.RegisterB))
677          (match Bool.andb carry_lives_after
678                   (Bool.orb (is_spilled dst1) (is_spilled dst2)) with
679           | Bool.True -> List.Cons (Joint.CLEAR_CARRY, List.Nil)
680           | Bool.False -> List.Nil))))))
681
682(** val move_to_dp :
683    AST.ident List.list -> arg_decision -> arg_decision -> Joint.joint_seq
684    List.list **)
685let move_to_dp globals arg1 arg2 =
686  match Bool.notb (arg_is_spilled arg1) with
687  | Bool.True ->
688    List.append
689      (move globals Bool.False (Interference.Decision_colour
690        I8051.RegisterDPH) arg2)
691      (move globals Bool.False (Interference.Decision_colour
692        I8051.RegisterDPL) arg1)
693  | Bool.False ->
694    (match Bool.notb (arg_is_spilled arg2) with
695     | Bool.True ->
696       List.append
697         (move globals Bool.False (Interference.Decision_colour
698           I8051.RegisterDPL) arg1)
699         (move globals Bool.False (Interference.Decision_colour
700           I8051.RegisterDPH) arg2)
701     | Bool.False ->
702       List.append
703         (move globals Bool.False (Interference.Decision_colour
704           I8051.RegisterB) arg1)
705         (List.append
706           (move globals Bool.False (Interference.Decision_colour
707             I8051.RegisterDPH) arg2)
708           (move globals Bool.False (Interference.Decision_colour
709             I8051.RegisterDPL) (Arg_decision_colour I8051.RegisterB))))
710
711(** val translate_store :
712    AST.ident List.list -> Bool.bool -> arg_decision -> arg_decision ->
713    arg_decision -> Joint.joint_seq List.list **)
714let translate_store globals carry_lives_after addr1 addr2 src =
715  preserve_carry_bit globals
716    (Bool.andb carry_lives_after
717      (Bool.orb (Bool.orb (arg_is_spilled addr1) (arg_is_spilled addr1))
718        (arg_is_spilled src)))
719    (let move_to_dptr = move_to_dp globals addr1 addr2 in
720    List.append
721      (match arg_is_spilled src with
722       | Bool.True ->
723         List.append
724           (move globals Bool.False (Interference.Decision_colour
725             I8051.registerST0) src)
726           (List.append move_to_dptr (List.Cons ((Joint.MOVE
727             (Obj.magic (Joint_LTL_LIN.To_acc (a, I8051.registerST0)))),
728             List.Nil)))
729       | Bool.False -> move_to_dptr) (List.Cons ((Joint.STORE
730      ((Obj.magic Types.It), (Obj.magic Types.It), (Obj.magic a))),
731      List.Nil)))
732
733(** val translate_load :
734    AST.ident List.list -> Bool.bool -> Interference.decision -> arg_decision
735    -> arg_decision -> Joint.joint_seq List.list **)
736let translate_load globals carry_lives_after dst addr1 addr2 =
737  preserve_carry_bit globals
738    (Bool.andb carry_lives_after
739      (Bool.orb (Bool.orb (is_spilled dst) (arg_is_spilled addr1))
740        (arg_is_spilled addr1)))
741    (List.append (move_to_dp globals addr1 addr2)
742      (List.append (List.Cons ((Joint.LOAD ((Obj.magic a),
743        (Obj.magic Types.It), (Obj.magic Types.It))), List.Nil))
744        (move globals Bool.False dst (Arg_decision_colour I8051.RegisterA))))
745
746(** val translate_address :
747    __ List.list -> Bool.bool -> __ -> Interference.decision ->
748    Interference.decision -> Joint.joint_seq List.list **)
749let translate_address globals carry_lives_after id addr1 addr2 =
750  preserve_carry_bit (Obj.magic globals)
751    (Bool.andb carry_lives_after
752      (Bool.orb (is_spilled addr1) (is_spilled addr2))) (List.Cons
753    ((Joint.ADDRESS ((Obj.magic id), (Obj.magic Types.It),
754    (Obj.magic Types.It))),
755    (List.append
756      (move (Obj.magic globals) Bool.False addr1 (Arg_decision_colour
757        I8051.RegisterDPL))
758      (move (Obj.magic globals) Bool.False addr2 (Arg_decision_colour
759        I8051.RegisterDPH)))))
760
761(** val translate_low_address :
762    AST.ident List.list -> Bool.bool -> Interference.decision -> Graphs.label
763    -> Joint.joint_seq List.list **)
764let translate_low_address globals carry_lives_after dst lbl =
765  match dst with
766  | Interference.Decision_spill x ->
767    List.Cons ((Joint.Extension_seq
768      (Obj.magic (Joint_LTL_LIN.LOW_ADDRESS (I8051.RegisterA, lbl)))),
769      (move globals carry_lives_after dst (Arg_decision_colour
770        I8051.RegisterA)))
771  | Interference.Decision_colour r ->
772    List.Cons ((Joint.Extension_seq
773      (Obj.magic (Joint_LTL_LIN.LOW_ADDRESS (r, lbl)))), List.Nil)
774
775(** val translate_high_address :
776    AST.ident List.list -> Bool.bool -> Interference.decision -> Graphs.label
777    -> Joint.joint_seq List.list **)
778let translate_high_address globals carry_lives_after dst lbl =
779  match dst with
780  | Interference.Decision_spill x ->
781    List.Cons ((Joint.Extension_seq
782      (Obj.magic (Joint_LTL_LIN.HIGH_ADDRESS (I8051.RegisterA, lbl)))),
783      (move globals carry_lives_after dst (Arg_decision_colour
784        I8051.RegisterA)))
785  | Interference.Decision_colour r ->
786    List.Cons ((Joint.Extension_seq
787      (Obj.magic (Joint_LTL_LIN.HIGH_ADDRESS (r, lbl)))), List.Nil)
788
789(** val translate_step :
790    AST.ident List.list -> Fixpoints.valuation -> Interference.coloured_graph
791    -> Nat.nat -> Graphs.label -> Joint.joint_step -> Blocks.bind_step_block **)
792let translate_step globals after grph stack_sz lbl s =
793  Bind_new.Bret
794    (let lookup1 = fun r -> grph.Interference.colouring (Types.Inl r) in
795    let lookup_arg = fun a0 ->
796      match a0 with
797      | Joint.Reg r -> dec_to_arg_dec (lookup1 r)
798      | Joint.Imm b -> Arg_decision_imm b
799    in
800    let carry_lives_after = Liveness.hlives I8051.RegisterCarry (after lbl)
801    in
802    let move0 = move globals carry_lives_after in
803    (match s with
804     | Joint.COST_LABEL cost_lbl ->
805       { Types.fst = { Types.fst = List.Nil; Types.snd = (fun x ->
806         Joint.COST_LABEL cost_lbl) }; Types.snd = List.Nil }
807     | Joint.CALL (f, n_args, x) ->
808       (match f with
809        | Types.Inl f0 ->
810          { Types.fst = { Types.fst = List.Nil; Types.snd = (fun x0 ->
811            Joint.CALL ((Types.Inl f0), n_args, (Obj.magic Types.It))) };
812            Types.snd = List.Nil }
813        | Types.Inr dp ->
814          let { Types.fst = dpl; Types.snd = dph } = dp in
815          { Types.fst = { Types.fst =
816          (Blocks.add_dummy_variance
817            (move_to_dp globals (Obj.magic lookup_arg dpl)
818              (Obj.magic lookup_arg dph))); Types.snd = (fun x0 -> Joint.CALL
819          ((Types.Inr { Types.fst = (Obj.magic Types.It); Types.snd =
820          (Obj.magic Types.It) }), n_args, (Obj.magic Types.It))) };
821          Types.snd = List.Nil })
822     | Joint.COND (r, ltrue) ->
823       { Types.fst = { Types.fst =
824         (Blocks.add_dummy_variance
825           (move0 (Interference.Decision_colour I8051.RegisterA)
826             (dec_to_arg_dec (Obj.magic lookup1 r)))); Types.snd = (fun x ->
827         Joint.COND ((Obj.magic Types.It), ltrue)) }; Types.snd = List.Nil }
828     | Joint.Step_seq s' ->
829       (match s' with
830        | Joint.COMMENT c ->
831          Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
832            globals (List.Cons ((Joint.COMMENT c), List.Nil))
833        | Joint.MOVE pair_regs ->
834          let lookup_move_dst = fun x ->
835            match x with
836            | ERTL.PSD r -> lookup1 r
837            | ERTL.HDW r -> Interference.Decision_colour r
838          in
839          let dst = lookup_move_dst (Obj.magic pair_regs).Types.fst in
840          let src =
841            match (Obj.magic pair_regs).Types.snd with
842            | Joint.Reg r -> dec_to_arg_dec (lookup_move_dst r)
843            | Joint.Imm b -> Arg_decision_imm b
844          in
845          Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
846            globals (move0 dst src)
847        | Joint.POP r ->
848          Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
849            globals (List.Cons ((Joint.POP (Obj.magic a)),
850            (move0 (Obj.magic lookup1 r) (Arg_decision_colour
851              I8051.RegisterA))))
852        | Joint.PUSH a0 ->
853          Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
854            globals
855            (List.append
856              (move0 (Interference.Decision_colour I8051.RegisterA)
857                (Obj.magic lookup_arg a0)) (List.Cons ((Joint.PUSH
858              (Obj.magic a)), List.Nil)))
859        | Joint.ADDRESS (lbl0, dpl, dph) ->
860          Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
861            globals
862            (translate_address (Obj.magic globals) carry_lives_after
863              (Obj.magic lbl0) (Obj.magic lookup1 dpl)
864              (Obj.magic lookup1 dph))
865        | Joint.OPACCS (op4, dst1, dst2, arg1, arg2) ->
866          Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
867            globals
868            (translate_opaccs globals carry_lives_after op4
869              (Obj.magic lookup1 dst1) (Obj.magic lookup1 dst2)
870              (Obj.magic lookup_arg arg1) (Obj.magic lookup_arg arg2))
871        | Joint.OP1 (op4, dst, arg) ->
872          Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
873            globals
874            (translate_op1 globals carry_lives_after op4
875              (Obj.magic lookup1 dst) (Obj.magic lookup1 arg))
876        | Joint.OP2 (op4, dst, arg1, arg2) ->
877          Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
878            globals
879            (translate_op2_smart globals carry_lives_after op4
880              (Obj.magic lookup1 dst) (Obj.magic lookup_arg arg1)
881              (Obj.magic lookup_arg arg2))
882        | Joint.CLEAR_CARRY ->
883          Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
884            globals (List.Cons (Joint.CLEAR_CARRY, List.Nil))
885        | Joint.SET_CARRY ->
886          Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
887            globals (List.Cons (Joint.CLEAR_CARRY, List.Nil))
888        | Joint.LOAD (dstr, addr1, addr2) ->
889          Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
890            globals
891            (translate_load globals carry_lives_after
892              (Obj.magic lookup1 dstr) (Obj.magic lookup_arg addr1)
893              (Obj.magic lookup_arg addr2))
894        | Joint.STORE (addr1, addr2, srcr) ->
895          Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
896            globals
897            (translate_store globals carry_lives_after
898              (Obj.magic lookup_arg addr1) (Obj.magic lookup_arg addr2)
899              (Obj.magic lookup_arg srcr))
900        | Joint.Extension_seq ext ->
901          Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
902            globals
903            (match Obj.magic ext with
904             | ERTLptr.Ertlptr_ertl ext' ->
905               (match ext' with
906                | ERTL.Ertl_new_frame -> newframe globals stack_sz
907                | ERTL.Ertl_del_frame -> delframe globals stack_sz
908                | ERTL.Ertl_frame_size r ->
909                  move0 (lookup1 r) (Arg_decision_imm
910                    (Joint.byte_of_nat stack_sz)))
911             | ERTLptr.LOW_ADDRESS (r5, l) ->
912               translate_low_address globals carry_lives_after (lookup1 r5) l
913             | ERTLptr.HIGH_ADDRESS (r5, l) ->
914               translate_high_address globals carry_lives_after (lookup1 r5)
915                 l))))
916
917(** val translate_fin_step :
918    AST.ident List.list -> Graphs.label -> Joint.joint_fin_step ->
919    Blocks.bind_fin_block **)
920let translate_fin_step globals lbl s =
921  Bind_new.Bret { Types.fst = List.Nil; Types.snd =
922    (match s with
923     | Joint.GOTO l -> Joint.GOTO l
924     | Joint.RETURN -> Joint.RETURN
925     | Joint.TAILCALL (x, x0) -> assert false (* absurd case *)) }
926
927(** val translate_data :
928    Fixpoints.fixpoint_computer -> Interference.coloured_graph_computer ->
929    AST.ident List.list -> Joint.joint_closed_internal_function ->
930    (Registers.register, TranslateUtils.b_graph_translate_data)
931    Bind_new.bind_new **)
932let translate_data the_fixpoint build globals int_fun =
933  let after =
934    Liveness.analyse_liveness the_fixpoint globals (Types.pi1 int_fun)
935  in
936  let coloured_graph0 = build globals (Types.pi1 int_fun) after in
937  let stack_sz =
938    Nat.plus coloured_graph0.Interference.spilled_no
939      (Types.pi1 int_fun).Joint.joint_if_stacksize
940  in
941  Bind_new.Bret { TranslateUtils.init_ret = (Obj.magic Types.It);
942  TranslateUtils.init_params = (Obj.magic Types.It);
943  TranslateUtils.init_stack_size = stack_sz; TranslateUtils.added_prologue =
944  List.Nil; TranslateUtils.f_step =
945  (translate_step globals after coloured_graph0 stack_sz);
946  TranslateUtils.f_fin = (translate_fin_step globals) }
947
948(** val ertlptr_to_ltl :
949    Fixpoints.fixpoint_computer -> Interference.coloured_graph_computer ->
950    ERTLptr.ertlptr_program -> LTL.ltl_program **)
951let ertlptr_to_ltl the_fixpoint build =
952  TranslateUtils.b_graph_transform_program ERTLptr.eRTLptr LTL.lTL
953    (translate_data the_fixpoint build)
954
Note: See TracBrowser for help on using the repository browser.