Merge pull request #11261 from ethereum/smt_choose_target

[SMTChecker] Add option to choose contracts to be analyzed

libsolidity/formal/BMC.cpp

@@ -41,10 +41,9 @@ BMC::BMC(
 	smtutil::SMTSolverChoice _enabledSolvers,
 	ModelCheckerSettings const& _settings
 ):
-	SMTEncoder(_context),
+	SMTEncoder(_context, _settings),
 	m_interface(make_unique<smtutil::SMTPortfolio>(_smtlib2Responses, _smtCallback, _enabledSolvers, _settings.timeout)),
-	m_outerErrorReporter(_errorReporter),
-	m_settings(_settings)
+	m_outerErrorReporter(_errorReporter)
 {
 #if defined (HAVE_Z3) || defined (HAVE_CVC4)
 	if (_enabledSolvers.some())
@@ -838,7 +837,7 @@ void BMC::addVerificationTarget(
 	Expression const* _expression
 )
 {
-	if (!m_settings.targets.has(_type) || (m_currentContract && !m_currentContract->canBeDeployed()))
+	if (!m_settings.targets.has(_type) || (m_currentContract && !shouldAnalyze(*m_currentContract)))
 		return;
 
 	BMCVerificationTarget target{

libsolidity/formal/BMC.h

@@ -193,8 +193,6 @@ private:
 
 	/// Targets that were already proven.
 	std::map<ASTNode const*, std::set<VerificationTargetType>> m_solvedTargets;
-
-	ModelCheckerSettings const& m_settings;
 };
 
 }

libsolidity/formal/CHC.cpp

@@ -59,10 +59,9 @@ CHC::CHC(
 	SMTSolverChoice _enabledSolvers,
 	ModelCheckerSettings const& _settings
 ):
-	SMTEncoder(_context),
+	SMTEncoder(_context, _settings),
 	m_outerErrorReporter(_errorReporter),
-	m_enabledSolvers(_enabledSolvers),
-	m_settings(_settings)
+	m_enabledSolvers(_enabledSolvers)
 {
 	bool usesZ3 = _enabledSolvers.z3;
 #ifdef HAVE_Z3
@@ -198,7 +197,7 @@ void CHC::endVisit(ContractDefinition const& _contract)
 	setCurrentBlock(*m_constructorSummaries.at(&_contract));
 
 	solAssert(&_contract == m_currentContract, "");
-	if (_contract.canBeDeployed())
+	if (shouldAnalyze(_contract))
 	{
 		auto constructor = _contract.constructor();
 		auto txConstraints = state().txTypeConstraints();
@@ -283,7 +282,7 @@ void CHC::endVisit(FunctionDefinition const& _function)
 		!_function.isConstructor() &&
 		_function.isPublic() &&
 		contractFunctions(*m_currentContract).count(&_function) &&
-		m_currentContract->canBeDeployed()
+		shouldAnalyze(*m_currentContract)
 	)
 	{
 		auto sum = summary(_function);

libsolidity/formal/CHC.h

@@ -374,8 +374,6 @@ private:
 
 	/// SMT solvers that are chosen at runtime.
 	smtutil::SMTSolverChoice m_enabledSolvers;
-
-	ModelCheckerSettings const& m_settings;
 };
 
 }

libsolidity/formal/ModelChecker.cpp

@@ -22,6 +22,7 @@
 #endif
 
 #include <range/v3/algorithm/any_of.hpp>
+#include <range/v3/view.hpp>
 
 using namespace std;
 using namespace solidity;
@@ -54,6 +55,38 @@ void ModelChecker::enableAllEnginesIfPragmaPresent(vector<shared_ptr<SourceUnit>
 		m_settings.engine = ModelCheckerEngine::All();
 }
 
+void ModelChecker::checkRequestedSourcesAndContracts(vector<shared_ptr<SourceUnit>> const& _sources)
+{
+	map<string, set<string>> exist;
+	for (auto const& source: _sources)
+		for (auto node: source->nodes())
+			if (auto contract = dynamic_pointer_cast<ContractDefinition>(node))
+				exist[contract->sourceUnitName()].insert(contract->name());
+
+	// Requested sources
+	for (auto const& sourceName: m_settings.contracts.contracts | ranges::views::keys)
+	{
+		if (!exist.count(sourceName))
+		{
+			m_errorReporter.warning(
+				9134_error,
+				SourceLocation(),
+				"Requested source \"" + sourceName + "\" does not exist."
+			);
+			continue;
+		}
+		auto const& source = exist.at(sourceName);
+		// Requested contracts in source `s`.
+		for (auto const& contract: m_settings.contracts.contracts.at(sourceName))
+			if (!source.count(contract))
+				m_errorReporter.warning(
+					7400_error,
+					SourceLocation(),
+					"Requested contract \"" + contract + "\" does not exist in source \"" + sourceName + "\"."
+				);
+	}
+}
+
 void ModelChecker::analyze(SourceUnit const& _source)
 {
 	// TODO This should be removed for 0.9.0.

libsolidity/formal/ModelChecker.h

@@ -58,6 +58,10 @@ public:
 	// TODO This should be removed for 0.9.0.
 	void enableAllEnginesIfPragmaPresent(std::vector<std::shared_ptr<SourceUnit>> const& _sources);
 
+	/// Generates error messages if the requested sources and contracts
+	/// do not exist.
+	void checkRequestedSourcesAndContracts(std::vector<std::shared_ptr<SourceUnit>> const& _sources);
+
 	void analyze(SourceUnit const& _sources);
 
 	/// This is used if the SMT solver is not directly linked into this binary.

libsolidity/formal/ModelCheckerSettings.cpp

@@ -62,3 +62,20 @@ bool ModelCheckerTargets::setFromString(string const& _target)
 	targets.insert(targetStrings.at(_target));
 	return true;
 }
+
+std::optional<ModelCheckerContracts> ModelCheckerContracts::fromString(string const& _contracts)
+{
+	map<string, set<string>> chosen;
+	if (_contracts == "default")
+		return ModelCheckerContracts::Default();
+
+	for (auto&& sourceContract: _contracts | views::split(',') | ranges::to<vector<string>>())
+	{
+		auto&& names = sourceContract | views::split(':') | ranges::to<vector<string>>();
+		if (names.size() != 2 || names.at(0).empty() || names.at(1).empty())
+			return {};
+		chosen[names.at(0)].insert(names.at(1));
+	}
+
+	return ModelCheckerContracts{chosen};
+}

libsolidity/formal/ModelCheckerSettings.h

@@ -26,6 +26,33 @@
 namespace solidity::frontend
 {
 
+struct ModelCheckerContracts
+{
+	/// By default all contracts are analyzed.
+	static ModelCheckerContracts Default() { return {}; }
+
+	/// Parses a string of the form <path>:<contract>,<path>:contract,...
+	/// and returns nullopt if a path or contract name is empty.
+	static std::optional<ModelCheckerContracts> fromString(std::string const& _contracts);
+
+	/// @returns true if all contracts should be analyzed.
+	bool isDefault() const { return contracts.empty(); }
+
+	bool has(std::string const& _source) const { return contracts.count(_source); }
+	bool has(std::string const& _source, std::string const& _contract) const
+	{
+		return has(_source) && contracts.at(_source).count(_contract);
+	}
+
+	/// Represents which contracts should be analyzed by the SMTChecker
+	/// as the most derived.
+	/// The key is the source file. If the map is empty, all sources must be analyzed.
+	/// For each source, contracts[source] represents the contracts in that source
+	/// that should be analyzed.
+	/// If the set of contracts is empty, all contracts in that source should be analyzed.
+	std::map<std::string, std::set<std::string>> contracts;
+};
+
 struct ModelCheckerEngine
 {
 	bool bmc = false;
@@ -58,7 +85,7 @@ enum class VerificationTargetType { ConstantCondition, Underflow, Overflow, Unde
 
 struct ModelCheckerTargets
 {
-	static ModelCheckerTargets All() { return *fromString("default"); }
+	static ModelCheckerTargets Default() { return *fromString("default"); }
 
 	static std::optional<ModelCheckerTargets> fromString(std::string const& _targets);
 
@@ -75,8 +102,9 @@ struct ModelCheckerTargets
 
 struct ModelCheckerSettings
 {
+	ModelCheckerContracts contracts = ModelCheckerContracts::Default();
 	ModelCheckerEngine engine = ModelCheckerEngine::None();
-	ModelCheckerTargets targets = ModelCheckerTargets::All();
+	ModelCheckerTargets targets = ModelCheckerTargets::Default();
 	std::optional<unsigned> timeout;
 };
 

libsolidity/formal/SMTEncoder.cpp

@@ -43,9 +43,13 @@ using namespace solidity::util;
 using namespace solidity::langutil;
 using namespace solidity::frontend;
 
-SMTEncoder::SMTEncoder(smt::EncodingContext& _context):
+SMTEncoder::SMTEncoder(
+	smt::EncodingContext& _context,
+	ModelCheckerSettings const& _settings
+):
 	m_errorReporter(m_smtErrors),
-	m_context(_context)
+	m_context(_context),
+	m_settings(_settings)
 {
 }
 
@@ -992,6 +996,15 @@ void SMTEncoder::visitPublicGetter(FunctionCall const& _funCall)
 	}
 }
 
+bool SMTEncoder::shouldAnalyze(ContractDefinition const& _contract) const
+{
+	if (!_contract.canBeDeployed())
+		return false;
+
+	return m_settings.contracts.isDefault() ||
+		m_settings.contracts.has(_contract.sourceUnitName(), _contract.name());
+}
+
 void SMTEncoder::visitTypeConversion(FunctionCall const& _funCall)
 {
 	solAssert(*_funCall.annotation().kind == FunctionCallKind::TypeConversion, "");

libsolidity/formal/SMTEncoder.h

@@ -51,7 +51,10 @@ namespace solidity::frontend
 class SMTEncoder: public ASTConstVisitor
 {
 public:
-	SMTEncoder(smt::EncodingContext& _context);
+	SMTEncoder(
+		smt::EncodingContext& _context,
+		ModelCheckerSettings const& _settings
+	);
 
 	/// @returns true if engine should proceed with analysis.
 	bool analyze(SourceUnit const& _sources);
@@ -203,6 +206,10 @@ protected:
 	void visitFunctionIdentifier(Identifier const& _identifier);
 	void visitPublicGetter(FunctionCall const& _funCall);
 
+	/// @returns true if @param _contract is set for analysis in the settings
+	/// and it is not abstract.
+	bool shouldAnalyze(ContractDefinition const& _contract) const;
+
 	bool isPublicGetter(Expression const& _expr);
 
 	/// Encodes a modifier or function body according to the modifier
@@ -455,6 +462,8 @@ protected:
 	/// Stores the context of the encoding.
 	smt::EncodingContext& m_context;
 
+	ModelCheckerSettings const& m_settings;
+
 	smt::SymbolicState& state();
 };
 

libsolidity/interface/CompilerStack.cpp

@@ -547,7 +547,9 @@ bool CompilerStack::analyze()
 		if (noErrors)
 		{
 			ModelChecker modelChecker(m_errorReporter, m_smtlib2Responses, m_modelCheckerSettings, m_readFile, m_enabledSMTSolvers);
-			modelChecker.enableAllEnginesIfPragmaPresent(applyMap(m_sourceOrder, [](Source const* _source) { return _source->ast; }));
+			auto allSources = applyMap(m_sourceOrder, [](Source const* _source) { return _source->ast; });
+			modelChecker.enableAllEnginesIfPragmaPresent(allSources);
+			modelChecker.checkRequestedSourcesAndContracts(allSources);
 			for (Source const* source: m_sourceOrder)
 				if (source->ast)
 					modelChecker.analyze(*source->ast);

libsolidity/interface/StandardCompiler.cpp

@@ -435,7 +435,7 @@ std::optional<Json::Value> checkSettingsKeys(Json::Value const& _input)
 
 std::optional<Json::Value> checkModelCheckerSettingsKeys(Json::Value const& _input)
 {
-	static set<string> keys{"engine", "targets", "timeout"};
+	static set<string> keys{"contracts", "engine", "targets", "timeout"};
 	return checkKeys(_input, keys, "modelChecker");
 }
 
@@ -901,6 +901,37 @@ std::variant<StandardCompiler::InputsAndSettings, Json::Value> StandardCompiler:
 	if (auto result = checkModelCheckerSettingsKeys(modelCheckerSettings))
 		return *result;
 
+	if (modelCheckerSettings.isMember("contracts"))
+	{
+		auto const& sources = modelCheckerSettings["contracts"];
+		if (!sources.isObject() && !sources.isNull())
+			return formatFatalError("JSONError", "settings.modelChecker.contracts is not a JSON object.");
+
+		map<string, set<string>> sourceContracts;
+		for (auto const& source: sources.getMemberNames())
+		{
+			if (source.empty())
+				return formatFatalError("JSONError", "Source name cannot be empty.");
+
+			auto const& contracts = sources[source];
+			if (!contracts.isArray())
+				return formatFatalError("JSONError", "Source contracts must be an array.");
+
+			for (auto const& contract: contracts)
+			{
+				if (!contract.isString())
+					return formatFatalError("JSONError", "Every contract in settings.modelChecker.contracts must be a string.");
+				if (contract.asString().empty())
+					return formatFatalError("JSONError", "Contract name cannot be empty.");
+				sourceContracts[source].insert(contract.asString());
+			}
+
+			if (sourceContracts[source].empty())
+				return formatFatalError("JSONError", "Source contracts must be a non-empty array.");
+		}
+		ret.modelCheckerSettings.contracts = {move(sourceContracts)};
+	}
+
 	if (modelCheckerSettings.isMember("engine"))
 	{
 		if (!modelCheckerSettings["engine"].isString())