"""
Interval 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 as an interval.
:Authors: Caterina Urban and Simon Wehrli
"""
from collections import defaultdict
from copy import deepcopy
from math import inf
from lyra.abstract_domains.basis import Basis
from lyra.abstract_domains.lattice import BottomMixin, ArithmeticMixin, BooleanMixin, SequenceMixin
from lyra.abstract_domains.state import State
from lyra.core.expressions import *
from lyra.core.utils import copy_docstring
from lyra.core.types import BooleanLyraType, IntegerLyraType, FloatLyraType
[docs]class IntervalLattice(BottomMixin, ArithmeticMixin, BooleanMixin, SequenceMixin):
"""Interval lattice. The bottom interval represents an empty set.
.. image:: _static/interval.jpg
The default abstraction is the unbounded interval ``[-oo, +oo]``.
.. document private methods
.. automethod:: IntervalLattice._less_equal
.. automethod:: IntervalLattice._meet
.. automethod:: IntervalLattice._join
.. automethod:: IntervalLattice._widening
.. automethod:: IntervalLattice._neg
.. automethod:: IntervalLattice._add
.. automethod:: IntervalLattice._sub
.. automethod:: IntervalLattice._mult
"""
def __init__(self, lower=-inf, upper=inf):
super().__init__()
if lower <= upper: # the interval is not empty
self._lower = lower
self._upper = upper
else: # the interval is empty
self.bottom()
[docs] @classmethod
def from_literal(cls, literal: Literal) -> 'IntervalLattice':
if isinstance(literal.typ, BooleanLyraType):
if literal.val == "True":
return cls().true()
assert literal.val == "False"
return cls().false()
elif isinstance(literal.typ, IntegerLyraType):
value = int(literal.val)
return cls(value, value)
elif isinstance(literal.typ, FloatLyraType):
value = float(literal.val)
return cls(value, value)
return cls()
@property
def lower(self):
"""Current lower bound.
:return: the current lower bound if the interval is not empty, ``None`` otherwise
"""
if self.is_bottom():
return None
return self._lower
@property
def upper(self):
"""Current upper bound.
:return: the current upper bound if the interval is not empty, ``None`` otherwise
"""
if self.is_bottom():
return None
return self._upper
def __repr__(self):
if self.is_bottom():
return "⊥"
return f"[{self.lower}, {self.upper}]"
[docs] @copy_docstring(BottomMixin.top)
def top(self) -> 'IntervalLattice':
"""The top lattice element is ``[-oo,+oo]``."""
self._replace(type(self)())
return self
[docs] @copy_docstring(BottomMixin.is_top)
def is_top(self) -> bool:
return self.lower == -inf and self.upper == inf
[docs] @copy_docstring(BottomMixin._less_equal)
def _less_equal(self, other: 'IntervalLattice') -> bool:
"""``[a, b] ⊑ [c, d]`` if and only if ``c <= a`` and ``b <= d``."""
return other.lower <= self.lower and self.upper <= other.upper
[docs] @copy_docstring(BottomMixin._join)
def _join(self, other: 'IntervalLattice') -> 'IntervalLattice':
"""``[a, b] ⊔ [c, d] = [min(a,c), max(b,d)]``."""
lower = min(self.lower, other.lower)
upper = max(self.upper, other.upper)
return self._replace(type(self)(lower, upper))
[docs] @copy_docstring(BottomMixin._meet)
def _meet(self, other: 'IntervalLattice') -> 'IntervalLattice':
"""``[a, b] ⊓ [c, d] = [max(a,c), min(b,d)]``."""
lower = max(self.lower, other.lower)
upper = min(self.upper, other.upper)
if lower <= upper:
return self._replace(type(self)(lower, upper))
return self.bottom()
[docs] @copy_docstring(BottomMixin._widening)
def _widening(self, other: 'IntervalLattice') -> 'IntervalLattice':
"""``[a, b] ▽ [c, d] = [(c < a ? -oo : a), (b < d ? +oo : b)]``."""
lower = self.lower
upper = self.upper
if other.lower < self.lower:
lower = -inf
if self.upper < other.upper:
upper = inf
return self._replace(type(self)(lower, upper))
# arithmetic operations
[docs] @copy_docstring(ArithmeticMixin._neg)
def _neg(self) -> 'IntervalLattice':
"""``- [a, b] = [-b, -a]``."""
lower = 0 - self.upper
upper = 0 - self.lower
return self._replace(type(self)(lower, upper))
[docs] @copy_docstring(ArithmeticMixin._add)
def _add(self, other: 'IntervalLattice') -> 'IntervalLattice':
"""``[a, b] + [c, d] = [a + c, b + d]``."""
lower = 0 + self.lower + other.lower
upper = 0 + self.upper + other.upper
return self._replace(type(self)(lower, upper))
[docs] @copy_docstring(ArithmeticMixin._sub)
def _sub(self, other: 'IntervalLattice') -> 'IntervalLattice':
"""``[a, b] - [c, d] = [a - d, b - c]``."""
lower = 0 + self.lower - other.upper
upper = 0 + self.upper - other.lower
return self._replace(type(self)(lower, upper))
[docs] @copy_docstring(ArithmeticMixin._mult)
def _mult(self, other: 'IntervalLattice') -> 'IntervalLattice':
"""``[a, b] * [c, d] = [min(a*c, a*d, b*c, b*d), max(a*c, a*d, b*c, b*d)]``."""
ac = 0 if self.lower == 0 or other.lower == 0 else 1 * self.lower * other.lower
ad = 0 if self.lower == 0 or other.upper == 0 else 1 * self.lower * other.upper
bc = 0 if self.upper == 0 or other.lower == 0 else 1 * self.upper * other.lower
bd = 0 if self.upper == 0 or other.upper == 0 else 1 * self.upper * other.upper
lower = min(ac, ad, bc, bd)
upper = max(ac, ad, bc, bd)
return self._replace(type(self)(lower, upper))
@copy_docstring(ArithmeticMixin._div)
def _div(self, other: 'IntervalLattice') -> 'IntervalLattice':
return self._replace(type(self)())
# boolean operations
[docs] @copy_docstring(BooleanMixin.false)
def false(self) -> 'IntervalLattice':
"""The false lattice element is ``[0,0]``."""
self._replace(type(self)(0, 0))
return self
[docs] @copy_docstring(BooleanMixin.true)
def true(self) -> 'IntervalLattice':
"""The true lattice element is ``[1,1]``."""
self._replace(type(self)(1, 1))
return self
[docs] @copy_docstring(BooleanMixin.maybe)
def maybe(self) -> 'IntervalLattice':
"""The maybe lattice element is ``[0,1]``."""
self._replace(type(self)(0, 1))
return self
[docs] @copy_docstring(BooleanMixin.is_false)
def is_false(self) -> bool:
return self.lower == 0 and self.upper == 0
[docs] @copy_docstring(BooleanMixin.is_true)
def is_true(self) -> bool:
return self.lower == 1 and self.upper == 1
[docs] @copy_docstring(BooleanMixin.is_maybe)
def is_maybe(self) -> bool:
return self.lower == 0 and self.upper == 1
# string operations
@copy_docstring(SequenceMixin._concat)
def _concat(self, other: 'IntervalLattice'):
return self.join(other)
[docs]class IntervalState(Basis):
"""Interval analysis state. An element of the interval abstract domain.
Map from each program variable to the interval representing its value.
The value of all program variables is represented by the unbounded interval by default.
.. note:: Program variables storing lists are abstracted via summarization.
.. document private methods
.. automethod:: IntervalState._assign
.. automethod:: IntervalState._assume
.. automethod:: IntervalState._output
.. automethod:: IntervalState._substitute
"""
def __init__(self, variables: Set[VariableIdentifier], precursory: State = None):
"""Map each program variable to the interval representing its value.
:param variables: set of program variables
"""
lattices = defaultdict(lambda: IntervalLattice)
super().__init__(variables, lattices, precursory=precursory)
[docs] @copy_docstring(Basis._assume)
def _assume(self, condition: Expression) -> 'IntervalState':
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:
expression = normal.expression
if isinstance(expression, VariableIdentifier):
typ = expression.typ
if isinstance(expression.typ, BooleanLyraType):
evaluation = self._evaluation.visit(normal, self, dict())
false = self.lattices[typ](**self.arguments[typ]).false()
return self._refinement.visit(expression, evaluation, false, self)
elif isinstance(normal, BinaryBooleanOperation):
return self._assume_binarybooleanoperation(normal)
elif isinstance(normal, BinaryComparisonOperation):
if normal.operator == BinaryComparisonOperation.Operator.Is:
error = f"Assumption of a comparison with {normal.operator} is unsupported!"
raise ValueError(error)
elif normal.operator == BinaryComparisonOperation.Operator.IsNot:
error = f"Assumption of a comparison with {normal.operator} is unsupported!"
raise ValueError(error)
elif normal.operator == BinaryComparisonOperation.Operator.In:
if isinstance(normal.right, Range):
typ = BooleanLyraType()
left = normal.left
lower_operator = BinaryComparisonOperation.Operator.GtE
lower_right = normal.right.start
lower = BinaryComparisonOperation(typ, left, lower_operator, lower_right)
upper_operator = BinaryComparisonOperation.Operator.Lt
upper_right = normal.right.stop
upper = BinaryComparisonOperation(typ, left, upper_operator, upper_right)
right = deepcopy(self)._assume(upper)
return self._assume(lower).meet(right)
elif normal.operator == BinaryComparisonOperation.Operator.NotIn:
if isinstance(normal.right, Range):
typ = BooleanLyraType()
left = normal.left
lower_operator = BinaryComparisonOperation.Operator.Lt
lower_right = normal.right.start
lower = BinaryComparisonOperation(typ, left, lower_operator, lower_right)
upper_operator = BinaryComparisonOperation.Operator.GtE
upper_right = normal.right.stop
upper = BinaryComparisonOperation(typ, left, upper_operator, upper_right)
right = deepcopy(self)._assume(upper)
return self._assume(lower).join(right)
evaluation = self._evaluation.visit(normal.left, self, dict())
nonpositive = self.lattices[normal.typ](upper=0)
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 interval 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 all instances