diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml new file mode 100644 index 000000000..3717e3b03 --- /dev/null +++ b/.github/workflows/release.yml @@ -0,0 +1,78 @@ +name: Upload to PyPI + +on: + release: + types: [published] + +jobs: + tests: + runs-on: ubuntu-18.04 + strategy: + matrix: + type: ["ethereum_truffle", "ethereum_bench", "examples", "ethereum", "ethereum_vm", "native", "wasm", "wasm_sym", "other"] + steps: + - uses: actions/checkout@v1 + - name: Set up Python 3.6 + uses: actions/setup-python@v1 + with: + python-version: 3.6 + - name: Install NPM + uses: actions/setup-node@v1 + with: + node-version: '13.x' + - name: Install dependencies + env: + TEST_TYPE: ${{ matrix.type }} + run: | + #install utils + pip install coveralls + pip install -e ".[dev-noks]" + #install cvc4 + sudo wget -O /usr/bin/cvc4 https://github.com/CVC4/CVC4/releases/download/1.7/cvc4-1.7-x86_64-linux-opt + sudo chmod +x /usr/bin/cvc4 + #install yices + sudo add-apt-repository ppa:sri-csl/formal-methods + sudo apt-get update + sudo apt-get install yices2 + #install boolector + mkdir -p /tmp/build + cd /tmp/build + git clone https://github.com/boolector/boolector.git + cd boolector + # Version 3.2.1 + git checkout "f61c0dcf4a76e2f7766a6358bfb9c16ca8217224" + git log -1 --oneline > ../boolector.commit + ./contrib/setup-lingeling.sh + ./contrib/setup-btor2tools.sh + ./configure.sh + cd build + make -j4 + mkdir -p /tmp/boolector + sudo make DESTDIR=/usr install + # Install solc unconditionally because it only takes a second or two + sudo wget -O /usr/bin/solc https://github.com/ethereum/solidity/releases/download/v0.4.24/solc-static-linux + sudo chmod +x /usr/bin/solc + - name: Run Tests + env: + TEST_TYPE: ${{ matrix.type }} + run: | + cp scripts/run_tests.sh . + ./run_tests.sh + + upload: + runs-on: ubuntu-18.04 + needs: tests + steps: + - uses: actions/checkout@v2 + - name: Set up Python 3.6 + uses: actions/setup-python@v1 + with: + python-version: 3.6 + - name: Build Dist + run: | + python3 -m pip install wheel + python3 setup.py sdist bdist_wheel + - name: Upload to PyPI + uses: pypa/gh-action-pypi-publish@v1.2.2 + with: + password: ${{ secrets.PYPI_UPLOAD }} diff --git a/CHANGELOG.md b/CHANGELOG.md index ddcc0caa8..452fcb487 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,6 +1,30 @@ # Change Log -## [Unreleased](https://github.com/trailofbits/manticore/compare/0.3.5...HEAD) +## [Unreleased](https://github.com/trailofbits/manticore/compare/0.3.6...HEAD) + +## 0.3.6 - 2021-06-09 + +Thanks to our external contributors! + - [timgates42](https://github.com/trailofbits/manticore/commits?author=timgates42) + +### Ethereum +* **[Changed API]** Default to quick mode: disable detectors and gas [#2457](https://github.com/trailofbits/manticore/pull/2457) +* Allow symbolic balances from the beginning of execution [#1818](https://github.com/trailofbits/manticore/pull/1818) +* Disable EVM Events in Testcases [#2417](https://github.com/trailofbits/manticore/pull/2417) + +### Native +* **[Added API]** Syscall-specific hooks [#2389](https://github.com/trailofbits/manticore/pull/2389) +* Fix wildcard behavior in symbolic files [#2454](https://github.com/trailofbits/manticore/pull/2454) +* Bugfixes for control transfer between Manticore & Unicorn [#1796](https://github.com/trailofbits/manticore/pull/1796) + +### Other +* Run multiple SMT solvers in parallel, take the fastest response [#2420](https://github.com/trailofbits/manticore/pull/2420) +* Add socket for TUI [#1620](https://github.com/trailofbits/manticore/pull/1620) +* Memory usage improvements in expression system [#2394](https://github.com/trailofbits/manticore/pull/2394) +* Support for Boolector [#2410](https://github.com/trailofbits/manticore/pull/2410) +* Solver Statistics API [#2415](https://github.com/trailofbits/manticore/pull/2415) +* Allow duplicated config options [#2397](https://github.com/trailofbits/manticore/pull/2397) + ## 0.3.5 - 2020-11-06 diff --git a/README.md b/README.md index b70fa3875..bd33f958f 100644 --- a/README.md +++ b/README.md @@ -46,10 +46,10 @@ Option 2: Installing from PyPI, with extra dependencies needed to execute native pip install "manticore[native]" ``` -Option 3: Installing a nightly development build (fill in the latest version from [the PyPI history](https://pypi.org/project/manticore/#history)): +Option 3: Installing a nightly development build: ```bash -pip install "manticore[native]==0.x.x.devYYMMDD" +pip install --pre "manticore[native]" ``` Option 4: Installing from the `master` branch: diff --git a/docs/conf.py b/docs/conf.py index 0aa17b00a..8c5ab6ebc 100644 --- a/docs/conf.py +++ b/docs/conf.py @@ -54,9 +54,9 @@ # built documents. # # The short X.Y version. -version = "0.3.5" +version = "0.3.6" # The full version, including alpha/beta/rc tags. -release = "0.3.5" +release = "0.3.6" # The language for content autogenerated by Sphinx. Refer to documentation # for a list of supported languages. diff --git a/examples/script/symbolic_file.py b/examples/script/symbolic_file.py new file mode 100755 index 000000000..73d5a2e12 --- /dev/null +++ b/examples/script/symbolic_file.py @@ -0,0 +1,77 @@ +#!/usr/bin/env python + +""" +Example to show usage of introducing a file with symbolic contents + +This script should be the equivalent of: + $ echo "+++++++++++++" > symbolic_file.txt + $ manticore -v --file symbolic_file.txt ../linux/fileio symbolic_file.txt +""" +import copy +import glob +import os +import pathlib +import sys +import tempfile + +from manticore.__main__ import main + + +def test_symbolic_file(tmp_path): + # Run this file with Manticore + filepath = pathlib.Path(__file__).resolve().parent.parent / pathlib.Path("linux/fileio") + assert filepath.exists(), f"Please run the Makefile in {filepath.parent} to build {filepath}" + + # Temporary workspace for Manticore + workspace_dir = tmp_path / "mcore_workspace" + workspace_dir.mkdir(parents=True, exist_ok=True) + assert ( + len(os.listdir(workspace_dir)) == 0 + ), f"Manticore workspace {workspace_dir} should be empty before running" + + # Manticore will search for and read this partially symbolic file + sym_file_name = "symbolic_file.txt" + sym_file = tmp_path / sym_file_name + sym_file.write_text("+++++++++++++") + + # Program arguments that would be passed to Manticore via CLI + manticore_args = [ + # Show some progress + "-v", + # Register our symbolic file with Manticore + "--file", + str(sym_file), + # Setup workspace, for this test, or omit to use current directory + "--workspace", + str(workspace_dir), + # Manticore will execute our file here with arguments + str(filepath), + str(sym_file), + ] + + # Bad hack to workaround passing the above arguments like we do on command + # line and have them parsed with argparse + backup_argv = copy.deepcopy(sys.argv[1:]) + del sys.argv[1:] + sys.argv.extend(manticore_args) + + # Call Manticore's main with our new argv list for argparse + main() + + del sys.argv[1:] + sys.argv.extend(backup_argv) + + # Manticore will write out the concretized contents of our symbolic file for + # each path in the program + all_concretized_sym_files = glob.glob(str(workspace_dir / f"*{sym_file_name}")) + assert ( + len(all_concretized_sym_files) > 1 + ), "Should have found more than 1 path through the program" + assert any( + map(lambda f: b"open sesame" in pathlib.Path(f).read_bytes(), all_concretized_sym_files) + ), "Could not find 'open sesame' in our concretized symbolic file" + + +if __name__ == "__main__": + with tempfile.TemporaryDirectory() as workspace: + test_symbolic_file(pathlib.Path(workspace)) diff --git a/manticore/__main__.py b/manticore/__main__.py index 2f7aa8583..3e8924ec6 100644 --- a/manticore/__main__.py +++ b/manticore/__main__.py @@ -230,10 +230,10 @@ def positive(value): ) eth_flags.add_argument( - "--quick-mode", + "--thorough-mode", action="store_true", - help="Configure Manticore for quick exploration. Disable gas, generate testcase only for alive states, " - "do not explore constant functions. Disable all detectors.", + help="Configure Manticore for more exhaustive exploration. Evaluate gas, generate testcases for dead states, " + "explore constant functions, and run a small suite of detectors.", ) config_flags = parser.add_argument_group("Constants") diff --git a/manticore/core/manticore.py b/manticore/core/manticore.py index 7f48ab25b..5c348155b 100644 --- a/manticore/core/manticore.py +++ b/manticore/core/manticore.py @@ -14,7 +14,7 @@ import shlex from ..core.plugin import Plugin, IntrospectionAPIPlugin, StateDescriptor -from ..core.smtlib import Expression +from ..core.smtlib import Expression, SOLVER_STATS from ..core.state import StateBase from ..core.workspace import ManticoreOutput from ..exceptions import ManticoreError @@ -49,7 +49,11 @@ default=False, description="If True enables to run workers over the network UNIMPLEMENTED", ) -consts.add("procs", default=10, description="Number of parallel processes to spawn") +consts.add( + "procs", + default=12, + description="Number of parallel processes to spawn in order to run every task, including solvers", +) proc_type = MProcessingType.threading if sys.platform != "linux": @@ -380,8 +384,9 @@ def __init__( raise TypeError(f"Invalid initial_state type: {type(initial_state).__name__}") self._put_state(initial_state) + nworkers = max(consts.procs // initial_state._solver.ncores, 1) # Workers will use manticore __dict__ So lets spawn them last - self._workers = [self._worker_type(id=i, manticore=self) for i in range(consts.procs)] + self._workers = [self._worker_type(id=i, manticore=self) for i in range(nworkers)] # Create log capture worker. We won't create the rest of the daemons until .run() is called self._daemon_threads: typing.Dict[int, DaemonThread] = { @@ -1106,6 +1111,10 @@ def run(self): """ Runs analysis. """ + # Start measuring the execution time + with self.locked_context() as context: + context["time_started"] = time.time() + # Delete state cache # The cached version of a state may get out of sync if a worker in a # different process modifies the state @@ -1219,7 +1228,28 @@ def save_run_data(self): with self._output.save_stream("manticore.yml") as f: config.save(f) + with self._output.save_stream("global.solver_stats") as f: + for s, n in sorted(SOLVER_STATS.items()): + f.write("%s: %d\n" % (s, n)) + + if SOLVER_STATS["timeout"] > 0 or SOLVER_STATS["unknown"] > 0: + logger.warning( + "The SMT solvers returned timeout or unknown for certain program paths. Results could not cover the entire set of possible paths" + ) + logger.info("Results in %s", self._output.store.uri) + + time_ended = time.time() + + with self.locked_context() as context: + if "time_started" in context: + time_elapsed = time_ended - context["time_started"] + logger.info("Total time: %s", time_elapsed) + context["time_ended"] = time_ended + context["time_elapsed"] = time_elapsed + else: + logger.warning("Manticore failed to run") + self.wait_for_log_purge() def introspect(self) -> typing.Dict[int, StateDescriptor]: diff --git a/manticore/core/plugin.py b/manticore/core/plugin.py index 80a7c091a..4e3f10dfc 100644 --- a/manticore/core/plugin.py +++ b/manticore/core/plugin.py @@ -467,6 +467,10 @@ class IntrospectionAPIPlugin(Plugin): NAME = "introspector" + @property + def name(self) -> str: + return "IntrospectionAPIPlugin" + def create_state(self, state_id: int): """ Adds a StateDescriptor to the context in the READY state list diff --git a/manticore/core/smtlib/solver.py b/manticore/core/smtlib/solver.py index 1affa3b1e..8ef71096d 100644 --- a/manticore/core/smtlib/solver.py +++ b/manticore/core/smtlib/solver.py @@ -15,15 +15,18 @@ # You can add new constraints. A new constraint may change the state from {None, sat} to {sat, unsat, unknown} import os +import fcntl import shutil import threading from queue import Queue import collections import shlex import time +from abc import abstractmethod from functools import lru_cache -from typing import Dict, Tuple, Sequence, Optional +from typing import Any, Dict, Tuple, Sequence, Optional, List from subprocess import PIPE, Popen, check_output +from random import shuffle import re from . import operators as Operators from .constraints import * @@ -32,17 +35,6 @@ from ...utils import config from . import issymbolic - -class SolverType(config.ConfigEnum): - """Used as configuration constant for choosing solver flavor""" - - z3 = "z3" - cvc4 = "cvc4" - yices = "yices" - auto = "auto" - boolector = "boolector" - - logger = logging.getLogger(__name__) consts = config.get_group("smt") consts.add("timeout", default=120, description="Timeout, in seconds, for each Z3 invocation") @@ -63,13 +55,10 @@ class SolverType(config.ConfigEnum): "optimize", default=True, description="Use smtlib command optimize to find min/max if available" ) -consts.add( - "solver", - default=SolverType.auto, - description="Choose default smtlib2 solver (z3, yices, cvc4, boolector, auto)", -) - # Regular expressions used by the solver +RE_GET_EXPR_VALUE_ALL = re.compile( + "\(([a-zA-Z0-9_]*)[ \\n\\s]*(#b[0-1]*|#x[0-9a-fA-F]*|[\(]?_ bv[0-9]* [0-9]*|true|false)\\)" +) RE_GET_EXPR_VALUE_FMT_BIN = re.compile(r"\(\((?P(.*))[ \n\s]*#b(?P([0-1]*))\)\)") RE_GET_EXPR_VALUE_FMT_DEC = re.compile(r"\(\((?P(.*))\ \(_\ bv(?P(\d*))\ \d*\)\)\)") RE_GET_EXPR_VALUE_FMT_HEX = re.compile(r"\(\((?P(.*))\ #x(?P([0-9a-fA-F]*))\)\)") @@ -78,6 +67,46 @@ class SolverType(config.ConfigEnum): ) RE_MIN_MAX_OBJECTIVE_EXPR_VALUE = re.compile(r"(?P.*?)\s+\|->\s+(?P.*)", re.DOTALL) +SOLVER_STATS = {"unknown": 0, "timeout": 0} + + +class SolverType(config.ConfigEnum): + """Used as configuration constant for choosing solver flavor""" + + z3 = "z3" + cvc4 = "cvc4" + yices = "yices" + auto = "auto" + portfolio = "portfolio" + boolector = "boolector" + + +consts.add( + "solver", + default=SolverType.auto, + description="Choose default smtlib2 solver (z3, yices, cvc4, boolector, portfolio, auto)", +) + + +def _convert(v): + r = None + if v == "true": + r = True + elif v == "false": + r = False + elif v.startswith("#b"): + r = int(v[2:], 2) + elif v.startswith("#x"): + r = int(v[2:], 16) + elif v.startswith("_ bv"): + r = int(v[len("_ bv") : -len(" 256")], 10) + elif v.startswith("(_ bv"): + v = v[len("(_ bv") :] + r = int(v[: v.find(" ")], 10) + + assert r is not None + return r + class SingletonMixin(object): __singleton_instances: Dict[Tuple[int, int], "SingletonMixin"] = {} @@ -178,6 +207,7 @@ def __init__(self, command: str, debug: bool = False): self._proc: Optional[Popen] = None self._command = command self._debug = debug + self._last_buf = "" def start(self): """Spawns POpen solver process""" @@ -192,6 +222,11 @@ def start(self): close_fds=True, ) + # stdout should be non-blocking + fl = fcntl.fcntl(self._proc.stdout, fcntl.F_GETFL) + fcntl.fcntl(self._proc.stdout, fcntl.F_SETFL, fl | os.O_NONBLOCK) + self._last_buf = "" + def stop(self): """ Stops the solver process by: @@ -211,18 +246,6 @@ def stop(self): # No need to wait for termination, zombies avoided. self._proc = None - def __readline_and_count(self): - assert self._proc - assert self._proc.stdout - buf = self._proc.stdout.readline() # No timeout enforced here - # If debug is enabled check if the solver reports a syntax error - # Error messages may contain an unbalanced parenthesis situation - if self._debug: - if "(error" in buf: - raise SolverException(f"Error in smtlib: {buf}") - lparen, rparen = map(sum, zip(*((c == "(", c == ")") for c in buf))) - return buf, lparen, rparen - def send(self, cmd: str) -> None: """ Send a string to the solver. @@ -242,17 +265,50 @@ def send(self, cmd: str) -> None: ) raise e - def recv(self) -> str: - """Reads the response from the smtlib solver""" - buf, left, right = self.__readline_and_count() - bufl = [buf] - while left != right: - buf, l, r = self.__readline_and_count() - bufl.append(buf) - left += l - right += r + def recv(self, wait=True) -> Optional[str]: + """Reads the response from the smtlib solver + + :param wait: a boolean that indicate to wait with a blocking call + until the results are available. Otherwise, it returns None if the solver + does not respond. + + """ + tries = 0 + timeout = 0.0 + + buf = "" + if self._last_buf != "": # we got a partial response last time, let's use it + buf = buf + self._last_buf + + while True: + try: + buf = buf + self._proc.stdout.read() # type: ignore + buf = buf.strip() + except TypeError: + if not wait: + if buf != "": # we got an error, but something was returned, let's save it + self._last_buf = buf + return None + else: + tries += 1 + + if buf == "": + continue + + # this verifies if the response from the solver is complete (it has balanced brackets) + lparen, rparen = map(sum, zip(*((c == "(", c == ")") for c in buf))) + if lparen == rparen and buf != "": + break - buf = "".join(bufl).strip() + if tries > 3: + time.sleep(timeout) + timeout += 0.1 + + buf = buf.strip() + self._last_buf = "" + + if "(error" in buf: + raise SolverException(f"Error in smtlib: {buf}") if self._debug: logger.debug("<%s", buf) @@ -269,6 +325,19 @@ def is_started(self): class SMTLIBSolver(Solver): + ncores: Optional[int] = None + sname: Optional[str] = None + + @classmethod + @abstractmethod + def command(self) -> str: + raise NotImplementedError() + + @classmethod + @abstractmethod + def inits(self) -> List[str]: + raise NotImplementedError() + def __init__( self, command: str, @@ -333,15 +402,28 @@ def _is_sat(self) -> bool: start = time.time() self._smtlib.send("(check-sat)") status = self._smtlib.recv() + assert status is not None logger.debug("Check took %s seconds (%s)", time.time() - start, status) + if "ALARM TRIGGERED" in status: + return False + if status not in ("sat", "unsat", "unknown"): raise SolverError(status) if consts.defaultunsat: if status == "unknown": logger.info("Found an unknown core, probably a solver timeout") + SOLVER_STATS["timeout"] += 1 status = "unsat" + raise SolverUnknown(status) + if status == "unknown": + SOLVER_STATS["unknown"] += 1 raise SolverUnknown(status) + else: + assert self.sname is not None + SOLVER_STATS.setdefault(self.sname, 0) + SOLVER_STATS[self.sname] += 1 + return status == "sat" def _assert(self, expression: Bool): @@ -352,6 +434,7 @@ def _assert(self, expression: Bool): def __getvalue_bv(self, expression_str: str) -> int: self._smtlib.send(f"(get-value ({expression_str}))") t = self._smtlib.recv() + assert t is not None base = 2 m = RE_GET_EXPR_VALUE_FMT_BIN.match(t) if m is None: @@ -371,6 +454,14 @@ def __getvalue_bool(self, expression_str): ret = self._smtlib.recv() return {"true": True, "false": False, "#b0": False, "#b1": True}[ret[2:-2].split(" ")[1]] + def __getvalue_all(self, expressions_str: List[str], is_bv: List[bool]) -> Dict[str, int]: + all_expressions_str = " ".join(expressions_str) + self._smtlib.send(f"(get-value ({all_expressions_str}))") + ret_solver: Optional[str] = self._smtlib.recv() + assert ret_solver is not None + return_values = re.findall(RE_GET_EXPR_VALUE_ALL, ret_solver) + return {value[0]: _convert(value[1]) for value in return_values} + def _getvalue(self, expression) -> Union[int, bool, bytes]: """ Ask the solver for one possible assignment for given expression using current set of constraints. @@ -472,6 +563,7 @@ def _optimize_generic(self, constraints: ConstraintSet, x: BitVec, goal: str, ma M = L if time.time() - start > consts.timeout: + SOLVER_STATS["timeout"] += 1 raise SolverError("Timeout") # reset to before the dichotomic search @@ -494,11 +586,15 @@ def _optimize_generic(self, constraints: ConstraintSet, x: BitVec, goal: str, ma self._assert(X != last_value) i = i + 1 if i > max_iter: + SOLVER_STATS["unknown"] += 1 raise SolverError("Optimizing error, maximum number of iterations was reached") if time.time() - start > consts.timeout: + SOLVER_STATS["timeout"] += 1 raise SolverError("Timeout") if last_value is not None: return last_value + + SOLVER_STATS["unknown"] += 1 raise SolverError("Optimizing error, unsat or unknown core") @lru_cache(maxsize=32) @@ -555,6 +651,7 @@ def get_all_values( else: raise TooManySolutions(result) if time.time() - start > consts.timeout: + SOLVER_STATS["timeout"] += 1 if silent: logger.info("Timeout searching for all solutions") return list(result) @@ -591,77 +688,130 @@ def _optimize_fancy(self, constraints: ConstraintSet, x: BitVec, goal: str, max_ self._smtlib.send("(%s %s)" % (goal, aux.name)) self._smtlib.send("(check-sat)") _status = self._smtlib.recv() + + assert self.sname is not None + SOLVER_STATS.setdefault(self.sname, 0) + SOLVER_STATS[self.sname] += 1 + if _status == "sat": return self._getvalue(aux) raise SolverError("Optimize failed") def get_value(self, constraints: ConstraintSet, *expressions): + values = self.get_value_in_batch(constraints, expressions) + if len(expressions) == 1: + return values[0] + else: + return values + + def get_value_in_batch(self, constraints: ConstraintSet, expressions): """ Ask the solver for one possible result of given expressions using given set of constraints. """ - values = [] + values: List[Any] = [None] * len(expressions) start = time.time() with constraints.related_to(*expressions) as temp_cs: - for expression in expressions: + vars: List[Any] = [] + for idx, expression in enumerate(expressions): if not issymbolic(expression): - values.append(expression) + values[idx] = expression + vars.append(None) continue assert isinstance(expression, (Bool, BitVec, Array)) if isinstance(expression, Bool): var = temp_cs.new_bool() + vars.append(var) + temp_cs.add(var == expression) elif isinstance(expression, BitVec): var = temp_cs.new_bitvec(expression.size) + vars.append(var) + temp_cs.add(var == expression) elif isinstance(expression, Array): var = [] - result = [] for i in range(expression.index_max): subvar = temp_cs.new_bitvec(expression.value_bits) var.append(subvar) temp_cs.add(subvar == simplify(expression[i])) - self._reset(temp_cs.to_string()) - if not self._is_sat(): - raise SolverError( - "Solver could not find a value for expression under current constraint set" - ) - - for i in range(expression.index_max): - result.append(self.__getvalue_bv(var[i].name)) - values.append(bytes(result)) - if time.time() - start > consts.timeout: - raise SolverError("Timeout") - continue + vars.append(var) - temp_cs.add(var == expression) + self._reset(temp_cs.to_string()) + if not self._is_sat(): + raise SolverError( + "Solver could not find a value for expression under current constraint set" + ) - self._reset(temp_cs.to_string()) + values_to_ask: List[str] = [] + is_bv: List[bool] = [] + for idx, expression in enumerate(expressions): + if not issymbolic(expression): + continue + var = vars[idx] + if isinstance(expression, Bool): + values_to_ask.append(var.name) + is_bv.append(False) + if isinstance(expression, BitVec): + values_to_ask.append(var.name) + is_bv.append(True) + if isinstance(expression, Array): + # result = [] + for i in range(expression.index_max): + values_to_ask.append(var[i].name) + is_bv.append(True) - if not self._is_sat(): - raise SolverError( - "Solver could not find a value for expression under current constraint set" - ) + if values_to_ask == []: + return values + values_returned = self.__getvalue_all(values_to_ask, is_bv) + for idx, expression in enumerate(expressions): + if not issymbolic(expression): + continue + var = vars[idx] if isinstance(expression, Bool): - values.append(self.__getvalue_bool(var.name)) + values[idx] = values_returned[var.name] if isinstance(expression, BitVec): - values.append(self.__getvalue_bv(var.name)) + if var.name not in values_returned: + logger.error( + "var.name", var.name, "not in values_returned", values_returned + ) + + values[idx] = values_returned[var.name] + if isinstance(expression, Array): + result = [] + for i in range(expression.index_max): + result.append(values_returned[var[i].name]) + values[idx] = bytes(result) + if time.time() - start > consts.timeout: + SOLVER_STATS["timeout"] += 1 raise SolverError("Timeout") - if len(expressions) == 1: - return values[0] - else: - return values + return values class Z3Solver(SMTLIBSolver): + sname = "z3" + + @classmethod + def command(self) -> str: + return f"{consts.z3_bin} -t:{consts.timeout * 1000} -memory:{consts.memory} -smt2 -in" + + @classmethod + def inits(self) -> List[str]: + return [ + "(set-logic QF_AUFBV)", + "(set-option :global-decls false)", + "(set-option :tactic.solve_eqs.context_solve false)", + ] + def __init__(self): """ Build a Z3 solver instance. This is implemented using an external z3 solver (via a subprocess). See https://github.com/Z3Prover/z3 """ - command = f"{consts.z3_bin} -t:{consts.timeout * 1000} -memory:{consts.memory} -smt2 -in" + command = self.command() + self.ncores = 1 init, support_minmax, support_reset, multiple_check = self.__autoconfig() super().__init__( @@ -675,26 +825,12 @@ def __init__(self): ) def __autoconfig(self): - init = [ - # http://smtlib.cs.uiowa.edu/logics-all.shtml#QF_AUFBV - # Closed quantifier-free formulas over the theory of bitvectors and bitvector arrays extended with - # free sort and function symbols. - "(set-logic QF_AUFBV)", - # The declarations and definitions will be scoped - "(set-option :global-decls false)", - ] + init = self.inits() # To cache what get-info returned; can be directly set when writing tests self.version = self._solver_version() support_reset = True - if self.version > Version(4, 8, 4): - # sam.moelius: Option "tactic.solve_eqs.context_solve" was turned on by this commit in z3: - # https://github.com/Z3Prover/z3/commit/3e53b6f2dbbd09380cd11706cabbc7e14b0cc6a2 - # Turning it off greatly improves Manticore's performance on test_integer_overflow_storageinvariant - # in test_consensys_benchmark.py. - init.append("(set-option :tactic.solve_eqs.context_solve false)") - support_minmax = self.version >= Version(4, 4, 1) # Certain version of Z3 fails to handle multiple check-sat @@ -729,9 +865,20 @@ def _solver_version(self) -> Version: class YicesSolver(SMTLIBSolver): + sname = "yices" + + @classmethod + def command(self) -> str: + return f"{consts.yices_bin} --timeout={consts.timeout} --incremental" + + @classmethod + def inits(self) -> List[str]: + return ["(set-logic QF_AUFBV)"] + def __init__(self): - init = ["(set-logic QF_AUFBV)"] - command = f"{consts.yices_bin} --timeout={consts.timeout} --incremental" + init = self.inits() + command = self.command() + self.ncores = 1 super().__init__( command=command, init=init, @@ -742,19 +889,200 @@ def __init__(self): class CVC4Solver(SMTLIBSolver): + sname = "cvc4" + + @classmethod + def command(self) -> str: + return f"{consts.cvc4_bin} --tlimit={consts.timeout * 1000} --lang=smt2 --incremental" + + @classmethod + def inits(self) -> List[str]: + return ["(set-logic QF_AUFBV)", "(set-option :produce-models true)"] + def __init__(self): - init = ["(set-logic QF_AUFBV)", "(set-option :produce-models true)"] - command = f"{consts.cvc4_bin} --tlimit={consts.timeout * 1000} --lang=smt2 --incremental" + init = self.inits() + command = self.command() + self.ncores = 1 super().__init__(command=command, init=init) class BoolectorSolver(SMTLIBSolver): - def __init__(self): - init = ["(set-logic QF_AUFBV)", "(set-option :produce-models true)"] - command = f"{consts.boolector_bin} --time={consts.timeout} -i" + sname = "boolector" + + @classmethod + def command(self) -> str: + return f"{consts.boolector_bin} --time={consts.timeout} -i" + + @classmethod + def inits(self) -> List[str]: + return ["(set-logic QF_AUFBV)", "(set-option :produce-models true)"] + + def __init__(self, args: List[str] = []): + init = self.inits() + command = self.command() + self.ncores = 1 super().__init__(command=command, init=init) +class SmtlibPortfolio: + def __init__(self, solvers: List[str], debug: bool = False): + """Single smtlib interactive process + + :param command: the shell command to execute + :param debug: log all messaging + """ + self._procs: Dict[str, SmtlibProc] = {} + self._solvers: List[str] = solvers + self._debug = debug + + def start(self): + if len(self._procs) == 0: + for solver in self._solvers: + self._procs[solver] = SmtlibProc(solver_selector[solver].command(), self._debug) + + for _, proc in self._procs.items(): + proc.start() + + def stop(self): + """ + Stops the solver process by: + - sending a SIGKILL signal, + - waiting till the process terminates (so we don't leave a zombie process) + """ + for solver, proc in self._procs.items(): + proc.stop() + + def send(self, cmd: str) -> None: + """ + Send a string to the solver. + + :param cmd: a SMTLIBv2 command (ex. (check-sat)) + """ + assert len(self._procs) > 0 + inds = list(range(len(self._procs))) + shuffle(inds) + + for i in inds: + solver = self._solvers[i] + proc = self._procs[solver] + if not proc.is_started(): + continue + + proc.send(cmd) + + def recv(self) -> str: + """Reads the response from the smtlib solver""" + tries = 0 + timeout = 0.0 + inds = list(range(len(self._procs))) + # print(self._solvers) + while True: + shuffle(inds) + for i in inds: + + solver = self._solvers[i] + proc = self._procs[solver] + + if not proc.is_started(): + continue + + buf = proc.recv(wait=False) + if buf is not None: + + for osolver in self._solvers: # iterate on all the solvers + if osolver != solver: # check for the other ones + self._procs[osolver].stop() # stop them + + return buf + else: + tries += 1 + + if tries > 10 * len(self._procs): + time.sleep(timeout) + timeout += 0.1 + + def _restart(self) -> None: + """Auxiliary to start or restart the external solver""" + self.stop() + self.start() + + def is_started(self): + return len(self._procs) > 0 + + def init(self): + assert len(self._solvers) == len(self._procs) + for solver, proc in self._procs.items(): + for cfg in solver_selector[solver].inits(): + proc.send(cfg) + + +class PortfolioSolver(SMTLIBSolver): + sname = "portfolio" + + def __init__(self): + solvers = [] + if shutil.which(consts.yices_bin): + solvers.append(consts.solver.yices.name) + # not sure we want z3 here, since it tends to be slower + # if shutil.which(consts.z3_bin): + # solvers.append(consts.solver.z3.name) + if shutil.which(consts.cvc4_bin): + solvers.append(consts.solver.cvc4.name) + if shutil.which(consts.boolector_bin): + solvers.append(consts.solver.boolector.name) + if solvers == []: + raise SolverException( + f"No Solver not found. Install one ({consts.yices_bin}, {consts.z3_bin}, {consts.cvc4_bin}, {consts.boolector_bin})." + ) + + logger.info("Creating portfolio with solvers: " + ",".join(solvers)) + assert len(solvers) > 0 + support_reset: bool = False + support_minmax: bool = False + support_pushpop: bool = False + multiple_check: bool = True + debug: bool = False + + self._smtlib: SmtlibPortfolio = SmtlibPortfolio(solvers, debug) + self._support_minmax = support_minmax + self._support_reset = support_reset + self._support_pushpop = support_pushpop + self._multiple_check = multiple_check + + if not self._support_pushpop: + setattr(self, "_push", None) + setattr(self, "_pop", None) + + if self._support_minmax and consts.optimize: + setattr(self, "optimize", self._optimize_fancy) + else: + setattr(self, "optimize", self._optimize_generic) + self.ncores = len(solvers) + + def _reset(self, constraints: Optional[str] = None) -> None: + """Auxiliary method to reset the smtlib external solver to initial defaults""" + if self._support_reset: + self._smtlib.start() # does not do anything if already started + self._smtlib.send("(reset)") + else: + self._smtlib.stop() # does not do anything if already stopped + self._smtlib.start() + + self._smtlib.init() + + if constraints is not None: + self._smtlib.send(constraints) + + +solver_selector = { + "cvc4": CVC4Solver, + "boolector": BoolectorSolver, + "yices": YicesSolver, + "z3": Z3Solver, + "portfolio": PortfolioSolver, +} + + class SelectedSolver: choice = None @@ -774,13 +1102,9 @@ def instance(cls): raise SolverException( f"No Solver not found. Install one ({consts.yices_bin}, {consts.z3_bin}, {consts.cvc4_bin}, {consts.boolector_bin})." ) + else: cls.choice = consts.solver - SelectedSolver = { - "cvc4": CVC4Solver, - "boolector": BoolectorSolver, - "yices": YicesSolver, - "z3": Z3Solver, - }[cls.choice.name] + SelectedSolver = solver_selector[cls.choice.name] return SelectedSolver.instance() diff --git a/manticore/core/state.py b/manticore/core/state.py index 854dc95bc..4a6fc65e3 100644 --- a/manticore/core/state.py +++ b/manticore/core/state.py @@ -1,7 +1,10 @@ import copy import logging +from typing import List, Tuple, Sequence + from .smtlib import solver, Bool, issymbolic, BitVecConstant +from .smtlib.expression import Expression from ..utils.event import Eventful from ..utils.helpers import PickleSerializer from ..utils import config @@ -452,30 +455,41 @@ def solve_one(self, expr, constrain=False): """ return self.solve_one_n(expr, constrain=constrain)[0] - def solve_one_n(self, *exprs, constrain=False): + def solve_one_n(self, *exprs: Expression, constrain: bool = False) -> List[int]: """ - Concretize a symbolic :class:`~manticore.core.smtlib.expression.Expression` into - one solution. + Concretize a list of symbolic :class:`~manticore.core.smtlib.expression.Expression` into + a list of solutions. :param exprs: An iterable of manticore.core.smtlib.Expression :param bool constrain: If True, constrain expr to solved solution value - :return: Concrete value or a tuple of concrete values - :rtype: int + :return: List of concrete value or a tuple of concrete values """ - values = [] - for expr in exprs: - if not issymbolic(expr): - values.append(expr) - else: - expr = self.migrate_expression(expr) - value = self._solver.get_value(self._constraints, expr) - if constrain: - self.constrain(expr == value) - # Include forgiveness here - if isinstance(value, bytearray): - value = bytes(value) - values.append(value) - return values + return self.solve_one_n_batched(exprs, constrain) + + def solve_one_n_batched( + self, exprs: Sequence[Expression], constrain: bool = False + ) -> List[int]: + """ + Concretize a list of symbolic :class:`~manticore.core.smtlib.expression.Expression` into + a list of solutions. + :param exprs: An iterable of manticore.core.smtlib.Expression + :param bool constrain: If True, constrain expr to solved solution value + :return: List of concrete value or a tuple of concrete values + """ + # Return ret instead of value, to allow the bytearray/bytes conversion + ret = [] + exprs = [self.migrate_expression(x) for x in exprs] + values = self._solver.get_value_in_batch(self._constraints, exprs) + assert len(values) == len(exprs) + for idx, expr in enumerate(exprs): + value = values[idx] + if constrain: + self.constrain(expr == values[idx]) + # Include forgiveness here + if isinstance(value, bytearray): + value = bytes(value) + ret.append(value) + return ret def solve_n(self, expr, nsolves): """ diff --git a/manticore/core/workspace.py b/manticore/core/workspace.py index a4a711ae3..9eaa84759 100644 --- a/manticore/core/workspace.py +++ b/manticore/core/workspace.py @@ -658,7 +658,7 @@ def save_constraints(testcase, state: StateBase): @staticmethod def save_input_symbols(testcase, state: StateBase): with testcase.open_stream("input") as f: - for symbol in state.input_symbols: + bufs = state.solve_one_n_batched(state.input_symbols) + for symbol, buf in zip(state.input_symbols, bufs): # TODO - constrain=False here, so the extra migration shouldn't cause problems, right? - buf = state.solve_one(symbol) f.write(f"{symbol.name}: {buf!r}\n") diff --git a/manticore/ethereum/cli.py b/manticore/ethereum/cli.py index f48e86a45..93dbf4dff 100644 --- a/manticore/ethereum/cli.py +++ b/manticore/ethereum/cli.py @@ -89,7 +89,7 @@ def choose_detectors(args): def ethereum_main(args, logger): m = ManticoreEVM(workspace_url=args.workspace) - if args.quick_mode: + if not args.thorough_mode: args.avoid_constant = True args.exclude_all = True args.only_alive_testcases = True diff --git a/manticore/ethereum/manticore.py b/manticore/ethereum/manticore.py index 66f5e324b..a303dc6c3 100644 --- a/manticore/ethereum/manticore.py +++ b/manticore/ethereum/manticore.py @@ -270,36 +270,43 @@ def _compile_through_crytic_compile(filename, contract_name, libraries, crytic_c else: crytic_compile = CryticCompile(filename) - if not contract_name: - if len(crytic_compile.contracts_names_without_libraries) > 1: - raise EthereumError( - f"Solidity file must contain exactly one contract or you must select one. Contracts found: {', '.join(crytic_compile.contracts_names)}" - ) - contract_name = list(crytic_compile.contracts_names_without_libraries)[0] + if crytic_compile.is_in_multiple_compilation_unit(contract_name): + raise EthereumError( + f"{contract_name} is shared in multiple compilation units, please split the codebase to prevent the duplicate" + ) + + for compilation_unit in crytic_compile.compilation_units.values(): - if contract_name not in crytic_compile.contracts_names: - raise ValueError(f"Specified contract not found: {contract_name}") + if not contract_name: + if len(compilation_unit.contracts_names_without_libraries) > 1: + raise EthereumError( + f"Solidity file must contain exactly one contract or you must select one. Contracts found: {', '.join(compilation_unit.contracts_names)}" + ) + contract_name = list(compilation_unit.contracts_names_without_libraries)[0] + + if contract_name not in compilation_unit.contracts_names: + raise ValueError(f"Specified contract not found: {contract_name}") - name = contract_name + name = contract_name - libs = crytic_compile.libraries_names(name) - if libraries: - libs = [l for l in libs if l not in libraries] - if libs: - raise DependencyError(libs) + libs = compilation_unit.libraries_names(name) + if libraries: + libs = [l for l in libs if l not in libraries] + if libs: + raise DependencyError(libs) - bytecode = bytes.fromhex(crytic_compile.bytecode_init(name, libraries)) - runtime = bytes.fromhex(crytic_compile.bytecode_runtime(name, libraries)) - srcmap = crytic_compile.srcmap_init(name) - srcmap_runtime = crytic_compile.srcmap_runtime(name) - hashes = crytic_compile.hashes(name) - abi = crytic_compile.abi(name) + bytecode = bytes.fromhex(compilation_unit.bytecode_init(name, libraries)) + runtime = bytes.fromhex(compilation_unit.bytecode_runtime(name, libraries)) + srcmap = compilation_unit.srcmap_init(name) + srcmap_runtime = compilation_unit.srcmap_runtime(name) + hashes = compilation_unit.hashes(name) + abi = compilation_unit.abi(name) - filename = crytic_compile.filename_of_contract(name).absolute - with open(filename) as f: - source_code = f.read() + filename = compilation_unit.filename_of_contract(name).absolute + with open(filename) as f: + source_code = f.read() - return name, source_code, bytecode, runtime, srcmap, srcmap_runtime, hashes, abi + return name, source_code, bytecode, runtime, srcmap, srcmap_runtime, hashes, abi except InvalidCompilation as e: raise EthereumError( @@ -1058,8 +1065,8 @@ def multi_tx_analysis( args=None, compile_args=None, ): - owner_account = self.create_account(balance=10 ** 10, name="owner") - attacker_account = self.create_account(balance=10 ** 10, name="attacker") + owner_account = self.create_account(balance=10 ** 10, name="owner", address=0x10000) + attacker_account = self.create_account(balance=10 ** 10, name="attacker", address=0x20000) # Pretty print logger.info("Starting symbolic create contract") @@ -1786,8 +1793,6 @@ def worker_finalize(q): global_findings_stream.write(" ".join(source_code_snippet.splitlines(True))) global_findings_stream.write("\n") - self.save_run_data() - with self._output.save_stream("global.summary") as global_summary: # (accounts created by contract code are not in this list ) global_summary.write("Global runtime coverage:\n") @@ -1855,6 +1860,7 @@ def worker_finalize(q): for o in sorted(visited): f.write("0x%x\n" % o) + self.save_run_data() self.remove_all() def global_coverage(self, account): diff --git a/manticore/ethereum/verifier.py b/manticore/ethereum/verifier.py index c4ce7a075..f400d1f1f 100644 --- a/manticore/ethereum/verifier.py +++ b/manticore/ethereum/verifier.py @@ -398,10 +398,10 @@ def main(): eth_flags = parser.add_argument_group("Ethereum flags") eth_flags.add_argument( - "--quick-mode", + "--thorough-mode", action="store_true", - help="Configure Manticore for quick exploration. Disable gas, generate testcase only for alive states, " - "do not explore constant functions. Disable all detectors.", + help="Configure Manticore for more exhaustive exploration. Evaluate gas, generate testcases for dead states, " + "explore constant functions, and run a small suite of detectors.", ) eth_flags.add_argument( "--contract_name", type=str, help="The target contract name defined in the source code" diff --git a/manticore/native/manticore.py b/manticore/native/manticore.py index b9cdee2af..73ae24039 100644 --- a/manticore/native/manticore.py +++ b/manticore/native/manticore.py @@ -402,8 +402,6 @@ def resolve(self, symbol): raise ValueError(f"The {self.binary_path} ELFfile does not contain symbol {symbol}") def run(self, timeout=None): - with self.locked_context() as context: - context["time_started"] = time.time() with self.kill_timeout(timeout): super().run() @@ -414,16 +412,6 @@ def finalize(self): def save_run_data(self): super().save_run_data() - time_ended = time.time() - - with self.locked_context() as context: - time_elapsed = time_ended - context["time_started"] - - logger.info("Total time: %s", time_elapsed) - - context["time_ended"] = time_ended - context["time_elapsed"] = time_elapsed - def _make_initial_state(binary_path, **kwargs): with open(binary_path, "rb") as f: diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py index 631166c8e..37f889096 100644 --- a/manticore/platforms/evm.py +++ b/manticore/platforms/evm.py @@ -182,13 +182,24 @@ def concretize(self, state, constrain=False): :param state: a manticore state :param bool constrain: If True, constrain expr to concretized value """ - conc_caller = state.solve_one(self.caller, constrain=constrain) - conc_address = state.solve_one(self.address, constrain=constrain) - conc_value = state.solve_one(self.value, constrain=constrain) - conc_gas = state.solve_one(self.gas, constrain=constrain) - conc_data = state.solve_one(self.data, constrain=constrain) - conc_return_data = state.solve_one(self.return_data, constrain=constrain) - conc_used_gas = state.solve_one(self.used_gas, constrain=constrain) + all_elems = [ + self.caller, + self.address, + self.value, + self.gas, + self.data, + self._return_data, + self.used_gas, + ] + values = state.solve_one_n_batched(all_elems, constrain=constrain) + conc_caller = values[0] + conc_address = values[1] + conc_value = values[2] + conc_gas = values[3] + conc_data = values[4] + conc_return_data = values[5] + conc_used_gas = values[6] + return Transaction( self.sort, conc_address, @@ -291,9 +302,7 @@ def dump(self, stream, state, mevm, conc_tx=None): ) # is this redundant since arguments are all concrete? stream.write("Function call:\n") stream.write("Constructor(") - stream.write( - ",".join(map(repr, map(state.solve_one, arguments))) - ) # is this redundant since arguments are all concrete? + stream.write(",".join(map(repr, arguments))) stream.write(") -> %s %s\n" % (self.result, flagged(is_argument_symbolic))) if self.sort == "CALL": @@ -3435,14 +3444,18 @@ def dump(self, stream, state, mevm, message): stream.write("Balance: %d %s\n" % (balance, flagged(is_balance_symbolic))) storage = blockchain.get_storage(account_address) - concrete_indexes = set() - for sindex in storage.written: - concrete_indexes.add(state.solve_one(sindex, constrain=True)) + concrete_indexes = [] + if len(storage.written) > 0: + concrete_indexes = state.solve_one_n_batched(storage.written, constrain=True) + + concrete_values = [] + if len(concrete_indexes) > 0: + concrete_values = state.solve_one_n_batched(concrete_indexes, constrain=True) + + assert len(concrete_indexes) == len(concrete_values) + for index, value in zip(concrete_indexes, concrete_values): + stream.write(f"storage[{index:x}] = {value:x}\n") - for index in concrete_indexes: - stream.write( - f"storage[{index:x}] = {state.solve_one(storage[index], constrain=True):x}\n" - ) storage = blockchain.get_storage(account_address) stream.write("Storage: %s\n" % translate_to_smtlib(storage, use_bindings=False)) diff --git a/manticore/platforms/linux.py b/manticore/platforms/linux.py index 2671f2e61..0752a24a8 100644 --- a/manticore/platforms/linux.py +++ b/manticore/platforms/linux.py @@ -477,6 +477,13 @@ def __init__( """ super().__init__(path, flags) + # Convert to numeric value because we read the file as bytes + wildcard_buf: bytes = wildcard.encode() + assert ( + len(wildcard_buf) == 1 + ), f"SymbolicFile wildcard needs to be a single byte, not {wildcard_buf!r}" + wildcard_val = wildcard_buf[0] + # read the concrete data using the parent the read() form the File class data = self.file.read() @@ -490,7 +497,7 @@ def __init__( symbols_cnt = 0 for i in range(size): - if data[i] != wildcard: + if data[i] != wildcard_val: self.array[i] = data[i] else: symbols_cnt += 1 diff --git a/manticore/wasm/manticore.py b/manticore/wasm/manticore.py index a90f89463..864f4bcc3 100644 --- a/manticore/wasm/manticore.py +++ b/manticore/wasm/manticore.py @@ -46,9 +46,6 @@ def run(self, timeout=None): :param timeout: number of seconds after which to kill execution """ - with self.locked_context() as context: - context["time_started"] = time.time() - with self.kill_timeout(timeout): super().run() @@ -63,16 +60,6 @@ def finalize(self): def save_run_data(self): super().save_run_data() - time_ended = time.time() - - with self.locked_context() as context: - time_elapsed = time_ended - context["time_started"] - - logger.info("Total time: %s", time_elapsed) - - context["time_ended"] = time_ended - context["time_elapsed"] = time_elapsed - def __getattr__(self, item): """ Allows users to invoke & run functions in the same style as ethereum smart contracts. So: diff --git a/scripts/run_tests.sh b/scripts/run_tests.sh index 7ebeb21b0..6cf01ff57 100755 --- a/scripts/run_tests.sh +++ b/scripts/run_tests.sh @@ -48,6 +48,12 @@ launch_examples() { return 1 fi + echo "Running fileio symbolic file test..." + coverage run --append ./symbolic_file.py + if [ $? -ne 0 ]; then + return 1 + fi + return 0 } @@ -89,7 +95,7 @@ make_wasm_sym_tests(){ } install_truffle(){ - npm install -g truffle + npm install -g truffle@5.3.13 } run_truffle_tests(){ @@ -97,7 +103,7 @@ run_truffle_tests(){ mkdir truffle_tests cd truffle_tests truffle unbox metacoin - coverage run -m manticore . --contract MetaCoin --workspace output --exclude-all --evm.oog ignore --evm.txfail optimistic + coverage run -m manticore . --contract MetaCoin --workspace output --exclude-all --thorough-mode --evm.oog ignore --evm.txfail optimistic --smt.solver portfolio # Truffle smoke test. We test if manticore is able to generate states # from a truffle project. count=$(find output/ -name '*tx' -type f | wc -l) diff --git a/setup.py b/setup.py index ecbf05e2b..41b4a5319 100644 --- a/setup.py +++ b/setup.py @@ -49,9 +49,11 @@ def rtd_dependent_deps(): # https://stackoverflow.com/a/4792601 grumble grumble -dev_extension = "" +version = "0.3.6" if "--dev_release" in sys.argv: - dev_extension = ".dev" + date.today().strftime("%y%m%d") + major, minor, point = tuple(int(t) for t in version.split(".")) + dev_extension = f"dev{date.today().strftime('%y%m%d')}" + version = f"{major}.{minor}.{point + 1}.{dev_extension}" sys.argv.remove("--dev_release") setup( @@ -61,7 +63,7 @@ def rtd_dependent_deps(): long_description=long_description, url="https://github.com/trailofbits/manticore", author="Trail of Bits", - version="0.3.5" + dev_extension, + version=version, packages=find_packages(exclude=["tests", "tests.*"]), python_requires=">=3.6", install_requires=[ @@ -73,7 +75,7 @@ def rtd_dependent_deps(): "ply", "rlp", "intervaltree", - "crytic-compile>=0.1.8", + "crytic-compile>=0.2.0", "wasm", "dataclasses; python_version < '3.7'", "pyevmasm>=0.2.3", diff --git a/tests/ethereum/test_detectors.py b/tests/ethereum/test_detectors.py index b0431bf22..00924eea9 100644 --- a/tests/ethereum/test_detectors.py +++ b/tests/ethereum/test_detectors.py @@ -9,7 +9,7 @@ import shutil from manticore.platforms.evm import EVMWorld -from manticore.core.smtlib import operators, ConstraintSet +from manticore.core.smtlib import operators, ConstraintSet, SolverType from manticore.ethereum import ( DetectDelegatecall, DetectEnvInstruction, @@ -32,6 +32,9 @@ consts = config.get_group("core") consts.mprocessing = consts.mprocessing.single +consts = config.get_group("smt") +consts.solver = SolverType.portfolio + THIS_DIR = os.path.dirname(os.path.abspath(__file__)) diff --git a/tests/ethereum/test_general.py b/tests/ethereum/test_general.py index 72264c741..00308a73f 100644 --- a/tests/ethereum/test_general.py +++ b/tests/ethereum/test_general.py @@ -14,8 +14,7 @@ from manticore import ManticoreError from manticore.core.plugin import Plugin -from manticore.core.smtlib import ConstraintSet, operators -from manticore.core.smtlib import Z3Solver +from manticore.core.smtlib import ConstraintSet, operators, PortfolioSolver, SolverType from manticore.core.smtlib.expression import BitVec, BitVecVariable from manticore.core.smtlib.visitors import to_constant from manticore.core.state import TerminateState @@ -41,7 +40,9 @@ import contextlib -solver = Z3Solver.instance() +solver = PortfolioSolver.instance() +consts = config.get_group("smt") +consts.solver = SolverType.portfolio THIS_DIR = os.path.dirname(os.path.abspath(__file__)) @@ -73,7 +74,7 @@ class EthVerifierIntegrationTest(unittest.TestCase): def test_propverif(self): smtcfg = config.get_group("smt") with smtcfg.temp_vals(): - smtcfg.solver = smtcfg.solver.yices + smtcfg.solver = smtcfg.solver.portfolio filename = os.path.join(THIS_DIR, "contracts/prop_verifier.sol") f = io.StringIO() diff --git a/tests/ethereum/test_regressions.py b/tests/ethereum/test_regressions.py index f55ff457a..0db87a17b 100644 --- a/tests/ethereum/test_regressions.py +++ b/tests/ethereum/test_regressions.py @@ -235,7 +235,9 @@ def test_regressions_imports(self): def test_1102(self): with tempfile.TemporaryDirectory() as workspace: - self._simple_cli_run("1102.sol", workspace=workspace, testcases=True) + self._simple_cli_run( + "1102.sol", workspace=workspace, testcases=True, args=["--thorough-mode"] + ) with open(os.path.join(workspace, "global.findings")) as gf: global_findings = gf.read().splitlines() diff --git a/tests/native/test_integration_native.py b/tests/native/test_integration_native.py index 2821c559d..53e992064 100644 --- a/tests/native/test_integration_native.py +++ b/tests/native/test_integration_native.py @@ -287,12 +287,6 @@ def test_fclose_linux_amd64(self) -> None: """ self._test_no_crash("fclose_linux_amd64", "+++++++") - def test_fileio_linux_amd64(self) -> None: - """ - Tests that the `fileio` example for amd64 linux doesn't crash. - """ - self._test_no_crash("fileio_linux_amd64", "+") - def test_ioctl_bogus(self) -> None: """ Tests that the `ioctl_bogus_linux_amd64` example for amd64 linux doesn't crash. diff --git a/tests/native/test_linux.py b/tests/native/test_linux.py index 9f9bd3df9..028cac39c 100644 --- a/tests/native/test_linux.py +++ b/tests/native/test_linux.py @@ -1,4 +1,5 @@ import errno +import logging import unittest from binascii import hexlify @@ -10,11 +11,11 @@ from manticore.native.cpu.abstractcpu import ConcretizeRegister from manticore.core.smtlib.solver import Z3Solver -from manticore.core.smtlib import BitVecVariable, issymbolic +from manticore.core.smtlib import BitVecVariable, issymbolic, ConstraintSet from manticore.native import Manticore from manticore.platforms import linux, linux_syscalls from manticore.utils.helpers import pickle_dumps -from manticore.platforms.linux import EnvironmentError +from manticore.platforms.linux import EnvironmentError, logger as linux_logger, SymbolicFile class LinuxTest(unittest.TestCase): @@ -56,6 +57,44 @@ def test_stack_init(self) -> None: for i, env in enumerate(envp): self.assertEqual(cpu.read_string(cpu.read_int(envp_ptr + i * 8)), env) + def test_symbolic_file_wildcard(self) -> None: + with tempfile.NamedTemporaryFile("w") as fp: + # Write mixed symbolic and concrete data to our file + fp.write("++concrete++") + fp.flush() + + # setup logger for our assertion + prev_log_level = linux_logger.getEffectiveLevel() + linux_logger.setLevel(logging.DEBUG) + + with self.assertLogs(linux_logger, logging.DEBUG) as cm: + _ = SymbolicFile(ConstraintSet(), fp.name) + dmsg = "Found 4 free symbolic values" + self.assertIn(dmsg, "\n".join(cm.output)) + + with self.assertLogs(linux_logger, logging.DEBUG) as cm: + _ = SymbolicFile(ConstraintSet(), fp.name, wildcard="+", max_size=4) + dmsg = "Found 4 free symbolic values" + self.assertIn(dmsg, "\n".join(cm.output)) + + with self.assertLogs(linux_logger, logging.DEBUG) as cm: + _ = SymbolicFile(ConstraintSet(), fp.name, wildcard="+", max_size=2) + dmsg = "Found 4 free symbolic values" + wmsg = "Found more wildcards in the file than free symbolic values allowed (4 > 2)" + self.assertIn(wmsg, "\n".join(cm.output)) + + with self.assertLogs(linux_logger, logging.DEBUG) as cm: + _ = SymbolicFile(ConstraintSet(), fp.name, wildcard="|") + dmsg = "Found 0 free symbolic values" + self.assertIn(dmsg, "\n".join(cm.output)) + + with self.assertRaises(AssertionError) as ex: + _ = SymbolicFile(ConstraintSet(), fp.name, wildcard="Æ") + emsg = "needs to be a single byte" + self.assertIn(emsg, repr(ex.exception)) + + linux_logger.setLevel(prev_log_level) + def test_load_maps(self) -> None: mappings = self.linux.current.memory.mappings() diff --git a/tests/other/test_smtlibv2.py b/tests/other/test_smtlibv2.py index 9ba50020b..d4bb1248f 100644 --- a/tests/other/test_smtlibv2.py +++ b/tests/other/test_smtlibv2.py @@ -16,7 +16,13 @@ replace, BitVecConstant, ) -from manticore.core.smtlib.solver import Z3Solver, YicesSolver, CVC4Solver, BoolectorSolver +from manticore.core.smtlib.solver import ( + Z3Solver, + YicesSolver, + CVC4Solver, + BoolectorSolver, + PortfolioSolver, +) from manticore.core.smtlib.expression import * from manticore.utils.helpers import pickle_dumps from manticore import config @@ -713,7 +719,7 @@ def testBool_nonzero(self): self.assertFalse(BoolConstant(value=False).__bool__()) def test_visitors(self): - solver = Z3Solver.instance() + solver = self.solver cs = ConstraintSet() arr = cs.new_array(name="MEM") a = cs.new_bitvec(32, name="VAR") @@ -866,7 +872,7 @@ def testBasicReplace(self): self.assertEqual(translate_to_smtlib(x), "(bvadd #x00000064 VAR2)") def testBasicMigration(self): - solver = Z3Solver.instance() + solver = self.solver cs1 = ConstraintSet() cs2 = ConstraintSet() var1 = cs1.new_bitvec(32, "var") @@ -888,7 +894,7 @@ def testBasicMigration(self): self.assertItemsEqual(solver.get_all_values(cs1, var1), [2]) # should only be [2] def test_SAR(self): - solver = Z3Solver.instance() + solver = self.solver A = 0xBADF00D for B in range(32): cs = ConstraintSet() @@ -904,7 +910,7 @@ def test_SAR(self): self.assertEqual(solver.get_value(cs, c), Operators.SAR(32, A, B)) def test_ConstraintsForking(self): - solver = Z3Solver.instance() + solver = self.solver import pickle cs = ConstraintSet() @@ -1006,7 +1012,7 @@ def test_ConstraintsForking(self): self.assertItemsEqual(solver.get_all_values(cs_down_left, y), range(0x00, 0x80)) def test_ORD(self): - solver = Z3Solver.instance() + solver = self.solver cs = ConstraintSet() a = cs.new_bitvec(8) cs.add(Operators.ORD(a) == Operators.ORD("Z")) @@ -1015,7 +1021,7 @@ def test_ORD(self): self.assertEqual(solver.get_value(cs, a), ord("Z")) def test_ORD_proper_extract(self): - solver = Z3Solver.instance() + solver = self.solver cs = ConstraintSet() a = cs.new_bitvec(32) cs.add(Operators.ORD(a) == Operators.ORD("\xff")) @@ -1024,7 +1030,7 @@ def test_ORD_proper_extract(self): self.assertEqual(solver.get_value(cs, a), ord("\xff")) def test_CHR(self): - solver = Z3Solver.instance() + solver = self.solver cs = ConstraintSet() a = cs.new_bitvec(8) cs.add(Operators.CHR(a) == Operators.CHR(0x41)) @@ -1033,7 +1039,7 @@ def test_CHR(self): self.assertEqual(solver.get_value(cs, a), 0x41) def test_CONCAT(self): - solver = Z3Solver.instance() + solver = self.solver cs = ConstraintSet() a = cs.new_bitvec(16) b = cs.new_bitvec(8) @@ -1047,7 +1053,7 @@ def test_CONCAT(self): self.assertEqual(solver.get_value(cs, a), Operators.CONCAT(a.size, 0x41, 0x42)) def test_ITEBV_1(self): - solver = Z3Solver.instance() + solver = self.solver cs = ConstraintSet() a = cs.new_bitvec(8) b = cs.new_bitvec(8) @@ -1061,7 +1067,7 @@ def test_ITEBV_1(self): self.assertEqual(solver.get_value(cs, a), 0x42) def test_ITEBV_2(self): - solver = Z3Solver.instance() + solver = self.solver cs = ConstraintSet() a = cs.new_bitvec(8) b = cs.new_bitvec(8) @@ -1075,7 +1081,7 @@ def test_ITEBV_2(self): self.assertEqual(solver.get_value(cs, a), 0x44) def test_ITE(self): - solver = Z3Solver.instance() + solver = self.solver cs = ConstraintSet() a = cs.new_bool() b = cs.new_bool() @@ -1089,7 +1095,7 @@ def test_ITE(self): self.assertEqual(solver.get_value(cs, a), False) def test_UREM(self): - solver = Z3Solver.instance() + solver = self.solver cs = ConstraintSet() a = cs.new_bitvec(8) b = cs.new_bitvec(8) @@ -1106,7 +1112,7 @@ def test_UREM(self): self.assertEqual(solver.get_value(cs, a), 0xF) def test_SREM(self): - solver = Z3Solver.instance() + solver = self.solver cs = ConstraintSet() a = cs.new_bitvec(8) b = cs.new_bitvec(8) @@ -1123,7 +1129,7 @@ def test_SREM(self): self.assertEqual(solver.get_value(cs, a), -3 & 0xFF) def test_UDIV(self): - solver = Z3Solver.instance() + solver = self.solver cs = ConstraintSet() a = cs.new_bitvec(8) b = cs.new_bitvec(8) @@ -1140,7 +1146,7 @@ def test_UDIV(self): self.assertEqual(solver.get_value(cs, a), 7) def test_SDIV(self): - solver = Z3Solver.instance() + solver = self.solver cs = ConstraintSet() a = cs.new_bitvec(8) b = cs.new_bitvec(8) @@ -1156,7 +1162,7 @@ def test_SDIV(self): self.assertEqual(solver.get_value(cs, a), -7 & 0xFF) def test_ULE(self): - solver = Z3Solver.instance() + solver = self.solver cs = ConstraintSet() a = cs.new_bitvec(8) b = cs.new_bitvec(8) @@ -1178,7 +1184,7 @@ def test_ULE(self): self.assertTrue(solver.must_be_true(cs, Operators.ULE(0x10, c))) def test_ULT(self): - solver = Z3Solver.instance() + solver = self.solver cs = ConstraintSet() a = cs.new_bitvec(8) b = cs.new_bitvec(8) @@ -1200,7 +1206,7 @@ def test_ULT(self): self.assertTrue(solver.must_be_true(cs, Operators.ULT(0x10, c))) def test_NOT(self): - solver = Z3Solver.instance() + solver = self.solver cs = ConstraintSet() a = cs.new_bitvec(8) b = cs.new_bitvec(8) @@ -1308,5 +1314,10 @@ def setUp(self): self.solver = BoolectorSolver.instance() +class ExpressionTestPortfolio(ExpressionTest): + def setUp(self): + self.solver = PortfolioSolver.instance() + + if __name__ == "__main__": unittest.main()