lyra.abstract_domains package

Subpackages

• lyra.abstract_domains.assumption package
  • Submodules
    • Alphabet Abstract Domain
    • Assumption Abstract Domains
    • Quantity Abstract Domain
    • Range Abstract Domain
    • Type Abstract Domain
• lyra.abstract_domains.liveness package
  • Submodules
    • Live Variable Abstract Domains
• lyra.abstract_domains.numerical package
  • Submodules
    • Interval Abstract Domain
    • Sign Abstract Domain
• lyra.abstract_domains.string package
  • Submodules
    • Character Inclusion Abstract Domain
• lyra.abstract_domains.usage package
  • Submodules
    • Syntactic Usage Abstract Domain
    • Usage Lattices

Submodules

Basis Abstract Domain

Interface of an abstract domain mapping variables to lattice elements.

Author:Caterina Urban

class lyra.abstract_domains.basis.Basis(variables: typing.Set[lyra.core.expressions.VariableIdentifier], lattices: typing.Dict[lyra.core.types.LyraType, typing.Type[lyra.abstract_domains.lattice.Lattice]], arguments: typing.Dict[lyra.core.types.LyraType, typing.Dict[str, typing.Any]] = defaultdict(<function Basis.<lambda>>, {}), precursory: lyra.abstract_domains.state.State = None)

Bases: lyra.abstract_domains.store.Store, lyra.abstract_domains.state.State

Analysis basic state. A mutable element of a basis abstract domain.

Warning

Lattice operations and statements modify the current state.

class ExpressionEvaluation

Bases: lyra.core.expressions.ExpressionVisitor

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

visit_AttributeReference(expr: lyra.core.expressions.AttributeReference, state=None, evaluation=None)

Visit of an attribute reference.

visit_BinaryArithmeticOperation(expr, state=None, evaluation=None)

Visit of a binary arithmetic operation.

visit_BinaryBooleanOperation(expr, state=None, evaluation=None)

Visit of a binary boolean operation.

visit_BinaryComparisonOperation(expr, state=None, evaluation=None)

Visit of a binary comparison operation.

visit_BinarySequenceOperation(expr, state=None, evaluation=None)

Visit of a binary sequence operation.

visit_DictDisplay(expr: lyra.core.expressions.DictDisplay, state=None, evaluation=None)

Visit of dictionary display.

visit_Input(expr: lyra.core.expressions.Input, state=None, evaluation=None)

Visit of an input call expression.

visit_LengthIdentifier(expr: lyra.core.expressions.LengthIdentifier, state=None, evaluation=None)

Visit of a sequence or collection length.

visit_ListDisplay(expr: lyra.core.expressions.ListDisplay, state=None, evaluation=None)

Visit of a list display.

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

Visit of a literal expression.

visit_Range(expr: lyra.core.expressions.Range, state=None, evaluation=None)

Visit of a range call expression.

visit_SetDisplay(expr: lyra.core.expressions.SetDisplay, state=None, evaluation=None)

Visit of a set display.

visit_Slicing(expr: lyra.core.expressions.Slicing, state=None, evaluation=None)

Visit of a slicing expression.

visit_Subscription(expr: lyra.core.expressions.Subscription, state=None, evaluation=None)

Visit of a subscription expression.

visit_TupleDisplay(expr: lyra.core.expressions.TupleDisplay, state=None, evaluation=None)

Visit of a tuple display.

visit_UnaryArithmeticOperation(expr, state=None, evaluation=None)

Visit of a unary arithmetic operation.

visit_UnaryBooleanOperation(expr, state=None, evaluation=None)

Visit of a unary boolean operation.

visit_VariableIdentifier(expr: lyra.core.expressions.VariableIdentifier, state=None, evaluation=None)

Visit of a variable identifier.

class ExpressionRefinement

Bases: lyra.core.expressions.ExpressionVisitor

Visitor that:

1. refines the value of an evaluated expression based on a given lattice element; and
2. modifies the current state based on the refined value of the expression.

visit_AttributeReference(expr, evaluation=None, value=None, state=None)

Visit of an attribute reference.

visit_BinaryArithmeticOperation(expr, evaluation=None, value=None, state=None)

Visit of a binary arithmetic operation.

