lyra.abstract_domains.usage package

Submodules

Syntactic Usage Abstract Domain

Abstract domain to be used for input data usage analysis using syntactic variable dependencies. A program variable can have value U (used), S (scoped), W (written), and N (not used).

Authors:Caterina Urban and Simon Wehrli

class lyra.abstract_domains.usage.usage_domain.SimpleUsageState(variables: typing.Set[lyra.core.expressions.VariableIdentifier], precursory: lyra.abstract_domains.state.State = None)

Bases: lyra.abstract_domains.stack.Stack, lyra.abstract_domains.state.State

Input data usage analysis state. An element of the syntactic usage abstract domain.

Stack of maps from each program variable to its usage status. The stack contains a single map 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.usage.usage_domain.SimpleUsageState

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.usage.usage_domain.SimpleUsageState

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.usage.usage_domain.SimpleUsageState

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.usage.usage_domain.SimpleUsageState

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.usage.usage_domain.SimpleUsageState

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.usage.usage_domain.SimpleUsageState

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.usage.usage_domain.SimpleUsageState

Exit a loop.

Warning

The current state could also be bottom or top.

Returns:current state modified to exit a loop

pop()

Pop an element from the current stack.

push()

Push an element on the current stack.

class lyra.abstract_domains.usage.usage_domain.SimpleUsageStore(variables: typing.Set[lyra.core.expressions.VariableIdentifier])

Bases: lyra.abstract_domains.usage.usage_domain.UsageStore

An element of a store mapping each program variable to its usage status.

All program variables are not used by default.

Note

Program variables storing lists are abstracted via summarization.

_less_equal(other: lyra.abstract_domains.store.Store) → bool

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

The comparison is performed point-wise for each variable.

_meet(other: lyra.abstract_domains.store.Store)

Greatest lower bound between default lattice elements.

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

The meet is performed point-wise for each variable.

_join(other: lyra.abstract_domains.store.Store) → lyra.abstract_domains.store.Store

Least upper bound between default lattice elements.

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

The join is performed point-wise for each variable.

class lyra.abstract_domains.usage.usage_domain.UsageStore(variables, lattices: typing.Dict[lyra.core.types.LyraType, typing.Type[lyra.abstract_domains.lattice.Lattice]])

Bases: lyra.abstract_domains.store.Store

An element of a store mapping each program variable to its usage status.

All program variables are not used by default.

_less_equal(other: lyra.abstract_domains.store.Store) → bool

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

The comparison is performed point-wise for each variable.

_meet(other: lyra.abstract_domains.store.Store)

Greatest lower bound between default lattice elements.

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

The meet is performed point-wise for each variable.

_join(other: lyra.abstract_domains.store.Store) → lyra.abstract_domains.store.Store

Least upper bound between default lattice elements.

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

The join is performed point-wise for each variable.

decrease(other: lyra.abstract_domains.usage.usage_domain.UsageStore) → lyra.abstract_domains.usage.usage_domain.UsageStore

Decrease the nesting level by combining lattice elements.

Parameters:other – other lattice element Returns:current lattice element modified to reflect a decreased nesting level

The decrease is performed point-wise for each variable.

increase() → lyra.abstract_domains.usage.usage_domain.UsageStore

Increase the nesting level.

Returns:current lattice element modified to reflect an increased nesting level

The increase is performed point-wise for each variable.

is_bottom() → bool

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.

Usage Lattices

Lattices to be used for input data usage analysis.

Authors:Caterina Urban and Simon Wehrli

class lyra.abstract_domains.usage.usage_lattice.UsageLattice(usage: lyra.abstract_domains.usage.usage_lattice.UsageLattice.Status = <Status.N: 0>)

Bases: lyra.abstract_domains.lattice.Lattice

Usage lattice:

    U
  /   \
S       W
  \   /
    N

The default lattice element is N (not used).

_less_equal(other: lyra.abstract_domains.usage.usage_lattice.UsageLattice) → bool

Partial order between 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.usage.usage_lattice.UsageLattice) → lyra.abstract_domains.usage.usage_lattice.UsageLattice

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.usage.usage_lattice.UsageLattice) → lyra.abstract_domains.usage.usage_lattice.UsageLattice

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.usage.usage_lattice.UsageLattice) → lyra.abstract_domains.usage.usage_lattice.UsageLattice

Widening between default lattice elements.

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

class Status

Bases: enum.Flag

Usage status.

The current lattice element can be:

• U (used): used at the current nesting level
• S (scoped): used at a lower nesting level
• W (written): used at a lower nesting level and modified at the current nesting level
• N (not used): unused

N = 0

S = 2

U = 3

W = 1

bottom()

Bottom lattice element.

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

The bottom lattice element is N (not used).

decrease(other: lyra.abstract_domains.usage.usage_lattice.UsageLattice) → lyra.abstract_domains.usage.usage_lattice.UsageLattice

Decrease the nesting level by combining lattice elements.

… | self | other | -> | … | self.decrease(other) |

Parameters:other – other lattice element, higher nesting level Returns:current lattice element modified to reflect a decreased nesting level

element

Current lattice element.

increase() → lyra.abstract_domains.usage.usage_lattice.UsageLattice

Increase the nesting level.

… | self | -> | … | self | self.increase |

Returns:current lattice element modified to reflect an increased nesting level

is_bottom()

Test whether the lattice element is bottom.

Returns:whether the lattice element is bottom

is_scoped()

Test whether the lattice element is S (scoped).

Returns:whether the lattice element is S (scoped)

is_top()

Test whether the lattice element is top.

Returns:whether the lattice element is top

is_written()

Test whether the lattice element is W (written).

Returns:whether the lattice element is W (written)

scoped()

Scoped lattice element.

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

The scoped lattice element is S (scoped).

top()

Top lattice element.

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

The top lattice element is U (used).

written()

Written lattice element.

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

The written lattice element is W (written).