lyra.abstract_domains.string package

Submodules

Character Inclusion Abstract Domain

Non-relational abstract domain to be used for string 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.string.character_domain.CharacterLattice(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.lattice.BottomMixin, lyra.abstract_domains.lattice.SequenceMixin

Character inclusion 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).

certainly

Current set of must characters.

Returns:the current set of must characters if there is no conflict, None otherwise

classmethod from_literal(literal: lyra.core.expressions.Literal) → lyra.abstract_domains.string.character_domain.CharacterLattice

is_top() → bool

Test whether the lattice element is top.

Returns:whether the lattice element is top

maybe

Current set of may characters.

Returns:the current set of may characters if there is no conflict, None otherwise

top()

Top lattice element.

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

The top lattice element is (∅, Σ).

class lyra.abstract_domains.string.character_domain.CharacterState(variables: typing.Set[lyra.core.expressions.VariableIdentifier], precursory: lyra.abstract_domains.state.State = None)

Bases: lyra.abstract_domains.basis.Basis

Character inclusion analysis state. An element of the character inclusion 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.

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.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 ExpressionEvaluation

Bases: lyra.abstract_domains.basis.ExpressionEvaluation

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

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

class ExpressionRefinement

Bases: lyra.abstract_domains.basis.ExpressionRefinement

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