lyra.abstract_domains.assumption package

Submodules

Alphabet Abstract Domain

Non-relational abstract domain to be used for input data assumption analysis. The set of possible string values of a program variable in a program state is represented by the sets of characters that must and may form the string.

Authors:Radwa Sherif Abdelbar and Caterina Urban

class lyra.abstract_domains.assumption.alphabet_domain.AlphabetLattice(certainly: typing.Set[str] = set(), maybe: typing.Set[str] = {‘&’, ‘8’, ’, ’, ’$’, ’n’, ‘5’, ’V’, ’o’, ’x’, ’#’, ’s’, ’}’, ’Q’, ’)’, ‘1’, ’M’, ’X’, ’b’, ’I’, ’.’, ’F’, ’h’, ’W’, ’-‘, ’H’, ’T’, ’l’, ’?’, ’_’, ”’”, ‘9’, ’j’, ‘7’, ’O’, ’<’, ’(‘, ’p’, ’{‘, ’x0b’, ’e’, ’R’, ’`’, ’C’, ’D’, ’k’, ’]’, ’f’, ’t’, ’E’, ’q’, ’”’, ‘2’, ’i’, ’=’, ’~’, ’B’, ’|’, ‘4’, ‘0’, ‘3’, ’m’, ’d’, ’L’, ’c’, ’%’, ’P’, ’@’, ’a’, ’U’, ’[‘, ’g’, ’S’, ’r’, ’A’, ’ ‘, ’v’, ’N’, ’n’, ’+’, ’^’, ’', ’r’, ’Z’, ’*’, ’/’, ’w’, ’G’, ’t’, ’!’, ’J’, ’z’, ’>’, ’y’, ‘6’, ’Y’, ’;’, ’u’, ’K’, ’:’, ’x0c’})

Bases: lyra.abstract_domains.string.character_domain.CharacterLattice, lyra.abstract_domains.assumption.assumption_domain.JSONMixin

Alphabet lattice.

The default abstraction is the unconstraining pair (∅, Σ), where Σ denotes the entire alphabet. The bottom element of the lattice represents a contradiction.

_less_equal(other: lyra.abstract_domains.string.character_domain.CharacterLattice) → 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

(c1, m1) ⊑ (c2, m2) if and only if c2 ⊆ c1 and m1 ⊆ m2.

_meet(other: lyra.abstract_domains.string.character_domain.CharacterLattice)

Greatest lower bound between default lattice elements.

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

(c1, m1) ⊓ (c2, m2) = (c1 ∪ c2, m1 ∩ m2).

_join(other: lyra.abstract_domains.string.character_domain.CharacterLattice) → lyra.abstract_domains.string.character_domain.CharacterLattice

Least upper bound between default lattice elements.

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

(c1, m1) ⊔ (c2, m2) = (c1 ∩ c2, m1 ∪ m2).

_widening(other: lyra.abstract_domains.string.character_domain.CharacterLattice)

Widening between default lattice elements.

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

(c1, m1) ▽ (c2, m2) = (c1, m1) ⊔ (c2, m2).

_concat(other: lyra.abstract_domains.string.character_domain.CharacterLattice) → lyra.abstract_domains.string.character_domain.CharacterLattice

Concatenation between two lattice elements.

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

(c1, m1) + (c2, m2) = (c1 ∪ c2, m1 ∪ m2).

static from_json(json: dict) → lyra.abstract_domains.assumption.assumption_domain.JSONMixin

Reconstruct a lattice element from its JSON format.

Parameters:json – JSON format of a lattice element Returns:reconstructed lattice element from its JSON format

to_json() → dict

Convert the current lattice element to JSON format.

Returns:JSON format of the current lattice element

class lyra.abstract_domains.assumption.alphabet_domain.AlphabetState(variables: typing.Set[lyra.core.expressions.VariableIdentifier], precursory: lyra.abstract_domains.assumption.assumption_domain.InputMixin = None)

Bases: lyra.abstract_domains.string.character_domain.CharacterState, lyra.abstract_domains.assumption.assumption_domain.InputMixin

Alphabet analysis state. An element of the alphabet abstract domain.

Map from each program variable to the sets of characters that must and may form its possible string values. The string value of all program variables is unconstrained by default.

When reading input data, the corresponding range assumptions are stored in the class member inputs, which is a map from each program point to the list of range assumptions on the input data read at that point.

_assume(condition: lyra.core.expressions.Expression) → lyra.abstract_domains.state.State

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

_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 ExpressionRefinement

Bases: lyra.abstract_domains.string.character_domain.ExpressionRefinement

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

Visit of an input call expression.

replace(variable: lyra.core.expressions.VariableIdentifier, expression: lyra.core.expressions.Expression) → lyra.abstract_domains.assumption.alphabet_domain.AlphabetState

unify(other: lyra.abstract_domains.assumption.alphabet_domain.AlphabetState) → lyra.abstract_domains.assumption.alphabet_domain.AlphabetState

Assumption Abstract Domains

Abstract domains to be used for input data assumption analysis.

Authors:Caterina Urban and Radwa Sherif Abdelbar

class lyra.abstract_domains.assumption.assumption_domain.AssumptionState(states: typing.List[typing.Type[lyra.abstract_domains.assumption.assumption_domain.InputMixin]], arguments: typing.Dict[typing.Type, typing.Dict[str, typing.Any]] = defaultdict(<function AssumptionState.<lambda>>, {}), precursory: lyra.abstract_domains.state.State = None)

Bases: lyra.abstract_domains.state.State

Assumption analysis state. An element of the assumption abstract domain.

Reduced product of a list of constraining states, which collect constraints on the program variables and (indirectly) on the input data, and a stack of assumptions on the input data, which (directly) constraints the input data read from the current program point.

_assume(condition: lyra.core.expressions.Expression) → lyra.abstract_domains.assumption.assumption_domain.AssumptionState

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

_substitute(left: lyra.core.expressions.Expression, right: lyra.core.expressions.Expression) → lyra.abstract_domains.assumption.assumption_domain.AssumptionState

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 InputStack(precursory: lyra.abstract_domains.state.State = None)

Bases: lyra.abstract_domains.stack.Stack, lyra.abstract_domains.state.State

Stack of assumptions on the input data.

class InputLattice(multiplier: lyra.core.expressions.Expression = <lyra.core.expressions.Literal object>, constraints: typing.List[typing.Union[typing.Tuple[lyra.core.statements.ProgramPoint, …], typing.Tuple[lyra.core.statements.ProgramPoint, typing.Tuple[lyra.abstract_domains.assumption.assumption_domain.JSONMixin, …]], _ForwardRef(‘AssumptionState.InputStack.InputLattice’)]] = [])

Bases: lyra.abstract_domains.lattice.BottomMixin

Assumptions on the input data.

Each assumption is a (possibly symbolic) repetition of constraints on the input data. A constraint can be:

• a basic constraint, i.e., a tuple of lattices (l, …) which indicates that an input data point is expected and restricts its possible value
• a star constraint, i.e., ★ which indicates that any number of input data points is expected
• another symbolically repeated assumption

Let S be the set of all possible sequences of input data points. The concretization function Ɣ: InputLattice -> 𝒫(S) is defined as follows:

Ɣ(1 * [★]) = S
...
Ɣ(1 * [(l1, l2), ★]) = { xs ∈ S | x ∈ Ɣ(l1) ⋂ Ɣ(l2) }
...
Ɣ(n * [(l1, l2)]) = { x^n ∈ S | x ∈ Ɣ(l1) ⋂ Ɣ(l2) }
...
Ɣ(1 * [(l1, l2)]) = { x ∈ S | x ∈ Ɣ(l1) ⋂ Ɣ(l2) }
...
Ɣ(1 * []) = { ε }

BasicConstraint

alias of Tuple

InputConstraint = typing.Union[typing.Tuple[lyra.core.statements.ProgramPoint, …], typing.Tuple[lyra.core.statements.ProgramPoint, typing.Tuple[lyra.abstract_domains.assumption.assumption_domain.JSONMixin, …]], _ForwardRef(‘AssumptionState.InputStack.InputLattice’)]

InputLattice = ‘AssumptionState.InputStack.InputLattice’

StarConstraint

alias of Tuple

constraints

Current list of constraints.

is_top() → bool

Test whether the lattice element is top.

Returns:whether the lattice element is top

multiplier

Current multiplier.

record(constraint: typing.Union[typing.Tuple[lyra.core.statements.ProgramPoint, …], typing.Tuple[lyra.core.statements.ProgramPoint, typing.Tuple[lyra.abstract_domains.assumption.assumption_domain.JSONMixin, …]], _ForwardRef(‘AssumptionState.InputStack.InputLattice’)]) → lyra.abstract_domains.assumption.assumption_domain.AssumptionState.InputStack.InputLattice

Record a constraint on the input data.

By default, the constraint is added to the current list of recorded constraints.

When leaving the body of a for loop another time than the first, the constraint to be recorded is instead merged with the previously recorded constraint.

Parameters:constraint – constraint to be recorded Returns:current lattice element modified to record the constraint

repeat(multiplier: lyra.core.expressions.Expression) → lyra.abstract_domains.assumption.assumption_domain.AssumptionState.InputStack.InputLattice

Repeat the current assumption on the input data.

Parameters:multiplier – repetitions to be performed Returns:current lattice element modified to repeat the assumption

replace(variable: lyra.core.expressions.VariableIdentifier, expression: lyra.core.expressions.Expression)

Replace a variable with an expression.

Parameters:

• variable – variable to be replaced
• expression – expression replacing the variable

Returns:

current lattice element modified to manifest the replacement

top()

Top lattice element.

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

The top lattice element is 1 * [★].

class InputReplacement(pp: lyra.core.statements.ProgramPoint)

Bases: lyra.core.expressions.ExpressionVisitor

Visitor that replaces any occurrence of an input (sub)expression with a fresh variable identifier that depends on a given program point.

Example:

input() - 3 * input()

given the program point [line:L, column:C] becomes:

L.1 - 3 * L.2

nonce

pp

visit_AttributeReference(expr: lyra.core.expressions.AttributeReference)

Visit of an attribute reference.

visit_BinaryArithmeticOperation(expr: lyra.core.expressions.BinaryArithmeticOperation)

Visit of a binary arithmetic operation.

visit_BinaryBooleanOperation(expr: lyra.core.expressions.BinaryBooleanOperation)

Visit of a binary boolean operation.

visit_BinaryComparisonOperation(expr: lyra.core.expressions.BinaryComparisonOperation)

Visit of a binary comparison operation.

visit_BinarySequenceOperation(expr: lyra.core.expressions.BinarySequenceOperation)

Visit of a binary sequence operation.

visit_DictDisplay(expr: lyra.core.expressions.DictDisplay)

Visit of dictionary display.

visit_Input(expr: lyra.core.expressions.Input)

Visit of an input call expression.

visit_LengthIdentifier(expr: lyra.core.expressions.LengthIdentifier)

Visit of a sequence or collection length.

visit_ListDisplay(expr: lyra.core.expressions.ListDisplay)

Visit of a list display.

visit_Literal(expr: lyra.core.expressions.Literal)

Visit of a literal expression.

visit_Range(expr: lyra.core.expressions.Range)

Visit of a range call expression.

visit_SetDisplay(expr: lyra.core.expressions.SetDisplay)

Visit of a set display.

visit_Slicing(expr: lyra.core.expressions.Slicing)

Visit of a slicing expression.

visit_Subscription(expr: lyra.core.expressions.Subscription)

Visit of a subscription expression.

visit_TupleDisplay(expr: lyra.core.expressions.TupleDisplay)

Visit of a tuple display.

visit_UnaryArithmeticOperation(expr: lyra.core.expressions.UnaryArithmeticOperation)

Visit of a unary arithmetic operation.

visit_UnaryBooleanOperation(expr: lyra.core.expressions.UnaryBooleanOperation)

Visit of a unary boolean operation.

visit_VariableIdentifier(expr: lyra.core.expressions.VariableIdentifier)

Visit of a variable identifier.

class Scope

Bases: enum.Enum

Scope type. Either Branch or Loop.

Branch = 0

Loop = 1

enter_if() → lyra.abstract_domains.assumption.assumption_domain.AssumptionState.InputStack

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.assumption.assumption_domain.AssumptionState.InputStack

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.assumption.assumption_domain.AssumptionState.InputStack

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.assumption.assumption_domain.AssumptionState.InputStack

Exit a loop.

Warning

The current state could also be bottom or top.

Returns:current state modified to exit a loop

pop() → lyra.abstract_domains.assumption.assumption_domain.AssumptionState.InputStack

Pop an element from the current stack.

push() → lyra.abstract_domains.assumption.assumption_domain.AssumptionState.InputStack

Push an element on the current stack.

record(constraint: typing.Union[typing.Tuple[lyra.core.statements.ProgramPoint, …], typing.Tuple[lyra.core.statements.ProgramPoint, typing.Tuple[lyra.abstract_domains.assumption.assumption_domain.JSONMixin, …]], _ForwardRef(‘AssumptionState.InputStack.InputLattice’)]) → lyra.abstract_domains.assumption.assumption_domain.AssumptionState.InputStack

Record a constraint on the input data.

Parameters:constraint – constraint to be recorded Returns:current stack modified to record the constraint

scope

Current scope type.

scopes

Current stack of scope types.

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

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

bottom() → lyra.abstract_domains.assumption.assumption_domain.AssumptionState

Bottom lattice element.

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

enter_if() → lyra.abstract_domains.assumption.assumption_domain.AssumptionState

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.assumption.assumption_domain.AssumptionState

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.assumption.assumption_domain.AssumptionState

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.assumption.assumption_domain.AssumptionState

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

is_top() → bool

Test whether the lattice element is top.

Returns:whether the lattice element is top

stack

Current stack of assumptions on the input data.

states

Current list of constraining states.

top() → lyra.abstract_domains.assumption.assumption_domain.AssumptionState

Top lattice element.

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

class lyra.abstract_domains.assumption.assumption_domain.InputMixin(precursory: lyra.abstract_domains.state.State = None)

Bases: lyra.abstract_domains.state.State

Mixin to add a mechanism for recording and retrieving constraints on the input data.

Constraints are recorded in the class member inputs, which is a map from each program point to the list of constraints on the input data read at that point.

join(other: lyra.abstract_domains.assumption.assumption_domain.InputMixin)

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.assumption.assumption_domain.InputMixin)

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.assumption.assumption_domain.InputMixin)

