Merge pull request #10036 from ethereum/smt_cli_option

Add CLI option to choose model checker engine

libsolidity/formal/BMC.cpp

@@ -836,7 +836,7 @@ void BMC::checkCondition(
 			"\nNote that some information is erased after the execution of loops.\n"
 			"You can re-introduce information using require().";
 	if (m_externalFunctionCallHappened)
-		extraComment+=
+		extraComment +=
 			"\nNote that external function calls are not inlined,"
 			" even if the source code of the function is available."
 			" This is due to the possibility that the actual called contract"
@@ -854,7 +854,7 @@ void BMC::checkCondition(
 		if (_callStack.size())
 		{
 			std::ostringstream modelMessage;
-			modelMessage << "\nCounterexample:\n";
+			modelMessage << "Counterexample:\n";
 			solAssert(values.size() == expressionNames.size(), "");
 			map<string, string> sortedModel;
 			for (size_t i = 0; i < values.size(); ++i)
@@ -863,6 +863,7 @@ void BMC::checkCondition(
 
 			for (auto const& eval: sortedModel)
 				modelMessage << "  " << eval.first << " = " << eval.second << "\n";
+
 			m_errorReporter.warning(
 				_errorHappens,
 				_location,

libsolidity/formal/CHC.cpp

@@ -1298,7 +1298,7 @@ void CHC::checkAndReportTarget(
 				_errorReporterId,
 				_scope->location(),
 				"CHC: " + _satMsg,
-				SecondarySourceLocation().append("\nCounterexample:\n" + *cex, SourceLocation{})
+				SecondarySourceLocation().append("Counterexample:\n" + *cex, SourceLocation{})
 			);
 		else
 			m_outerErrorReporter.warning(
@@ -1402,9 +1402,13 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
 			}
 		}
 		else
+		{
+			auto modelMsg = formatVariableModel(*stateVars, stateValues, ", ");
 			/// We report the state after every tx in the trace except for the last, which is reported
 			/// first in the code above.
-			path.emplace_back("State: " + formatVariableModel(*stateVars, stateValues, ", "));
+			if (!modelMsg.empty())
+				path.emplace_back("State: " + modelMsg);
+		}
 
 		string txCex = summaryPredicate->formatSummaryCall(summaryArgs);
 		path.emplace_back(txCex);

libsolidity/formal/ModelChecker.cpp

@@ -27,9 +27,11 @@ using namespace solidity::frontend;
 ModelChecker::ModelChecker(
 	ErrorReporter& _errorReporter,
 	map<h256, string> const& _smtlib2Responses,
+	ModelCheckerEngine _engine,
 	ReadCallback::Callback const& _smtCallback,
 	smtutil::SMTSolverChoice _enabledSolvers
 ):
+	m_engine(_engine),
 	m_context(),
 	m_bmc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, _enabledSolvers),
 	m_chc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, _enabledSolvers)
@@ -41,13 +43,15 @@ void ModelChecker::analyze(SourceUnit const& _source)
 	if (!_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker))
 		return;
 
-	m_chc.analyze(_source);
+	if (m_engine.chc)
+		m_chc.analyze(_source);
 
 	auto solvedTargets = m_chc.safeTargets();
 	for (auto const& target: m_chc.unsafeTargets())
 		solvedTargets[target.first] += target.second;
 
-	m_bmc.analyze(_source, solvedTargets);
+	if (m_engine.bmc)
+		m_bmc.analyze(_source, solvedTargets);
 }
 
 vector<string> ModelChecker::unhandledQueries()

libsolidity/formal/ModelChecker.h

@@ -32,6 +32,8 @@
 #include <libsmtutil/SolverInterface.h>
 #include <liblangutil/ErrorReporter.h>
 
