lyra.abstract_domains.numerical package

Submodules

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

class lyra.abstract_domains.numerical.interval_domain.IntervalLattice(lower=-inf, upper=inf)

Bases: lyra.abstract_domains.lattice.BottomMixin, lyra.abstract_domains.lattice.ArithmeticMixin, lyra.abstract_domains.lattice.BooleanMixin, lyra.abstract_domains.lattice.SequenceMixin

Interval lattice. The bottom interval represents an empty set.

The default abstraction is the unbounded interval [-oo, +oo].

_less_equal(other: lyra.abstract_domains.numerical.interval_domain.IntervalLattice) → bool

Partial order between default lattice elements.

Parameters:other – other lattice element Returns:whether the current lattice element is less than or equal to the other element

[a, b] ⊑ [c, d] if and only if c <= a and b <= d.

_meet(other: lyra.abstract_domains.numerical.interval_domain.IntervalLattice) → lyra.abstract_domains.numerical.interval_domain.IntervalLattice

Greatest lower bound between default lattice elements.

Parameters:other – other lattice element Returns:current lattice element modified to be the greatest lower bound

[a, b] ⊓ [c, d] = [max(a,c), min(b,d)].

_join(other: lyra.abstract_domains.numerical.interval_domain.IntervalLattice) → lyra.abstract_domains.numerical.interval_domain.IntervalLattice

Least upper bound between default lattice elements.

Parameters:other – other lattice element Returns:current lattice element modified to be the least upper bound

[a, b] ⊔ [c, d] = [min(a,c), max(b,d)].

_widening(other: lyra.abstract_domains.numerical.interval_domain.IntervalLattice) → lyra.abstract_domains.numerical.interval_domain.IntervalLattice

Widening between default lattice elements.

Parameters:other – other lattice element Returns:current lattice element modified to be the widening

[a, b] ▽ [c, d] = [(c < a ? -oo : a), (b < d ? +oo : b)].

_neg() → lyra.abstract_domains.numerical.interval_domain.IntervalLattice

Negation of a default lattice elements.

Returns:current lattice element modified to be its negation

- [a, b] = [-b, -a].

_add(other: lyra.abstract_domains.numerical.interval_domain.IntervalLattice) → lyra.abstract_domains.numerical.interval_domain.IntervalLattice

Addition between two default lattice elements.

Parameters:other – other lattice element Returns:current lattice element modified to be the sum

[a, b] + [c, d] = [a + c, b + d].

_sub(other: lyra.abstract_domains.numerical.interval_domain.IntervalLattice) → lyra.abstract_domains.numerical.interval_domain.IntervalLattice

Subtraction between two default lattice elements.

Parameters:other – other lattice element Returns:current lattice element modified to be the difference

[a, b] - [c, d] = [a - d, b - c].

_mult(other: lyra.abstract_domains.numerical.interval_domain.IntervalLattice) → lyra.abstract_domains.numerical.interval_domain.IntervalLattice

Multiplication between two default lattice elements.

Parameters:other – other lattice element Returns:current lattice element modified to be the product

[a, b] * [c, d] = [min(a*c, a*d, b*c, b*d), max(a*c, a*d, b*c, b*d)].

false() → lyra.abstract_domains.numerical.interval_domain.IntervalLattice

False lattice element.

Returns:current lattice element modified to be the false lattice element

The false lattice element is [0,0].

classmethod from_literal(literal: lyra.core.expressions.Literal) → lyra.abstract_domains.numerical.interval_domain.IntervalLattice

is_false() → bool

Test whether the lattice element is false.

Returns:whether the lattice element is false

is_maybe() → bool

Test whether the lattice element is maybe.

Returns:whether the lattice element is maybe

is_top() → bool

Test whether the lattice element is top.

Returns:whether the lattice element is top

is_true() → bool

Test whether the lattice element is true.

Returns:whether the lattice element is true

lower

Current lower bound.

Returns:the current lower bound if the interval is not empty, None otherwise

maybe() → lyra.abstract_domains.numerical.interval_domain.IntervalLattice

Maybe lattice element.

Returns:current lattice element modified to be the maybe lattice element

The maybe lattice element is [0,1].