visit_BinaryBooleanOperation(expr, evaluation=None, value=None, state=None)

Visit of a binary boolean operation.

visit_BinaryComparisonOperation(expr, evaluation=None, value=None, state=None)

Visit of a binary comparison operation.

visit_BinarySequenceOperation(expr, evaluation=None, value=None, state=None)

Visit of a binary sequence operation.

visit_DictDisplay(expr: lyra.core.expressions.DictDisplay, evaluation=None, value=None, state=None)

Visit of dictionary display.

visit_Input(expr: lyra.core.expressions.Input, evaluation=None, value=None, state=None)

Visit of an input call expression.

visit_LengthIdentifier(expr, evaluation=None, value=None, state=None)

Visit of a sequence or collection length.

visit_ListDisplay(expr: lyra.core.expressions.ListDisplay, evaluation=None, value=None, state=None)

Visit of a list display.

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

Visit of a literal expression.

visit_Range(expr: lyra.core.expressions.Range, state=None, evaluation=None)

Visit of a range call expression.

visit_SetDisplay(expr: lyra.core.expressions.SetDisplay, evaluation=None, value=None, state=None)

Visit of a set display.

visit_Slicing(expr: lyra.core.expressions.Slicing, evaluation=None, value=None, state=None)

Visit of a slicing expression.

visit_Subscription(expr: lyra.core.expressions.Subscription, evaluation=None, value=None, state=None)

Visit of a subscription expression.

visit_TupleDisplay(expr: lyra.core.expressions.TupleDisplay, evaluation=None, value=None, state=None)

Visit of a tuple display.

visit_UnaryArithmeticOperation(expr, evaluation=None, value=None, state=None)

Visit of a unary arithmetic operation.

visit_UnaryBooleanOperation(expr, evaluation=None, value=None, state=None)

Visit of a unary boolean operation.

visit_VariableIdentifier(expr, evaluation=None, value=None, state=None)

Visit of a variable identifier.

class LengthEvaluation

Bases: lyra.core.expressions.ExpressionVisitor

Visitor that computes the length of an expression corresponding to a sequence type.

visit_AttributeReference(expr: lyra.core.expressions.AttributeReference, state=None, evaluation=None)

Visit of an attribute reference.

visit_BinaryArithmeticOperation(expr, state=None, evaluation=None)

Visit of a binary arithmetic operation.

visit_BinaryBooleanOperation(expr, state=None, evaluation=None)

Visit of a binary boolean operation.

visit_BinaryComparisonOperation(expr, state=None, evaluation=None)

Visit of a binary comparison operation.

visit_BinarySequenceOperation(expr, state=None, evaluation=None)

Visit of a binary sequence operation.

visit_DictDisplay(expr: lyra.core.expressions.DictDisplay, state=None, evaluation=None)

Visit of dictionary display.

visit_Input(expr: lyra.core.expressions.Input, state=None, evaluation=None)

Visit of an input call expression.

visit_LengthIdentifier(expr: lyra.core.expressions.LengthIdentifier, state=None, evaluation=None)

Visit of a sequence or collection length.

visit_ListDisplay(expr: lyra.core.expressions.ListDisplay, state=None, evaluation=None)

Visit of a list display.

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

Visit of a literal expression.

visit_Range(expr: lyra.core.expressions.Range, state=None, evaluation=None)

Visit of a range call expression.

visit_SetDisplay(expr: lyra.core.expressions.SetDisplay, state=None, evaluation=None)

Visit of a set display.

visit_Slicing(expr: lyra.core.expressions.Slicing, state=None, evaluation=None)

Visit of a slicing expression.

visit_Subscription(expr: lyra.core.expressions.Subscription, state=None, evaluation=None)

Visit of a subscription expression.

visit_TupleDisplay(expr: lyra.core.expressions.TupleDisplay, state=None, evaluation=None)

Visit of a tuple display.

visit_UnaryArithmeticOperation(expr, state=None, evaluation=None)

Visit of a unary arithmetic operation.

visit_UnaryBooleanOperation(expr, state=None, evaluation=None)

Visit of a unary boolean operation.

visit_VariableIdentifier(expr: lyra.core.expressions.VariableIdentifier, state=None, evaluation=None)

Visit of a variable identifier.

enter_if()

Enter a conditional if statement.

