TheDude
/
mythril
mirror of https://github.com/ConsenSys/mythril
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Fix formatting

Browse Source
pull/885/head
Dimitar Bounov 6 years ago
parent 4c1ddb9fbe
commit cfc4746291
7 changed files with 231 additions and 235 deletions
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Show Stats Download Patch File Download Diff File
  1. 121
      mypy-stubs/z3/__init__.pyi
  2. 1
      mypy-stubs/z3/z3core.pyi
  3. 7
      mypy-stubs/z3/z3types.pyi
  4. 36
      mythril/laser/smt/__init__.py
  5. 1
      mythril/laser/smt/array.py
  6. 6
      mythril/laser/smt/expression.py

121
mypy-stubs/z3/__init__.pyi
Unescape View File

@ -1,32 +1,37 @@
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= ...
self.ctx: Context = ...
@overload
def __init__(self, ast: Ast) -> None:
self.ast: Ast = ...
self.ctx: Context= ...
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: ...
# def __eq__(self, other: object) -> ArithRef: ...
class SortRef(AstRef):
...
class SortRef(AstRef): ...
class FuncDeclRef(AstRef):
def arity(self) -> int: ...
@ -37,15 +42,9 @@ class ExprRef(AstRef):
def sort(self) -> SortRef: ...
def decl(self) -> FuncDeclRef: ...
class BoolSortRef(SortRef):
...
class ArraySortRef(SortRef):
...
class BoolRef(ExprRef):
...
class BoolSortRef(SortRef): ...
class ArraySortRef(SortRef): ...
class BoolRef(ExprRef): ...
def is_true(a: BoolRef) -> bool: ...
def is_false(a: BoolRef) -> bool: ...
@ -53,9 +52,7 @@ 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: ...
@ -70,8 +67,7 @@ class ArithRef(ExprRef):
def __truediv__(self, other: ArithRef) -> ArithRef: ...
def __mod__(self, other: ArithRef) -> ArithRef: ...
class BitVecSortRef(SortRef):
...
class BitVecSortRef(SortRef): ...
class BitVecRef(ExprRef):
def size(self) -> int: ...
@ -81,7 +77,6 @@ class BitVecRef(ExprRef):
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: ...
@ -97,13 +92,10 @@ class BitVecRef(ExprRef):
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: ...
@ -118,21 +110,11 @@ 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):
...
class SeqSortRef(ExprRef): ...
class SeqRef(ExprRef): ...
class ReSortRef(ExprRef): ...
class ReRef(ExprRef): ...
class ArrayRef(ExprRef): ...
class CheckSatResult: ...
class ModelRef(Z3PPObject):
@ -151,13 +133,11 @@ class FuncInterp(Z3PPObject):
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 __init__(self, ctx: Optional[Context] = None) -> None: ...
def to_smt2(self) -> str: ...
def check(self) -> CheckSatResult: ...
def push(self) -> None: ...
@ -172,8 +152,7 @@ class Solver(Z3PPObject):
class Optimize(Z3PPObject):
ctx: Context
def __init__(self, ctx:Optional[Context] = None) -> None: ...
def __init__(self, ctx: Optional[Context] = None) -> None: ...
def check(self) -> CheckSatResult: ...
def push(self) -> None: ...
def pop(self) -> None: ...
@ -188,22 +167,18 @@ class Optimize(Z3PPObject):
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: ...
@ -212,9 +187,10 @@ def K(domain: SortRef, v: Union[ExprRef, int, bool, str]) -> ArrayRef: ...
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)
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: ...
@ -228,7 +204,6 @@ 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: ...
@overload
@ -241,38 +216,42 @@ def Concat(*args: ReRef) -> ReRef: ...
def Concat(args: List[BitVecRef]) -> BitVecRef: ...
@overload
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: ...
@overload
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: ...
# @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 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 BoolSort(ctx: Optional[Context] = None) -> BoolSortRef: ...
def ArraySort(domain: SortRef, range: SortRef) -> ArraySortRef: ...
def BitVecSort(domain: int, ctx:Optional[Context] = None) -> BoolSortRef: ...
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: ...

1
mypy-stubs/z3/z3core.pyi
Unescape View File

@ -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: ...

7
mypy-stubs/z3/z3types.pyi
Unescape View File

@ -5,8 +5,5 @@ class Z3Exception(Exception):
self.value = a
...
class ContextObj:
...
class Ast:
...
class ContextObj: ...
class Ast: ...

36
mythril/laser/smt/__init__.py
Unescape View File

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

1
mythril/laser/smt/array.py
Unescape View File

@ -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

6
mythril/laser/smt/expression.py
Unescape View File

@ -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:

Write Preview
Loading…
Cancel
Save