top() → lyra.abstract_domains.numerical.interval_domain.IntervalLattice

Top lattice element.

Returns:current lattice element modified to be the top lattice element

The top lattice element is [-oo,+oo].

true() → lyra.abstract_domains.numerical.interval_domain.IntervalLattice

True lattice element.

Returns:current lattice element modified to be the true lattice element

The true lattice element is [1,1].

upper

Current upper bound.

Returns:the current upper bound if the interval is not empty, None otherwise

class lyra.abstract_domains.numerical.interval_domain.IntervalState(variables: typing.Set[lyra.core.expressions.VariableIdentifier], precursory: lyra.abstract_domains.state.State = None)

Bases: lyra.abstract_domains.basis.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.

_assign(left: lyra.core.expressions.Expression, right: lyra.core.expressions.Expression) → lyra.abstract_domains.basis.Basis

Assign an expression to another expression.

Warning

The current state could also be bottom or top.

Parameters:

• left – expression to be assigned to
• right – expression to assign

Returns:

current state modified by the assignment

_assume(condition: lyra.core.expressions.Expression) → lyra.abstract_domains.numerical.interval_domain.IntervalState

Assume that some condition holds in the current state.

Warning

The current state could also be bottom or top.

Parameters:condition – expression representing the assumed condition Returns:current state modified to satisfy the assumption

_output(output: lyra.core.expressions.Expression) → lyra.abstract_domains.basis.Basis

Outputs something in the current state.

Warning

The current state could also be bottom or top.

Parameters:output – expression representing the output Returns:current state modified by the output

_substitute(left: lyra.core.expressions.Expression, right: lyra.core.expressions.Expression)

Substitute an expression to another expression.

Warning

The current state could also be bottom or top.

Parameters:

• left – expression to be substituted
• right – expression to substitute

Returns:

current state modified by the substitution

class ExpressionEvaluation

Bases: lyra.abstract_domains.basis.ExpressionEvaluation

Visitor that performs the evaluation of an expression in the interval lattice.

visit_Literal(expr: lyra.core.expressions.Literal, state=None, evaluation=None)

Visit of a literal expression.

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

class lyra.abstract_domains.numerical.sign_domain.SignLattice(negative=True, zero=True, positive=True)

Bases: lyra.abstract_domains.lattice.ArithmeticMixin, lyra.abstract_domains.lattice.BooleanMixin

Sign lattice.

_less_equal(other: lyra.abstract_domains.numerical.sign_domain.SignLattice) → bool

Partial order between default lattice elements.

Parameters:other – other lattice element Returns:whether the current lattice element is less than or equal to the other element

_meet(other: lyra.abstract_domains.numerical.sign_domain.SignLattice) → lyra.abstract_domains.numerical.sign_domain.SignLattice

Greatest lower bound between default lattice elements.

Parameters:other – other lattice element Returns:current lattice element modified to be the greatest lower bound

_join(other: lyra.abstract_domains.numerical.sign_domain.SignLattice) → lyra.abstract_domains.numerical.sign_domain.SignLattice

Least upper bound between default lattice elements.

Parameters:other – other lattice element Returns:current lattice element modified to be the least upper bound

_widening(other: lyra.abstract_domains.numerical.sign_domain.SignLattice) → lyra.abstract_domains.numerical.sign_domain.SignLattice

Widening between default lattice elements.

Parameters:other – other lattice element Returns:current lattice element modified to be the widening

_neg() → lyra.abstract_domains.numerical.sign_domain.SignLattice

Negation of a default lattice elements.

Returns:current lattice element modified to be its negation

_add(other: lyra.abstract_domains.numerical.sign_domain.SignLattice) → lyra.abstract_domains.numerical.sign_domain.SignLattice

_sub(other: lyra.abstract_domains.numerical.sign_domain.SignLattice) → lyra.abstract_domains.numerical.sign_domain.SignLattice

_mult(other: lyra.abstract_domains.numerical.sign_domain.SignLattice) → lyra.abstract_domains.numerical.sign_domain.SignLattice

bottom() → lyra.abstract_domains.numerical.sign_domain.SignLattice

Bottom lattice element.

