source: extracted/eRTLptrToLTL.ml @ 2717

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

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

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