Merge pull request #10181 from ethereum/smt_user_timeout

[SMTChecker] User timeout option

Changelog.md

@@ -6,6 +6,8 @@ Language Features:
 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:

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
       }
     }
 

libsmtutil/CHCSmtLib2Interface.cpp

@@ -36,11 +36,13 @@ using namespace solidity::frontend;
 using namespace solidity::smtutil;
 
 CHCSmtLib2Interface::CHCSmtLib2Interface(
-	map<h256, string> const& _queryResponses,
-	ReadCallback::Callback const& _smtCallback
+	map<h256, string> _queryResponses,
+	ReadCallback::Callback _smtCallback,
+	optional<unsigned> _queryTimeout
 ):
-	m_smtlib2(make_unique<SMTLib2Interface>(_queryResponses, _smtCallback)),
-	m_queryResponses(_queryResponses),
+	CHCSolverInterface(_queryTimeout),
+	m_smtlib2(make_unique<SMTLib2Interface>(_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)

libsmtutil/CHCSmtLib2Interface.h

@@ -33,8 +33,9 @@ class CHCSmtLib2Interface: public CHCSolverInterface
 {
 public:
 	explicit CHCSmtLib2Interface(
-		std::map<util::h256, std::string> const& _queryResponses,
-		frontend::ReadCallback::Callback const& _smtCallback
+		std::map<util::h256, std::string> _queryResponses = {},
+		frontend::ReadCallback::Callback _smtCallback = {},
+		std::optional<unsigned> _queryTimeout = {}
 	);
 
 	void reset();

libsmtutil/CHCSolverInterface.h

@@ -33,6 +33,8 @@ namespace solidity::smtutil
 class CHCSolverInterface
 {
 public:
+	CHCSolverInterface(std::optional<unsigned> _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<CheckResult, CexGraph> query(
 		Expression const& _expr
 	) = 0;
+
+protected:
+	std::optional<unsigned> m_queryTimeout;
 };
 
 }

libsmtutil/CVC4Interface.cpp

@@ -27,7 +27,8 @@ using namespace solidity;
 using namespace solidity::util;
 using namespace solidity::smtutil;
 
-CVC4Interface::CVC4Interface():
+CVC4Interface::CVC4Interface(optional<unsigned> _queryTimeout):
+	SolverInterface(_queryTimeout),
 	m_solver(&m_context)
 {
 	reset();
@@ -38,6 +39,9 @@ void CVC4Interface::reset()
 	m_variables.clear();
 	m_solver.reset();
 	m_solver.setOption("produce-models", true);
+	if (m_queryTimeout)
+		m_solver.setTimeLimit(*m_queryTimeout);
+	else
 		m_solver.setResourceLimit(resourceLimit);
 }
 

libsmtutil/CVC4Interface.h

@@ -40,7 +40,7 @@ namespace solidity::smtutil
 class CVC4Interface: public SolverInterface, public boost::noncopyable
 {
 public:
-	CVC4Interface();
+	CVC4Interface(std::optional<unsigned> _queryTimeout = {});
 
 	void reset() override;
 

libsmtutil/SMTLib2Interface.cpp

@@ -39,8 +39,10 @@ using namespace solidity::smtutil;
 
 SMTLib2Interface::SMTLib2Interface(
 	map<h256, string> _queryResponses,
-	ReadCallback::Callback _smtCallback
+	ReadCallback::Callback _smtCallback,
+	optional<unsigned> _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)");
 }
 

libsmtutil/SMTLib2Interface.h

@@ -40,7 +40,8 @@ class SMTLib2Interface: public SolverInterface, public boost::noncopyable
 public:
 	explicit SMTLib2Interface(
 		std::map<util::h256, std::string> _queryResponses = {},
-		frontend::ReadCallback::Callback _smtCallback = {}
+		frontend::ReadCallback::Callback _smtCallback = {},
+		std::optional<unsigned> _queryTimeout = {}
 	);
 
 	void reset() override;

libsmtutil/SMTPortfolio.cpp

@@ -35,17 +35,19 @@ using namespace solidity::smtutil;
 SMTPortfolio::SMTPortfolio(
 	map<h256, string> _smtlib2Responses,
 	frontend::ReadCallback::Callback _smtCallback,
-	[[maybe_unused]] SMTSolverChoice _enabledSolvers
-)
+	[[maybe_unused]] SMTSolverChoice _enabledSolvers,
+	optional<unsigned> _queryTimeout
+):
+	SolverInterface(_queryTimeout)
 {
-	m_solvers.emplace_back(make_unique<SMTLib2Interface>(move(_smtlib2Responses), move(_smtCallback)));
+	m_solvers.emplace_back(make_unique<SMTLib2Interface>(move(_smtlib2Responses), move(_smtCallback), m_queryTimeout));
 #ifdef HAVE_Z3
 	if (_enabledSolvers.z3)
-		m_solvers.emplace_back(make_unique<Z3Interface>());
+		m_solvers.emplace_back(make_unique<Z3Interface>(m_queryTimeout));
 #endif
 #ifdef HAVE_CVC4
 	if (_enabledSolvers.cvc4)
-		m_solvers.emplace_back(make_unique<CVC4Interface>());
+		m_solvers.emplace_back(make_unique<CVC4Interface>(m_queryTimeout));
 #endif
 }
 

libsmtutil/SMTPortfolio.h

@@ -42,7 +42,8 @@ public:
 	SMTPortfolio(
 		std::map<util::h256, std::string> _smtlib2Responses = {},
 		frontend::ReadCallback::Callback _smtCallback = {},
-		SMTSolverChoice _enabledSolvers = SMTSolverChoice::All()
+		SMTSolverChoice _enabledSolvers = SMTSolverChoice::All(),
+		std::optional<unsigned> _queryTimeout = {}
 	);
 
 	void reset() override;

libsmtutil/SolverInterface.h

@@ -374,6 +374,8 @@ DEV_SIMPLE_EXCEPTION(SolverError);
 class SolverInterface
 {
 public:
+	SolverInterface(std::optional<unsigned> _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<unsigned> m_queryTimeout;
 };
 
 }

libsmtutil/Z3CHCInterface.cpp

@@ -27,13 +27,18 @@ using namespace std;
 using namespace solidity;
 using namespace solidity::smtutil;
 
-Z3CHCInterface::Z3CHCInterface():
-	m_z3Interface(make_unique<Z3Interface>()),
+Z3CHCInterface::Z3CHCInterface(optional<unsigned> _queryTimeout):
+	CHCSolverInterface(_queryTimeout),
+	m_z3Interface(make_unique<Z3Interface>(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);
+
+	if (m_queryTimeout)
+		m_context->set("timeout", int(*m_queryTimeout));
+	else
 		z3::set_param("rlimit", Z3Interface::resourceLimit);
 
 	setSpacerOptions();
@@ -97,7 +102,13 @@ pair<CheckResult, CHCSolverInterface::CexGraph> Z3CHCInterface::query(Expression
 	}
 	catch (z3::exception const& _err)
 	{
-		if (_err.msg() == string("max. resource limit exceeded"))
+		set<string> 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;

libsmtutil/Z3CHCInterface.h

@@ -33,7 +33,7 @@ namespace solidity::smtutil
 class Z3CHCInterface: public CHCSolverInterface
 {
 public:
-	Z3CHCInterface();
+	Z3CHCInterface(std::optional<unsigned> _queryTimeout = {});
 
 	/// Forwards variable declaration to Z3Interface.
 	void declareVariable(std::string const& _name, SortPointer const& _sort) override;

libsmtutil/Z3Interface.cpp

@@ -27,11 +27,16 @@ using namespace std;
 using namespace solidity::smtutil;
 using namespace solidity::util;
 
-Z3Interface::Z3Interface():
+Z3Interface::Z3Interface(std::optional<unsigned> _queryTimeout):
+	SolverInterface(_queryTimeout),
 	m_solver(m_context)
 {
 	// These need to be set globally.
 	z3::set_param("rewriter.pull_cheap_ite", true);
+
+	if (m_queryTimeout)
+		m_context.set("timeout", int(*m_queryTimeout));
+	else
 		z3::set_param("rlimit", resourceLimit);
 }
 
@@ -104,8 +109,18 @@ pair<CheckResult, vector<string>> Z3Interface::check(vector<Expression> const& _
 				values.push_back(util::toString(m.eval(toZ3Expr(e))));
 		}
 	}
-	catch (z3::exception const&)
+	catch (z3::exception const& _err)
 	{
+		set<string> 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();
 	}

libsmtutil/Z3Interface.h

@@ -28,7 +28,7 @@ namespace solidity::smtutil
 class Z3Interface: public SolverInterface, public boost::noncopyable
 {
 public:
-	Z3Interface();
+	Z3Interface(std::optional<unsigned> _queryTimeout = {});
 
 	void reset() override;
 

libsolidity/formal/BMC.cpp

@@ -34,10 +34,11 @@ BMC::BMC(
 	ErrorReporter& _errorReporter,
 	map<h256, string> const& _smtlib2Responses,
 	ReadCallback::Callback const& _smtCallback,
-	smtutil::SMTSolverChoice _enabledSolvers
+	smtutil::SMTSolverChoice _enabledSolvers,
+	optional<unsigned> _timeout
 ):
 	SMTEncoder(_context),
-	m_interface(make_unique<smtutil::SMTPortfolio>(_smtlib2Responses, _smtCallback, _enabledSolvers)),
+	m_interface(make_unique<smtutil::SMTPortfolio>(_smtlib2Responses, _smtCallback, _enabledSolvers, _timeout)),
 	m_outerErrorReporter(_errorReporter)
 {
 #if defined (HAVE_Z3) || defined (HAVE_CVC4)

libsolidity/formal/BMC.h

@@ -61,7 +61,8 @@ public:
 		langutil::ErrorReporter& _errorReporter,
 		std::map<h256, std::string> const& _smtlib2Responses,
 		ReadCallback::Callback const& _smtCallback,
-		smtutil::SMTSolverChoice _enabledSolvers
+		smtutil::SMTSolverChoice _enabledSolvers,
+		std::optional<unsigned> timeout
 	);
 
 	void analyze(SourceUnit const& _sources, std::map<ASTNode const*, std::set<VerificationTarget::Type>> _solvedTargets);

libsolidity/formal/CHC.cpp

@@ -49,18 +49,20 @@ CHC::CHC(
 	ErrorReporter& _errorReporter,
 	[[maybe_unused]] map<util::h256, string> const& _smtlib2Responses,
 	[[maybe_unused]] ReadCallback::Callback const& _smtCallback,
-	SMTSolverChoice _enabledSolvers
+	SMTSolverChoice _enabledSolvers,
+	optional<unsigned> _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<CHCSmtLib2Interface>(_smtlib2Responses, _smtCallback);
+		m_interface = make_unique<CHCSmtLib2Interface>(_smtlib2Responses, _smtCallback, m_queryTimeout);
 }
 
 void CHC::analyze(SourceUnit const& _source)
@@ -699,7 +701,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<Z3CHCInterface const*>(m_interface.get());
 		solAssert(z3Interface, "");
 		m_context.setSolver(z3Interface->z3Interface());

libsolidity/formal/CHC.h

@@ -55,7 +55,8 @@ public:
 		langutil::ErrorReporter& _errorReporter,
 		std::map<util::h256, std::string> const& _smtlib2Responses,
 		ReadCallback::Callback const& _smtCallback,
-		smtutil::SMTSolverChoice _enabledSolvers
+		smtutil::SMTSolverChoice _enabledSolvers,
+		std::optional<unsigned> 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<unsigned> m_queryTimeout;
 };
 
 }

libsolidity/formal/ModelChecker.cpp

@@ -27,14 +27,14 @@ using namespace solidity::frontend;
 ModelChecker::ModelChecker(
 	ErrorReporter& _errorReporter,
 	map<h256, string> 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);
 }
 

libsolidity/formal/ModelChecker.h

@@ -71,6 +71,12 @@ struct ModelCheckerEngine
 	}
 };
 
