source: extracted/eRTLptrToLTL.ml @ 2867

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

New extraction after indianess bug fixes by Paolo.

File size: 37.0 KB
Line 
1open Preamble
2
3open String
4
5open Sets
6
7open Listb
8
9open LabelledObjects
10
11open BitVectorTrie
12
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
53open Setoids
54
55open Monad
56
57open Option
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_21937 -> h_arg_decision_colour x_21937
170| Arg_decision_spill x_21938 -> h_arg_decision_spill x_21938
171| Arg_decision_imm x_21939 -> h_arg_decision_imm x_21939
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_21944 -> h_arg_decision_colour x_21944
178| Arg_decision_spill x_21945 -> h_arg_decision_spill x_21945
179| Arg_decision_imm x_21946 -> h_arg_decision_imm x_21946
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_21951 -> h_arg_decision_colour x_21951
186| Arg_decision_spill x_21952 -> h_arg_decision_spill x_21952
187| Arg_decision_imm x_21953 -> h_arg_decision_imm x_21953
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_21958 -> h_arg_decision_colour x_21958
194| Arg_decision_spill x_21959 -> h_arg_decision_spill x_21959
195| Arg_decision_imm x_21960 -> h_arg_decision_imm x_21960
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_21965 -> h_arg_decision_colour x_21965
202| Arg_decision_spill x_21966 -> h_arg_decision_spill x_21966
203| Arg_decision_imm x_21967 -> h_arg_decision_imm x_21967
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_21972 -> h_arg_decision_colour x_21972
210| Arg_decision_spill x_21973 -> h_arg_decision_spill x_21973
211| Arg_decision_imm x_21974 -> h_arg_decision_imm x_21974
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 -> Nat.nat -> I8051.register -> Nat.nat ->
343    Joint.joint_seq List.list **)
344let get_stack globals localss r off =
345  let off0 = Nat.plus localss off in
346  List.append (set_dp_by_offset globals off0)
347    (List.append (List.Cons ((Joint.LOAD ((Obj.magic a),
348      (Obj.magic Types.It), (Obj.magic Types.It))), List.Nil))
349      (match I8051.eq_Register r I8051.RegisterA with
350       | Bool.True -> List.Nil
351       | Bool.False ->
352         List.Cons ((Joint.MOVE (Obj.magic (Joint_LTL_LIN.From_acc (r, a)))),
353           List.Nil)))
354
355(** val set_stack_not_a :
356    AST.ident List.list -> Nat.nat -> Nat.nat -> I8051.register ->
357    Joint.joint_seq List.list **)
358let set_stack_not_a globals localss off r =
359  let off0 = Nat.plus localss off in
360  List.append (set_dp_by_offset globals off0) (List.Cons ((Joint.MOVE
361    (Obj.magic (Joint_LTL_LIN.To_acc (a, r)))), (List.Cons ((Joint.STORE
362    ((Obj.magic Types.It), (Obj.magic Types.It), (Obj.magic a))),
363    List.Nil))))
364
365(** val set_stack_a :
366    AST.ident List.list -> Nat.nat -> Nat.nat -> Joint.joint_seq List.list **)
367let set_stack_a globals localss off =
368  List.append (List.Cons ((Joint.MOVE
369    (Obj.magic (Joint_LTL_LIN.From_acc (I8051.registerST1, a)))), List.Nil))
370    (set_stack_not_a globals localss off I8051.registerST1)
371
372(** val set_stack :
373    AST.ident List.list -> Nat.nat -> Nat.nat -> I8051.register ->
374    Joint.joint_seq List.list **)
375let set_stack globals localss off r =
376  match I8051.eq_Register r I8051.RegisterA with
377  | Bool.True -> set_stack_a globals localss off
378  | Bool.False -> set_stack_not_a globals localss off r
379
380(** val set_stack_int :
381    AST.ident List.list -> Nat.nat -> Nat.nat -> BitVector.byte ->
382    Joint.joint_seq List.list **)
383let set_stack_int globals localss off int =
384  let off0 = Nat.plus localss off in
385  List.append (set_dp_by_offset globals off0) (List.Cons ((Joint.MOVE
386    (Obj.magic (Joint_LTL_LIN.Int_to_acc (a, int)))), (List.Cons
387    ((Joint.STORE ((Obj.magic Types.It), (Obj.magic Types.It),
388    (Obj.magic a))), List.Nil))))
389
390(** val move :
391    AST.ident List.list -> Nat.nat -> Bool.bool -> Interference.decision ->
392    arg_decision -> Joint.joint_seq List.list **)
393let move globals localss carry_lives_after dst src =
394  match dst with
395  | Interference.Decision_spill dsto ->
396    (match src with
397     | Arg_decision_colour srcr ->
398       preserve_carry_bit globals carry_lives_after
399         (set_stack globals localss dsto srcr)
400     | Arg_decision_spill srco ->
401       (match Nat.eqb srco dsto with
402        | Bool.True -> List.Nil
403        | Bool.False ->
404          preserve_carry_bit globals carry_lives_after
405            (List.append (get_stack globals localss I8051.RegisterA srco)
406              (set_stack globals localss dsto I8051.RegisterA)))
407     | Arg_decision_imm int ->
408       preserve_carry_bit globals carry_lives_after
409         (set_stack_int globals localss dsto int))
410  | Interference.Decision_colour dstr ->
411    (match src with
412     | Arg_decision_colour srcr ->
413       (match I8051.eq_Register dstr srcr with
414        | Bool.True -> List.Nil
415        | Bool.False ->
416          (match I8051.eq_Register dstr I8051.RegisterA with
417           | Bool.True ->
418             List.Cons ((Joint.MOVE
419               (Obj.magic (Joint_LTL_LIN.To_acc (a, srcr)))), List.Nil)
420           | Bool.False ->
421             (match I8051.eq_Register srcr I8051.RegisterA with
422              | Bool.True ->
423                List.Cons ((Joint.MOVE
424                  (Obj.magic (Joint_LTL_LIN.From_acc (dstr, a)))), List.Nil)
425              | Bool.False ->
426                List.Cons ((Joint.MOVE
427                  (Obj.magic (Joint_LTL_LIN.To_acc (a, srcr)))), (List.Cons
428                  ((Joint.MOVE
429                  (Obj.magic (Joint_LTL_LIN.From_acc (dstr, a)))),
430                  List.Nil))))))
431     | Arg_decision_spill srco ->
432       preserve_carry_bit globals carry_lives_after
433         (get_stack globals localss dstr srco)
434     | Arg_decision_imm int ->
435       List.append (List.Cons ((Joint.MOVE
436         (Obj.magic (Joint_LTL_LIN.Int_to_acc (a, int)))), List.Nil))
437         (match I8051.eq_Register dstr I8051.RegisterA with
438          | Bool.True -> List.Nil
439          | Bool.False ->
440            List.Cons ((Joint.MOVE
441              (Obj.magic (Joint_LTL_LIN.From_acc (dstr, a)))), List.Nil)))
442
443(** val arg_is_spilled : arg_decision -> Bool.bool **)
444let arg_is_spilled = function
445| Arg_decision_colour x0 -> Bool.False
446| Arg_decision_spill x0 -> Bool.True
447| Arg_decision_imm x0 -> Bool.False
448
449(** val is_spilled : Interference.decision -> Bool.bool **)
450let is_spilled = function
451| Interference.Decision_spill x0 -> Bool.True
452| Interference.Decision_colour x0 -> Bool.False
453
454(** val newframe :
455    AST.ident List.list -> Nat.nat -> Joint.joint_seq List.list **)
456let newframe globals stack_sz =
457  List.Cons (Joint.CLEAR_CARRY, (List.Cons ((Joint.MOVE
458    (Obj.magic (Joint_LTL_LIN.To_acc (a, I8051.registerSPL)))), (List.Cons
459    ((Joint.OP2 (BackEndOps.Sub, (Obj.magic a), (Obj.magic a),
460    (Obj.magic (Joint.hdw_argument_from_byte (Joint.byte_of_nat stack_sz))))),
461    (List.Cons ((Joint.MOVE
462    (Obj.magic (Joint_LTL_LIN.From_acc (I8051.registerSPL, a)))), (List.Cons
463    ((Joint.MOVE (Obj.magic (Joint_LTL_LIN.To_acc (a, I8051.registerSPH)))),
464    (List.Cons ((Joint.OP2 (BackEndOps.Sub, (Obj.magic a), (Obj.magic a),
465    (Obj.magic (Joint.hdw_argument_from_byte Joint.zero_byte)))), (List.Cons
466    ((Joint.MOVE
467    (Obj.magic (Joint_LTL_LIN.From_acc (I8051.registerSPH, a)))),
468    List.Nil)))))))))))))
469
470(** val delframe :
471    AST.ident List.list -> Nat.nat -> Joint.joint_seq List.list **)
472let delframe globals stack_sz =
473  List.Cons ((Joint.MOVE
474    (Obj.magic (Joint_LTL_LIN.To_acc (a, I8051.registerSPL)))), (List.Cons
475    ((Joint.OP2 (BackEndOps.Add, (Obj.magic a), (Obj.magic a),
476    (Obj.magic (Joint.hdw_argument_from_byte (Joint.byte_of_nat stack_sz))))),
477    (List.Cons ((Joint.MOVE
478    (Obj.magic (Joint_LTL_LIN.From_acc (I8051.registerSPL, a)))), (List.Cons
479    ((Joint.MOVE (Obj.magic (Joint_LTL_LIN.To_acc (a, I8051.registerSPH)))),
480    (List.Cons ((Joint.OP2 (BackEndOps.Addc, (Obj.magic a), (Obj.magic a),
481    (Obj.magic (Joint.hdw_argument_from_byte Joint.zero_byte)))), (List.Cons
482    ((Joint.MOVE
483    (Obj.magic (Joint_LTL_LIN.From_acc (I8051.registerSPH, a)))),
484    List.Nil)))))))))))
485
486(** val commutative : BackEndOps.op2 -> Bool.bool **)
487let commutative = function
488| BackEndOps.Add -> Bool.True
489| BackEndOps.Addc -> Bool.True
490| BackEndOps.Sub -> Bool.False
491| BackEndOps.And -> Bool.True
492| BackEndOps.Or -> Bool.True
493| BackEndOps.Xor -> Bool.True
494
495(** val uses_carry : BackEndOps.op2 -> Bool.bool **)
496let uses_carry = function
497| BackEndOps.Add -> Bool.False
498| BackEndOps.Addc -> Bool.True
499| BackEndOps.Sub -> Bool.True
500| BackEndOps.And -> Bool.False
501| BackEndOps.Or -> Bool.False
502| BackEndOps.Xor -> Bool.False
503
504(** val sets_carry : BackEndOps.op2 -> Bool.bool **)
505let sets_carry = function
506| BackEndOps.Add -> Bool.True
507| BackEndOps.Addc -> Bool.True
508| BackEndOps.Sub -> Bool.True
509| BackEndOps.And -> Bool.False
510| BackEndOps.Or -> Bool.False
511| BackEndOps.Xor -> Bool.False
512
513(** val translate_op2 :
514    AST.ident List.list -> Nat.nat -> Bool.bool -> BackEndOps.op2 ->
515    Interference.decision -> arg_decision -> arg_decision -> Joint.joint_seq
516    List.list **)
517let translate_op2 globals localss carry_lives_after op dst arg1 arg2 =
518  List.append
519    (preserve_carry_bit globals
520      (Bool.andb (uses_carry op)
521        (Bool.orb (arg_is_spilled arg1) (arg_is_spilled arg2)))
522      (List.append
523        (move globals localss Bool.False (Interference.Decision_colour
524          I8051.RegisterB) arg2)
525        (move globals localss Bool.False (Interference.Decision_colour
526          I8051.RegisterA) arg1)))
527    (List.append (List.Cons ((Joint.OP2 (op, (Obj.magic a), (Obj.magic a),
528      (Obj.magic (Joint.hdw_argument_from_reg I8051.RegisterB)))), List.Nil))
529      (move globals localss (Bool.andb (sets_carry op) carry_lives_after) dst
530        (Arg_decision_colour I8051.RegisterA)))
531
532(** val translate_op2_smart :
533    AST.ident List.list -> Nat.nat -> Bool.bool -> BackEndOps.op2 ->
534    Interference.decision -> arg_decision -> arg_decision -> Joint.joint_seq
535    List.list **)
536let translate_op2_smart globals localss carry_lives_after op dst arg1 arg2 =
537  preserve_carry_bit globals
538    (Bool.andb (Bool.andb (Bool.notb (sets_carry op)) carry_lives_after)
539      (Bool.orb (Bool.orb (arg_is_spilled arg1) (arg_is_spilled arg2))
540        (is_spilled dst)))
541    (match arg2 with
542     | Arg_decision_colour arg2r ->
543       List.append
544         (move globals localss (uses_carry op) (Interference.Decision_colour
545           I8051.RegisterA) arg1)
546         (List.append (List.Cons ((Joint.OP2 (op, (Obj.magic a),
547           (Obj.magic a), (Obj.magic (Joint.hdw_argument_from_reg arg2r)))),
548           List.Nil))
549           (move globals localss
550             (Bool.andb (sets_carry op) carry_lives_after) dst
551             (Arg_decision_colour I8051.RegisterA)))
552     | Arg_decision_spill x ->
553       (match commutative op with
554        | Bool.True ->
555          (match arg1 with
556           | Arg_decision_colour arg1r ->
557             List.append
558               (move globals localss (uses_carry op)
559                 (Interference.Decision_colour I8051.RegisterA) arg2)
560               (List.append (List.Cons ((Joint.OP2 (op, (Obj.magic a),
561                 (Obj.magic a),
562                 (Obj.magic (Joint.hdw_argument_from_reg arg1r)))),
563                 List.Nil))
564                 (move globals localss
565                   (Bool.andb (sets_carry op) carry_lives_after) dst
566                   (Arg_decision_colour I8051.RegisterA)))
567           | Arg_decision_spill x0 ->
568             translate_op2 globals localss carry_lives_after op dst arg1 arg2
569           | Arg_decision_imm arg1i ->
570             List.append
571               (move globals localss (uses_carry op)
572                 (Interference.Decision_colour I8051.RegisterA) arg2)
573               (List.append (List.Cons ((Joint.OP2 (op, (Obj.magic a),
574                 (Obj.magic a),
575                 (Obj.magic (Joint.hdw_argument_from_byte arg1i)))),
576                 List.Nil))
577                 (move globals localss
578                   (Bool.andb (sets_carry op) carry_lives_after) dst
579                   (Arg_decision_colour I8051.RegisterA))))
580        | Bool.False ->
581          translate_op2 globals localss carry_lives_after op dst arg1 arg2)
582     | Arg_decision_imm arg2i ->
583       List.append
584         (move globals localss (uses_carry op) (Interference.Decision_colour
585           I8051.RegisterA) arg1)
586         (List.append (List.Cons ((Joint.OP2 (op, (Obj.magic a),
587           (Obj.magic a), (Obj.magic (Joint.hdw_argument_from_byte arg2i)))),
588           List.Nil))
589           (move globals localss
590             (Bool.andb (sets_carry op) carry_lives_after) dst
591             (Arg_decision_colour I8051.RegisterA))))
592
593(** val dec_to_arg_dec : Interference.decision -> arg_decision **)
594let dec_to_arg_dec = function
595| Interference.Decision_spill n -> Arg_decision_spill n
596| Interference.Decision_colour r -> Arg_decision_colour r
597
598(** val reg_to_dec__o__dec_arg_dec__o__inject :
599    I8051.register -> arg_decision Types.sig0 **)
600let reg_to_dec__o__dec_arg_dec__o__inject x0 =
601  dec_to_arg_dec (Interference.Decision_colour x0)
602
603(** val dpi1__o__Reg_to_dec__o__dec_arg_dec__o__inject :
604    (I8051.register, 'a1) Types.dPair -> arg_decision Types.sig0 **)
605let dpi1__o__Reg_to_dec__o__dec_arg_dec__o__inject x2 =
606  dec_to_arg_dec (dpi1__o__Reg_to_dec x2)
607
608(** val eject__o__Reg_to_dec__o__dec_arg_dec__o__inject :
609    I8051.register Types.sig0 -> arg_decision Types.sig0 **)
610let eject__o__Reg_to_dec__o__dec_arg_dec__o__inject x2 =
611  dec_to_arg_dec (eject__o__Reg_to_dec x2)
612
613(** val dpi1__o__dec_arg_dec__o__inject :
614    (Interference.decision, 'a1) Types.dPair -> arg_decision Types.sig0 **)
615let dpi1__o__dec_arg_dec__o__inject x2 =
616  dec_to_arg_dec x2.Types.dpi1
617
618(** val eject__o__dec_arg_dec__o__inject :
619    Interference.decision Types.sig0 -> arg_decision Types.sig0 **)
620let eject__o__dec_arg_dec__o__inject x2 =
621  dec_to_arg_dec (Types.pi1 x2)
622
623(** val dec_arg_dec__o__inject :
624    Interference.decision -> arg_decision Types.sig0 **)
625let dec_arg_dec__o__inject x1 =
626  dec_to_arg_dec x1
627
628(** val reg_to_dec__o__dec_arg_dec : I8051.register -> arg_decision **)
629let reg_to_dec__o__dec_arg_dec x0 =
630  dec_to_arg_dec (Interference.Decision_colour x0)
631
632(** val dpi1__o__Reg_to_dec__o__dec_arg_dec :
633    (I8051.register, 'a1) Types.dPair -> arg_decision **)
634let dpi1__o__Reg_to_dec__o__dec_arg_dec x1 =
635  dec_to_arg_dec (dpi1__o__Reg_to_dec x1)
636
637(** val eject__o__Reg_to_dec__o__dec_arg_dec :
638    I8051.register Types.sig0 -> arg_decision **)
639let eject__o__Reg_to_dec__o__dec_arg_dec x1 =
640  dec_to_arg_dec (eject__o__Reg_to_dec x1)
641
642(** val dpi1__o__dec_arg_dec :
643    (Interference.decision, 'a1) Types.dPair -> arg_decision **)
644let dpi1__o__dec_arg_dec x1 =
645  dec_to_arg_dec x1.Types.dpi1
646
647(** val eject__o__dec_arg_dec :
648    Interference.decision Types.sig0 -> arg_decision **)
649let eject__o__dec_arg_dec x1 =
650  dec_to_arg_dec (Types.pi1 x1)
651
652(** val translate_op1 :
653    AST.ident List.list -> Nat.nat -> Bool.bool -> BackEndOps.op1 ->
654    Interference.decision -> Interference.decision -> Joint.joint_seq
655    List.list **)
656let translate_op1 globals localss carry_lives_after op dst arg =
657  let preserve_carry =
658    Bool.andb carry_lives_after (Bool.orb (is_spilled dst) (is_spilled arg))
659  in
660  preserve_carry_bit globals preserve_carry
661    (List.append
662      (move globals localss Bool.False (Interference.Decision_colour
663        I8051.RegisterA) (dec_to_arg_dec arg)) (List.Cons ((Joint.OP1 (op,
664      (Obj.magic Types.It), (Obj.magic Types.It))),
665      (move globals localss Bool.False dst (Arg_decision_colour
666        I8051.RegisterA)))))
667
668(** val translate_opaccs :
669    AST.ident List.list -> Nat.nat -> Bool.bool -> BackEndOps.opAccs ->
670    Interference.decision -> Interference.decision -> arg_decision ->
671    arg_decision -> Joint.joint_seq List.list **)
672let translate_opaccs globals localss carry_lives_after op dst1 dst2 arg1 arg2 =
673  List.append
674    (move globals localss Bool.False (Interference.Decision_colour
675      I8051.RegisterB) arg2)
676    (List.append
677      (move globals localss Bool.False (Interference.Decision_colour
678        I8051.RegisterA) arg1) (List.Cons ((Joint.OPACCS (op,
679      (Obj.magic Types.It), (Obj.magic Types.It), (Obj.magic Types.It),
680      (Obj.magic Types.It))),
681      (List.append
682        (move globals localss Bool.False dst1 (Arg_decision_colour
683          I8051.RegisterA))
684        (List.append
685          (move globals localss Bool.False dst2 (Arg_decision_colour
686            I8051.RegisterB))
687          (match Bool.andb carry_lives_after
688                   (Bool.orb (is_spilled dst1) (is_spilled dst2)) with
689           | Bool.True -> List.Cons (Joint.CLEAR_CARRY, List.Nil)
690           | Bool.False -> List.Nil))))))
691
692(** val move_to_dp :
693    AST.ident List.list -> Nat.nat -> arg_decision -> arg_decision ->
694    Joint.joint_seq List.list **)
695let move_to_dp globals localss arg1 arg2 =
696  match Bool.notb (arg_is_spilled arg1) with
697  | Bool.True ->
698    List.append
699      (move globals localss Bool.False (Interference.Decision_colour
700        I8051.RegisterDPH) arg2)
701      (move globals localss Bool.False (Interference.Decision_colour
702        I8051.RegisterDPL) arg1)
703  | Bool.False ->
704    (match Bool.notb (arg_is_spilled arg2) with
705     | Bool.True ->
706       List.append
707         (move globals localss Bool.False (Interference.Decision_colour
708           I8051.RegisterDPL) arg1)
709         (move globals localss Bool.False (Interference.Decision_colour
710           I8051.RegisterDPH) arg2)
711     | Bool.False ->
712       List.append
713         (move globals localss Bool.False (Interference.Decision_colour
714           I8051.RegisterB) arg1)
715         (List.append
716           (move globals localss Bool.False (Interference.Decision_colour
717             I8051.RegisterDPH) arg2)
718           (move globals localss Bool.False (Interference.Decision_colour
719             I8051.RegisterDPL) (Arg_decision_colour I8051.RegisterB))))
720
721(** val translate_store :
722    AST.ident List.list -> Nat.nat -> Bool.bool -> arg_decision ->
723    arg_decision -> arg_decision -> Joint.joint_seq List.list **)
724let translate_store globals localss carry_lives_after addr1 addr2 src =
725  preserve_carry_bit globals
726    (Bool.andb carry_lives_after
727      (Bool.orb (Bool.orb (arg_is_spilled addr1) (arg_is_spilled addr1))
728        (arg_is_spilled src)))
729    (let move_to_dptr = move_to_dp globals localss addr1 addr2 in
730    List.append
731      (match arg_is_spilled src with
732       | Bool.True ->
733         List.append
734           (move globals localss Bool.False (Interference.Decision_colour
735             I8051.registerST0) src)
736           (List.append move_to_dptr (List.Cons ((Joint.MOVE
737             (Obj.magic (Joint_LTL_LIN.To_acc (a, I8051.registerST0)))),
738             List.Nil)))
739       | Bool.False -> move_to_dptr) (List.Cons ((Joint.STORE
740      ((Obj.magic Types.It), (Obj.magic Types.It), (Obj.magic a))),
741      List.Nil)))
742
743(** val translate_load :
744    AST.ident List.list -> Nat.nat -> Bool.bool -> Interference.decision ->
745    arg_decision -> arg_decision -> Joint.joint_seq List.list **)
746let translate_load globals localss carry_lives_after dst addr1 addr2 =
747  preserve_carry_bit globals
748    (Bool.andb carry_lives_after
749      (Bool.orb (Bool.orb (is_spilled dst) (arg_is_spilled addr1))
750        (arg_is_spilled addr1)))
751    (List.append (move_to_dp globals localss addr1 addr2)
752      (List.append (List.Cons ((Joint.LOAD ((Obj.magic a),
753        (Obj.magic Types.It), (Obj.magic Types.It))), List.Nil))
754        (move globals localss Bool.False dst (Arg_decision_colour
755          I8051.RegisterA))))
756
757(** val translate_address :
758    __ List.list -> Nat.nat -> Bool.bool -> __ -> Interference.decision ->
759    Interference.decision -> Joint.joint_seq List.list **)
760let translate_address globals localss carry_lives_after id addr1 addr2 =
761  preserve_carry_bit (Obj.magic globals)
762    (Bool.andb carry_lives_after
763      (Bool.orb (is_spilled addr1) (is_spilled addr2))) (List.Cons
764    ((Joint.ADDRESS ((Obj.magic id), (Obj.magic Types.It),
765    (Obj.magic Types.It))),
766    (List.append
767      (move (Obj.magic globals) localss Bool.False addr1 (Arg_decision_colour
768        I8051.RegisterDPL))
769      (move (Obj.magic globals) localss Bool.False addr2 (Arg_decision_colour
770        I8051.RegisterDPH)))))
771
772(** val translate_low_address :
773    AST.ident List.list -> Nat.nat -> Bool.bool -> Interference.decision ->
774    Graphs.label -> Joint.joint_seq List.list **)
775let translate_low_address globals localss carry_lives_after dst lbl =
776  match dst with
777  | Interference.Decision_spill x ->
778    List.Cons ((Joint.Extension_seq
779      (Obj.magic (Joint_LTL_LIN.LOW_ADDRESS (I8051.RegisterA, lbl)))),
780      (move globals localss carry_lives_after dst (Arg_decision_colour
781        I8051.RegisterA)))
782  | Interference.Decision_colour r ->
783    List.Cons ((Joint.Extension_seq
784      (Obj.magic (Joint_LTL_LIN.LOW_ADDRESS (r, lbl)))), List.Nil)
785
786(** val translate_high_address :
787    AST.ident List.list -> Nat.nat -> Bool.bool -> Interference.decision ->
788    Graphs.label -> Joint.joint_seq List.list **)
789let translate_high_address globals localss carry_lives_after dst lbl =
790  match dst with
791  | Interference.Decision_spill x ->
792    List.Cons ((Joint.Extension_seq
793      (Obj.magic (Joint_LTL_LIN.HIGH_ADDRESS (I8051.RegisterA, lbl)))),
794      (move globals localss carry_lives_after dst (Arg_decision_colour
795        I8051.RegisterA)))
796  | Interference.Decision_colour r ->
797    List.Cons ((Joint.Extension_seq
798      (Obj.magic (Joint_LTL_LIN.HIGH_ADDRESS (r, lbl)))), List.Nil)
799
800(** val translate_step :
801    AST.ident List.list -> Nat.nat -> Fixpoints.valuation ->
802    Interference.coloured_graph -> Nat.nat -> Graphs.label ->
803    Joint.joint_step -> Blocks.bind_step_block **)
804let translate_step globals localss after grph stack_sz lbl s =
805  Bind_new.Bret
806    (let lookup = fun r -> grph.Interference.colouring (Types.Inl r) in
807    let lookup_arg = fun a0 ->
808      match a0 with
809      | Joint.Reg r -> dec_to_arg_dec (lookup r)
810      | Joint.Imm b -> Arg_decision_imm b
811    in
812    let carry_lives_after = Liveness.hlives I8051.RegisterCarry (after lbl)
813    in
814    let move0 = move globals localss carry_lives_after in
815    (match s with
816     | Joint.COST_LABEL cost_lbl ->
817       { Types.fst = { Types.fst = List.Nil; Types.snd = (fun x ->
818         Joint.COST_LABEL cost_lbl) }; Types.snd = List.Nil }
819     | Joint.CALL (f, n_args, x) ->
820       (match f with
821        | Types.Inl f0 ->
822          { Types.fst = { Types.fst = List.Nil; Types.snd = (fun x0 ->
823            Joint.CALL ((Types.Inl f0), n_args, (Obj.magic Types.It))) };
824            Types.snd = List.Nil }
825        | Types.Inr dp ->
826          let { Types.fst = dpl; Types.snd = dph } = dp in
827          { Types.fst = { Types.fst =
828          (Blocks.add_dummy_variance
829            (move_to_dp globals localss (Obj.magic lookup_arg dpl)
830              (Obj.magic lookup_arg dph))); Types.snd = (fun x0 -> Joint.CALL
831          ((Types.Inr { Types.fst = (Obj.magic Types.It); Types.snd =
832          (Obj.magic Types.It) }), n_args, (Obj.magic Types.It))) };
833          Types.snd = List.Nil })
834     | Joint.COND (r, ltrue) ->
835       { Types.fst = { Types.fst =
836         (Blocks.add_dummy_variance
837           (move0 (Interference.Decision_colour I8051.RegisterA)
838             (dec_to_arg_dec (Obj.magic lookup r)))); Types.snd = (fun x ->
839         Joint.COND ((Obj.magic Types.It), ltrue)) }; Types.snd = List.Nil }
840     | Joint.Step_seq s' ->
841       (match s' with
842        | Joint.COMMENT c ->
843          Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
844            globals (List.Cons ((Joint.COMMENT c), List.Nil))
845        | Joint.MOVE pair_regs ->
846          let lookup_move_dst = fun x ->
847            match x with
848            | ERTL.PSD r -> lookup r
849            | ERTL.HDW r -> Interference.Decision_colour r
850          in
851          let dst = lookup_move_dst (Obj.magic pair_regs).Types.fst in
852          let src =
853            match (Obj.magic pair_regs).Types.snd with
854            | Joint.Reg r -> dec_to_arg_dec (lookup_move_dst r)
855            | Joint.Imm b -> Arg_decision_imm b
856          in
857          Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
858            globals (move0 dst src)
859        | Joint.POP r ->
860          Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
861            globals (List.Cons ((Joint.POP (Obj.magic a)),
862            (move0 (Obj.magic lookup r) (Arg_decision_colour
863              I8051.RegisterA))))
864        | Joint.PUSH a0 ->
865          Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
866            globals
867            (List.append
868              (move0 (Interference.Decision_colour I8051.RegisterA)
869                (Obj.magic lookup_arg a0)) (List.Cons ((Joint.PUSH
870              (Obj.magic a)), List.Nil)))
871        | Joint.ADDRESS (lbl0, dpl, dph) ->
872          Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
873            globals
874            (translate_address (Obj.magic globals) localss carry_lives_after
875              (Obj.magic lbl0) (Obj.magic lookup dpl) (Obj.magic lookup dph))
876        | Joint.OPACCS (op, dst1, dst2, arg1, arg2) ->
877          Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
878            globals
879            (translate_opaccs globals localss carry_lives_after op
880              (Obj.magic lookup dst1) (Obj.magic lookup dst2)
881              (Obj.magic lookup_arg arg1) (Obj.magic lookup_arg arg2))
882        | Joint.OP1 (op, dst, arg) ->
883          Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
884            globals
885            (translate_op1 globals localss carry_lives_after op
886              (Obj.magic lookup dst) (Obj.magic lookup arg))
887        | Joint.OP2 (op, dst, arg1, arg2) ->
888          Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
889            globals
890            (translate_op2_smart globals localss carry_lives_after op
891              (Obj.magic lookup dst) (Obj.magic lookup_arg arg1)
892              (Obj.magic lookup_arg arg2))
893        | Joint.CLEAR_CARRY ->
894          Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
895            globals (List.Cons (Joint.CLEAR_CARRY, List.Nil))
896        | Joint.SET_CARRY ->
897          Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
898            globals (List.Cons (Joint.SET_CARRY, List.Nil))
899        | Joint.LOAD (dstr, addr1, addr2) ->
900          Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
901            globals
902            (translate_load globals localss carry_lives_after
903              (Obj.magic lookup dstr) (Obj.magic lookup_arg addr1)
904              (Obj.magic lookup_arg addr2))
905        | Joint.STORE (addr1, addr2, srcr) ->
906          Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
907            globals
908            (translate_store globals localss carry_lives_after
909              (Obj.magic lookup_arg addr1) (Obj.magic lookup_arg addr2)
910              (Obj.magic lookup_arg srcr))
911        | Joint.Extension_seq ext ->
912          Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
913            globals
914            (match Obj.magic ext with
915             | ERTLptr.Ertlptr_ertl ext' ->
916               (match ext' with
917                | ERTL.Ertl_new_frame -> newframe globals stack_sz
918                | ERTL.Ertl_del_frame -> delframe globals stack_sz
919                | ERTL.Ertl_frame_size r ->
920                  move0 (lookup r) (Arg_decision_imm
921                    (Joint.byte_of_nat stack_sz)))
922             | ERTLptr.LOW_ADDRESS (r1, l) ->
923               translate_low_address globals localss carry_lives_after
924                 (lookup r1) l
925             | ERTLptr.HIGH_ADDRESS (r1, l) ->
926               translate_high_address globals localss carry_lives_after
927                 (lookup r1) l))))
928
929(** val translate_fin_step :
930    AST.ident List.list -> Graphs.label -> Joint.joint_fin_step ->
931    Blocks.bind_fin_block **)
932let translate_fin_step globals lbl s =
933  Bind_new.Bret { Types.fst = List.Nil; Types.snd =
934    (match s with
935     | Joint.GOTO l -> Joint.GOTO l
936     | Joint.RETURN -> Joint.RETURN
937     | Joint.TAILCALL (x, x0) -> assert false (* absurd case *)) }
938
939(** val translate_data :
940    Fixpoints.fixpoint_computer -> Interference.coloured_graph_computer ->
941    AST.ident List.list -> Joint.joint_closed_internal_function ->
942    (Registers.register, TranslateUtils.b_graph_translate_data)
943    Bind_new.bind_new **)
944let translate_data the_fixpoint build globals int_fun =
945  let after =
946    Liveness.analyse_liveness the_fixpoint globals (Types.pi1 int_fun)
947  in
948  let coloured_graph = build globals (Types.pi1 int_fun) after in
949  let stack_sz =
950    Nat.plus coloured_graph.Interference.spilled_no
951      (Types.pi1 int_fun).Joint.joint_if_stacksize
952  in
953  Bind_new.Bret { TranslateUtils.init_ret = (Obj.magic Types.It);
954  TranslateUtils.init_params = (Obj.magic Types.It);
955  TranslateUtils.init_stack_size = stack_sz; TranslateUtils.added_prologue =
956  List.Nil; TranslateUtils.new_regs = List.Nil; TranslateUtils.f_step =
957  (translate_step globals (Types.pi1 int_fun).Joint.joint_if_local_stacksize
958    after coloured_graph stack_sz); TranslateUtils.f_fin =
959  (translate_fin_step globals) }
960
961(** val ertlptr_to_ltl :
962    Fixpoints.fixpoint_computer -> Interference.coloured_graph_computer ->
963    ERTLptr.ertlptr_program -> ((LTL.ltl_program, Joint.stack_cost_model)
964    Types.prod, Nat.nat) Types.prod **)
965let ertlptr_to_ltl the_fixpoint build pr =
966  let ltlprog =
967    TranslateUtils.b_graph_transform_program ERTLptr.eRTLptr LTL.lTL
968      (fun globals h -> translate_data the_fixpoint build globals h) pr
969  in
970  { Types.fst = { Types.fst = ltlprog; Types.snd =
971  (Joint.stack_cost (Joint.graph_params_to_params LTL.lTL) ltlprog) };
972  Types.snd =
973  (Nat.minus
974    (Exp.exp (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
975      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
976      Nat.O)))))))))))))))))
977    (Joint.globals_stacksize (Joint.graph_params_to_params LTL.lTL) ltlprog)) }
978
Note: See TracBrowser for help on using the repository browser.