Merge branch 'develop' into calldata_improvements

README.md

@@ -9,7 +9,7 @@
 ![Master Build Status](https://img.shields.io/circleci/project/github/ConsenSys/mythril-classic/master.svg)
 [![Waffle.io - Columns and their card count](https://badge.waffle.io/ConsenSys/mythril-classic.svg?columns=In%20Progress)](https://waffle.io/ConsenSys/mythril-classic/)
 [![Sonarcloud - Maintainability](https://sonarcloud.io/api/project_badges/measure?project=mythril&metric=sqale_rating)](https://sonarcloud.io/dashboard?id=mythril)
-[![PyPI Statistics](https://pypistats.com/badge/mythril.svg)](https://pypistats.com/package/mythril)
+[![Downloads](https://pepy.tech/badge/mythril)](https://pepy.tech/project/mythril)
 
 Mythril Classic is an open-source security analysis tool for Ethereum smart contracts. It uses concolic analysis, taint analysis and control flow checking to detect a variety of security vulnerabilities. 
 

mythril/analysis/modules/integer.py

@@ -72,11 +72,13 @@ def _check_integer_overflow(statespace, state, node):
     # Formulate expression
     if instruction["opcode"] == "ADD":
         expr = op0 + op1
+        # constraint = Not(BVAddNoOverflow(op0, op1, signed=False))
     else:
         expr = op1 * op0
+        # constraint = Not(BVMulNoOverflow(op0, op1, signed=False))
 
-    # Check satisfiable
     constraint = Or(And(ULT(expr, op0), op1 != 0), And(ULT(expr, op1), op0 != 0))
+    # Check satisfiable
     model = _try_constraints(node.constraints, [constraint])
 
     if model is None:
@@ -130,11 +132,8 @@ def _try_constraints(constraints, new_constraints):
     Tries new constraints
     :return Model if satisfiable otherwise None
     """
-    _constraints = copy.deepcopy(constraints)
-    for constraint in new_constraints:
-        _constraints.append(copy.deepcopy(constraint))
     try:
-        model = solver.get_model(_constraints)
+        model = solver.get_model(constraints + new_constraints)
         return model
     except UnsatError:
         return None

mythril/analysis/modules/transaction_order_dependence.py

@@ -1,5 +1,6 @@
 import logging
 import re
+import copy
 
 from mythril.analysis import solver
 from mythril.analysis.ops import *

mythril/analysis/symbolic.py

@@ -1,6 +1,6 @@
 from mythril.laser.ethereum import svm
 from mythril.laser.ethereum.state import Account
-from mythril.ether.soliditycontract import SolidityContract
+from mythril.ether.soliditycontract import SolidityContract, ETHContract
 import copy
 import logging
 from .ops import get_variable, SStore, Call, VarType
@@ -64,6 +64,10 @@ class SymExecWrapper:
             self.laser.sym_exec(
                 creation_code=contract.creation_code, contract_name=contract.name
             )
+        elif isinstance(contract, ETHContract) and contract.creation_code:
+            self.laser.sym_exec(
+                creation_code=contract.creation_code, contract_name=contract.name
+            )
         else:
             self.laser.sym_exec(address)
 

mythril/ether/ethcontract.py

@@ -6,7 +6,7 @@ import re
 
 class ETHContract(persistent.Persistent):
     def __init__(
-        self, code, creation_code="", name="Unknown", enable_online_lookup=False
+        self, code="", creation_code="", name="Unknown", enable_online_lookup=False
     ):
 
         # Workaround: We currently do not support compile-time linking.
@@ -27,7 +27,6 @@ class ETHContract(persistent.Persistent):
     def as_dict(self):
 
         return {
-            "address": self.address,
             "name": self.name,
             "code": self.code,
             "creation_code": self.creation_code,

mythril/ether/soliditycontract.py

@@ -25,18 +25,23 @@ class SourceCodeInfo:
         self.code = code
 
 
-def get_contracts_from_file(input_file, solc_args=None):
+def get_contracts_from_file(input_file, solc_args=None, solc_binary="solc"):
-    data = get_solc_json(input_file, solc_args=solc_args)
+    data = get_solc_json(input_file, solc_args=solc_args, solc_binary=solc_binary)
     for key, contract in data["contracts"].items():
         filename, name = key.split(":")
         if filename == input_file and len(contract["bin-runtime"]):
-            yield SolidityContract(input_file, name, solc_args)
+            yield SolidityContract(
+                input_file=input_file,
+                name=name,
+                solc_args=solc_args,
+                solc_binary=solc_binary,
+            )
 
 
 class SolidityContract(ETHContract):
-    def __init__(self, input_file, name=None, solc_args=None):
+    def __init__(self, input_file, name=None, solc_args=None, solc_binary="solc"):
 
-        data = get_solc_json(input_file, solc_args=solc_args)
+        data = get_solc_json(input_file, solc_args=solc_args, solc_binary=solc_binary)
 
         self.solidity_files = []
 

mythril/interfaces/cli.py

@@ -90,6 +90,11 @@ def main():
         action="store_true",
         help="auto-load dependencies from the blockchain",
     )
+    inputs.add_argument(
+        "--bin-runtime",
+        action="store_true",
+        help="Only when -c or -f is used. Consider the input bytecode as binary runtime code, default being the contract creation bytecode.",
+    )
 
     outputs = parser.add_argument_group("output formats")
     outputs.add_argument(
@@ -317,10 +322,10 @@ def main():
 
         if args.code:
             # Load from bytecode
-            address, _ = mythril.load_from_bytecode(args.code)
+            address, _ = mythril.load_from_bytecode(args.code, args.bin_runtime)
         elif args.codefile:
             bytecode = "".join([l.strip() for l in args.codefile if len(l.strip()) > 0])
-            address, _ = mythril.load_from_bytecode(bytecode)
+            address, _ = mythril.load_from_bytecode(bytecode, args.bin_runtime)
         elif args.address:
             # Get bytecode from a contract address
             address, _ = mythril.load_from_address(args.address)

mythril/laser/ethereum/instructions.py

@@ -18,7 +18,6 @@ from z3 import (
     URem,
     SRem,
     BitVec,
-    Solver,
     is_true,
     BitVecVal,
     If,
@@ -43,7 +42,6 @@ from mythril.laser.ethereum.transaction import (
     TransactionStartSignal,
     ContractCreationTransaction,
 )
-from mythril.analysis.solver import get_model
 
 TT256 = 2 ** 256
 TT256M1 = 2 ** 256 - 1
@@ -931,9 +929,6 @@ class Instruction:
             storage_keys = global_state.environment.active_account.storage.keys()
             keccak_keys = filter(keccak_function_manager.is_keccak, storage_keys)
 
-            solver = Solver()
-            solver.set(timeout=1000)
-
             results = []
             new = False
 
@@ -941,7 +936,7 @@ class Instruction:
                 key_argument = keccak_function_manager.get_argument(keccak_key)
                 index_argument = keccak_function_manager.get_argument(index)
 
-                if is_true(key_argument == index_argument):
+                if is_true(simplify(key_argument == index_argument)):
                     return self._sstore_helper(
                         copy(global_state),
                         keccak_key,

mythril/laser/ethereum/svm.py

@@ -129,7 +129,7 @@ class LaserEVM:
                 / float(coverage[0])
                 * 100
             )
-            logging.info("Achieved {} coverage for code: {}".format(cov, code))
+            logging.info("Achieved {:.2f}% coverage for code: {}".format(cov, code))
 
     def _get_covered_instructions(self) -> int:
         """ Gets the total number of covered instructions for all accounts in the svm"""

mythril/mythril.py

@@ -311,11 +311,22 @@ class Mythril(object):
 
         print(self.eth_db.contract_hash_to_address(hash))
 
-    def load_from_bytecode(self, code):
+    def load_from_bytecode(self, code, bin_runtime=False):
         address = util.get_indexed_address(0)
+        if bin_runtime:
             self.contracts.append(
                 ETHContract(
-                code, name="MAIN", enable_online_lookup=self.enable_online_lookup
+                    code=code,
+                    name="MAIN",
+                    enable_online_lookup=self.enable_online_lookup,
+                )
+            )
+        else:
+            self.contracts.append(
+                ETHContract(
+                    creation_code=code,
+                    name="MAIN",
+                    enable_online_lookup=self.enable_online_lookup,
                 )
             )
         return address, self.contracts[-1]  # return address and contract object
@@ -375,13 +386,18 @@ class Mythril(object):
 
                 if contract_name is not None:
                     contract = SolidityContract(
-                        file, contract_name, solc_args=self.solc_args
+                        input_file=file,
+                        name=contract_name,
+                        solc_args=self.solc_args,
+                        solc_binary=self.solc_binary,
                     )
                     self.contracts.append(contract)
                     contracts.append(contract)
                 else:
                     for contract in get_contracts_from_file(
-                        file, solc_args=self.solc_args
+                        input_file=file,
+                        solc_args=self.solc_args,
+                        solc_binary=self.solc_binary,
                     ):
                         self.contracts.append(contract)
                         contracts.append(contract)

mythril/version.py

@@ -1,3 +1,3 @@
 # This file is suitable for sourcing inside POSIX shell, e.g. bash as
 # well as for importing into Python
-VERSION = "v0.18.13"  # NOQA
+VERSION = "v0.19.3"  # NOQA

requirements.txt

@@ -24,5 +24,5 @@ pytest_mock
 requests
 rlp>=1.0.1
 transaction>=2.2.1
-z3-solver>=4.5
+z3-solver==4.5.1.0.post2
 pysha3

setup.py

@@ -75,7 +75,7 @@ setup(
     install_requires=[
         "coloredlogs>=10.0",
         "ethereum>=2.3.2",
-        "z3-solver>=4.5",
+        "z3-solver==4.5.1.0.post2",
         "requests",
         "py-solc",
         "plyvel",

tests/cmd_line_test.py

@@ -10,7 +10,7 @@ def output_of(command):
 
 class CommandLineToolTestCase(BaseTestCase):
     def test_disassemble_code_correctly(self):
-        command = "python3 {} MYTH -d -c 0x5050".format(MYTH)
+        command = "python3 {} MYTH -d --bin-runtime -c 0x5050".format(MYTH)
         self.assertEqual("0 POP\n1 POP\n", output_of(command))
 
     def test_disassemble_solidity_file_correctly(self):