lyra.semantics package

Submodules

Backward Semantics

Lyra’s internal backward semantics of statements.

Authors:Caterina Urban
class lyra.semantics.backward.AssignmentSemantics[source]

Bases: lyra.semantics.backward.BackwardSemantics

Backward semantics of assignments.

assignment_semantics(stmt: lyra.core.statements.Assignment, state: lyra.abstract_domains.state.State) → lyra.abstract_domains.state.State[source]

Backward semantics of an assignment.

Parameters:
  • stmt – assignment statement to be executed
  • state – state before executing the assignment
Returns:

state modified by the assignment
class lyra.semantics.backward.BackwardSemantics[source]

Bases: lyra.semantics.semantics.Semantics

Backward semantics of statements.

class lyra.semantics.backward.DefaultBackwardSemantics[source]

Bases: lyra.semantics.semantics.DefaultSemantics, lyra.semantics.backward.UserDefinedCallSemantics, lyra.semantics.backward.AssignmentSemantics

Default backward semantics of statements.

class lyra.semantics.backward.UserDefinedCallSemantics[source]

Bases: lyra.semantics.backward.BackwardSemantics

Backward semantics of user-defined function/method calls.

user_defined_call_semantics(stmt: lyra.core.statements.Call, state: lyra.abstract_domains.state.State)[source]

Backward semantics of a user-defined function/method call.

Parameters:
  • stmt – call statement to be executed
  • state – state before executing the call statement
Returns:

state modified by the call statement

Forward Semantics

Lyra’s internal forward semantics of statements.

Authors:Caterina Urban
class lyra.semantics.forward.AssignmentSemantics[source]

Bases: lyra.semantics.forward.ForwardSemantics

Forward semantics of assignments.

assignment_semantics(stmt: lyra.core.statements.Assignment, state: lyra.abstract_domains.state.State) → lyra.abstract_domains.state.State[source]

Forward semantics of an assignment.

Parameters:
  • stmt – assignment statement to be executed
  • state – state before executing the assignment
Returns:

state modified by the assignment
class lyra.semantics.forward.DefaultForwardSemantics[source]

Bases: lyra.semantics.semantics.DefaultSemantics, lyra.semantics.forward.UserDefinedCallSemantics, lyra.semantics.forward.AssignmentSemantics

Default forward semantics of statements.

class lyra.semantics.forward.ForwardSemantics[source]

Bases: lyra.semantics.semantics.Semantics

Forward semantics of statements.

append_call_semantics(stmt: lyra.core.statements.Call, state: lyra.abstract_domains.state.State) → lyra.abstract_domains.state.State[source]
class lyra.semantics.forward.UserDefinedCallSemantics[source]

Bases: lyra.semantics.forward.ForwardSemantics

Forward semantics of user-defined function/method calls.

user_defined_call_semantics(stmt: lyra.core.statements.Call, state: lyra.abstract_domains.state.State)[source]

Forward semantics of a user-defined function/method call.

Parameters:
  • stmt – call statement to be executed
  • state – state before executing the call statement
Returns:

state modified by the call statement

Semantics

Lyra’s internal semantics of statements.

Authors:Caterina Urban and Simon Wehrli
class lyra.semantics.semantics.BuiltInCallSemantics[source]

Bases: lyra.semantics.semantics.CallSemantics

Semantics of built-in function/method calls.

add_call_semantics(stmt: lyra.core.statements.Call, state: lyra.abstract_domains.state.State) → lyra.abstract_domains.state.State[source]

Semantics of a call to ‘+’ (addition or concatenation).

Parameters:
  • stmt – call to ‘+’ to be executed
  • state – state before executing the call statement
Returns:

state modified by the call statement
and_call_semantics(stmt: lyra.core.statements.Call, state: lyra.abstract_domains.state.State) → lyra.abstract_domains.state.State[source]

Semantics of a call to ‘and’.

Parameters:
  • stmt – call to ‘add’ to be executed
  • state – state before executing the call statement
Returns:

state modified by the call statement
bool_call_semantics(stmt: lyra.core.statements.Call, state: lyra.abstract_domains.state.State) → lyra.abstract_domains.state.State[source]

Semantics of a call to ‘bool’.

Parameters:
  • stmt – call to ‘bool’ to be executed
  • state – state before executing the call statement
Returns:

state modified by the call statement
dict_call_semantics(stmt: lyra.core.statements.Call, state: lyra.abstract_domains.state.State) → lyra.abstract_domains.state.State[source]

Semantics of a call to ‘dict’.

Parameters:
  • stmt – call to ‘dict’ to be executed
  • state – state before executing the call statement
Returns:

