Add SMTCheckerTest for isoltest

libsolidity/formal/CHC.cpp

@@ -48,7 +48,8 @@ CHC::CHC(
 #else
 	m_interface(make_shared<smt::CHCSmtLib2Interface>(_smtlib2Responses)),
 #endif
-	m_outerErrorReporter(_errorReporter)
+	m_outerErrorReporter(_errorReporter),
+	m_enabledSolvers(_enabledSolvers)
 {
 	(void)_smtlib2Responses;
 	(void)_enabledSolvers;
@@ -58,15 +59,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);
+	usesZ3 = m_enabledSolvers.z3;
-	solAssert(z3Interface, "");
+	if (usesZ3)
-	m_context.setSolver(z3Interface->z3Interface());
+	{
-#else
+		auto z3Interface = dynamic_pointer_cast<smt::Z3CHCInterface>(m_interface);
-	auto smtlib2Interface = dynamic_pointer_cast<smt::CHCSmtLib2Interface>(m_interface);
+		solAssert(z3Interface, "");
-	solAssert(smtlib2Interface, "");
+		m_context.setSolver(z3Interface->z3Interface());
-	m_context.setSolver(smtlib2Interface->smtlib2Interface());
+	}
 #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

@@ -208,6 +208,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

@@ -46,3 +46,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

@@ -59,6 +59,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)
@@ -179,6 +187,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_optimiserSettings = OptimiserSettings::minimal();
@@ -372,7 +381,7 @@ bool CompilerStack::analyze()
 
 		if (noErrors)
 		{
-			ModelChecker modelChecker(m_errorReporter, m_smtlib2Responses);
+			ModelChecker modelChecker(m_errorReporter, m_smtlib2Responses, m_enabledSMTSolvers);
 			for (Source const* source: m_sourceOrder)
 				modelChecker.analyze(*source->ast);
 			m_unhandledSMTLib2Queries += modelChecker.unhandledQueries();

libsolidity/interface/CompilerStack.h

@@ -26,6 +26,7 @@
 #include <libsolidity/interface/ReadFile.h>
 #include <libsolidity/interface/OptimiserSettings.h>
 #include <libsolidity/interface/Version.h>
+#include <libsolidity/formal/SolverInterface.h>
 
 #include <liblangutil/ErrorReporter.h>
 #include <liblangutil/EVMVersion.h>
@@ -152,6 +153,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.
@@ -413,6 +417,7 @@ private:
 	ReadCallback::Callback m_readFile;
 	OptimiserSettings m_optimiserSettings;
 	langutil::EVMVersion m_evmVersion;
+	smt::SMTSolverChoice m_enabledSMTSolvers;
 	std::map<std::string, std::set<std::string>> m_requestedContractNames;
 	bool m_generateIR;
 	bool m_generateEWasm;

test/CMakeLists.txt

@@ -91,6 +91,8 @@ set(libsolidity_sources
     libsolidity/SMTChecker.cpp
     libsolidity/SMTCheckerJSONTest.cpp
     libsolidity/SMTCheckerJSONTest.h
+    libsolidity/SMTCheckerTest.cpp
+    libsolidity/SMTCheckerTest.h
     libsolidity/SolidityCompiler.cpp
     libsolidity/SolidityEndToEndTest.cpp
     libsolidity/SolidityExecutionFramework.cpp

test/InteractiveTests.h

@@ -23,6 +23,7 @@
 #include <test/libsolidity/GasTest.h>
 #include <test/libsolidity/SyntaxTest.h>
 #include <test/libsolidity/SemanticTest.h>
+#include <test/libsolidity/SMTCheckerTest.h>
 #include <test/libsolidity/SMTCheckerJSONTest.h>
 #include <test/libyul/EWasmTranslationTest.h>
 #include <test/libyul/YulOptimizerTest.h>
@@ -65,8 +66,8 @@ Testsuite const g_interactiveTestsuites[] = {
 	{"Semantic",            "libsolidity", "semanticTests",       false, true,  &SemanticTest::create},
 	{"JSON AST",            "libsolidity", "ASTJSON",             false, false, &ASTJSONTest::create},
 	{"JSON ABI",            "libsolidity", "ABIJson",             false, false, &ABIJsonTest::create},
-	{"SMT Checker",         "libsolidity", "smtCheckerTests",     true,  false, &SyntaxTest::create},
+	{"SMT Checker",         "libsolidity", "smtCheckerTests",     true,  false, &SMTCheckerTest::create},
-	{"SMT Checker JSON",    "libsolidity", "smtCheckerTestsJSON", true,  false, &SMTCheckerTest::create},
+	{"SMT Checker JSON",    "libsolidity", "smtCheckerTestsJSON", true,  false, &SMTCheckerJSONTest::create},
 	{"Gas Estimates",       "libsolidity", "gasTests",            false, false, &GasTest::create}
 };
 

test/libsolidity/SMTCheckerJSONTest.cpp

@@ -36,7 +36,7 @@ using namespace dev;
 using namespace std;
 using namespace boost::unit_test;
 
-SMTCheckerTest::SMTCheckerTest(string const& _filename, langutil::EVMVersion _evmVersion)
+SMTCheckerJSONTest::SMTCheckerJSONTest(string const& _filename, langutil::EVMVersion _evmVersion)
 : SyntaxTest(_filename, _evmVersion)
 {
 	if (!boost::algorithm::ends_with(_filename, ".sol"))
@@ -50,7 +50,7 @@ SMTCheckerTest::SMTCheckerTest(string const& _filename, langutil::EVMVersion _ev
 		BOOST_THROW_EXCEPTION(runtime_error("Invalid JSON file."));
 }
 
-TestCase::TestResult SMTCheckerTest::run(ostream& _stream, string const& _linePrefix, bool _formatted)
+TestCase::TestResult SMTCheckerJSONTest::run(ostream& _stream, string const& _linePrefix, bool _formatted)
 {
 	StandardCompiler compiler;
 
@@ -129,7 +129,7 @@ TestCase::TestResult SMTCheckerTest::run(ostream& _stream, string const& _linePr
 	return printExpectationAndError(_stream, _linePrefix, _formatted) ? TestResult::Success : TestResult::Failure;
 }
 
-vector<string> SMTCheckerTest::hashesFromJson(Json::Value const& _jsonObj, string const& _auxInput, string const& _smtlib)
+vector<string> SMTCheckerJSONTest::hashesFromJson(Json::Value const& _jsonObj, string const& _auxInput, string const& _smtlib)
 {
 	vector<string> hashes;
 	Json::Value const& auxInputs = _jsonObj[_auxInput];
@@ -143,7 +143,7 @@ vector<string> SMTCheckerTest::hashesFromJson(Json::Value const& _jsonObj, strin
 	return hashes;
 }
 
-Json::Value SMTCheckerTest::buildJson(string const& _extra)
+Json::Value SMTCheckerJSONTest::buildJson(string const& _extra)
 {
 	string language = "\"language\": \"Solidity\"";
 	string sources = " \"sources\": { ";

test/libsolidity/SMTCheckerJSONTest.h

@@ -30,14 +30,14 @@ namespace solidity
 namespace test
 {
 
-class SMTCheckerTest: public SyntaxTest
+class SMTCheckerJSONTest: public SyntaxTest
 {
 public:
 	static std::unique_ptr<TestCase> create(Config const& _config)
 	{
-		return std::make_unique<SMTCheckerTest>(_config.filename, _config.evmVersion);
+		return std::make_unique<SMTCheckerJSONTest>(_config.filename, _config.evmVersion);
 	}
-	SMTCheckerTest(std::string const& _filename, langutil::EVMVersion _evmVersion);
+	SMTCheckerJSONTest(std::string const& _filename, langutil::EVMVersion _evmVersion);
 
 	TestResult run(std::ostream& _stream, std::string const& _linePrefix = "", bool _formatted = false) override;
 

test/libsolidity/SMTCheckerTest.cpp

@@ -0,0 +1,71 @@
+/*
+	This file is part of solidity.
+
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+
+#include <test/libsolidity/SMTCheckerTest.h>
+#include <test/Options.h>
+
+#include <libsolidity/formal/ModelChecker.h>
+
+using namespace langutil;
+using namespace dev::solidity;
+using namespace dev::solidity::test;
+using namespace dev;
+using namespace std;
+
+SMTCheckerTest::SMTCheckerTest(string const& _filename, langutil::EVMVersion _evmVersion): SyntaxTest(_filename, _evmVersion)
+{
+	if (m_settings.count("SMTSolvers"))
+	{
+		auto const& choice = m_settings.at("SMTSolvers");
+		if (choice == "any")
+			m_enabledSolvers = smt::SMTSolverChoice::All();
+		else if (choice == "z3")
+			m_enabledSolvers = smt::SMTSolverChoice::Z3();
+		else if (choice == "cvc4")
+			m_enabledSolvers = smt::SMTSolverChoice::CVC4();
+		else if (choice == "none")
+			m_enabledSolvers = smt::SMTSolverChoice::None();
+		else
+			BOOST_THROW_EXCEPTION(runtime_error("Invalid SMT solver choice."));
+	}
+	else
+		m_enabledSolvers = smt::SMTSolverChoice::All();
+}
+
+TestCase::TestResult SMTCheckerTest::run(ostream& _stream, string const& _linePrefix, bool _formatted)
+{
+	setupCompiler();
+	compiler().setSMTSolverChoice(m_enabledSolvers);
+	parseAndAnalyze();
+	filterObtainedErrors();
+
+	return printExpectationAndError(_stream, _linePrefix, _formatted) ? TestResult::Success : TestResult::Failure;
+}
+
+bool SMTCheckerTest::validateSettings(langutil::EVMVersion _evmVersion)
+{
+	auto available = ModelChecker::availableSolvers();
+	if (!available.z3)
+		m_enabledSolvers.z3 = false;
+	if (!available.cvc4)
+		m_enabledSolvers.cvc4 = false;
+
+	if (m_enabledSolvers.none())
+		return false;
+
+	return SyntaxTest::validateSettings(_evmVersion);
+}

test/libsolidity/SMTCheckerTest.h

@@ -0,0 +1,55 @@
+/*
+	This file is part of solidity.
+
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+
+#pragma once
+
+#include <test/libsolidity/SyntaxTest.h>
+
+#include <libsolidity/formal/SolverInterface.h>
+
+#include <string>
+
+namespace dev
+{
+namespace solidity
+{
+namespace test
+{
+
+class SMTCheckerTest: public SyntaxTest
+{
+public:
+	static std::unique_ptr<TestCase> create(Config const& _config)
+	{
+		return std::make_unique<SMTCheckerTest>(_config.filename, _config.evmVersion);
+	}
+	SMTCheckerTest(std::string const& _filename, langutil::EVMVersion _evmVersion);
+
+	TestResult run(std::ostream& _stream, std::string const& _linePrefix = "", bool _formatted = false) override;
+
+	bool validateSettings(langutil::EVMVersion _evmVersion) override;
+
+protected:
+	/// This is set via option SMTSolvers in the test.
+	/// The possible options are `all`, `z3`, `cvc4`, `none`,
+	/// where if none is given the default used option is `all`.
+	smt::SMTSolverChoice m_enabledSolvers;
+};
+
+}
+}
+}

test/libsolidity/SyntaxTest.cpp

@@ -176,23 +176,22 @@ void SyntaxTest::setupCompiler()
 
 void SyntaxTest::parseAndAnalyze()
 {
-	if (compiler().parse())
+	if (compiler().parse() && compiler().analyze())
-		if (compiler().analyze())
+		try
-			try
+		{
-			{
+			if (!compiler().compile())
-				if (!compiler().compile())
+				BOOST_THROW_EXCEPTION(runtime_error("Compilation failed even though analysis was successful."));
-					BOOST_THROW_EXCEPTION(runtime_error("Compilation failed even though analysis was successful."));
+		}
-			}
+		catch (UnimplementedFeatureError const& _e)
-			catch (UnimplementedFeatureError const& _e)
+		{
-			{
+			m_errorList.emplace_back(SyntaxTestError{
-				m_errorList.emplace_back(SyntaxTestError{
+				"UnimplementedFeatureError",
-					"UnimplementedFeatureError",
+				errorMessage(_e),
-					errorMessage(_e),
+				"",
-					"",
+				-1,
-					-1,
+				-1
-					-1
+			});
-				});
+		}
-			}
 }
 
 void SyntaxTest::filterObtainedErrors()

test/tools/CMakeLists.txt

@@ -29,6 +29,7 @@ add_executable(isoltest
 	../ExecutionFramework.cpp
 	../libsolidity/ABIJsonTest.cpp
 	../libsolidity/ASTJSONTest.cpp
+	../libsolidity/SMTCheckerTest.cpp
 	../libsolidity/SMTCheckerJSONTest.cpp
 	../libyul/Common.cpp
 	../libyul/EWasmTranslationTest.cpp