mythril.laser.smt package

Subpackages

• mythril.laser.smt.solver package
  • Submodules
  • mythril.laser.smt.solver.independence_solver module
    • DependenceBucket
    • DependenceMap
      • DependenceMap.add_condition()
    • IndependenceSolver
      • IndependenceSolver.add()
      • IndependenceSolver.append()
      • IndependenceSolver.check()
      • IndependenceSolver.model()
      • IndependenceSolver.pop()
      • IndependenceSolver.reset()
      • IndependenceSolver.set_timeout()
  • mythril.laser.smt.solver.solver module
    • BaseSolver
      • BaseSolver.add()
      • BaseSolver.append()
      • BaseSolver.check()
      • BaseSolver.model()
      • BaseSolver.set_timeout()
      • BaseSolver.sexpr()
    • Optimize
      • Optimize.maximize()
      • Optimize.minimize()
    • Solver
      • Solver.pop()
      • Solver.reset()
  • mythril.laser.smt.solver.solver_statistics module
    • SolverStatistics
    • stat_smt_query()
  • Module contents

Submodules

mythril.laser.smt.array module

This module contains an SMT abstraction of arrays.

This includes an Array class to implement basic store and set operations, as well as as a K-array, which can be initialized with default values over a certain range.

class mythril.laser.smt.array.Array(name: str, domain: int, value_range: int)

Bases: BaseArray

A basic symbolic array.

class mythril.laser.smt.array.BaseArray(raw)

Bases: object

Base array type, which implements basic store and set operations.

substitute(original_expression, new_expression)

Parameters:

• original_expression

• new_expression

class mythril.laser.smt.array.K(domain: int, value_range: int, value: int)

Bases: BaseArray

A basic symbolic array, which can be initialized with a default value.

mythril.laser.smt.bitvec module

This module provides classes for an SMT abstraction of bit vectors.

class mythril.laser.smt.bitvec.BitVec(raw: BitVecRef, annotations: Set[Any] | None = None)

Bases: Expression[BitVecRef]

A bit vector symbol.

size() → int

TODO: documentation

Returns:

property symbolic: bool

Returns whether this symbol doesn’t have a concrete value.

Returns:

property value: int | None

Returns the value of this symbol if concrete, otherwise None.

Returns:

mythril.laser.smt.bitvec_helper module

mythril.laser.smt.bitvec_helper.BVAddNoOverflow(a: BitVec | int, b: BitVec | int, signed: bool) → Bool

Creates predicate that verifies that the addition doesn’t overflow.

Parameters:

• a

• b

• signed

Returns:

mythril.laser.smt.bitvec_helper.BVMulNoOverflow(a: BitVec | int, b: BitVec | int, signed: bool) → Bool

Creates predicate that verifies that the multiplication doesn’t overflow.

Parameters:

• a

• b

• signed

Returns:

mythril.laser.smt.bitvec_helper.BVSubNoUnderflow(a: BitVec | int, b: BitVec | int, signed: bool) → Bool

Creates predicate that verifies that the subtraction doesn’t overflow.

Parameters:

• a

• b

• signed

Returns:

mythril.laser.smt.bitvec_helper.Concat(*args: List[BitVec]) → BitVec

mythril.laser.smt.bitvec_helper.Concat(*args: BitVec) → BitVec

Create a concatenation expression.

Parameters:

args

Returns:

mythril.laser.smt.bitvec_helper.Extract(high: int, low: int, bv: BitVec) → BitVec

Create an extract expression.

Parameters:

• high

• low

• bv

Returns:

mythril.laser.smt.bitvec_helper.If(a: Bool | bool, b: BitVec | int, c: BitVec | int) → BitVec

mythril.laser.smt.bitvec_helper.If(a: Bool | bool, b: BaseArray, c: BaseArray) → BaseArray

Create an if-then-else expression.

Parameters:

• a

• b

• c

Returns:

mythril.laser.smt.bitvec_helper.LShR(a: BitVec, b: BitVec)

mythril.laser.smt.bitvec_helper.SRem(a: BitVec, b: BitVec) → BitVec

Create a signed remainder expression.

Parameters:

• a

• b

Returns:

mythril.laser.smt.bitvec_helper.Sum(*args: BitVec) → BitVec

Create sum expression.

Returns:

mythril.laser.smt.bitvec_helper.UDiv(a: BitVec, b: BitVec) → BitVec

Create an unsigned division expression.

Parameters:

• a

• b

Returns:

mythril.laser.smt.bitvec_helper.UGE(a: BitVec, b: BitVec) → Bool

Create an unsigned greater than or equal to expression.

Parameters:

• a

• b

Returns:

mythril.laser.smt.bitvec_helper.UGT(a: BitVec, b: BitVec) → Bool

