source: extracted/eRTLToLTL.ml @ 3019

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

New extraction after ERTLptr abortion.

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