"""
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
"""
from collections import defaultdict
from enum import IntEnum
from typing import Set
from lyra.abstract_domains.lattice import Lattice
from lyra.abstract_domains.state import State
from lyra.core.expressions import Expression, VariableIdentifier, Subscription, Slicing
from lyra.abstract_domains.store import Store
from lyra.core.utils import copy_docstring
[docs]class LivenessLattice(Lattice):
"""Liveness lattice::
Live
|
Dead
The default lattice element is ``Dead``.
.. document private methods
.. automethod:: LivenessLattice._less_equal
.. automethod:: LivenessLattice._meet
.. automethod:: LivenessLattice._join
.. automethod:: LivenessLattice._widening
"""
[docs] class Status(IntEnum):
"""Liveness status. The current lattice element is ether ``Live`` or ``Dead``."""
Live = 1
Dead = 0
def __init__(self, liveness: Status = Status.Dead):
super().__init__()
self._element = liveness
@property
def element(self) -> Status:
"""Current lattice element."""
return self._element
def __repr__(self):
return self.element.name
[docs] @copy_docstring(Lattice.bottom)
def bottom(self) -> 'LivenessLattice':
"""The bottom lattice element is ``Dead``."""
self._replace(LivenessLattice(LivenessLattice.Status.Dead))
return self
[docs] @copy_docstring(Lattice.top)
def top(self) -> 'LivenessLattice':
"""The top lattice element is ``Live``."""
self._replace(LivenessLattice(LivenessLattice.Status.Live))
return self
[docs] @copy_docstring(Lattice.is_bottom)
def is_bottom(self) -> bool:
return self.element == LivenessLattice.Status.Dead
[docs] @copy_docstring(Lattice.is_top)
def is_top(self) -> bool:
return self.element == LivenessLattice.Status.Live
[docs] @copy_docstring(Lattice._less_equal)
def _less_equal(self, other: 'LivenessLattice') -> bool:
return self.element <= other.element
[docs] @copy_docstring(Lattice._meet)
def _meet(self, other: 'LivenessLattice') -> 'LivenessLattice':
self._replace(LivenessLattice(min(self.element, other.element)))
return self
[docs] @copy_docstring(Lattice._join)
def _join(self, other: 'LivenessLattice') -> 'LivenessLattice':
self._replace(LivenessLattice(max(self.element, other.element)))
return self
[docs] @copy_docstring(Lattice._widening)
def _widening(self, other: 'LivenessLattice') -> 'LivenessLattice':
return self._join(other)
[docs]class LivenessState(Store, 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.
.. document private methods
.. automethod:: LivenessState._assign
.. automethod:: LivenessState._assume
.. automethod:: LivenessState._output
.. automethod:: LivenessState._substitute
"""
def __init__(self, variables: Set[VariableIdentifier], precursory: State = None):
"""Map each program variable to its liveness status.
:param variables: set of program variables
"""
lattices = defaultdict(lambda: LivenessLattice)
super().__init__(variables, lattices)
State.__init__(self, precursory)
[docs] @copy_docstring(Store.is_bottom)
def is_bottom(self) -> bool:
"""The current store is bottom if `all` of its variables map to a bottom element."""
return all(element.is_bottom() for element in self.store.values())
[docs] @copy_docstring(State._assign)
def _assign(self, left: Expression, right: Expression):
raise RuntimeError("Unexpected assignment in a backward analysis!")
[docs] @copy_docstring(State._assume)
def _assume(self, condition: Expression) -> 'LivenessState':
for identifier in condition.ids():
self.store[identifier].top()
return self
[docs] @copy_docstring(State.enter_if)
def enter_if(self) -> 'LivenessState':
return self # nothing to be done
[docs] @copy_docstring(State.exit_if)
def exit_if(self) -> 'LivenessState':
return self # nothing to be done
[docs] @copy_docstring(State.enter_loop)
def enter_loop(self) -> 'LivenessState':
return self # nothing to be done
[docs] @copy_docstring(State.exit_loop)
def exit_loop(self) -> 'LivenessState':
return self # nothing to be done
[docs] @copy_docstring(State._output)
def _output(self, output: Expression) -> 'LivenessState':
return self # nothing to be done
[docs] @copy_docstring(State._substitute)
def _substitute(self, left: Expression, right: Expression) -> 'LivenessState':
if isinstance(left, VariableIdentifier):
self.store[left].bottom()
for identifier in right.ids():
self.store[identifier].top()
return self
error = f"Substitution for {left} is not yet implemented!"
raise NotImplementedError(error)
[docs]class StrongLivenessState(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.
.. document private methods
.. automethod:: StrongLivenessState._assign
.. automethod:: StrongLivenessState._assume
.. automethod:: StrongLivenessState._output
.. automethod:: StrongLivenessState._substitute
"""
[docs] @copy_docstring(LivenessState._output)
def _output(self, output: Expression) -> 'StrongLivenessState':
for identifier in output.ids():
self.store[identifier] = LivenessLattice(LivenessLattice.Status.Live)
return self
[docs] @copy_docstring(LivenessState._substitute)
def _substitute(self, left: Expression, right: Expression) -> 'StrongLivenessState':
if isinstance(left, VariableIdentifier):
if self.store[left].is_top(): # the assigned variable is strongly-live
self.store[left].bottom()
for identifier in right.ids():
self.store[identifier].top()
return self
elif isinstance(left, Subscription) or isinstance(left, Slicing):
target = left.target
if self.store[target].is_top(): # the target variable (list, dict,..) is strongly-live
# summarization abstraction (weak update)
for identifier in right.ids():
self.store[identifier].top()
if isinstance(left, Subscription):
ids = left.key.ids()
else: # Slicing
ids = left.lower.ids() | left.upper.ids()
for identifier in ids: # make ids in subscript strongly live
self.store[identifier].top()
return self
error = f"Substitution for {left} is not yet implemented!"
raise NotImplementedError(error)