"""
Sign Abstract Domain
====================
Non-relational abstract domain to be used for **numerical analysis**.
The set of possible numerical values of a program variable in a program state
is represented by their sign (negative, zero, positive, ...).
:Author: Jérôme Dohrau and Caterina Urban
"""
from collections import defaultdict
from lyra.abstract_domains.basis import Basis
from lyra.abstract_domains.lattice import ArithmeticMixin, BooleanMixin
from lyra.abstract_domains.state import State
from lyra.core.expressions import *
from lyra.core.types import FloatLyraType
from lyra.core.utils import copy_docstring
[docs]class SignLattice(ArithmeticMixin, BooleanMixin):
"""Sign lattice.
.. image:: _static/sign.png
.. document private methods
.. automethod:: SignLattice._less_equal
.. automethod:: SignLattice._meet
.. automethod:: SignLattice._join
.. automethod:: SignLattice._widening
.. automethod:: SignLattice._neg
.. automethod:: SignLattice._add
.. automethod:: SignLattice._sub
.. automethod:: SignLattice._mult
"""
def __init__(self, negative=True, zero=True, positive=True):
super().__init__()
self._negative = negative
self._zero = zero
self._positive = positive
[docs] @classmethod
def from_literal(cls, literal: Literal) -> 'SignLattice':
if isinstance(literal.typ, BooleanLyraType):
if literal.val == "True":
return cls(False, False, True)
assert literal.val == "False"
return cls(False, True, False)
elif isinstance(literal.typ, IntegerLyraType):
value = int(literal.val)
return cls(value < 0, value == 0, value > 0)
elif isinstance(literal.typ, FloatLyraType):
value = float(literal.val)
return cls(value < 0.0, value == 0.0, value > 0.0)
return cls()
@property
def negative(self):
"""Current negative flag.
:return: the current negative flag
"""
return self._negative
@property
def zero(self):
"""Current zero flag.
:return: the current zero flag
"""
return self._zero
@property
def positive(self):
"""Current positive flag.
:return: the current positive flag
"""
return self._positive
[docs] def is_negative(self) -> bool:
""" Indicates whether the element is certainly negative.
:return: ``True`` if the element is negative.
"""
return self.negative and not self.positive and not self.zero
[docs] def is_zero(self) -> bool:
""" Indicates whether the element is certainly zero.
:return: ``True`` if the element is zero.
"""
return not self.negative and not self.positive and self.zero
[docs] def is_positive(self) -> bool:
""" Indicates whether the element is certainly positive.
:return: ``True`` if the element is positive.
"""
return not self.negative and self.positive and not self.zero
[docs] def maybe_negative(self) -> bool:
""" Indicates whether the element may be negative.
:return: ``True`` if the element may be negative.
"""
return self.negative
[docs] def maybe_zero(self) -> bool:
""" Indicates whether the element may be zero.
:return: ``True`` if the element may be zero.
"""
return self.zero
[docs] def maybe_positive(self) -> bool:
""" Indicates whether the element may be positive.
:return: ``True`` if the element may be positive.
"""
return self.positive
[docs] def maybe_non_negative(self) -> bool:
""" Indicates whether the element may be non-negative.
:return: ``True`` if the element may be non-negative.
"""
return self.zero or self.positive
[docs] def maybe_non_zero(self) -> bool:
""" Indicates whether the element may be non-zero.
:return: ``True`` if the element may be non-zero.
"""
return self.negative or self.positive
[docs] def maybe_non_positive(self) -> bool:
""" Indicates whether the element may be non-positive.
:return: ``True`` if the element may be non-positive.
"""
return self.negative or self.zero
def __repr__(self):
if self.is_top():
return "⊤"
elif self.maybe_negative() and self.maybe_zero():
return "≤0"
elif self.maybe_zero() and self.maybe_positive():
return "≥0"
elif self.maybe_negative() and self.maybe_positive():
return "≠0"
elif self.maybe_negative():
return "<0"
elif self.maybe_positive():
return ">0"
elif self.maybe_zero():
return "=0"
else: # self.is_bottom()
return "⊥"
[docs] @copy_docstring(ArithmeticMixin.bottom)
def bottom(self) -> 'SignLattice':
return self._replace(type(self)(False, False, False))
[docs] @copy_docstring(ArithmeticMixin.top)
def top(self) -> 'SignLattice':
return self._replace(type(self)(True, True, True))
[docs] @copy_docstring(ArithmeticMixin.is_bottom)
def is_bottom(self) -> bool:
return not self.negative and not self.positive and not self.zero
[docs] @copy_docstring(ArithmeticMixin.is_top)
def is_top(self) -> bool:
return self.negative and self.positive and self.zero
[docs] @copy_docstring(ArithmeticMixin._less_equal)
def _less_equal(self, other: 'SignLattice') -> bool:
negative = not self.maybe_negative() or other.maybe_negative()
zero = not self.maybe_zero() or other.maybe_zero()
positive = not self.maybe_positive() or other.maybe_positive()
return negative and zero and positive
[docs] @copy_docstring(ArithmeticMixin._join)
def _join(self, other: 'SignLattice') -> 'SignLattice':
negative = self.maybe_negative() or other.maybe_negative()
zero = self.maybe_zero() or other.maybe_zero()
positive = self.maybe_positive() or other.maybe_positive()
return self._replace(type(self)(negative, zero, positive))
[docs] @copy_docstring(ArithmeticMixin._meet)
def _meet(self, other: 'SignLattice') -> 'SignLattice':
negative = self.maybe_negative() and other.maybe_negative()
zero = self.maybe_zero() and other.maybe_zero()
positive = self.maybe_positive() and other.maybe_positive()
return self._replace(type(self)(negative, zero, positive))
[docs] @copy_docstring(ArithmeticMixin._widening)
def _widening(self, other: 'SignLattice') -> 'SignLattice':
return self._join(other)
# arithmetic operations
[docs] @copy_docstring(ArithmeticMixin._neg)
def _neg(self) -> 'SignLattice':
negative = self.maybe_positive()
zero = self.maybe_zero()
positive = self.maybe_negative()
return self._replace(type(self)(negative, zero, positive))
[docs] def _add(self, other: 'SignLattice') -> 'SignLattice':
negative = self.maybe_negative() or other.maybe_negative()
positive = self.maybe_positive() or other.maybe_positive()
zero = (self.maybe_zero() and other.maybe_zero()) or \
(self.maybe_negative() and other.maybe_positive()) or \
(self.maybe_positive() and other.maybe_negative())
return self._replace(type(self)(negative, zero, positive))
[docs] def _sub(self, other: 'SignLattice') -> 'SignLattice':
negative = self.maybe_negative() or other.maybe_positive()
positive = self.maybe_positive() or other.maybe_negative()
zero = (self.maybe_zero() and other.maybe_zero()) or \
(self.maybe_negative() and other.maybe_negative()) or \
(self.maybe_positive() and other.maybe_positive())
return self._replace(type(self)(negative, zero, positive))
[docs] def _mult(self, other: 'SignLattice') -> 'SignLattice':
negative = (self.maybe_negative() and other.maybe_positive()) or \
(self.maybe_positive() and other.maybe_negative())
positive = (self.maybe_negative() and other.maybe_negative()) or \
(self.maybe_positive() and other.maybe_positive())
zero = self.maybe_zero() or other.maybe_zero()
return self._replace(type(self)(negative, zero, positive))
def _div(self, other: 'SignLattice') -> 'SignLattice':
return self._replace(type(self)())
# boolean operations
[docs] @copy_docstring(BooleanMixin.false)
def false(self) -> 'SignLattice':
"""The false lattice element is ``=0``."""
self._replace(type(self)(False, True, False))
return self
[docs] @copy_docstring(BooleanMixin.true)
def true(self) -> 'SignLattice':
"""The true lattice element is ``>0``."""
self._replace(type(self)(False, False, True))
return self
[docs] @copy_docstring(BooleanMixin.maybe)
def maybe(self) -> 'SignLattice':
"""The maybe lattice element is ``≥0``."""
self._replace(type(self)(False, True, True))
return self
[docs] @copy_docstring(BooleanMixin.is_false)
def is_false(self) -> bool:
return not self.negative and self.zero and not self.positive
[docs] @copy_docstring(BooleanMixin.is_true)
def is_true(self) -> bool:
return not self.negative and not self.zero and self.positive
[docs] @copy_docstring(BooleanMixin.is_maybe)
def is_maybe(self) -> bool:
return not self.negative and self.zero and self.positive
[docs]class SignState(Basis):
"""Sign analysis state. An element of the sign abstract domain.
Map from each program variable to the sign representing its value.
.. document private methods
.. automethod:: SignState._assign
.. automethod:: SignState._assume
.. automethod:: SignState._output
.. automethod:: SignState._substitute
"""
def __init__(self, variables: Set[VariableIdentifier], precursory: State = None):
"""Map each program variable to the sign representing its value.
:param variables: set of program variables
"""
lattices = defaultdict(lambda: SignLattice)
super().__init__(variables, lattices, precursory=precursory)
[docs] @copy_docstring(State._assume)
def _assume(self, condition: Expression) -> 'SignState':
normal = NegationFreeNormalExpression().visit(condition)
if isinstance(normal, VariableIdentifier) and isinstance(normal.typ, BooleanLyraType):
evaluation = self._evaluation.visit(normal, self, dict())
true = self.lattices[normal.typ](**self.arguments[normal.typ]).true()
return self._refinement.visit(normal, evaluation, true, self)
elif isinstance(normal, UnaryBooleanOperation):
if normal.operator == UnaryBooleanOperation.Operator.Neg:
if isinstance(normal.expression, VariableIdentifier):
typ = normal.expression.typ
if isinstance(typ, BooleanLyraType):
evaluation = self._evaluation.visit(normal, self, dict())
false = self.lattices[typ](**self.arguments[typ]).false()
return self._refinement.visit(normal.expression, evaluation, false, self)
elif isinstance(normal, BinaryBooleanOperation):
return self._assume_binarybooleanoperation(normal)
elif isinstance(normal, BinaryComparisonOperation):
evaluation = self._evaluation.visit(normal.left, self, dict())
nonpositive = self.lattices[normal.typ](True, True, False)
return self._refinement.visit(normal.left, evaluation, nonpositive, self)
error = f"Assumption of a {normal.__class__.__name__} expression is unsupported!"
raise ValueError(error)
# expression evaluation
[docs] class ExpressionEvaluation(Basis.ExpressionEvaluation):
"""Visitor that performs the evaluation of an expression in the sign lattice."""
[docs] @copy_docstring(Basis.ExpressionEvaluation.visit_Literal)
def visit_Literal(self, expr: Literal, state=None, evaluation=None):
if expr in evaluation:
return evaluation # nothing to be done
evaluation[expr] = state.lattices[expr.typ].from_literal(expr)
return evaluation
_evaluation = ExpressionEvaluation() # static class member shared between instances