From ddc478e3e44ea14ea5c9b7e24c855e3bc602b777 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Tue, 17 Sep 2019 16:06:43 +0200 Subject: [PATCH] Add CallbackKind and use it for the SMT solver --- .circleci/config.yml | 7 ++++++- Changelog.md | 1 + libsolc/libsolc.cpp | 4 ++-- libsolc/libsolc.h | 11 ++++++----- libsolidity/formal/BMC.cpp | 8 ++++++-- libsolidity/formal/BMC.h | 7 ++++++- libsolidity/formal/CHC.cpp | 6 ++++-- libsolidity/formal/CHC.h | 5 ++++- libsolidity/formal/CHCSmtLib2Interface.cpp | 19 ++++++++++++------ libsolidity/formal/CHCSmtLib2Interface.h | 7 ++++++- libsolidity/formal/ModelChecker.cpp | 10 +++++++--- libsolidity/formal/ModelChecker.h | 6 +++++- libsolidity/formal/SMTLib2Interface.cpp | 17 +++++++++++----- libsolidity/formal/SMTLib2Interface.h | 7 ++++++- libsolidity/formal/SMTPortfolio.cpp | 7 +++++-- libsolidity/formal/SMTPortfolio.h | 5 ++++- libsolidity/interface/CompilerStack.cpp | 4 ++-- libsolidity/interface/CompilerStack.h | 2 +- libsolidity/interface/ReadFile.h | 23 +++++++++++++++++++++- libsolidity/interface/StandardCompiler.cpp | 2 +- libsolidity/interface/StandardCompiler.h | 2 +- solc/CommandLineInterface.cpp | 7 ++++++- test/externalTests/solc-js/solc-js.sh | 3 +++ test/libsolidity/LibSolc.cpp | 4 +++- 24 files changed, 132 insertions(+), 42 deletions(-) diff --git a/.circleci/config.yml b/.circleci/config.yml index 0787855df..3fd62d9d8 100644 --- a/.circleci/config.yml +++ b/.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: | diff --git a/Changelog.md b/Changelog.md index 5298d2ef5..eea0f017f 100644 --- a/Changelog.md +++ b/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. diff --git a/libsolc/libsolc.cpp b/libsolc/libsolc.cpp index 29b732156..eba3aa7aa 100644 --- a/libsolc/libsolc.cpp +++ b/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) diff --git a/libsolc/libsolc.h b/libsolc/libsolc.h index a4ca377a2..ca7ded32b 100644 --- a/libsolc/libsolc.h +++ b/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; diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index dc1f611b6..6950e95c0 100644 --- a/libsolidity/formal/BMC.cpp +++ b/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 const& _smtlib2Responses): +BMC::BMC( + smt::EncodingContext& _context, + ErrorReporter& _errorReporter, map const& _smtlib2Responses, + ReadCallback::Callback const& _smtCallback +): SMTEncoder(_context), m_outerErrorReporter(_errorReporter), - m_interface(make_shared(_smtlib2Responses)) + m_interface(make_shared(_smtlib2Responses, _smtCallback)) { #if defined (HAVE_Z3) || defined (HAVE_CVC4) if (!_smtlib2Responses.empty()) diff --git a/libsolidity/formal/BMC.h b/libsolidity/formal/BMC.h index 432050e78..d5b9d88d1 100644 --- a/libsolidity/formal/BMC.h +++ b/libsolidity/formal/BMC.h @@ -53,7 +53,12 @@ namespace solidity class BMC: public SMTEncoder { public: - BMC(smt::EncodingContext& _context, langutil::ErrorReporter& _errorReporter, std::map const& _smtlib2Responses); + BMC( + smt::EncodingContext& _context, + langutil::ErrorReporter& _errorReporter, + std::map const& _smtlib2Responses, + ReadCallback::Callback const& _smtCallback + ); void analyze(SourceUnit const& _sources, std::set _safeAssertions); diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 8405668ef..92acca004 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -35,17 +35,19 @@ using namespace dev::solidity; CHC::CHC( smt::EncodingContext& _context, ErrorReporter& _errorReporter, - map const& _smtlib2Responses + map const& _smtlib2Responses, + ReadCallback::Callback const& _smtCallback ): SMTEncoder(_context), #ifdef HAVE_Z3 m_interface(make_shared()), #else - m_interface(make_shared(_smtlib2Responses)), + m_interface(make_shared(_smtlib2Responses, _smtCallback)), #endif m_outerErrorReporter(_errorReporter) { (void)_smtlib2Responses; + (void)_smtCallback; } void CHC::analyze(SourceUnit const& _source) diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h index a9fb9f2b7..8e6484a18 100644 --- a/libsolidity/formal/CHC.h +++ b/libsolidity/formal/CHC.h @@ -34,6 +34,8 @@ #include +#include + #include namespace dev @@ -47,7 +49,8 @@ public: CHC( smt::EncodingContext& _context, langutil::ErrorReporter& _errorReporter, - std::map const& _smtlib2Responses + std::map const& _smtlib2Responses, + ReadCallback::Callback const& _smtCallback ); void analyze(SourceUnit const& _sources); diff --git a/libsolidity/formal/CHCSmtLib2Interface.cpp b/libsolidity/formal/CHCSmtLib2Interface.cpp index fb424d782..ceb12bbac 100644 --- a/libsolidity/formal/CHCSmtLib2Interface.cpp +++ b/libsolidity/formal/CHCSmtLib2Interface.cpp @@ -34,9 +34,13 @@ using namespace dev; using namespace dev::solidity; using namespace dev::solidity::smt; -CHCSmtLib2Interface::CHCSmtLib2Interface(map const& _queryResponses): - m_smtlib2(make_shared(_queryResponses)), - m_queryResponses(_queryResponses) +CHCSmtLib2Interface::CHCSmtLib2Interface( + map const& _queryResponses, + ReadCallback::Callback const& _smtCallback +): + m_smtlib2(make_shared(_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"; } diff --git a/libsolidity/formal/CHCSmtLib2Interface.h b/libsolidity/formal/CHCSmtLib2Interface.h index 22bbba859..8aebdd8b2 100644 --- a/libsolidity/formal/CHCSmtLib2Interface.h +++ b/libsolidity/formal/CHCSmtLib2Interface.h @@ -35,7 +35,10 @@ namespace smt class CHCSmtLib2Interface: public CHCSolverInterface { public: - explicit CHCSmtLib2Interface(std::map const& _queryResponses); + explicit CHCSmtLib2Interface( + std::map const& _queryResponses, + ReadCallback::Callback const& _smtCallback + ); void reset(); @@ -68,6 +71,8 @@ private: std::map const& m_queryResponses; std::vector m_unhandledQueries; + + ReadCallback::Callback m_smtCallback; }; } diff --git a/libsolidity/formal/ModelChecker.cpp b/libsolidity/formal/ModelChecker.cpp index c061c8416..20bc527d3 100644 --- a/libsolidity/formal/ModelChecker.cpp +++ b/libsolidity/formal/ModelChecker.cpp @@ -22,9 +22,13 @@ using namespace dev; using namespace langutil; using namespace dev::solidity; -ModelChecker::ModelChecker(ErrorReporter& _errorReporter, map const& _smtlib2Responses): - m_bmc(m_context, _errorReporter, _smtlib2Responses), - m_chc(m_context, _errorReporter, _smtlib2Responses), +ModelChecker::ModelChecker( + ErrorReporter& _errorReporter, + map const& _smtlib2Responses, + ReadCallback::Callback const& _smtCallback +): + m_bmc(m_context, _errorReporter, _smtlib2Responses, _smtCallback), + m_chc(m_context, _errorReporter, _smtlib2Responses, _smtCallback), m_context() { } diff --git a/libsolidity/formal/ModelChecker.h b/libsolidity/formal/ModelChecker.h index 349ed76d4..764803141 100644 --- a/libsolidity/formal/ModelChecker.h +++ b/libsolidity/formal/ModelChecker.h @@ -43,7 +43,11 @@ namespace solidity class ModelChecker { public: - ModelChecker(langutil::ErrorReporter& _errorReporter, std::map const& _smtlib2Responses); + ModelChecker( + langutil::ErrorReporter& _errorReporter, + std::map const& _smtlib2Responses, + ReadCallback::Callback const& _smtCallback = ReadCallback::Callback() + ); void analyze(SourceUnit const& _sources); diff --git a/libsolidity/formal/SMTLib2Interface.cpp b/libsolidity/formal/SMTLib2Interface.cpp index 3c0f38601..77a44abe1 100644 --- a/libsolidity/formal/SMTLib2Interface.cpp +++ b/libsolidity/formal/SMTLib2Interface.cpp @@ -34,8 +34,12 @@ using namespace dev; using namespace dev::solidity; using namespace dev::solidity::smt; -SMTLib2Interface::SMTLib2Interface(map const& _queryResponses): - m_queryResponses(_queryResponses) +SMTLib2Interface::SMTLib2Interface( + map 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"; } diff --git a/libsolidity/formal/SMTLib2Interface.h b/libsolidity/formal/SMTLib2Interface.h index 21c11f80d..f3e242f93 100644 --- a/libsolidity/formal/SMTLib2Interface.h +++ b/libsolidity/formal/SMTLib2Interface.h @@ -41,7 +41,10 @@ namespace smt class SMTLib2Interface: public SolverInterface, public boost::noncopyable { public: - explicit SMTLib2Interface(std::map const& _queryResponses); + explicit SMTLib2Interface( + std::map const& _queryResponses, + ReadCallback::Callback const& _smtCallback + ); void reset() override; @@ -78,6 +81,8 @@ private: std::map const& m_queryResponses; std::vector m_unhandledQueries; + + ReadCallback::Callback m_smtCallback; }; } diff --git a/libsolidity/formal/SMTPortfolio.cpp b/libsolidity/formal/SMTPortfolio.cpp index d47c01f31..96e758b10 100644 --- a/libsolidity/formal/SMTPortfolio.cpp +++ b/libsolidity/formal/SMTPortfolio.cpp @@ -30,9 +30,12 @@ using namespace dev; using namespace dev::solidity; using namespace dev::solidity::smt; -SMTPortfolio::SMTPortfolio(map const& _smtlib2Responses) +SMTPortfolio::SMTPortfolio( + map const& _smtlib2Responses, + ReadCallback::Callback const& _smtCallback +) { - m_solvers.emplace_back(make_unique(_smtlib2Responses)); + m_solvers.emplace_back(make_unique(_smtlib2Responses, _smtCallback)); #ifdef HAVE_Z3 m_solvers.emplace_back(make_unique()); #endif diff --git a/libsolidity/formal/SMTPortfolio.h b/libsolidity/formal/SMTPortfolio.h index d922affd2..62b084ee7 100644 --- a/libsolidity/formal/SMTPortfolio.h +++ b/libsolidity/formal/SMTPortfolio.h @@ -42,7 +42,10 @@ namespace smt class SMTPortfolio: public SolverInterface, public boost::noncopyable { public: - SMTPortfolio(std::map const& _smtlib2Responses); + SMTPortfolio( + std::map const& _smtlib2Responses, + ReadCallback::Callback const& _smtCallback + ); void reset() override; diff --git a/libsolidity/interface/CompilerStack.cpp b/libsolidity/interface/CompilerStack.cpp index ac317d5bf..2d8cb9863 100644 --- a/libsolidity/interface/CompilerStack.cpp +++ b/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; diff --git a/libsolidity/interface/CompilerStack.h b/libsolidity/interface/CompilerStack.h index b7137ee92..be0f19d29 100644 --- a/libsolidity/interface/CompilerStack.h +++ b/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()); diff --git a/libsolidity/interface/ReadFile.h b/libsolidity/interface/ReadFile.h index 3b3d747ed..05fd2c5a2 100644 --- a/libsolidity/interface/ReadFile.h +++ b/libsolidity/interface/ReadFile.h @@ -17,6 +17,8 @@ #pragma once +#include + #include #include #include @@ -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; + using Callback = std::function; }; } diff --git a/libsolidity/interface/StandardCompiler.cpp b/libsolidity/interface/StandardCompiler.cpp index bc77e50c5..fd927828e 100644 --- a/libsolidity/interface/StandardCompiler.cpp +++ b/libsolidity/interface/StandardCompiler.cpp @@ -555,7 +555,7 @@ boost::variant 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)) diff --git a/libsolidity/interface/StandardCompiler.h b/libsolidity/interface/StandardCompiler.h index 030ade0f1..346ef7dcd 100644 --- a/libsolidity/interface/StandardCompiler.h +++ b/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) diff --git a/solc/CommandLineInterface.cpp b/solc/CommandLineInterface.cpp index da34ef868..e0e0c596e 100644 --- a/solc/CommandLineInterface.cpp +++ b/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; diff --git a/test/externalTests/solc-js/solc-js.sh b/test/externalTests/solc-js/solc-js.sh index 4267ba11b..daffee0e3 100755 --- a/test/externalTests/solc-js/solc-js.sh +++ b/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) diff --git a/test/libsolidity/LibSolc.cpp b/test/libsolidity/LibSolc.cpp index 3f55cdaed..7beebf3ea 100644 --- a/test/libsolidity/LibSolc.cpp +++ b/test/libsolidity/LibSolc.cpp @@ -22,6 +22,7 @@ #include #include #include +#include #include #include @@ -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 {}"};