Least upper bound between lattice elements.

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

record(constraint: lyra.abstract_domains.assumption.assumption_domain.JSONMixin) → lyra.abstract_domains.assumption.assumption_domain.InputMixin

Record an constraint.

Parameters:constraint – constraint to be recorded Returns:current state modified to record the constraint

replace(variable: lyra.core.expressions.VariableIdentifier, expression: lyra.core.expressions.Expression) → lyra.abstract_domains.assumption.assumption_domain.InputMixin

Replace a variable with an expression.

Note

The new variables appearing in the replacing expression are added to the current state.

Parameters:

• variable – variable to be replaced
• expression – expression replacing the variable

Returns:

current state modified to manifest the replacement

retrieve() → typing.List[lyra.abstract_domains.assumption.assumption_domain.JSONMixin]

Retrieve and forget the constraints corresponding to the current program point.

Warning

The current state is modified to forget the returned constraints.

Returns:the list of constraints corresponding to the current program point

unify(other: lyra.abstract_domains.assumption.assumption_domain.InputMixin) → lyra.abstract_domains.assumption.assumption_domain.InputMixin

Unification of the environment of the current state with the environment of another state.

This is needed when new variables are introduced by replace() to represent input expressions. The unification should match variables in the order of the program points on which they depend.

Parameters:other – state whose environment we want to unify with Returns:current state modified to reflect the unification