state modified by the call statement
div_call_semantics(stmt: lyra.core.statements.Call, state: lyra.abstract_domains.state.State) → lyra.abstract_domains.state.State[source]

Semantics of a call to ‘/’ (division).

Parameters:
  • stmt – call to ‘/’ to be executed
  • state – state before executing the call statement
Returns:

state modified by the call statement
eq_call_semantics(stmt: lyra.core.statements.Call, state: lyra.abstract_domains.state.State) → lyra.abstract_domains.state.State[source]

Semantics of a call to ‘==’ (equality).

Parameters:
  • stmt – call to ‘==’ to be executed
  • state – state before executing the call statement
Returns:

state modified by the call statement
float_call_semantics(stmt: lyra.core.statements.Call, state: lyra.abstract_domains.state.State) → lyra.abstract_domains.state.State[source]

Semantics of a call to ‘float’.

Parameters:
  • stmt – call to ‘float’ to be executed
  • state – state before executing the call statement
Returns:

state modified by the call statement
gt_call_semantics(stmt: lyra.core.statements.Call, state: lyra.abstract_domains.state.State) → lyra.abstract_domains.state.State[source]

Semantics of a call to ‘>’ (greater than).

Parameters:
  • stmt – call to ‘>’ to be executed
  • state – state before executing the call statement
Returns:

state modified by the call statement
gte_call_semantics(stmt: lyra.core.statements.Call, state: lyra.abstract_domains.state.State) → lyra.abstract_domains.state.State[source]

Semantics of a call to ‘>=’ (greater than or equal to).

Parameters:
  • stmt – call to ‘>=’ to be executed
  • state – state before executing the call statement
Returns:

state modified by the call statement
in_call_semantics(stmt: lyra.core.statements.Call, state: lyra.abstract_domains.state.State) → lyra.abstract_domains.state.State[source]

Semantics of a call to ‘in’ (membership).

Parameters:
  • stmt – call to ‘in’ to be executed
  • state – state before executing the call statement
Returns:

state modified by the call statement
input_call_semantics(stmt: lyra.core.statements.Call, state: lyra.abstract_domains.state.State) → lyra.abstract_domains.state.State[source]

Semantics of a calls to ‘input’.

Parameters:
  • stmt – call to ‘input’ to be executed
  • state – state before executing the call statement
Returns:

state modified by the call statement
int_call_semantics(stmt: lyra.core.statements.Call, state: lyra.abstract_domains.state.State) → lyra.abstract_domains.state.State[source]

Semantics of a call to ‘int’.

Parameters:
  • stmt – call to ‘int’ to be executed
  • state – state before executing the call statement
Returns:

state modified by the call statement
is_call_semantics(stmt: lyra.core.statements.Call, state: lyra.abstract_domains.state.State) → lyra.abstract_domains.state.State[source]

Semantics of a call to ‘is’ (identity).

Parameters:
  • stmt – call to ‘is’ to be executed
  • state – state before executing the call statement
Returns:

state modified by the call statement
isnot_call_semantics(stmt: lyra.core.statements.Call, state: lyra.abstract_domains.state.State) → lyra.abstract_domains.state.State[source]

Semantics of a call to ‘is not’ (mismatch).

Parameters:
  • stmt – call to ‘is not’ to be executed
  • state – state before executing the call statement
Returns:

state modified by the call statement
items_call_semantics(stmt: lyra.core.statements.Call, state: lyra.abstract_domains.state.State) → lyra.abstract_domains.state.State[source]

Semantics of calls to ‘items’.

Parameters:
  • stmt – call to ‘items’ to be executed
  • state – state before executing the call statement
Returns:

state modified by the call statement
keys_call_semantics(stmt: lyra.core.statements.Call, state: lyra.abstract_domains.state.State) → lyra.abstract_domains.state.State[source]

Semantics of calls to ‘keys’.

Parameters:
  • stmt – call to ‘keys’ to be executed
  • state – state before executing the call statement
Returns:

state modified by the call statement
len_call_semantics(stmt: lyra.core.statements.Call, state: lyra.abstract_domains.state.State) → lyra.abstract_domains.state.State[source]

Semantics of a call to ‘len’.

Parameters:
  • stmt – call to ‘len’ to be executed
  • state – state before executing the call statement
Returns:

state modified by the call statement
list_call_semantics(stmt: lyra.core.statements.Call, state: lyra.abstract_domains.state.State) → lyra.abstract_domains.state.State[source]

Semantics of a call to ‘list’.

Parameters:
  • stmt – call to ‘list’ to be executed
  • state – state before executing the call statement
Returns:

state modified by the call statement
lower_call_semantics(stmt: lyra.core.statements.Call, state: lyra.abstract_domains.state.State) → lyra.abstract_domains.state.State[source]

