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: z3.z3.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) → None[source]

Adds the constraints to this solver.

Parameters:constraints – constraints to add
append(*constraints) → None[source]

Adds the constraints to this solver.

Parameters:constraints – constraints to add
check(**kwargs)
model() → mythril.laser.smt.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: typing.Generic

add(*constraints) → None[source]

Adds the constraints to this solver.

Parameters:constraints –
Returns:
append(*constraints) → None[source]

Adds the constraints to this solver.

Parameters:constraints –
Returns:
check(**kwargs)
model() → mythril.laser.smt.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: mythril.laser.smt.solver.solver.BaseSolver

An optimizing smt solver.

maximize(element: mythril.laser.smt.expression.Expression[z3.z3.ExprRef][z3.z3.ExprRef]) → None[source]

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

Parameters:element –
minimize(element: mythril.laser.smt.expression.Expression[z3.z3.ExprRef][z3.z3.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: mythril.laser.smt.solver.solver.BaseSolver

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[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