widening(other: lyra.abstract_domains.assumption.assumption_domain.InputMixin)

Least upper bound between lattice elements.

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

class lyra.abstract_domains.assumption.assumption_domain.JSONMixin

Bases: lyra.abstract_domains.lattice.Lattice

Mixin to add a mechanism for converting a lattice to and from JSON format.

static from_json(json: str) → lyra.abstract_domains.assumption.assumption_domain.JSONMixin

Reconstruct a lattice element from its JSON format.

Parameters:json – JSON format of a lattice element Returns:reconstructed lattice element from its JSON format

to_json() → str

Convert the current lattice element to JSON format.

Returns:JSON format of the current lattice element

class lyra.abstract_domains.assumption.assumption_domain.TypeAlphabetAssumptionState(variables: typing.Set[lyra.core.expressions.VariableIdentifier], precursory: lyra.abstract_domains.state.State = None)

Bases: lyra.abstract_domains.assumption.assumption_domain.AssumptionState

Type+alphabet assumption analysis state.

Reduced product of type and string constraining states, and a stack of assumptions on the input data.

_assume(condition: lyra.core.expressions.Expression) → lyra.abstract_domains.assumption.assumption_domain.AssumptionState

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

_substitute(left: lyra.core.expressions.Expression, right: lyra.core.expressions.Expression) → lyra.abstract_domains.assumption.assumption_domain.AssumptionState

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 lyra.abstract_domains.assumption.assumption_domain.TypeQuantityAssumptionState(variables: typing.Set[lyra.core.expressions.VariableIdentifier], precursory: lyra.abstract_domains.state.State = None)

