diff --git a/Changelog.md b/Changelog.md index 0ced53d8d..51201c06b 100644 --- a/Changelog.md +++ b/Changelog.md @@ -3,6 +3,8 @@ Compiler Features: * SMTChecker: Add division by zero checks in the CHC engine. * SMTChecker: Support ``selector`` for expressions with value known at compile-time. + * Command Line Interface: New option ``--model-checker-timeout`` sets a timeout in milliseconds for each individual query performed by the SMTChecker. + * Standard JSON: New option ``modelCheckerSettings.timeout`` sets a timeout in milliseconds for each individual query performed by the SMTChecker. Bugfixes: diff --git a/docs/using-the-compiler.rst b/docs/using-the-compiler.rst index 95a563688..69ec0d9dd 100644 --- a/docs/using-the-compiler.rst +++ b/docs/using-the-compiler.rst @@ -346,7 +346,12 @@ Input Description "modelCheckerSettings": { // Choose which model checker engine to use: all (default), bmc, chc, none. - "engine": "chc" + "engine": "chc", + // Timeout for each SMT query in milliseconds. + // If this option is not given, the SMTChecker will use a deterministic + // resource limit by default. + // A given timeout of 0 means no resource/time restrictions for any query. + "timeout": 20000 } } diff --git a/libsmtutil/CHCSmtLib2Interface.cpp b/libsmtutil/CHCSmtLib2Interface.cpp index bc3d1c6d9..d64f39379 100644 --- a/libsmtutil/CHCSmtLib2Interface.cpp +++ b/libsmtutil/CHCSmtLib2Interface.cpp @@ -36,11 +36,13 @@ using namespace solidity::frontend; using namespace solidity::smtutil; CHCSmtLib2Interface::CHCSmtLib2Interface( - map const& _queryResponses, - ReadCallback::Callback const& _smtCallback + map _queryResponses, + ReadCallback::Callback _smtCallback, + optional _queryTimeout ): - m_smtlib2(make_unique(_queryResponses, _smtCallback)), - m_queryResponses(_queryResponses), + CHCSolverInterface(_queryTimeout), + m_smtlib2(make_unique(_queryResponses, _smtCallback, m_queryTimeout)), + m_queryResponses(move(_queryResponses)), m_smtCallback(_smtCallback) { reset(); @@ -51,6 +53,8 @@ void CHCSmtLib2Interface::reset() m_accumulatedOutput.clear(); m_variables.clear(); m_unhandledQueries.clear(); + if (m_queryTimeout) + write("(set-option :timeout " + to_string(*m_queryTimeout) + ")"); } void CHCSmtLib2Interface::registerRelation(Expression const& _expr) diff --git a/libsmtutil/CHCSmtLib2Interface.h b/libsmtutil/CHCSmtLib2Interface.h index 7039431c4..f797d3d77 100644 --- a/libsmtutil/CHCSmtLib2Interface.h +++ b/libsmtutil/CHCSmtLib2Interface.h @@ -33,8 +33,9 @@ class CHCSmtLib2Interface: public CHCSolverInterface { public: explicit CHCSmtLib2Interface( - std::map const& _queryResponses, - frontend::ReadCallback::Callback const& _smtCallback + std::map _queryResponses = {}, + frontend::ReadCallback::Callback _smtCallback = {}, + std::optional _queryTimeout = {} ); void reset(); diff --git a/libsmtutil/CHCSolverInterface.h b/libsmtutil/CHCSolverInterface.h index c088f3d0f..203255345 100644 --- a/libsmtutil/CHCSolverInterface.h +++ b/libsmtutil/CHCSolverInterface.h @@ -33,6 +33,8 @@ namespace solidity::smtutil class CHCSolverInterface { public: + CHCSolverInterface(std::optional _queryTimeout = {}): m_queryTimeout(_queryTimeout) {} + virtual ~CHCSolverInterface() = default; virtual void declareVariable(std::string const& _name, SortPointer const& _sort) = 0; @@ -56,6 +58,9 @@ public: virtual std::pair query( Expression const& _expr ) = 0; + +protected: + std::optional m_queryTimeout; }; } diff --git a/libsmtutil/CVC4Interface.cpp b/libsmtutil/CVC4Interface.cpp index ced8f184a..56504930f 100644 --- a/libsmtutil/CVC4Interface.cpp +++ b/libsmtutil/CVC4Interface.cpp @@ -27,7 +27,8 @@ using namespace solidity; using namespace solidity::util; using namespace solidity::smtutil; -CVC4Interface::CVC4Interface(): +CVC4Interface::CVC4Interface(optional _queryTimeout): + SolverInterface(_queryTimeout), m_solver(&m_context) { reset(); @@ -38,7 +39,10 @@ void CVC4Interface::reset() m_variables.clear(); m_solver.reset(); m_solver.setOption("produce-models", true); - m_solver.setResourceLimit(resourceLimit); + if (m_queryTimeout) + m_solver.setTimeLimit(*m_queryTimeout); + else + m_solver.setResourceLimit(resourceLimit); } void CVC4Interface::push() diff --git a/libsmtutil/CVC4Interface.h b/libsmtutil/CVC4Interface.h index 16f9f1f81..5727be0e2 100644 --- a/libsmtutil/CVC4Interface.h +++ b/libsmtutil/CVC4Interface.h @@ -40,7 +40,7 @@ namespace solidity::smtutil class CVC4Interface: public SolverInterface, public boost::noncopyable { public: - CVC4Interface(); + CVC4Interface(std::optional _queryTimeout = {}); void reset() override; diff --git a/libsmtutil/SMTLib2Interface.cpp b/libsmtutil/SMTLib2Interface.cpp index e1bc7d0b4..e4ea16545 100644 --- a/libsmtutil/SMTLib2Interface.cpp +++ b/libsmtutil/SMTLib2Interface.cpp @@ -39,8 +39,10 @@ using namespace solidity::smtutil; SMTLib2Interface::SMTLib2Interface( map _queryResponses, - ReadCallback::Callback _smtCallback + ReadCallback::Callback _smtCallback, + optional _queryTimeout ): + SolverInterface(_queryTimeout), m_queryResponses(move(_queryResponses)), m_smtCallback(move(_smtCallback)) { @@ -54,6 +56,8 @@ void SMTLib2Interface::reset() m_variables.clear(); m_userSorts.clear(); write("(set-option :produce-models true)"); + if (m_queryTimeout) + write("(set-option :timeout " + to_string(*m_queryTimeout) + ")"); write("(set-logic ALL)"); } diff --git a/libsmtutil/SMTLib2Interface.h b/libsmtutil/SMTLib2Interface.h index 4c21b1f1c..104862f27 100644 --- a/libsmtutil/SMTLib2Interface.h +++ b/libsmtutil/SMTLib2Interface.h @@ -40,7 +40,8 @@ class SMTLib2Interface: public SolverInterface, public boost::noncopyable public: explicit SMTLib2Interface( std::map _queryResponses = {}, - frontend::ReadCallback::Callback _smtCallback = {} + frontend::ReadCallback::Callback _smtCallback = {}, + std::optional _queryTimeout = {} ); void reset() override; diff --git a/libsmtutil/SMTPortfolio.cpp b/libsmtutil/SMTPortfolio.cpp index 9858247a1..4718d36c4 100644 --- a/libsmtutil/SMTPortfolio.cpp +++ b/libsmtutil/SMTPortfolio.cpp @@ -35,17 +35,19 @@ using namespace solidity::smtutil; SMTPortfolio::SMTPortfolio( map _smtlib2Responses, frontend::ReadCallback::Callback _smtCallback, - [[maybe_unused]] SMTSolverChoice _enabledSolvers -) + [[maybe_unused]] SMTSolverChoice _enabledSolvers, + optional _queryTimeout +): + SolverInterface(_queryTimeout) { - m_solvers.emplace_back(make_unique(move(_smtlib2Responses), move(_smtCallback))); + m_solvers.emplace_back(make_unique(move(_smtlib2Responses), move(_smtCallback), m_queryTimeout)); #ifdef HAVE_Z3 if (_enabledSolvers.z3) - m_solvers.emplace_back(make_unique()); + m_solvers.emplace_back(make_unique(m_queryTimeout)); #endif #ifdef HAVE_CVC4 if (_enabledSolvers.cvc4) - m_solvers.emplace_back(make_unique()); + m_solvers.emplace_back(make_unique(m_queryTimeout)); #endif } diff --git a/libsmtutil/SMTPortfolio.h b/libsmtutil/SMTPortfolio.h index e4a662203..aca50eef7 100644 --- a/libsmtutil/SMTPortfolio.h +++ b/libsmtutil/SMTPortfolio.h @@ -42,7 +42,8 @@ public: SMTPortfolio( std::map _smtlib2Responses = {}, frontend::ReadCallback::Callback _smtCallback = {}, - SMTSolverChoice _enabledSolvers = SMTSolverChoice::All() + SMTSolverChoice _enabledSolvers = SMTSolverChoice::All(), + std::optional _queryTimeout = {} ); void reset() override; diff --git a/libsmtutil/SolverInterface.h b/libsmtutil/SolverInterface.h index 8ea0c5250..a3a3fb497 100644 --- a/libsmtutil/SolverInterface.h +++ b/libsmtutil/SolverInterface.h @@ -374,6 +374,8 @@ DEV_SIMPLE_EXCEPTION(SolverError); class SolverInterface { public: + SolverInterface(std::optional _queryTimeout = {}): m_queryTimeout(_queryTimeout) {} + virtual ~SolverInterface() = default; virtual void reset() = 0; @@ -401,6 +403,9 @@ public: /// @returns how many SMT solvers this interface has. virtual unsigned solvers() { return 1; } + +protected: + std::optional m_queryTimeout; }; } diff --git a/libsmtutil/Z3CHCInterface.cpp b/libsmtutil/Z3CHCInterface.cpp index e2b933b68..66ba55801 100644 --- a/libsmtutil/Z3CHCInterface.cpp +++ b/libsmtutil/Z3CHCInterface.cpp @@ -27,14 +27,19 @@ using namespace std; using namespace solidity; using namespace solidity::smtutil; -Z3CHCInterface::Z3CHCInterface(): - m_z3Interface(make_unique()), +Z3CHCInterface::Z3CHCInterface(optional _queryTimeout): + CHCSolverInterface(_queryTimeout), + m_z3Interface(make_unique(m_queryTimeout)), m_context(m_z3Interface->context()), m_solver(*m_context) { // These need to be set globally. z3::set_param("rewriter.pull_cheap_ite", true); - z3::set_param("rlimit", Z3Interface::resourceLimit); + + if (m_queryTimeout) + m_context->set("timeout", int(*m_queryTimeout)); + else + z3::set_param("rlimit", Z3Interface::resourceLimit); setSpacerOptions(); } @@ -97,7 +102,13 @@ pair Z3CHCInterface::query(Expression } catch (z3::exception const& _err) { - if (_err.msg() == string("max. resource limit exceeded")) + set msgs{ + /// Resource limit (rlimit) exhausted. + "max. resource limit exceeded", + /// User given timeout exhausted. + "canceled" + }; + if (msgs.count(_err.msg())) result = CheckResult::UNKNOWN; else result = CheckResult::ERROR; diff --git a/libsmtutil/Z3CHCInterface.h b/libsmtutil/Z3CHCInterface.h index 00e4ca285..a0d678536 100644 --- a/libsmtutil/Z3CHCInterface.h +++ b/libsmtutil/Z3CHCInterface.h @@ -33,7 +33,7 @@ namespace solidity::smtutil class Z3CHCInterface: public CHCSolverInterface { public: - Z3CHCInterface(); + Z3CHCInterface(std::optional _queryTimeout = {}); /// Forwards variable declaration to Z3Interface. void declareVariable(std::string const& _name, SortPointer const& _sort) override; diff --git a/libsmtutil/Z3Interface.cpp b/libsmtutil/Z3Interface.cpp index cfef7db72..3e01dd62c 100644 --- a/libsmtutil/Z3Interface.cpp +++ b/libsmtutil/Z3Interface.cpp @@ -27,12 +27,17 @@ using namespace std; using namespace solidity::smtutil; using namespace solidity::util; -Z3Interface::Z3Interface(): +Z3Interface::Z3Interface(std::optional _queryTimeout): + SolverInterface(_queryTimeout), m_solver(m_context) { // These need to be set globally. z3::set_param("rewriter.pull_cheap_ite", true); - z3::set_param("rlimit", resourceLimit); + + if (m_queryTimeout) + m_context.set("timeout", int(*m_queryTimeout)); + else + z3::set_param("rlimit", resourceLimit); } void Z3Interface::reset() @@ -104,9 +109,19 @@ pair> Z3Interface::check(vector const& _ values.push_back(util::toString(m.eval(toZ3Expr(e)))); } } - catch (z3::exception const&) + catch (z3::exception const& _err) { - result = CheckResult::ERROR; + set msgs{ + /// Resource limit (rlimit) exhausted. + "max. resource limit exceeded", + /// User given timeout exhausted. + "canceled" + }; + + if (msgs.count(_err.msg())) + result = CheckResult::UNKNOWN; + else + result = CheckResult::ERROR; values.clear(); } diff --git a/libsmtutil/Z3Interface.h b/libsmtutil/Z3Interface.h index 487723416..16c8ceb2b 100644 --- a/libsmtutil/Z3Interface.h +++ b/libsmtutil/Z3Interface.h @@ -28,7 +28,7 @@ namespace solidity::smtutil class Z3Interface: public SolverInterface, public boost::noncopyable { public: - Z3Interface(); + Z3Interface(std::optional _queryTimeout = {}); void reset() override; diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index e41c69cd2..8dc72c8a4 100644 --- a/libsolidity/formal/BMC.cpp +++ b/libsolidity/formal/BMC.cpp @@ -34,10 +34,11 @@ BMC::BMC( ErrorReporter& _errorReporter, map const& _smtlib2Responses, ReadCallback::Callback const& _smtCallback, - smtutil::SMTSolverChoice _enabledSolvers + smtutil::SMTSolverChoice _enabledSolvers, + optional _timeout ): SMTEncoder(_context), - m_interface(make_unique(_smtlib2Responses, _smtCallback, _enabledSolvers)), + m_interface(make_unique(_smtlib2Responses, _smtCallback, _enabledSolvers, _timeout)), m_outerErrorReporter(_errorReporter) { #if defined (HAVE_Z3) || defined (HAVE_CVC4) diff --git a/libsolidity/formal/BMC.h b/libsolidity/formal/BMC.h index b1fc5f675..d55ce7666 100644 --- a/libsolidity/formal/BMC.h +++ b/libsolidity/formal/BMC.h @@ -61,7 +61,8 @@ public: langutil::ErrorReporter& _errorReporter, std::map const& _smtlib2Responses, ReadCallback::Callback const& _smtCallback, - smtutil::SMTSolverChoice _enabledSolvers + smtutil::SMTSolverChoice _enabledSolvers, + std::optional timeout ); void analyze(SourceUnit const& _sources, std::map> _solvedTargets); diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 87f5ad1b8..3b870b364 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -49,18 +49,20 @@ CHC::CHC( ErrorReporter& _errorReporter, [[maybe_unused]] map const& _smtlib2Responses, [[maybe_unused]] ReadCallback::Callback const& _smtCallback, - SMTSolverChoice _enabledSolvers + SMTSolverChoice _enabledSolvers, + optional _timeout ): SMTEncoder(_context), m_outerErrorReporter(_errorReporter), - m_enabledSolvers(_enabledSolvers) + m_enabledSolvers(_enabledSolvers), + m_queryTimeout(_timeout) { bool usesZ3 = _enabledSolvers.z3; #ifndef HAVE_Z3 usesZ3 = false; #endif if (!usesZ3) - m_interface = make_unique(_smtlib2Responses, _smtCallback); + m_interface = make_unique(_smtlib2Responses, _smtCallback, m_queryTimeout); } void CHC::analyze(SourceUnit const& _source) @@ -681,7 +683,7 @@ void CHC::resetSourceAnalysis() if (usesZ3) { /// z3::fixedpoint does not have a reset mechanism, so we need to create another. - m_interface.reset(new Z3CHCInterface()); + m_interface.reset(new Z3CHCInterface(m_queryTimeout)); auto z3Interface = dynamic_cast(m_interface.get()); solAssert(z3Interface, ""); m_context.setSolver(z3Interface->z3Interface()); diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h index 179ae62af..498689887 100644 --- a/libsolidity/formal/CHC.h +++ b/libsolidity/formal/CHC.h @@ -55,7 +55,8 @@ public: langutil::ErrorReporter& _errorReporter, std::map const& _smtlib2Responses, ReadCallback::Callback const& _smtCallback, - smtutil::SMTSolverChoice _enabledSolvers + smtutil::SMTSolverChoice _enabledSolvers, + std::optional timeout ); void analyze(SourceUnit const& _sources); @@ -330,6 +331,9 @@ private: /// SMT solvers that are chosen at runtime. smtutil::SMTSolverChoice m_enabledSolvers; + + /// SMT query timeout in seconds. + std::optional m_queryTimeout; }; } diff --git a/libsolidity/formal/ModelChecker.cpp b/libsolidity/formal/ModelChecker.cpp index 40317e2ca..eab27589b 100644 --- a/libsolidity/formal/ModelChecker.cpp +++ b/libsolidity/formal/ModelChecker.cpp @@ -27,14 +27,14 @@ using namespace solidity::frontend; ModelChecker::ModelChecker( ErrorReporter& _errorReporter, map const& _smtlib2Responses, - ModelCheckerEngine _engine, + ModelCheckerSettings _settings, ReadCallback::Callback const& _smtCallback, smtutil::SMTSolverChoice _enabledSolvers ): - m_engine(_engine), + m_settings(_settings), m_context(), - m_bmc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, _enabledSolvers), - m_chc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, _enabledSolvers) + m_bmc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, _enabledSolvers, _settings.timeout), + m_chc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, _enabledSolvers, _settings.timeout) { } @@ -43,14 +43,14 @@ void ModelChecker::analyze(SourceUnit const& _source) if (!_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker)) return; - if (m_engine.chc) + if (m_settings.engine.chc) m_chc.analyze(_source); auto solvedTargets = m_chc.safeTargets(); for (auto const& target: m_chc.unsafeTargets()) solvedTargets[target.first] += target.second; - if (m_engine.bmc) + if (m_settings.engine.bmc) m_bmc.analyze(_source, solvedTargets); } diff --git a/libsolidity/formal/ModelChecker.h b/libsolidity/formal/ModelChecker.h index 658bfb6da..78770aa4e 100644 --- a/libsolidity/formal/ModelChecker.h +++ b/libsolidity/formal/ModelChecker.h @@ -71,6 +71,12 @@ struct ModelCheckerEngine } }; +struct ModelCheckerSettings +{ + ModelCheckerEngine engine = ModelCheckerEngine::All(); + std::optional timeout; +}; + class ModelChecker { public: @@ -79,7 +85,7 @@ public: ModelChecker( langutil::ErrorReporter& _errorReporter, std::map const& _smtlib2Responses, - ModelCheckerEngine _engine = ModelCheckerEngine::All(), + ModelCheckerSettings _settings = ModelCheckerSettings{}, ReadCallback::Callback const& _smtCallback = ReadCallback::Callback(), smtutil::SMTSolverChoice _enabledSolvers = smtutil::SMTSolverChoice::All() ); @@ -95,7 +101,7 @@ public: static smtutil::SMTSolverChoice availableSolvers(); private: - ModelCheckerEngine m_engine; + ModelCheckerSettings m_settings; /// Stores the context of the encoding. smt::EncodingContext m_context; diff --git a/libsolidity/interface/CompilerStack.cpp b/libsolidity/interface/CompilerStack.cpp index 119ea42b8..5961e58a9 100644 --- a/libsolidity/interface/CompilerStack.cpp +++ b/libsolidity/interface/CompilerStack.cpp @@ -87,7 +87,6 @@ static int g_compilerStackCounts = 0; CompilerStack::CompilerStack(ReadCallback::Callback _readFile): m_readFile{std::move(_readFile)}, - m_modelCheckerEngine{ModelCheckerEngine::All()}, m_enabledSMTSolvers{smtutil::SMTSolverChoice::All()}, m_errorReporter{m_errorList} { @@ -139,11 +138,11 @@ void CompilerStack::setEVMVersion(langutil::EVMVersion _version) m_evmVersion = _version; } -void CompilerStack::setModelCheckerEngine(ModelCheckerEngine _engine) +void CompilerStack::setModelCheckerSettings(ModelCheckerSettings _settings) { if (m_stackState >= ParsedAndImported) - BOOST_THROW_EXCEPTION(CompilerError() << errinfo_comment("Must set enabled model checking engines before parsing.")); - m_modelCheckerEngine = _engine; + BOOST_THROW_EXCEPTION(CompilerError() << errinfo_comment("Must set model checking settings before parsing.")); + m_modelCheckerSettings = _settings; } void CompilerStack::setSMTSolverChoice(smtutil::SMTSolverChoice _enabledSMTSolvers) @@ -215,7 +214,7 @@ void CompilerStack::reset(bool _keepSettings) m_remappings.clear(); m_libraries.clear(); m_evmVersion = langutil::EVMVersion(); - m_modelCheckerEngine = ModelCheckerEngine::All(); + m_modelCheckerSettings = ModelCheckerSettings{}; m_enabledSMTSolvers = smtutil::SMTSolverChoice::All(); m_generateIR = false; m_generateEwasm = false; @@ -452,7 +451,7 @@ bool CompilerStack::analyze() if (noErrors) { - ModelChecker modelChecker(m_errorReporter, m_smtlib2Responses, m_modelCheckerEngine, m_readFile, m_enabledSMTSolvers); + ModelChecker modelChecker(m_errorReporter, m_smtlib2Responses, m_modelCheckerSettings, m_readFile, m_enabledSMTSolvers); for (Source const* source: m_sourceOrder) if (source->ast) modelChecker.analyze(*source->ast); diff --git a/libsolidity/interface/CompilerStack.h b/libsolidity/interface/CompilerStack.h index fd82c8feb..a0c02e881 100644 --- a/libsolidity/interface/CompilerStack.h +++ b/libsolidity/interface/CompilerStack.h @@ -167,8 +167,8 @@ public: /// Must be set before parsing. void setEVMVersion(langutil::EVMVersion _version = langutil::EVMVersion{}); - /// Set which model checking engines should be used. - void setModelCheckerEngine(ModelCheckerEngine _engine); + /// Set model checker settings. + void setModelCheckerSettings(ModelCheckerSettings _settings); /// Set which SMT solvers should be enabled. void setSMTSolverChoice(smtutil::SMTSolverChoice _enabledSolvers); @@ -456,7 +456,7 @@ private: RevertStrings m_revertStrings = RevertStrings::Default; State m_stopAfter = State::CompilationSuccessful; langutil::EVMVersion m_evmVersion; - ModelCheckerEngine m_modelCheckerEngine; + ModelCheckerSettings m_modelCheckerSettings; smtutil::SMTSolverChoice m_enabledSMTSolvers; std::map> m_requestedContractNames; bool m_generateEvmBytecode = true; diff --git a/libsolidity/interface/StandardCompiler.cpp b/libsolidity/interface/StandardCompiler.cpp index 1a1a013fb..3b4ef56c5 100644 --- a/libsolidity/interface/StandardCompiler.cpp +++ b/libsolidity/interface/StandardCompiler.cpp @@ -420,7 +420,7 @@ std::optional checkSettingsKeys(Json::Value const& _input) std::optional checkModelCheckerSettingsKeys(Json::Value const& _input) { - static set keys{"engine"}; + static set keys{"engine", "timeout"}; return checkKeys(_input, keys, "modelCheckerSettings"); } @@ -885,7 +885,14 @@ std::variant StandardCompiler: std::optional engine = ModelCheckerEngine::fromString(modelCheckerSettings["engine"].asString()); if (!engine) return formatFatalError("JSONError", "Invalid model checker engine requested."); - ret.modelCheckerEngine = *engine; + ret.modelCheckerSettings.engine = *engine; + } + + if (modelCheckerSettings.isMember("timeout")) + { + if (!modelCheckerSettings["timeout"].isUInt()) + return formatFatalError("JSONError", "modelCheckerSettings.timeout must be an unsigned integer."); + ret.modelCheckerSettings.timeout = modelCheckerSettings["timeout"].asUInt(); } return { std::move(ret) }; @@ -908,7 +915,7 @@ Json::Value StandardCompiler::compileSolidity(StandardCompiler::InputsAndSetting compilerStack.useMetadataLiteralSources(_inputsAndSettings.metadataLiteralSources); compilerStack.setMetadataHash(_inputsAndSettings.metadataHash); compilerStack.setRequestedContractNames(requestedContractNames(_inputsAndSettings.outputSelection)); - compilerStack.setModelCheckerEngine(_inputsAndSettings.modelCheckerEngine); + compilerStack.setModelCheckerSettings(_inputsAndSettings.modelCheckerSettings); compilerStack.enableEvmBytecodeGeneration(isEvmBytecodeRequested(_inputsAndSettings.outputSelection)); compilerStack.enableIRGeneration(isIRRequested(_inputsAndSettings.outputSelection)); diff --git a/libsolidity/interface/StandardCompiler.h b/libsolidity/interface/StandardCompiler.h index d517b2eec..54b3fd3cf 100644 --- a/libsolidity/interface/StandardCompiler.h +++ b/libsolidity/interface/StandardCompiler.h @@ -71,7 +71,7 @@ private: bool metadataLiteralSources = false; CompilerStack::MetadataHash metadataHash = CompilerStack::MetadataHash::IPFS; Json::Value outputSelection; - ModelCheckerEngine modelCheckerEngine = ModelCheckerEngine::All(); + ModelCheckerSettings modelCheckerSettings = ModelCheckerSettings{}; }; /// Parses the input json (and potentially invokes the read callback) and either returns diff --git a/solc/CommandLineInterface.cpp b/solc/CommandLineInterface.cpp index 3ba999e09..1d8e24b7e 100644 --- a/solc/CommandLineInterface.cpp +++ b/solc/CommandLineInterface.cpp @@ -147,6 +147,7 @@ static string const g_strMetadata = "metadata"; static string const g_strMetadataHash = "metadata-hash"; static string const g_strMetadataLiteral = "metadata-literal"; static string const g_strModelCheckerEngine = "model-checker-engine"; +static string const g_strModelCheckerTimeout = "model-checker-timeout"; static string const g_strNatspecDev = "devdoc"; static string const g_strNatspecUser = "userdoc"; static string const g_strNone = "none"; @@ -217,6 +218,7 @@ static string const g_argMetadata = g_strMetadata; static string const g_argMetadataHash = g_strMetadataHash; static string const g_argMetadataLiteral = g_strMetadataLiteral; static string const g_argModelCheckerEngine = g_strModelCheckerEngine; +static string const g_argModelCheckerTimeout = g_strModelCheckerTimeout; static string const g_argNatspecDev = g_strNatspecDev; static string const g_argNatspecUser = g_strNatspecUser; static string const g_argOpcodes = g_strOpcodes; @@ -1002,6 +1004,13 @@ General Information)").c_str(), po::value()->value_name("all,bmc,chc,none")->default_value("all"), "Select model checker engine." ) + ( + g_strModelCheckerTimeout.c_str(), + po::value()->value_name("ms"), + "Set model checker timeout per query in milliseconds. " + "The default is a deterministic resource limit. " + "A timeout of 0 means no resource/time restrictions for any query." + ) ; desc.add(smtCheckerOptions); @@ -1400,9 +1409,12 @@ bool CommandLineInterface::processInput() serr() << "Invalid option for --" << g_argModelCheckerEngine << ": " << engineStr << endl; return false; } - m_modelCheckerEngine = *engine; + m_modelCheckerSettings.engine = *engine; } + if (m_args.count(g_argModelCheckerTimeout)) + m_modelCheckerSettings.timeout = m_args[g_argModelCheckerTimeout].as(); + m_compiler = make_unique(fileReader); unique_ptr formatter; @@ -1417,8 +1429,8 @@ bool CommandLineInterface::processInput() m_compiler->useMetadataLiteralSources(true); if (m_args.count(g_argMetadataHash)) m_compiler->setMetadataHash(m_metadataHash); - if (m_args.count(g_argModelCheckerEngine)) - m_compiler->setModelCheckerEngine(m_modelCheckerEngine); + if (m_args.count(g_argModelCheckerEngine) || m_args.count(g_argModelCheckerTimeout)) + m_compiler->setModelCheckerSettings(m_modelCheckerSettings); if (m_args.count(g_argInputFile)) m_compiler->setRemappings(m_remappings); diff --git a/solc/CommandLineInterface.h b/solc/CommandLineInterface.h index 12ed819e9..f7abb0524 100644 --- a/solc/CommandLineInterface.h +++ b/solc/CommandLineInterface.h @@ -133,8 +133,8 @@ private: RevertStrings m_revertStrings = RevertStrings::Default; /// Chosen hash method for the bytecode metadata. CompilerStack::MetadataHash m_metadataHash = CompilerStack::MetadataHash::IPFS; - /// Chosen model checker engine. - ModelCheckerEngine m_modelCheckerEngine = ModelCheckerEngine::All(); + /// Model checker settings. + ModelCheckerSettings m_modelCheckerSettings; /// Whether or not to colorize diagnostics output. bool m_coloredOutput = true; /// Whether or not to output error IDs. diff --git a/test/cmdlineTests/model_checker_timeout_all/args b/test/cmdlineTests/model_checker_timeout_all/args new file mode 100644 index 000000000..23b9eefe0 --- /dev/null +++ b/test/cmdlineTests/model_checker_timeout_all/args @@ -0,0 +1 @@ +--model-checker-timeout 1 diff --git a/test/cmdlineTests/model_checker_timeout_all/err b/test/cmdlineTests/model_checker_timeout_all/err new file mode 100644 index 000000000..7b991760d --- /dev/null +++ b/test/cmdlineTests/model_checker_timeout_all/err @@ -0,0 +1,50 @@ +Warning: CHC: Assertion violation might happen here. + --> model_checker_timeout_all/input.sol:6:3: + | +6 | assert(x > 0); + | ^^^^^^^^^^^^^ + +Warning: CHC: Assertion violation might happen here. + --> model_checker_timeout_all/input.sol:7:3: + | +7 | assert(x > 2); + | ^^^^^^^^^^^^^ + +Warning: CHC: Assertion violation might happen here. + --> model_checker_timeout_all/input.sol:8:3: + | +8 | assert(x > 4); + | ^^^^^^^^^^^^^ + +Warning: BMC: Assertion violation happens here. + --> model_checker_timeout_all/input.sol:6:3: + | +6 | assert(x > 0); + | ^^^^^^^^^^^^^ +Note: Counterexample: + x = 0 + +Note: Callstack: +Note: + +Warning: BMC: Assertion violation happens here. + --> model_checker_timeout_all/input.sol:7:3: + | +7 | assert(x > 2); + | ^^^^^^^^^^^^^ +Note: Counterexample: + x = 1 + +Note: Callstack: +Note: + +Warning: BMC: Assertion violation happens here. + --> model_checker_timeout_all/input.sol:8:3: + | +8 | assert(x > 4); + | ^^^^^^^^^^^^^ +Note: Counterexample: + x = 3 + +Note: Callstack: +Note: diff --git a/test/cmdlineTests/model_checker_timeout_all/input.sol b/test/cmdlineTests/model_checker_timeout_all/input.sol new file mode 100644 index 000000000..9c0134028 --- /dev/null +++ b/test/cmdlineTests/model_checker_timeout_all/input.sol @@ -0,0 +1,10 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; +pragma experimental SMTChecker; +contract test { + function f(uint x) public pure { + assert(x > 0); + assert(x > 2); + assert(x > 4); + } +} \ No newline at end of file diff --git a/test/cmdlineTests/model_checker_timeout_bmc/args b/test/cmdlineTests/model_checker_timeout_bmc/args new file mode 100644 index 000000000..fb07933d7 --- /dev/null +++ b/test/cmdlineTests/model_checker_timeout_bmc/args @@ -0,0 +1 @@ +--model-checker-engine bmc --model-checker-timeout 1 diff --git a/test/cmdlineTests/model_checker_timeout_bmc/err b/test/cmdlineTests/model_checker_timeout_bmc/err new file mode 100644 index 000000000..e44cc1c13 --- /dev/null +++ b/test/cmdlineTests/model_checker_timeout_bmc/err @@ -0,0 +1,32 @@ +Warning: BMC: Assertion violation happens here. + --> model_checker_timeout_bmc/input.sol:6:3: + | +6 | assert(x > 0); + | ^^^^^^^^^^^^^ +Note: Counterexample: + x = 0 + +Note: Callstack: +Note: + +Warning: BMC: Assertion violation happens here. + --> model_checker_timeout_bmc/input.sol:7:3: + | +7 | assert(x > 2); + | ^^^^^^^^^^^^^ +Note: Counterexample: + x = 1 + +Note: Callstack: +Note: + +Warning: BMC: Assertion violation happens here. + --> model_checker_timeout_bmc/input.sol:8:3: + | +8 | assert(x > 4); + | ^^^^^^^^^^^^^ +Note: Counterexample: + x = 3 + +Note: Callstack: +Note: diff --git a/test/cmdlineTests/model_checker_timeout_bmc/input.sol b/test/cmdlineTests/model_checker_timeout_bmc/input.sol new file mode 100644 index 000000000..9c0134028 --- /dev/null +++ b/test/cmdlineTests/model_checker_timeout_bmc/input.sol @@ -0,0 +1,10 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; +pragma experimental SMTChecker; +contract test { + function f(uint x) public pure { + assert(x > 0); + assert(x > 2); + assert(x > 4); + } +} \ No newline at end of file diff --git a/test/cmdlineTests/model_checker_timeout_chc/args b/test/cmdlineTests/model_checker_timeout_chc/args new file mode 100644 index 000000000..ff00f6407 --- /dev/null +++ b/test/cmdlineTests/model_checker_timeout_chc/args @@ -0,0 +1 @@ +--model-checker-engine chc --model-checker-timeout 1 diff --git a/test/cmdlineTests/model_checker_timeout_chc/err b/test/cmdlineTests/model_checker_timeout_chc/err new file mode 100644 index 000000000..d19b218f2 --- /dev/null +++ b/test/cmdlineTests/model_checker_timeout_chc/err @@ -0,0 +1,17 @@ +Warning: CHC: Assertion violation might happen here. + --> model_checker_timeout_chc/input.sol:6:3: + | +6 | assert(x > 0); + | ^^^^^^^^^^^^^ + +Warning: CHC: Assertion violation might happen here. + --> model_checker_timeout_chc/input.sol:7:3: + | +7 | assert(x > 2); + | ^^^^^^^^^^^^^ + +Warning: CHC: Assertion violation might happen here. + --> model_checker_timeout_chc/input.sol:8:3: + | +8 | assert(x > 4); + | ^^^^^^^^^^^^^ diff --git a/test/cmdlineTests/model_checker_timeout_chc/input.sol b/test/cmdlineTests/model_checker_timeout_chc/input.sol new file mode 100644 index 000000000..9c0134028 --- /dev/null +++ b/test/cmdlineTests/model_checker_timeout_chc/input.sol @@ -0,0 +1,10 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; +pragma experimental SMTChecker; +contract test { + function f(uint x) public pure { + assert(x > 0); + assert(x > 2); + assert(x > 4); + } +} \ No newline at end of file diff --git a/test/cmdlineTests/standard_model_checker_timeout_all/input.json b/test/cmdlineTests/standard_model_checker_timeout_all/input.json new file mode 100644 index 000000000..73e7f6641 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_timeout_all/input.json @@ -0,0 +1,14 @@ +{ + "language": "Solidity", + "sources": + { + "A": + { + "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract C { function f(uint x) public pure { assert(x > 0); } }" + } + }, + "modelCheckerSettings": + { + "timeout": 1 + } +} diff --git a/test/cmdlineTests/standard_model_checker_timeout_all/output.json b/test/cmdlineTests/standard_model_checker_timeout_all/output.json new file mode 100644 index 000000000..263414b68 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_timeout_all/output.json @@ -0,0 +1,37 @@ +{"auxiliaryInputRequested":{"smtlib2queries":{"0x067a0b3dedbdbea0177dfdac7720e0016881a66f25f487ed054daeecdca08a44":"(set-option :produce-models true) +(set-option :timeout 1) +(set-logic ALL) +(declare-fun |error_0| () Int) +(declare-fun |this_0| () Int) +(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) +(declare-fun |state_0| () |state_type|) +(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) +(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) +(declare-fun |tx_0| () |tx_type|) +(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) +(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) +(declare-fun |crypto_0| () |crypto_type|) +(declare-fun |x_4_0| () Int) +(declare-fun |expr_8_0| () Int) +(declare-fun |expr_9_0| () Int) +(declare-fun |expr_10_1| () Bool) + +(assert (and (and true (and (= expr_10_1 (> expr_8_0 expr_9_0)) (and (= expr_9_0 0) (and (= expr_8_0 x_4_0) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) true))))) (not expr_10_1))) +(declare-const |EVALEXPR_0| Int) +(assert (= |EVALEXPR_0| x_4_0)) +(check-sat) +(get-value (|EVALEXPR_0| )) +"}},"errors":[{"component":"general","errorCode":"6328","formattedMessage":"A:4:47: Warning: CHC: Assertion violation might happen here. +contract C { function f(uint x) public pure { assert(x > 0); } } + ^-----------^ +","message":"CHC: Assertion violation might happen here.","severity":"warning","sourceLocation":{"end":150,"file":"A","start":137},"type":"Warning"},{"component":"general","errorCode":"4661","formattedMessage":"A:4:47: Warning: BMC: Assertion violation happens here. +contract C { function f(uint x) public pure { assert(x > 0); } } + ^-----------^ +Counterexample: + x = 0 + +Callstack: + +","message":"BMC: Assertion violation happens here.","secondarySourceLocations":[{"message":"Counterexample: + x = 0 +"},{"message":"Callstack:"},{"message":""}],"severity":"warning","sourceLocation":{"end":150,"file":"A","start":137},"type":"Warning"}],"sources":{"A":{"id":0}}} diff --git a/test/cmdlineTests/standard_model_checker_timeout_bmc/input.json b/test/cmdlineTests/standard_model_checker_timeout_bmc/input.json new file mode 100644 index 000000000..0317e46a2 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_timeout_bmc/input.json @@ -0,0 +1,15 @@ +{ + "language": "Solidity", + "sources": + { + "A": + { + "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract C { function f(uint x) public pure { assert(x > 0); } }" + } + }, + "modelCheckerSettings": + { + "engine": "bmc", + "timeout": 1 + } +} diff --git a/test/cmdlineTests/standard_model_checker_timeout_bmc/output.json b/test/cmdlineTests/standard_model_checker_timeout_bmc/output.json new file mode 100644 index 000000000..aca766903 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_timeout_bmc/output.json @@ -0,0 +1,34 @@ +{"auxiliaryInputRequested":{"smtlib2queries":{"0x067a0b3dedbdbea0177dfdac7720e0016881a66f25f487ed054daeecdca08a44":"(set-option :produce-models true) +(set-option :timeout 1) +(set-logic ALL) +(declare-fun |error_0| () Int) +(declare-fun |this_0| () Int) +(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) +(declare-fun |state_0| () |state_type|) +(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) +(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) +(declare-fun |tx_0| () |tx_type|) +(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) +(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) +(declare-fun |crypto_0| () |crypto_type|) +(declare-fun |x_4_0| () Int) +(declare-fun |expr_8_0| () Int) +(declare-fun |expr_9_0| () Int) +(declare-fun |expr_10_1| () Bool) + +(assert (and (and true (and (= expr_10_1 (> expr_8_0 expr_9_0)) (and (= expr_9_0 0) (and (= expr_8_0 x_4_0) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) true))))) (not expr_10_1))) +(declare-const |EVALEXPR_0| Int) +(assert (= |EVALEXPR_0| x_4_0)) +(check-sat) +(get-value (|EVALEXPR_0| )) +"}},"errors":[{"component":"general","errorCode":"4661","formattedMessage":"A:4:47: Warning: BMC: Assertion violation happens here. +contract C { function f(uint x) public pure { assert(x > 0); } } + ^-----------^ +Counterexample: + x = 0 + +Callstack: + +","message":"BMC: Assertion violation happens here.","secondarySourceLocations":[{"message":"Counterexample: + x = 0 +"},{"message":"Callstack:"},{"message":""}],"severity":"warning","sourceLocation":{"end":150,"file":"A","start":137},"type":"Warning"}],"sources":{"A":{"id":0}}} diff --git a/test/cmdlineTests/standard_model_checker_timeout_chc/input.json b/test/cmdlineTests/standard_model_checker_timeout_chc/input.json new file mode 100644 index 000000000..fe490f665 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_timeout_chc/input.json @@ -0,0 +1,15 @@ +{ + "language": "Solidity", + "sources": + { + "A": + { + "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract C { function f(uint x) public pure { assert(x > 0); } }" + } + }, + "modelCheckerSettings": + { + "engine": "chc", + "timeout": 1 + } +} diff --git a/test/cmdlineTests/standard_model_checker_timeout_chc/output.json b/test/cmdlineTests/standard_model_checker_timeout_chc/output.json new file mode 100644 index 000000000..e68f8f62a --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_timeout_chc/output.json @@ -0,0 +1,4 @@ +{"errors":[{"component":"general","errorCode":"6328","formattedMessage":"A:4:47: Warning: CHC: Assertion violation might happen here. +contract C { function f(uint x) public pure { assert(x > 0); } } + ^-----------^ +","message":"CHC: Assertion violation might happen here.","severity":"warning","sourceLocation":{"end":150,"file":"A","start":137},"type":"Warning"}],"sources":{"A":{"id":0}}} diff --git a/test/cmdlineTests/standard_model_checker_timeout_wrong_key/input.json b/test/cmdlineTests/standard_model_checker_timeout_wrong_key/input.json new file mode 100644 index 000000000..7b1c26f56 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_timeout_wrong_key/input.json @@ -0,0 +1,15 @@ +{ + "language": "Solidity", + "sources": + { + "A": + { + "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract C { function f(uint x) public pure { assert(x > 0); } }" + } + }, + "modelCheckerSettings": + { + "engine": "chc", + "atimeout": 1 + } +} diff --git a/test/cmdlineTests/standard_model_checker_timeout_wrong_key/output.json b/test/cmdlineTests/standard_model_checker_timeout_wrong_key/output.json new file mode 100644 index 000000000..a02329045 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_timeout_wrong_key/output.json @@ -0,0 +1 @@ +{"errors":[{"component":"general","formattedMessage":"Unknown key \"atimeout\"","message":"Unknown key \"atimeout\"","severity":"error","type":"JSONError"}]} diff --git a/test/cmdlineTests/standard_model_checker_timeout_wrong_value/input.json b/test/cmdlineTests/standard_model_checker_timeout_wrong_value/input.json new file mode 100644 index 000000000..21a5a2e73 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_timeout_wrong_value/input.json @@ -0,0 +1,14 @@ +{ + "language": "Solidity", + "sources": + { + "A": + { + "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract C { function f(uint x) public pure { assert(x > 0); } }" + } + }, + "modelCheckerSettings": + { + "timeout": "asd" + } +} diff --git a/test/cmdlineTests/standard_model_checker_timeout_wrong_value/output.json b/test/cmdlineTests/standard_model_checker_timeout_wrong_value/output.json new file mode 100644 index 000000000..4bd0dde9a --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_timeout_wrong_value/output.json @@ -0,0 +1 @@ +{"errors":[{"component":"general","formattedMessage":"modelCheckerSettings.timeout must be an unsigned integer.","message":"modelCheckerSettings.timeout must be an unsigned integer.","severity":"error","type":"JSONError"}]}