Warning

The current state could also be bottom or top.

Returns:current state modified to enter a conditional if statement

enter_loop()

Enter a loop.

Warning

The current state could also be bottom or top.

Returns:current state modified to enter a loop

exit_if()

Exit a conditional if statement.

Warning

The current state could also be bottom or top.

Returns:current state modified to enter a conditional if statement

exit_loop()

Exit a loop.

Warning

The current state could also be bottom or top.

Returns:current state modified to exit a loop

is_bottom() → bool

Test whether the lattice element is bottom.

Returns:whether the lattice element is bottom

The current state is bottom if any non-summary variable maps to a bottom element.

Lattice

Interface of a lattice. Lattice elements support lattice operations.

Author:Caterina Urban

class lyra.abstract_domains.lattice.ArithmeticMixin

Bases: lyra.abstract_domains.lattice.Lattice

Mixin to add arithmetic operations to a lattice.

add(other: lyra.abstract_domains.lattice.ArithmeticMixin) → lyra.abstract_domains.lattice.ArithmeticMixin

Addition between two lattice elements.

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

div(other: lyra.abstract_domains.lattice.ArithmeticMixin) → lyra.abstract_domains.lattice.ArithmeticMixin

Multiplication between two lattice elements.

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

mult(other: lyra.abstract_domains.lattice.ArithmeticMixin) → lyra.abstract_domains.lattice.ArithmeticMixin

Multiplication between two lattice elements.

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

neg() → lyra.abstract_domains.lattice.ArithmeticMixin

Negation of a lattice elements.

Returns:current lattice element modified to be its negation

sub(other: lyra.abstract_domains.lattice.ArithmeticMixin) → lyra.abstract_domains.lattice.ArithmeticMixin

Subtraction between two lattice elements.

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

class lyra.abstract_domains.lattice.BooleanMixin

Bases: lyra.abstract_domains.lattice.Lattice

Mixin to add boolean operations to a lattice.

compl() → lyra.abstract_domains.lattice.BooleanMixin

Complement of a lattice elements.

Returns:current lattice element modified to be its complement

conj(other: lyra.abstract_domains.lattice.BooleanMixin) → lyra.abstract_domains.lattice.BooleanMixin

Conjunction between two lattice elements.

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

disj(other: lyra.abstract_domains.lattice.BooleanMixin) → lyra.abstract_domains.lattice.BooleanMixin

Disjunction between two lattice elements.

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

false() → lyra.abstract_domains.lattice.BooleanMixin

False lattice element.

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

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_true() → bool

Test whether the lattice element is true.

Returns:whether the lattice element is true

maybe() → lyra.abstract_domains.lattice.BooleanMixin

Maybe lattice element.

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

true() → lyra.abstract_domains.lattice.BooleanMixin

True lattice element.

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

class lyra.abstract_domains.lattice.BottomMixin

Bases: lyra.abstract_domains.lattice.KindMixin

Mixin to add a predefined bottom element to a lattice.

Warning

Subclasses are expected to provide consistent method implementations that check for the eventuality of is_bottom() being true.

bottom()

Bottom lattice element.

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

is_bottom() → bool

Test whether the lattice element is bottom.

Returns:whether the lattice element is bottom

class lyra.abstract_domains.lattice.BoundedLattice

Bases: lyra.abstract_domains.lattice.TopMixin, lyra.abstract_domains.lattice.BottomMixin

Mutable lattice element, with predefined bottom and top elements.

Warning

Lattice operations modify the current lattice element.

bottom() → lyra.abstract_domains.lattice.BoundedLattice

Bottom lattice element.

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

is_bottom() → bool

Test whether the lattice element is bottom.

Returns:whether the lattice element is bottom

is_top() → bool

Test whether the lattice element is top.

Returns:whether the lattice element is top

top() → lyra.abstract_domains.lattice.BoundedLattice

Top lattice element.

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

class lyra.abstract_domains.lattice.KindMixin

Bases: lyra.abstract_domains.lattice.Lattice

Mixin to add an explicit distinction between bottom, default, and top lattice elements.

class Kind

Bases: enum.Enum

Kind of a lattice element.

BOTTOM = 1

DEFAULT = 2

TOP = 3

kind

The kind of the current lattice element.

