mythril.laser.smt package

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)[source]

Bases: mythril.laser.smt.array.BaseArray

A basic symbolic array.

class mythril.laser.smt.array.BaseArray(raw)[source]

Bases: object

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

substitute(original_expression, new_expression)[source]
Parameters:
  • original_expression –
  • new_expression –
class mythril.laser.smt.array.K(domain: int, value_range: int, value: int)[source]

Bases: mythril.laser.smt.array.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: z3.z3.BitVecRef, annotations: Optional[Set[Any]] = None)[source]

Bases: mythril.laser.smt.expression.Expression

A bit vector symbol.

size() → int[source]

TODO: documentation

Returns:
symbolic

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

Returns:
value

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

Returns:

mythril.laser.smt.bitvec_helper module

mythril.laser.smt.bitvec_helper.BVAddNoOverflow(a: Union[mythril.laser.smt.bitvec.BitVec, int], b: Union[mythril.laser.smt.bitvec.BitVec, int], signed: bool) → mythril.laser.smt.bool.Bool[source]

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

Parameters:
  • a –
  • b –
  • signed –
Returns:
mythril.laser.smt.bitvec_helper.BVMulNoOverflow(a: Union[mythril.laser.smt.bitvec.BitVec, int], b: Union[mythril.laser.smt.bitvec.BitVec, int], signed: bool) → mythril.laser.smt.bool.Bool[source]

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

Parameters:
  • a –
  • b –
  • signed –
Returns:
mythril.laser.smt.bitvec_helper.BVSubNoUnderflow(a: Union[mythril.laser.smt.bitvec.BitVec, int], b: Union[mythril.laser.smt.bitvec.BitVec, int], signed: bool) → mythril.laser.smt.bool.Bool[source]

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

Parameters:
  • a –
  • b –
  • signed –
Returns:
mythril.laser.smt.bitvec_helper.Concat(*args) → mythril.laser.smt.bitvec.BitVec[source]

Create a concatenation expression.

Parameters:args –
Returns:
mythril.laser.smt.bitvec_helper.Extract(high: int, low: int, bv: mythril.laser.smt.bitvec.BitVec) → mythril.laser.smt.bitvec.BitVec[source]

Create an extract expression.

Parameters:
  • high –
  • low –
  • bv –
Returns:
mythril.laser.smt.bitvec_helper.If(a: Union[mythril.laser.smt.bool.Bool, bool], b: Union[mythril.laser.smt.array.BaseArray, mythril.laser.smt.bitvec.BitVec, int], c: Union[mythril.laser.smt.array.BaseArray, mythril.laser.smt.bitvec.BitVec, int]) → Union[mythril.laser.smt.bitvec.BitVec, mythril.laser.smt.array.BaseArray][source]

Create an if-then-else expression.

Parameters:
  • a –
  • b –
  • c –
Returns:
mythril.laser.smt.bitvec_helper.LShR(a: mythril.laser.smt.bitvec.BitVec, b: mythril.laser.smt.bitvec.BitVec)[source]
mythril.laser.smt.bitvec_helper.SRem(a: mythril.laser.smt.bitvec.BitVec, b: mythril.laser.smt.bitvec.BitVec) → mythril.laser.smt.bitvec.BitVec[source]

Create a signed remainder expression.

Parameters:
  • a –
  • b –
Returns:
mythril.laser.smt.bitvec_helper.Sum(*args) → mythril.laser.smt.bitvec.BitVec[source]

Create sum expression.

Returns:
mythril.laser.smt.bitvec_helper.UDiv(a: mythril.laser.smt.bitvec.BitVec, b: mythril.laser.smt.bitvec.BitVec) → mythril.laser.smt.bitvec.BitVec[source]

Create an unsigned division expression.

Parameters:
  • a –
  • b –
Returns:
mythril.laser.smt.bitvec_helper.UGE(a: mythril.laser.smt.bitvec.BitVec, b: mythril.laser.smt.bitvec.BitVec) → mythril.laser.smt.bool.Bool[source]

Create an unsigned greater than or equal to expression.

Parameters:
  • a –
  • b –
Returns:
mythril.laser.smt.bitvec_helper.UGT(a: mythril.laser.smt.bitvec.BitVec, b: mythril.laser.smt.bitvec.BitVec) → mythril.laser.smt.bool.Bool[source]

Create an unsigned greater than expression.

Parameters:
  • a –
  • b –
Returns:
mythril.laser.smt.bitvec_helper.ULE(a: mythril.laser.smt.bitvec.BitVec, b: mythril.laser.smt.bitvec.BitVec) → mythril.laser.smt.bool.Bool[source]

Create an unsigned less than or equal to expression.

Parameters:
  • a –
  • b –
Returns:
mythril.laser.smt.bitvec_helper.ULT(a: mythril.laser.smt.bitvec.BitVec, b: mythril.laser.smt.bitvec.BitVec) → mythril.laser.smt.bool.Bool[source]

Create an unsigned less than expression.

Parameters:
  • a –
  • b –
Returns:
mythril.laser.smt.bitvec_helper.URem(a: mythril.laser.smt.bitvec.BitVec, b: mythril.laser.smt.bitvec.BitVec) → mythril.laser.smt.bitvec.BitVec[source]

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) → mythril.laser.smt.bool.Bool[source]

Create an And expression.

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

Bases: mythril.laser.smt.expression.Expression

This is a Bool expression.

is_false

Specifies whether this variable can be simplified to false.

Returns:
is_true

Specifies whether this variable can be simplified to true.

Returns:
substitute(original_expression, new_expression)[source]
Parameters:
  • original_expression –
  • new_expression –
value

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

Returns:Concrete value or None
mythril.laser.smt.bool.Not(a: mythril.laser.smt.bool.Bool) → mythril.laser.smt.bool.Bool[source]

Create a Not expression.

Parameters:a –
Returns:
mythril.laser.smt.bool.Or(*args) → mythril.laser.smt.bool.Bool[source]

Create an or expression.

Parameters:
  • a –
  • b –
Returns:
mythril.laser.smt.bool.Xor(a: mythril.laser.smt.bool.Bool, b: mythril.laser.smt.bool.Bool) → mythril.laser.smt.bool.Bool[source]

Create an And expression.

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

Returns whether the provided bool can be simplified to false.

Parameters:a –
Returns:
mythril.laser.smt.bool.is_true(a: mythril.laser.smt.bool.Bool) → bool[source]

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: Optional[Set[Any]] = None)[source]

Bases: typing.Generic

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

annotate(annotation: Any) → None[source]

Annotates this expression with the given annotation.

Parameters:annotation –
annotations

Gets the annotations for this expression.

Returns:
get_annotations(annotation: Any)[source]
simplify() → None[source]

Simplify this expression.

size()[source]
mythril.laser.smt.expression.simplify(expression: G) → G[source]

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)[source]

Bases: object

An uninterpreted function.

mythril.laser.smt.model module

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

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[z3.z3.ExprRef][source]

Get the declarations for this model

eval(expression: z3.z3.ExprRef, model_completion: bool = False) → Union[None, z3.z3.ExprRef][source]

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

Bases: typing.Generic

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

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

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: Optional[Set[Any]] = None) → U[source]

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: Optional[Set[Any]] = None) → T[source]

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: Optional[Set[Any]] = None) → T[source]

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()