Merge pull request #7447 from ethereum/smt_callback

[SMTChecker] Create new auxiliary input callback and use as SMT solver

.circleci/config.yml

@@ -583,13 +583,18 @@ jobs:
 
   t_ems_solcjs:
     docker:
-      - image: circleci/node:10
+      - image: ethereum/solidity-buildpack-deps:ubuntu1904
     environment:
       TERM: xterm
     steps:
       - checkout
       - attach_workspace:
           at: /tmp/workspace
+      - run:
+          name: Install test dependencies
+          command: |
+            apt-get update
+            apt-get install -qqy --no-install-recommends nodejs npm cvc4
       - run:
           name: Test solcjs
           command: |

Changelog.md

@@ -3,6 +3,7 @@
 Breaking changes:
  * ABI: remove the deprecated ``constant`` and ``payable`` fields.
  * ABI: the ``type`` field is now required and no longer specified to default to ``function``.
+ * C API (``libsolc``): the provided callback now takes two parameters, kind and data. The callback can then be used for multiple purposes, such has file imports and SMT queries.
  * Commandline interface: remove the text-based ast printer (``--ast``).
  * Command line interface: Switch to the new error reporter by default. ``--old-reporter`` falls back to the deprecated old error reporter.
  * Command line interface: Add option to disable or choose hash method between IPFS and Swarm for the bytecode metadata.

libsolc/libsolc.cpp