class lyra.abstract_domains.lattice.Lattice

Bases: object

Mutable lattice element.

Warning

Lattice operations modify the current lattice element.

Subclasses are expected to provide consistent method implementations for bottom(), is_bottom(), top() and is_top().

big_join(elements: typing.List[_ForwardRef(‘Lattice’)]) → lyra.abstract_domains.lattice.Lattice

Least upper bound between multiple lattice elements.

Parameters:elements – lattice elements to compute the least upper bound of Returns:current lattice element modified to be the least upper bound

big_meet(elements: typing.List[_ForwardRef(‘Lattice’)]) → lyra.abstract_domains.lattice.Lattice

Greatest lower bound between multiple lattice elements.

Parameters:elements – lattice elements to compute the greatest lower bound of Returns:current lattice element modified to be the least upper bound

bottom()

Bottom lattice element.

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

is_bottom() → bool

Test whether the lattice element is bottom.

Returns:whether the lattice element is bottom

is_top() → bool

Test whether the lattice element is top.

Returns:whether the lattice element is top

join(other: lyra.abstract_domains.lattice.Lattice) → lyra.abstract_domains.lattice.Lattice

Least upper bound between lattice elements.

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

less_equal(other: lyra.abstract_domains.lattice.Lattice) → bool

Partial order between 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.lattice.Lattice)

Greatest lower bound between lattice elements.

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

top()

Top lattice element.

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

widening(other: lyra.abstract_domains.lattice.Lattice)

Widening between lattice elements.

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

class lyra.abstract_domains.lattice.SequenceMixin

Bases: lyra.abstract_domains.lattice.Lattice

Mixin to add sequence operations to a lattice.

concat(other: lyra.abstract_domains.lattice.SequenceMixin) → lyra.abstract_domains.lattice.SequenceMixin

Concatenation between two lattice elements.

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

class lyra.abstract_domains.lattice.TopMixin

Bases: lyra.abstract_domains.lattice.KindMixin

Mixin to add a predefined top element to another lattice.

Warning

Subclasses are expected to provide consistent method implementations that check for the eventuality of is_top() being true.

is_top() → bool

Test whether the lattice element is top.

Returns:whether the lattice element is top

top()

Top lattice element.

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

Stack

Stack of lattices.

Authors:Caterina Urban and Simon Wehrli

class lyra.abstract_domains.stack.Stack(lattice: typing.Type, arguments: typing.Dict[str, typing.Any])

Bases: lyra.abstract_domains.lattice.BoundedLattice

Mutable stack of elements of a lattice.

Warning

Lattice operations modify the current stack.

_less_equal(other: lyra.abstract_domains.stack.Stack) → 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

The comparison is performed point-wise for each stack element.

_meet(other: lyra.abstract_domains.stack.Stack)

Greatest lower bound between default lattice elements.

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

The meet is performed point-wise for each stack element.

_join(other: lyra.abstract_domains.stack.Stack) → lyra.abstract_domains.stack.Stack

Least upper bound between default lattice elements.

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

The join is performed point-wise for each stack element.

lattice

Lattice element currently on top of the stack.

pop()

Pop an element from the current stack.

push()

Push an element on the current stack.

stack

Current stack of lattice elements.

Abstract Domain

Interface of an abstract domain. Abstract domain elements support lattice operations and program statements.

Author:Caterina Urban

class lyra.abstract_domains.state.EnvironmentMixin(precursory: typing.Union[lyra.abstract_domains.state.State, NoneType] = None)

Bases: lyra.abstract_domains.state.State

Mixin to add environment modification operations to another state.

add_variable(variable: lyra.core.expressions.VariableIdentifier)

Add a variable.

Parameters:variable – variable to be added Returns:current state modified by the variable addition

forget_variable(variable: lyra.core.expressions.VariableIdentifier)

Forget the value of a variable.

Parameters:variable – variable whose value is to be forgotten Returns:current state modified to have value top for the forgotten variable

remove_variable(variable: lyra.core.expressions.VariableIdentifier)

Remove a variable.

Parameters:variable – variable to be removed Returns:current state modified by the variable removal

class lyra.abstract_domains.state.State(precursory: typing.Union[lyra.abstract_domains.state.State, NoneType] = None)

Bases: lyra.abstract_domains.lattice.Lattice

