Source code for lyra.abstract_domains.stack

"""
Stack
=====

Stack of lattices.

:Authors: Caterina Urban and Simon Wehrli
"""

from abc import ABCMeta, abstractmethod
from typing import Type, Dict, Any

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


[docs]class Stack(BoundedLattice, metaclass=ABCMeta): """Mutable stack of elements of a lattice. .. warning:: Lattice operations modify the current stack. .. document private methods .. automethod:: Stack._less_equal .. automethod:: Stack._meet .. automethod:: Stack._join """ def __init__(self, lattice: Type, arguments: Dict[str, Any]): """Create a stack of elements of a lattice. :param lattice: type of the lattice """ super().__init__() self._stack = [lattice(**arguments)] @property def stack(self): """Current stack of lattice elements.""" return self._stack @property def lattice(self): """Lattice element currently on top of the stack.""" return self.stack[-1] def __repr__(self): return " | ".join(map(repr, reversed(self.stack)))
[docs] @abstractmethod def push(self): """Push an element on the current stack."""
[docs] @abstractmethod def pop(self): """Pop an element from the current stack."""
[docs] @copy_docstring(BoundedLattice._less_equal) def _less_equal(self, other: 'Stack') -> bool: """The comparison is performed point-wise for each stack element.""" if len(self.stack) != len(other.stack): raise Exception("Stacks must be equally long") return all(l.less_equal(r) for l, r in zip(self.stack, other.stack))
[docs] @copy_docstring(BoundedLattice._meet) def _meet(self, other: 'Stack'): """The meet is performed point-wise for each stack element.""" if len(self.stack) != len(other.stack): raise Exception("Stacks must be equally long") for i, item in enumerate(self.stack): item.meet(other.stack[i]) return self
[docs] @copy_docstring(BoundedLattice._join) def _join(self, other: 'Stack') -> 'Stack': """The join is performed point-wise for each stack element.""" if len(self.stack) != len(other.stack): raise Exception("Stacks must be equally long") for i, item in enumerate(self.stack): item.join(other.stack[i]) return self
@copy_docstring(BoundedLattice._widening) def _widening(self, other: 'Stack'): return self._join(other)