Merge pull request #1142 from ConsenSys/develop

Merge for v0.21.7

.circleci/config.yml

@@ -107,9 +107,10 @@ jobs:
                 -e CIRCLE_BUILD_URL=$CIRCLE_BUILD_URL \
                 -e CIRCLE_WEBHOOK_URL=$CIRCLE_WEBHOOK_URL \
                 --rm edelweiss-mythril:latest \
-                --timeout 45 \
+                --timeout 60 \
                 --output-dir /opt/edelweiss \
                 --s3 \
+                --dynamodb \
                 --circle-ci CircleCI/mythril.csv \
                 --ignore-false-positives $IGNORE_FALSE_POSITIVES \
                 --ignore-regressions $IGNORE_REGRESSIONS

mythril/__version__.py

@@ -4,4 +4,4 @@ This file is suitable for sourcing inside POSIX shell, e.g. bash as well
 as for importing into Python.
 """
 
-__version__ = "v0.21.6"
+__version__ = "v0.21.7"

mythril/laser/ethereum/call.py

@@ -96,7 +96,7 @@ def get_callee_address(
         # attempt to read the contract address from instance storage
         try:
             callee_address = dynamic_loader.read_storage(
-                hex(environment.active_account.address.value), index
+                "0x{:040X}".format(environment.active_account.address.value), index
             )
         # TODO: verify whether this happens or not
         except:

mythril/laser/ethereum/state/account.py

@@ -64,7 +64,7 @@ class Storage:
                 storage[item] = symbol_factory.BitVecVal(
                     int(
                         self.dynld.read_storage(
-                            contract_address=hex(self.address.value),
+                            contract_address="0x{:040X}".format(self.address.value),
                             index=int(item.value),
                         ),
                         16,

mythril/laser/smt/bitvec.py

@@ -190,6 +190,9 @@ class BitVec(Expression[z3.BitVecRef]):
             )
 
         union = self.annotations.union(other.annotations)
+        # Some of the BitVecs can be 512 bit due to sha3()
+        if self.raw.size() != other.raw.size():
+            return Bool(z3.BoolVal(False), annotations=union)
         # MYPY: fix complaints due to z3 overriding __eq__
         return Bool(cast(z3.BoolRef, self.raw == other.raw), annotations=union)
 
@@ -208,6 +211,9 @@ class BitVec(Expression[z3.BitVecRef]):
             )
 
         union = self.annotations.union(other.annotations)
+        # Some of the BitVecs can be 512 bit due to sha3()
+        if self.raw.size() != other.raw.size():
+            return Bool(z3.BoolVal(True), annotations=union)
         # MYPY: fix complaints due to z3 overriding __eq__
         return Bool(cast(z3.BoolRef, self.raw != other.raw), annotations=union)
 
@@ -386,9 +392,12 @@ def Concat(*args: Union[BitVec, List[BitVec]]) -> BitVec:
             bitvecfunc = True
 
     if bitvecfunc:
-        # Is there a better value to set func_name and input to in this case?
+        # Added this not so good and misleading NOTATION to help with this
+        str_hash = ",".join(["hashed({})".format(hash(bv)) for bv in bvs])
+        input_string = "MisleadingNotationConcat({})".format(str_hash)
+
         return BitVecFunc(
-            raw=nraw, func_name=None, input_=None, annotations=annotations
+            raw=nraw, func_name="Hybrid", input_=BitVec(z3.BitVec(input_string, 256), annotations=annotations)
         )
 
     return BitVec(nraw, annotations)
@@ -404,9 +413,10 @@ def Extract(high: int, low: int, bv: BitVec) -> BitVec:
     """
     raw = z3.Extract(high, low, bv.raw)
     if isinstance(bv, BitVecFunc):
+        input_string = "MisleadingNotationExtract({}, {}, hashed({}))".format(high, low, hash(bv))
         # Is there a better value to set func_name and input to in this case?
         return BitVecFunc(
-            raw=raw, func_name=None, input_=None, annotations=bv.annotations
+            raw=raw, func_name="Hybrid", input_=BitVec(z3.BitVec(input_string, 256), annotations=bv.annotations)
         )
 
     return BitVec(raw, annotations=bv.annotations)
@@ -457,7 +467,7 @@ def Sum(*args: BitVec) -> BitVec:
             bitvecfuncs.append(bv)
 
     if len(bitvecfuncs) >= 2:
-        return BitVecFunc(raw=raw, func_name=None, input_=None, annotations=annotations)
+        return BitVecFunc(raw=raw, func_name="Hybrid", input_=None, annotations=annotations)
     elif len(bitvecfuncs) == 1:
         return BitVecFunc(
             raw=raw,

mythril/laser/smt/bitvecfunc.py

@@ -27,7 +27,14 @@ def _arithmetic_helper(
 
     if isinstance(b, BitVecFunc):
         # TODO: Find better value to set input and name to in this case?
-        return BitVecFunc(raw=raw, func_name=None, input_=None, annotations=union)
+        input_string = "MisleadingNotationop(invhash({}) {} invhash({})".format(
+            hash(a), operation, hash(b)
+        )
+        return BitVecFunc(
+            raw=raw,
+            func_name="Hybrid",
+            input_=BitVec(z3.BitVec(input_string, 256), annotations=union),
+        )
 
     return BitVecFunc(
         raw=raw, func_name=a.func_name, input_=a.input_, annotations=union
@@ -52,7 +59,6 @@ def _comparison_helper(
     # Is there some hack for gt/lt comparisons?
     if isinstance(b, int):
         b = BitVec(z3.BitVecVal(b, a.size()))
-
     union = a.annotations.union(b.annotations)
 
     if not a.symbolic and not b.symbolic:
@@ -193,6 +199,7 @@ class BitVecFunc(BitVec):
         :param other: The int or BitVec to compare to this BitVecFunc
         :return: The resulting Bool
         """
+
         return _comparison_helper(
             self, other, operator.eq, default_value=False, inputs_equal=True
         )

mythril/mythril/mythril_config.py

@@ -175,7 +175,7 @@ class MythrilConfig:
         :param rpc: either of the strings - ganache, infura-mainnet, infura-rinkeby, infura-kovan, infura-ropsten
         """
         if rpc == "ganache":
-            rpcconfig = ("localhost", 8545, False)
+            rpcconfig = ("localhost", 7545, False)
         else:
             m = re.match(r"infura-(.*)", rpc)
             if m and m.group(1) in ["mainnet", "rinkeby", "kovan", "ropsten"]:

tests/mythril/mythril_config_test.py

@@ -19,7 +19,7 @@ def test_config_path_dynloading():
 
 rpc_types_tests = [
     ("infura", "mainnet.infura.io", 443, True),
-    ("ganache", "localhost", 8545, True),
+    ("ganache", "localhost", 7545, True),
     ("infura-rinkeby", "rinkeby.infura.io", 443, True),
     ("infura-ropsten", "ropsten.infura.io", 443, True),
     ("infura-kovan", "kovan.infura.io", 443, True),