Analysis state. A mutable element of an abstract domain.

Warning

Lattice operations and statements modify the current state.

assign(left: typing.Set[lyra.core.expressions.Expression], right: typing.Set[lyra.core.expressions.Expression]) → lyra.abstract_domains.state.State

Assign an expression to another expression.

Parameters:

• left – set of expressions representing the expression to be assigned to
• right – set of expressions representing the expression to assign

Returns:

current state modified by the assignment

assume(condition: typing.Set[lyra.core.expressions.Expression]) → lyra.abstract_domains.state.State

Assume that some condition holds in the current state.

Parameters:condition – set of expressions representing the assumed condition Returns:current state modified to satisfy the assumption

before(pp: lyra.core.statements.ProgramPoint, precursory: typing.Union[_ForwardRef(‘State’), NoneType]) → lyra.abstract_domains.state.State

Set the program point of the currently analyzed statement and the current precursory analysis state.

Parameters:

• pp – current program point
• precursory – current precursory analysis state

Returns:

current state modified to set the current program point and precursory state

enter_if() → lyra.abstract_domains.state.State

Enter a conditional if statement.

Warning

The current state could also be bottom or top.

Returns:current state modified to enter a conditional if statement

enter_loop() → lyra.abstract_domains.state.State

Enter a loop.

Warning

The current state could also be bottom or top.

Returns:current state modified to enter a loop

exit_if() → lyra.abstract_domains.state.State

Exit a conditional if statement.

Warning

The current state could also be bottom or top.

Returns:current state modified to enter a conditional if statement

exit_loop() → lyra.abstract_domains.state.State

Exit a loop.

Warning

The current state could also be bottom or top.

Returns:current state modified to exit a loop

filter() → lyra.abstract_domains.state.State

Assume that the current result holds in the current state.

Returns:current state modified to satisfy the current result

output(output: typing.Set[lyra.core.expressions.Expression]) → lyra.abstract_domains.state.State

Outputs something in the current state.

Parameters:output – set of expressions representing the output Returns:current state modified by the output

pp

Program point of the currently analyzed statement.

precursory

Current precursory analysis state.

raise_error() → lyra.abstract_domains.state.State

Raise an error.

Returns:current state modified to be the bottom state

result

Result of the previously analyzed statement.

substitute(left: typing.Set[lyra.core.expressions.Expression], right: typing.Set[lyra.core.expressions.Expression]) → lyra.abstract_domains.state.State

Substitute an expression to another expression.

Parameters:

• left – set of expressions representing the expression to be substituted
• right – set of expressions representing the expression to substitute

Returns:

current state modified by the substitution

Store

Lifting of a lattice to a set of program variables.

Authors:Caterina Urban and Simon Wehrli

class lyra.abstract_domains.store.Store(variables: typing.Set[lyra.core.expressions.VariableIdentifier], lattices: typing.Dict[lyra.core.types.LyraType, typing.Type[lyra.abstract_domains.lattice.Lattice]], arguments: typing.Dict[lyra.core.types.LyraType, typing.Dict[str, typing.Any]] = defaultdict(<function Store.<lambda>>, {}))

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

_less_equal(other: lyra.abstract_domains.store.Store) → 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

The comparison is performed point-wise for each variable.

_meet(other: lyra.abstract_domains.store.Store)

Greatest lower bound between default lattice elements.

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

The meet is performed point-wise for each variable.

_join(other: lyra.abstract_domains.store.Store) → lyra.abstract_domains.store.Store

Least upper bound between default lattice elements.

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

The join is performed point-wise for each variable.

arguments

Current dictionary from variable types to argument of the corresponding lattices.

bottom() → lyra.abstract_domains.store.Store

Bottom lattice element.

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

is_bottom() → bool

Test whether the lattice element is bottom.

Returns:whether the lattice element is bottom

The current store is bottom if any of its variables map to a bottom element.

is_top() → bool

Test whether the lattice element is top.

Returns:whether the lattice element is top

The current store is top if all of its variables map to a top element.

lattices

Current dictionary fro variable types to the corresponding lattice types.

store

Current mapping from variables to their corresponding lattice element.

top() → lyra.abstract_domains.store.Store

Top lattice element.

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

variables

Variables of the current store.