"""
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)