From 165bb4780e44abe7e93b148f66a6defe87f8fdb9 Mon Sep 17 00:00:00 2001 From: feliam Date: Thu, 21 May 2020 16:31:58 -0300 Subject: [PATCH 01/28] Rollback to support yices again --- manticore/core/smtlib/solver.py | 153 +++++++++++++++++----------- manticore/core/state.py | 4 +- manticore/core/workspace.py | 4 +- manticore/ethereum/manticore.py | 6 +- manticore/native/cpu/abstractcpu.py | 4 +- manticore/native/manticore.py | 4 +- manticore/native/memory.py | 10 +- manticore/native/models.py | 4 +- manticore/native/state_merging.py | 20 ++-- manticore/platforms/evm.py | 30 +++--- manticore/platforms/linux.py | 10 +- manticore/utils/emulate.py | 4 +- manticore/wasm/manticore.py | 6 +- manticore/wasm/structure.py | 4 +- 14 files changed, 148 insertions(+), 115 deletions(-) diff --git a/manticore/core/smtlib/solver.py b/manticore/core/smtlib/solver.py index 708e6dcee..5299e4f05 100644 --- a/manticore/core/smtlib/solver.py +++ b/manticore/core/smtlib/solver.py @@ -142,78 +142,26 @@ def minmax(self, constraints, x, iters=10000): Version = collections.namedtuple("Version", "major minor patch") - -class Z3Solver(Solver): - def __init__(self): +class SMTLIBSolver(Solver): + def __init__(self, command, init): """ - Build a Z3 solver instance. - This is implemented using an external z3 solver (via a subprocess). - See https://github.com/Z3Prover/z3 + Build a smtlib solver instance. + This is implemented using an external solver (via a subprocess). """ super().__init__() self._proc: Popen = None - self._command = ( - f"{consts.z3_bin} -t:{consts.timeout*1000} -memory:{consts.memory} -smt2 -in" - ) - - # Commands used to initialize z3 - 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)", - # 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. - "(set-option :tactic.solve_eqs.context_solve false)", - ] + self._command = command + # Commands used to initialize smtlib + self._init = init self._get_value_fmt = (RE_GET_EXPR_VALUE_FMT, 16) self.debug = False - # To cache what get-info returned; can be directly set when writing tests - self._received_version = None - self.version = self._solver_version() - self.support_maximize = False self.support_minimize = False self.support_reset = True - logger.debug("Z3 version: %s", self.version) - if self.version >= Version(4, 5, 0): - self.support_maximize = False - self.support_minimize = False - self.support_reset = False - elif self.version >= Version(4, 4, 1): - self.support_maximize = True - self.support_minimize = True - self.support_reset = False - else: - logger.debug(" Please install Z3 4.4.1 or newer to get optimization support") - - def _solver_version(self) -> Version: - """ - If we fail to parse the version, we assume z3's output has changed, meaning it's a newer - version than what's used now, and therefore ok. - - Anticipated version_cmd_output format: 'Z3 version 4.4.2' - 'Z3 version 4.4.5 - 64 bit - build hashcode $Z3GITHASH' - """ - self._reset() - if self._received_version is None: - self._send("(get-info :version)") - self._received_version = self._recv() - key, version = shlex.split(self._received_version[1:-1]) - try: - parsed_version = Version(*map(int, version.split(" ", 1)[0].split("."))) - except (ValueError, TypeError) as e: - logger.warning(f"Could not parse Z3 version: '{version}'. Assuming compatibility.") - parsed_version = Version(float("inf"), float("inf"), float("inf")) - return parsed_version def _start_proc(self): """Spawns z3 solver process""" @@ -304,7 +252,9 @@ def _send(self, cmd: str) -> None: :param cmd: a SMTLIBv2 command (ex. (check-sat)) """ - # logger.debug('>%s', cmd) + if self.debug: + logger.debug('>%s', cmd) + print (">", cmd) try: if self._proc.stdout: self._proc.stdout.flush() @@ -331,6 +281,11 @@ def _recv(self) -> str: raise SolverException(f"Error in smtlib: {bufl[0]}") buf = "".join(bufl).strip() + + if self.debug: + logger.debug('<%s', buf) + print ("<", buf) + if "(error" in bufl[0]: raise SolverException(f"Error in smtlib: {bufl[0]}") @@ -677,3 +632,81 @@ def get_value(self, constraints: ConstraintSet, *expressions): return values[0] else: return values + + +class Z3Solver(SMTLIBSolver): + 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 + """ + 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)", + # 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. + "(set-option :tactic.solve_eqs.context_solve false)", + ] + command = f"{consts.z3_bin} -t:{consts.timeout * 1000} -memory:{consts.memory} -smt2 -in" + super().__init__(command=command, + init=init,) + # To cache what get-info returned; can be directly set when writing tests + self._received_version = None + self.version = self._solver_version() + logger.debug("Z3 version: %s", self.version) + + if self.version >= Version(4, 5, 0): + self.support_maximize = False + self.support_minimize = False + self.support_reset = False + elif self.version >= Version(4, 4, 1): + self.support_maximize = True + self.support_minimize = True + self.support_reset = False + else: + logger.debug(" Please install Z3 4.4.1 or newer to get optimization support") + + def _solver_version(self) -> Version: + """ + If we fail to parse the version, we assume z3's output has changed, meaning it's a newer + version than what's used now, and therefore ok. + + Anticipated version_cmd_output format: 'Z3 version 4.4.2' + 'Z3 version 4.4.5 - 64 bit - build hashcode $Z3GITHASH' + """ + self._reset() + if self._received_version is None: + self._send("(get-info :version)") + self._received_version = self._recv() + key, version = shlex.split(self._received_version[1:-1]) + try: + parsed_version = Version(*map(int, version.split(" ", 1)[0].split("."))) + except (ValueError, TypeError) as e: + logger.warning(f"Could not parse Z3 version: '{version}'. Assuming compatibility.") + parsed_version = Version(float("inf"), float("inf"), float("inf")) + return parsed_version + +class YicesSolver(SMTLIBSolver): + def __init__(self): + init = [ + "(set-logic QF_AUFBV)", + ] + command = f"yices-smt2 --timeout={consts.timeout * 1000} --incremental" + super().__init__(command=command, + init=init,) + self.support_maximize = False + self.support_minimize = False + self.support_reset = False + self.debug=False + RE_GET_EXPR_VALUE_FMT_B = re.compile( + r"\(\((?P(.*))[ \n\s]*#b(?P([0-1]*))\)\)") + + self._get_value_fmt = (RE_GET_EXPR_VALUE_FMT_B, 2) + diff --git a/manticore/core/state.py b/manticore/core/state.py index d5a8927de..9ec198700 100644 --- a/manticore/core/state.py +++ b/manticore/core/state.py @@ -306,9 +306,9 @@ def concretize(self, symbolic, policy, maxcount=7): @property def _solver(self): - from .smtlib import Z3Solver + from .smtlib import YicesSolver - return Z3Solver.instance() # solver + return YicesSolver.instance() # solver def migrate_expression(self, expression): if not issymbolic(expression): diff --git a/manticore/core/workspace.py b/manticore/core/workspace.py index f77093e61..b6b2c3119 100644 --- a/manticore/core/workspace.py +++ b/manticore/core/workspace.py @@ -29,7 +29,7 @@ def __exit__(self, *excinfo): import threading from ..utils import config from ..utils.helpers import StateSerializer, PickleSerializer -from .smtlib.solver import Z3Solver +from .smtlib.solver import YicesSolver from .state import StateBase from ..exceptions import ManticoreError @@ -658,5 +658,5 @@ def save_constraints(testcase, state: StateBase): def save_input_symbols(testcase, state: StateBase): with testcase.open_stream("input") as f: for symbol in state.input_symbols: - buf = Z3Solver.instance().get_value(state.constraints, symbol) + buf = YicesSolver.instance().get_value(state.constraints, symbol) f.write(f"{symbol.name}: {buf!r}\n") diff --git a/manticore/ethereum/manticore.py b/manticore/ethereum/manticore.py index e5a2d9670..99968de27 100644 --- a/manticore/ethereum/manticore.py +++ b/manticore/ethereum/manticore.py @@ -25,7 +25,7 @@ Expression, issymbolic, simplify, - Z3Solver, + YicesSolver, ) from ..core.state import TerminateState, AbandonState from .account import EVMContract, EVMAccount, ABI @@ -585,7 +585,7 @@ def solidity_create_contract( # Balance could be symbolic, lets ask the solver # Option 1: balance can not be 0 and the function is marked as not payable - if not Z3Solver.instance().can_be_true(self.constraints, balance == 0): + if not YicesSolver.instance().can_be_true(self.constraints, balance == 0): # balance always != 0 if not md.constructor_abi["payable"]: raise EthereumError( @@ -596,7 +596,7 @@ def solidity_create_contract( for state in self.ready_states: world = state.platform - if not Z3Solver.instance().can_be_true( + if not YicesSolver.instance().can_be_true( self.constraints, Operators.UGE(world.get_balance(owner.address), balance), ): diff --git a/manticore/native/cpu/abstractcpu.py b/manticore/native/cpu/abstractcpu.py index 2a41e88dd..eb2be3c09 100644 --- a/manticore/native/cpu/abstractcpu.py +++ b/manticore/native/cpu/abstractcpu.py @@ -13,7 +13,7 @@ from ..memory import LazySMemory, Memory from ...core.smtlib import Operators, Constant, issymbolic from ...core.smtlib import visitors -from ...core.smtlib.solver import Z3Solver +from ...core.smtlib.solver import YicesSolver from ...utils.emulate import ConcreteUnicornEmulator from ...utils.event import Eventful from ...utils.fallback_emulator import UnicornEmulator @@ -908,7 +908,7 @@ def decode_instruction(self, pc: int): c = bytes([vals[0]]) except visitors.ArraySelectSimplifier.ExpressionNotSimple: c = struct.pack( - "B", Z3Solver.instance().get_value(self.memory.constraints, c) + "B", YicesSolver.instance().get_value(self.memory.constraints, c) ) elif isinstance(c, Constant): c = bytes([c.value]) diff --git a/manticore/native/manticore.py b/manticore/native/manticore.py index 5ec14e3b9..82b15eb6c 100644 --- a/manticore/native/manticore.py +++ b/manticore/native/manticore.py @@ -12,7 +12,7 @@ from .state import State from ..core.manticore import ManticoreBase from ..core.smtlib import ConstraintSet -from ..core.smtlib.solver import Z3Solver, issymbolic +from ..core.smtlib.solver import YicesSolver, issymbolic from ..exceptions import ManticoreError from ..utils import log, config @@ -190,7 +190,7 @@ def _assertions_callback(self, state, pc, instruction): # This will interpret the buffer specification written in INTEL ASM. # (It may dereference pointers) assertion = parse(program, state.cpu.read_int, state.cpu.read_register) - if not Z3Solver.instance().can_be_true(state.constraints, assertion): + if not YicesSolver.instance().can_be_true(state.constraints, assertion): logger.info(str(state.cpu)) logger.info( "Assertion %x -> {%s} does not hold. Aborting state.", state.cpu.pc, program diff --git a/manticore/native/memory.py b/manticore/native/memory.py index 3e5ecdc8b..6a0e6db3c 100644 --- a/manticore/native/memory.py +++ b/manticore/native/memory.py @@ -5,7 +5,7 @@ Operators, ConstraintSet, arithmetic_simplify, - Z3Solver, + YicesSolver, TooManySolutions, BitVec, BitVecConstant, @@ -1194,7 +1194,7 @@ def read(self, address, size, force=False): solutions = self._try_get_solutions(address, size, "r", force=force) assert len(solutions) > 0 except TooManySolutions as e: - solver = Z3Solver.instance() + solver = YicesSolver.instance() m, M = solver.minmax(self.constraints, address) logger.debug( f"Got TooManySolutions on a symbolic read. Range [{m:x}, {M:x}]. Not crashing!" @@ -1327,7 +1327,7 @@ def _try_get_solutions(self, address, size, access, max_solutions=0x1000, force= :rtype: list """ assert issymbolic(address) - solver = Z3Solver.instance() + solver = YicesSolver.instance() solutions = solver.get_all_values(self.constraints, address, maxcnt=max_solutions) crashing_condition = False @@ -1435,7 +1435,7 @@ def _deref_can_succeed(self, mapping, address, size): if not issymbolic(address): return address >= mapping.start and address + size < mapping.end else: - solver = Z3Solver.instance() + solver = YicesSolver.instance() constraint = Operators.AND(address >= mapping.start, address + size < mapping.end) return solver.can_be_true(self.constraints, constraint) @@ -1473,7 +1473,7 @@ def _map_deref_expr(self, map, address): return Operators.AND(Operators.UGE(address, map.start), Operators.ULT(address, map.end)) def _reachable_range(self, sym_address, size): - solver = Z3Solver.instance() + solver = YicesSolver.instance() addr_min, addr_max = solver.minmax(self.constraints, sym_address) return addr_min, addr_max + size - 1 diff --git a/manticore/native/models.py b/manticore/native/models.py index 4cbfa3951..71e7b225c 100644 --- a/manticore/native/models.py +++ b/manticore/native/models.py @@ -4,7 +4,7 @@ from .cpu.abstractcpu import ConcretizeArgument from ..core.smtlib import issymbolic -from ..core.smtlib.solver import Z3Solver +from ..core.smtlib.solver import YicesSolver from ..core.smtlib.operators import ITEBV, ZEXTEND VARIADIC_FUNC_ATTR = "_variadic" @@ -46,7 +46,7 @@ def _find_zero(cpu, constrs, ptr): byt = cpu.read_int(ptr + offset, 8) if issymbolic(byt): - if not Z3Solver.instance().can_be_true(constrs, byt != 0): + if not YicesSolver.instance().can_be_true(constrs, byt != 0): break else: if byt == 0: diff --git a/manticore/native/state_merging.py b/manticore/native/state_merging.py index 51836c764..0be56a7b4 100644 --- a/manticore/native/state_merging.py +++ b/manticore/native/state_merging.py @@ -1,4 +1,4 @@ -from ..core.smtlib import Z3Solver, ConstraintSet, Operators, issymbolic, BitVec +from ..core.smtlib import YicesSolver, ConstraintSet, Operators, issymbolic, BitVec def compare_sockets(cs, socket1, socket2): @@ -7,7 +7,7 @@ def compare_sockets(cs, socket1, socket2): It uses `compare_buffers` for checking buffer attributes for equality. It calls itself for comparing peer Socket objects. Returns True if the Socket objects are equal, false otherwise. - :param cs: ConstraintSet to be used for checking Socket.buffer for semantic equality using `Z3Solver.instance().must_be_true()` + :param cs: ConstraintSet to be used for checking Socket.buffer for semantic equality using `YicesSolver.instance().must_be_true()` :param socket1: one of two Socket objects to be compared for equality against socket2 :param socket2: one of two Socket objects to be compared for equality against socket1 :return: True, if the Socket objects are found to be equal, False otherwise @@ -23,8 +23,8 @@ def compare_sockets(cs, socket1, socket2): def compare_buffers(cs, buffer1, buffer2): """ - This method compares the two List objects for equality using the `Z3Solver.instance().must_be_true()` call. - :param cs: ConstraintSet to be used for checking buffer1 for semantic equality with buffer2 using `Z3Solver.instance().must_be_true()` + This method compares the two List objects for equality using the `YicesSolver.instance().must_be_true()` call. + :param cs: ConstraintSet to be used for checking buffer1 for semantic equality with buffer2 using `YicesSolver.instance().must_be_true()` :param buffer1: one of two List objects to be compared for equality against buffer2 :param buffer2: one of two List objects to be compared for equality against buffer1 :return: True, if the List objects are equal, False otherwise @@ -32,7 +32,7 @@ def compare_buffers(cs, buffer1, buffer2): if len(buffer1) != len(buffer2): return False for b1, b2 in zip(buffer1, buffer2): - if not Z3Solver.instance().must_be_true(cs, b1 == b2): + if not YicesSolver.instance().must_be_true(cs, b1 == b2): return False return True @@ -62,7 +62,7 @@ def compare_byte_vals(mem1, mem2, addr, merged_constraint): :param mem1: first of two memory objects we want to use for comparison :param mem2: second of two memory objects we want to use for comparison :param addr: address at which bytes values are to be compared - :param merged_constraint: ConstraintSet to be used when using the call to `Z3Solver.instance().must_be_true()` + :param merged_constraint: ConstraintSet to be used when using the call to `YicesSolver.instance().must_be_true()` :return: returns True if 1 byte values at address `addr` in `mem1` and `mem2` are semantically equal, False otherwise """ val1 = mem1.read(addr, 1) @@ -70,7 +70,7 @@ def compare_byte_vals(mem1, mem2, addr, merged_constraint): # since we only read a single byte value, these lists should only have one entry in them assert len(val1) == 1 and len(val2) == 1 cond_to_check = val1[0] == val2[0] - if not Z3Solver.instance().must_be_true(merged_constraint, cond_to_check): + if not YicesSolver.instance().must_be_true(merged_constraint, cond_to_check): return False else: return True @@ -85,7 +85,7 @@ def compare_mem(mem1, mem2, merged_constraint): type SMemory. :param mem1: one of two memory objects to be compared :param mem2: second of two memory objects to be compared - :param merged_constraint: ConstraintSet object that is to be used with `Z3Solver.instance().must_be_true()` calls to check the + :param merged_constraint: ConstraintSet object that is to be used with `YicesSolver.instance().must_be_true()` calls to check the memory objects for semantic equality :return: True, if the memory objects are equal, False otherwise """ @@ -180,7 +180,7 @@ def merge_cpu(cpu1, cpu2, state, exp1, merged_constraint): :param exp1: the expression that if satisfiable will cause the CPU registers to take corresponding values from `cpu1`, else they will take corresponding values from `cpu2` :param merged_constraint: ConstraintSet under which we would want inequality between CPU register values to be - satisfiable as checked using `Z3Solver.instance().must_be_true()` + satisfiable as checked using `YicesSolver.instance().must_be_true()` :return: List of registers that were merged """ merged_regs = [] @@ -190,7 +190,7 @@ def merge_cpu(cpu1, cpu2, state, exp1, merged_constraint): if isinstance(val1, BitVec) and isinstance(val2, BitVec): assert val1.size == val2.size if issymbolic(val1) or issymbolic(val2) or val1 != val2: - if Z3Solver.instance().must_be_true(merged_constraint, val1 != val2): + if YicesSolver.instance().must_be_true(merged_constraint, val1 != val2): merged_regs.append(reg) if cpu1.regfile.sizeof(reg) == 1: state.cpu.write_register(reg, Operators.ITE(exp1, val1, val2)) diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py index 34472aa34..c735a5e81 100644 --- a/manticore/platforms/evm.py +++ b/manticore/platforms/evm.py @@ -9,7 +9,7 @@ from typing import List, Set, Tuple, Union from ..platforms.platform import * from ..core.smtlib import ( - Z3Solver, + YicesSolver, BitVec, Array, ArrayProxy, @@ -991,7 +991,7 @@ def _consume(self, fee): reps, m = getattr(self, "_mgas", (0, None)) reps += 1 if m is None and reps > 10: - m = Z3Solver.instance().min(self.constraints, self._gas) + m = YicesSolver.instance().min(self.constraints, self._gas) self._mgas = reps, m if m is not None and fee < m: @@ -1012,7 +1012,7 @@ def _consume(self, fee): elif isinstance(constraint, bool): enough_gas_solutions = (constraint,) # (self._gas - fee >= 0,) else: - enough_gas_solutions = Z3Solver.instance().get_all_values( + enough_gas_solutions = YicesSolver.instance().get_all_values( self.constraints, constraint ) @@ -1042,7 +1042,7 @@ def _consume(self, fee): # Try not to OOG. If it may be enough gas we ignore the OOG case. # A constraint is added to assert the gas is enough and the OOG state is ignored. # explore only when there is enough gas if possible - if Z3Solver.instance().can_be_true(self.constraints, Operators.UGT(self.gas, fee)): + if YicesSolver.instance().can_be_true(self.constraints, Operators.UGT(self.gas, fee)): self.constraints.add(Operators.UGT(self.gas, fee)) else: logger.debug( @@ -1053,7 +1053,7 @@ def _consume(self, fee): # OOG soon. If it may NOT be enough gas we ignore the normal case. # A constraint is added to assert the gas is NOT enough and the other state is ignored. # explore only when there is enough gas if possible - if Z3Solver.instance().can_be_true(self.constraints, Operators.ULE(self.gas, fee)): + if YicesSolver.instance().can_be_true(self.constraints, Operators.ULE(self.gas, fee)): self.constraints.add(Operators.ULE(self.gas, fee)) raise NotEnoughGas() else: @@ -1187,7 +1187,7 @@ def _check_jmpdest(self): if isinstance(should_check_jumpdest, Constant): should_check_jumpdest = should_check_jumpdest.value elif issymbolic(should_check_jumpdest): - should_check_jumpdest_solutions = Z3Solver.instance().get_all_values( + should_check_jumpdest_solutions = YicesSolver.instance().get_all_values( self.constraints, should_check_jumpdest ) if len(should_check_jumpdest_solutions) != 1: @@ -1571,7 +1571,7 @@ def try_simplify_to_constant(self, data): concrete_data.append(simplified.value) else: # simplify by solving. probably means that we need to improve simplification - solutions = Z3Solver.instance().get_all_values( + solutions = YicesSolver.instance().get_all_values( self.constraints, simplified, 2, silent=True ) if len(solutions) != 1: @@ -1691,7 +1691,7 @@ def CALLDATACOPY(self, mem_offset, data_offset, size): if consts.oog == "complete": # gas reduced cond = Operators.ULT(self.gas, self._checkpoint_data[1]) - if not Z3Solver.instance().can_be_true(self.constraints, cond): + if not YicesSolver.instance().can_be_true(self.constraints, cond): raise NotEnoughGas() self.constraints.add(cond) @@ -1700,7 +1700,7 @@ def CALLDATACOPY(self, mem_offset, data_offset, size): max_size = size if issymbolic(max_size): - max_size = Z3Solver.instance().max(self.constraints, size) + max_size = YicesSolver.instance().max(self.constraints, size) if calldata_overflow is not None: cap = len(self.data) + calldata_overflow @@ -1748,7 +1748,7 @@ def CODECOPY(self, mem_offset, code_offset, size): self._consume(copyfee) if issymbolic(size): - max_size = Z3Solver.instance().max(self.constraints, size) + max_size = YicesSolver.instance().max(self.constraints, size) else: max_size = size @@ -2154,7 +2154,7 @@ def SELFDESTRUCT(self, recipient): # FIXME for on the known addresses if issymbolic(recipient): logger.info("Symbolic recipient on self destruct") - recipient = Z3Solver.instance().get_value(self.constraints, recipient) + recipient = YicesSolver.instance().get_value(self.constraints, recipient) if recipient not in self.world: self.world.create_account(address=recipient) @@ -2336,7 +2336,7 @@ def try_simplify_to_constant(self, data): concrete_data.append(simplified.value) else: # simplify by solving. probably means that we need to improve simplification - solutions = Z3Solver.instance().get_all_values( + solutions = YicesSolver.instance().get_all_values( self.constraints, simplified, 2, silent=True ) if len(solutions) != 1: @@ -2361,7 +2361,7 @@ def symbolic_function(self, func, data): return result[0] except Exception as e: logger.info("Error! %r", e) - data_c = Z3Solver.instance().get_value(self.constraints, data) + data_c = YicesSolver.instance().get_value(self.constraints, data) return int(sha3.keccak_256(data_c).hexdigest(), 16) @property @@ -3021,7 +3021,7 @@ def _process_pending_transaction(self): if not failed: src_balance = self.get_balance(caller) enough_balance = Operators.UGE(src_balance, value) - enough_balance_solutions = Z3Solver.instance().get_all_values( + enough_balance_solutions = YicesSolver.instance().get_all_values( self._constraints, enough_balance ) @@ -3112,7 +3112,7 @@ def dump(self, stream, state, mevm, message): # temp_cs.add(storage.get(index) != 0) temp_cs.add(storage.is_known(index)) # Query the solver to get all storage indexes with used slots - all_used_indexes = Z3Solver.instance().get_all_values(temp_cs, index) + all_used_indexes = YicesSolver.instance().get_all_values(temp_cs, index) if all_used_indexes: stream.write("Storage:\n") diff --git a/manticore/platforms/linux.py b/manticore/platforms/linux.py index c4f746d70..c97fe4147 100644 --- a/manticore/platforms/linux.py +++ b/manticore/platforms/linux.py @@ -27,7 +27,7 @@ from .linux_syscall_stubs import SyscallStubs from ..core.state import TerminateState from ..core.smtlib import ConstraintSet, Operators, Expression, issymbolic, ArrayProxy -from ..core.smtlib.solver import Z3Solver +from ..core.smtlib.solver import YicesSolver from ..exceptions import SolverError from ..native.cpu.abstractcpu import Cpu, Syscall, ConcretizeArgument, Interruption from ..native.cpu.cpufactory import CpuFactory @@ -2299,7 +2299,7 @@ def sys_writev(self, fd, iov, count): size = cpu.read_int(iov + i * sizeof_iovec + (sizeof_iovec // 2), ptrsize) if issymbolic(size): - size = Z3Solver.instance().get_value(self.constraints, size) + size = YicesSolver.instance().get_value(self.constraints, size) data = [Operators.CHR(cpu.read_int(buf + i, 8)) for i in range(size)] data = self._transform_write_data(data) @@ -3247,7 +3247,7 @@ def _transform_write_data(self, data: MixedSymbolicBuffer) -> bytes: for c in data: if issymbolic(c): bytes_concretized += 1 - c = bytes([Z3Solver.instance().get_value(self.constraints, c)]) + c = bytes([YicesSolver.instance().get_value(self.constraints, c)]) concrete_data += cast(bytes, c) if bytes_concretized > 0: @@ -3259,7 +3259,7 @@ def _transform_write_data(self, data: MixedSymbolicBuffer) -> bytes: def sys_exit_group(self, error_code): if issymbolic(error_code): - error_code = Z3Solver.instance().get_value(self.constraints, error_code) + error_code = YicesSolver.instance().get_value(self.constraints, error_code) return self._exit( f"Program finished with exit status: {ctypes.c_int32(error_code).value} (*)" ) @@ -3455,7 +3455,7 @@ def make_chr(c): try: for c in data: if issymbolic(c): - c = Z3Solver.instance().get_value(self.constraints, c) + c = YicesSolver.instance().get_value(self.constraints, c) fd.write(make_chr(c)) except SolverError: fd.write("{SolverError}") diff --git a/manticore/utils/emulate.py b/manticore/utils/emulate.py index ebaa95656..1f719fd99 100644 --- a/manticore/utils/emulate.py +++ b/manticore/utils/emulate.py @@ -10,7 +10,7 @@ from unicorn.arm_const import * from unicorn.x86_const import * -from ..core.smtlib import Operators, Z3Solver, issymbolic +from ..core.smtlib import Operators, YicesSolver, issymbolic from ..native.memory import MemoryException logger = logging.getLogger(__name__) @@ -351,7 +351,7 @@ def write_back_memory(self, where, expr, size): concrete_data = [] for c in data: if issymbolic(c): - c = chr(Z3Solver.instance().get_value(self._cpu.memory.constraints, c)) + c = chr(YicesSolver.instance().get_value(self._cpu.memory.constraints, c)) concrete_data.append(c) data = concrete_data else: diff --git a/manticore/wasm/manticore.py b/manticore/wasm/manticore.py index 5c3b7701e..08f87f9fa 100644 --- a/manticore/wasm/manticore.py +++ b/manticore/wasm/manticore.py @@ -5,7 +5,7 @@ from .state import State from ..core.manticore import ManticoreBase -from ..core.smtlib import ConstraintSet, issymbolic, Z3Solver +from ..core.smtlib import ConstraintSet, issymbolic, YicesSolver from .types import I32, I64, F32, F64 from .structure import FuncInst @@ -161,7 +161,7 @@ def collect_returns(self, n=1): inner.append( list( I32(a) # TODO - eventually we'll need to support floats as well. - for a in Z3Solver.instance().get_all_values(state.constraints, ret) + for a in YicesSolver.instance().get_all_values(state.constraints, ret) ) ) elif ret.size == 64: @@ -170,7 +170,7 @@ def collect_returns(self, n=1): I64( a ) # TODO - that'll probably require us to subclass bitvecs into IxxBV and FxxBV - for a in Z3Solver.instance().get_all_values(state.constraints, ret) + for a in YicesSolver.instance().get_all_values(state.constraints, ret) ) ) else: diff --git a/manticore/wasm/structure.py b/manticore/wasm/structure.py index 47c3515c2..4f070a940 100644 --- a/manticore/wasm/structure.py +++ b/manticore/wasm/structure.py @@ -65,9 +65,9 @@ SEC_UNK, ) -from ..core.smtlib.solver import Z3Solver +from ..core.smtlib.solver import YicesSolver -solver = Z3Solver.instance() +solver = YicesSolver.instance() logger = logging.getLogger(__name__) # logger.setLevel(logging.DEBUG) From c43036a8760e9dfda811f2b8a13c0df431884a7b Mon Sep 17 00:00:00 2001 From: feliam Date: Thu, 21 May 2020 16:35:17 -0300 Subject: [PATCH 02/28] CC --- manticore/core/smtlib/solver.py | 27 +++++++++++---------------- 1 file changed, 11 insertions(+), 16 deletions(-) diff --git a/manticore/core/smtlib/solver.py b/manticore/core/smtlib/solver.py index 5299e4f05..c0cf69d2b 100644 --- a/manticore/core/smtlib/solver.py +++ b/manticore/core/smtlib/solver.py @@ -142,6 +142,7 @@ def minmax(self, constraints, x, iters=10000): Version = collections.namedtuple("Version", "major minor patch") + class SMTLIBSolver(Solver): def __init__(self, command, init): """ @@ -162,7 +163,6 @@ def __init__(self, command, init): self.support_minimize = False self.support_reset = True - def _start_proc(self): """Spawns z3 solver process""" assert "_proc" not in dir(self) or self._proc is None @@ -253,8 +253,8 @@ def _send(self, cmd: str) -> None: :param cmd: a SMTLIBv2 command (ex. (check-sat)) """ if self.debug: - logger.debug('>%s', cmd) - print (">", cmd) + logger.debug(">%s", cmd) + print(">", cmd) try: if self._proc.stdout: self._proc.stdout.flush() @@ -283,8 +283,8 @@ def _recv(self) -> str: buf = "".join(bufl).strip() if self.debug: - logger.debug('<%s', buf) - print ("<", buf) + logger.debug("<%s", buf) + print("<", buf) if "(error" in bufl[0]: raise SolverException(f"Error in smtlib: {bufl[0]}") @@ -655,8 +655,7 @@ def __init__(self): "(set-option :tactic.solve_eqs.context_solve false)", ] command = f"{consts.z3_bin} -t:{consts.timeout * 1000} -memory:{consts.memory} -smt2 -in" - super().__init__(command=command, - init=init,) + super().__init__(command=command, init=init) # To cache what get-info returned; can be directly set when writing tests self._received_version = None self.version = self._solver_version() @@ -693,20 +692,16 @@ def _solver_version(self) -> Version: parsed_version = Version(float("inf"), float("inf"), float("inf")) return parsed_version + class YicesSolver(SMTLIBSolver): def __init__(self): - init = [ - "(set-logic QF_AUFBV)", - ] + init = ["(set-logic QF_AUFBV)"] command = f"yices-smt2 --timeout={consts.timeout * 1000} --incremental" - super().__init__(command=command, - init=init,) + super().__init__(command=command, init=init) self.support_maximize = False self.support_minimize = False self.support_reset = False - self.debug=False - RE_GET_EXPR_VALUE_FMT_B = re.compile( - r"\(\((?P(.*))[ \n\s]*#b(?P([0-1]*))\)\)") + self.debug = False + RE_GET_EXPR_VALUE_FMT_B = re.compile(r"\(\((?P(.*))[ \n\s]*#b(?P([0-1]*))\)\)") self._get_value_fmt = (RE_GET_EXPR_VALUE_FMT_B, 2) - From 9cb8ae35d1ebcd273cf67051fe5e95bc06eb8ac6 Mon Sep 17 00:00:00 2001 From: feliam Date: Thu, 21 May 2020 17:05:52 -0300 Subject: [PATCH 03/28] Test yices --- .github/workflows/ci.yml | 9 +++++++++ tests/other/test_smtlibv2.py | 5 ++++- 2 files changed, 13 insertions(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 44dd0f781..bd0825bba 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -49,6 +49,15 @@ jobs: env: TEST_TYPE: ${{ matrix.type }} run: | + # Install yikes like a cave man + #sudo wget https://yices.csl.sri.com/releases/2.6.2/yices-2.6.2-x86_64-pc-linux-gnu-static-gmp.tar.gz + #sudo tar -zxvf yices-2.6.2-x86_64-pc-linux-gnu-static-gmp.tar.gz + #cd yices-2.6.2 + #sudo ./install-yices + #cd .. + sudo add-apt-repository ppa:sri-csl/formal-methods + sudo apt-get update + sudo apt-get install yices2 # 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 diff --git a/tests/other/test_smtlibv2.py b/tests/other/test_smtlibv2.py index c9b230fdf..39781993e 100644 --- a/tests/other/test_smtlibv2.py +++ b/tests/other/test_smtlibv2.py @@ -12,7 +12,7 @@ constant_folder, replace, ) -from manticore.core.smtlib.solver import Z3Solver +from manticore.core.smtlib.solver import Z3Solver, YicesSolver from manticore.core.smtlib.expression import * from manticore.utils.helpers import pickle_dumps @@ -1001,6 +1001,9 @@ def test_API(self): for attr in attrs: self.assertTrue(hasattr(cls, attr), f"{cls.__name__} is missing attribute {attr}") +class ExpressionTestYices(ExpressionTest): + def setUp(self): + self.solver = YicesSolver.instance() if __name__ == "__main__": unittest.main() From 69337d05d76b68758e73f021475f96f7539379b1 Mon Sep 17 00:00:00 2001 From: feliam Date: Thu, 21 May 2020 19:02:39 -0300 Subject: [PATCH 04/28] Better get-value handling --- manticore/core/smtlib/solver.py | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/manticore/core/smtlib/solver.py b/manticore/core/smtlib/solver.py index c0cf69d2b..c535355f6 100644 --- a/manticore/core/smtlib/solver.py +++ b/manticore/core/smtlib/solver.py @@ -351,7 +351,11 @@ def _getvalue(self, expression): expression_str = translate_to_smtlib(c) self._send("(get-value (%s))" % expression_str) response = self._recv() - result.append(int("0x{:s}".format(response.split(expression_str)[1][3:-2]), 16)) + response.split(expression_str)[1].strip(")") + pattern, base = self._get_value_fmt + m = pattern.match(response) + expr, value = m.group("expr"), m.group("value") + result.append(int(value, base)) #int("0x{:s}".format(response.split(expression_str)[1][3:-2]), 16)) return bytes(result) else: self._send("(get-value (%s))" % expression.name) From b4c899df9b7a91fb460a0b332123f0097e371a96 Mon Sep 17 00:00:00 2001 From: feliam Date: Fri, 22 May 2020 20:04:54 -0300 Subject: [PATCH 05/28] Z3/CVC4/YICES --- .github/workflows/ci.yml | 10 +- manticore/core/smtlib/solver.py | 580 +++++++++++++++------------- manticore/core/state.py | 4 +- manticore/core/workspace.py | 4 +- manticore/ethereum/manticore.py | 6 +- manticore/native/cpu/abstractcpu.py | 4 +- manticore/native/manticore.py | 4 +- manticore/native/memory.py | 10 +- manticore/native/models.py | 4 +- manticore/native/state_merging.py | 20 +- manticore/platforms/evm.py | 30 +- manticore/platforms/linux.py | 10 +- manticore/utils/emulate.py | 4 +- manticore/wasm/manticore.py | 6 +- manticore/wasm/structure.py | 4 +- tests/other/test_smtlibv2.py | 59 ++- 16 files changed, 403 insertions(+), 356 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index bd0825bba..16203038a 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -49,12 +49,10 @@ jobs: env: TEST_TYPE: ${{ matrix.type }} run: | - # Install yikes like a cave man - #sudo wget https://yices.csl.sri.com/releases/2.6.2/yices-2.6.2-x86_64-pc-linux-gnu-static-gmp.tar.gz - #sudo tar -zxvf yices-2.6.2-x86_64-pc-linux-gnu-static-gmp.tar.gz - #cd yices-2.6.2 - #sudo ./install-yices - #cd .. + #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 diff --git a/manticore/core/smtlib/solver.py b/manticore/core/smtlib/solver.py index c535355f6..8c8ceb9ab 100644 --- a/manticore/core/smtlib/solver.py +++ b/manticore/core/smtlib/solver.py @@ -13,14 +13,16 @@ # Once you Solver.check() it the status is changed to sat or unsat (or unknown+exception) # You can create new symbols operate on them. The declarations will be sent to the smtlib process when needed. # You can add new constraints. A new constraint may change the state from {None, sat} to {sat, unsat, unknown} + import os import threading +from queue import Queue import collections import shlex import time from functools import lru_cache from typing import Dict, Tuple -from subprocess import PIPE, Popen +from subprocess import PIPE, Popen, check_output import re from . import operators as Operators from .constraints import * @@ -45,12 +47,13 @@ "optimize", default=True, description="Use smtlib command optimize to find min/max if available" ) +consts.add("solver", default="cvc4", description="Choose default smtlib2 solver (z3, yices, cvc4, race)") # Regular expressions used by the solver -RE_GET_EXPR_VALUE_FMT = re.compile(r"\(\((?P(.*))\ #x(?P([0-9a-fA-F]*))\)\)") -RE_OBJECTIVES_EXPR_VALUE = re.compile( - r"\(objectives.*\((?P.*) (?P\d*)\).*\).*", re.MULTILINE | re.DOTALL -) +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]*))\)\)") +RE_OBJECTIVES_EXPR_VALUE = re.compile(r"\(objectives.*\((?P.*) (?P\d*)\).*\).*", re.MULTILINE | re.DOTALL) RE_MIN_MAX_OBJECTIVE_EXPR_VALUE = re.compile(r"(?P.*?)\s+\|->\s+(?P.*)", re.DOTALL) @@ -70,7 +73,6 @@ class SolverException(SmtlibError): """ Solver exception """ - pass @@ -143,162 +145,151 @@ def minmax(self, constraints, x, iters=10000): Version = collections.namedtuple("Version", "major minor patch") -class SMTLIBSolver(Solver): - def __init__(self, command, init): - """ - Build a smtlib solver instance. - This is implemented using an external solver (via a subprocess). - """ - super().__init__() - self._proc: Popen = None +class SmtlibProc: + def __init__(self, command:str, debug:bool=False): + """ Single smtlib interactive process + :param command: the shell command to execute + :param debug: log all messaging + """ + self._proc = None self._command = command + self._debug = debug - # Commands used to initialize smtlib - self._init = init - self._get_value_fmt = (RE_GET_EXPR_VALUE_FMT, 16) - - self.debug = False - self.support_maximize = False - self.support_minimize = False - self.support_reset = True - - def _start_proc(self): - """Spawns z3 solver process""" - assert "_proc" not in dir(self) or self._proc is None - try: - self._proc = Popen( - shlex.split(self._command), - stdin=PIPE, - stdout=PIPE, - bufsize=0, - universal_newlines=True, - close_fds=True, - ) - except OSError as e: - print(e, "Probably too many cached expressions? visitors._cache...") - # Z3 was removed from the system in the middle of operation - raise Z3NotFoundError # TODO(mark) don't catch this exception in two places - - # run solver specific initializations - for cfg in self._init: - self._send(cfg) - - def _stop_proc(self): + def start(self): + """Spawns POpen solver process""" + if self._proc is not None: + return + self._proc = Popen( + shlex.split(self._command), + stdin=PIPE, + stdout=PIPE, + bufsize=0, + universal_newlines=True, + close_fds=True, + ) + + def stop(self): """ - Stops the z3 solver process by: - - sending an exit command to it, + Stops the solver process by: - sending a SIGKILL signal, - waiting till the process terminates (so we don't leave a zombie process) """ if self._proc is None: return + #if it did not finished already if self._proc.returncode is None: - try: - self._send("(exit)") - except (SolverError, IOError) as e: - # z3 was too fast to close - logger.debug(str(e)) - finally: - try: - self._proc.stdin.close() - except IOError as e: - logger.debug(str(e)) - try: - self._proc.stdout.close() - except IOError as e: - logger.debug(str(e)) - self._proc.kill() - # Wait for termination, to avoid zombies. - self._proc.wait() - + self._proc.stdin.close() + self._proc.stdout.close() + # Kill the process + self._proc.kill() + # Wait for termination, to avoid zombies. + self._proc.wait() self._proc: Popen = None - # marshaling/pickle - def __getstate__(self): - raise SolverException() - - def __setstate__(self, state): - raise SolverException() - - def __del__(self): - try: - if self._proc is not None: - self._stop_proc() - # self._proc.stdin.writelines(('(exit)\n',)) - # self._proc.wait() - except Exception as e: - logger.error(str(e)) - - def _reset(self, constraints: Optional[str] = None) -> None: - """Auxiliary method to reset the smtlib external solver to initial defaults""" - if self._proc is None: - self._start_proc() - else: - if self.support_reset: - self._send("(reset)") - - for cfg in self._init: - self._send(cfg) - else: - self._stop_proc() - self._start_proc() - if constraints is not None: - self._send(constraints) + def __readline_and_count(self) -> Tuple[str, int, int]: + buf = self._proc.stdout.readline() #No timeout enforced here + #lparen, rparen = buf.count("("), buf.count(")") + lparen, rparen = map(sum, zip( * ((c == '(', c == ')') for c in buf) )) + return buf, lparen, rparen - def _send(self, cmd: str) -> None: + def send(self, cmd: str) -> None: """ Send a string to the solver. :param cmd: a SMTLIBv2 command (ex. (check-sat)) """ - if self.debug: + if self._debug: logger.debug(">%s", cmd) print(">", cmd) - try: - if self._proc.stdout: - self._proc.stdout.flush() - else: - raise SolverError("Could not flush stdout: file descriptor is None") - if self._proc.stdin: - self._proc.stdin.write(f"{cmd}\n") - else: - raise SolverError("Could not write to stdin: file descriptor is None") - except IOError as e: - raise SolverError(str(e)) + self._proc.stdout.flush() + self._proc.stdin.write(f"{cmd}\n") + - def _recv(self) -> str: - """Reads the response from the solver""" + 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 - if "(error" in bufl[0]: - raise SolverException(f"Error in smtlib: {bufl[0]}") buf = "".join(bufl).strip() - if self.debug: + if self._debug: logger.debug("<%s", buf) print("<", buf) - if "(error" in bufl[0]: - raise SolverException(f"Error in smtlib: {bufl[0]}") - return buf - def __readline_and_count(self) -> Tuple[str, int, int]: - stdout = self._proc.stdout - if stdout is None: - raise SolverError("Could not read from stdout: file descriptor is None") - buf = stdout.readline() - if buf is None: - raise SolverError("Could not read from stdout") - return buf, buf.count("("), buf.count(")") + def _restart(self) -> None: + """Auxiliary to start or restart the external solver""" + self._stop() + self._start() + + def is_started(self): + return self._proc != None + + +class SMTLIBSolver(Solver): + def __init__(self, + command:str, + init:List[str]=None, + value_fmt:int=16, + support_reset:bool=False, + support_minmax:bool=False, + support_pushpop:bool=False, + debug:bool=False): + + """ + Build a smtlib solver instance. + This is implemented using an external solver (via a subprocess). + """ + super().__init__() + self._smtlib: SmtlibProc = SmtlibProc(command, debug) + + # Commands used to initialize smtlib + self._init = init + self._get_value_fmt = ({ 2: RE_GET_EXPR_VALUE_FMT_BIN, + 10: RE_GET_EXPR_VALUE_FMT_DEC, + 16: RE_GET_EXPR_VALUE_FMT_HEX}[value_fmt], + value_fmt) + + self._support_minmax = support_minmax + self._support_reset = support_reset + self._support_pushpop = support_pushpop + + if not self._support_pushpop: + self._push = self._pop = None + + if self._support_minmax and consts.optimize: + self.optimize = self._optimize_fancy + else: + self.optimize = self._optimize_generic + + self._smtlib.start() + # run solver specific initializations + for cfg in self._init: + self._smtlib.send(cfg) + + + 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() + + for cfg in self._init: + self._smtlib.send(cfg) + + if constraints is not None: + self._smtlib.send(constraints) + # UTILS: check-sat get-value def _is_sat(self) -> bool: @@ -307,10 +298,9 @@ def _is_sat(self) -> bool: :return: whether current state is satisfiable or not. """ - logger.debug("Solver.check() ") start = time.time() - self._send("(check-sat)") - status = self._recv() + self._smtlib.send("(check-sat)") + status = self._smtlib.recv() logger.debug("Check took %s seconds (%s)", time.time() - start, status) if status not in ("sat", "unsat", "unknown"): raise SolverError(status) @@ -318,23 +308,17 @@ def _is_sat(self) -> bool: if status == "unknown": logger.info("Found an unknown core, probably a solver timeout") status = "unsat" - if status == "unknown": raise SolverUnknown(status) - - is_sat = status == "sat" - if not is_sat: - check_memory_usage() - check_disk_usage() - return is_sat + return status == "sat" def _assert(self, expression: Bool): """Auxiliary method to send an assert""" - assert isinstance(expression, Bool) smtlib = translate_to_smtlib(expression) - self._send("(assert %s)" % smtlib) + self._smtlib.send(f"(assert {smtlib})") - def _getvalue(self, expression): + #Union[Variable, int, bool, bytes] + def _getvalue(self, expression) -> Union[int, bool, bytes]: """ Ask the solver for one possible assignment for given expression using current set of constraints. The current set of expressions must be sat. @@ -343,25 +327,21 @@ def _getvalue(self, expression): """ if not issymbolic(expression): return expression - assert isinstance(expression, Variable) if isinstance(expression, Array): result = bytearray() for c in expression: expression_str = translate_to_smtlib(c) - self._send("(get-value (%s))" % expression_str) - response = self._recv() - response.split(expression_str)[1].strip(")") + self._smtlib.send(f"(get-value ({expression_str}))") + response = self._recv().split(expression_str)[1].strip(")") pattern, base = self._get_value_fmt m = pattern.match(response) expr, value = m.group("expr"), m.group("value") - result.append(int(value, base)) #int("0x{:s}".format(response.split(expression_str)[1][3:-2]), 16)) + result.append(int(value, base)) return bytes(result) else: - self._send("(get-value (%s))" % expression.name) - ret = self._recv() - assert ret.startswith("((") and ret.endswith("))"), ret - + self._smtlib.send(f"(get-value ({expression.name}))") + ret = self._smtlib.recv() if isinstance(expression, Bool): return {"true": True, "false": False}[ret[2:-2].split(" ")[1]] elif isinstance(expression, BitVec): @@ -370,16 +350,16 @@ def _getvalue(self, expression): expr, value = m.group("expr"), m.group("value") return int(value, base) - raise NotImplementedError("_getvalue only implemented for Bool and BitVec") + raise NotImplementedError("_getvalue only implemented for Bool, BitVec and Array") # push pop def _push(self): """Pushes and save the current constraint store and state.""" - self._send("(push 1)") + self._smtlib.send("(push 1)") def _pop(self): """Recall the last pushed constraint store and state.""" - self._send("(pop 1)") + self._smtlib.send("(pop 1)") @lru_cache(maxsize=32) def can_be_true(self, constraints: ConstraintSet, expression: Union[bool, Bool] = True) -> bool: @@ -391,20 +371,91 @@ def can_be_true(self, constraints: ConstraintSet, expression: Union[bool, Bool] # if True check if constraints are feasible self._reset(constraints.to_string()) return self._is_sat() - assert isinstance(expression, Bool) with constraints as temp_cs: temp_cs.add(expression) - self._reset(temp_cs.to_string(related_to=expression)) - return self._is_sat() + return self.can_be_true(temp_cs) # get-all-values min max minmax + def _optimize_generic(self, constraints: ConstraintSet, x: BitVec, goal: str, max_iter=10000): + """ + Iteratively finds the maximum or minimum value for the operation + (Normally Operators.UGT or Operators.ULT) + + :param constraints: constraints to take into account + :param x: a symbol or expression + :param goal: goal to achieve, either 'maximize' or 'minimize' + :param max_iter: maximum number of iterations allowed + """ + # TODO: consider adding a mode to return best known value on timeout + assert goal in ("maximize", "minimize") + operation = {"maximize": Operators.UGE, "minimize": Operators.ULE}[goal] + + start = time.time() + with constraints as temp_cs: + X = temp_cs.new_bitvec(x.size) + temp_cs.add(X == x) + aux = temp_cs.new_bitvec(X.size, name="optimized_") + self._reset(temp_cs.to_string(related_to=X)) + + # Find one value and use it as currently known min/Max + if not self._is_sat(): + raise SolverException("UNSAT") + last_value = self._getvalue(X) + self._assert(operation(X, last_value)) + + # This uses a binary search to find a suitable range for aux + # Use known solution as min or max depending on the goal + if goal == "maximize": + m, M = last_value, (1 << x.size) - 1 + else: + m, M = 0, last_value + + # Iteratively divide the range + L = None + while L not in (M, m): + L = (m + M) // 2 + self._assert(operation(X, L)) + sat = self._is_sat() + + # depending on the goal move one of the extremes + if goal == "maximize" and sat or goal == "minimize" and not sat: + m = L + else: + M = L + + if time.time() - start > consts.timeout: + raise SolverError("Timeout") + + #reset to before the dichotomic search + self._reset(temp_cs.to_string(related_to=X)) + + # At this point we know aux is inside [m,M] + # Lets constrain it to that range + self._assert(Operators.UGE(X, m)) + self._assert(Operators.ULE(X, M)) + + # And now check all remaining possible extremes + last_value = None + i = 0 + while self._is_sat(): + last_value = self._getvalue(X) + self._assert(operation(X, last_value)) + self._assert(X != last_value) + i = i + 1 + if i > max_iter: + raise SolverError("Optimizing error, maximum number of iterations was reached") + if time.time() - start > consts.timeout: + raise SolverError("Timeout") + if last_value is not None: + return last_value + raise SolverError("Optimizing error, unsat or unknown core") + @lru_cache(maxsize=32) - def get_all_values(self, constraints, expression, maxcnt=None, silent=False): + def get_all_values(self, constraints:ConstraintSet, expression, maxcnt:bool=None, silent:bool=False): """Returns a list with all the possible values for the symbol x""" if not isinstance(expression, Expression): return [expression] - assert isinstance(constraints, ConstraintSet) assert isinstance(expression, Expression) expression = simplify(expression) if maxcnt is None: @@ -449,7 +500,7 @@ def get_all_values(self, constraints, expression, maxcnt=None, silent=False): raise SolverError("Timeout") return result - def optimize(self, constraints: ConstraintSet, x: BitVec, goal: str, max_iter=10000): + def _optimize_fancy(self, constraints: ConstraintSet, x: BitVec, goal: str, max_iter=10000): """ Iteratively finds the maximum or minimum value for the operation (Normally Operators.UGT or Operators.ULT) @@ -468,101 +519,42 @@ def optimize(self, constraints: ConstraintSet, x: BitVec, goal: str, max_iter=10 temp_cs.add(X == x) aux = temp_cs.new_bitvec(X.size, name="optimized_") self._reset(temp_cs.to_string(related_to=X)) - self._send(aux.declaration) + self._smtlib.send(aux.declaration) start = time.time() - if consts.optimize and getattr(self, f"support_{goal}", False): - self._push() - try: - self._assert(operation(X, aux)) - self._send("(%s %s)" % (goal, aux.name)) - self._send("(check-sat)") - _status = self._recv() - if _status not in ("sat", "unsat", "unknown"): - # Minimize (or Maximize) sometimes prints the objective before the status - # This will be a line like NAME |-> VALUE - maybe_sat = self._recv() - if maybe_sat == "sat": - match = RE_MIN_MAX_OBJECTIVE_EXPR_VALUE.match(_status) - if match: - expr, value = match.group("expr"), match.group("value") - assert expr == aux.name - return int(value) - else: - raise SolverError("Could not match MinMax objective value regex") - elif _status == "sat": - ret = self._recv() - if not (ret.startswith("(") and ret.endswith(")")): - raise SolverError("bad output on max, z3 may have been killed") - - match = RE_OBJECTIVES_EXPR_VALUE.match(ret) + try: + self._assert(operation(X, aux)) + self._smtlib.send("(%s %s)" % (goal, aux.name)) + self._smtlib.send("(check-sat)") + _status = self._smtlib.recv() + if _status not in ("sat", "unsat", "unknown"): + # Minimize (or Maximize) sometimes prints the objective before the status + # This will be a line like NAME |-> VALUE + maybe_sat = self._recv() + if maybe_sat == "sat": + match = RE_MIN_MAX_OBJECTIVE_EXPR_VALUE.match(_status) if match: expr, value = match.group("expr"), match.group("value") assert expr == aux.name return int(value) else: - raise SolverError("Could not match objective value regex") - finally: - self._pop() - self._reset(temp_cs.to_string()) - self._send(aux.declaration) - - operation = {"maximize": Operators.UGE, "minimize": Operators.ULE}[goal] - self._assert(aux == X) - - # Find one value and use it as currently known min/Max - if not self._is_sat(): - raise SolverException("UNSAT") - last_value = self._getvalue(aux) - self._assert(operation(aux, last_value)) - - # This uses a binary search to find a suitable range for aux - # Use known solution as min or max depending on the goal - if goal == "maximize": - m, M = last_value, (1 << x.size) - 1 - else: - m, M = 0, last_value - - # Iteratively divide the range - L = None - while L not in (M, m): - L = (m + M) // 2 - self._push() - try: - self._assert(operation(aux, L)) - sat = self._is_sat() - finally: - self._pop() - - # depending on the goal move one of the extremes - if goal == "maximize" and sat or goal == "minimize" and not sat: - m = L - else: - M = L - - if time.time() - start > consts.timeout: - raise SolverError("Timeout") - - # At this point we know aux is inside [m,M] - # Lets constrain it to that range - self._assert(Operators.UGE(aux, m)) - self._assert(Operators.ULE(aux, M)) + raise SolverError("Could not match MinMax objective value regex") + elif _status == "sat": + ret = self._smtlib.recv() + if not (ret.startswith("(") and ret.endswith(")")): + raise SolverError("bad output on max, z3 may have been killed") + + match = RE_OBJECTIVES_EXPR_VALUE.match(ret) + if match: + expr, value = match.group("expr"), match.group("value") + assert expr == aux.name + return int(value) + else: + raise SolverError("Could not match objective value regex") + finally: + self._reset(temp_cs.to_string()) + self._smtlib.send(aux.declaration) - # And now check all remaining possible extremes - last_value = None - i = 0 - while self._is_sat(): - last_value = self._getvalue(aux) - self._assert(operation(aux, last_value)) - self._assert(aux != last_value) - i = i + 1 - if i > max_iter: - raise SolverError("Optimizing error, maximum number of iterations was reached") - if time.time() - start > consts.timeout: - raise SolverError("Timeout") - if last_value is not None: - return last_value - raise SolverError("Optimizing error, unsat or unknown core") def get_value(self, constraints: ConstraintSet, *expressions): """ @@ -596,9 +588,8 @@ def get_value(self, constraints: ConstraintSet, *expressions): ) for i in range(expression.index_max): - self._send("(get-value (%s))" % var[i].name) - ret = self._recv() - assert ret.startswith("((") and ret.endswith("))") + self._smtlib.send("(get-value (%s))" % var[i].name) + ret = self._smtlib.recv() pattern, base = self._get_value_fmt m = pattern.match(ret) expr, value = m.group("expr"), m.group("value") @@ -617,8 +608,8 @@ def get_value(self, constraints: ConstraintSet, *expressions): "Solver could not find a value for expression under current constraint set" ) - self._send("(get-value (%s))" % var.name) - ret = self._recv() + self._smtlib.send("(get-value (%s))" % var.name) + ret = self._smtlib.recv() if not (ret.startswith("((") and ret.endswith("))")): raise SolverError("SMTLIB error parsing response: %s" % ret) @@ -659,22 +650,22 @@ def __init__(self): "(set-option :tactic.solve_eqs.context_solve false)", ] command = f"{consts.z3_bin} -t:{consts.timeout * 1000} -memory:{consts.memory} -smt2 -in" - super().__init__(command=command, init=init) + + support_minmax, support_reset = self.__autoconfig() + super().__init__(command=command, init=init, value_fmt=16, support_minmax=False, support_reset=True, support_pushpop=True, debug=False) + + def __autoconfig(self): # To cache what get-info returned; can be directly set when writing tests - self._received_version = None self.version = self._solver_version() - logger.debug("Z3 version: %s", self.version) - if self.version >= Version(4, 5, 0): - self.support_maximize = False - self.support_minimize = False - self.support_reset = False + support_minmax = False + support_reset = False elif self.version >= Version(4, 4, 1): - self.support_maximize = True - self.support_minimize = True - self.support_reset = False + support_minmax = True + support_reset = False else: logger.debug(" Please install Z3 4.4.1 or newer to get optimization support") + return support_minmax, support_reset def _solver_version(self) -> Version: """ @@ -684,15 +675,15 @@ def _solver_version(self) -> Version: Anticipated version_cmd_output format: 'Z3 version 4.4.2' 'Z3 version 4.4.5 - 64 bit - build hashcode $Z3GITHASH' """ - self._reset() - if self._received_version is None: - self._send("(get-info :version)") - self._received_version = self._recv() - key, version = shlex.split(self._received_version[1:-1]) try: - parsed_version = Version(*map(int, version.split(" ", 1)[0].split("."))) + received_version = check_output([f"{consts.z3_bin}", "--version"]) + Z3VERSION = re.compile( + r".*(?P([0-9]+))\.(?P([0-9]+))\.(?P([0-9]+)).*") + m = Z3VERSION.match(received_version.decode('utf-8')) + major, minor, patch = map(int, (m.group("major"), m.group("minor"), m.group("patch"))) + parsed_version = Version(major, minor, patch) except (ValueError, TypeError) as e: - logger.warning(f"Could not parse Z3 version: '{version}'. Assuming compatibility.") + logger.warning(f"Could not parse Z3 version: '{received_version}'. Assuming compatibility.") parsed_version = Version(float("inf"), float("inf"), float("inf")) return parsed_version @@ -701,11 +692,52 @@ class YicesSolver(SMTLIBSolver): def __init__(self): init = ["(set-logic QF_AUFBV)"] command = f"yices-smt2 --timeout={consts.timeout * 1000} --incremental" - super().__init__(command=command, init=init) - self.support_maximize = False - self.support_minimize = False - self.support_reset = False - self.debug = False - RE_GET_EXPR_VALUE_FMT_B = re.compile(r"\(\((?P(.*))[ \n\s]*#b(?P([0-1]*))\)\)") - - self._get_value_fmt = (RE_GET_EXPR_VALUE_FMT_B, 2) + super().__init__(command=command, + init=init, + value_fmt=2, + debug=False, + support_minmax=False, + support_reset=False) + + +class CVC4Solver(SMTLIBSolver): + def __init__(self): + init = ["(set-logic QF_AUFBV)", '(set-option :produce-models true)'] + command = f"cvc4 --lang=smt2 --incremental" + super().__init__(command=command, value_fmt=10, init=init) + +class ddRaceSolver(SMTLIBSolver): + def __init__(self, *solvers): + if not solvers: + solvers = (Z3Solver, YicesSolver, CVC4Solver) + self._solvers = solvers + + def _race(self, function_name, *args, **kwargs): + q = Queue() + solver_instances = [ x() for x in self._solvers ] + def thread(solver): + try: + x = getattr(solver, function_name)(*args, **kwargs) + q.put(x) + except Exception as e: + print (e) + pass + + threads = [ threading.Thread(target=thread, args=(x,)) for x in solver_instances ] + for t in threads: + t.start() + result = q.get(block=True, timeout=consts.timeout) + for instance in solver_instances: + try: + instance._proc.kill() + except: + pass # already died + for t in threads: + t.join() + return result + + +SelectedSolver = {'cvc4':CVC4Solver, + 'yices':YicesSolver, + 'z3': Z3Solver, + }[consts.solver] diff --git a/manticore/core/state.py b/manticore/core/state.py index 9ec198700..45f6dc307 100644 --- a/manticore/core/state.py +++ b/manticore/core/state.py @@ -306,9 +306,9 @@ def concretize(self, symbolic, policy, maxcount=7): @property def _solver(self): - from .smtlib import YicesSolver + from .smtlib import SelectedSolver - return YicesSolver.instance() # solver + return SelectedSolver.instance() # solver def migrate_expression(self, expression): if not issymbolic(expression): diff --git a/manticore/core/workspace.py b/manticore/core/workspace.py index b6b2c3119..6041ba1ef 100644 --- a/manticore/core/workspace.py +++ b/manticore/core/workspace.py @@ -29,7 +29,7 @@ def __exit__(self, *excinfo): import threading from ..utils import config from ..utils.helpers import StateSerializer, PickleSerializer -from .smtlib.solver import YicesSolver +from .smtlib.solver import SelectedSolver from .state import StateBase from ..exceptions import ManticoreError @@ -658,5 +658,5 @@ def save_constraints(testcase, state: StateBase): def save_input_symbols(testcase, state: StateBase): with testcase.open_stream("input") as f: for symbol in state.input_symbols: - buf = YicesSolver.instance().get_value(state.constraints, symbol) + buf = SelectedSolver.instance().get_value(state.constraints, symbol) f.write(f"{symbol.name}: {buf!r}\n") diff --git a/manticore/ethereum/manticore.py b/manticore/ethereum/manticore.py index 99968de27..84e557293 100644 --- a/manticore/ethereum/manticore.py +++ b/manticore/ethereum/manticore.py @@ -25,7 +25,7 @@ Expression, issymbolic, simplify, - YicesSolver, + SelectedSolver, ) from ..core.state import TerminateState, AbandonState from .account import EVMContract, EVMAccount, ABI @@ -585,7 +585,7 @@ def solidity_create_contract( # Balance could be symbolic, lets ask the solver # Option 1: balance can not be 0 and the function is marked as not payable - if not YicesSolver.instance().can_be_true(self.constraints, balance == 0): + if not SelectedSolver.instance().can_be_true(self.constraints, balance == 0): # balance always != 0 if not md.constructor_abi["payable"]: raise EthereumError( @@ -596,7 +596,7 @@ def solidity_create_contract( for state in self.ready_states: world = state.platform - if not YicesSolver.instance().can_be_true( + if not SelectedSolver.instance().can_be_true( self.constraints, Operators.UGE(world.get_balance(owner.address), balance), ): diff --git a/manticore/native/cpu/abstractcpu.py b/manticore/native/cpu/abstractcpu.py index eb2be3c09..57489de5c 100644 --- a/manticore/native/cpu/abstractcpu.py +++ b/manticore/native/cpu/abstractcpu.py @@ -13,7 +13,7 @@ from ..memory import LazySMemory, Memory from ...core.smtlib import Operators, Constant, issymbolic from ...core.smtlib import visitors -from ...core.smtlib.solver import YicesSolver +from ...core.smtlib.solver import SelectedSolver from ...utils.emulate import ConcreteUnicornEmulator from ...utils.event import Eventful from ...utils.fallback_emulator import UnicornEmulator @@ -908,7 +908,7 @@ def decode_instruction(self, pc: int): c = bytes([vals[0]]) except visitors.ArraySelectSimplifier.ExpressionNotSimple: c = struct.pack( - "B", YicesSolver.instance().get_value(self.memory.constraints, c) + "B", SelectedSolver.instance().get_value(self.memory.constraints, c) ) elif isinstance(c, Constant): c = bytes([c.value]) diff --git a/manticore/native/manticore.py b/manticore/native/manticore.py index 82b15eb6c..95827b706 100644 --- a/manticore/native/manticore.py +++ b/manticore/native/manticore.py @@ -12,7 +12,7 @@ from .state import State from ..core.manticore import ManticoreBase from ..core.smtlib import ConstraintSet -from ..core.smtlib.solver import YicesSolver, issymbolic +from ..core.smtlib.solver import SelectedSolver, issymbolic from ..exceptions import ManticoreError from ..utils import log, config @@ -190,7 +190,7 @@ def _assertions_callback(self, state, pc, instruction): # This will interpret the buffer specification written in INTEL ASM. # (It may dereference pointers) assertion = parse(program, state.cpu.read_int, state.cpu.read_register) - if not YicesSolver.instance().can_be_true(state.constraints, assertion): + if not SelectedSolver.instance().can_be_true(state.constraints, assertion): logger.info(str(state.cpu)) logger.info( "Assertion %x -> {%s} does not hold. Aborting state.", state.cpu.pc, program diff --git a/manticore/native/memory.py b/manticore/native/memory.py index 6a0e6db3c..70025a0fc 100644 --- a/manticore/native/memory.py +++ b/manticore/native/memory.py @@ -5,7 +5,7 @@ Operators, ConstraintSet, arithmetic_simplify, - YicesSolver, + SelectedSolver, TooManySolutions, BitVec, BitVecConstant, @@ -1194,7 +1194,7 @@ def read(self, address, size, force=False): solutions = self._try_get_solutions(address, size, "r", force=force) assert len(solutions) > 0 except TooManySolutions as e: - solver = YicesSolver.instance() + solver = SelectedSolver.instance() m, M = solver.minmax(self.constraints, address) logger.debug( f"Got TooManySolutions on a symbolic read. Range [{m:x}, {M:x}]. Not crashing!" @@ -1327,7 +1327,7 @@ def _try_get_solutions(self, address, size, access, max_solutions=0x1000, force= :rtype: list """ assert issymbolic(address) - solver = YicesSolver.instance() + solver = SelectedSolver.instance() solutions = solver.get_all_values(self.constraints, address, maxcnt=max_solutions) crashing_condition = False @@ -1435,7 +1435,7 @@ def _deref_can_succeed(self, mapping, address, size): if not issymbolic(address): return address >= mapping.start and address + size < mapping.end else: - solver = YicesSolver.instance() + solver = SelectedSolver.instance() constraint = Operators.AND(address >= mapping.start, address + size < mapping.end) return solver.can_be_true(self.constraints, constraint) @@ -1473,7 +1473,7 @@ def _map_deref_expr(self, map, address): return Operators.AND(Operators.UGE(address, map.start), Operators.ULT(address, map.end)) def _reachable_range(self, sym_address, size): - solver = YicesSolver.instance() + solver = SelectedSolver.instance() addr_min, addr_max = solver.minmax(self.constraints, sym_address) return addr_min, addr_max + size - 1 diff --git a/manticore/native/models.py b/manticore/native/models.py index 71e7b225c..8930ddaff 100644 --- a/manticore/native/models.py +++ b/manticore/native/models.py @@ -4,7 +4,7 @@ from .cpu.abstractcpu import ConcretizeArgument from ..core.smtlib import issymbolic -from ..core.smtlib.solver import YicesSolver +from ..core.smtlib.solver import SelectedSolver from ..core.smtlib.operators import ITEBV, ZEXTEND VARIADIC_FUNC_ATTR = "_variadic" @@ -46,7 +46,7 @@ def _find_zero(cpu, constrs, ptr): byt = cpu.read_int(ptr + offset, 8) if issymbolic(byt): - if not YicesSolver.instance().can_be_true(constrs, byt != 0): + if not SelectedSolver.instance().can_be_true(constrs, byt != 0): break else: if byt == 0: diff --git a/manticore/native/state_merging.py b/manticore/native/state_merging.py index 0be56a7b4..2ff9f2e64 100644 --- a/manticore/native/state_merging.py +++ b/manticore/native/state_merging.py @@ -1,4 +1,4 @@ -from ..core.smtlib import YicesSolver, ConstraintSet, Operators, issymbolic, BitVec +from ..core.smtlib import SelectedSolver, ConstraintSet, Operators, issymbolic, BitVec def compare_sockets(cs, socket1, socket2): @@ -7,7 +7,7 @@ def compare_sockets(cs, socket1, socket2): It uses `compare_buffers` for checking buffer attributes for equality. It calls itself for comparing peer Socket objects. Returns True if the Socket objects are equal, false otherwise. - :param cs: ConstraintSet to be used for checking Socket.buffer for semantic equality using `YicesSolver.instance().must_be_true()` + :param cs: ConstraintSet to be used for checking Socket.buffer for semantic equality using `SelectedSolver.instance().must_be_true()` :param socket1: one of two Socket objects to be compared for equality against socket2 :param socket2: one of two Socket objects to be compared for equality against socket1 :return: True, if the Socket objects are found to be equal, False otherwise @@ -23,8 +23,8 @@ def compare_sockets(cs, socket1, socket2): def compare_buffers(cs, buffer1, buffer2): """ - This method compares the two List objects for equality using the `YicesSolver.instance().must_be_true()` call. - :param cs: ConstraintSet to be used for checking buffer1 for semantic equality with buffer2 using `YicesSolver.instance().must_be_true()` + This method compares the two List objects for equality using the `SelectedSolver.instance().must_be_true()` call. + :param cs: ConstraintSet to be used for checking buffer1 for semantic equality with buffer2 using `SelectedSolver.instance().must_be_true()` :param buffer1: one of two List objects to be compared for equality against buffer2 :param buffer2: one of two List objects to be compared for equality against buffer1 :return: True, if the List objects are equal, False otherwise @@ -32,7 +32,7 @@ def compare_buffers(cs, buffer1, buffer2): if len(buffer1) != len(buffer2): return False for b1, b2 in zip(buffer1, buffer2): - if not YicesSolver.instance().must_be_true(cs, b1 == b2): + if not SelectedSolver.instance().must_be_true(cs, b1 == b2): return False return True @@ -62,7 +62,7 @@ def compare_byte_vals(mem1, mem2, addr, merged_constraint): :param mem1: first of two memory objects we want to use for comparison :param mem2: second of two memory objects we want to use for comparison :param addr: address at which bytes values are to be compared - :param merged_constraint: ConstraintSet to be used when using the call to `YicesSolver.instance().must_be_true()` + :param merged_constraint: ConstraintSet to be used when using the call to `SelectedSolver.instance().must_be_true()` :return: returns True if 1 byte values at address `addr` in `mem1` and `mem2` are semantically equal, False otherwise """ val1 = mem1.read(addr, 1) @@ -70,7 +70,7 @@ def compare_byte_vals(mem1, mem2, addr, merged_constraint): # since we only read a single byte value, these lists should only have one entry in them assert len(val1) == 1 and len(val2) == 1 cond_to_check = val1[0] == val2[0] - if not YicesSolver.instance().must_be_true(merged_constraint, cond_to_check): + if not SelectedSolver.instance().must_be_true(merged_constraint, cond_to_check): return False else: return True @@ -85,7 +85,7 @@ def compare_mem(mem1, mem2, merged_constraint): type SMemory. :param mem1: one of two memory objects to be compared :param mem2: second of two memory objects to be compared - :param merged_constraint: ConstraintSet object that is to be used with `YicesSolver.instance().must_be_true()` calls to check the + :param merged_constraint: ConstraintSet object that is to be used with `SelectedSolver.instance().must_be_true()` calls to check the memory objects for semantic equality :return: True, if the memory objects are equal, False otherwise """ @@ -180,7 +180,7 @@ def merge_cpu(cpu1, cpu2, state, exp1, merged_constraint): :param exp1: the expression that if satisfiable will cause the CPU registers to take corresponding values from `cpu1`, else they will take corresponding values from `cpu2` :param merged_constraint: ConstraintSet under which we would want inequality between CPU register values to be - satisfiable as checked using `YicesSolver.instance().must_be_true()` + satisfiable as checked using `SelectedSolver.instance().must_be_true()` :return: List of registers that were merged """ merged_regs = [] @@ -190,7 +190,7 @@ def merge_cpu(cpu1, cpu2, state, exp1, merged_constraint): if isinstance(val1, BitVec) and isinstance(val2, BitVec): assert val1.size == val2.size if issymbolic(val1) or issymbolic(val2) or val1 != val2: - if YicesSolver.instance().must_be_true(merged_constraint, val1 != val2): + if SelectedSolver.instance().must_be_true(merged_constraint, val1 != val2): merged_regs.append(reg) if cpu1.regfile.sizeof(reg) == 1: state.cpu.write_register(reg, Operators.ITE(exp1, val1, val2)) diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py index c735a5e81..501e095b8 100644 --- a/manticore/platforms/evm.py +++ b/manticore/platforms/evm.py @@ -9,7 +9,7 @@ from typing import List, Set, Tuple, Union from ..platforms.platform import * from ..core.smtlib import ( - YicesSolver, + SelectedSolver, BitVec, Array, ArrayProxy, @@ -991,7 +991,7 @@ def _consume(self, fee): reps, m = getattr(self, "_mgas", (0, None)) reps += 1 if m is None and reps > 10: - m = YicesSolver.instance().min(self.constraints, self._gas) + m = SelectedSolver.instance().min(self.constraints, self._gas) self._mgas = reps, m if m is not None and fee < m: @@ -1012,7 +1012,7 @@ def _consume(self, fee): elif isinstance(constraint, bool): enough_gas_solutions = (constraint,) # (self._gas - fee >= 0,) else: - enough_gas_solutions = YicesSolver.instance().get_all_values( + enough_gas_solutions = SelectedSolver.instance().get_all_values( self.constraints, constraint ) @@ -1042,7 +1042,7 @@ def _consume(self, fee): # Try not to OOG. If it may be enough gas we ignore the OOG case. # A constraint is added to assert the gas is enough and the OOG state is ignored. # explore only when there is enough gas if possible - if YicesSolver.instance().can_be_true(self.constraints, Operators.UGT(self.gas, fee)): + if SelectedSolver.instance().can_be_true(self.constraints, Operators.UGT(self.gas, fee)): self.constraints.add(Operators.UGT(self.gas, fee)) else: logger.debug( @@ -1053,7 +1053,7 @@ def _consume(self, fee): # OOG soon. If it may NOT be enough gas we ignore the normal case. # A constraint is added to assert the gas is NOT enough and the other state is ignored. # explore only when there is enough gas if possible - if YicesSolver.instance().can_be_true(self.constraints, Operators.ULE(self.gas, fee)): + if SelectedSolver.instance().can_be_true(self.constraints, Operators.ULE(self.gas, fee)): self.constraints.add(Operators.ULE(self.gas, fee)) raise NotEnoughGas() else: @@ -1187,7 +1187,7 @@ def _check_jmpdest(self): if isinstance(should_check_jumpdest, Constant): should_check_jumpdest = should_check_jumpdest.value elif issymbolic(should_check_jumpdest): - should_check_jumpdest_solutions = YicesSolver.instance().get_all_values( + should_check_jumpdest_solutions = SelectedSolver.instance().get_all_values( self.constraints, should_check_jumpdest ) if len(should_check_jumpdest_solutions) != 1: @@ -1571,7 +1571,7 @@ def try_simplify_to_constant(self, data): concrete_data.append(simplified.value) else: # simplify by solving. probably means that we need to improve simplification - solutions = YicesSolver.instance().get_all_values( + solutions = SelectedSolver.instance().get_all_values( self.constraints, simplified, 2, silent=True ) if len(solutions) != 1: @@ -1691,7 +1691,7 @@ def CALLDATACOPY(self, mem_offset, data_offset, size): if consts.oog == "complete": # gas reduced cond = Operators.ULT(self.gas, self._checkpoint_data[1]) - if not YicesSolver.instance().can_be_true(self.constraints, cond): + if not SelectedSolver.instance().can_be_true(self.constraints, cond): raise NotEnoughGas() self.constraints.add(cond) @@ -1700,7 +1700,7 @@ def CALLDATACOPY(self, mem_offset, data_offset, size): max_size = size if issymbolic(max_size): - max_size = YicesSolver.instance().max(self.constraints, size) + max_size = SelectedSolver.instance().max(self.constraints, size) if calldata_overflow is not None: cap = len(self.data) + calldata_overflow @@ -1748,7 +1748,7 @@ def CODECOPY(self, mem_offset, code_offset, size): self._consume(copyfee) if issymbolic(size): - max_size = YicesSolver.instance().max(self.constraints, size) + max_size = SelectedSolver.instance().max(self.constraints, size) else: max_size = size @@ -2154,7 +2154,7 @@ def SELFDESTRUCT(self, recipient): # FIXME for on the known addresses if issymbolic(recipient): logger.info("Symbolic recipient on self destruct") - recipient = YicesSolver.instance().get_value(self.constraints, recipient) + recipient = SelectedSolver.instance().get_value(self.constraints, recipient) if recipient not in self.world: self.world.create_account(address=recipient) @@ -2336,7 +2336,7 @@ def try_simplify_to_constant(self, data): concrete_data.append(simplified.value) else: # simplify by solving. probably means that we need to improve simplification - solutions = YicesSolver.instance().get_all_values( + solutions = SelectedSolver.instance().get_all_values( self.constraints, simplified, 2, silent=True ) if len(solutions) != 1: @@ -2361,7 +2361,7 @@ def symbolic_function(self, func, data): return result[0] except Exception as e: logger.info("Error! %r", e) - data_c = YicesSolver.instance().get_value(self.constraints, data) + data_c = SelectedSolver.instance().get_value(self.constraints, data) return int(sha3.keccak_256(data_c).hexdigest(), 16) @property @@ -3021,7 +3021,7 @@ def _process_pending_transaction(self): if not failed: src_balance = self.get_balance(caller) enough_balance = Operators.UGE(src_balance, value) - enough_balance_solutions = YicesSolver.instance().get_all_values( + enough_balance_solutions = SelectedSolver.instance().get_all_values( self._constraints, enough_balance ) @@ -3112,7 +3112,7 @@ def dump(self, stream, state, mevm, message): # temp_cs.add(storage.get(index) != 0) temp_cs.add(storage.is_known(index)) # Query the solver to get all storage indexes with used slots - all_used_indexes = YicesSolver.instance().get_all_values(temp_cs, index) + all_used_indexes = SelectedSolver.instance().get_all_values(temp_cs, index) if all_used_indexes: stream.write("Storage:\n") diff --git a/manticore/platforms/linux.py b/manticore/platforms/linux.py index c97fe4147..bc2e88f01 100644 --- a/manticore/platforms/linux.py +++ b/manticore/platforms/linux.py @@ -27,7 +27,7 @@ from .linux_syscall_stubs import SyscallStubs from ..core.state import TerminateState from ..core.smtlib import ConstraintSet, Operators, Expression, issymbolic, ArrayProxy -from ..core.smtlib.solver import YicesSolver +from ..core.smtlib.solver import SelectedSolver from ..exceptions import SolverError from ..native.cpu.abstractcpu import Cpu, Syscall, ConcretizeArgument, Interruption from ..native.cpu.cpufactory import CpuFactory @@ -2299,7 +2299,7 @@ def sys_writev(self, fd, iov, count): size = cpu.read_int(iov + i * sizeof_iovec + (sizeof_iovec // 2), ptrsize) if issymbolic(size): - size = YicesSolver.instance().get_value(self.constraints, size) + size = SelectedSolver.instance().get_value(self.constraints, size) data = [Operators.CHR(cpu.read_int(buf + i, 8)) for i in range(size)] data = self._transform_write_data(data) @@ -3247,7 +3247,7 @@ def _transform_write_data(self, data: MixedSymbolicBuffer) -> bytes: for c in data: if issymbolic(c): bytes_concretized += 1 - c = bytes([YicesSolver.instance().get_value(self.constraints, c)]) + c = bytes([SelectedSolver.instance().get_value(self.constraints, c)]) concrete_data += cast(bytes, c) if bytes_concretized > 0: @@ -3259,7 +3259,7 @@ def _transform_write_data(self, data: MixedSymbolicBuffer) -> bytes: def sys_exit_group(self, error_code): if issymbolic(error_code): - error_code = YicesSolver.instance().get_value(self.constraints, error_code) + error_code = SelectedSolver.instance().get_value(self.constraints, error_code) return self._exit( f"Program finished with exit status: {ctypes.c_int32(error_code).value} (*)" ) @@ -3455,7 +3455,7 @@ def make_chr(c): try: for c in data: if issymbolic(c): - c = YicesSolver.instance().get_value(self.constraints, c) + c = SelectedSolver.instance().get_value(self.constraints, c) fd.write(make_chr(c)) except SolverError: fd.write("{SolverError}") diff --git a/manticore/utils/emulate.py b/manticore/utils/emulate.py index 1f719fd99..1c677bef1 100644 --- a/manticore/utils/emulate.py +++ b/manticore/utils/emulate.py @@ -10,7 +10,7 @@ from unicorn.arm_const import * from unicorn.x86_const import * -from ..core.smtlib import Operators, YicesSolver, issymbolic +from ..core.smtlib import Operators, SelectedSolver, issymbolic from ..native.memory import MemoryException logger = logging.getLogger(__name__) @@ -351,7 +351,7 @@ def write_back_memory(self, where, expr, size): concrete_data = [] for c in data: if issymbolic(c): - c = chr(YicesSolver.instance().get_value(self._cpu.memory.constraints, c)) + c = chr(SelectedSolver.instance().get_value(self._cpu.memory.constraints, c)) concrete_data.append(c) data = concrete_data else: diff --git a/manticore/wasm/manticore.py b/manticore/wasm/manticore.py index 08f87f9fa..287223325 100644 --- a/manticore/wasm/manticore.py +++ b/manticore/wasm/manticore.py @@ -5,7 +5,7 @@ from .state import State from ..core.manticore import ManticoreBase -from ..core.smtlib import ConstraintSet, issymbolic, YicesSolver +from ..core.smtlib import ConstraintSet, issymbolic, SelectedSolver from .types import I32, I64, F32, F64 from .structure import FuncInst @@ -161,7 +161,7 @@ def collect_returns(self, n=1): inner.append( list( I32(a) # TODO - eventually we'll need to support floats as well. - for a in YicesSolver.instance().get_all_values(state.constraints, ret) + for a in SelectedSolver.instance().get_all_values(state.constraints, ret) ) ) elif ret.size == 64: @@ -170,7 +170,7 @@ def collect_returns(self, n=1): I64( a ) # TODO - that'll probably require us to subclass bitvecs into IxxBV and FxxBV - for a in YicesSolver.instance().get_all_values(state.constraints, ret) + for a in SelectedSolver.instance().get_all_values(state.constraints, ret) ) ) else: diff --git a/manticore/wasm/structure.py b/manticore/wasm/structure.py index 4f070a940..6be764c7b 100644 --- a/manticore/wasm/structure.py +++ b/manticore/wasm/structure.py @@ -65,9 +65,9 @@ SEC_UNK, ) -from ..core.smtlib.solver import YicesSolver +from ..core.smtlib.solver import SelectedSolver -solver = YicesSolver.instance() +solver = SelectedSolver.instance() logger = logging.getLogger(__name__) # logger.setLevel(logging.DEBUG) diff --git a/tests/other/test_smtlibv2.py b/tests/other/test_smtlibv2.py index 39781993e..9943aec94 100644 --- a/tests/other/test_smtlibv2.py +++ b/tests/other/test_smtlibv2.py @@ -12,7 +12,7 @@ constant_folder, replace, ) -from manticore.core.smtlib.solver import Z3Solver, YicesSolver +from manticore.core.smtlib.solver import Z3Solver, YicesSolver, CVC4Solver from manticore.core.smtlib.expression import * from manticore.utils.helpers import pickle_dumps @@ -21,6 +21,34 @@ # level = logging.DEBUG) +class Z3Specific(unittest.TestCase): + _multiprocess_can_split_ = True + + def setUp(self): + self.solver = Z3Solver.instance() + + + def test_check_solver_min(self): + self.solver._received_version = '(:version "4.4.1")' + self.assertTrue(self.solver._solver_version() == Version(major=4, minor=4, patch=1)) + + def test_check_solver_newer(self): + self.solver._received_version = '(:version "4.5.0")' + self.assertTrue(self.solver._solver_version() > Version(major=4, minor=4, patch=1)) + + def test_check_solver_long_format(self): + self.solver._received_version = '(:version "4.8.6 - build hashcode 78ed71b8de7d")' + self.assertTrue(self.solver._solver_version() == Version(major=4, minor=8, patch=6)) + + def test_check_solver_undefined(self): + self.solver._received_version = '(:version "78ed71b8de7d")' + self.assertTrue( + self.solver._solver_version() + == Version(major=float("inf"), minor=float("inf"), patch=float("inf")) + ) + self.assertTrue(self.solver._solver_version() > Version(major=4, minor=4, patch=1)) + + class ExpressionTest(unittest.TestCase): _multiprocess_can_split_ = True @@ -959,26 +987,6 @@ def test_NOT(self): self.assertTrue(solver.must_be_true(cs, Operators.NOT(False))) self.assertTrue(solver.must_be_true(cs, Operators.NOT(a == b))) - def test_check_solver_min(self): - self.solver._received_version = '(:version "4.4.1")' - self.assertTrue(self.solver._solver_version() == Version(major=4, minor=4, patch=1)) - - def test_check_solver_newer(self): - self.solver._received_version = '(:version "4.5.0")' - self.assertTrue(self.solver._solver_version() > Version(major=4, minor=4, patch=1)) - - def test_check_solver_long_format(self): - self.solver._received_version = '(:version "4.8.6 - build hashcode 78ed71b8de7d")' - self.assertTrue(self.solver._solver_version() == Version(major=4, minor=8, patch=6)) - - def test_check_solver_undefined(self): - self.solver._received_version = '(:version "78ed71b8de7d")' - self.assertTrue( - self.solver._solver_version() - == Version(major=float("inf"), minor=float("inf"), patch=float("inf")) - ) - self.assertTrue(self.solver._solver_version() > Version(major=4, minor=4, patch=1)) - def test_API(self): """ As we've split up the Constant, Variable, and Operation classes to avoid using multiple inheritance, @@ -1005,5 +1013,14 @@ class ExpressionTestYices(ExpressionTest): def setUp(self): self.solver = YicesSolver.instance() +class ExpressionTestCVC4(ExpressionTest): + def setUp(self): + self.solver = CVC4Solver.instance() + + +class ExpressionTestRace(ExpressionTest): + def setUp(self): + self.solver = RaceSolver.instance() + if __name__ == "__main__": unittest.main() From 09b0374a6c9414eafde646a6a5e9cde5e19cd871 Mon Sep 17 00:00:00 2001 From: feliam Date: Fri, 22 May 2020 22:03:37 -0300 Subject: [PATCH 06/28] CC --- manticore/core/smtlib/solver.py | 113 +++++++++++++++++++------------- 1 file changed, 67 insertions(+), 46 deletions(-) diff --git a/manticore/core/smtlib/solver.py b/manticore/core/smtlib/solver.py index 8c8ceb9ab..c03eeb89c 100644 --- a/manticore/core/smtlib/solver.py +++ b/manticore/core/smtlib/solver.py @@ -47,13 +47,17 @@ "optimize", default=True, description="Use smtlib command optimize to find min/max if available" ) -consts.add("solver", default="cvc4", description="Choose default smtlib2 solver (z3, yices, cvc4, race)") +consts.add( + "solver", default="cvc4", description="Choose default smtlib2 solver (z3, yices, cvc4, race)" +) # Regular expressions used by the solver 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_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]*))\)\)") -RE_OBJECTIVES_EXPR_VALUE = re.compile(r"\(objectives.*\((?P.*) (?P\d*)\).*\).*", re.MULTILINE | re.DOTALL) +RE_OBJECTIVES_EXPR_VALUE = re.compile( + r"\(objectives.*\((?P.*) (?P\d*)\).*\).*", re.MULTILINE | re.DOTALL +) RE_MIN_MAX_OBJECTIVE_EXPR_VALUE = re.compile(r"(?P.*?)\s+\|->\s+(?P.*)", re.DOTALL) @@ -73,6 +77,7 @@ class SolverException(SmtlibError): """ Solver exception """ + pass @@ -146,7 +151,7 @@ def minmax(self, constraints, x, iters=10000): class SmtlibProc: - def __init__(self, command:str, debug:bool=False): + def __init__(self, command: str, debug: bool = False): """ Single smtlib interactive process :param command: the shell command to execute @@ -177,7 +182,7 @@ def stop(self): """ if self._proc is None: return - #if it did not finished already + # if it did not finished already if self._proc.returncode is None: self._proc.stdin.close() self._proc.stdout.close() @@ -188,9 +193,9 @@ def stop(self): self._proc: Popen = None def __readline_and_count(self) -> Tuple[str, int, int]: - buf = self._proc.stdout.readline() #No timeout enforced here - #lparen, rparen = buf.count("("), buf.count(")") - lparen, rparen = map(sum, zip( * ((c == '(', c == ')') for c in buf) )) + buf = self._proc.stdout.readline() # No timeout enforced here + # lparen, rparen = buf.count("("), buf.count(")") + lparen, rparen = map(sum, zip(*((c == "(", c == ")") for c in buf))) return buf, lparen, rparen def send(self, cmd: str) -> None: @@ -205,7 +210,6 @@ def send(self, cmd: str) -> None: self._proc.stdout.flush() self._proc.stdin.write(f"{cmd}\n") - def recv(self) -> str: """Reads the response from the smtlib solver""" buf, left, right = self.__readline_and_count() @@ -234,14 +238,16 @@ def is_started(self): class SMTLIBSolver(Solver): - def __init__(self, - command:str, - init:List[str]=None, - value_fmt:int=16, - support_reset:bool=False, - support_minmax:bool=False, - support_pushpop:bool=False, - debug:bool=False): + def __init__( + self, + command: str, + init: List[str] = None, + value_fmt: int = 16, + support_reset: bool = False, + support_minmax: bool = False, + support_pushpop: bool = False, + debug: bool = False, + ): """ Build a smtlib solver instance. @@ -252,10 +258,14 @@ def __init__(self, # Commands used to initialize smtlib self._init = init - self._get_value_fmt = ({ 2: RE_GET_EXPR_VALUE_FMT_BIN, - 10: RE_GET_EXPR_VALUE_FMT_DEC, - 16: RE_GET_EXPR_VALUE_FMT_HEX}[value_fmt], - value_fmt) + self._get_value_fmt = ( + { + 2: RE_GET_EXPR_VALUE_FMT_BIN, + 10: RE_GET_EXPR_VALUE_FMT_DEC, + 16: RE_GET_EXPR_VALUE_FMT_HEX, + }[value_fmt], + value_fmt, + ) self._support_minmax = support_minmax self._support_reset = support_reset @@ -274,7 +284,6 @@ def __init__(self, for cfg in self._init: self._smtlib.send(cfg) - def _reset(self, constraints: Optional[str] = None) -> None: """Auxiliary method to reset the smtlib external solver to initial defaults""" if self._support_reset: @@ -290,7 +299,6 @@ def _reset(self, constraints: Optional[str] = None) -> None: if constraints is not None: self._smtlib.send(constraints) - # UTILS: check-sat get-value def _is_sat(self) -> bool: """ @@ -317,7 +325,7 @@ def _assert(self, expression: Bool): smtlib = translate_to_smtlib(expression) self._smtlib.send(f"(assert {smtlib})") - #Union[Variable, int, bool, bytes] + # Union[Variable, int, bool, bytes] def _getvalue(self, expression) -> Union[int, bool, bytes]: """ Ask the solver for one possible assignment for given expression using current set of constraints. @@ -427,7 +435,7 @@ def _optimize_generic(self, constraints: ConstraintSet, x: BitVec, goal: str, ma if time.time() - start > consts.timeout: raise SolverError("Timeout") - #reset to before the dichotomic search + # reset to before the dichotomic search self._reset(temp_cs.to_string(related_to=X)) # At this point we know aux is inside [m,M] @@ -452,7 +460,9 @@ def _optimize_generic(self, constraints: ConstraintSet, x: BitVec, goal: str, ma raise SolverError("Optimizing error, unsat or unknown core") @lru_cache(maxsize=32) - def get_all_values(self, constraints:ConstraintSet, expression, maxcnt:bool=None, silent:bool=False): + def get_all_values( + self, constraints: ConstraintSet, expression, maxcnt: bool = None, silent: bool = False + ): """Returns a list with all the possible values for the symbol x""" if not isinstance(expression, Expression): return [expression] @@ -555,7 +565,6 @@ def _optimize_fancy(self, constraints: ConstraintSet, x: BitVec, goal: str, max_ self._reset(temp_cs.to_string()) self._smtlib.send(aux.declaration) - def get_value(self, constraints: ConstraintSet, *expressions): """ Ask the solver for one possible result of given expressions using @@ -652,7 +661,15 @@ def __init__(self): command = f"{consts.z3_bin} -t:{consts.timeout * 1000} -memory:{consts.memory} -smt2 -in" support_minmax, support_reset = self.__autoconfig() - super().__init__(command=command, init=init, value_fmt=16, support_minmax=False, support_reset=True, support_pushpop=True, debug=False) + super().__init__( + command=command, + init=init, + value_fmt=16, + support_minmax=False, + support_reset=True, + support_pushpop=True, + debug=False, + ) def __autoconfig(self): # To cache what get-info returned; can be directly set when writing tests @@ -678,12 +695,15 @@ def _solver_version(self) -> Version: try: received_version = check_output([f"{consts.z3_bin}", "--version"]) Z3VERSION = re.compile( - r".*(?P([0-9]+))\.(?P([0-9]+))\.(?P([0-9]+)).*") - m = Z3VERSION.match(received_version.decode('utf-8')) + r".*(?P([0-9]+))\.(?P([0-9]+))\.(?P([0-9]+)).*" + ) + m = Z3VERSION.match(received_version.decode("utf-8")) major, minor, patch = map(int, (m.group("major"), m.group("minor"), m.group("patch"))) parsed_version = Version(major, minor, patch) except (ValueError, TypeError) as e: - logger.warning(f"Could not parse Z3 version: '{received_version}'. Assuming compatibility.") + logger.warning( + f"Could not parse Z3 version: '{received_version}'. Assuming compatibility." + ) parsed_version = Version(float("inf"), float("inf"), float("inf")) return parsed_version @@ -692,20 +712,23 @@ class YicesSolver(SMTLIBSolver): def __init__(self): init = ["(set-logic QF_AUFBV)"] command = f"yices-smt2 --timeout={consts.timeout * 1000} --incremental" - super().__init__(command=command, - init=init, - value_fmt=2, - debug=False, - support_minmax=False, - support_reset=False) + super().__init__( + command=command, + init=init, + value_fmt=2, + debug=False, + support_minmax=False, + support_reset=False, + ) class CVC4Solver(SMTLIBSolver): def __init__(self): - init = ["(set-logic QF_AUFBV)", '(set-option :produce-models true)'] + init = ["(set-logic QF_AUFBV)", "(set-option :produce-models true)"] command = f"cvc4 --lang=smt2 --incremental" super().__init__(command=command, value_fmt=10, init=init) + class ddRaceSolver(SMTLIBSolver): def __init__(self, *solvers): if not solvers: @@ -714,16 +737,17 @@ def __init__(self, *solvers): def _race(self, function_name, *args, **kwargs): q = Queue() - solver_instances = [ x() for x in self._solvers ] + solver_instances = [x() for x in self._solvers] + def thread(solver): try: x = getattr(solver, function_name)(*args, **kwargs) q.put(x) except Exception as e: - print (e) + print(e) pass - threads = [ threading.Thread(target=thread, args=(x,)) for x in solver_instances ] + threads = [threading.Thread(target=thread, args=(x,)) for x in solver_instances] for t in threads: t.start() result = q.get(block=True, timeout=consts.timeout) @@ -731,13 +755,10 @@ def thread(solver): try: instance._proc.kill() except: - pass # already died + pass # already died for t in threads: t.join() return result -SelectedSolver = {'cvc4':CVC4Solver, - 'yices':YicesSolver, - 'z3': Z3Solver, - }[consts.solver] +SelectedSolver = {"cvc4": CVC4Solver, "yices": YicesSolver, "z3": Z3Solver}[consts.solver] From 0649f853bd23de392300457041e5caf8098934f5 Mon Sep 17 00:00:00 2001 From: feliam Date: Tue, 26 May 2020 11:48:07 -0300 Subject: [PATCH 07/28] Yices/CVC4 --- manticore/core/smtlib/expression.py | 4 ++ manticore/core/smtlib/solver.py | 103 ++++++++++++++++------------ tests/other/test_smtlibv2.py | 21 ++++-- 3 files changed, 76 insertions(+), 52 deletions(-) diff --git a/manticore/core/smtlib/expression.py b/manticore/core/smtlib/expression.py index d300d85e5..534f77c83 100644 --- a/manticore/core/smtlib/expression.py +++ b/manticore/core/smtlib/expression.py @@ -770,6 +770,10 @@ def __getitem__(self, index): raise IndexError return self.select(self.cast_index(index)) + def __iter__(self): + for i in range(len(self)): + yield self[i] + def __eq__(self, other): # FIXME taint def compare_buffers(a, b): diff --git a/manticore/core/smtlib/solver.py b/manticore/core/smtlib/solver.py index c03eeb89c..0b4a25aff 100644 --- a/manticore/core/smtlib/solver.py +++ b/manticore/core/smtlib/solver.py @@ -21,7 +21,7 @@ import shlex import time from functools import lru_cache -from typing import Dict, Tuple +from typing import Dict, Tuple, Sequence from subprocess import PIPE, Popen, check_output import re from . import operators as Operators @@ -157,7 +157,7 @@ def __init__(self, command: str, debug: bool = False): :param command: the shell command to execute :param debug: log all messaging """ - self._proc = None + self._proc: Optional[Popen] = None self._command = command self._debug = debug @@ -190,9 +190,11 @@ def stop(self): self._proc.kill() # Wait for termination, to avoid zombies. self._proc.wait() - self._proc: Popen = None + self._proc = None - def __readline_and_count(self) -> Tuple[str, int, int]: + def __readline_and_count(self): + assert self._proc + assert self._proc.stdout buf = self._proc.stdout.readline() # No timeout enforced here # lparen, rparen = buf.count("("), buf.count(")") lparen, rparen = map(sum, zip(*((c == "(", c == ")") for c in buf))) @@ -204,6 +206,9 @@ def send(self, cmd: str) -> None: :param cmd: a SMTLIBv2 command (ex. (check-sat)) """ + assert self._proc + assert self._proc.stdout + assert self._proc.stdin if self._debug: logger.debug(">%s", cmd) print(">", cmd) @@ -230,8 +235,8 @@ def recv(self) -> str: def _restart(self) -> None: """Auxiliary to start or restart the external solver""" - self._stop() - self._start() + self.stop() + self.start() def is_started(self): return self._proc != None @@ -241,7 +246,7 @@ class SMTLIBSolver(Solver): def __init__( self, command: str, - init: List[str] = None, + init: Sequence[str] = None, value_fmt: int = 16, support_reset: bool = False, support_minmax: bool = False, @@ -257,6 +262,8 @@ def __init__( self._smtlib: SmtlibProc = SmtlibProc(command, debug) # Commands used to initialize smtlib + if init is None: + init = tuple() self._init = init self._get_value_fmt = ( { @@ -272,12 +279,13 @@ def __init__( self._support_pushpop = support_pushpop if not self._support_pushpop: - self._push = self._pop = None + setattr(self, "_push", None) + setattr(self, "_pop", None) if self._support_minmax and consts.optimize: - self.optimize = self._optimize_fancy + setattr(self, "optimize", self._optimize_fancy) else: - self.optimize = self._optimize_generic + setattr(self, "optimize", self._optimize_generic) self._smtlib.start() # run solver specific initializations @@ -326,6 +334,18 @@ def _assert(self, expression: Bool): self._smtlib.send(f"(assert {smtlib})") # Union[Variable, int, bool, bytes] + def __getvalue_bv(self, expression_str): + self._smtlib.send(f"(get-value ({expression_str}))") + pattern, base = self._get_value_fmt + m = pattern.match(self._smtlib.recv()) + expr, value = m.group("expr"), m.group("value") + return int(value, base) + + def __getvalue_bool(self, expression_str): + self._smtlib.send(f"(get-value ({expression_str}))") + ret = self._smtlib.recv() + return {"true": True, "false": False}[ret[2:-2].split(" ")[1]] + def _getvalue(self, expression) -> Union[int, bool, bytes]: """ Ask the solver for one possible assignment for given expression using current set of constraints. @@ -340,23 +360,19 @@ def _getvalue(self, expression) -> Union[int, bool, bytes]: result = bytearray() for c in expression: expression_str = translate_to_smtlib(c) - self._smtlib.send(f"(get-value ({expression_str}))") - response = self._recv().split(expression_str)[1].strip(")") - pattern, base = self._get_value_fmt - m = pattern.match(response) - expr, value = m.group("expr"), m.group("value") - result.append(int(value, base)) + # self._smtlib.send(f"(get-value ({expression_str}))") + # response = self._smtlib.recv().split(expression_str)[1].strip(")") + # pattern, base = self._get_value_fmt + # m = pattern.match(response) + # expr, value = m.group("expr"), m.group("value") + # result.append(int(value, base)) + result.append(self.__getvalue_bv(expression_str)) return bytes(result) else: - self._smtlib.send(f"(get-value ({expression.name}))") - ret = self._smtlib.recv() - if isinstance(expression, Bool): - return {"true": True, "false": False}[ret[2:-2].split(" ")[1]] - elif isinstance(expression, BitVec): - pattern, base = self._get_value_fmt - m = pattern.match(ret) - expr, value = m.group("expr"), m.group("value") - return int(value, base) + if isinstance(expression, BoolVariable): + return self.__getvalue_bool(expression.name) + elif isinstance(expression, BitVecVariable): + return self.__getvalue_bv(expression.name) raise NotImplementedError("_getvalue only implemented for Bool, BitVec and Array") @@ -399,6 +415,8 @@ def _optimize_generic(self, constraints: ConstraintSet, x: BitVec, goal: str, ma assert goal in ("maximize", "minimize") operation = {"maximize": Operators.UGE, "minimize": Operators.ULE}[goal] + last_value: Optional[Union[int, bool, bytes]] = None + start = time.time() with constraints as temp_cs: X = temp_cs.new_bitvec(x.size) @@ -540,7 +558,7 @@ def _optimize_fancy(self, constraints: ConstraintSet, x: BitVec, goal: str, max_ if _status not in ("sat", "unsat", "unknown"): # Minimize (or Maximize) sometimes prints the objective before the status # This will be a line like NAME |-> VALUE - maybe_sat = self._recv() + maybe_sat = self._smtlib.recv() if maybe_sat == "sat": match = RE_MIN_MAX_OBJECTIVE_EXPR_VALUE.match(_status) if match: @@ -597,12 +615,13 @@ def get_value(self, constraints: ConstraintSet, *expressions): ) for i in range(expression.index_max): - self._smtlib.send("(get-value (%s))" % var[i].name) - ret = self._smtlib.recv() - pattern, base = self._get_value_fmt - m = pattern.match(ret) - expr, value = m.group("expr"), m.group("value") - result.append(int(value, base)) + # self._smtlib.send("(get-value (%s))" % var[i].name) + # ret = self._smtlib.recv() + # pattern, base = self._get_value_fmt + # m = pattern.match(ret) + # expr, value = m.group("expr"), m.group("value") + # result.append(int(value, base)) + result.append(self.__getvalue_bv(var[i].name)) values.append(bytes(result)) if time.time() - start > consts.timeout: raise SolverError("Timeout") @@ -617,18 +636,10 @@ def get_value(self, constraints: ConstraintSet, *expressions): "Solver could not find a value for expression under current constraint set" ) - self._smtlib.send("(get-value (%s))" % var.name) - ret = self._smtlib.recv() - if not (ret.startswith("((") and ret.endswith("))")): - raise SolverError("SMTLIB error parsing response: %s" % ret) - if isinstance(expression, Bool): - values.append({"true": True, "false": False}[ret[2:-2].split(" ")[1]]) + values.append(self.__getvalue_bool(var.name)) if isinstance(expression, BitVec): - pattern, base = self._get_value_fmt - m = pattern.match(ret) - expr, value = m.group("expr"), m.group("value") - values.append(int(value, base)) + values.append(self.__getvalue_bv(var.name)) if time.time() - start > consts.timeout: raise SolverError("Timeout") @@ -698,11 +709,13 @@ def _solver_version(self) -> Version: r".*(?P([0-9]+))\.(?P([0-9]+))\.(?P([0-9]+)).*" ) m = Z3VERSION.match(received_version.decode("utf-8")) - major, minor, patch = map(int, (m.group("major"), m.group("minor"), m.group("patch"))) + major, minor, patch = map( + int, (m.group("major"), m.group("minor"), m.group("patch")) # type: ignore + ) parsed_version = Version(major, minor, patch) except (ValueError, TypeError) as e: logger.warning( - f"Could not parse Z3 version: '{received_version}'. Assuming compatibility." + f"Could not parse Z3 version: '{str(received_version)}'. Assuming compatibility." ) parsed_version = Version(float("inf"), float("inf"), float("inf")) return parsed_version @@ -716,7 +729,7 @@ def __init__(self): command=command, init=init, value_fmt=2, - debug=False, + debug=True, support_minmax=False, support_reset=False, ) diff --git a/tests/other/test_smtlibv2.py b/tests/other/test_smtlibv2.py index 9943aec94..6f0de887f 100644 --- a/tests/other/test_smtlibv2.py +++ b/tests/other/test_smtlibv2.py @@ -1,4 +1,5 @@ import unittest +from unittest.mock import patch, mock_open from manticore.core.smtlib import ( ConstraintSet, @@ -21,6 +22,7 @@ # level = logging.DEBUG) +''' class Z3Specific(unittest.TestCase): _multiprocess_can_split_ = True @@ -28,8 +30,14 @@ def setUp(self): self.solver = Z3Solver.instance() - def test_check_solver_min(self): - self.solver._received_version = '(:version "4.4.1")' + @patch('subprocess.check_output', mock_open()) + def test_check_solver_min(self, mock_check_output): + mock_check_output.return_value = ("output", "Error") + #mock_check_output.return_value='(:version "4.4.1")' + #mock_function = create_autospec(function, return_value='(:version "4.4.1")') + #with patch.object(subprocess, 'check_output' , return_value='(:version "4.4.1")'): + #test_patch.return_value = '(:version "4.4.1")' + print (self.solver._solver_version()) self.assertTrue(self.solver._solver_version() == Version(major=4, minor=4, patch=1)) def test_check_solver_newer(self): @@ -43,11 +51,12 @@ def test_check_solver_long_format(self): def test_check_solver_undefined(self): self.solver._received_version = '(:version "78ed71b8de7d")' self.assertTrue( + self.solver._solver_version() == Version(major=float("inf"), minor=float("inf"), patch=float("inf")) ) self.assertTrue(self.solver._solver_version() > Version(major=4, minor=4, patch=1)) - +''' class ExpressionTest(unittest.TestCase): _multiprocess_can_split_ = True @@ -1009,18 +1018,16 @@ def test_API(self): for attr in attrs: self.assertTrue(hasattr(cls, attr), f"{cls.__name__} is missing attribute {attr}") + class ExpressionTestYices(ExpressionTest): def setUp(self): self.solver = YicesSolver.instance() + class ExpressionTestCVC4(ExpressionTest): def setUp(self): self.solver = CVC4Solver.instance() -class ExpressionTestRace(ExpressionTest): - def setUp(self): - self.solver = RaceSolver.instance() - if __name__ == "__main__": unittest.main() From 2af40be34ee2ff4a6c7703c2c0834afcf264de22 Mon Sep 17 00:00:00 2001 From: feliam Date: Tue, 26 May 2020 12:08:58 -0300 Subject: [PATCH 08/28] CC --- manticore/core/smtlib/solver.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/manticore/core/smtlib/solver.py b/manticore/core/smtlib/solver.py index 0b4a25aff..261a38934 100644 --- a/manticore/core/smtlib/solver.py +++ b/manticore/core/smtlib/solver.py @@ -239,7 +239,7 @@ def _restart(self) -> None: self.start() def is_started(self): - return self._proc != None + return self._proc is not None class SMTLIBSolver(Solver): @@ -767,7 +767,7 @@ def thread(solver): for instance in solver_instances: try: instance._proc.kill() - except: + except Exception: pass # already died for t in threads: t.join() From 57aa1872a89561b6939a19f78a1c38a86432f74a Mon Sep 17 00:00:00 2001 From: feliam Date: Tue, 26 May 2020 12:10:46 -0300 Subject: [PATCH 09/28] Default yices --- manticore/core/smtlib/solver.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/manticore/core/smtlib/solver.py b/manticore/core/smtlib/solver.py index 261a38934..5a00ececb 100644 --- a/manticore/core/smtlib/solver.py +++ b/manticore/core/smtlib/solver.py @@ -48,7 +48,7 @@ ) consts.add( - "solver", default="cvc4", description="Choose default smtlib2 solver (z3, yices, cvc4, race)" + "solver", default="yices", description="Choose default smtlib2 solver (z3, yices, cvc4, race)" ) # Regular expressions used by the solver From 0cdbaedf41feab66520da6314d664d67bb36c436 Mon Sep 17 00:00:00 2001 From: feliam Date: Tue, 26 May 2020 12:30:00 -0300 Subject: [PATCH 10/28] Default debug level fix --- manticore/core/smtlib/solver.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/manticore/core/smtlib/solver.py b/manticore/core/smtlib/solver.py index 5a00ececb..7801dff52 100644 --- a/manticore/core/smtlib/solver.py +++ b/manticore/core/smtlib/solver.py @@ -729,7 +729,7 @@ def __init__(self): command=command, init=init, value_fmt=2, - debug=True, + debug=False, support_minmax=False, support_reset=False, ) From 5c173094ba85b70bdc3c2c61c7d7d8c545d9ccd5 Mon Sep 17 00:00:00 2001 From: feliam Date: Tue, 26 May 2020 14:48:34 -0300 Subject: [PATCH 11/28] Quick auto solver --- manticore/core/smtlib/solver.py | 42 +++++++++++++++++++++++++++++---- manticore/utils/config.py | 10 ++++++++ manticore/wasm/structure.py | 3 ++- 3 files changed, 49 insertions(+), 6 deletions(-) diff --git a/manticore/core/smtlib/solver.py b/manticore/core/smtlib/solver.py index 7801dff52..b1b48e0e5 100644 --- a/manticore/core/smtlib/solver.py +++ b/manticore/core/smtlib/solver.py @@ -32,6 +32,13 @@ from ...utils.resources import check_memory_usage, check_disk_usage from . import issymbolic +class SolverType(config.ConfigEnum): + """Used as configuration constant for choosing solver flavor""" + z3 = "z3" + cvc4 = "cvc4" + yices = "yices" + auto = "auto" + logger = logging.getLogger(__name__) consts = config.get_group("smt") consts.add("timeout", default=240, description="Timeout, in seconds, for each Z3 invocation") @@ -41,14 +48,18 @@ default=10000, description="Maximum solutions to provide when solving for all values", ) -consts.add("z3_bin", default="z3", description="Z3 binary to use") +consts.add("z3_bin", default="z3", description="Z3 solver binary to use") +consts.add("cvc4_bin", default="cvc4", description="CVC4 solver binary to use") +consts.add("yices_bin", default="yices-smt2", description="Yices solver binary to use") + + consts.add("defaultunsat", default=True, description="Consider solver timeouts as unsat core") consts.add( "optimize", default=True, description="Use smtlib command optimize to find min/max if available" ) consts.add( - "solver", default="yices", description="Choose default smtlib2 solver (z3, yices, cvc4, race)" + "solver", default=SolverType.auto, description="Choose default smtlib2 solver (z3, yices, cvc4, race)" ) # Regular expressions used by the solver @@ -724,7 +735,7 @@ def _solver_version(self) -> Version: class YicesSolver(SMTLIBSolver): def __init__(self): init = ["(set-logic QF_AUFBV)"] - command = f"yices-smt2 --timeout={consts.timeout * 1000} --incremental" + command = f"{consts.yices_bin} --timeout={consts.timeout * 1000} --incremental" super().__init__( command=command, init=init, @@ -738,7 +749,7 @@ def __init__(self): class CVC4Solver(SMTLIBSolver): def __init__(self): init = ["(set-logic QF_AUFBV)", "(set-option :produce-models true)"] - command = f"cvc4 --lang=smt2 --incremental" + command = f"{consts.cvc4_bin} --lang=smt2 --incremental" super().__init__(command=command, value_fmt=10, init=init) @@ -773,5 +784,26 @@ def thread(solver): t.join() return result +class SelectedSolver: + choice = None + + @classmethod + def instance(cls): + if consts.solver == consts.solver.auto: + if cls.choice is None: + if os.path.exists(consts.yices_bin): + cls.choice = consts.solver.yices + elif os.path.exists(consts.z3_bin): + cls.choice = consts.solver.z3 + elif os.path.exists(consts.cvc4_bin): + cls.choice = consts.solver.cvc4 + else: + raise SolverException(f"No Solver not found. Install one ({const.yices_bin}, {consts.z3_bin}, {consts.cvc4_bin}).") + else: + cls.choice = consts.solver + + SelectedSolver = {"cvc4": CVC4Solver, "yices": YicesSolver, "z3": Z3Solver}[cls.choice.name] + print ("Using", SelectedSolver) + return SelectedSolver.instance() + -SelectedSolver = {"cvc4": CVC4Solver, "yices": YicesSolver, "z3": Z3Solver}[consts.solver] diff --git a/manticore/utils/config.py b/manticore/utils/config.py index a18f5e156..309f9d4dd 100644 --- a/manticore/utils/config.py +++ b/manticore/utils/config.py @@ -26,6 +26,16 @@ class ConfigError(Exception): pass +class ConfigEnum(Enum): + """Used as configuration constant for choosing flavors""" + + def title(self): + return self._name_.title() + + @classmethod + def from_string(cls, name): + return cls.__members__[name] + class _Var: def __init__(self, name: str = "", default=None, description: str = None, defined: bool = True): diff --git a/manticore/wasm/structure.py b/manticore/wasm/structure.py index 6be764c7b..5becb3ecf 100644 --- a/manticore/wasm/structure.py +++ b/manticore/wasm/structure.py @@ -67,7 +67,7 @@ from ..core.smtlib.solver import SelectedSolver -solver = SelectedSolver.instance() + logger = logging.getLogger(__name__) # logger.setLevel(logging.DEBUG) @@ -732,6 +732,7 @@ def __setstate__(self, state): def _eval_maybe_symbolic(constraints, expression) -> bool: if issymbolic(expression): + solver = SelectedSolver.instance() return solver.must_be_true(constraints, expression) return True if expression else False From a92cb6e7e773c7620117376fa70858f630803f15 Mon Sep 17 00:00:00 2001 From: feliam Date: Tue, 26 May 2020 15:01:49 -0300 Subject: [PATCH 12/28] shutil.which --- manticore/core/smtlib/solver.py | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/manticore/core/smtlib/solver.py b/manticore/core/smtlib/solver.py index b1b48e0e5..d5d674915 100644 --- a/manticore/core/smtlib/solver.py +++ b/manticore/core/smtlib/solver.py @@ -15,6 +15,7 @@ # You can add new constraints. A new constraint may change the state from {None, sat} to {sat, unsat, unknown} import os +import shutil import threading from queue import Queue import collections @@ -791,19 +792,18 @@ class SelectedSolver: def instance(cls): if consts.solver == consts.solver.auto: if cls.choice is None: - if os.path.exists(consts.yices_bin): + if shutil.which(consts.yices_bin): cls.choice = consts.solver.yices - elif os.path.exists(consts.z3_bin): + elif shutil.which(consts.z3_bin): cls.choice = consts.solver.z3 - elif os.path.exists(consts.cvc4_bin): + elif shutil.which(consts.cvc4_bin): cls.choice = consts.solver.cvc4 else: - raise SolverException(f"No Solver not found. Install one ({const.yices_bin}, {consts.z3_bin}, {consts.cvc4_bin}).") + raise SolverException(f"No Solver not found. Install one ({consts.yices_bin}, {consts.z3_bin}, {consts.cvc4_bin}).") else: cls.choice = consts.solver SelectedSolver = {"cvc4": CVC4Solver, "yices": YicesSolver, "z3": Z3Solver}[cls.choice.name] - print ("Using", SelectedSolver) return SelectedSolver.instance() From 3d912669530c8495ed2ca57ac8c5bcfcbf841674 Mon Sep 17 00:00:00 2001 From: feliam Date: Tue, 26 May 2020 15:50:25 -0300 Subject: [PATCH 13/28] CC --- manticore/core/smtlib/solver.py | 14 ++++++++++---- manticore/utils/config.py | 1 + manticore/wasm/structure.py | 1 - 3 files changed, 11 insertions(+), 5 deletions(-) diff --git a/manticore/core/smtlib/solver.py b/manticore/core/smtlib/solver.py index d5d674915..c38e10742 100644 --- a/manticore/core/smtlib/solver.py +++ b/manticore/core/smtlib/solver.py @@ -33,13 +33,16 @@ from ...utils.resources import check_memory_usage, check_disk_usage from . import issymbolic + class SolverType(config.ConfigEnum): """Used as configuration constant for choosing solver flavor""" + z3 = "z3" cvc4 = "cvc4" yices = "yices" auto = "auto" + logger = logging.getLogger(__name__) consts = config.get_group("smt") consts.add("timeout", default=240, description="Timeout, in seconds, for each Z3 invocation") @@ -60,7 +63,9 @@ class SolverType(config.ConfigEnum): ) consts.add( - "solver", default=SolverType.auto, description="Choose default smtlib2 solver (z3, yices, cvc4, race)" + "solver", + default=SolverType.auto, + description="Choose default smtlib2 solver (z3, yices, cvc4, race)", ) # Regular expressions used by the solver @@ -785,6 +790,7 @@ def thread(solver): t.join() return result + class SelectedSolver: choice = None @@ -799,11 +805,11 @@ def instance(cls): elif shutil.which(consts.cvc4_bin): cls.choice = consts.solver.cvc4 else: - raise SolverException(f"No Solver not found. Install one ({consts.yices_bin}, {consts.z3_bin}, {consts.cvc4_bin}).") + raise SolverException( + f"No Solver not found. Install one ({consts.yices_bin}, {consts.z3_bin}, {consts.cvc4_bin})." + ) else: cls.choice = consts.solver SelectedSolver = {"cvc4": CVC4Solver, "yices": YicesSolver, "z3": Z3Solver}[cls.choice.name] return SelectedSolver.instance() - - diff --git a/manticore/utils/config.py b/manticore/utils/config.py index 309f9d4dd..c1c617548 100644 --- a/manticore/utils/config.py +++ b/manticore/utils/config.py @@ -26,6 +26,7 @@ class ConfigError(Exception): pass + class ConfigEnum(Enum): """Used as configuration constant for choosing flavors""" diff --git a/manticore/wasm/structure.py b/manticore/wasm/structure.py index 5becb3ecf..667b052f2 100644 --- a/manticore/wasm/structure.py +++ b/manticore/wasm/structure.py @@ -68,7 +68,6 @@ from ..core.smtlib.solver import SelectedSolver - logger = logging.getLogger(__name__) # logger.setLevel(logging.DEBUG) From 60e020bae98c46a7e674df9692df264b2b1be506 Mon Sep 17 00:00:00 2001 From: feliam Date: Wed, 27 May 2020 00:36:32 -0300 Subject: [PATCH 14/28] Default yices for testing --- manticore/core/smtlib/solver.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/manticore/core/smtlib/solver.py b/manticore/core/smtlib/solver.py index c38e10742..1e91e8ce3 100644 --- a/manticore/core/smtlib/solver.py +++ b/manticore/core/smtlib/solver.py @@ -64,7 +64,7 @@ class SolverType(config.ConfigEnum): consts.add( "solver", - default=SolverType.auto, + default=SolverType.yices, description="Choose default smtlib2 solver (z3, yices, cvc4, race)", ) From afcd693adc763a99b05d02ac352c3f57ff79af0a Mon Sep 17 00:00:00 2001 From: feliam Date: Wed, 27 May 2020 00:38:58 -0300 Subject: [PATCH 15/28] Remove old commented out code --- manticore/core/smtlib/solver.py | 6 ------ 1 file changed, 6 deletions(-) diff --git a/manticore/core/smtlib/solver.py b/manticore/core/smtlib/solver.py index 1e91e8ce3..87f8e0015 100644 --- a/manticore/core/smtlib/solver.py +++ b/manticore/core/smtlib/solver.py @@ -377,12 +377,6 @@ def _getvalue(self, expression) -> Union[int, bool, bytes]: result = bytearray() for c in expression: expression_str = translate_to_smtlib(c) - # self._smtlib.send(f"(get-value ({expression_str}))") - # response = self._smtlib.recv().split(expression_str)[1].strip(")") - # pattern, base = self._get_value_fmt - # m = pattern.match(response) - # expr, value = m.group("expr"), m.group("value") - # result.append(int(value, base)) result.append(self.__getvalue_bv(expression_str)) return bytes(result) else: From 20f846dfc23237524f5d4e7d745cdc5f1ec5625e Mon Sep 17 00:00:00 2001 From: feliam Date: Thu, 28 May 2020 12:02:09 -0300 Subject: [PATCH 16/28] Update manticore/core/smtlib/solver.py Co-authored-by: Eric Kilmer --- manticore/core/smtlib/solver.py | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/manticore/core/smtlib/solver.py b/manticore/core/smtlib/solver.py index 1e91e8ce3..f9cae6c2f 100644 --- a/manticore/core/smtlib/solver.py +++ b/manticore/core/smtlib/solver.py @@ -350,8 +350,7 @@ def _assert(self, expression: Bool): smtlib = translate_to_smtlib(expression) self._smtlib.send(f"(assert {smtlib})") - # Union[Variable, int, bool, bytes] - def __getvalue_bv(self, expression_str): + def __getvalue_bv(self, expression_str: Union[Variable, int, bool, bytes]) -> int: self._smtlib.send(f"(get-value ({expression_str}))") pattern, base = self._get_value_fmt m = pattern.match(self._smtlib.recv()) From a60a6e70a76581e6ad0c8a6a5ff7a8a3a9523a5e Mon Sep 17 00:00:00 2001 From: feliam Date: Thu, 28 May 2020 12:02:28 -0300 Subject: [PATCH 17/28] Update manticore/core/smtlib/solver.py Co-authored-by: Eric Kilmer --- manticore/core/smtlib/solver.py | 6 ------ 1 file changed, 6 deletions(-) diff --git a/manticore/core/smtlib/solver.py b/manticore/core/smtlib/solver.py index f9cae6c2f..b66483ea2 100644 --- a/manticore/core/smtlib/solver.py +++ b/manticore/core/smtlib/solver.py @@ -631,12 +631,6 @@ def get_value(self, constraints: ConstraintSet, *expressions): ) for i in range(expression.index_max): - # self._smtlib.send("(get-value (%s))" % var[i].name) - # ret = self._smtlib.recv() - # pattern, base = self._get_value_fmt - # m = pattern.match(ret) - # expr, value = m.group("expr"), m.group("value") - # result.append(int(value, base)) result.append(self.__getvalue_bv(var[i].name)) values.append(bytes(result)) if time.time() - start > consts.timeout: From e4e3a65e9e9edaf1a757246183c9abf5b34b6359 Mon Sep 17 00:00:00 2001 From: feliam Date: Thu, 28 May 2020 12:05:26 -0300 Subject: [PATCH 18/28] Remove unused class --- manticore/core/smtlib/solver.py | 34 +-------------------------------- 1 file changed, 1 insertion(+), 33 deletions(-) diff --git a/manticore/core/smtlib/solver.py b/manticore/core/smtlib/solver.py index 1409504e6..e9a04519c 100644 --- a/manticore/core/smtlib/solver.py +++ b/manticore/core/smtlib/solver.py @@ -65,7 +65,7 @@ class SolverType(config.ConfigEnum): consts.add( "solver", default=SolverType.yices, - description="Choose default smtlib2 solver (z3, yices, cvc4, race)", + description="Choose default smtlib2 solver (z3, yices, cvc4, auto)", ) # Regular expressions used by the solver @@ -746,38 +746,6 @@ def __init__(self): super().__init__(command=command, value_fmt=10, init=init) -class ddRaceSolver(SMTLIBSolver): - def __init__(self, *solvers): - if not solvers: - solvers = (Z3Solver, YicesSolver, CVC4Solver) - self._solvers = solvers - - def _race(self, function_name, *args, **kwargs): - q = Queue() - solver_instances = [x() for x in self._solvers] - - def thread(solver): - try: - x = getattr(solver, function_name)(*args, **kwargs) - q.put(x) - except Exception as e: - print(e) - pass - - threads = [threading.Thread(target=thread, args=(x,)) for x in solver_instances] - for t in threads: - t.start() - result = q.get(block=True, timeout=consts.timeout) - for instance in solver_instances: - try: - instance._proc.kill() - except Exception: - pass # already died - for t in threads: - t.join() - return result - - class SelectedSolver: choice = None From af198630e575cef5232fba148bcf4909f5acd3d7 Mon Sep 17 00:00:00 2001 From: feliam Date: Thu, 28 May 2020 12:16:00 -0300 Subject: [PATCH 19/28] Update manticore/core/smtlib/solver.py Co-authored-by: Eric Kilmer --- manticore/core/smtlib/solver.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/manticore/core/smtlib/solver.py b/manticore/core/smtlib/solver.py index e9a04519c..0e583dfb1 100644 --- a/manticore/core/smtlib/solver.py +++ b/manticore/core/smtlib/solver.py @@ -580,7 +580,7 @@ def _optimize_fancy(self, constraints: ConstraintSet, x: BitVec, goal: str, max_ elif _status == "sat": ret = self._smtlib.recv() if not (ret.startswith("(") and ret.endswith(")")): - raise SolverError("bad output on max, z3 may have been killed") + raise SolverError("bad output on max, solver may have been killed") match = RE_OBJECTIVES_EXPR_VALUE.match(ret) if match: From 3061b7ce18e66aec1f454e07f11cfe358c1df889 Mon Sep 17 00:00:00 2001 From: feliam Date: Thu, 28 May 2020 12:16:19 -0300 Subject: [PATCH 20/28] Update manticore/core/smtlib/solver.py Co-authored-by: Eric Kilmer --- manticore/core/smtlib/solver.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/manticore/core/smtlib/solver.py b/manticore/core/smtlib/solver.py index 0e583dfb1..da9dd0001 100644 --- a/manticore/core/smtlib/solver.py +++ b/manticore/core/smtlib/solver.py @@ -384,7 +384,7 @@ def _getvalue(self, expression) -> Union[int, bool, bytes]: elif isinstance(expression, BitVecVariable): return self.__getvalue_bv(expression.name) - raise NotImplementedError("_getvalue only implemented for Bool, BitVec and Array") + raise NotImplementedError(f"_getvalue only implemented for Bool, BitVec and Array. Got {type(expression)}") # push pop def _push(self): From 38c888bb998e98f54d186632b9171d0df8c1fd02 Mon Sep 17 00:00:00 2001 From: feliam Date: Thu, 28 May 2020 12:53:21 -0300 Subject: [PATCH 21/28] Readme hack --- README.md | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/README.md b/README.md index 3f95e1ca3..bc65bb997 100644 --- a/README.md +++ b/README.md @@ -216,6 +216,23 @@ for idx, val_list in enumerate(m.collect_returns()): * We're still in the process of implementing full support for the EVM Istanbul instruction semantics, so certain opcodes may not be supported. In a pinch, you can try compiling with Solidity 0.4.x to avoid generating those instructions. +## Using a different solverr (Z3, Yices, CVC4) +Manticore relies on an external solver supporting smtlib2. Curently Z3, Yices and CVC4 are supported and can be selected via commandline or configuration settings. +By default Manticore will use Z3. Once you installed a different solver you can choose a different solver like this: +```manticore --smt.solver yices``` +### Installing CVC4 +For more details go to https://cvc4.github.io/. Otherwise just get the binary and use it. + + 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 + +### Installing Yices +Yices is incredibly fast. More details here https://yices.csl.sri.com/ + + sudo add-apt-repository ppa:sri-csl/formal-methods + sudo apt-get update + sudo apt-get install yices2 + ## Getting Help Feel free to stop by our #manticore slack channel in [Empire Hacking](https://empireslacking.herokuapp.com/) for help using or extending Manticore. From 6db6e77dd25d352b0e0d9f9eb8f72bcd7eaead35 Mon Sep 17 00:00:00 2001 From: feliam Date: Thu, 28 May 2020 14:21:18 -0300 Subject: [PATCH 22/28] CC/lint --- manticore/core/smtlib/solver.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/manticore/core/smtlib/solver.py b/manticore/core/smtlib/solver.py index da9dd0001..8e972ae9f 100644 --- a/manticore/core/smtlib/solver.py +++ b/manticore/core/smtlib/solver.py @@ -350,11 +350,11 @@ def _assert(self, expression: Bool): smtlib = translate_to_smtlib(expression) self._smtlib.send(f"(assert {smtlib})") - def __getvalue_bv(self, expression_str: Union[Variable, int, bool, bytes]) -> int: + def __getvalue_bv(self, expression_str: str) -> int: self._smtlib.send(f"(get-value ({expression_str}))") pattern, base = self._get_value_fmt m = pattern.match(self._smtlib.recv()) - expr, value = m.group("expr"), m.group("value") + expr, value = m.group("expr"), m.group("value") # type: ignore return int(value, base) def __getvalue_bool(self, expression_str): From 3e68a854533826cdfa52079a35637f9692649c14 Mon Sep 17 00:00:00 2001 From: feliam Date: Thu, 28 May 2020 15:59:03 -0300 Subject: [PATCH 23/28] Fix typing --- manticore/core/smtlib/solver.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/manticore/core/smtlib/solver.py b/manticore/core/smtlib/solver.py index 8e972ae9f..23d55c9c1 100644 --- a/manticore/core/smtlib/solver.py +++ b/manticore/core/smtlib/solver.py @@ -22,7 +22,7 @@ import shlex import time from functools import lru_cache -from typing import Dict, Tuple, Sequence +from typing import Dict, Tuple, Sequence, Optional from subprocess import PIPE, Popen, check_output import re from . import operators as Operators @@ -489,7 +489,7 @@ def _optimize_generic(self, constraints: ConstraintSet, x: BitVec, goal: str, ma @lru_cache(maxsize=32) def get_all_values( - self, constraints: ConstraintSet, expression, maxcnt: bool = None, silent: bool = False + self, constraints: ConstraintSet, expression, maxcnt: Optional[bool] = None, silent: bool = False ): """Returns a list with all the possible values for the symbol x""" if not isinstance(expression, Expression): From 5a97426a51f13416fb37e346131e36a94122af0a Mon Sep 17 00:00:00 2001 From: feliam Date: Fri, 29 May 2020 00:07:54 -0300 Subject: [PATCH 24/28] z3 back to the rodeo --- manticore/core/smtlib/solver.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/manticore/core/smtlib/solver.py b/manticore/core/smtlib/solver.py index 23d55c9c1..3abedc60d 100644 --- a/manticore/core/smtlib/solver.py +++ b/manticore/core/smtlib/solver.py @@ -64,7 +64,7 @@ class SolverType(config.ConfigEnum): consts.add( "solver", - default=SolverType.yices, + default=SolverType.z3, description="Choose default smtlib2 solver (z3, yices, cvc4, auto)", ) From 3ddb5b61e445733a965e4b96dd79da45299ed281 Mon Sep 17 00:00:00 2001 From: feliam Date: Tue, 2 Jun 2020 11:54:41 -0300 Subject: [PATCH 25/28] lint --- manticore/core/smtlib/solver.py | 10 ++++++++-- manticore/platforms/evm.py | 8 ++++++-- manticore/utils/emulate.py | 4 +++- manticore/wasm/manticore.py | 8 ++++++-- tests/other/test_smtlibv2.py | 5 +++-- 5 files changed, 26 insertions(+), 9 deletions(-) diff --git a/manticore/core/smtlib/solver.py b/manticore/core/smtlib/solver.py index 3abedc60d..ad7605e8f 100644 --- a/manticore/core/smtlib/solver.py +++ b/manticore/core/smtlib/solver.py @@ -384,7 +384,9 @@ def _getvalue(self, expression) -> Union[int, bool, bytes]: elif isinstance(expression, BitVecVariable): return self.__getvalue_bv(expression.name) - raise NotImplementedError(f"_getvalue only implemented for Bool, BitVec and Array. Got {type(expression)}") + raise NotImplementedError( + f"_getvalue only implemented for Bool, BitVec and Array. Got {type(expression)}" + ) # push pop def _push(self): @@ -489,7 +491,11 @@ def _optimize_generic(self, constraints: ConstraintSet, x: BitVec, goal: str, ma @lru_cache(maxsize=32) def get_all_values( - self, constraints: ConstraintSet, expression, maxcnt: Optional[bool] = None, silent: bool = False + self, + constraints: ConstraintSet, + expression, + maxcnt: Optional[bool] = None, + silent: bool = False, ): """Returns a list with all the possible values for the symbol x""" if not isinstance(expression, Expression): diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py index 501e095b8..c9fd43c87 100644 --- a/manticore/platforms/evm.py +++ b/manticore/platforms/evm.py @@ -1042,7 +1042,9 @@ def _consume(self, fee): # Try not to OOG. If it may be enough gas we ignore the OOG case. # A constraint is added to assert the gas is enough and the OOG state is ignored. # explore only when there is enough gas if possible - if SelectedSolver.instance().can_be_true(self.constraints, Operators.UGT(self.gas, fee)): + if SelectedSolver.instance().can_be_true( + self.constraints, Operators.UGT(self.gas, fee) + ): self.constraints.add(Operators.UGT(self.gas, fee)) else: logger.debug( @@ -1053,7 +1055,9 @@ def _consume(self, fee): # OOG soon. If it may NOT be enough gas we ignore the normal case. # A constraint is added to assert the gas is NOT enough and the other state is ignored. # explore only when there is enough gas if possible - if SelectedSolver.instance().can_be_true(self.constraints, Operators.ULE(self.gas, fee)): + if SelectedSolver.instance().can_be_true( + self.constraints, Operators.ULE(self.gas, fee) + ): self.constraints.add(Operators.ULE(self.gas, fee)) raise NotEnoughGas() else: diff --git a/manticore/utils/emulate.py b/manticore/utils/emulate.py index 1c677bef1..47a294cf8 100644 --- a/manticore/utils/emulate.py +++ b/manticore/utils/emulate.py @@ -351,7 +351,9 @@ def write_back_memory(self, where, expr, size): concrete_data = [] for c in data: if issymbolic(c): - c = chr(SelectedSolver.instance().get_value(self._cpu.memory.constraints, c)) + c = chr( + SelectedSolver.instance().get_value(self._cpu.memory.constraints, c) + ) concrete_data.append(c) data = concrete_data else: diff --git a/manticore/wasm/manticore.py b/manticore/wasm/manticore.py index 287223325..8826c8e4c 100644 --- a/manticore/wasm/manticore.py +++ b/manticore/wasm/manticore.py @@ -161,7 +161,9 @@ def collect_returns(self, n=1): inner.append( list( I32(a) # TODO - eventually we'll need to support floats as well. - for a in SelectedSolver.instance().get_all_values(state.constraints, ret) + for a in SelectedSolver.instance().get_all_values( + state.constraints, ret + ) ) ) elif ret.size == 64: @@ -170,7 +172,9 @@ def collect_returns(self, n=1): I64( a ) # TODO - that'll probably require us to subclass bitvecs into IxxBV and FxxBV - for a in SelectedSolver.instance().get_all_values(state.constraints, ret) + for a in SelectedSolver.instance().get_all_values( + state.constraints, ret + ) ) ) else: diff --git a/tests/other/test_smtlibv2.py b/tests/other/test_smtlibv2.py index 6f0de887f..ac14a267c 100644 --- a/tests/other/test_smtlibv2.py +++ b/tests/other/test_smtlibv2.py @@ -22,7 +22,7 @@ # level = logging.DEBUG) -''' +""" class Z3Specific(unittest.TestCase): _multiprocess_can_split_ = True @@ -56,7 +56,8 @@ def test_check_solver_undefined(self): == Version(major=float("inf"), minor=float("inf"), patch=float("inf")) ) self.assertTrue(self.solver._solver_version() > Version(major=4, minor=4, patch=1)) -''' +""" + class ExpressionTest(unittest.TestCase): _multiprocess_can_split_ = True From 2391ca18cb4790885170a19e67ba6f8c871ce68f Mon Sep 17 00:00:00 2001 From: feliam Date: Tue, 2 Jun 2020 18:45:07 -0300 Subject: [PATCH 26/28] Fancy optimize --- manticore/core/smtlib/solver.py | 42 +++++++-------------------------- 1 file changed, 8 insertions(+), 34 deletions(-) diff --git a/manticore/core/smtlib/solver.py b/manticore/core/smtlib/solver.py index ad7605e8f..233ab0568 100644 --- a/manticore/core/smtlib/solver.py +++ b/manticore/core/smtlib/solver.py @@ -565,39 +565,13 @@ def _optimize_fancy(self, constraints: ConstraintSet, x: BitVec, goal: str, max_ self._reset(temp_cs.to_string(related_to=X)) self._smtlib.send(aux.declaration) - start = time.time() - try: - self._assert(operation(X, aux)) - self._smtlib.send("(%s %s)" % (goal, aux.name)) - self._smtlib.send("(check-sat)") - _status = self._smtlib.recv() - if _status not in ("sat", "unsat", "unknown"): - # Minimize (or Maximize) sometimes prints the objective before the status - # This will be a line like NAME |-> VALUE - maybe_sat = self._smtlib.recv() - if maybe_sat == "sat": - match = RE_MIN_MAX_OBJECTIVE_EXPR_VALUE.match(_status) - if match: - expr, value = match.group("expr"), match.group("value") - assert expr == aux.name - return int(value) - else: - raise SolverError("Could not match MinMax objective value regex") - elif _status == "sat": - ret = self._smtlib.recv() - if not (ret.startswith("(") and ret.endswith(")")): - raise SolverError("bad output on max, solver may have been killed") - - match = RE_OBJECTIVES_EXPR_VALUE.match(ret) - if match: - expr, value = match.group("expr"), match.group("value") - assert expr == aux.name - return int(value) - else: - raise SolverError("Could not match objective value regex") - finally: - self._reset(temp_cs.to_string()) - self._smtlib.send(aux.declaration) + self._assert(operation(X, aux)) + self._smtlib.send("(%s %s)" % (goal, aux.name)) + self._smtlib.send("(check-sat)") + _status = self._smtlib.recv() + if _status == "sat": + return self._getvalue(aux) + raise SolverError("Optimize failed") def get_value(self, constraints: ConstraintSet, *expressions): """ @@ -686,7 +660,7 @@ def __init__(self): command=command, init=init, value_fmt=16, - support_minmax=False, + support_minmax=True, support_reset=True, support_pushpop=True, debug=False, From 05071bff841908fc4e0182e8e8653489ff095294 Mon Sep 17 00:00:00 2001 From: feliam Date: Fri, 5 Jun 2020 16:29:42 -0300 Subject: [PATCH 27/28] Fix lint --- manticore/core/smtlib/solver.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/manticore/core/smtlib/solver.py b/manticore/core/smtlib/solver.py index 55b5b7748..5b70dec76 100644 --- a/manticore/core/smtlib/solver.py +++ b/manticore/core/smtlib/solver.py @@ -496,7 +496,7 @@ def get_all_values( self, constraints: ConstraintSet, expression, - maxcnt: Optional[bool] = None, + maxcnt: Optional[int] = None, silent: bool = False, ): """Returns a list with all the possible values for the symbol x""" From 3f11904a46ee9f7d114842e272c8807285225707 Mon Sep 17 00:00:00 2001 From: feliam Date: Tue, 9 Jun 2020 11:54:20 -0300 Subject: [PATCH 28/28] CC reviewed --- manticore/core/smtlib/solver.py | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) diff --git a/manticore/core/smtlib/solver.py b/manticore/core/smtlib/solver.py index 5b70dec76..365b83a0e 100644 --- a/manticore/core/smtlib/solver.py +++ b/manticore/core/smtlib/solver.py @@ -205,16 +205,18 @@ def stop(self): self._proc.stdout.close() # Kill the process self._proc.kill() - # Wait for termination, to avoid zombies. - self._proc.wait() + # 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 "(error" in buf: - raise SolverException(f"Error in smtlib: {buf}") + # 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 = buf.count("("), buf.count(")") lparen, rparen = map(sum, zip(*((c == "(", c == ")") for c in buf))) return buf, lparen, rparen @@ -225,14 +227,11 @@ def send(self, cmd: str) -> None: :param cmd: a SMTLIBv2 command (ex. (check-sat)) """ - assert self._proc - assert self._proc.stdout - assert self._proc.stdin if self._debug: logger.debug(">%s", cmd) print(">", cmd) - self._proc.stdout.flush() - self._proc.stdin.write(f"{cmd}\n") + self._proc.stdout.flush() # type: ignore + self._proc.stdin.write(f"{cmd}\n") # type: ignore def recv(self) -> str: """Reads the response from the smtlib solver"""