mythril.laser.smt package¶
Subpackages¶
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.
-
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.
-
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.bool module¶
This module provides classes for an SMT abstraction of boolean expressions.
-
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.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:
-
mythril.laser.smt.function module¶
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.
-
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