source: driver/extracted/eRTLToLTL.ml @ 3106

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

New extraction.
File size: 37.1 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_19045 -> h_arg_decision_colour x_19045
182| Arg_decision_spill x_19046 -> h_arg_decision_spill x_19046
183| Arg_decision_imm x_19047 -> h_arg_decision_imm x_19047
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_19052 -> h_arg_decision_colour x_19052
190| Arg_decision_spill x_19053 -> h_arg_decision_spill x_19053
191| Arg_decision_imm x_19054 -> h_arg_decision_imm x_19054
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_19059 -> h_arg_decision_colour x_19059
198| Arg_decision_spill x_19060 -> h_arg_decision_spill x_19060
199| Arg_decision_imm x_19061 -> h_arg_decision_imm x_19061
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_19066 -> h_arg_decision_colour x_19066
206| Arg_decision_spill x_19067 -> h_arg_decision_spill x_19067
207| Arg_decision_imm x_19068 -> h_arg_decision_imm x_19068
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_19073 -> h_arg_decision_colour x_19073
214| Arg_decision_spill x_19074 -> h_arg_decision_spill x_19074
215| Arg_decision_imm x_19075 -> h_arg_decision_imm x_19075
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_19080 -> h_arg_decision_colour x_19080
222| Arg_decision_spill x_19081 -> h_arg_decision_spill x_19081
223| Arg_decision_imm x_19082 -> h_arg_decision_imm x_19082
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 ->
752         List.append move_to_dptr
753           (move globals localss Bool.False (Interference.Decision_colour
754             I8051.RegisterA) src)) (List.Cons ((Joint.STORE
755      ((Obj.magic Types.It), (Obj.magic Types.It), (Obj.magic a))),
756      List.Nil)))
757
758(** val translate_load :
759    AST.ident List.list -> Nat.nat -> Bool.bool -> Interference.decision ->
760    arg_decision -> arg_decision -> Joint.joint_seq List.list **)
761let translate_load globals localss carry_lives_after dst addr1 addr2 =
762  preserve_carry_bit globals
763    (Bool.andb carry_lives_after
764      (Bool.orb (Bool.orb (is_spilled dst) (arg_is_spilled addr1))
765        (arg_is_spilled addr1)))
766    (List.append (move_to_dp globals localss addr1 addr2)
767      (List.append (List.Cons ((Joint.LOAD ((Obj.magic a),
768        (Obj.magic Types.It), (Obj.magic Types.It))), List.Nil))
769        (move globals localss Bool.False dst (Arg_decision_colour
770          I8051.RegisterA))))
771
772(** val translate_address :
773    __ List.list -> Nat.nat -> Bool.bool -> __ -> BitVector.word ->
774    Interference.decision -> Interference.decision -> Joint.joint_seq
775    List.list **)
776let translate_address globals localss carry_lives_after id off addr1 addr2 =
777  preserve_carry_bit (Obj.magic globals)
778    (Bool.andb carry_lives_after
779      (Bool.orb (is_spilled addr1) (is_spilled addr2))) (List.Cons
780    ((Joint.ADDRESS ((Obj.magic id), off, (Obj.magic Types.It),
781    (Obj.magic Types.It))),
782    (List.append
783      (move (Obj.magic globals) localss Bool.False addr1 (Arg_decision_colour
784        I8051.RegisterDPL))
785      (move (Obj.magic globals) localss Bool.False addr2 (Arg_decision_colour
786        I8051.RegisterDPH)))))
787
788(** val translate_step :
789    AST.ident List.list -> Joint.joint_internal_function -> Nat.nat ->
790    Fixpoints.valuation -> Interference.coloured_graph -> Nat.nat ->
791    Graphs.label -> Joint.joint_step -> Blocks.bind_step_block **)
792let translate_step globals fn localss after grph stack_sz lbl s =
793  Bind_new.Bret
794    (let lookup = fun r -> grph.Interference.colouring (Types.Inl r) in
795    let lookup_arg = fun a0 ->
796      match a0 with
797      | Joint.Reg r -> dec_to_arg_dec (lookup r)
798      | Joint.Imm b -> Arg_decision_imm b
799    in
800    let carry_lives_after = Liveness.hlives I8051.RegisterCarry (after lbl)
801    in
802    let move0 = move globals localss carry_lives_after in
803    (match Liveness.eliminable_step globals (after lbl) s with
804     | Bool.True ->
805       let x =
806         Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
807           globals List.Nil
808       in
809       x
810     | Bool.False ->
811       (match s with
812        | Joint.COST_LABEL cost_lbl ->
813          { Types.fst = { Types.fst = List.Nil; Types.snd = (fun x ->
814            Joint.COST_LABEL cost_lbl) }; Types.snd = List.Nil }
815        | Joint.CALL (f, n_args, x) ->
816          (match f with
817           | Types.Inl f0 ->
818             { Types.fst = { Types.fst = List.Nil; Types.snd = (fun x0 ->
819               Joint.CALL ((Types.Inl f0), n_args, (Obj.magic Types.It))) };
820               Types.snd = List.Nil }
821           | Types.Inr dp ->
822             let { Types.fst = dpl; Types.snd = dph } = dp in
823             { Types.fst = { Types.fst =
824             (List.append
825               (Blocks.add_dummy_variance
826                 (move_to_dp globals localss (Obj.magic lookup_arg dpl)
827                   (Obj.magic lookup_arg dph))) (List.Cons ((fun l ->
828               let x0 = Joint.Extension_seq
829                 (Obj.magic (Joint_LTL_LIN.LOW_ADDRESS (Obj.magic l)))
830               in
831               x0), (List.Cons ((fun x0 -> Joint.PUSH (Obj.magic Types.It)),
832               (List.Cons ((fun l -> Joint.Extension_seq
833               (Obj.magic (Joint_LTL_LIN.HIGH_ADDRESS (Obj.magic l)))),
834               (List.Cons ((fun x0 -> Joint.PUSH (Obj.magic Types.It)),
835               (List.Cons ((fun x0 -> Joint.MOVE
836               (Obj.magic (Joint_LTL_LIN.Int_to_acc (a, Joint.zero_byte)))),
837               List.Nil))))))))))); Types.snd = (fun x0 -> Joint.CALL
838             ((Types.Inr { Types.fst = (Obj.magic Types.It); Types.snd =
839             (Obj.magic Types.It) }), n_args, (Obj.magic Types.It))) };
840             Types.snd = List.Nil })
841        | Joint.COND (r, ltrue) ->
842          { Types.fst = { Types.fst =
843            (Blocks.add_dummy_variance
844              (move0 (Interference.Decision_colour I8051.RegisterA)
845                (dec_to_arg_dec (Obj.magic lookup r)))); Types.snd =
846            (fun x -> Joint.COND ((Obj.magic Types.It), ltrue)) };
847            Types.snd = List.Nil }
848        | Joint.Step_seq s' ->
849          (match s' with
850           | Joint.COMMENT c ->
851             Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
852               globals (List.Cons ((Joint.COMMENT c), List.Nil))
853           | Joint.MOVE pair_regs ->
854             let lookup_move_dst = fun x ->
855               match x with
856               | ERTL.PSD r -> lookup r
857               | ERTL.HDW r -> Interference.Decision_colour r
858             in
859             let dst = lookup_move_dst (Obj.magic pair_regs).Types.fst in
860             let src =
861               match (Obj.magic pair_regs).Types.snd with
862               | Joint.Reg r -> dec_to_arg_dec (lookup_move_dst r)
863               | Joint.Imm b -> Arg_decision_imm b
864             in
865             Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
866               globals (move0 dst src)
867           | Joint.POP r ->
868             Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
869               globals (List.Cons ((Joint.POP (Obj.magic a)),
870               (move0 (Obj.magic lookup r) (Arg_decision_colour
871                 I8051.RegisterA))))
872           | Joint.PUSH a0 ->
873             Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
874               globals
875               (List.append
876                 (move0 (Interference.Decision_colour I8051.RegisterA)
877                   (Obj.magic lookup_arg a0)) (List.Cons ((Joint.PUSH
878                 (Obj.magic a)), List.Nil)))
879           | Joint.ADDRESS (lbl0, off, dpl, dph) ->
880             Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
881               globals
882               (translate_address (Obj.magic globals) localss
883                 carry_lives_after (Obj.magic lbl0) off
884                 (Obj.magic lookup dpl) (Obj.magic lookup dph))
885           | Joint.OPACCS (op, dst1, dst2, arg1, arg2) ->
886             Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
887               globals
888               (translate_opaccs globals localss carry_lives_after op
889                 (Obj.magic lookup dst1) (Obj.magic lookup dst2)
890                 (Obj.magic lookup_arg arg1) (Obj.magic lookup_arg arg2))
891           | Joint.OP1 (op, dst, arg) ->
892             Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
893               globals
894               (translate_op1 globals localss carry_lives_after op
895                 (Obj.magic lookup dst) (Obj.magic lookup arg))
896           | Joint.OP2 (op, dst, arg1, arg2) ->
897             Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
898               globals
899               (translate_op2_smart globals localss carry_lives_after op
900                 (Obj.magic lookup dst) (Obj.magic lookup_arg arg1)
901                 (Obj.magic lookup_arg arg2))
902           | Joint.CLEAR_CARRY ->
903             Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
904               globals (List.Cons (Joint.CLEAR_CARRY, List.Nil))
905           | Joint.SET_CARRY ->
906             Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
907               globals (List.Cons (Joint.SET_CARRY, List.Nil))
908           | Joint.LOAD (dstr, addr1, addr2) ->
909             Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
910               globals
911               (translate_load globals localss carry_lives_after
912                 (Obj.magic lookup dstr) (Obj.magic lookup_arg addr1)
913                 (Obj.magic lookup_arg addr2))
914           | Joint.STORE (addr1, addr2, srcr) ->
915             Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
916               globals
917               (translate_store globals localss carry_lives_after
918                 (Obj.magic lookup_arg addr1) (Obj.magic lookup_arg addr2)
919                 (Obj.magic lookup_arg srcr))
920           | Joint.Extension_seq ext ->
921             Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
922               globals
923               (match Obj.magic ext with
924                | ERTL.Ertl_new_frame -> newframe globals stack_sz
925                | ERTL.Ertl_del_frame -> delframe globals stack_sz
926                | ERTL.Ertl_frame_size r ->
927                  move0 (lookup r) (Arg_decision_imm
928                    (Joint.byte_of_nat stack_sz)))))))
929
930(** val translate_fin_step :
931    AST.ident List.list -> Graphs.label -> Joint.joint_fin_step ->
932    Blocks.bind_fin_block **)
933let translate_fin_step globals lbl s =
934  Bind_new.Bret { Types.fst = List.Nil; Types.snd =
935    (match s with
936     | Joint.GOTO l -> Joint.GOTO l
937     | Joint.RETURN -> Joint.RETURN
938     | Joint.TAILCALL (x, x0) -> assert false (* absurd case *)) }
939
940(** val translate_data :
941    Fixpoints.fixpoint_computer -> Interference.coloured_graph_computer ->
942    AST.ident List.list -> Joint.joint_closed_internal_function ->
943    (Registers.register, TranslateUtils.b_graph_translate_data)
944    Bind_new.bind_new **)
945let translate_data the_fixpoint build globals int_fun =
946  let after =
947    Liveness.analyse_liveness the_fixpoint globals (Types.pi1 int_fun)
948  in
949  let coloured_graph =
950    build globals (Types.pi1 int_fun)
951      (Fixpoints.fix_lfp Liveness.register_lattice
952        (Liveness.liveafter globals (Types.pi1 int_fun)) after)
953  in
954  let stack_sz =
955    Nat.plus coloured_graph.Interference.spilled_no
956      (Types.pi1 int_fun).Joint.joint_if_stacksize
957  in
958  Bind_new.Bret { TranslateUtils.init_ret = (Obj.magic Types.It);
959  TranslateUtils.init_params = (Obj.magic Types.It);
960  TranslateUtils.init_stack_size = stack_sz; TranslateUtils.added_prologue =
961  List.Nil; TranslateUtils.new_regs = List.Nil; TranslateUtils.f_step =
962  (translate_step globals (Types.pi1 int_fun)
963    (Types.pi1 int_fun).Joint.joint_if_local_stacksize
964    (Fixpoints.fix_lfp Liveness.register_lattice
965      (Liveness.liveafter globals (Types.pi1 int_fun)) after) coloured_graph
966    stack_sz); TranslateUtils.f_fin = (translate_fin_step globals) }
967
968(** val ertl_to_ltl :
969    Fixpoints.fixpoint_computer -> Interference.coloured_graph_computer ->
970    ERTL.ertl_program -> ((LTL.ltl_program, Joint.stack_cost_model)
971    Types.prod, Nat.nat) Types.prod **)
972let ertl_to_ltl the_fixpoint build pr =
973  let ltlprog =
974    TranslateUtils.b_graph_transform_program ERTL.eRTL LTL.lTL
975      (fun globals h -> translate_data the_fixpoint build globals h) pr
976  in
977  { Types.fst = { Types.fst = ltlprog; Types.snd =
978  (Joint.stack_cost (Joint.graph_params_to_params LTL.lTL) ltlprog) };
979  Types.snd =
980  (Nat.minus
981    (Exp.exp (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
982      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
983      Nat.O)))))))))))))))))
984    (Joint.globals_stacksize (Joint.graph_params_to_params LTL.lTL) ltlprog)) }
985
Note: See TracBrowser for help on using the repository browser.