Create an unsigned greater than expression.

Parameters:

• a

• b

Returns:

mythril.laser.smt.bitvec_helper.ULE(a: BitVec, b: BitVec) → Bool

Create an unsigned less than or equal to expression.

Parameters:

• a

• b

Returns:

mythril.laser.smt.bitvec_helper.ULT(a: BitVec, b: BitVec) → Bool

Create an unsigned less than expression.

Parameters:

• a

• b

Returns:

mythril.laser.smt.bitvec_helper.URem(a: BitVec, b: BitVec) → BitVec

Create an unsigned remainder expression.

Parameters:

• a

• b

Returns:

mythril.laser.smt.bool module

This module provides classes for an SMT abstraction of boolean expressions.

mythril.laser.smt.bool.And(*args: Bool | bool) → Bool

Create an And expression.

class mythril.laser.smt.bool.Bool(raw: T, annotations: Set[Any] | None = None)

Bases: Expression[BoolRef]

This is a Bool expression.

property is_false: bool

Specifies whether this variable can be simplified to false.

Returns:

property is_true: bool

Specifies whether this variable can be simplified to true.

Returns:

substitute(original_expression, new_expression)

Parameters:

• original_expression

• new_expression

property value: bool | None

Returns the concrete value of this bool if concrete, otherwise None.

Returns:

Concrete value or None

mythril.laser.smt.bool.Not(a: Bool) → Bool

Create a Not expression.

Parameters:

a

Returns:

mythril.laser.smt.bool.Or(*args: Bool | bool) → Bool

Create an or expression.

Parameters:

• a

• b

Returns:

mythril.laser.smt.bool.Xor(a: Bool, b: Bool) → Bool

Create an And expression.

mythril.laser.smt.bool.is_false(a: Bool) → bool

Returns whether the provided bool can be simplified to false.

Parameters:

a

Returns:

mythril.laser.smt.bool.is_true(a: Bool) → bool

Returns whether the provided bool can be simplified to true.

Parameters:

a

Returns:

mythril.laser.smt.expression module

This module contains the SMT abstraction for a basic symbol expression.

class mythril.laser.smt.expression.Expression(raw: T, annotations: Set[Any] | None = None)

Bases: Generic[T]

This is the base symbol class and maintains functionality for simplification and annotations.

annotate(annotation: Any) → None

Annotates this expression with the given annotation.

Parameters:

annotation

property annotations: Set[Any]

Gets the annotations for this expression.

Returns:

get_annotations(annotation: Any)

simplify() → None

Simplify this expression.

simplify_yes() → None

Simplify this expression.

size()

mythril.laser.smt.expression.simplify(expression: G) → G

Simplify the expression .

Parameters:

expression

Returns:

mythril.laser.smt.expression.simplify_yes(expression: G) → G

Simplify the expression .

Parameters:

expression

Returns:

mythril.laser.smt.function module

class mythril.laser.smt.function.Function(name: str, domain: List[int], value_range: int)

Bases: object

An uninterpreted function.

mythril.laser.smt.model module

class mythril.laser.smt.model.Model(models: List[ModelRef] | None = None)

Bases: object

The model class wraps a z3 model

This implementation allows for multiple internal models, this is required for the use of an independence solver which has models for multiple queries which need an uniform output.

decls() → List[ExprRef]

Get the declarations for this model

eval(expression: ExprRef, model_completion: bool = False) → None | ExprRef

Evaluate the expression using this model

Parameters:

• expression – The expression to evaluate

• model_completion – Use the default value if the model has no interpretation of the given expression

Returns:

The evaluated expression

Module contents

class mythril.laser.smt.SymbolFactory

Bases: Generic[T, U]

A symbol factory provides a default interface for all the components of mythril to create symbols

static BitVecSym(name: str, size: int, annotations: Set[Any] | None = None) → U

Creates a new bit vector with a symbolic value.

Parameters:

• name – The name of the symbolic bit vector

• size – The size of the bit vector

• annotations – The annotations to initialize the bit vector with

Returns:

The freshly created bit vector

static BitVecVal(value: int, size: int, annotations: Set[Any] | None = None) → U

Creates a new bit vector with a concrete value.

Parameters:

• value – The concrete value to set the bit vector to

• size – The size of the bit vector

• annotations – The annotations to initialize the bit vector with

Returns:

The freshly created bit vector

static Bool(value: __builtins__.bool, annotations: Set[Any] | None = None) → T

Creates a Bool with concrete value :param value: The boolean value :param annotations: The annotations to initialize the bool with :return: The freshly created Bool()

static BoolSym(name: str, annotations: Set[Any] | None = None) → T

Creates a boolean symbol :param name: The name of the Bool variable :param annotations: The annotations to initialize the bool with :return: The freshly created Bool()