Returns:current lattice element modified to be the bottom lattice element

false() → lyra.abstract_domains.numerical.sign_domain.SignLattice

False lattice element.

Returns:current lattice element modified to be the false lattice element

The false lattice element is =0.

classmethod from_literal(literal: lyra.core.expressions.Literal) → lyra.abstract_domains.numerical.sign_domain.SignLattice

is_bottom() → bool

Test whether the lattice element is bottom.

Returns:whether the lattice element is bottom

is_false() → bool

Test whether the lattice element is false.

Returns:whether the lattice element is false

is_maybe() → bool

Test whether the lattice element is maybe.

Returns:whether the lattice element is maybe

is_negative() → bool

Indicates whether the element is certainly negative.

Returns:True if the element is negative.

is_positive() → bool

Indicates whether the element is certainly positive.

Returns:True if the element is positive.

is_top() → bool

Test whether the lattice element is top.

Returns:whether the lattice element is top

is_true() → bool

Test whether the lattice element is true.

Returns:whether the lattice element is true

is_zero() → bool

Indicates whether the element is certainly zero.

Returns:True if the element is zero.

maybe() → lyra.abstract_domains.numerical.sign_domain.SignLattice

Maybe lattice element.

Returns:current lattice element modified to be the maybe lattice element

The maybe lattice element is ≥0.

maybe_negative() → bool

Indicates whether the element may be negative.

Returns:True if the element may be negative.

maybe_non_negative() → bool

Indicates whether the element may be non-negative.

Returns:True if the element may be non-negative.

maybe_non_positive() → bool

Indicates whether the element may be non-positive.

Returns:True if the element may be non-positive.

maybe_non_zero() → bool

Indicates whether the element may be non-zero.

Returns:True if the element may be non-zero.

maybe_positive() → bool

Indicates whether the element may be positive.

Returns:True if the element may be positive.

maybe_zero() → bool

Indicates whether the element may be zero.

Returns:True if the element may be zero.

negative

Current negative flag.

Returns:the current negative flag

positive

Current positive flag.

Returns:the current positive flag

top() → lyra.abstract_domains.numerical.sign_domain.SignLattice

Top lattice element.

Returns:current lattice element modified to be the top lattice element

true() → lyra.abstract_domains.numerical.sign_domain.SignLattice

True lattice element.

Returns:current lattice element modified to be the true lattice element

The true lattice element is >0.

zero

Current zero flag.

Returns:the current zero flag

class lyra.abstract_domains.numerical.sign_domain.SignState(variables: typing.Set[lyra.core.expressions.VariableIdentifier], precursory: lyra.abstract_domains.state.State = None)

Bases: lyra.abstract_domains.basis.Basis

Sign analysis state. An element of the sign abstract domain.

Map from each program variable to the sign representing its value.

_assign(left: lyra.core.expressions.Expression, right: lyra.core.expressions.Expression) → lyra.abstract_domains.basis.Basis

Assign an expression to another expression.

Warning

The current state could also be bottom or top.

Parameters:

• left – expression to be assigned to
• right – expression to assign

Returns:

current state modified by the assignment

_assume(condition: lyra.core.expressions.Expression) → lyra.abstract_domains.numerical.sign_domain.SignState

Assume that some condition holds in the current state.

Warning

The current state could also be bottom or top.

Parameters:condition – expression representing the assumed condition Returns:current state modified to satisfy the assumption

_output(output: lyra.core.expressions.Expression) → lyra.abstract_domains.basis.Basis

Outputs something in the current state.

Warning

The current state could also be bottom or top.

Parameters:output – expression representing the output Returns:current state modified by the output

_substitute(left: lyra.core.expressions.Expression, right: lyra.core.expressions.Expression)

Substitute an expression to another expression.

Warning

The current state could also be bottom or top.

Parameters:

• left – expression to be substituted
• right – expression to substitute

Returns:

current state modified by the substitution

class ExpressionEvaluation

Bases: lyra.abstract_domains.basis.ExpressionEvaluation

Visitor that performs the evaluation of an expression in the sign lattice.

visit_Literal(expr: lyra.core.expressions.Literal, state=None, evaluation=None)

Visit of a literal expression.