Semantics of calls to ‘lower’.

Parameters:
  • stmt – call to ‘lower’ to be executed
  • state – state before executing the call statement
Returns:

state modified by the call statement
lt_call_semantics(stmt: lyra.core.statements.Call, state: lyra.abstract_domains.state.State) → lyra.abstract_domains.state.State[source]

Semantics of a call to ‘<’ (less than).

Parameters:
  • stmt – call to ‘<’ to be executed
  • state – state before executing the call statement
Returns:

state modified by the call statement
lte_call_semantics(stmt: lyra.core.statements.Call, state: lyra.abstract_domains.state.State) → lyra.abstract_domains.state.State[source]

Semantics of a call to ‘<=’ (less than or equal to).

Parameters:
  • stmt – call to ‘<=’ to be executed
  • state – state before executing the call statement
Returns:

state modified by the call statement
mult_call_semantics(stmt: lyra.core.statements.Call, state: lyra.abstract_domains.state.State) → lyra.abstract_domains.state.State[source]

Semantics of a call to ‘*’ (multiplication, not repetition).

Parameters:
  • stmt – call to ‘*’ to be executed
  • state – state before executing the call statement
Returns:

state modified by the call statement
not_call_semantics(stmt: lyra.core.statements.Call, state: lyra.abstract_domains.state.State) → lyra.abstract_domains.state.State[source]

Semantics of a call to ‘!’ (negation).

Parameters:
  • stmt – call to ‘!’ to be executed
  • state – state before executing the call statement
Returns:

state modified by the call statement
noteq_call_semantics(stmt: lyra.core.statements.Call, state: lyra.abstract_domains.state.State) → lyra.abstract_domains.state.State[source]

Semantics of a call to ‘!=’ (inequality).

Parameters:
  • stmt – call to ‘!=’ to be executed
  • state – state before executing the call statement
Returns:

state modified by the call statement
notin_call_semantics(stmt: lyra.core.statements.Call, state: lyra.abstract_domains.state.State) → lyra.abstract_domains.state.State[source]

Semantics of a call to ‘not in’ (non-membership).

Parameters:
  • stmt – call to ‘not in’ to be executed
  • state – state before executing the call statement
Returns:

state modified by the call statement
or_call_semantics(stmt: lyra.core.statements.Call, state: lyra.abstract_domains.state.State) → lyra.abstract_domains.state.State[source]

Semantics of a call to ‘or’.

Parameters:
  • stmt – call to ‘or’ to be executed
  • state – state before executing the call statement
Returns:

state modified by the call statement
print_call_semantics(stmt: lyra.core.statements.Call, state: lyra.abstract_domains.state.State) → lyra.abstract_domains.state.State[source]

Semantics of a call to ‘print’.

Parameters:
  • stmt – call to ‘print’ to be executed
  • state – state before executing the call statement
Returns:

state modified by the call statement
raise_semantics(_, state: lyra.abstract_domains.state.State) → lyra.abstract_domains.state.State[source]

Semantics of raising an Error.

Parameters:
  • _ – raise statement to be executed
  • state – state before executing the raise Error
Returns:

state modified by the raise
range_call_semantics(stmt: lyra.core.statements.Call, state: lyra.abstract_domains.state.State) → lyra.abstract_domains.state.State[source]
set_call_semantics(stmt: lyra.core.statements.Call, state: lyra.abstract_domains.state.State) → lyra.abstract_domains.state.State[source]

Semantics of a call to ‘set’.

Parameters:
  • stmt – call to ‘set’ to be executed
  • state – state before executing the call statement
Returns:

state modified by the call statement
split_call_semantics(stmt: lyra.core.statements.Call, state: lyra.abstract_domains.state.State) → lyra.abstract_domains.state.State[source]
sub_call_semantics(stmt: lyra.core.statements.Call, state: lyra.abstract_domains.state.State) → lyra.abstract_domains.state.State[source]

Semantics of a call to ‘-‘ (subtraction).

Parameters:
  • stmt – call to ‘-‘ to be executed
  • state – state before executing the call statement
Returns:

state modified by the call statement
uadd_call_semantics(stmt: lyra.core.statements.Call, state: lyra.abstract_domains.state.State) → lyra.abstract_domains.state.State[source]

Semantics of a call to ‘+’ (unary plus).

Parameters:
  • stmt – call to ‘+’ to be executed
  • state – state before executing the call statement
Returns:

state modified by the call statement
usub_call_semantics(stmt: lyra.core.statements.Call, state: lyra.abstract_domains.state.State) → lyra.abstract_domains.state.State[source]