Bases: lyra.abstract_domains.assumption.assumption_domain.AssumptionState

Type+quantity assumption analysis state. An element of the type+quantity assumption abstract domain.

Reduced product of type and quantity constraining states, which respectively collect constraints on the type and sign of values of the program variables and (indirectly) on the input data, and a stack of assumptions on the input data, which (directly) constraints the input data read from the current program point.

_assume(condition: lyra.core.expressions.Expression) → lyra.abstract_domains.assumption.assumption_domain.AssumptionState

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

_substitute(left: lyra.core.expressions.Expression, right: lyra.core.expressions.Expression) → lyra.abstract_domains.assumption.assumption_domain.AssumptionState

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 lyra.abstract_domains.assumption.assumption_domain.TypeRangeAlphabetAssumptionState(variables: typing.Set[lyra.core.expressions.VariableIdentifier], precursory: lyra.abstract_domains.state.State = None)

Bases: lyra.abstract_domains.assumption.assumption_domain.AssumptionState

Type+range+alphabet assumption analysis state.

Reduced product of type, range, and string constraining states, and a stack of assumptions on the input data.

_assume(condition: lyra.core.expressions.Expression) → lyra.abstract_domains.assumption.assumption_domain.AssumptionState

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

_substitute(left: lyra.core.expressions.Expression, right: lyra.core.expressions.Expression) → lyra.abstract_domains.assumption.assumption_domain.AssumptionState

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 lyra.abstract_domains.assumption.assumption_domain.TypeRangeAssumptionState(variables: typing.Set[lyra.core.expressions.VariableIdentifier], precursory: lyra.abstract_domains.state.State = None)

