(* This module performs liveness analysis over the control flow
   graph of a single [ERTL] procedure. *)

(* In the following, a ``variable'' means a pseudo-register or an
   allocatable hardware register. *)

(* We collect liveness information about variables. We are not
   interested in collecting information about non-allocatable hardware
   registers such as [$gp], [$sp], etc. so they are considered never
   defined and never used as far as [ERTL] is concerned. *)

open ERTL

(* This is the lattice of sets of variables. *)

module L : sig
  type t = Register.Set.t * MIPS.RegisterSet.t
  val bottom: t
  val join: t -> t -> t
  val equal: t -> t -> bool
  val diff: t -> t -> t
  val psingleton: Register.t -> t
  val hsingleton: MIPS.register -> t
end

(* [defined i] is the set of variables defined at (written by)
   instruction [i]. *)

val defined: instruction -> L.t

(* A valuation is a function that maps a program point (a control flow
   graph label) to the set of variables that are live after that
   point. *)

type valuation =
    Label.t -> L.t

(* [analyze proc] analyzes the procedure [proc] and returns a valuation. *)

val analyze: procedure -> valuation

(* Pure instructions whose destination pseudo-register is dead after the
   instruction will be eliminated during the translation of [ERTL] to [LTL].
   [eliminable liveafter i] returns [Some successor], where [successor] is
   [i]'s single successor, if instruction [i] is eliminable. Otherwise, it
   returns [None]. *)

val eliminable: L.t -> instruction -> Label.t option