Semantics of a call to ‘-‘ (unary minus).

Parameters:
  • stmt – call to ‘-‘ to be executed
  • state – state before executing the call statement
Returns:

state modified by the call statement
values_call_semantics(stmt: lyra.core.statements.Call, state: lyra.abstract_domains.state.State) → lyra.abstract_domains.state.State[source]

Semantics of calls to ‘values’.

Parameters:
  • stmt – call to ‘values’ to be executed
  • state – state before executing the call statement
Returns:

state modified by the call statement
class lyra.semantics.semantics.CallSemantics[source]

Bases: lyra.semantics.semantics.Semantics

Semantics of function/method calls.

call_semantics(stmt: lyra.core.statements.Call, state: lyra.abstract_domains.state.State) → lyra.abstract_domains.state.State[source]

Semantics of a function/method call.

Parameters:
  • stmt – call statement to be executed
  • state – state before executing the call statement
Returns:

state modified by the call statement
class lyra.semantics.semantics.DefaultSemantics[source]

Bases: lyra.semantics.semantics.ExpressionSemantics, lyra.semantics.semantics.BuiltInCallSemantics

Default semantics of statements.

The semantics is independent of the direction (forward/backward) of the analysis.

class lyra.semantics.semantics.ExpressionSemantics[source]

Bases: lyra.semantics.semantics.Semantics

Semantics of expression evaluations and accesses.

dict_display_access_semantics(stmt: lyra.core.statements.DictDisplayAccess, state: lyra.abstract_domains.state.State) → lyra.abstract_domains.state.State[source]

Semantics of a list display access.

Parameters:
  • stmt – dictionary display access statement to be executed
  • state – state before executing the dictionary display access
Returns:

state modified by the dictionary display access
list_display_access_semantics(stmt: lyra.core.statements.ListDisplayAccess, state: lyra.abstract_domains.state.State) → lyra.abstract_domains.state.State[source]

Semantics of a list display access.

Parameters:
  • stmt – list display access statement to be executed
  • state – state before executing the list display access
Returns:

state modified by the list display access
literal_evaluation_semantics(stmt: lyra.core.statements.LiteralEvaluation, state: lyra.abstract_domains.state.State) → lyra.abstract_domains.state.State[source]

Semantics of a literal evaluation.

Parameters:
  • stmt – literal evaluation statement to be executed
  • state – state before executing the literal evaluation
Returns:

stated modified by the literal evaluation
set_display_access_semantics(stmt: lyra.core.statements.SetDisplayAccess, state: lyra.abstract_domains.state.State) → lyra.abstract_domains.state.State[source]

Semantics of a set display access.

Parameters:
  • stmt – set display access statement to be executed
  • state – state before executing the set display access
Returns:

state modified by the set display access
slicing_access_semantics(stmt: lyra.core.statements.SlicingAccess, state: lyra.abstract_domains.state.State) → lyra.abstract_domains.state.State[source]

Semantics of a slicing access.

Parameters:
  • stmt – slicing access statement to be executed
  • state – state before executing the slicing access
Returns:

state modified by the slicing access
subscription_access_semantics(stmt: lyra.core.statements.SubscriptionAccess, state: lyra.abstract_domains.state.State) → lyra.abstract_domains.state.State[source]

Semantics of a subscription access.

Parameters:
  • stmt – subscription access statement to be executed
  • state – state before executing the subscription access
Returns:

state modified by the subscription access
tuple_display_access_semantics(stmt: lyra.core.statements.TupleDisplayAccess, state: lyra.abstract_domains.state.State) → lyra.abstract_domains.state.State[source]

Semantics of a tuple display access.

Parameters:
  • stmt – tuple display access statement to be executed
  • state – state before executing the tuple display access
Returns:

state modified by the tuple display access
variable_access_semantics(stmt: lyra.core.statements.VariableAccess, state: lyra.abstract_domains.state.State) → lyra.abstract_domains.state.State[source]

Semantics of a variable access.

Parameters:
  • stmt – variable access statement to be executed
  • state – state before executing the variable access
Returns:

state modified by the variable access
class lyra.semantics.semantics.Semantics[source]

Bases: object

Semantics of statements.

The semantics is independent of the direction (forward/backward) of the analysis.

semantics(stmt: lyra.core.statements.Statement, state: lyra.abstract_domains.state.State) → lyra.abstract_domains.state.State[source]

Semantics of a statement.

Parameters:
  • stmt – statement to be executed
  • state – state before executing the statement
Returns:

state modified by the statement execution
lyra.semantics.semantics.camel_to_snake(name: str) → str[source]

Convert CamelCase to snake_case

Parameters:name – name in CamelCase
Returns:name in snake_case