Bases: lyra.abstract_domains.assumption.assumption_domain.AssumptionState

Type+range assumption analysis state. An element of the type+range assumption abstract domain.

Reduced product of type and range constraining states, which respectively collect constraints on the type and range of values of the program variables and (indirectly) on the input data, and a stack of assumptions on the input data, which (directly) constraints the input data read from the current program point.

_assume(condition: lyra.core.expressions.Expression) → lyra.abstract_domains.assumption.assumption_domain.AssumptionState

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

_substitute(left: lyra.core.expressions.Expression, right: lyra.core.expressions.Expression) → lyra.abstract_domains.assumption.assumption_domain.AssumptionState

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

Quantity Abstract Domain

Non-relational abstract domain to be used for input data assumptions analysis. The set of possible values of a program variables in a program state is represented by their sign (negative, zero, positive, …)

Authors:Caterina Urban

class lyra.abstract_domains.assumption.quantity_domain.QuantityLattice(negative=True, zero=True, positive=True)

Bases: lyra.abstract_domains.numerical.sign_domain.SignLattice, lyra.abstract_domains.assumption.assumption_domain.JSONMixin

Quantity 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

static from_json(json: str) → lyra.abstract_domains.assumption.assumption_domain.JSONMixin

Reconstruct a lattice element from its JSON format.

