source: extracted/liveness.ml @ 3001

Last change on this file since 3001 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: 15.1 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 (x, nparams, x0) ->
259     { Types.fst = Set_adt.set_empty; Types.snd =
260       (Set_adt.set_from_list
261         (Util.prefix (Obj.magic nparams) I8051.registerParams)) }
262   | Joint.COND (r, lbl_true) -> Obj.magic (rl_psingleton (Obj.magic r))
263   | Joint.Step_seq s0 ->
264     (match s0 with
265      | Joint.COMMENT x -> Obj.magic rl_bottom
266      | Joint.MOVE pair_reg ->
267        let r2 = (Obj.magic pair_reg).Types.snd in
268        (match r2 with
269         | Joint.Reg p ->
270           (match p with
271            | ERTL.PSD r -> Obj.magic (rl_psingleton r)
272            | ERTL.HDW r -> Obj.magic (rl_hsingleton r))
273         | Joint.Imm x -> Obj.magic rl_bottom)
274      | Joint.POP x -> Obj.magic rl_bottom
275      | Joint.PUSH r -> Obj.magic (rl_arg (Obj.magic r))
276      | Joint.ADDRESS (x, x1, x2) -> Obj.magic rl_bottom
277      | Joint.OPACCS (opaccs, dr1, dr2, sr1, sr2) ->
278        Obj.magic (rl_join (rl_arg (Obj.magic sr1)) (rl_arg (Obj.magic sr2)))
279      | Joint.OP1 (op1, r1, r2) -> Obj.magic (rl_psingleton (Obj.magic r2))
280      | Joint.OP2 (op2, acc_a, r1, r2) ->
281        Obj.magic
282          (rl_join (rl_join (rl_arg (Obj.magic r1)) (rl_arg (Obj.magic r2)))
283            (match op2 with
284             | BackEndOps.Add -> rl_bottom
285             | BackEndOps.Addc -> rl_hsingleton I8051.RegisterCarry
286             | BackEndOps.Sub -> rl_hsingleton I8051.RegisterCarry
287             | BackEndOps.And -> rl_bottom
288             | BackEndOps.Or -> rl_bottom
289             | BackEndOps.Xor -> rl_bottom))
290      | Joint.CLEAR_CARRY -> Obj.magic rl_bottom
291      | Joint.SET_CARRY -> Obj.magic rl_bottom
292      | Joint.LOAD (acc_a, dpl, dph) ->
293        Obj.magic (rl_join (rl_arg (Obj.magic dpl)) (rl_arg (Obj.magic dph)))
294      | Joint.STORE (acc_a, dpl, dph) ->
295        Obj.magic
296          (rl_join
297            (rl_join (rl_arg (Obj.magic acc_a)) (rl_arg (Obj.magic dpl)))
298            (rl_arg (Obj.magic dph)))
299      | Joint.Extension_seq ext ->
300        (match Obj.magic ext with
301         | ERTLptr.Ertlptr_ertl ext' ->
302           (match ext' with
303            | ERTL.Ertl_new_frame ->
304              Obj.magic
305                (rl_join (rl_hsingleton I8051.registerSPL)
306                  (rl_hsingleton I8051.registerSPH))
307            | ERTL.Ertl_del_frame ->
308              Obj.magic
309                (rl_join (rl_hsingleton I8051.registerSPL)
310                  (rl_hsingleton I8051.registerSPH))
311            | ERTL.Ertl_frame_size r -> Obj.magic rl_bottom)
312         | ERTLptr.LOW_ADDRESS (r1, l0) -> Obj.magic rl_bottom
313         | ERTLptr.HIGH_ADDRESS (r1, l0) -> Obj.magic rl_bottom)))
314| Joint.Final fin ->
315  (match fin with
316   | Joint.GOTO l -> Obj.magic rl_bottom
317   | Joint.RETURN ->
318     { Types.fst = Set_adt.set_empty; Types.snd =
319       (Set_adt.set_union (Set_adt.set_from_list I8051.registerCalleeSaved)
320         ret_regs) }
321   | Joint.TAILCALL (x, x0) -> assert false (* absurd case *))
322| Joint.FCOND (x, x0, x1) -> assert false (* absurd case *)
323
324(** val eliminable_step :
325    AST.ident List.list -> __ -> Joint.joint_step -> Bool.bool **)
326let eliminable_step globals l s =
327  let pliveafter = (Obj.magic l).Types.fst in
328  let hliveafter = (Obj.magic l).Types.snd in
329  (match s with
330   | Joint.COST_LABEL x -> Bool.False
331   | Joint.CALL (x, x0, x1) -> Bool.False
332   | Joint.COND (x, x0) -> Bool.False
333   | Joint.Step_seq s0 ->
334     (match s0 with
335      | Joint.COMMENT x -> Bool.False
336      | Joint.MOVE pair_reg ->
337        Bool.notb
338          (match (Obj.magic pair_reg).Types.fst with
339           | ERTL.PSD p1 ->
340             Set_adt.set_member
341               (Identifiers.eq_identifier PreIdentifiers.RegisterTag) p1
342               pliveafter
343           | ERTL.HDW h1 ->
344             Set_adt.set_member I8051.eq_Register h1 hliveafter)
345      | Joint.POP x -> Bool.False
346      | Joint.PUSH x -> Bool.False
347      | Joint.ADDRESS (x, r1, r2) ->
348        Bool.notb
349          (Bool.orb
350            (Set_adt.set_member
351              (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
352              (Obj.magic r1) pliveafter)
353            (Set_adt.set_member
354              (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
355              (Obj.magic r2) pliveafter))
356      | Joint.OPACCS (opaccs, dr1, dr2, sr1, sr2) ->
357        Bool.notb
358          (Bool.orb
359            (Bool.orb
360              (Set_adt.set_member
361                (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
362                (Obj.magic dr1) pliveafter)
363              (Set_adt.set_member
364                (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
365                (Obj.magic dr2) pliveafter))
366            (Set_adt.set_member I8051.eq_Register I8051.RegisterCarry
367              hliveafter))
368      | Joint.OP1 (op1, r1, r2) ->
369        Bool.notb
370          (Set_adt.set_member
371            (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
372            (Obj.magic r1) pliveafter)
373      | Joint.OP2 (op2, r1, r2, r3) ->
374        Bool.notb
375          (Bool.orb
376            (match op2 with
377             | BackEndOps.Add ->
378               Set_adt.set_member I8051.eq_Register I8051.RegisterCarry
379                 hliveafter
380             | BackEndOps.Addc ->
381               Set_adt.set_member I8051.eq_Register I8051.RegisterCarry
382                 hliveafter
383             | BackEndOps.Sub ->
384               Set_adt.set_member I8051.eq_Register I8051.RegisterCarry
385                 hliveafter
386             | BackEndOps.And -> Bool.False
387             | BackEndOps.Or -> Bool.False
388             | BackEndOps.Xor -> Bool.False)
389            (Set_adt.set_member
390              (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
391              (Obj.magic r1) pliveafter))
392      | Joint.CLEAR_CARRY -> Bool.False
393      | Joint.SET_CARRY -> Bool.False
394      | Joint.LOAD (acc_a, dpl, dph) ->
395        Bool.notb
396          (Set_adt.set_member
397            (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
398            (Obj.magic acc_a) pliveafter)
399      | Joint.STORE (x, x0, x1) -> Bool.False
400      | Joint.Extension_seq ext ->
401        (match Obj.magic ext with
402         | ERTLptr.Ertlptr_ertl ext' ->
403           (match ext' with
404            | ERTL.Ertl_new_frame -> Bool.False
405            | ERTL.Ertl_del_frame -> Bool.False
406            | ERTL.Ertl_frame_size r ->
407              Bool.notb
408                (Set_adt.set_member
409                  (Identifiers.eq_identifier PreIdentifiers.RegisterTag) r
410                  pliveafter))
411         | ERTLptr.LOW_ADDRESS (r1, l') ->
412           Bool.notb
413             (Set_adt.set_member
414               (Identifiers.eq_identifier PreIdentifiers.RegisterTag) r1
415               pliveafter)
416         | ERTLptr.HIGH_ADDRESS (r1, l') ->
417           Bool.notb
418             (Set_adt.set_member
419               (Identifiers.eq_identifier PreIdentifiers.RegisterTag) r1
420               pliveafter))))
421
422(** val eliminable :
423    AST.ident List.list -> __ -> Joint.joint_statement -> Bool.bool **)
424let eliminable globals l s =
425  let pliveafter = (Obj.magic l).Types.fst in
426  let hliveafter = (Obj.magic l).Types.snd in
427  (match s with
428   | Joint.Sequential (seq, x) -> eliminable_step globals l seq
429   | Joint.Final x -> Bool.False
430   | Joint.FCOND (x0, x1, x2) -> Bool.False)
431
432(** val statement_semantics :
433    AST.ident List.list -> Joint.joint_statement -> __ -> __ **)
434let statement_semantics globals stmt liveafter =
435  match eliminable globals liveafter stmt with
436  | Bool.True -> liveafter
437  | Bool.False ->
438    rl_join (rl_diff liveafter (defined globals stmt))
439      (Obj.magic (used globals stmt))
440
441(** val livebefore :
442    AST.ident List.list -> Joint.joint_internal_function ->
443    Fixpoints.valuation -> Fixpoints.valuation **)
444let livebefore globals int_fun liveafter label =
445  match Identifiers.lookup PreIdentifiers.LabelTag
446          (Obj.magic int_fun.Joint.joint_if_code) label with
447  | Types.None -> rl_bottom
448  | Types.Some stmt -> statement_semantics globals stmt (liveafter label)
449
450(** val liveafter :
451    AST.ident List.list -> Joint.joint_internal_function ->
452    PreIdentifiers.identifier -> Fixpoints.valuation -> __ **)
453let liveafter globals int_fun label liveafter0 =
454  match Identifiers.lookup PreIdentifiers.LabelTag
455          (Obj.magic int_fun.Joint.joint_if_code) label with
456  | Types.None -> rl_bottom
457  | Types.Some stmt ->
458    List.fold rl_join rl_bottom (fun successor -> Bool.True)
459      (fun successor -> livebefore globals int_fun liveafter0 successor)
460      (Joint.stmt_labels { Joint.uns_pars = (Joint.g_u_pars ERTLptr.eRTLptr);
461        Joint.succ_label = (Obj.magic (fun x -> Types.Some x));
462        Joint.has_fcond = Bool.False } globals stmt)
463
464(** val analyse_liveness :
465    Fixpoints.fixpoint_computer -> AST.ident List.list ->
466    Joint.joint_internal_function -> Fixpoints.fixpoint **)
467let analyse_liveness the_fixpoint globals int_fun =
468  the_fixpoint register_lattice (liveafter globals int_fun)
469
470type vertex = (Registers.register, I8051.register) Types.sum
471
472(** val plives : Registers.register -> __ -> Bool.bool **)
473let plives vertex0 prop =
474  Set_adt.set_member (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
475    vertex0 (Obj.magic prop).Types.fst
476
477(** val hlives : I8051.register -> __ -> Bool.bool **)
478let hlives vertex0 prop =
479  Set_adt.set_member I8051.eq_Register vertex0 (Obj.magic prop).Types.snd
480
481(** val lives : vertex -> __ -> Bool.bool **)
482let lives = function
483| Types.Inl v -> plives v
484| Types.Inr v -> hlives v
485
Note: See TracBrowser for help on using the repository browser.