+#include <optional>
+
 namespace solidity::langutil
 {
 class ErrorReporter;
@@ -41,6 +43,34 @@ struct SourceLocation;
 namespace solidity::frontend
 {
 
+struct ModelCheckerEngine
+{
+	bool bmc = false;
+	bool chc = false;
+
+	static constexpr ModelCheckerEngine All() { return {true, true}; }
+	static constexpr ModelCheckerEngine BMC() { return {true, false}; }
+	static constexpr ModelCheckerEngine CHC() { return {false, true}; }
+	static constexpr ModelCheckerEngine None() { return {false, false}; }
+
+	bool none() const { return !any(); }
+	bool any() const { return bmc || chc; }
+	bool all() const { return bmc && chc; }
+
+	static std::optional<ModelCheckerEngine> fromString(std::string const& _engine)
+	{
+		static std::map<std::string, ModelCheckerEngine> engineMap{
+			{"all", All()},
+			{"bmc", BMC()},
+			{"chc", CHC()},
+			{"none", None()}
+		};
+		if (engineMap.count(_engine))
+			return engineMap.at(_engine);
+		return {};
+	}
+};
+
 class ModelChecker
 {
 public:
@@ -49,6 +79,7 @@ public:
 	ModelChecker(
 		langutil::ErrorReporter& _errorReporter,
 		std::map<solidity::util::h256, std::string> const& _smtlib2Responses,
+		ModelCheckerEngine _engine = ModelCheckerEngine::All(),
 		ReadCallback::Callback const& _smtCallback = ReadCallback::Callback(),
 		smtutil::SMTSolverChoice _enabledSolvers = smtutil::SMTSolverChoice::All()
 	);
@@ -64,6 +95,8 @@ public:
 	static smtutil::SMTSolverChoice availableSolvers();
 
 private:
+	ModelCheckerEngine m_engine;
+
 	/// Stores the context of the encoding.
 	smt::EncodingContext m_context;
 

libsolidity/formal/SMTEncoder.cpp

@@ -2132,7 +2132,7 @@ SecondarySourceLocation SMTEncoder::callStackMessage(vector<CallStackEntry> cons
 {
 	SecondarySourceLocation callStackLocation;
 	solAssert(!_callStack.empty(), "");
-	callStackLocation.append("Callstack: ", SourceLocation());
+	callStackLocation.append("Callstack:", SourceLocation());
 	for (auto const& call: _callStack | boost::adaptors::reversed)
 		if (call.second)
 			callStackLocation.append("", call.second->location());

libsolidity/interface/CompilerStack.cpp

@@ -87,6 +87,7 @@ 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}
 {
@@ -138,6 +139,13 @@ void CompilerStack::setEVMVersion(langutil::EVMVersion _version)
 	m_evmVersion = _version;
 }
 
+void CompilerStack::setModelCheckerEngine(ModelCheckerEngine _engine)
+{
+	if (m_stackState >= ParsedAndImported)
+		BOOST_THROW_EXCEPTION(CompilerError() << errinfo_comment("Must set enabled model checking engines before parsing."));
+	m_modelCheckerEngine = _engine;
+}
+
 void CompilerStack::setSMTSolverChoice(smtutil::SMTSolverChoice _enabledSMTSolvers)
 {
 	if (m_stackState >= ParsedAndImported)
@@ -207,6 +215,7 @@ void CompilerStack::reset(bool _keepSettings)
 		m_remappings.clear();
 		m_libraries.clear();
 		m_evmVersion = langutil::EVMVersion();
+		m_modelCheckerEngine = ModelCheckerEngine::All();
 		m_enabledSMTSolvers = smtutil::SMTSolverChoice::All();
 		m_generateIR = false;
 		m_generateEwasm = false;
@@ -443,7 +452,7 @@ bool CompilerStack::analyze()
 
 		if (noErrors)
 		{
-			ModelChecker modelChecker(m_errorReporter, m_smtlib2Responses, m_readFile, m_enabledSMTSolvers);
+			ModelChecker modelChecker(m_errorReporter, m_smtlib2Responses, m_modelCheckerEngine, m_readFile, m_enabledSMTSolvers);
 			for (Source const* source: m_sourceOrder)
 				if (source->ast)
 					modelChecker.analyze(*source->ast);

libsolidity/interface/CompilerStack.h

@@ -29,6 +29,8 @@
 #include <libsolidity/interface/Version.h>
 #include <libsolidity/interface/DebugSettings.h>
 
+#include <libsolidity/formal/ModelChecker.h>
+
 #include <libsmtutil/SolverInterface.h>
 
 #include <liblangutil/ErrorReporter.h>
@@ -165,6 +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 which SMT solvers should be enabled.
 	void setSMTSolverChoice(smtutil::SMTSolverChoice _enabledSolvers);
 
@@ -452,6 +456,7 @@ private:
 	RevertStrings m_revertStrings = RevertStrings::Default;
 	State m_stopAfter = State::CompilationSuccessful;
 	langutil::EVMVersion m_evmVersion;
+	ModelCheckerEngine m_modelCheckerEngine;
 	smtutil::SMTSolverChoice m_enabledSMTSolvers;
 	std::map<std::string, std::set<std::string>> m_requestedContractNames;
 	bool m_generateEvmBytecode = true;

libsolidity/interface/StandardCompiler.cpp

@@ -414,7 +414,7 @@ std::optional<Json::Value> checkAuxiliaryInputKeys(Json::Value const& _input)
 
 std::optional<Json::Value> checkSettingsKeys(Json::Value const& _input)
 {
-	static set<string> keys{"parserErrorRecovery", "debug", "evmVersion", "libraries", "metadata", "optimizer", "outputSelection", "remappings", "stopAfter"};
+	static set<string> keys{"parserErrorRecovery", "debug", "evmVersion", "libraries", "metadata", "optimizer", "outputSelection", "remappings", "stopAfter", "modelCheckerEngine"};
 	return checkKeys(_input, keys, "settings");
 }
 
@@ -527,6 +527,7 @@ std::optional<Json::Value> checkOutputSelection(Json::Value const& _outputSelect
 
 	return std::nullopt;
 }
+
 /// Validates the optimizer settings and returns them in a parsed object.
 /// On error returns the json-formatted error message.
 std::variant<OptimiserSettings, Json::Value> parseOptimizerSettings(Json::Value const& _jsonInput)
@@ -866,6 +867,16 @@ std::variant<StandardCompiler::InputsAndSettings, Json::Value> StandardCompiler:
 			"Requested output selection conflicts with \"settings.stopAfter\"."
 		);
 
+	if (settings.isMember("modelCheckerEngine"))
+	{
+		if (!settings["modelCheckerEngine"].isString())
+			return formatFatalError("JSONError", "modelCheckerEngine must be a string.");
+		std::optional<ModelCheckerEngine> engine = ModelCheckerEngine::fromString(settings["modelCheckerEngine"].asString());
+		if (!engine)
+			return formatFatalError("JSONError", "Invalid model checker engine requested.");
+		ret.modelCheckerEngine = *engine;
+	}
+
 	return { std::move(ret) };
 }
 
@@ -886,6 +897,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.enableEvmBytecodeGeneration(isEvmBytecodeRequested(_inputsAndSettings.outputSelection));
 	compilerStack.enableIRGeneration(isIRRequested(_inputsAndSettings.outputSelection));

libsolidity/interface/StandardCompiler.h

@@ -71,6 +71,7 @@ private:
 		bool metadataLiteralSources = false;
 		CompilerStack::MetadataHash metadataHash = CompilerStack::MetadataHash::IPFS;
 		Json::Value outputSelection;
+		ModelCheckerEngine modelCheckerEngine = ModelCheckerEngine::All();
 	};
 
 	/// Parses the input json (and potentially invokes the read callback) and either returns