Parameters:json – JSON format of a lattice element Returns:reconstructed lattice element from its JSON format

to_json() → str

Convert the current lattice element to JSON format.

Returns:JSON format of the current lattice element

class lyra.abstract_domains.assumption.quantity_domain.QuantityState(variables: typing.Set[lyra.core.expressions.VariableIdentifier], precursory: lyra.abstract_domains.assumption.assumption_domain.InputMixin = None)

Bases: lyra.abstract_domains.numerical.sign_domain.SignState, lyra.abstract_domains.assumption.assumption_domain.InputMixin

Quantity assumption analysis state. An element of the quantity assumption abstract domain.

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

When reading input data, the corresponding quantity assumptions are stored in the class member inputs, which is a map from each program point to the list of quantity assumptions on the input data read at that point.

_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

_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 ExpressionRefinement

Bases: lyra.abstract_domains.basis.ExpressionRefinement

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

Visit of a binary arithmetic operation.

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

Visit of an input call expression.

replace(variable: lyra.core.expressions.VariableIdentifier, expression: lyra.core.expressions.Expression) → lyra.abstract_domains.assumption.quantity_domain.QuantityState

Replace a variable with an expression.

Note

The new variables appearing in the replacing expression are added to the current state.

Parameters:

• variable – variable to be replaced
• expression – expression replacing the variable

Returns:

current state modified to manifest the replacement

unify(other: lyra.abstract_domains.assumption.quantity_domain.QuantityState) → lyra.abstract_domains.assumption.quantity_domain.QuantityState

Unification of the environment of the current state with the environment of another state.

This is needed when new variables are introduced by replace() to represent input expressions. The unification should match variables in the order of the program points on which they depend.

Parameters:other – state whose environment we want to unify with Returns:current state modified to reflect the unification

Range Abstract Domain

Non-relational abstract domain to be used for input data assumption analysis. The set of possible values of a program variable in a program state is represented by a value range.

Authors:Caterina Urban and Madelin Schumacher

class lyra.abstract_domains.assumption.range_domain.RangeLattice(lower=-inf, upper=inf)

Bases: lyra.abstract_domains.numerical.interval_domain.IntervalLattice, lyra.abstract_domains.assumption.assumption_domain.JSONMixin

Range lattice. The bottom range represents an empty set of values.

The default abstraction is the unbounded range [-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)].

static from_json(json: str) → lyra.abstract_domains.assumption.assumption_domain.JSONMixin

Reconstruct a lattice element from its JSON format.

Parameters:json – JSON format of a lattice element Returns:reconstructed lattice element from its JSON format

to_json() → str

Convert the current lattice element to JSON format.

