mythril.laser.smt.solver package

Submodules

mythril.laser.smt.solver.independence_solver module

class mythril.laser.smt.solver.independence_solver.DependenceBucket(variables=None, conditions=None)[source]

Bases: object

Bucket object to contain a set of conditions that are dependent on each other

class mythril.laser.smt.solver.independence_solver.DependenceMap[source]

Bases: object

DependenceMap object that maintains a set of dependence buckets, used to separate independent smt queries

add_condition(condition: BoolRef) → None[source]

Add condition to the dependence map :param condition: The condition that is to be added to the dependence map

class mythril.laser.smt.solver.independence_solver.IndependenceSolver[source]

Bases: object

An SMT solver object that uses independence optimization

add(*constraints: Tuple[Bool]) → None[source]

Adds the constraints to this solver.

Parameters:

constraints – constraints to add

append(*constraints: Tuple[Bool]) → None[source]

Adds the constraints to this solver.

Parameters:

constraints – constraints to add

check(**kwargs)
model() → Model[source]

Returns z3 model for a solution.

pop(num) → None[source]

Pop num constraints from this solver.

reset() → None[source]

Reset this solver.

set_timeout(timeout: int) → None[source]

Sets the timeout that will be used by this solver, timeout is in milliseconds.

Parameters:

timeout

mythril.laser.smt.solver.solver module

This module contains an abstract SMT representation of an SMT solver.

class mythril.laser.smt.solver.solver.BaseSolver(raw: T)[source]

Bases: Generic[T]

add(*constraints: List[Bool]) → None[source]

Adds the constraints to this solver.

Parameters:

constraints

Returns:

append(*constraints: List[Bool]) → None[source]

Adds the constraints to this solver.

Parameters:

constraints

Returns:

check(**kwargs)
model() → Model[source]

Returns z3 model for a solution.

Returns:

set_timeout(timeout: int) → None[source]

Sets the timeout that will be used by this solver, timeout is in milliseconds.

Parameters:

timeout

sexpr()[source]
class mythril.laser.smt.solver.solver.Optimize[source]

Bases: BaseSolver[Optimize]

An optimizing smt solver.

maximize(element: Expression[ExprRef]) → None[source]

In solving this solver will try to maximize the passed expression.

Parameters:

element

minimize(element: Expression[ExprRef]) → None[source]

In solving this solver will try to minimize the passed expression.

Parameters:

element

class mythril.laser.smt.solver.solver.Solver[source]

Bases: BaseSolver[Solver]

An SMT solver object.

pop(num: int) → None[source]

Pop num constraints from this solver.

Parameters:

num

reset() → None[source]

Reset this solver.

mythril.laser.smt.solver.solver_statistics module

class mythril.laser.smt.solver.solver_statistics.SolverStatistics(*args, **kwargs)[source]

Bases: object

Solver Statistics Class

Keeps track of the important statistics around smt queries

mythril.laser.smt.solver.solver_statistics.stat_smt_query(func: Callable)[source]

Measures statistics for annotated smt query check function

Module contents