src/ERTL/liveness.mli

   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
  14 open ERTL
  15
  16 (* This is the lattice of sets of variables. *)
  17
  18 module 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
  26 end
  27
  28 (* [defined i] is the set of variables defined at (written by)
  29    statement [i]. *)
  30
  31 val 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
  37 type valuation =
  38     Label.t -> L.t
  39
  40 (* [analyze int_fun] analyzes the function [int_fun] and returns a valuation. *)
  41
  42 val 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
  50 val eliminable: L.t -> statement -> Label.t option
  51