From f9aafe8a9fa497130808422067a9422afdbaf24d Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Thu, 31 Jan 2019 22:33:12 +0530 Subject: [PATCH] Add a execution-time require checker flag --- mythril/analysis/solver.py | 11 +++++++---- tests/laser/evm_testsuite/evm_test.py | 3 ++- 2 files changed, 9 insertions(+), 5 deletions(-) diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py index 2eb057f6..98d3633a 100644 --- a/mythril/analysis/solver.py +++ b/mythril/analysis/solver.py @@ -13,18 +13,21 @@ import logging log = logging.getLogger(__name__) -def get_model(constraints, minimize=(), maximize=()): +def get_model(constraints, minimize=(), maximize=(), enforce_execution_time=True): """ :param constraints: :param minimize: :param maximize: + :param enforce_execution_time: Bool variable which enforces --execution-timeout's time :return: """ s = Optimize() - timeout = min(100000, time_handler.time_remaining() - 500) - if timeout <= 0: - raise UnsatError + timeout = 100000 + if enforce_execution_time: + timeout = min(timeout, time_handler.time_remaining() - 500) + if timeout <= 0: + raise UnsatError s.set_timeout(timeout) for constraint in constraints: if type(constraint) == bool and not constraint: diff --git a/tests/laser/evm_testsuite/evm_test.py b/tests/laser/evm_testsuite/evm_test.py index 4f32cc6d..6227b3ce 100644 --- a/tests/laser/evm_testsuite/evm_test.py +++ b/tests/laser/evm_testsuite/evm_test.py @@ -127,7 +127,8 @@ def test_vmtest( assert len(laser_evm.open_states) == 1 world_state = laser_evm.open_states[0] model = get_model( - next(iter(laser_evm.nodes.values())).states[0].mstate.constraints + next(iter(laser_evm.nodes.values())).states[0].mstate.constraints, + enforce_execution_time=False, ) for address, details in post_condition.items():