source: extracted/eRTLptrToLTL.ml @ 2775

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

The compiler now computes also the stack cost model.

File size: 36.3 KB
RevLine 
[2717]1open Preamble
2
3open String
4
5open Sets
6
7open Listb
8
9open LabelledObjects
10
[2773]11open BitVectorTrie
12
[2717]13open Graphs
14
15open I8051
16
17open Order
18
19open Registers
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 Lists
40
41open Identifiers
42
43open Integers
44
45open AST
46
47open Division
48
49open Exp
50
51open Arithmetic
52
[2773]53open Setoids
54
55open Monad
56
57open Option
58
[2717]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
[2730]123open Deqsets_extra
[2717]124
125open State
126
127open Bind_new
128
129open BindLists
130
131open Blocks
132
133open TranslateUtils
134
[2743]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
[2717]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
[2775]169| Arg_decision_colour x_21731 -> h_arg_decision_colour x_21731
170| Arg_decision_spill x_21732 -> h_arg_decision_spill x_21732
171| Arg_decision_imm x_21733 -> h_arg_decision_imm x_21733
[2717]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
[2775]177| Arg_decision_colour x_21738 -> h_arg_decision_colour x_21738
178| Arg_decision_spill x_21739 -> h_arg_decision_spill x_21739
179| Arg_decision_imm x_21740 -> h_arg_decision_imm x_21740
[2717]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
[2775]185| Arg_decision_colour x_21745 -> h_arg_decision_colour x_21745
186| Arg_decision_spill x_21746 -> h_arg_decision_spill x_21746
187| Arg_decision_imm x_21747 -> h_arg_decision_imm x_21747
[2717]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
[2775]193| Arg_decision_colour x_21752 -> h_arg_decision_colour x_21752
194| Arg_decision_spill x_21753 -> h_arg_decision_spill x_21753
195| Arg_decision_imm x_21754 -> h_arg_decision_imm x_21754
[2717]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
[2775]201| Arg_decision_colour x_21759 -> h_arg_decision_colour x_21759
202| Arg_decision_spill x_21760 -> h_arg_decision_spill x_21760
203| Arg_decision_imm x_21761 -> h_arg_decision_imm x_21761
[2717]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
[2775]209| Arg_decision_colour x_21766 -> h_arg_decision_colour x_21766
210| Arg_decision_spill x_21767 -> h_arg_decision_spill x_21767
211| Arg_decision_imm x_21768 -> h_arg_decision_imm x_21768
[2717]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
[2743]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
[2717]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
[2743]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
[2717]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 **)
[2773]381let set_stack_int globals off int =
[2717]382  List.append (set_dp_by_offset globals off) (List.Cons ((Joint.MOVE
[2773]383    (Obj.magic (Joint_LTL_LIN.Int_to_acc (a, int)))), (List.Cons
[2717]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)))
[2773]404     | Arg_decision_imm int ->
[2717]405       preserve_carry_bit globals carry_lives_after
[2773]406         (set_stack_int globals dsto int))
[2717]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)
[2773]431     | Arg_decision_imm int ->
[2717]432       List.append (List.Cons ((Joint.MOVE
[2773]433         (Obj.magic (Joint_LTL_LIN.Int_to_acc (a, int)))), List.Nil))
[2717]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 **)
[2773]514let translate_op2 globals carry_lives_after op dst arg1 arg2 =
[2717]515  List.append
516    (preserve_carry_bit globals
[2773]517      (Bool.andb (uses_carry op)
[2717]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)))
[2773]524    (List.append (List.Cons ((Joint.OP2 (op, (Obj.magic a), (Obj.magic a),
[2717]525      (Obj.magic (Joint.hdw_argument_from_reg I8051.RegisterB)))), List.Nil))
[2773]526      (move globals (Bool.andb (sets_carry op) carry_lives_after) dst
[2717]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 **)
[2773]533let translate_op2_smart globals carry_lives_after op dst arg1 arg2 =
[2717]534  preserve_carry_bit globals
[2773]535    (Bool.andb (Bool.andb (Bool.notb (sets_carry op)) carry_lives_after)
[2717]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
[2773]541         (move globals (uses_carry op) (Interference.Decision_colour
[2717]542           I8051.RegisterA) arg1)
[2773]543         (List.append (List.Cons ((Joint.OP2 (op, (Obj.magic a),
[2717]544           (Obj.magic a), (Obj.magic (Joint.hdw_argument_from_reg arg2r)))),
545           List.Nil))
[2773]546           (move globals (Bool.andb (sets_carry op) carry_lives_after) dst
[2717]547             (Arg_decision_colour I8051.RegisterA)))
548     | Arg_decision_spill x ->
[2773]549       (match commutative op with
[2717]550        | Bool.True ->
551          (match arg1 with
552           | Arg_decision_colour arg1r ->
553             List.append
[2773]554               (move globals (uses_carry op) (Interference.Decision_colour
[2717]555                 I8051.RegisterA) arg2)
[2773]556               (List.append (List.Cons ((Joint.OP2 (op, (Obj.magic a),
[2717]557                 (Obj.magic a),
558                 (Obj.magic (Joint.hdw_argument_from_reg arg1r)))),
559                 List.Nil))
[2773]560                 (move globals (Bool.andb (sets_carry op) carry_lives_after)
[2717]561                   dst (Arg_decision_colour I8051.RegisterA)))
562           | Arg_decision_spill x0 ->
[2773]563             translate_op2 globals carry_lives_after op dst arg1 arg2
[2717]564           | Arg_decision_imm arg1i ->
565             List.append
[2773]566               (move globals (uses_carry op) (Interference.Decision_colour
[2717]567                 I8051.RegisterA) arg2)
[2773]568               (List.append (List.Cons ((Joint.OP2 (op, (Obj.magic a),
[2717]569                 (Obj.magic a),
570                 (Obj.magic (Joint.hdw_argument_from_byte arg1i)))),
571                 List.Nil))
[2773]572                 (move globals (Bool.andb (sets_carry op) carry_lives_after)
[2717]573                   dst (Arg_decision_colour I8051.RegisterA))))
574        | Bool.False ->
[2773]575          translate_op2 globals carry_lives_after op dst arg1 arg2)
[2717]576     | Arg_decision_imm arg2i ->
577       List.append
[2773]578         (move globals (uses_carry op) (Interference.Decision_colour
[2717]579           I8051.RegisterA) arg1)
[2773]580         (List.append (List.Cons ((Joint.OP2 (op, (Obj.magic a),
[2717]581           (Obj.magic a), (Obj.magic (Joint.hdw_argument_from_byte arg2i)))),
582           List.Nil))
[2773]583           (move globals (Bool.andb (sets_carry op) carry_lives_after) dst
[2717]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
[2743]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
[2717]645(** val translate_op1 :
646    AST.ident List.list -> Bool.bool -> BackEndOps.op1 ->
647    Interference.decision -> Interference.decision -> Joint.joint_seq
648    List.list **)
[2773]649let translate_op1 globals carry_lives_after op dst arg =
[2717]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)
[2773]656        (dec_to_arg_dec arg)) (List.Cons ((Joint.OP1 (op,
[2717]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 **)
[2773]664let translate_opaccs globals carry_lives_after op dst1 dst2 arg1 arg2 =
[2717]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)
[2773]670        arg1) (List.Cons ((Joint.OPACCS (op, (Obj.magic Types.It),
[2717]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
[2773]794    (let lookup = fun r -> grph.Interference.colouring (Types.Inl r) in
[2717]795    let lookup_arg = fun a0 ->
796      match a0 with
[2773]797      | Joint.Reg r -> dec_to_arg_dec (lookup r)
[2717]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)
[2773]826             (dec_to_arg_dec (Obj.magic lookup r)))); Types.snd = (fun x ->
[2717]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
[2773]836            | ERTL.PSD r -> lookup r
[2717]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)),
[2773]850            (move0 (Obj.magic lookup r) (Arg_decision_colour
[2717]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
[2773]863              (Obj.magic lbl0) (Obj.magic lookup dpl) (Obj.magic lookup dph))
864        | Joint.OPACCS (op, dst1, dst2, arg1, arg2) ->
[2717]865          Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
866            globals
[2773]867            (translate_opaccs globals carry_lives_after op
868              (Obj.magic lookup dst1) (Obj.magic lookup dst2)
[2717]869              (Obj.magic lookup_arg arg1) (Obj.magic lookup_arg arg2))
[2773]870        | Joint.OP1 (op, dst, arg) ->
[2717]871          Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
872            globals
[2773]873            (translate_op1 globals carry_lives_after op
874              (Obj.magic lookup dst) (Obj.magic lookup arg))
875        | Joint.OP2 (op, dst, arg1, arg2) ->
[2717]876          Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
877            globals
[2773]878            (translate_op2_smart globals carry_lives_after op
879              (Obj.magic lookup dst) (Obj.magic lookup_arg arg1)
[2717]880              (Obj.magic lookup_arg arg2))
881        | Joint.CLEAR_CARRY ->
882          Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
883            globals (List.Cons (Joint.CLEAR_CARRY, List.Nil))
884        | Joint.SET_CARRY ->
885          Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
886            globals (List.Cons (Joint.CLEAR_CARRY, List.Nil))
887        | Joint.LOAD (dstr, addr1, addr2) ->
888          Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
889            globals
[2773]890            (translate_load globals carry_lives_after (Obj.magic lookup dstr)
891              (Obj.magic lookup_arg addr1) (Obj.magic lookup_arg addr2))
[2717]892        | Joint.STORE (addr1, addr2, srcr) ->
893          Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
894            globals
895            (translate_store globals carry_lives_after
896              (Obj.magic lookup_arg addr1) (Obj.magic lookup_arg addr2)
897              (Obj.magic lookup_arg srcr))
898        | Joint.Extension_seq ext ->
899          Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
900            globals
901            (match Obj.magic ext with
902             | ERTLptr.Ertlptr_ertl ext' ->
903               (match ext' with
904                | ERTL.Ertl_new_frame -> newframe globals stack_sz
905                | ERTL.Ertl_del_frame -> delframe globals stack_sz
906                | ERTL.Ertl_frame_size r ->
[2773]907                  move0 (lookup r) (Arg_decision_imm
[2717]908                    (Joint.byte_of_nat stack_sz)))
[2773]909             | ERTLptr.LOW_ADDRESS (r1, l) ->
910               translate_low_address globals carry_lives_after (lookup r1) l
911             | ERTLptr.HIGH_ADDRESS (r1, l) ->
912               translate_high_address globals carry_lives_after (lookup r1) l))))
[2717]913
914(** val translate_fin_step :
915    AST.ident List.list -> Graphs.label -> Joint.joint_fin_step ->
916    Blocks.bind_fin_block **)
917let translate_fin_step globals lbl s =
918  Bind_new.Bret { Types.fst = List.Nil; Types.snd =
919    (match s with
920     | Joint.GOTO l -> Joint.GOTO l
921     | Joint.RETURN -> Joint.RETURN
922     | Joint.TAILCALL (x, x0) -> assert false (* absurd case *)) }
923
924(** val translate_data :
925    Fixpoints.fixpoint_computer -> Interference.coloured_graph_computer ->
926    AST.ident List.list -> Joint.joint_closed_internal_function ->
927    (Registers.register, TranslateUtils.b_graph_translate_data)
928    Bind_new.bind_new **)
929let translate_data the_fixpoint build globals int_fun =
930  let after =
931    Liveness.analyse_liveness the_fixpoint globals (Types.pi1 int_fun)
932  in
[2773]933  let coloured_graph = build globals (Types.pi1 int_fun) after in
[2717]934  let stack_sz =
[2773]935    Nat.plus coloured_graph.Interference.spilled_no
[2717]936      (Types.pi1 int_fun).Joint.joint_if_stacksize
937  in
938  Bind_new.Bret { TranslateUtils.init_ret = (Obj.magic Types.It);
939  TranslateUtils.init_params = (Obj.magic Types.It);
940  TranslateUtils.init_stack_size = stack_sz; TranslateUtils.added_prologue =
941  List.Nil; TranslateUtils.f_step =
[2773]942  (translate_step globals after coloured_graph stack_sz);
[2717]943  TranslateUtils.f_fin = (translate_fin_step globals) }
944
[2775]945(** val first_free_stack_addr : LTL.ltl_program -> Nat.nat **)
946let first_free_stack_addr p =
947  let globals_addr_internal = fun offset x_size ->
948    let { Types.fst = eta4401; Types.snd = size } = x_size in
949    let { Types.fst = x; Types.snd = region } = eta4401 in
950    Nat.plus offset size
951  in
952  Util.foldl globals_addr_internal Nat.O p.AST.prog_vars
953
[2717]954(** val ertlptr_to_ltl :
955    Fixpoints.fixpoint_computer -> Interference.coloured_graph_computer ->
[2775]956    ERTLptr.ertlptr_program -> ((LTL.ltl_program, Joint.stack_cost_model)
957    Types.prod, Nat.nat) Types.prod **)
958let ertlptr_to_ltl the_fixpoint build pr =
959  let ltlprog =
960    TranslateUtils.b_graph_transform_program ERTLptr.eRTLptr LTL.lTL
961      (translate_data the_fixpoint build) pr
962  in
963  { Types.fst = { Types.fst = ltlprog; Types.snd =
964  (Joint.stack_cost (Joint.graph_params_to_params LTL.lTL) ltlprog) };
965  Types.snd =
966  (Nat.minus
967    (Exp.exp (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
968      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
969      Nat.O))))))))))))))))) (first_free_stack_addr ltlprog)) }
[2717]970
Note: See TracBrowser for help on using the repository browser.