Source code for lyra.abstract_domains.usage.usage_lattice

"""
Usage Lattices
==============

Lattices to be used for **input data usage analysis**.

:Authors: Caterina Urban and Simon Wehrli
"""


from enum import Flag

from lyra.abstract_domains.lattice import Lattice
from lyra.core.utils import copy_docstring


[docs]class UsageLattice(Lattice): """Usage lattice:: U / \\ S W \\ / N The default lattice element is ``N`` (not used). .. document private methods .. automethod:: UsageLattice._less_equal .. automethod:: UsageLattice._meet .. automethod:: UsageLattice._join .. automethod:: UsageLattice._widening """
[docs] class Status(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 """ U = 3 S = 2 W = 1 N = 0
def __init__(self, usage: Status = Status.N): super().__init__() self._element = usage @property def element(self): """Current lattice element.""" return self._element def __repr__(self): return self.element.name
[docs] @copy_docstring(Lattice.bottom) def bottom(self): """The bottom lattice element is ``N`` (not used).""" self._replace(UsageLattice(UsageLattice.Status.N)) return self
[docs] def scoped(self): """Scoped lattice element. :return: current lattice element modified to be the scoped lattice element The scoped lattice element is ``S`` (scoped). """ self._replace(UsageLattice(UsageLattice.Status.S)) return self
[docs] def written(self): """Written lattice element. :return: current lattice element modified to be the written lattice element The written lattice element is ``W`` (written). """ self._replace(UsageLattice(UsageLattice.Status.W)) return self
[docs] @copy_docstring(Lattice.top) def top(self): """The top lattice element is ``U`` (used).""" self._replace(UsageLattice(UsageLattice.Status.U)) return self
[docs] @copy_docstring(Lattice.is_bottom) def is_bottom(self): return self.element == UsageLattice.Status.N
[docs] def is_scoped(self): """Test whether the lattice element is ``S`` (scoped). :return: whether the lattice element is ``S`` (scoped) """ return self.element == UsageLattice.Status.S
[docs] def is_written(self): """Test whether the lattice element is ``W`` (written). :return: whether the lattice element is ``W`` (written) """ return self.element == UsageLattice.Status.W
[docs] @copy_docstring(Lattice.is_top) def is_top(self): return self.element == UsageLattice.Status.U
[docs] def increase(self) -> 'UsageLattice': """Increase the nesting level. | ... | self | -> | ... | self | self.increase | :return: current lattice element modified to reflect an increased nesting level """ if self.is_top(): return self.scoped() elif self.is_written(): return self.bottom() return self
[docs] def decrease(self, other: 'UsageLattice') -> 'UsageLattice': """Decrease the nesting level by combining lattice elements. | ... | self | other | -> | ... | self.decrease(other) | :param other: other lattice element, higher nesting level :return: current lattice element modified to reflect a decreased nesting level """ assert not self.is_written() or not other.is_scoped() if self.is_bottom() or other.is_written() or other.is_top(): self._replace(other) return self
[docs] @copy_docstring(Lattice.less_equal) def _less_equal(self, other: 'UsageLattice') -> bool: return self.element == other.element
[docs] @copy_docstring(Lattice._meet) def _meet(self, other: 'UsageLattice') -> 'UsageLattice': self._replace(UsageLattice(self.element & other.element)) return self
[docs] @copy_docstring(Lattice._join) def _join(self, other: 'UsageLattice') -> 'UsageLattice': self._replace(UsageLattice(self.element | other.element)) return self
[docs] @copy_docstring(Lattice._widening) def _widening(self, other: 'UsageLattice') -> 'UsageLattice': return self._join(other)