lyra.abstract_domains.liveness package¶

Submodules¶

Live Variable Abstract Domains¶

Abstract domains to be used for live variable analysis and strongly live variable analysis.

A program variable is live in a state if its value may be used before the variable is redefined. A program variable is strongly live if it is used in an assignment to another strongly live variable, or if is used in a statement other than an assignment.

Author:	Caterina Urban

class lyra.abstract_domains.liveness.liveness_domain.LivenessLattice(liveness: lyra.abstract_domains.liveness.liveness_domain.LivenessLattice.Status = <Status.Dead: 0>)[source]¶

Bases: lyra.abstract_domains.lattice.Lattice

Liveness lattice:

Live
  |
Dead

The default lattice element is Dead.

_less_equal(other: lyra.abstract_domains.liveness.liveness_domain.LivenessLattice) → bool[source]¶

Partial order between default lattice elements.

Parameters:	other – other lattice element
Returns:	whether the current lattice element is less than or equal to the other element

_meet(other: lyra.abstract_domains.liveness.liveness_domain.LivenessLattice) → lyra.abstract_domains.liveness.liveness_domain.LivenessLattice[source]¶

Greatest lower bound between default lattice elements.

Parameters:	other – other lattice element
Returns:	current lattice element modified to be the greatest lower bound

_join(other: lyra.abstract_domains.liveness.liveness_domain.LivenessLattice) → lyra.abstract_domains.liveness.liveness_domain.LivenessLattice[source]¶

Least upper bound between default lattice elements.

Parameters:	other – other lattice element
Returns:	current lattice element modified to be the least upper bound

_widening(other: lyra.abstract_domains.liveness.liveness_domain.LivenessLattice) → lyra.abstract_domains.liveness.liveness_domain.LivenessLattice[source]¶

Widening between default lattice elements.

Parameters:	other – other lattice element
Returns:	current lattice element modified to be the widening

class Status[source]¶

Bases: enum.IntEnum

Liveness status. The current lattice element is ether Live or Dead.

Dead = 0¶

Live = 1¶

bottom() → lyra.abstract_domains.liveness.liveness_domain.LivenessLattice[source]¶

Bottom lattice element.

Returns:	current lattice element modified to be the bottom lattice element

The bottom lattice element is Dead.

element¶: Current lattice element.

is_bottom() → bool[source]¶

Test whether the lattice element is bottom.

Returns:	whether the lattice element is bottom

is_top() → bool[source]¶

Test whether the lattice element is top.

Returns:	whether the lattice element is top

top() → lyra.abstract_domains.liveness.liveness_domain.LivenessLattice[source]¶

Top lattice element.

Returns:	current lattice element modified to be the top lattice element

The top lattice element is Live.

class lyra.abstract_domains.liveness.liveness_domain.LivenessState(variables: typing.Set[lyra.core.expressions.VariableIdentifier], precursory: lyra.abstract_domains.state.State = None)[source]¶

Bases: lyra.abstract_domains.store.Store, lyra.abstract_domains.state.State

Live variable analysis state. An element of the live variable abstract domain.

Map from each program variable to its liveness status. All program variables are dead by default.

Note

Program variables storing lists are abstracted via summarization.

_assign(left: lyra.core.expressions.Expression, right: lyra.core.expressions.Expression)[source]¶

Assign an expression to another expression.

Warning

The current state could also be bottom or top.

Parameters:	left – expression to be assigned to right – expression to assign
Returns:	current state modified by the assignment

_assume(condition: lyra.core.expressions.Expression) → lyra.abstract_domains.liveness.liveness_domain.LivenessState[source]¶

Assume that some condition holds in the current state.

Warning

The current state could also be bottom or top.

Parameters:	condition – expression representing the assumed condition
Returns:	current state modified to satisfy the assumption

_output(output: lyra.core.expressions.Expression) → lyra.abstract_domains.liveness.liveness_domain.LivenessState[source]¶

Outputs something in the current state.

Warning

The current state could also be bottom or top.

Parameters:	output – expression representing the output
Returns:	current state modified by the output

_substitute(left: lyra.core.expressions.Expression, right: lyra.core.expressions.Expression) → lyra.abstract_domains.liveness.liveness_domain.LivenessState[source]¶

Substitute an expression to another expression.

Warning

The current state could also be bottom or top.

Parameters:	left – expression to be substituted right – expression to substitute
Returns:	current state modified by the substitution

enter_if() → lyra.abstract_domains.liveness.liveness_domain.LivenessState[source]¶

Enter a conditional if statement.

Warning

The current state could also be bottom or top.

Returns:	current state modified to enter a conditional if statement

enter_loop() → lyra.abstract_domains.liveness.liveness_domain.LivenessState[source]¶

Enter a loop.

Warning

The current state could also be bottom or top.

Returns:	current state modified to enter a loop

exit_if() → lyra.abstract_domains.liveness.liveness_domain.LivenessState[source]¶

Exit a conditional if statement.

Warning

The current state could also be bottom or top.

Returns:	current state modified to enter a conditional if statement

exit_loop() → lyra.abstract_domains.liveness.liveness_domain.LivenessState[source]¶

Exit a loop.

Warning

The current state could also be bottom or top.

Returns:	current state modified to exit a loop

is_bottom() → bool[source]¶

Test whether the lattice element is bottom.

Returns:	whether the lattice element is bottom

The current store is bottom if any of its variables map to a bottom element.The current store is bottom if all of its variables map to a bottom element.

class lyra.abstract_domains.liveness.liveness_domain.StrongLivenessState(variables: typing.Set[lyra.core.expressions.VariableIdentifier], precursory: lyra.abstract_domains.state.State = None)[source]¶

Bases: lyra.abstract_domains.liveness.liveness_domain.LivenessState

Strongly live variable analysis state. An element of the strongly live variable abstract domain.

Map from each program variable to its liveness status. All program variables are dead by default.

Note

Program variables storing lists are abstracted via summarization.

_assign(left: lyra.core.expressions.Expression, right: lyra.core.expressions.Expression)¶

Assign an expression to another expression.

Warning

The current state could also be bottom or top.

Parameters:	left – expression to be assigned to right – expression to assign
Returns:	current state modified by the assignment

_assume(condition: lyra.core.expressions.Expression) → lyra.abstract_domains.liveness.liveness_domain.LivenessState¶

Assume that some condition holds in the current state.

Warning

The current state could also be bottom or top.

Parameters:	condition – expression representing the assumed condition
Returns:	current state modified to satisfy the assumption

_output(output: lyra.core.expressions.Expression) → lyra.abstract_domains.liveness.liveness_domain.StrongLivenessState[source]¶

Outputs something in the current state.

Warning

The current state could also be bottom or top.

Parameters:	output – expression representing the output
Returns:	current state modified by the output

_substitute(left: lyra.core.expressions.Expression, right: lyra.core.expressions.Expression) → lyra.abstract_domains.liveness.liveness_domain.StrongLivenessState[source]¶

Substitute an expression to another expression.

Warning

The current state could also be bottom or top.

Parameters:	left – expression to be substituted right – expression to substitute
Returns:	current state modified by the substitution