source: extracted/eRTLptrToLTL.ml @ 2951

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

New extraction. Novely: a pre-main is used in the back-end. Initialization
of global data is performed in LINToASM.

Note: the cost-emission of the initialization costlabel in the front-end is
virtual, but not performed in the traces I generate and print. To be fixed
(how?)

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