"""
Abstract Domain
===============
Interface of an abstract domain.
Abstract domain elements support lattice operations and program statements.
:Author: Caterina Urban
"""
from abc import ABCMeta, abstractmethod
from copy import deepcopy
from typing import Set, Optional
from lyra.abstract_domains.lattice import Lattice
from lyra.core.expressions import Expression, VariableIdentifier
from lyra.core.statements import ProgramPoint
[docs]class State(Lattice, metaclass=ABCMeta):
"""Analysis state. A mutable element of an abstract domain.
.. warning::
Lattice operations and statements modify the current state.
"""
def __init__(self, precursory: 'State' = None):
super().__init__()
self._result = set()
self._pp = None
self._precursory = precursory
@property
def result(self):
"""Result of the previously analyzed statement."""
return self._result
@result.setter
def result(self, result: Set[Expression]):
self._result = result
@property
def pp(self):
"""Program point of the currently analyzed statement."""
return self._pp
@pp.setter
def pp(self, pp: ProgramPoint):
self._pp = pp
@property
def precursory(self):
"""Current precursory analysis state."""
return self._precursory
@precursory.setter
def precursory(self, precursory: 'State'):
self._precursory = precursory
def __repr__(self):
return ", ".join("{}".format(expression) for expression in self.result)
@abstractmethod
def _assign(self, left: Expression, right: Expression) -> 'State':
"""Assign an expression to another expression.
.. warning::
The current state could also be bottom or top.
:param left: expression to be assigned to
:param right: expression to assign
:return: current state modified by the assignment
"""
[docs] def assign(self, left: Set[Expression], right: Set[Expression]) -> 'State':
"""Assign an expression to another expression.
:param left: set of expressions representing the expression to be assigned to
:param right: set of expressions representing the expression to assign
:return: current state modified by the assignment
"""
self.big_join([deepcopy(self)._assign(lhs, rhs) for lhs in left for rhs in right])
self.result = set() # assignments have no result, only side-effects
return self
@abstractmethod
def _assume(self, condition: Expression) -> 'State':
"""Assume that some condition holds in the current state.
.. warning::
The current state could also be bottom or top.
:param condition: expression representing the assumed condition
:return: current state modified to satisfy the assumption
"""
[docs] def assume(self, condition: Set[Expression]) -> 'State':
"""Assume that some condition holds in the current state.
:param condition: set of expressions representing the assumed condition
:return: current state modified to satisfy the assumption
"""
self.big_join([deepcopy(self)._assume(expr) for expr in condition])
return self
[docs] def before(self, pp: ProgramPoint, precursory: Optional['State']) -> 'State':
"""Set the program point of the currently analyzed statement
and the current precursory analysis state.
:param pp: current program point
:param precursory: current precursory analysis state
:return: current state modified to set the current program point and precursory state
"""
self.pp = pp
self.precursory = precursory
return self
[docs] @abstractmethod
def enter_if(self) -> 'State':
"""Enter a conditional if statement.
.. warning::
The current state could also be bottom or top.
:return: current state modified to enter a conditional if statement
"""
[docs] @abstractmethod
def exit_if(self) -> 'State':
"""Exit a conditional if statement.
.. warning::
The current state could also be bottom or top.
:return: current state modified to enter a conditional if statement
"""
[docs] @abstractmethod
def enter_loop(self) -> 'State':
"""Enter a loop.
.. warning::
The current state could also be bottom or top.
:return: current state modified to enter a loop
"""
[docs] @abstractmethod
def exit_loop(self) -> 'State':
"""Exit a loop.
.. warning::
The current state could also be bottom or top.
:return: current state modified to exit a loop
"""
[docs] def filter(self) -> 'State':
"""Assume that the current result holds in the current state.
:return: current state modified to satisfy the current result
"""
self.assume(self.result)
self.result = set() # filtering has no result, only side-effects
return self
@abstractmethod
def _output(self, output: Expression) -> 'State':
"""Outputs something in the current state.
.. warning::
The current state could also be bottom or top.
:param output: expression representing the output
:return: current state modified by the output
"""
[docs] def output(self, output: Set[Expression]) -> 'State':
"""Outputs something in the current state.
:param output: set of expressions representing the output
:return: current state modified by the output
"""
self.big_join([deepcopy(self)._output(expr) for expr in output])
self.result = set() # outputs have no result, only side-effects
return self
[docs] def raise_error(self) -> 'State':
"""Raise an error.
:return: current state modified to be the bottom state
"""
return self.bottom()
@abstractmethod
def _substitute(self, left: Expression, right: Expression) -> 'State':
"""Substitute an expression to another expression.
.. warning::
The current state could also be bottom or top.
:param left: expression to be substituted
:param right: expression to substitute
:return: current state modified by the substitution
"""
[docs] def substitute(self, left: Set[Expression], right: Set[Expression]) -> 'State':
"""Substitute an expression to another expression.
:param left: set of expressions representing the expression to be substituted
:param right: set of expressions representing the expression to substitute
:return: current state modified by the substitution
"""
self.big_join([deepcopy(self)._substitute(l, r) for l in left for r in right])
self.result = set() # assignments have no result, only side-effects
return self
[docs]class EnvironmentMixin(State, metaclass=ABCMeta):
"""Mixin to add environment modification operations to another state."""
[docs] @abstractmethod
def add_variable(self, variable: VariableIdentifier):
"""Add a variable.
:param variable: variable to be added
:return: current state modified by the variable addition
"""
[docs] @abstractmethod
def forget_variable(self, variable: VariableIdentifier):
"""Forget the value of a variable.
:param variable: variable whose value is to be forgotten
:return: current state modified to have value top for the forgotten variable
"""
[docs] @abstractmethod
def remove_variable(self, variable: VariableIdentifier):
"""Remove a variable.
:param variable: variable to be removed
:return: current state modified by the variable removal
"""