Module Std.Live

Live Variables.

Computes the set of live variables for each block in a subroutine, taking into account subroutine arguments.

A variable v is live at a program point x if there exists a path from x to a use of v that doesn't go through a definition of v.

This module computes liveness on the block granularity, which gives rise to the following notions.

A variable is live-in at a basic block x if it is live at the begining of the block x.

A variable is live-out at a basic block x if it is live on any of the outcoming edges of x.

A variable is live-through at a basic block x if it is both live-in and live-out at it.

Liveness in the SSA form

The algorithm works with the SSA form. From the perspective of liveness, the phi-nodes define their right-hand sides on the edges incoming from the corresponding blocks. More formally, for a phi-node at block b0, x0 := phi([b1,x1; b2,x2;...;bN,xN]), the defined variable x0 is considered to be defined at blocks bi and the variable xi live-out of basic block bi, for 0 < i <= N.

Intuitively, this can be visualized as if the following program,

        b1:
        x.1 := 1
        goto b3

        b2:
        x.2 := 2
        goto b3

        b3:
        x.3 <- phi([b1,x1]; [b2, x2])
        ...

is rewritten to an equivalent (but not in SSA) program,

        b1:
        x.1 := 1
        x.3 := x1
        goto b3

        b2:
        x.2 := 2
        x.3 := x2
        goto b3

        b3:
        ...

That means that a variable defined by a phi-node in a block x could be live-in at the block x.

The Live.defs and Live.uses includes the variables from the corresponding phi-nodes, e.g., Live.defs b1 will is {x1,x3} and Live.uses b1 is {x1}.

type t
val compute : ?keep:Var.Set.t -> sub term -> t

compute sub computes the subroutine liveness information.

Variables specified by keep will be kept live at the exit from the function. In addition to the variables in keep, all free variables used by in and in/out arguments of the subroutine will be kept alive at the exit.

val vars : t -> Var.Set.t

vars live the variables that are live in the subroutine.

The set of variables that are live-in on the entry block of the subroutine that was used to compute live. The live variables of the subroutine also called free variables or upper-exposed variables. They may be used in the subroutine before they are assigned.

val ins : t -> tid -> Var.Set.t

ins live blk the set of live-in variables at blk.

The set of variables that are live at the entry to the basic block blk.

Returns an empty set if blk doesn't belong to the sub graph.

val outs : t -> tid -> Var.Set.t

outs live blk the set of live-outs variables at blk.

The set of variables that are live at the exist from the basic block blk.

Returns an empty set if blk doesn't belong to the sub graph.

val blks : t -> var -> Core_kernel.Set.M(Tid).t

blks live var the set of blks where var is live-in.

val defs : t -> tid -> Var.Set.t

defs live blk the set of variables defined by blk.

Aka the KILL set, i.e., the set of variables whose liveness is killed in the block blk.

val uses : t -> tid -> Var.Set.t

uses live blk the set of variables used by blk.

Aka the GEN set, i.e., the set of variables generated by the block blk.

val fold : t -> init:'a -> f:('a -> tid -> Var.Set.t -> 'a) -> 'a

fold live ~init ~f folds over live-ins of blocks.

Applies f to live-in set of variables of each block of the subroutine.

Note, pseudo start and exit nodes are not folded over.

val solution : t -> (tid, Var.Set.t) Graphlib.Std.Solution.t

solution live returns the fixed point solution.

The solution is the mapping from blocks to their live-outs.

val pp : Stdlib.Format.formatter -> t -> unit

pp ppf live prints the live-in sets of each basic block.