Returns:JSON format of the current lattice element

class lyra.abstract_domains.assumption.range_domain.RangeState(variables: typing.Set[lyra.core.expressions.VariableIdentifier], precursory: lyra.abstract_domains.assumption.assumption_domain.InputMixin = None)

Bases: lyra.abstract_domains.numerical.interval_domain.IntervalState, lyra.abstract_domains.assumption.assumption_domain.InputMixin

Range assumption analysis state. An element of the range assumption abstract domain.

Map from each program variable to the value range representing its value. The value of all program variables is represented by the unbounded range by default.

When reading input data, the corresponding range assumptions are stored in the class member inputs, which is a map from each program point to the list of range assumptions on the input data read at that point.

_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

_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 ExpressionRefinement

Bases: lyra.abstract_domains.basis.ExpressionRefinement

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

Visit of an input call expression.

replace(variable: lyra.core.expressions.VariableIdentifier, expression: lyra.core.expressions.Expression) → lyra.abstract_domains.assumption.range_domain.RangeState

Replace a variable with an expression.

Note

The new variables appearing in the replacing expression are added to the current state.

Parameters:

• variable – variable to be replaced
• expression – expression replacing the variable

Returns:

current state modified to manifest the replacement

unify(other: lyra.abstract_domains.assumption.range_domain.RangeState) → lyra.abstract_domains.assumption.range_domain.RangeState

Unification of the environment of the current state with the environment of another state.

This is needed when new variables are introduced by replace() to represent input expressions. The unification should match variables in the order of the program points on which they depend.

Parameters:other – state whose environment we want to unify with Returns:current state modified to reflect the unification

Type Abstract Domain

Non-relational abstract domain to be used for input data assumption analysis. The set of possible values of a program variable in a state is represented as a type.

Authors:Caterina Urban and Madelin Schumacher

class lyra.abstract_domains.assumption.type_domain.TypeLattice(type_status: lyra.abstract_domains.assumption.type_domain.TypeLattice.Status = <Status.String: 3>)

Bases: lyra.abstract_domains.lattice.BottomMixin, lyra.abstract_domains.lattice.ArithmeticMixin, lyra.abstract_domains.assumption.assumption_domain.JSONMixin

Type Lattice:

String
  |
Float
  |
Integer
  |
Boolean
  |
  ⊥

The default lattice element is String.

Let S be the set of all possible strings. We define F ⊆ S, I ⊆ F, B ⊆ I to be the sets of all possible strings that can be interpreted as floating-point numbers (i.e., F = { 2.35, …, 9.345, …}), integers (i.e., I = { -3, …, 15, …}), and booleans (i.e., B = { 0, 1 }), respectively. The concretization function Ɣ: TypeLattice -> 𝒫(S) is defined as follows:

Ɣ(String) = S
Ɣ(Float) = F
Ɣ(Integer) = I
Ɣ(Boolean) = B
Ɣ(⊥) = ∅

Note

One might want to have Ɣ(Boolean) = { ‘True’, ‘False’ }. This, however, would yield the following different lattice structure:

       String
     /        \
    /        Float
Boolean        |
     \      Integer
      \      /
          ⊥

which is not compatible with subtyping between boolean and integer types in Python.

_less_equal(other: lyra.abstract_domains.assumption.type_domain.TypeLattice) → 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.assumption.type_domain.TypeLattice)

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.assumption.type_domain.TypeLattice) → lyra.abstract_domains.assumption.type_domain.TypeLattice

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.assumption.type_domain.TypeLattice)

Widening between default lattice elements.

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

class Status

Bases: enum.IntEnum

Type status.

The current lattice element can be:

• String: String type
• Float: Float type
• Integer Integer type
• Boolean: Boolean type

Boolean = 0

Float = 2

Integer = 1

String = 3

boolean() → lyra.abstract_domains.assumption.type_domain.TypeLattice

Integer lattice element.

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

