Source code for lyra.abstract_domains.store

"""
Store
=====

Lifting of a lattice to a set of program variables.

:Authors: Caterina Urban and Simon Wehrli
"""


from collections import defaultdict
from typing import Dict, Any, Type, Set

from lyra.core.expressions import VariableIdentifier
from lyra.abstract_domains.lattice import Lattice
from lyra.core.types import LyraType
from lyra.core.utils import copy_docstring


[docs]class Store(Lattice): """Mutable element of a store ``Var -> L``, lifting a lattice ``L`` to a set of program variables ``Var``. .. warning:: Lattice operations modify the current store. .. document private methods .. automethod:: Store._less_equal .. automethod:: Store._meet .. automethod:: Store._join """ def __init__(self, variables: Set[VariableIdentifier], lattices: Dict[LyraType, Type[Lattice]], arguments: Dict[LyraType, Dict[str, Any]] = defaultdict(lambda: dict())): """Create a mapping Var -> L from each variable in Var to the corresponding element in L. :param variables: set of program variables :param lattices: dictionary from variable types to the corresponding lattice types :param arguments: dictionary from variable types to arguments of the corresponding lattices """ super().__init__() self._variables = variables self._lattices = lattices self._arguments = arguments try: self._store = {v: lattices[v.typ](**arguments[v.typ]) for v in variables} except KeyError as key: error = f"Missing lattice for variable type {repr(key.args[0])}!" raise ValueError(error) @property def variables(self): """Variables of the current store.""" return self._variables @property def lattices(self): """Current dictionary fro variable types to the corresponding lattice types.""" return self._lattices @property def arguments(self): """Current dictionary from variable types to argument of the corresponding lattices.""" return self._arguments @property def store(self): """Current mapping from variables to their corresponding lattice element.""" return self._store def __repr__(self): items = sorted(self.store.items(), key=lambda x: x[0].name) return ", ".join("{} -> {}".format(variable, value) for variable, value in items)
[docs] @copy_docstring(Lattice.bottom) def bottom(self) -> 'Store': for var in self.store: self.store[var].bottom() return self
[docs] @copy_docstring(Lattice.top) def top(self) -> 'Store': for var in self.store: self.store[var].top() return self
[docs] @copy_docstring(Lattice.is_bottom) def is_bottom(self) -> bool: """The current store is bottom if `any` of its variables map to a bottom element.""" return any(element.is_bottom() for element in self.store.values())
[docs] @copy_docstring(Lattice.is_top) def is_top(self) -> bool: """The current store is top if `all` of its variables map to a top element.""" return all(element.is_top() for element in self.store.values())
[docs] @copy_docstring(Lattice._less_equal) def _less_equal(self, other: 'Store') -> bool: """The comparison is performed point-wise for each variable.""" return all(self.store[var].less_equal(other.store[var]) for var in self.store)
[docs] @copy_docstring(Lattice._meet) def _meet(self, other: 'Store'): """The meet is performed point-wise for each variable.""" for var in self.store: self.store[var].meet(other.store[var]) return self
[docs] @copy_docstring(Lattice._join) def _join(self, other: 'Store') -> 'Store': """The join is performed point-wise for each variable.""" for var in self.store: self.store[var].join(other.store[var]) return self
@copy_docstring(Lattice._widening) def _widening(self, other: 'Store'): """The widening is performed point-wise for each variable.""" for var in self.store: self.store[var].widening(other.store[var]) return self