source: driver/extracted/liveness.ml @ 3106

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

New major extraction that should have solved all remaining issues.
As tests/PROBLEMI shows, we still have some bugs with:

a) initialization of global data (regression)
b) function pointers call
File size: 14.4 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 Set_adt
124
125open Fixpoints
126
127(** val rl_included :
128    (PreIdentifiers.identifier Set_adt.set, I8051.register Set_adt.set)
129    Types.prod -> (PreIdentifiers.identifier Set_adt.set, I8051.register
130    Set_adt.set) Types.prod -> Bool.bool **)
131let rl_included left right =
132  Bool.andb
133    (Set_adt.set_subset
134      (Identifiers.eq_identifier PreIdentifiers.RegisterTag) left.Types.fst
135      right.Types.fst)
136    (Set_adt.set_subset I8051.eq_Register left.Types.snd right.Types.snd)
137
138(** val register_lattice : Fixpoints.property_lattice **)
139let register_lattice =
140  { Fixpoints.l_bottom =
141    (Obj.magic { Types.fst = Set_adt.set_empty; Types.snd =
142      Set_adt.set_empty }); Fixpoints.l_equal = (fun left right ->
143    Bool.andb
144      (Set_adt.set_equal
145        (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
146        (Obj.magic left).Types.fst (Obj.magic right).Types.fst)
147      (Set_adt.set_equal I8051.eq_Register (Obj.magic left).Types.snd
148        (Obj.magic right).Types.snd)); Fixpoints.l_included =
149    (Obj.magic rl_included); Fixpoints.l_is_maximal = (fun x -> Bool.False) }
150
151(** val rl_bottom : __ **)
152let rl_bottom =
153  register_lattice.Fixpoints.l_bottom
154
155(** val rl_psingleton : Registers.register -> __ **)
156let rl_psingleton r =
157  Obj.magic { Types.fst = (Set_adt.set_singleton r); Types.snd =
158    Set_adt.set_empty }
159
160(** val rl_hsingleton : I8051.register -> __ **)
161let rl_hsingleton r =
162  Obj.magic { Types.fst = Set_adt.set_empty; Types.snd =
163    (Set_adt.set_singleton r) }
164
165(** val pairwise :
166    ('a1 -> 'a1 -> 'a1) -> ('a2 -> 'a2 -> 'a2) -> ('a1, 'a2) Types.prod ->
167    ('a1, 'a2) Types.prod -> ('a1, 'a2) Types.prod **)
168let pairwise f g c1 c2 =
169  { Types.fst = (f c1.Types.fst c2.Types.fst); Types.snd =
170    (g c1.Types.snd c2.Types.snd) }
171
172(** val rl_join : __ -> __ -> __ **)
173let rl_join =
174  Obj.magic (pairwise Set_adt.set_union Set_adt.set_union)
175
176(** val rl_diff : __ -> __ -> __ **)
177let rl_diff =
178  Obj.magic (pairwise Set_adt.set_diff Set_adt.set_diff)
179
180(** val defined : AST.ident List.list -> Joint.joint_statement -> __ **)
181let defined globals = function
182| Joint.Sequential (seq, l) ->
183  (match seq with
184   | Joint.COST_LABEL clabel -> rl_bottom
185   | Joint.CALL (x, x0, x1) ->
186     Obj.magic { Types.fst = Set_adt.set_empty; Types.snd =
187       (Set_adt.set_from_list I8051.registerCallerSaved) }
188   | Joint.COND (r, lbl_true) -> rl_bottom
189   | Joint.Step_seq s0 ->
190     (match s0 with
191      | Joint.COMMENT c -> rl_bottom
192      | Joint.MOVE pair_reg ->
193        (match (Obj.magic pair_reg).Types.fst with
194         | ERTL.PSD p -> rl_psingleton p
195         | ERTL.HDW h -> rl_hsingleton h)
196      | Joint.POP r -> rl_psingleton (Obj.magic r)
197      | Joint.PUSH r -> rl_bottom
198      | Joint.ADDRESS (x, x1, r1, r2) ->
199        rl_join (rl_psingleton (Obj.magic r1)) (rl_psingleton (Obj.magic r2))
200      | Joint.OPACCS (opaccs, dr1, dr2, sr1, sr2) ->
201        rl_join
202          (rl_join (rl_psingleton (Obj.magic dr1))
203            (rl_psingleton (Obj.magic dr2)))
204          (rl_hsingleton I8051.RegisterCarry)
205      | Joint.OP1 (op1, r1, r2) -> rl_psingleton (Obj.magic r1)
206      | Joint.OP2 (op2, r1, r2, x) ->
207        (match op2 with
208         | BackEndOps.Add ->
209           rl_join (rl_hsingleton I8051.RegisterCarry)
210             (rl_psingleton (Obj.magic r1))
211         | BackEndOps.Addc ->
212           rl_join (rl_hsingleton I8051.RegisterCarry)
213             (rl_psingleton (Obj.magic r1))
214         | BackEndOps.Sub ->
215           rl_join (rl_hsingleton I8051.RegisterCarry)
216             (rl_psingleton (Obj.magic r1))
217         | BackEndOps.And -> rl_psingleton (Obj.magic r1)
218         | BackEndOps.Or -> rl_psingleton (Obj.magic r1)
219         | BackEndOps.Xor -> rl_psingleton (Obj.magic r1))
220      | Joint.CLEAR_CARRY -> rl_hsingleton I8051.RegisterCarry
221      | Joint.SET_CARRY -> rl_hsingleton I8051.RegisterCarry
222      | Joint.LOAD (r, x, x0) -> rl_psingleton (Obj.magic r)
223      | Joint.STORE (acc_a, dpl, dph) -> rl_bottom
224      | Joint.Extension_seq ext ->
225        (match Obj.magic ext with
226         | ERTL.Ertl_new_frame ->
227           rl_join (rl_hsingleton I8051.registerSPL)
228             (rl_hsingleton I8051.registerSPH)
229         | ERTL.Ertl_del_frame ->
230           rl_join (rl_hsingleton I8051.registerSPL)
231             (rl_hsingleton I8051.registerSPH)
232         | ERTL.Ertl_frame_size r -> rl_psingleton r)))
233| Joint.Final x -> rl_bottom
234| Joint.FCOND (x, x0, x1) -> assert false (* absurd case *)
235
236(** val ret_regs : I8051.register Set_adt.set **)
237let ret_regs =
238  Set_adt.set_from_list I8051.registerRets
239
240(** val rl_arg : Joint.psd_argument -> __ **)
241let rl_arg = function
242| Joint.Reg r -> rl_psingleton r
243| Joint.Imm x -> rl_bottom
244
245(** val used :
246    AST.ident List.list -> Joint.joint_statement -> (Registers.register
247    Set_adt.set, I8051.register Set_adt.set) Types.prod **)
248let used globals = function
249| Joint.Sequential (seq, l) ->
250  (match seq with
251   | Joint.COST_LABEL clabel -> Obj.magic rl_bottom
252   | Joint.CALL (f, nparams, x) ->
253     Obj.magic
254       (rl_join
255         (match f with
256          | Types.Inl x0 -> rl_bottom
257          | Types.Inr pr ->
258            rl_join (rl_arg (Obj.magic pr).Types.fst)
259              (rl_arg (Obj.magic pr).Types.snd))
260         (Obj.magic { Types.fst = Set_adt.set_empty; Types.snd =
261           (Set_adt.set_from_list
262             (Util.prefix (Obj.magic nparams) I8051.registerParams)) }))
263   | Joint.COND (r, lbl_true) -> Obj.magic (rl_psingleton (Obj.magic r))
264   | Joint.Step_seq s0 ->
265     (match s0 with
266      | Joint.COMMENT x -> Obj.magic rl_bottom
267      | Joint.MOVE pair_reg ->
268        let r2 = (Obj.magic pair_reg).Types.snd in
269        (match r2 with
270         | Joint.Reg p ->
271           (match p with
272            | ERTL.PSD r -> Obj.magic (rl_psingleton r)
273            | ERTL.HDW r -> Obj.magic (rl_hsingleton r))
274         | Joint.Imm x -> Obj.magic rl_bottom)
275      | Joint.POP x -> Obj.magic rl_bottom
276      | Joint.PUSH r -> Obj.magic (rl_arg (Obj.magic r))
277      | Joint.ADDRESS (x, x1, x2, x3) -> Obj.magic rl_bottom
278      | Joint.OPACCS (opaccs, dr1, dr2, sr1, sr2) ->
279        Obj.magic (rl_join (rl_arg (Obj.magic sr1)) (rl_arg (Obj.magic sr2)))
280      | Joint.OP1 (op1, r1, r2) -> Obj.magic (rl_psingleton (Obj.magic r2))
281      | Joint.OP2 (op2, acc_a, r1, r2) ->
282        Obj.magic
283          (rl_join (rl_join (rl_arg (Obj.magic r1)) (rl_arg (Obj.magic r2)))
284            (match op2 with
285             | BackEndOps.Add -> rl_bottom
286             | BackEndOps.Addc -> rl_hsingleton I8051.RegisterCarry
287             | BackEndOps.Sub -> rl_hsingleton I8051.RegisterCarry
288             | BackEndOps.And -> rl_bottom
289             | BackEndOps.Or -> rl_bottom
290             | BackEndOps.Xor -> rl_bottom))
291      | Joint.CLEAR_CARRY -> Obj.magic rl_bottom
292      | Joint.SET_CARRY -> Obj.magic rl_bottom
293      | Joint.LOAD (acc_a, dpl, dph) ->
294        Obj.magic (rl_join (rl_arg (Obj.magic dpl)) (rl_arg (Obj.magic dph)))
295      | Joint.STORE (acc_a, dpl, dph) ->
296        Obj.magic
297          (rl_join
298            (rl_join (rl_arg (Obj.magic acc_a)) (rl_arg (Obj.magic dpl)))
299            (rl_arg (Obj.magic dph)))
300      | Joint.Extension_seq ext ->
301        (match Obj.magic ext with
302         | ERTL.Ertl_new_frame ->
303           Obj.magic
304             (rl_join (rl_hsingleton I8051.registerSPL)
305               (rl_hsingleton I8051.registerSPH))
306         | ERTL.Ertl_del_frame ->
307           Obj.magic
308             (rl_join (rl_hsingleton I8051.registerSPL)
309               (rl_hsingleton I8051.registerSPH))
310         | ERTL.Ertl_frame_size r -> Obj.magic rl_bottom)))
311| Joint.Final fin ->
312  (match fin with
313   | Joint.GOTO l -> Obj.magic rl_bottom
314   | Joint.RETURN ->
315     { Types.fst = Set_adt.set_empty; Types.snd =
316       (Set_adt.set_union (Set_adt.set_from_list I8051.registerCalleeSaved)
317         ret_regs) }
318   | Joint.TAILCALL (x, x0) -> assert false (* absurd case *))
319| Joint.FCOND (x, x0, x1) -> assert false (* absurd case *)
320
321(** val eliminable_step :
322    AST.ident List.list -> __ -> Joint.joint_step -> Bool.bool **)
323let eliminable_step globals l s =
324  let pliveafter = (Obj.magic l).Types.fst in
325  let hliveafter = (Obj.magic l).Types.snd in
326  (match s with
327   | Joint.COST_LABEL x -> Bool.False
328   | Joint.CALL (x, x0, x1) -> Bool.False
329   | Joint.COND (x, x0) -> Bool.False
330   | Joint.Step_seq s0 ->
331     (match s0 with
332      | Joint.COMMENT x -> Bool.False
333      | Joint.MOVE pair_reg ->
334        Bool.notb
335          (match (Obj.magic pair_reg).Types.fst with
336           | ERTL.PSD p1 ->
337             Set_adt.set_member
338               (Identifiers.eq_identifier PreIdentifiers.RegisterTag) p1
339               pliveafter
340           | ERTL.HDW h1 ->
341             Set_adt.set_member I8051.eq_Register h1 hliveafter)
342      | Joint.POP x -> Bool.False
343      | Joint.PUSH x -> Bool.False
344      | Joint.ADDRESS (x, x1, r1, r2) ->
345        Bool.notb
346          (Bool.orb
347            (Set_adt.set_member
348              (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
349              (Obj.magic r1) pliveafter)
350            (Set_adt.set_member
351              (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
352              (Obj.magic r2) pliveafter))
353      | Joint.OPACCS (opaccs, dr1, dr2, sr1, sr2) ->
354        Bool.notb
355          (Bool.orb
356            (Bool.orb
357              (Set_adt.set_member
358                (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
359                (Obj.magic dr1) pliveafter)
360              (Set_adt.set_member
361                (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
362                (Obj.magic dr2) pliveafter))
363            (Set_adt.set_member I8051.eq_Register I8051.RegisterCarry
364              hliveafter))
365      | Joint.OP1 (op1, r1, r2) ->
366        Bool.notb
367          (Set_adt.set_member
368            (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
369            (Obj.magic r1) pliveafter)
370      | Joint.OP2 (op2, r1, r2, r3) ->
371        Bool.notb
372          (Bool.orb
373            (match op2 with
374             | BackEndOps.Add ->
375               Set_adt.set_member I8051.eq_Register I8051.RegisterCarry
376                 hliveafter
377             | BackEndOps.Addc ->
378               Set_adt.set_member I8051.eq_Register I8051.RegisterCarry
379                 hliveafter
380             | BackEndOps.Sub ->
381               Set_adt.set_member I8051.eq_Register I8051.RegisterCarry
382                 hliveafter
383             | BackEndOps.And -> Bool.False
384             | BackEndOps.Or -> Bool.False
385             | BackEndOps.Xor -> Bool.False)
386            (Set_adt.set_member
387              (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
388              (Obj.magic r1) pliveafter))
389      | Joint.CLEAR_CARRY -> Bool.False
390      | Joint.SET_CARRY -> Bool.False
391      | Joint.LOAD (acc_a, dpl, dph) ->
392        Bool.notb
393          (Set_adt.set_member
394            (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
395            (Obj.magic acc_a) pliveafter)
396      | Joint.STORE (x, x0, x1) -> Bool.False
397      | Joint.Extension_seq ext ->
398        (match Obj.magic ext with
399         | ERTL.Ertl_new_frame -> Bool.False
400         | ERTL.Ertl_del_frame -> Bool.False
401         | ERTL.Ertl_frame_size r ->
402           Bool.notb
403             (Set_adt.set_member
404               (Identifiers.eq_identifier PreIdentifiers.RegisterTag) r
405               pliveafter))))
406
407(** val eliminable :
408    AST.ident List.list -> __ -> Joint.joint_statement -> Bool.bool **)
409let eliminable globals l s =
410  let pliveafter = (Obj.magic l).Types.fst in
411  let hliveafter = (Obj.magic l).Types.snd in
412  (match s with
413   | Joint.Sequential (seq, x) -> eliminable_step globals l seq
414   | Joint.Final x -> Bool.False
415   | Joint.FCOND (x0, x1, x2) -> Bool.False)
416
417(** val statement_semantics :
418    AST.ident List.list -> Joint.joint_statement -> __ -> __ **)
419let statement_semantics globals stmt liveafter =
420  match eliminable globals liveafter stmt with
421  | Bool.True -> liveafter
422  | Bool.False ->
423    rl_join (rl_diff liveafter (defined globals stmt))
424      (Obj.magic (used globals stmt))
425
426(** val livebefore :
427    AST.ident List.list -> Joint.joint_internal_function ->
428    Fixpoints.valuation -> Fixpoints.valuation **)
429let livebefore globals int_fun liveafter label =
430  match Identifiers.lookup PreIdentifiers.LabelTag
431          (Obj.magic int_fun.Joint.joint_if_code) label with
432  | Types.None -> rl_bottom
433  | Types.Some stmt -> statement_semantics globals stmt (liveafter label)
434
435(** val liveafter :
436    AST.ident List.list -> Joint.joint_internal_function ->
437    PreIdentifiers.identifier -> Fixpoints.valuation -> __ **)
438let liveafter globals int_fun label liveafter0 =
439  match Identifiers.lookup PreIdentifiers.LabelTag
440          (Obj.magic int_fun.Joint.joint_if_code) label with
441  | Types.None -> rl_bottom
442  | Types.Some stmt ->
443    List.fold rl_join rl_bottom (fun successor -> Bool.True)
444      (fun successor -> livebefore globals int_fun liveafter0 successor)
445      (Joint.stmt_labels { Joint.uns_pars = (Joint.g_u_pars ERTL.eRTL);
446        Joint.succ_label = (Obj.magic (fun x -> Types.Some x));
447        Joint.has_fcond = Bool.False } globals stmt)
448
449(** val analyse_liveness :
450    Fixpoints.fixpoint_computer -> AST.ident List.list ->
451    Joint.joint_internal_function -> Fixpoints.fixpoint **)
452let analyse_liveness the_fixpoint globals int_fun =
453  the_fixpoint register_lattice (liveafter globals int_fun)
454
455type vertex = (Registers.register, I8051.register) Types.sum
456
457(** val plives : Registers.register -> __ -> Bool.bool **)
458let plives vertex0 prop =
459  Set_adt.set_member (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
460    vertex0 (Obj.magic prop).Types.fst
461
462(** val hlives : I8051.register -> __ -> Bool.bool **)
463let hlives vertex0 prop =
464  Set_adt.set_member I8051.eq_Register vertex0 (Obj.magic prop).Types.snd
465
466(** val lives : vertex -> __ -> Bool.bool **)
467let lives = function
468| Types.Inl v -> plives v
469| Types.Inr v -> hlives v
470
Note: See TracBrowser for help on using the repository browser.