15 open Hints_declaration
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 **)
131 let rl_included left right =
134 (Identifiers.eq_identifier PreIdentifiers.RegisterTag) left.Types.fst
136 (Set_adt.set_subset I8051.eq_Register left.Types.snd right.Types.snd)
138 (** val register_lattice : Fixpoints.property_lattice **)
139 let 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 ->
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) }
151 (** val rl_bottom : __ **)
153 register_lattice.Fixpoints.l_bottom
155 (** val rl_psingleton : Registers.register -> __ **)
156 let rl_psingleton r =
157 Obj.magic { Types.fst = (Set_adt.set_singleton r); Types.snd =
160 (** val rl_hsingleton : I8051.register -> __ **)
161 let rl_hsingleton r =
162 Obj.magic { Types.fst = Set_adt.set_empty; Types.snd =
163 (Set_adt.set_singleton r) }
166 ('a1 -> 'a1 -> 'a1) -> ('a2 -> 'a2 -> 'a2) -> ('a1, 'a2) Types.prod ->
167 ('a1, 'a2) Types.prod -> ('a1, 'a2) Types.prod **)
168 let 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) }
172 (** val rl_join : __ -> __ -> __ **)
174 Obj.magic (pairwise Set_adt.set_union Set_adt.set_union)
176 (** val rl_diff : __ -> __ -> __ **)
178 Obj.magic (pairwise Set_adt.set_diff Set_adt.set_diff)
180 (** val defined : AST.ident List.list -> Joint.joint_statement -> __ **)
181 let defined globals = function
182 | Joint.Sequential (seq, l) ->
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 ->
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) ->
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) ->
209 rl_join (rl_hsingleton I8051.RegisterCarry)
210 (rl_psingleton (Obj.magic r1))
212 rl_join (rl_hsingleton I8051.RegisterCarry)
213 (rl_psingleton (Obj.magic r1))
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 *)
236 (** val ret_regs : I8051.register Set_adt.set **)
238 Set_adt.set_from_list I8051.registerRets
240 (** val rl_arg : Joint.psd_argument -> __ **)
241 let rl_arg = function
242 | Joint.Reg r -> rl_psingleton r
243 | Joint.Imm x -> rl_bottom
246 AST.ident List.list -> Joint.joint_statement -> (Registers.register
247 Set_adt.set, I8051.register Set_adt.set) Types.prod **)
248 let used globals = function
249 | Joint.Sequential (seq, l) ->
251 | Joint.COST_LABEL clabel -> Obj.magic rl_bottom
252 | Joint.CALL (f, nparams, x) ->
256 | Types.Inl x0 -> rl_bottom
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 ->
266 | Joint.COMMENT x -> Obj.magic rl_bottom
267 | Joint.MOVE pair_reg ->
268 let r2 = (Obj.magic pair_reg).Types.snd in
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) ->
283 (rl_join (rl_join (rl_arg (Obj.magic r1)) (rl_arg (Obj.magic r2)))
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) ->
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 ->
304 (rl_join (rl_hsingleton I8051.registerSPL)
305 (rl_hsingleton I8051.registerSPH))
306 | ERTL.Ertl_del_frame ->
308 (rl_join (rl_hsingleton I8051.registerSPL)
309 (rl_hsingleton I8051.registerSPH))
310 | ERTL.Ertl_frame_size r -> Obj.magic rl_bottom)))
313 | Joint.GOTO l -> Obj.magic rl_bottom
315 { Types.fst = Set_adt.set_empty; Types.snd =
316 (Set_adt.set_union (Set_adt.set_from_list I8051.registerCalleeSaved)
318 | Joint.TAILCALL (x, x0) -> assert false (* absurd case *))
319 | Joint.FCOND (x, x0, x1) -> assert false (* absurd case *)
321 (** val eliminable_step :
322 AST.ident List.list -> __ -> Joint.joint_step -> Bool.bool **)
323 let eliminable_step globals l s =
324 let pliveafter = (Obj.magic l).Types.fst in
325 let hliveafter = (Obj.magic l).Types.snd in
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 ->
332 | Joint.COMMENT x -> Bool.False
333 | Joint.MOVE pair_reg ->
335 (match (Obj.magic pair_reg).Types.fst with
338 (Identifiers.eq_identifier PreIdentifiers.RegisterTag) p1
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) ->
348 (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
349 (Obj.magic r1) pliveafter)
351 (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
352 (Obj.magic r2) pliveafter))
353 | Joint.OPACCS (opaccs, dr1, dr2, sr1, sr2) ->
358 (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
359 (Obj.magic dr1) pliveafter)
361 (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
362 (Obj.magic dr2) pliveafter))
363 (Set_adt.set_member I8051.eq_Register I8051.RegisterCarry
365 | Joint.OP1 (op1, r1, r2) ->
368 (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
369 (Obj.magic r1) pliveafter)
370 | Joint.OP2 (op2, r1, r2, r3) ->
375 Set_adt.set_member I8051.eq_Register I8051.RegisterCarry
378 Set_adt.set_member I8051.eq_Register I8051.RegisterCarry
381 Set_adt.set_member I8051.eq_Register I8051.RegisterCarry
383 | BackEndOps.And -> Bool.False
384 | BackEndOps.Or -> Bool.False
385 | BackEndOps.Xor -> Bool.False)
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) ->
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 ->
404 (Identifiers.eq_identifier PreIdentifiers.RegisterTag) r
408 AST.ident List.list -> __ -> Joint.joint_statement -> Bool.bool **)
409 let eliminable globals l s =
410 let pliveafter = (Obj.magic l).Types.fst in
411 let hliveafter = (Obj.magic l).Types.snd in
413 | Joint.Sequential (seq, x) -> eliminable_step globals l seq
414 | Joint.Final x -> Bool.False
415 | Joint.FCOND (x0, x1, x2) -> Bool.False)
417 (** val statement_semantics :
418 AST.ident List.list -> Joint.joint_statement -> __ -> __ **)
419 let statement_semantics globals stmt liveafter =
420 match eliminable globals liveafter stmt with
421 | Bool.True -> liveafter
423 rl_join (rl_diff liveafter (defined globals stmt))
424 (Obj.magic (used globals stmt))
427 AST.ident List.list -> Joint.joint_internal_function ->
428 Fixpoints.valuation -> Fixpoints.valuation **)
429 let 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)
436 AST.ident List.list -> Joint.joint_internal_function ->
437 PreIdentifiers.identifier -> Fixpoints.valuation -> __ **)
438 let 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
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)
449 (** val analyse_liveness :
450 Fixpoints.fixpoint_computer -> AST.ident List.list ->
451 Joint.joint_internal_function -> Fixpoints.fixpoint **)
452 let analyse_liveness the_fixpoint globals int_fun =
453 the_fixpoint register_lattice (liveafter globals int_fun)
455 type vertex = (Registers.register, I8051.register) Types.sum
457 (** val plives : Registers.register -> __ -> Bool.bool **)
458 let plives vertex0 prop =
459 Set_adt.set_member (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
460 vertex0 (Obj.magic prop).Types.fst
462 (** val hlives : I8051.register -> __ -> Bool.bool **)
463 let hlives vertex0 prop =
464 Set_adt.set_member I8051.eq_Register vertex0 (Obj.magic prop).Types.snd
466 (** val lives : vertex -> __ -> Bool.bool **)
468 | Types.Inl v -> plives v
469 | Types.Inr v -> hlives v