@@ -43,11 +43,11 @@ ReadCallback::Callback wrapReadCallback(CStyleReadFileCallback _readCallback = n
 	ReadCallback::Callback readCallback;
 	if (_readCallback)
 	{
-		readCallback = [=](string const& _path)
+		readCallback = [=](string const& _kind, string const& _data)
 		{
 			char* contents_c = nullptr;
 			char* error_c = nullptr;
-			_readCallback(_path.c_str(), &contents_c, &error_c);
+			_readCallback(_kind.c_str(), _data.c_str(), &contents_c, &error_c);
 			ReadCallback::Result result;
 			result.success = true;
 			if (!contents_c && !error_c)

libsolc/libsolc.h

@@ -34,16 +34,17 @@
 extern "C" {
 #endif
 
-/// Callback used to retrieve additional source files.
+/// Callback used to retrieve additional source files or data.
 ///
-/// @param _path The path for loading.
+/// @param _kind The kind of callback (a string).
+/// @param _data The data for the callback.
 /// @param o_contents A pointer to the contents of the file, if found.
 /// @param o_error A pointer to an error message, if there is one.
 ///
 /// If the callback is not supported, o_contents and o_error should be set to NULL.
 ///
 /// The two pointers (o_contents and o_error) should be heap-allocated and are free'd by the caller.
-typedef void (*CStyleReadFileCallback)(char const* _path, char** o_contents, char** o_error);
+typedef void (*CStyleReadFileCallback)(char const* _kind, char const* _data, char** o_contents, char** o_error);
 
 /// Returns the complete license document.
 ///
@@ -58,8 +59,8 @@ char const* solidity_version() SOLC_NOEXCEPT;
 /// Takes a "Standard Input JSON" and an optional callback (can be set to null). Returns
 /// a "Standard Output JSON". Both are to be UTF-8 encoded.
 ///
-/// @param _input
-/// @param _readCallback
+/// @param _input The input JSON to process.
+/// @param _readCallback The optional callback pointer. Can be NULL.
 ///
 /// @returns A pointer to the result. The pointer returned must not be freed by the caller.
 char const* solidity_compile(char const* _input, CStyleReadFileCallback _readCallback) SOLC_NOEXCEPT;

libsolidity/formal/BMC.cpp

@@ -27,10 +27,14 @@ using namespace dev;
 using namespace langutil;
 using namespace dev::solidity;
 
-BMC::BMC(smt::EncodingContext& _context, ErrorReporter& _errorReporter, map<h256, string> const& _smtlib2Responses):
+BMC::BMC(
+	smt::EncodingContext& _context,
+	ErrorReporter& _errorReporter, map<h256, string> const& _smtlib2Responses,
+	ReadCallback::Callback const& _smtCallback
+):
 	SMTEncoder(_context),
 	m_outerErrorReporter(_errorReporter),
-	m_interface(make_shared<smt::SMTPortfolio>(_smtlib2Responses))
+	m_interface(make_shared<smt::SMTPortfolio>(_smtlib2Responses, _smtCallback))
 {
 #if defined (HAVE_Z3) || defined (HAVE_CVC4)
 	if (!_smtlib2Responses.empty())

libsolidity/formal/BMC.h

@@ -53,7 +53,12 @@ namespace solidity
 class BMC: public SMTEncoder
 {
 public:
-	BMC(smt::EncodingContext& _context, langutil::ErrorReporter& _errorReporter, std::map<h256, std::string> const& _smtlib2Responses);
+	BMC(
+		smt::EncodingContext& _context,
+		langutil::ErrorReporter& _errorReporter,
+		std::map<h256, std::string> const& _smtlib2Responses,
+		ReadCallback::Callback const& _smtCallback
+	);
 
 	void analyze(SourceUnit const& _sources, std::set<Expression const*> _safeAssertions);
 

libsolidity/formal/CHC.cpp

@@ -35,17 +35,19 @@ using namespace dev::solidity;
 CHC::CHC(
 	smt::EncodingContext& _context,
 	ErrorReporter& _errorReporter,
-	map<h256, string> const& _smtlib2Responses
+	map<h256, string> const& _smtlib2Responses,
+	ReadCallback::Callback const& _smtCallback
 ):
 	SMTEncoder(_context),
 #ifdef HAVE_Z3
 	m_interface(make_shared<smt::Z3CHCInterface>()),
 #else
-	m_interface(make_shared<smt::CHCSmtLib2Interface>(_smtlib2Responses)),
+	m_interface(make_shared<smt::CHCSmtLib2Interface>(_smtlib2Responses, _smtCallback)),
 #endif
 	m_outerErrorReporter(_errorReporter)
 {
 	(void)_smtlib2Responses;
+	(void)_smtCallback;
 }
 
 void CHC::analyze(SourceUnit const& _source)

libsolidity/formal/CHC.h

@@ -34,6 +34,8 @@
 
 #include <libsolidity/formal/CHCSolverInterface.h>
 
+#include <libsolidity/interface/ReadFile.h>
+
 #include <set>
 
 namespace dev
@@ -47,7 +49,8 @@ public:
 	CHC(
 		smt::EncodingContext& _context,
 		langutil::ErrorReporter& _errorReporter,
-		std::map<h256, std::string> const& _smtlib2Responses
+		std::map<h256, std::string> const& _smtlib2Responses,
+		ReadCallback::Callback const& _smtCallback
 	);
 
 	void analyze(SourceUnit const& _sources);

libsolidity/formal/CHCSmtLib2Interface.cpp

@@ -34,9 +34,13 @@ using namespace dev;
 using namespace dev::solidity;
 using namespace dev::solidity::smt;
 
-CHCSmtLib2Interface::CHCSmtLib2Interface(map<h256, string> const& _queryResponses):
-	m_smtlib2(make_shared<SMTLib2Interface>(_queryResponses)),
-	m_queryResponses(_queryResponses)
+CHCSmtLib2Interface::CHCSmtLib2Interface(
+	map<h256, string> const& _queryResponses,
+	ReadCallback::Callback const& _smtCallback
+):
+	m_smtlib2(make_shared<SMTLib2Interface>(_queryResponses, _smtCallback)),
+	m_queryResponses(_queryResponses),
+	m_smtCallback(_smtCallback)
 {
 	reset();
 }
@@ -152,9 +156,12 @@ string CHCSmtLib2Interface::querySolver(string const& _input)
 	h256 inputHash = dev::keccak256(_input);
 	if (m_queryResponses.count(inputHash))
 		return m_queryResponses.at(inputHash);
-	else
+	if (m_smtCallback)
 	{
-		m_unhandledQueries.push_back(_input);
-		return "unknown\n";
+		auto result = m_smtCallback(ReadCallback::kindString(ReadCallback::Kind::SMTQuery), _input);
+		if (result.success)
+			return result.responseOrErrorMessage;
 	}
+	m_unhandledQueries.push_back(_input);
+	return "unknown\n";
 }

libsolidity/formal/CHCSmtLib2Interface.h

@@ -35,7 +35,10 @@ namespace smt
 class CHCSmtLib2Interface: public CHCSolverInterface
 {
 public:
-	explicit CHCSmtLib2Interface(std::map<h256, std::string> const& _queryResponses);
+	explicit CHCSmtLib2Interface(
+		std::map<h256, std::string> const& _queryResponses,
+		ReadCallback::Callback const& _smtCallback
+	);
 
 	void reset();
 
@@ -68,6 +71,8 @@ private:
 
 	std::map<h256, std::string> const& m_queryResponses;
 	std::vector<std::string> m_unhandledQueries;
+
+	ReadCallback::Callback m_smtCallback;
 };
 
 }

libsolidity/formal/ModelChecker.cpp

@@ -22,9 +22,13 @@ using namespace dev;
 using namespace langutil;
 using namespace dev::solidity;
 
-ModelChecker::ModelChecker(ErrorReporter& _errorReporter, map<h256, string> const& _smtlib2Responses):
-	m_bmc(m_context, _errorReporter, _smtlib2Responses),
-	m_chc(m_context, _errorReporter, _smtlib2Responses),
+ModelChecker::ModelChecker(
+	ErrorReporter& _errorReporter,
+	map<h256, string> const& _smtlib2Responses,
+	ReadCallback::Callback const& _smtCallback
+):
+	m_bmc(m_context, _errorReporter, _smtlib2Responses, _smtCallback),
+	m_chc(m_context, _errorReporter, _smtlib2Responses, _smtCallback),
 	m_context()
 {
 }

libsolidity/formal/ModelChecker.h

@@ -43,7 +43,11 @@ namespace solidity
 class ModelChecker
 {
 public:
-	ModelChecker(langutil::ErrorReporter& _errorReporter, std::map<h256, std::string> const& _smtlib2Responses);
+	ModelChecker(
+		langutil::ErrorReporter& _errorReporter,
+		std::map<h256, std::string> const& _smtlib2Responses,
+		ReadCallback::Callback const& _smtCallback = ReadCallback::Callback()
+	);
 
 	void analyze(SourceUnit const& _sources);
 

libsolidity/formal/SMTLib2Interface.cpp

@@ -34,8 +34,12 @@ using namespace dev;
 using namespace dev::solidity;
 using namespace dev::solidity::smt;
 
-SMTLib2Interface::SMTLib2Interface(map<h256, string> const& _queryResponses):
-	m_queryResponses(_queryResponses)
+SMTLib2Interface::SMTLib2Interface(
+	map<h256, string> const& _queryResponses,
+	ReadCallback::Callback const& _smtCallback
+):
+	m_queryResponses(_queryResponses),
+	m_smtCallback(_smtCallback)
 {
 	reset();
 }
@@ -230,9 +234,12 @@ string SMTLib2Interface::querySolver(string const& _input)
 	h256 inputHash = dev::keccak256(_input);
 	if (m_queryResponses.count(inputHash))
 		return m_queryResponses.at(inputHash);
-	else
+	if (m_smtCallback)
 	{
-		m_unhandledQueries.push_back(_input);
-		return "unknown\n";
+		auto result = m_smtCallback(ReadCallback::kindString(ReadCallback::Kind::SMTQuery), _input);
+		if (result.success)
+			return result.responseOrErrorMessage;
 	}
+	m_unhandledQueries.push_back(_input);
+	return "unknown\n";
 }

libsolidity/formal/SMTLib2Interface.h

@@ -41,7 +41,10 @@ namespace smt
 class SMTLib2Interface: public SolverInterface, public boost::noncopyable
 {
 public:
-	explicit SMTLib2Interface(std::map<h256, std::string> const& _queryResponses);
+	explicit SMTLib2Interface(
+		std::map<h256, std::string> const& _queryResponses,
+		ReadCallback::Callback const& _smtCallback
+	);
 
 	void reset() override;
 
@@ -78,6 +81,8 @@ private:
 
 	std::map<h256, std::string> const& m_queryResponses;
 	std::vector<std::string> m_unhandledQueries;
+
+	ReadCallback::Callback m_smtCallback;
 };
 
 }

libsolidity/formal/SMTPortfolio.cpp

@@ -30,9 +30,12 @@ using namespace dev;
 using namespace dev::solidity;
 using namespace dev::solidity::smt;
 
-SMTPortfolio::SMTPortfolio(map<h256, string> const& _smtlib2Responses)
+SMTPortfolio::SMTPortfolio(
+	map<h256, string> const& _smtlib2Responses,
+	ReadCallback::Callback const& _smtCallback
+)
 {
-	m_solvers.emplace_back(make_unique<smt::SMTLib2Interface>(_smtlib2Responses));
+	m_solvers.emplace_back(make_unique<smt::SMTLib2Interface>(_smtlib2Responses, _smtCallback));
 #ifdef HAVE_Z3
 	m_solvers.emplace_back(make_unique<smt::Z3Interface>());
 #endif

libsolidity/formal/SMTPortfolio.h

@@ -42,7 +42,10 @@ namespace smt
 class SMTPortfolio: public SolverInterface, public boost::noncopyable
 {
 public:
-	SMTPortfolio(std::map<h256, std::string> const& _smtlib2Responses);
+	SMTPortfolio(
+		std::map<h256, std::string> const& _smtlib2Responses,
+		ReadCallback::Callback const& _smtCallback
+	);
 
 	void reset() override;
 

libsolidity/interface/CompilerStack.cpp

@@ -389,7 +389,7 @@ bool CompilerStack::analyze()
 
 		if (noErrors)
 		{
-			ModelChecker modelChecker(m_errorReporter, m_smtlib2Responses);
+			ModelChecker modelChecker(m_errorReporter, m_smtlib2Responses, m_readFile);
 			for (Source const* source: m_sourceOrder)
 				modelChecker.analyze(*source->ast);
 			m_unhandledSMTLib2Queries += modelChecker.unhandledQueries();
@@ -886,7 +886,7 @@ StringMap CompilerStack::loadMissingSources(SourceUnit const& _ast, std::string
 
 			ReadCallback::Result result{false, string("File not supplied initially.")};
 			if (m_readFile)
-				result = m_readFile(importPath);
+				result = m_readFile(ReadCallback::kindString(ReadCallback::Kind::ReadFile), importPath);
 
 			if (result.success)
 				newSources[importPath] = result.responseOrErrorMessage;

libsolidity/interface/CompilerStack.h

@@ -107,7 +107,7 @@ public:
 	};
 
 	/// Creates a new compiler stack.
-	/// @param _readFile callback to used to read files for import statements. Must return
+	/// @param _readFile callback used to read files for import statements. Must return
 	/// and must not emit exceptions.
 	explicit CompilerStack(ReadCallback::Callback const& _readFile = ReadCallback::Callback());
 

libsolidity/interface/ReadFile.h

@@ -17,6 +17,8 @@
 
 #pragma once
 
+#include <liblangutil/Exceptions.h>
+
 #include <boost/noncopyable.hpp>
 #include <functional>
 #include <string>
@@ -37,8 +39,27 @@ public:
 		std::string responseOrErrorMessage;
 	};
 
+	enum class Kind
+	{
+		ReadFile,
+		SMTQuery
+	};
+
+	static std::string kindString(Kind _kind)
+	{
+		switch (_kind)
+		{
+		case Kind::ReadFile:
+			return "source";
+		case Kind::SMTQuery:
+			return "smt-query";
+		default:
+			solAssert(false, "");
+		}
+	}
+
 	/// File reading or generic query callback.
-	using Callback = std::function<Result(std::string const&)>;
+	using Callback = std::function<Result(std::string const&, std::string const&)>;
 };
 
 }

libsolidity/interface/StandardCompiler.cpp

@@ -555,7 +555,7 @@ boost::variant<StandardCompiler::InputsAndSettings, Json::Value> StandardCompile
 			{
 				if (!url.isString())
 					return formatFatalError("JSONError", "URL must be a string.");
-				ReadCallback::Result result = m_readFile(url.asString());
+				ReadCallback::Result result = m_readFile(ReadCallback::kindString(ReadCallback::Kind::ReadFile), url.asString());
 				if (result.success)
 				{
 					if (!hash.empty() && !hashMatchesContent(hash, result.responseOrErrorMessage))

libsolidity/interface/StandardCompiler.h

@@ -41,7 +41,7 @@ class StandardCompiler: boost::noncopyable
 {
 public:
 	/// Creates a new StandardCompiler.
-	/// @param _readFile callback to used to read files for import statements. Must return
+	/// @param _readFile callback used to read files for import statements. Must return
 	/// and must not emit exceptions.
 	explicit StandardCompiler(ReadCallback::Callback const& _readFile = ReadCallback::Callback()):
 		m_readFile(_readFile)

solc/CommandLineInterface.cpp

@@ -848,10 +848,15 @@ Allowed options)",
 
 bool CommandLineInterface::processInput()
 {
-	ReadCallback::Callback fileReader = [this](string const& _path)
+	ReadCallback::Callback fileReader = [this](string const& _kind, string const& _path)
 	{
 		try
 		{
+			if (_kind != ReadCallback::kindString(ReadCallback::Kind::ReadFile))
+				BOOST_THROW_EXCEPTION(InternalCompilerError() << errinfo_comment(
+					"ReadFile callback used as callback kind " +
+					_kind
+				));
 			auto path = boost::filesystem::path(_path);
 			auto canonicalPath = boost::filesystem::weakly_canonical(path);
 			bool isAllowed = false;

test/externalTests/solc-js/solc-js.sh

@@ -46,6 +46,9 @@ function solcjs_test
     printLog "Copying contracts..."
     cp -Rf $SOLCJS_INPUT_DIR/DAO test/
 
+    printLog "Copying SMTChecker tests..."
+    cp -Rf "$TEST_DIR"/test/libsolidity/smtCheckerTests test/
+
     run_install install_fn
 
     # Update version (needed for some tests)

test/libsolidity/LibSolc.cpp

@@ -22,6 +22,7 @@
 #include <string>
 #include <boost/test/unit_test.hpp>
 #include <libdevcore/JSON.h>
+#include <libsolidity/interface/ReadFile.h>
 #include <libsolidity/interface/Version.h>
 #include <libsolc/libsolc.h>
 
@@ -137,9 +138,10 @@ BOOST_AUTO_TEST_CASE(with_callback)
 	)";
 
 	CStyleReadFileCallback callback{
-		[](char const* _path, char** o_contents, char** o_error)
+		[](char const* _kind, char const* _path, char** o_contents, char** o_error)
 		{
 			// Caller frees the pointers.
+			BOOST_CHECK(string(_kind) == ReadCallback::kindString(ReadCallback::Kind::ReadFile));
 			if (string(_path) == "found.sol")
 			{
 				static string content{"import \"missing.sol\"; contract B {}"};