Merge remote-tracking branch 'origin/develop' into develop_060

libsolidity/formal/CHC.cpp

@@ -49,7 +49,8 @@ CHC::CHC(
 #else
 	m_interface(make_shared<smt::CHCSmtLib2Interface>(_smtlib2Responses, _smtCallback)),
 #endif
-	m_outerErrorReporter(_errorReporter)
+	m_outerErrorReporter(_errorReporter),
+	m_enabledSolvers(_enabledSolvers)
 {
 	(void)_smtlib2Responses;
 	(void)_enabledSolvers;
@@ -60,15 +61,22 @@ void CHC::analyze(SourceUnit const& _source)
 {
 	solAssert(_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker), "");
 
+	bool usesZ3 = false;
 #ifdef HAVE_Z3
-	auto z3Interface = dynamic_pointer_cast<smt::Z3CHCInterface>(m_interface);
-	solAssert(z3Interface, "");
-	m_context.setSolver(z3Interface->z3Interface());
-#else
-	auto smtlib2Interface = dynamic_pointer_cast<smt::CHCSmtLib2Interface>(m_interface);
-	solAssert(smtlib2Interface, "");
-	m_context.setSolver(smtlib2Interface->smtlib2Interface());
+	usesZ3 = m_enabledSolvers.z3;
+	if (usesZ3)
+	{
+		auto z3Interface = dynamic_pointer_cast<smt::Z3CHCInterface>(m_interface);
+		solAssert(z3Interface, "");
+		m_context.setSolver(z3Interface->z3Interface());
+	}
 #endif
+	if (!usesZ3)
+	{
+		auto smtlib2Interface = dynamic_pointer_cast<smt::CHCSmtLib2Interface>(m_interface);
+		solAssert(smtlib2Interface, "");
+		m_context.setSolver(smtlib2Interface->smtlib2Interface());
+	}
 	m_context.clear();
 	m_context.setAssertionAccumulation(false);
 	m_variableUsage.setFunctionInlining(false);

libsolidity/formal/CHC.h

@@ -211,6 +211,9 @@ private:
 
 	/// ErrorReporter that comes from CompilerStack.
 	langutil::ErrorReporter& m_outerErrorReporter;
+
+	/// SMT solvers that are chosen at runtime.
+	smt::SMTSolverChoice m_enabledSolvers;
 };
 
 }

libsolidity/formal/ModelChecker.cpp

@@ -47,3 +47,15 @@ vector<string> ModelChecker::unhandledQueries()
 {
 	return m_bmc.unhandledQueries() + m_chc.unhandledQueries();
 }
+
+smt::SMTSolverChoice ModelChecker::availableSolvers()
+{
+	smt::SMTSolverChoice available = smt::SMTSolverChoice::None();
+#ifdef HAVE_Z3
+	available.z3 = true;
+#endif
+#ifdef HAVE_CVC4
+	available.cvc4 = true;
+#endif
+	return available;
+}

libsolidity/formal/ModelChecker.h

@@ -60,6 +60,9 @@ public:
 	/// the constructor.
 	std::vector<std::string> unhandledQueries();
 
+	/// @returns SMT solvers that are available via the C++ API.
+	static smt::SMTSolverChoice availableSolvers();
+
 private:
 	/// Bounded Model Checker engine.
 	BMC m_bmc;

libsolidity/interface/CompilerStack.cpp

@@ -79,6 +79,7 @@ static int g_compilerStackCounts = 0;
 
 CompilerStack::CompilerStack(ReadCallback::Callback const& _readFile):
 	m_readFile{_readFile},
+	m_enabledSMTSolvers{smt::SMTSolverChoice::All()},
 	m_generateIR{false},
 	m_generateEWasm{false},
 	m_errorList{},
@@ -132,6 +133,13 @@ void CompilerStack::setEVMVersion(langutil::EVMVersion _version)
 	m_evmVersion = _version;
 }
 
+void CompilerStack::setSMTSolverChoice(smt::SMTSolverChoice _enabledSMTSolvers)
+{
+	if (m_stackState >= ParsingPerformed)
+		BOOST_THROW_EXCEPTION(CompilerError() << errinfo_comment("Must set enabled SMT solvers before parsing."));
+	m_enabledSMTSolvers = _enabledSMTSolvers;
+}
+
 void CompilerStack::setLibraries(std::map<std::string, h160> const& _libraries)
 {
 	if (m_stackState >= ParsingPerformed)
@@ -194,6 +202,7 @@ void CompilerStack::reset(bool _keepSettings)
 		m_remappings.clear();
 		m_libraries.clear();
 		m_evmVersion = langutil::EVMVersion();
+		m_enabledSMTSolvers = smt::SMTSolverChoice::All();
 		m_generateIR = false;
 		m_generateEWasm = false;
 		m_revertStrings = RevertStrings::Default;
@@ -383,7 +392,7 @@ bool CompilerStack::analyze()
 
 		if (noErrors)
 		{
-			ModelChecker modelChecker(m_errorReporter, m_smtlib2Responses, m_readFile);
+			ModelChecker modelChecker(m_errorReporter, m_smtlib2Responses, m_readFile, m_enabledSMTSolvers);
 			for (Source const* source: m_sourceOrder)
 				modelChecker.analyze(*source->ast);
 			m_unhandledSMTLib2Queries += modelChecker.unhandledQueries();

libsolidity/interface/CompilerStack.h

@@ -27,6 +27,7 @@
 #include <libsolidity/interface/OptimiserSettings.h>
 #include <libsolidity/interface/Version.h>
 #include <libsolidity/interface/DebugSettings.h>
+#include <libsolidity/formal/SolverInterface.h>
 
 #include <liblangutil/ErrorReporter.h>
 #include <liblangutil/EVMVersion.h>
@@ -162,6 +163,9 @@ public:
 	/// Must be set before parsing.
 	void setEVMVersion(langutil::EVMVersion _version = langutil::EVMVersion{});
 
+	/// Set which SMT solvers should be enabled.
+	void setSMTSolverChoice(smt::SMTSolverChoice _enabledSolvers);
+
 	/// Sets the requested contract names by source.
 	/// If empty, no filtering is performed and every contract
 	/// found in the supplied sources is compiled.
@@ -429,6 +433,7 @@ private:
 	OptimiserSettings m_optimiserSettings;
 	RevertStrings m_revertStrings = RevertStrings::Default;
 	langutil::EVMVersion m_evmVersion;
+	smt::SMTSolverChoice m_enabledSMTSolvers;
 	std::map<std::string, std::set<std::string>> m_requestedContractNames;
 	bool m_generateIR;
 	bool m_generateEWasm;