diff --git a/mythril/laser/smt/independence_solver.py b/mythril/laser/smt/independence_solver.py index 4fab307e..01552410 100644 --- a/mythril/laser/smt/independence_solver.py +++ b/mythril/laser/smt/independence_solver.py @@ -3,6 +3,7 @@ import z3 from mythril.laser.smt import Model from typing import List + def _get_expr_variables(expression: z3.ExprRef): """ Get's the variables that make up the current expression @@ -20,6 +21,7 @@ def _get_expr_variables(expression: z3.ExprRef): class DependenceBucket: """ Bucket object to contain a set of conditions that are dependent on each other """ + def __init__(self, variables=None, condition=None): """ Initializes a DependenceBucket object @@ -32,6 +34,7 @@ class DependenceBucket: class DependenceMap: """ DependenceMap object that maintains a set of dependence buckets, used to separate independent smt queries """ + def __init__(self): """ Initializes a DependenceMap object """ self.buckets = [] @@ -154,11 +157,12 @@ class IndependenceSolver: from mythril.laser.smt import symbol_factory -a = symbol_factory.BitVecSym('a', 256) -c = symbol_factory.BitVecSym('c', 256) + +a = symbol_factory.BitVecSym("a", 256) +c = symbol_factory.BitVecSym("c", 256) b = c == (a + symbol_factory.BitVecVal(1, 256)) -e = symbol_factory.BitVecSym('d', 256) == symbol_factory.BitVecVal(3, 256) +e = symbol_factory.BitVecSym("d", 256) == symbol_factory.BitVecVal(3, 256) solver = IndependenceSolver() solver.add([b, e]) diff --git a/mythril/laser/smt/model.py b/mythril/laser/smt/model.py index ff3c3756..1e758008 100644 --- a/mythril/laser/smt/model.py +++ b/mythril/laser/smt/model.py @@ -7,6 +7,7 @@ class 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. """ + def __init__(self, models=None): """ Initialize a model object diff --git a/mythril/laser/smt/solver.py b/mythril/laser/smt/solver.py index d9eb5c13..3794c613 100644 --- a/mythril/laser/smt/solver.py +++ b/mythril/laser/smt/solver.py @@ -4,6 +4,7 @@ import z3 from mythril.laser.smt.expression import Expression from mythril.laser.smt.model import Model + class Solver: """An SMT solver object."""