The integer lattice element is Boolean

element

Current lattice element.

Returns:the current lattice element if the type is not bottom, None otherwise

float() → lyra.abstract_domains.assumption.type_domain.TypeLattice

Float lattice element.

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

The float lattice element is Float.

static from_json(json: str) → lyra.abstract_domains.assumption.assumption_domain.JSONMixin

Reconstruct a lattice element from its JSON format.

Parameters:json – JSON format of a lattice element Returns:reconstructed lattice element from its JSON format

classmethod from_lyra_type(lyra_type: lyra.core.types.LyraType)

integer() → lyra.abstract_domains.assumption.type_domain.TypeLattice

Integer lattice element.

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

The integer lattice element is Integer

is_boolean() → bool

Test whether the lattice element is boolean.

Returns:whether the lattice element is Boolean

is_float() → bool

Test whether the lattice element is float.

Returns:whether the lattice element is Float

is_integer() → bool

Test whether the lattice element is integer.

Returns:whether the lattice element is Integer

is_top() → bool

Test whether the lattice element is top.

Returns:whether the lattice element is top

to_json() → str

Convert the current lattice element to JSON format.

Returns:JSON format of the current lattice element

top() → lyra.abstract_domains.assumption.type_domain.TypeLattice

Top lattice element.

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

The top lattice element is String.

class lyra.abstract_domains.assumption.type_domain.TypeState(variables: typing.Set[lyra.core.expressions.VariableIdentifier], precursory: lyra.abstract_domains.state.State = None)

Bases: lyra.abstract_domains.store.Store, lyra.abstract_domains.assumption.assumption_domain.InputMixin

Type assumption analysis state. An element of the type assumption abstract domain.

Map from each program variable to the type representing its value. The value of all program variables is represented by their Lyra type by default.

Note

This means that, for any map m: VariableIdentifier -> TypeLattice and variable x, we should always have m(x) ≤ TypeLattice.from_lyra_type(x.typ)

When reading input data, the corresponding type assumptions are stored in the class member inputs, which is a map from each program point to the list of type assumptions on the inputs read at that point.

_assume(condition: lyra.core.expressions.Expression) → lyra.abstract_domains.assumption.type_domain.TypeState

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

_substitute(left: lyra.core.expressions.Expression, right: lyra.core.expressions.Expression) → lyra.abstract_domains.assumption.type_domain.TypeState

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 ArithmeticExpressionRefinement

Bases: lyra.core.expressions.ExpressionVisitor

Visitor that:

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

visit(expr: lyra.core.expressions.Expression, *args, **kwargs)

Visit of an evaluated 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, state=None, evaluation=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, state=None, evaluation=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, state=None, evaluation=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 ExpressionEvaluation

Bases: lyra.core.expressions.ExpressionVisitor

Visitor that performs the evaluation of an expression in the type 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.

enter_if() → lyra.abstract_domains.assumption.type_domain.TypeState

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.assumption.type_domain.TypeState

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.assumption.type_domain.TypeState

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.assumption.type_domain.TypeState

Exit a loop.

Warning

The current state could also be bottom or top.

Returns:current state modified to exit a loop

replace(variable: lyra.core.expressions.VariableIdentifier, expression: lyra.core.expressions.Expression) → lyra.abstract_domains.assumption.type_domain.TypeState

Replace a variable with an expression.

Note

The new variables appearing in the replacing expression are added to the current state.

Parameters:

• variable – variable to be replaced
• expression – expression replacing the variable

Returns:

current state modified to manifest the replacement

unify(other: lyra.abstract_domains.assumption.type_domain.TypeState) → lyra.abstract_domains.assumption.type_domain.TypeState

Unification of the environment of the current state with the environment of another state.

This is needed when new variables are introduced by replace() to represent input expressions. The unification should match variables in the order of the program points on which they depend.

Parameters:other – state whose environment we want to unify with Returns:current state modified to reflect the unification