source: extracted/liveness.ml @ 3009

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

New extraction.

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