source: Deliverables/D2.2/8051/src/ERTL/liveness.mli @ 486

Last change on this file since 486 was 486, checked in by ayache, 9 years ago

Deliverable D2.2

File size: 1.6 KB
Line 
1(* Pasted from Pottier's PP compiler *)
2
3(** This module performs liveness analysis over the control flow graph
4    of a single [ERTL] procedure. *)
5
6(* In the following, a ``variable'' means a pseudo-register or an
7   allocatable hardware register. *)
8
9(* We collect liveness information about variables. We are not interested in
10   collecting information about non-allocatable hardware registers such as the
11   stack pointer registers, etc. so they are considered never defined and never
12   used as far as [ERTL] is concerned. *)
13
14open ERTL
15
16(* This is the lattice of sets of variables. *)
17
18module L : sig
19  type t = Register.Set.t * I8051.RegisterSet.t
20  val bottom: t
21  val join: t -> t -> t
22  val equal: t -> t -> bool
23  val diff: t -> t -> t
24  val psingleton: Register.t -> t
25  val hsingleton: I8051.register -> t
26end
27
28(* [defined i] is the set of variables defined at (written by)
29   statement [i]. *)
30
31val defined: statement -> L.t
32
33(* A valuation is a function that maps a program point (a control flow
34   graph label) to the set of variables that are live after that
35   point. *)
36
37type valuation =
38    Label.t -> L.t
39
40(* [analyze int_fun] analyzes the function [int_fun] and returns a valuation. *)
41
42val analyze: internal_function -> valuation
43
44(* Pure instructions whose destination pseudo-register is dead after the
45   instruction will be eliminated during the translation of [ERTL] to [LTL].
46   [eliminable liveafter i] returns [Some successor], where [successor] is
47   [i]'s single successor, if instruction [i] is eliminable. Otherwise, it
48   returns [None]. *)
49
50val eliminable: L.t -> statement -> Label.t option
51
Note: See TracBrowser for help on using the repository browser.