+struct ModelCheckerSettings
+{
+	ModelCheckerEngine engine = ModelCheckerEngine::All();
+	std::optional<unsigned> timeout;
+};
+
 class ModelChecker
 {
 public:
@@ -79,7 +85,7 @@ public:
 	ModelChecker(
 		langutil::ErrorReporter& _errorReporter,
 		std::map<solidity::util::h256, std::string> 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;

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);

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<std::string, std::set<std::string>> m_requestedContractNames;
 	bool m_generateEvmBytecode = true;

libsolidity/interface/StandardCompiler.cpp

@@ -420,7 +420,7 @@ std::optional<Json::Value> checkSettingsKeys(Json::Value const& _input)
 
 std::optional<Json::Value> checkModelCheckerSettingsKeys(Json::Value const& _input)
 {
-	static set<string> keys{"engine"};
+	static set<string> keys{"engine", "timeout"};
 	return checkKeys(_input, keys, "modelCheckerSettings");
 }
 
@@ -885,7 +885,14 @@ std::variant<StandardCompiler::InputsAndSettings, Json::Value> StandardCompiler:
 		std::optional<ModelCheckerEngine> 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));

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

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<string>()->value_name("all,bmc,chc,none")->default_value("all"),
 			"Select model checker engine."
 		)
+		(
+			g_strModelCheckerTimeout.c_str(),
+			po::value<unsigned>()->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<unsigned>();
+
 	m_compiler = make_unique<CompilerStack>(fileReader);
 
 	unique_ptr<SourceReferenceFormatter> 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);
 

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.

test/cmdlineTests/model_checker_timeout_all/args

@@ -0,0 +1 @@
+--model-checker-timeout 1

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:

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);
+    }
+}

test/cmdlineTests/model_checker_timeout_bmc/args

@@ -0,0 +1 @@
+--model-checker-engine bmc --model-checker-timeout 1

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:

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);
+    }
+}

test/cmdlineTests/model_checker_timeout_chc/args

@@ -0,0 +1 @@
+--model-checker-engine chc --model-checker-timeout 1

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);
+  | 		^^^^^^^^^^^^^

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);
+    }
+}

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
+	}
+}

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}}}

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
+	}
+}

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}}}

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
+	}
+}

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}}}

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
+	}
+}

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"}]}

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"
+	}
+}

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"}]}