source: extracted/liveness.ml @ 2746

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

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

File size: 15.9 KB
Line 
1open Preamble
2
3open Div_and_mod
4
5open Jmeq
6
7open Russell
8
9open Bool
10
11open Relations
12
13open Nat
14
15open Hints_declaration
16
17open Core_notation
18
19open Pts
20
21open Logic
22
23open Types
24
25open List
26
27open Util
28
29open String
30
31open Sets
32
33open Listb
34
35open LabelledObjects
36
37open Graphs
38
39open I8051
40
41open Order
42
43open Registers
44
45open BitVectorTrie
46
47open CostLabel
48
49open Hide
50
51open Proper
52
53open PositiveMap
54
55open Deqsets
56
57open ErrorMessages
58
59open PreIdentifiers
60
61open Errors
62
63open Extralib
64
65open Setoids
66
67open Monad
68
69open Option
70
71open Lists
72
73open Identifiers
74
75open Integers
76
77open AST
78
79open Division
80
81open Exp
82
83open Arithmetic
84
85open Extranat
86
87open Vector
88
89open FoldStuff
90
91open BitVector
92
93open Positive
94
95open Z
96
97open BitVectorZ
98
99open Pointers
100
101open ByteValues
102
103open BackEndOps
104
105open Joint
106
107open ERTL
108
109open ERTLptr
110
111open Set_adt
112
113open Fixpoints
114
115(** val register_lattice : Fixpoints.property_lattice **)
116let register_lattice =
117  { Fixpoints.l_bottom =
118    (Obj.magic { Types.fst = Set_adt.set_empty; Types.snd =
119      Set_adt.set_empty }); Fixpoints.l_equal = (fun left right ->
120    Bool.andb
121      (Set_adt.set_equal
122        (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
123        (Obj.magic left).Types.fst (Obj.magic right).Types.fst)
124      (Set_adt.set_equal I8051.eq_Register (Obj.magic left).Types.snd
125        (Obj.magic right).Types.snd)); Fixpoints.l_included =
126    (fun left right ->
127    Bool.andb
128      (Set_adt.set_subset
129        (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
130        (Obj.magic left).Types.fst (Obj.magic right).Types.fst)
131      (Set_adt.set_subset I8051.eq_Register (Obj.magic left).Types.snd
132        (Obj.magic right).Types.snd)); Fixpoints.l_is_maximal = (fun x ->
133    Bool.False) }
134
135(** val rl_bottom : __ **)
136let rl_bottom =
137  register_lattice.Fixpoints.l_bottom
138
139(** val rl_psingleton : Registers.register -> __ **)
140let rl_psingleton r =
141  Obj.magic { Types.fst = (Set_adt.set_singleton r); Types.snd =
142    Set_adt.set_empty }
143
144(** val rl_hsingleton : I8051.register -> __ **)
145let rl_hsingleton r =
146  Obj.magic { Types.fst = Set_adt.set_empty; Types.snd =
147    (Set_adt.set_singleton r) }
148
149(** val rl_join : __ -> __ -> __ **)
150let rl_join left right =
151  let { Types.fst = lp; Types.snd = lh } = Obj.magic left in
152  let { Types.fst = rp; Types.snd = rh } = Obj.magic right in
153  Obj.magic { Types.fst = (Set_adt.set_union lp rp); Types.snd =
154    (Set_adt.set_union lh rh) }
155
156(** val rl_diff : __ -> __ -> __ **)
157let rl_diff left right =
158  let { Types.fst = lp; Types.snd = lh } = Obj.magic left in
159  let { Types.fst = rp; Types.snd = rh } = Obj.magic right in
160  Obj.magic { Types.fst = (Set_adt.set_diff lp rp); Types.snd =
161    (Set_adt.set_diff lh rh) }
162
163(** val defined : AST.ident List.list -> Joint.joint_statement -> __ **)
164let defined globals = function
165| Joint.Sequential (seq, l) ->
166  (match seq with
167   | Joint.COST_LABEL clabel -> rl_bottom
168   | Joint.CALL (x, x0, x1) ->
169     Obj.magic { Types.fst = Set_adt.set_empty; Types.snd =
170       (Set_adt.set_from_list I8051.registerCallerSaved) }
171   | Joint.COND (r, lbl_true) -> rl_bottom
172   | Joint.Step_seq s0 ->
173     (match s0 with
174      | Joint.COMMENT c -> rl_bottom
175      | Joint.MOVE pair_reg ->
176        (match (Obj.magic pair_reg).Types.fst with
177         | ERTL.PSD p -> rl_psingleton p
178         | ERTL.HDW h -> rl_hsingleton h)
179      | Joint.POP r -> rl_psingleton (Obj.magic r)
180      | Joint.PUSH r -> rl_bottom
181      | Joint.ADDRESS (x, r5, r6) ->
182        rl_join (rl_psingleton (Obj.magic r5)) (rl_psingleton (Obj.magic r6))
183      | Joint.OPACCS (opaccs0, dr1, dr2, sr1, sr2) ->
184        rl_join
185          (rl_join (rl_psingleton (Obj.magic dr1))
186            (rl_psingleton (Obj.magic dr2)))
187          (rl_hsingleton I8051.RegisterCarry)
188      | Joint.OP1 (op4, r5, r6) -> rl_psingleton (Obj.magic r5)
189      | Joint.OP2 (op4, r5, r6, x) ->
190        (match op4 with
191         | BackEndOps.Add ->
192           rl_join (rl_hsingleton I8051.RegisterCarry)
193             (rl_psingleton (Obj.magic r5))
194         | BackEndOps.Addc ->
195           rl_join (rl_hsingleton I8051.RegisterCarry)
196             (rl_psingleton (Obj.magic r5))
197         | BackEndOps.Sub ->
198           rl_join (rl_hsingleton I8051.RegisterCarry)
199             (rl_psingleton (Obj.magic r5))
200         | BackEndOps.And -> rl_psingleton (Obj.magic r5)
201         | BackEndOps.Or -> rl_psingleton (Obj.magic r5)
202         | BackEndOps.Xor -> rl_psingleton (Obj.magic r5))
203      | Joint.CLEAR_CARRY -> rl_hsingleton I8051.RegisterCarry
204      | Joint.SET_CARRY -> rl_hsingleton I8051.RegisterCarry
205      | Joint.LOAD (r, x, x0) -> rl_psingleton (Obj.magic r)
206      | Joint.STORE (acc_a, dpl, dph) -> rl_bottom
207      | Joint.Extension_seq ext ->
208        (match Obj.magic ext with
209         | ERTLptr.Ertlptr_ertl ext' ->
210           (match ext' with
211            | ERTL.Ertl_new_frame ->
212              rl_join (rl_hsingleton I8051.registerSPL)
213                (rl_hsingleton I8051.registerSPH)
214            | ERTL.Ertl_del_frame ->
215              rl_join (rl_hsingleton I8051.registerSPL)
216                (rl_hsingleton I8051.registerSPH)
217            | ERTL.Ertl_frame_size r -> rl_psingleton r)
218         | ERTLptr.LOW_ADDRESS (r5, l0) -> rl_psingleton r5
219         | ERTLptr.HIGH_ADDRESS (r5, l0) -> rl_psingleton r5)))
220| Joint.Final x -> rl_bottom
221| Joint.FCOND (x, x0, x1) -> assert false (* absurd case *)
222
223(** val ret_regs : I8051.register Set_adt.set **)
224let ret_regs =
225  Set_adt.set_from_list I8051.registerRets
226
227(** val rl_arg : Joint.psd_argument -> __ **)
228let rl_arg = function
229| Joint.Reg r -> rl_psingleton r
230| Joint.Imm x -> rl_bottom
231
232(** val used :
233    AST.ident List.list -> Joint.joint_statement -> (Registers.register
234    Set_adt.set, I8051.register Set_adt.set) Types.prod **)
235let used globals = function
236| Joint.Sequential (seq, l) ->
237  (match seq with
238   | Joint.COST_LABEL clabel -> Obj.magic rl_bottom
239   | Joint.CALL (x, nparams, x0) ->
240     { Types.fst = Set_adt.set_empty; Types.snd =
241       (Set_adt.set_from_list
242         (Util.prefix (Obj.magic nparams) I8051.registerParams)) }
243   | Joint.COND (r, lbl_true) -> Obj.magic (rl_psingleton (Obj.magic r))
244   | Joint.Step_seq s0 ->
245     (match s0 with
246      | Joint.COMMENT x -> Obj.magic rl_bottom
247      | Joint.MOVE pair_reg ->
248        let r5 = (Obj.magic pair_reg).Types.snd in
249        (match r5 with
250         | Joint.Reg p ->
251           (match p with
252            | ERTL.PSD r -> Obj.magic (rl_psingleton r)
253            | ERTL.HDW r -> Obj.magic (rl_hsingleton r))
254         | Joint.Imm x -> Obj.magic rl_bottom)
255      | Joint.POP x -> Obj.magic rl_bottom
256      | Joint.PUSH r -> Obj.magic (rl_arg (Obj.magic r))
257      | Joint.ADDRESS (x, x1, x2) -> Obj.magic rl_bottom
258      | Joint.OPACCS (opaccs0, dr1, dr2, sr1, sr2) ->
259        Obj.magic (rl_join (rl_arg (Obj.magic sr1)) (rl_arg (Obj.magic sr2)))
260      | Joint.OP1 (op4, r5, r6) -> Obj.magic (rl_psingleton (Obj.magic r6))
261      | Joint.OP2 (op4, acc_a, r5, r6) ->
262        Obj.magic
263          (rl_join (rl_join (rl_arg (Obj.magic r5)) (rl_arg (Obj.magic r6)))
264            (match op4 with
265             | BackEndOps.Add -> rl_bottom
266             | BackEndOps.Addc -> rl_hsingleton I8051.RegisterCarry
267             | BackEndOps.Sub -> rl_hsingleton I8051.RegisterCarry
268             | BackEndOps.And -> rl_bottom
269             | BackEndOps.Or -> rl_bottom
270             | BackEndOps.Xor -> rl_bottom))
271      | Joint.CLEAR_CARRY -> Obj.magic rl_bottom
272      | Joint.SET_CARRY -> Obj.magic rl_bottom
273      | Joint.LOAD (acc_a, dpl, dph) ->
274        Obj.magic (rl_join (rl_arg (Obj.magic dpl)) (rl_arg (Obj.magic dph)))
275      | Joint.STORE (acc_a, dpl, dph) ->
276        Obj.magic
277          (rl_join
278            (rl_join (rl_arg (Obj.magic acc_a)) (rl_arg (Obj.magic dpl)))
279            (rl_arg (Obj.magic dph)))
280      | Joint.Extension_seq ext ->
281        (match Obj.magic ext with
282         | ERTLptr.Ertlptr_ertl ext' ->
283           (match ext' with
284            | ERTL.Ertl_new_frame ->
285              Obj.magic
286                (rl_join (rl_hsingleton I8051.registerSPL)
287                  (rl_hsingleton I8051.registerSPH))
288            | ERTL.Ertl_del_frame ->
289              Obj.magic
290                (rl_join (rl_hsingleton I8051.registerSPL)
291                  (rl_hsingleton I8051.registerSPH))
292            | ERTL.Ertl_frame_size r -> Obj.magic rl_bottom)
293         | ERTLptr.LOW_ADDRESS (r5, l0) -> Obj.magic rl_bottom
294         | ERTLptr.HIGH_ADDRESS (r5, l0) -> Obj.magic rl_bottom)))
295| Joint.Final fin ->
296  (match fin with
297   | Joint.GOTO l -> Obj.magic rl_bottom
298   | Joint.RETURN ->
299     { Types.fst = Set_adt.set_empty; Types.snd =
300       (Set_adt.set_union (Set_adt.set_from_list I8051.registerCalleeSaved)
301         ret_regs) }
302   | Joint.TAILCALL (x, x0) -> assert false (* absurd case *))
303| Joint.FCOND (x, x0, x1) -> assert false (* absurd case *)
304
305(** val eliminable :
306    AST.ident List.list -> __ -> Joint.joint_statement -> __ Types.option **)
307let eliminable globals l s =
308  let pliveafter = (Obj.magic l).Types.fst in
309  let hliveafter = (Obj.magic l).Types.snd in
310  (match s with
311   | Joint.Sequential (seq, l0) ->
312     (match seq with
313      | Joint.COST_LABEL x -> Types.None
314      | Joint.CALL (x, x0, x1) -> Types.None
315      | Joint.COND (x, x0) -> Types.None
316      | Joint.Step_seq s0 ->
317        (match s0 with
318         | Joint.COMMENT x -> Types.None
319         | Joint.MOVE pair_reg ->
320           (match match (Obj.magic pair_reg).Types.fst with
321                  | ERTL.PSD p3 ->
322                    Set_adt.set_member
323                      (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
324                      p3 pliveafter
325                  | ERTL.HDW h1 ->
326                    Set_adt.set_member I8051.eq_Register h1 hliveafter with
327            | Bool.True -> Types.None
328            | Bool.False -> Types.Some l0)
329         | Joint.POP x -> Types.None
330         | Joint.PUSH x -> Types.None
331         | Joint.ADDRESS (x, r5, r6) ->
332           (match Bool.orb
333                    (Set_adt.set_member
334                      (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
335                      (Obj.magic r5) pliveafter)
336                    (Set_adt.set_member
337                      (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
338                      (Obj.magic r6) pliveafter) with
339            | Bool.True -> Types.None
340            | Bool.False -> Types.Some l0)
341         | Joint.OPACCS (opaccs0, dr1, dr2, sr1, sr2) ->
342           (match Bool.orb
343                    (Bool.orb
344                      (Set_adt.set_member
345                        (Identifiers.eq_identifier
346                          PreIdentifiers.RegisterTag) (Obj.magic dr1)
347                        pliveafter)
348                      (Set_adt.set_member
349                        (Identifiers.eq_identifier
350                          PreIdentifiers.RegisterTag) (Obj.magic dr2)
351                        pliveafter))
352                    (Set_adt.set_member I8051.eq_Register I8051.RegisterCarry
353                      hliveafter) with
354            | Bool.True -> Types.None
355            | Bool.False -> Types.Some l0)
356         | Joint.OP1 (op4, r5, r6) ->
357           (match Set_adt.set_member
358                    (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
359                    (Obj.magic r5) pliveafter with
360            | Bool.True -> Types.None
361            | Bool.False -> Types.Some l0)
362         | Joint.OP2 (op4, r5, r6, r7) ->
363           (match Bool.orb
364                    (match op4 with
365                     | BackEndOps.Add ->
366                       Set_adt.set_member I8051.eq_Register
367                         I8051.RegisterCarry hliveafter
368                     | BackEndOps.Addc ->
369                       Set_adt.set_member I8051.eq_Register
370                         I8051.RegisterCarry hliveafter
371                     | BackEndOps.Sub ->
372                       Set_adt.set_member I8051.eq_Register
373                         I8051.RegisterCarry hliveafter
374                     | BackEndOps.And -> Bool.False
375                     | BackEndOps.Or -> Bool.False
376                     | BackEndOps.Xor -> Bool.False)
377                    (Set_adt.set_member
378                      (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
379                      (Obj.magic r5) pliveafter) with
380            | Bool.True -> Types.None
381            | Bool.False -> Types.Some l0)
382         | Joint.CLEAR_CARRY -> Types.None
383         | Joint.SET_CARRY -> Types.None
384         | Joint.LOAD (acc_a, dpl, dph) ->
385           (match Set_adt.set_member
386                    (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
387                    (Obj.magic acc_a) pliveafter with
388            | Bool.True -> Types.None
389            | Bool.False -> Types.Some l0)
390         | Joint.STORE (x, x0, x1) -> Types.None
391         | Joint.Extension_seq ext ->
392           (match Obj.magic ext with
393            | ERTLptr.Ertlptr_ertl ext' ->
394              (match ext' with
395               | ERTL.Ertl_new_frame -> Types.None
396               | ERTL.Ertl_del_frame -> Types.None
397               | ERTL.Ertl_frame_size r ->
398                 (match Set_adt.set_member
399                          (Identifiers.eq_identifier
400                            PreIdentifiers.RegisterTag) r pliveafter with
401                  | Bool.True -> Types.None
402                  | Bool.False -> Types.Some l0))
403            | ERTLptr.LOW_ADDRESS (r5, l') ->
404              (match Set_adt.set_member
405                       (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
406                       r5 pliveafter with
407               | Bool.True -> Types.None
408               | Bool.False -> Types.Some l0)
409            | ERTLptr.HIGH_ADDRESS (r5, l') ->
410              (match Set_adt.set_member
411                       (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
412                       r5 pliveafter with
413               | Bool.True -> Types.None
414               | Bool.False -> Types.Some l0))))
415   | Joint.Final x -> Types.None
416   | Joint.FCOND (x0, x1, x2) -> Types.None)
417
418(** val statement_semantics :
419    AST.ident List.list -> Joint.joint_statement -> __ -> __ **)
420let statement_semantics globals stmt liveafter =
421  match eliminable globals liveafter stmt with
422  | Types.None ->
423    rl_join (rl_diff liveafter (defined globals stmt))
424      (Obj.magic (used globals stmt))
425  | Types.Some l -> liveafter
426
427(** val livebefore :
428    AST.ident List.list -> Joint.joint_internal_function ->
429    PreIdentifiers.identifier -> Fixpoints.valuation -> __ **)
430let livebefore globals int_fun label0 liveafter =
431  match Identifiers.lookup0 PreIdentifiers.LabelTag
432          (Obj.magic int_fun.Joint.joint_if_code) label0 with
433  | Types.None -> rl_bottom
434  | Types.Some stmt -> statement_semantics globals stmt (liveafter label0)
435
436(** val liveafter :
437    AST.ident List.list -> Joint.joint_internal_function ->
438    PreIdentifiers.identifier -> Fixpoints.valuation -> __ **)
439let liveafter globals int_fun label0 liveafter0 =
440  match Identifiers.lookup0 PreIdentifiers.LabelTag
441          (Obj.magic int_fun.Joint.joint_if_code) label0 with
442  | Types.None -> rl_bottom
443  | Types.Some stmt ->
444    List.fold rl_join rl_bottom (fun successor -> Bool.True)
445      (fun successor -> livebefore globals int_fun successor liveafter0)
446      (Joint.stmt_labels { Joint.uns_pars = (Joint.g_u_pars ERTLptr.eRTLptr);
447        Joint.succ_label = (Obj.magic (fun x -> Types.Some x));
448        Joint.has_fcond = Bool.False } globals stmt)
449
450(** val analyse_liveness :
451    Fixpoints.fixpoint_computer -> AST.ident List.list ->
452    Joint.joint_internal_function -> Fixpoints.valuation **)
453let analyse_liveness the_fixpoint globals int_fun =
454  Fixpoints.fix_lfp register_lattice (the_fixpoint register_lattice)
455    (liveafter globals int_fun)
456
457type vertex = (Registers.register, I8051.register) Types.sum
458
459(** val plives : Registers.register -> __ -> Bool.bool **)
460let plives vertex0 prop =
461  Set_adt.set_member (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
462    vertex0 (Obj.magic prop).Types.fst
463
464(** val hlives : I8051.register -> __ -> Bool.bool **)
465let hlives vertex0 prop =
466  Set_adt.set_member I8051.eq_Register vertex0 (Obj.magic prop).Types.snd
467
468(** val lives : vertex -> __ -> Bool.bool **)
469let lives = function
470| Types.Inl v -> plives v
471| Types.Inr v -> hlives v
472
Note: See TracBrowser for help on using the repository browser.