From cfc4746291b71c85982d949397b5af2e35dd793b Mon Sep 17 00:00:00 2001 From: Dimitar Bounov Date: Mon, 14 Jan 2019 18:12:21 +0200 Subject: [PATCH] Fix formatting --- mypy-stubs/z3/__init__.pyi | 407 +++++++++++++++----------------- mypy-stubs/z3/z3core.pyi | 1 + mypy-stubs/z3/z3types.pyi | 13 +- mythril/laser/smt/__init__.py | 36 ++- mythril/laser/smt/array.py | 1 + mythril/laser/smt/expression.py | 6 +- mythril/laser/smt/solver.py | 2 +- 7 files changed, 231 insertions(+), 235 deletions(-) diff --git a/mypy-stubs/z3/__init__.pyi b/mypy-stubs/z3/__init__.pyi index 202a6835..25bd6231 100644 --- a/mypy-stubs/z3/__init__.pyi +++ b/mypy-stubs/z3/__init__.pyi @@ -1,283 +1,262 @@ -from typing import overload, Tuple, Any, List, Iterable, Iterator, Optional, TypeVar, Union +from typing import ( + overload, + Tuple, + Any, + List, + Iterable, + Iterator, + Optional, + TypeVar, + Union, +) from .z3types import Ast, ContextObj -class Context: - ... - -class Z3PPObject: - ... +class Context: ... +class Z3PPObject: ... class AstRef(Z3PPObject): - @overload - def __init__(self, ast: Ast, ctx: Context) -> None: - self.ast: Ast = ... - self.ctx: Context= ... - - @overload - def __init__(self, ast: Ast) -> None: - self.ast: Ast = ... - self.ctx: Context= ... - def ctx_ref(self) -> ContextObj: ... - def as_ast(self) -> Ast: ... - def children(self) -> List[AstRef]: ... - def eq(self, other: AstRef) -> bool: ... - # TODO: Cannot add __eq__ currently: mypy complains conflict with - # object.__eq__ signature - #def __eq__(self, other: object) -> ArithRef: ... - -class SortRef(AstRef): - ... + @overload + def __init__(self, ast: Ast, ctx: Context) -> None: + self.ast: Ast = ... + self.ctx: Context = ... + @overload + def __init__(self, ast: Ast) -> None: + self.ast: Ast = ... + self.ctx: Context = ... + def ctx_ref(self) -> ContextObj: ... + def as_ast(self) -> Ast: ... + def children(self) -> List[AstRef]: ... + def eq(self, other: AstRef) -> bool: ... + # TODO: Cannot add __eq__ currently: mypy complains conflict with + # object.__eq__ signature + # def __eq__(self, other: object) -> ArithRef: ... + +class SortRef(AstRef): ... class FuncDeclRef(AstRef): - def arity(self) -> int: ... - def name(self) -> str: ... - def __call__(self, *args: ExprRef) -> ExprRef: ... + def arity(self) -> int: ... + def name(self) -> str: ... + def __call__(self, *args: ExprRef) -> ExprRef: ... class ExprRef(AstRef): - def sort(self) -> SortRef: ... - def decl(self) -> FuncDeclRef: ... - -class BoolSortRef(SortRef): - ... - -class ArraySortRef(SortRef): - ... + def sort(self) -> SortRef: ... + def decl(self) -> FuncDeclRef: ... -class BoolRef(ExprRef): - ... +class BoolSortRef(SortRef): ... +class ArraySortRef(SortRef): ... +class BoolRef(ExprRef): ... - -def is_true(a: BoolRef) -> bool: ... -def is_false(a: BoolRef) -> bool: ... -def is_int_value(a: AstRef) -> bool: ... +def is_true(a: BoolRef) -> bool: ... +def is_false(a: BoolRef) -> bool: ... +def is_int_value(a: AstRef) -> bool: ... def substitute(a: AstRef, *m: Tuple[AstRef, AstRef]) -> AstRef: ... def simplify(a: AstRef, *args: Any, **kwargs: Any) -> AstRef: ... - -class ArithSortRef(SortRef): - ... +class ArithSortRef(SortRef): ... class ArithRef(ExprRef): - def __neg__(self) -> ExprRef: ... - def __le__(self, other: ArithRef) -> BoolRef: ... - def __lt__(self, other: ArithRef) -> BoolRef: ... - def __ge__(self, other: ArithRef) -> BoolRef: ... - def __gt__(self, other: ArithRef) -> BoolRef: ... - def __add__(self, other: ArithRef) -> ArithRef: ... - def __sub__(self, other: ArithRef) -> ArithRef: ... - def __mul__(self, other: ArithRef) -> ArithRef: ... - def __div__(self, other: ArithRef) -> ArithRef: ... - def __truediv__(self, other: ArithRef) -> ArithRef: ... - def __mod__(self, other: ArithRef) -> ArithRef: ... - -class BitVecSortRef(SortRef): - ... + def __neg__(self) -> ExprRef: ... + def __le__(self, other: ArithRef) -> BoolRef: ... + def __lt__(self, other: ArithRef) -> BoolRef: ... + def __ge__(self, other: ArithRef) -> BoolRef: ... + def __gt__(self, other: ArithRef) -> BoolRef: ... + def __add__(self, other: ArithRef) -> ArithRef: ... + def __sub__(self, other: ArithRef) -> ArithRef: ... + def __mul__(self, other: ArithRef) -> ArithRef: ... + def __div__(self, other: ArithRef) -> ArithRef: ... + def __truediv__(self, other: ArithRef) -> ArithRef: ... + def __mod__(self, other: ArithRef) -> ArithRef: ... + +class BitVecSortRef(SortRef): ... class BitVecRef(ExprRef): - def size(self) -> int: ... - def __add__(self, other: Union[BitVecRef, int]) -> BitVecRef: ... - def __radd__(self, other: Union[BitVecRef, int]) -> BitVecRef: ... - def __mul__(self, other: Union[BitVecRef, int]) -> BitVecRef: ... - def __rmul__(self, other: Union[BitVecRef, int]) -> BitVecRef: ... - def __sub__(self, other: Union[BitVecRef, int]) -> BitVecRef: ... - def __rsub__(self, other: Union[BitVecRef, int]) -> BitVecRef: ... - - def __or__(self, other: Union[BitVecRef, int]) -> BitVecRef: ... - def __ror__(self, other: Union[BitVecRef, int]) -> BitVecRef: ... - def __and__(self, other: Union[BitVecRef, int]) -> BitVecRef: ... - def __rand__(self, other: Union[BitVecRef, int]) -> BitVecRef: ... - def __xor__(self, other: Union[BitVecRef, int]) -> BitVecRef: ... - def __rxor__(self, other: Union[BitVecRef, int]) -> BitVecRef: ... - def __pos__(self) -> BitVecRef: ... - def __neg__(self) -> BitVecRef: ... - def __invert__(self) -> BitVecRef: ... - def __div__(self, other: BitVecRef) -> BitVecRef: ... - def __rdiv__(self, other: BitVecRef) -> BitVecRef: ... - def __truediv__(self, other: BitVecRef) -> BitVecRef: ... - def __rtruediv__(self, other: BitVecRef) -> BitVecRef: ... - def __mod__(self, other: BitVecRef) -> BitVecRef: ... - def __rmod__(self, other: BitVecRef) -> BitVecRef: ... - - def __le__(self, other: BitVecRef) -> BoolRef: ... - def __lt__(self, other: BitVecRef) -> BoolRef: ... - def __ge__(self, other: BitVecRef) -> BoolRef: ... - def __gt__(self, other: BitVecRef) -> BoolRef: ... - - - def __rshift__(self, other: BitVecRef) -> BitVecRef: ... - def __lshift__(self, other: BitVecRef) -> BitVecRef: ... - def __rrshift__(self, other: BitVecRef) -> BitVecRef: ... - def __rlshift__(self, other: BitVecRef) -> BitVecRef: ... + def size(self) -> int: ... + def __add__(self, other: Union[BitVecRef, int]) -> BitVecRef: ... + def __radd__(self, other: Union[BitVecRef, int]) -> BitVecRef: ... + def __mul__(self, other: Union[BitVecRef, int]) -> BitVecRef: ... + def __rmul__(self, other: Union[BitVecRef, int]) -> BitVecRef: ... + def __sub__(self, other: Union[BitVecRef, int]) -> BitVecRef: ... + def __rsub__(self, other: Union[BitVecRef, int]) -> BitVecRef: ... + def __or__(self, other: Union[BitVecRef, int]) -> BitVecRef: ... + def __ror__(self, other: Union[BitVecRef, int]) -> BitVecRef: ... + def __and__(self, other: Union[BitVecRef, int]) -> BitVecRef: ... + def __rand__(self, other: Union[BitVecRef, int]) -> BitVecRef: ... + def __xor__(self, other: Union[BitVecRef, int]) -> BitVecRef: ... + def __rxor__(self, other: Union[BitVecRef, int]) -> BitVecRef: ... + def __pos__(self) -> BitVecRef: ... + def __neg__(self) -> BitVecRef: ... + def __invert__(self) -> BitVecRef: ... + def __div__(self, other: BitVecRef) -> BitVecRef: ... + def __rdiv__(self, other: BitVecRef) -> BitVecRef: ... + def __truediv__(self, other: BitVecRef) -> BitVecRef: ... + def __rtruediv__(self, other: BitVecRef) -> BitVecRef: ... + def __mod__(self, other: BitVecRef) -> BitVecRef: ... + def __rmod__(self, other: BitVecRef) -> BitVecRef: ... + def __le__(self, other: BitVecRef) -> BoolRef: ... + def __lt__(self, other: BitVecRef) -> BoolRef: ... + def __ge__(self, other: BitVecRef) -> BoolRef: ... + def __gt__(self, other: BitVecRef) -> BoolRef: ... + def __rshift__(self, other: BitVecRef) -> BitVecRef: ... + def __lshift__(self, other: BitVecRef) -> BitVecRef: ... + def __rrshift__(self, other: BitVecRef) -> BitVecRef: ... + def __rlshift__(self, other: BitVecRef) -> BitVecRef: ... class BitVecNumRef(BitVecRef): - def as_long(self) -> int: ... - def as_signed_long(self) -> int: ... - def as_string(self) -> str: ... + def as_long(self) -> int: ... + def as_signed_long(self) -> int: ... + def as_string(self) -> str: ... class IntNumRef(ArithRef): - def as_long(self) -> int: ... - def as_string(self) -> str: ... - -class SeqSortRef(ExprRef): - ... - -class SeqRef(ExprRef): - ... - -class ReSortRef(ExprRef): - ... - -class ReRef(ExprRef): - ... - -class ArrayRef(ExprRef): - ... - + def as_long(self) -> int: ... + def as_string(self) -> str: ... + +class SeqSortRef(ExprRef): ... +class SeqRef(ExprRef): ... +class ReSortRef(ExprRef): ... +class ReRef(ExprRef): ... +class ArrayRef(ExprRef): ... class CheckSatResult: ... class ModelRef(Z3PPObject): - def __getitem__(self, k: FuncDeclRef) -> IntNumRef: ... - def decls(self) -> Iterable[FuncDeclRef]: ... - def __iter__(self) -> Iterator[FuncDeclRef]: ... + def __getitem__(self, k: FuncDeclRef) -> IntNumRef: ... + def decls(self) -> Iterable[FuncDeclRef]: ... + def __iter__(self) -> Iterator[FuncDeclRef]: ... class FuncEntry: - def num_args(self) -> int: ... - def arg_value(self, idx: int) -> ExprRef: ... - def value(self) -> ExprRef: ... + def num_args(self) -> int: ... + def arg_value(self, idx: int) -> ExprRef: ... + def value(self) -> ExprRef: ... class FuncInterp(Z3PPObject): - def else_value(self) -> ExprRef: ... - def num_entries(self) -> int: ... - def arity(self) -> int: ... - def entry(self, idx: int) -> FuncEntry: ... + def else_value(self) -> ExprRef: ... + def num_entries(self) -> int: ... + def arity(self) -> int: ... + def entry(self, idx: int) -> FuncEntry: ... -class Goal(Z3PPObject): - ... +class Goal(Z3PPObject): ... class Solver(Z3PPObject): - ctx: Context - def __init__(self, ctx:Optional[Context] = None) -> None: ... - - def to_smt2(self) -> str: ... - def check(self) -> CheckSatResult: ... - def push(self) -> None: ... - def pop(self, num: Optional[int] = 1) -> None: ... - def model(self) -> ModelRef: ... - def set(self, *args: Any, **kwargs: Any) -> None: ... - @overload - def add(self, *args: Union[BoolRef, Goal]) -> None: ... - @overload - def add(self, args: List[Union[BoolRef, Goal]]) -> None: ... - def reset(self) -> None: ... + ctx: Context + def __init__(self, ctx: Optional[Context] = None) -> None: ... + def to_smt2(self) -> str: ... + def check(self) -> CheckSatResult: ... + def push(self) -> None: ... + def pop(self, num: Optional[int] = 1) -> None: ... + def model(self) -> ModelRef: ... + def set(self, *args: Any, **kwargs: Any) -> None: ... + @overload + def add(self, *args: Union[BoolRef, Goal]) -> None: ... + @overload + def add(self, args: List[Union[BoolRef, Goal]]) -> None: ... + def reset(self) -> None: ... class Optimize(Z3PPObject): - ctx: Context - def __init__(self, ctx:Optional[Context] = None) -> None: ... - - def check(self) -> CheckSatResult: ... - def push(self) -> None: ... - def pop(self) -> None: ... - def model(self) -> ModelRef: ... - def set(self, *args: Any, **kwargs: Any) -> None: ... - @overload - def add(self, *args: Union[BoolRef, Goal]) -> None: ... - @overload - def add(self, args: List[Union[BoolRef, Goal]]) -> None: ... - def minimize(self, element: ExprRef) -> None: ... - def maximize(self, element: ExprRef) -> None: ... + ctx: Context + def __init__(self, ctx: Optional[Context] = None) -> None: ... + def check(self) -> CheckSatResult: ... + def push(self) -> None: ... + def pop(self) -> None: ... + def model(self) -> ModelRef: ... + def set(self, *args: Any, **kwargs: Any) -> None: ... + @overload + def add(self, *args: Union[BoolRef, Goal]) -> None: ... + @overload + def add(self, args: List[Union[BoolRef, Goal]]) -> None: ... + def minimize(self, element: ExprRef) -> None: ... + def maximize(self, element: ExprRef) -> None: ... sat: CheckSatResult = ... unsat: CheckSatResult = ... - @overload def Int(name: str) -> ArithRef: ... @overload def Int(name: str, ctx: Context) -> ArithRef: ... - @overload def Bool(name: str) -> BoolRef: ... @overload def Bool(name: str, ctx: Context) -> BoolRef: ... - @overload def parse_smt2_string(s: str) -> ExprRef: ... @overload def parse_smt2_string(s: str, ctx: Context) -> ExprRef: ... - -def Array(name: str, domain: SortRef, range: SortRef) -> ArrayRef: ... -def K(domain: SortRef, v: Union[ExprRef, int, bool, str]) -> ArrayRef: ... +def Array(name: str, domain: SortRef, range: SortRef) -> ArrayRef: ... +def K(domain: SortRef, v: Union[ExprRef, int, bool, str]) -> ArrayRef: ... # Can't give more precise types here since func signature is # a vararg list of ExprRef optionally followed by a Context def Or(*args: Any) -> BoolRef: ... def And(*args: Any) -> BoolRef: ... def Not(p: BoolRef, ctx: Optional[Context] = None) -> BoolRef: ... -def Implies(a: BoolRef, b: BoolRef, ctx:Context) -> BoolRef: ... +def Implies(a: BoolRef, b: BoolRef, ctx: Context) -> BoolRef: ... -T=TypeVar("T", bound=ExprRef) -def If(a: BoolRef, b: T, c: T, ctx: Optional[Context] = None) -> T: ... -def ULE(a: T, b: T) -> BoolRef: ... -def ULT(a: T, b: T) -> BoolRef: ... -def UGE(a: T, b: T) -> BoolRef: ... -def UGT(a: T, b: T) -> BoolRef: ... -def UDiv(a: T, b: T) -> T: ... -def URem(a: T, b: T) -> T: ... -def SRem(a: T, b: T) -> T: ... -def LShR(a: T, b: T) -> T: ... -def RotateLeft(a: T, b: T) -> T: ... -def RotateRight(a: T, b: T) -> T: ... -def SignExt(n: int, a: BitVecRef) -> BitVecRef: ... -def ZeroExt(n: int, a: BitVecRef) -> BitVecRef: ... +T = TypeVar("T", bound=ExprRef) +def If(a: BoolRef, b: T, c: T, ctx: Optional[Context] = None) -> T: ... +def ULE(a: T, b: T) -> BoolRef: ... +def ULT(a: T, b: T) -> BoolRef: ... +def UGE(a: T, b: T) -> BoolRef: ... +def UGT(a: T, b: T) -> BoolRef: ... +def UDiv(a: T, b: T) -> T: ... +def URem(a: T, b: T) -> T: ... +def SRem(a: T, b: T) -> T: ... +def LShR(a: T, b: T) -> T: ... +def RotateLeft(a: T, b: T) -> T: ... +def RotateRight(a: T, b: T) -> T: ... +def SignExt(n: int, a: BitVecRef) -> BitVecRef: ... +def ZeroExt(n: int, a: BitVecRef) -> BitVecRef: ... @overload -def Concat(args: List[Union[SeqRef, str]]) -> SeqRef: ... +def Concat(args: List[Union[SeqRef, str]]) -> SeqRef: ... @overload -def Concat(*args: Union[SeqRef, str]) -> SeqRef: ... +def Concat(*args: Union[SeqRef, str]) -> SeqRef: ... @overload -def Concat(args: List[ReRef]) -> ReRef: ... +def Concat(args: List[ReRef]) -> ReRef: ... @overload -def Concat(*args: ReRef) -> ReRef: ... +def Concat(*args: ReRef) -> ReRef: ... @overload -def Concat(args: List[BitVecRef]) -> BitVecRef: ... +def Concat(args: List[BitVecRef]) -> BitVecRef: ... @overload -def Concat(*args: BitVecRef) -> BitVecRef: ... - +def Concat(*args: BitVecRef) -> BitVecRef: ... @overload -def Extract(high: Union[SeqRef], lo: Union[int, ArithRef], a: Union[int, ArithRef]) -> SeqRef: ... +def Extract( + high: Union[SeqRef], lo: Union[int, ArithRef], a: Union[int, ArithRef] +) -> SeqRef: ... @overload -def Extract(high: Union[int, ArithRef], lo: Union[int, ArithRef], a: BitVecRef) -> BitVecRef: ... - +def Extract( + high: Union[int, ArithRef], lo: Union[int, ArithRef], a: BitVecRef +) -> BitVecRef: ... @overload -def Sum(arg: BitVecRef, *args: Union[BitVecRef, int]) -> BitVecRef: ... +def Sum(arg: BitVecRef, *args: Union[BitVecRef, int]) -> BitVecRef: ... @overload -def Sum(arg: Union[List[BitVecRef], int]) -> BitVecRef: ... +def Sum(arg: Union[List[BitVecRef], int]) -> BitVecRef: ... @overload -def Sum(arg: ArithRef, *args: Union[ArithRef, int]) -> ArithRef: ... -# Can't include this overload as it overlaps with the second overload. -#@overload -#def Sum(arg: Union[List[ArithRef], int]) -> ArithRef: ... - -def Function(name: str, *sig: SortRef) -> FuncDeclRef: ... -def IntVal(val: int, ctx: Optional[Context] = None) -> IntNumRef: ... -def BoolVal(val: bool, ctx: Optional[Context] = None) -> BoolRef: ... -def BitVecVal(val: int, bv: Union[int, BitVecSortRef], ctx: Optional[Context] = None) -> BitVecRef: ... -def BitVec(val: str, bv: Union[int, BitVecSortRef], ctx: Optional[Context] = None) -> BitVecRef: ... - -def IntSort(ctx: Optional[Context] = None) -> ArithSortRef: ... -def BoolSort(ctx:Optional[Context] = None) -> BoolSortRef: ... -def ArraySort(domain: SortRef, range: SortRef) -> ArraySortRef: ... -def BitVecSort(domain: int, ctx:Optional[Context] = None) -> BoolSortRef: ... +def Sum(arg: ArithRef, *args: Union[ArithRef, int]) -> ArithRef: ... +# Can't include this overload as it overlaps with the second overload. +# @overload +# def Sum(arg: Union[List[ArithRef], int]) -> ArithRef: ... + +def Function(name: str, *sig: SortRef) -> FuncDeclRef: ... +def IntVal(val: int, ctx: Optional[Context] = None) -> IntNumRef: ... +def BoolVal(val: bool, ctx: Optional[Context] = None) -> BoolRef: ... +def BitVecVal( + val: int, bv: Union[int, BitVecSortRef], ctx: Optional[Context] = None +) -> BitVecRef: ... +def BitVec( + val: str, bv: Union[int, BitVecSortRef], ctx: Optional[Context] = None +) -> BitVecRef: ... +def IntSort(ctx: Optional[Context] = None) -> ArithSortRef: ... +def BoolSort(ctx: Optional[Context] = None) -> BoolSortRef: ... +def ArraySort(domain: SortRef, range: SortRef) -> ArraySortRef: ... +def BitVecSort(domain: int, ctx: Optional[Context] = None) -> BoolSortRef: ... def ForAll(vs: List[ExprRef], expr: ExprRef) -> ExprRef: ... -def Select(arr: ExprRef, ind: ExprRef) -> ExprRef: ... -def Update(arr: ArrayRef, ind: ExprRef, newVal: ExprRef) -> ArrayRef: ... -def Store(arr: ArrayRef, ind: ExprRef, newVal: ExprRef) -> ArrayRef: ... - -def BVAddNoOverflow(a: BitVecRef, b: BitVecRef, signed: bool) -> BoolRef: ... -def BVAddNoUnderflow(a: BitVecRef, b: BitVecRef) -> BoolRef: ... -def BVSubNoOverflow(a: BitVecRef, b: BitVecRef) -> BoolRef: ... -def BVSubNoUnderflow(a: BitVecRef, b: BitVecRef, signed: bool) -> BoolRef: ... -def BVSDivNoOverflow(a: BitVecRef, b: BitVecRef) -> BoolRef: ... -def BVSNegNoOverflow(a: BitVecRef) -> BoolRef: ... -def BVMulNoOverflow(a: BitVecRef, b: BitVecRef, signed: bool) -> BoolRef: ... -def BVMulNoUnderflow(a: BitVecRef, b: BitVecRef) -> BoolRef: ... +def Select(arr: ExprRef, ind: ExprRef) -> ExprRef: ... +def Update(arr: ArrayRef, ind: ExprRef, newVal: ExprRef) -> ArrayRef: ... +def Store(arr: ArrayRef, ind: ExprRef, newVal: ExprRef) -> ArrayRef: ... +def BVAddNoOverflow(a: BitVecRef, b: BitVecRef, signed: bool) -> BoolRef: ... +def BVAddNoUnderflow(a: BitVecRef, b: BitVecRef) -> BoolRef: ... +def BVSubNoOverflow(a: BitVecRef, b: BitVecRef) -> BoolRef: ... +def BVSubNoUnderflow(a: BitVecRef, b: BitVecRef, signed: bool) -> BoolRef: ... +def BVSDivNoOverflow(a: BitVecRef, b: BitVecRef) -> BoolRef: ... +def BVSNegNoOverflow(a: BitVecRef) -> BoolRef: ... +def BVMulNoOverflow(a: BitVecRef, b: BitVecRef, signed: bool) -> BoolRef: ... +def BVMulNoUnderflow(a: BitVecRef, b: BitVecRef) -> BoolRef: ... diff --git a/mypy-stubs/z3/z3core.pyi b/mypy-stubs/z3/z3core.pyi index 36f1f887..b77e0914 100644 --- a/mypy-stubs/z3/z3core.pyi +++ b/mypy-stubs/z3/z3core.pyi @@ -1,3 +1,4 @@ from .z3types import Ast, ContextObj + def Z3_mk_eq(ctx: ContextObj, a: Ast, b: Ast) -> Ast: ... def Z3_mk_div(ctx: ContextObj, a: Ast, b: Ast) -> Ast: ... diff --git a/mypy-stubs/z3/z3types.pyi b/mypy-stubs/z3/z3types.pyi index fa8fc446..91d5d905 100644 --- a/mypy-stubs/z3/z3types.pyi +++ b/mypy-stubs/z3/z3types.pyi @@ -1,12 +1,9 @@ from typing import Any class Z3Exception(Exception): - def __init__(self, a: Any) -> None: - self.value = a - ... + def __init__(self, a: Any) -> None: + self.value = a + ... -class ContextObj: - ... - -class Ast: - ... +class ContextObj: ... +class Ast: ... diff --git a/mythril/laser/smt/__init__.py b/mythril/laser/smt/__init__.py index 80cc7308..81b8e221 100644 --- a/mythril/laser/smt/__init__.py +++ b/mythril/laser/smt/__init__.py @@ -30,7 +30,9 @@ class SymbolFactory: """A symbol factory provides a default interface for all the components of mythril to create symbols""" @staticmethod - def Bool(value: __builtins__.bool, annotations: Annotations=None) -> Union[bool.Bool, z3.BoolRef]: + def Bool( + value: __builtins__.bool, annotations: Annotations = None + ) -> Union[bool.Bool, z3.BoolRef]: """ Creates a Bool with concrete value :param value: The boolean value @@ -40,7 +42,9 @@ class SymbolFactory: raise NotImplementedError @staticmethod - def BitVecVal(value: int, size: int, annotations: Annotations=None) -> Union[BitVec, z3.BitVecRef]: + def BitVecVal( + value: int, size: int, annotations: Annotations = None + ) -> Union[BitVec, z3.BitVecRef]: """Creates a new bit vector with a concrete value. :param value: The concrete value to set the bit vector to @@ -51,7 +55,9 @@ class SymbolFactory: raise NotImplementedError() @staticmethod - def BitVecSym(name: str, size: int, annotations: Annotations=None) -> Union[BitVec, z3.BitVecRef]: + def BitVecSym( + name: str, size: int, annotations: Annotations = None + ) -> Union[BitVec, z3.BitVecRef]: """Creates a new bit vector with a symbolic value. :param name: The name of the symbolic bit vector @@ -69,7 +75,9 @@ class _SmtSymbolFactory(SymbolFactory): """ @staticmethod - def Bool(value: __builtins__.bool, annotations: Annotations=None) -> Union[bool.Bool, z3.BoolRef]: + def Bool( + value: __builtins__.bool, annotations: Annotations = None + ) -> Union[bool.Bool, z3.BoolRef]: """ Creates a Bool with concrete value :param value: The boolean value @@ -80,13 +88,17 @@ class _SmtSymbolFactory(SymbolFactory): return Bool(raw, annotations) @staticmethod - def BitVecVal(value: int, size: int, annotations: Annotations=None) -> Union[BitVec, z3.BitVecRef]: + def BitVecVal( + value: int, size: int, annotations: Annotations = None + ) -> Union[BitVec, z3.BitVecRef]: """Creates a new bit vector with a concrete value.""" raw = z3.BitVecVal(value, size) return BitVec(raw, annotations) @staticmethod - def BitVecSym(name: str, size: int, annotations: Annotations=None) -> Union[BitVec, z3.BitVecRef]: + def BitVecSym( + name: str, size: int, annotations: Annotations = None + ) -> Union[BitVec, z3.BitVecRef]: """Creates a new bit vector with a symbolic value.""" raw = z3.BitVec(name, size) return BitVec(raw, annotations) @@ -99,17 +111,23 @@ class _Z3SymbolFactory(SymbolFactory): """ @staticmethod - def Bool(value: __builtins__.bool, annotations: Annotations=None) -> Union[bool.Bool, z3.BoolRef]: + def Bool( + value: __builtins__.bool, annotations: Annotations = None + ) -> Union[bool.Bool, z3.BoolRef]: """ Creates a new bit vector with a concrete value """ return z3.BoolVal(value) @staticmethod - def BitVecVal(value: int, size: int, annotations: Annotations=None) -> Union[BitVec, z3.BitVecRef]: + def BitVecVal( + value: int, size: int, annotations: Annotations = None + ) -> Union[BitVec, z3.BitVecRef]: """Creates a new bit vector with a concrete value.""" return z3.BitVecVal(value, size) @staticmethod - def BitVecSym(name: str, size: int, annotations: Annotations=None) -> Union[BitVec, z3.BitVecRef]: + def BitVecSym( + name: str, size: int, annotations: Annotations = None + ) -> Union[BitVec, z3.BitVecRef]: """Creates a new bit vector with a symbolic value.""" return z3.BitVec(name, size) diff --git a/mythril/laser/smt/array.py b/mythril/laser/smt/array.py index 3df06301..c4c1644c 100644 --- a/mythril/laser/smt/array.py +++ b/mythril/laser/smt/array.py @@ -13,6 +13,7 @@ from mythril.laser.smt.bitvec import BitVec class BaseArray: """Base array type, which implements basic store and set operations.""" + domain: z3.SortRef range: z3.SortRef raw: z3.ArrayRef diff --git a/mythril/laser/smt/expression.py b/mythril/laser/smt/expression.py index 0a054af0..2ed166c7 100644 --- a/mythril/laser/smt/expression.py +++ b/mythril/laser/smt/expression.py @@ -3,15 +3,15 @@ from typing import Optional, List, Any, TypeVar, Generic, cast import z3 -Annotations=List[Any] -T = TypeVar('T', bound=z3.ExprRef) +Annotations = List[Any] +T = TypeVar("T", bound=z3.ExprRef) class Expression(Generic[T]): """This is the base symbol class and maintains functionality for simplification and annotations.""" - def __init__(self, raw: T, annotations: Optional[Annotations]=None): + def __init__(self, raw: T, annotations: Optional[Annotations] = None): """ :param raw: diff --git a/mythril/laser/smt/solver.py b/mythril/laser/smt/solver.py index 1523456d..cd419f56 100644 --- a/mythril/laser/smt/solver.py +++ b/mythril/laser/smt/solver.py @@ -10,7 +10,7 @@ class Solver: def __init__(self) -> None: """""" - self.raw = z3.Solver() # type: Union[z3.Solver, z3.Optimize] + self.raw = z3.Solver() # type: Union[z3.Solver, z3.Optimize] def set_timeout(self, timeout: int) -> None: """Sets the timeout that will be used by this solver, timeout is in