diff --git a/Changelog.md b/Changelog.md index 449798a45..ca904ffc0 100644 --- a/Changelog.md +++ b/Changelog.md @@ -6,6 +6,7 @@ Language Features: Compiler Features: * Build System: LLL is not built anymore by default. Must configure it with CMake as `-DLLL=ON`. * Code generator: Do not perform redundant double cleanup on unsigned integers when loading from calldata. + * SMTChecker: SMTLib2 queries and responses passed via standard JSON compiler interface. * SMTChecker: Support ``msg``, ``tx`` and ``block`` member variables. * SMTChecker: Support ``gasleft()`` and ``blockhash()`` functions. * SMTChecker: Support internal bound function calls. diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index bb9b498fc..0af171a74 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -32,8 +32,8 @@ using namespace dev; using namespace langutil; using namespace dev::solidity; -SMTChecker::SMTChecker(ErrorReporter& _errorReporter, ReadCallback::Callback const& _readFileCallback): - m_interface(make_shared(_readFileCallback)), +SMTChecker::SMTChecker(ErrorReporter& _errorReporter, map const& _smtlib2Responses): + m_interface(make_shared(_smtlib2Responses)), m_errorReporter(_errorReporter) { } diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index 5f51beb73..347248486 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -47,10 +47,15 @@ class VariableUsage; class SMTChecker: private ASTConstVisitor { public: - SMTChecker(langutil::ErrorReporter& _errorReporter, ReadCallback::Callback const& _readCallback); + SMTChecker(langutil::ErrorReporter& _errorReporter, std::map const& _smtlib2Responses); void analyze(SourceUnit const& _sources, std::shared_ptr const& _scanner); + /// This is used if the SMT solver is not directly linked into this binary. + /// @returns a list of inputs to the SMT solver that were not part of the argument to + /// the constructor. + std::vector unhandledQueries() { return m_interface->unhandledQueries(); } + private: // TODO: Check that we do not have concurrent reads and writes to a variable, // because the order of expression evaluation is undefined diff --git a/libsolidity/formal/SMTLib2Interface.cpp b/libsolidity/formal/SMTLib2Interface.cpp index 55c72cfc3..80ecc715d 100644 --- a/libsolidity/formal/SMTLib2Interface.cpp +++ b/libsolidity/formal/SMTLib2Interface.cpp @@ -20,6 +20,8 @@ #include #include +#include + #include #include #include @@ -37,8 +39,8 @@ using namespace dev; using namespace dev::solidity; using namespace dev::solidity::smt; -SMTLib2Interface::SMTLib2Interface(ReadCallback::Callback const& _queryCallback): - m_queryCallback(_queryCallback) +SMTLib2Interface::SMTLib2Interface(map const& _smtlib2Responses): + m_smtlib2Responses(_smtlib2Responses) { reset(); } @@ -212,11 +214,12 @@ vector SMTLib2Interface::parseValues(string::const_iterator _start, stri string SMTLib2Interface::querySolver(string const& _input) { - if (!m_queryCallback) - BOOST_THROW_EXCEPTION(SolverError() << errinfo_comment("No SMT solver available.")); - - ReadCallback::Result queryResult = m_queryCallback(_input); - if (!queryResult.success) - BOOST_THROW_EXCEPTION(SolverError() << errinfo_comment(queryResult.responseOrErrorMessage)); - return queryResult.responseOrErrorMessage; + h256 inputHash = dev::keccak256(_input); + if (m_smtlib2Responses.count(inputHash)) + return m_smtlib2Responses.at(inputHash); + else + { + m_unhandledQueries.push_back(_input); + return "unknown\n"; + } } diff --git a/libsolidity/formal/SMTLib2Interface.h b/libsolidity/formal/SMTLib2Interface.h index 4f72d27c4..c67101ae5 100644 --- a/libsolidity/formal/SMTLib2Interface.h +++ b/libsolidity/formal/SMTLib2Interface.h @@ -22,6 +22,8 @@ #include #include +#include + #include #include @@ -42,7 +44,7 @@ namespace smt class SMTLib2Interface: public SolverInterface, public boost::noncopyable { public: - explicit SMTLib2Interface(ReadCallback::Callback const& _queryCallback); + explicit SMTLib2Interface(std::map const& _smtlib2Responses); void reset() override; @@ -54,6 +56,8 @@ public: void addAssertion(Expression const& _expr) override; std::pair> check(std::vector const& _expressionsToEvaluate) override; + std::vector unhandledQueries() override { return m_unhandledQueries; } + private: void declareFunction(std::string const&, Sort const&); @@ -69,9 +73,11 @@ private: /// Communicates with the solver via the callback. Throws SMTSolverError on error. std::string querySolver(std::string const& _input); - ReadCallback::Callback m_queryCallback; + std::map const& m_smtlib2Responses; std::vector m_accumulatedOutput; std::set m_variables; + + std::vector m_unhandledQueries; }; } diff --git a/libsolidity/formal/SMTPortfolio.cpp b/libsolidity/formal/SMTPortfolio.cpp index 224e5cd61..4c5913805 100644 --- a/libsolidity/formal/SMTPortfolio.cpp +++ b/libsolidity/formal/SMTPortfolio.cpp @@ -32,7 +32,7 @@ using namespace dev; using namespace dev::solidity; using namespace dev::solidity::smt; -SMTPortfolio::SMTPortfolio(ReadCallback::Callback const& _readCallback) +SMTPortfolio::SMTPortfolio(map const& _smtlib2Responses) { #ifdef HAVE_Z3 m_solvers.emplace_back(make_shared()); @@ -41,9 +41,9 @@ SMTPortfolio::SMTPortfolio(ReadCallback::Callback const& _readCallback) m_solvers.emplace_back(make_shared()); #endif #if !defined (HAVE_Z3) && !defined (HAVE_CVC4) - m_solvers.emplace_back(make_shared(_readCallback)), + m_solvers.emplace_back(make_shared(_smtlib2Responses)), #endif - (void)_readCallback; + (void)_smtlib2Responses; } void SMTPortfolio::reset() diff --git a/libsolidity/formal/SMTPortfolio.h b/libsolidity/formal/SMTPortfolio.h index 12e2be669..7f5ba37ee 100644 --- a/libsolidity/formal/SMTPortfolio.h +++ b/libsolidity/formal/SMTPortfolio.h @@ -22,8 +22,11 @@ #include +#include + #include +#include #include namespace dev @@ -42,7 +45,7 @@ namespace smt class SMTPortfolio: public SolverInterface, public boost::noncopyable { public: - SMTPortfolio(ReadCallback::Callback const& _readCallback); + SMTPortfolio(std::map const& _smtlib2Responses); void reset() override; @@ -54,6 +57,7 @@ public: void addAssertion(Expression const& _expr) override; std::pair> check(std::vector const& _expressionsToEvaluate) override; + std::vector unhandledQueries() override { return m_solvers.at(0)->unhandledQueries(); } private: static bool solverAnswered(CheckResult result); diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h index fd1abd611..cc8214de8 100644 --- a/libsolidity/formal/SolverInterface.h +++ b/libsolidity/formal/SolverInterface.h @@ -284,6 +284,9 @@ public: virtual std::pair> check(std::vector const& _expressionsToEvaluate) = 0; + /// @returns a list of queries that the system was not able to respond to. + virtual std::vector unhandledQueries() { return {}; } + protected: // SMT query timeout in milliseconds. static int const queryTimeout = 10000; diff --git a/libsolidity/interface/CompilerStack.cpp b/libsolidity/interface/CompilerStack.cpp index a56747052..ae85276e1 100644 --- a/libsolidity/interface/CompilerStack.cpp +++ b/libsolidity/interface/CompilerStack.cpp @@ -107,6 +107,8 @@ void CompilerStack::reset(bool _keepSources) m_stackState = Empty; m_sources.clear(); } + m_smtlib2Responses.clear(); + m_unhandledSMTLib2Queries.clear(); m_libraries.clear(); m_evmVersion = EVMVersion(); m_optimize = false; @@ -283,9 +285,10 @@ bool CompilerStack::analyze() if (noErrors) { - SMTChecker smtChecker(m_errorReporter, m_smtQuery); + SMTChecker smtChecker(m_errorReporter, m_smtlib2Responses); for (Source const* source: m_sourceOrder) smtChecker.analyze(*source->ast, source->scanner); + m_unhandledSMTLib2Queries += smtChecker.unhandledQueries(); } } catch(FatalError const&) diff --git a/libsolidity/interface/CompilerStack.h b/libsolidity/interface/CompilerStack.h index 8c50266ef..3fceed242 100644 --- a/libsolidity/interface/CompilerStack.h +++ b/libsolidity/interface/CompilerStack.h @@ -153,6 +153,13 @@ public: /// @returns true if a source object by the name already existed and was replaced. bool addSource(std::string const& _name, std::string const& _content, bool _isLibrary = false); + /// Adds a response to an SMTLib2 query (identified by the hash of the query input). + void addSMTLib2Response(h256 const& _hash, std::string const& _response) { m_smtlib2Responses[_hash] = _response; } + + /// @returns a list of unhandled queries to the SMT solver (has to be supplied in a second run + /// by calling @a addSMTLib2Response. + std::vector const& unhandledSMTQueries() const { return m_unhandledSMTLib2Queries; } + /// Parses all source units that were added /// @returns false on error. bool parse(); @@ -334,7 +341,6 @@ private: ) const; ReadCallback::Callback m_readFile; - ReadCallback::Callback m_smtQuery; bool m_optimize = false; unsigned m_optimizeRuns = 200; EVMVersion m_evmVersion; @@ -344,6 +350,8 @@ private: /// "context:prefix=target" std::vector m_remappings; std::map m_sources; + std::vector m_unhandledSMTLib2Queries; + std::map m_smtlib2Responses; std::shared_ptr m_globalContext; std::vector m_sourceOrder; /// This is updated during compilation. diff --git a/libsolidity/interface/StandardCompiler.cpp b/libsolidity/interface/StandardCompiler.cpp index 291a1071b..59c28cd9a 100644 --- a/libsolidity/interface/StandardCompiler.cpp +++ b/libsolidity/interface/StandardCompiler.cpp @@ -319,6 +319,27 @@ Json::Value StandardCompiler::compileInternal(Json::Value const& _input) return formatFatalError("JSONError", "Invalid input source specified."); } + Json::Value const& auxInputs = _input["auxiliaryInput"]; + if (!!auxInputs) + { + Json::Value const& smtlib2Responses = auxInputs["smtlib2"]; + if (!!smtlib2Responses) + for (auto const& hashString: smtlib2Responses.getMemberNames()) + { + h256 hash; + try + { + hash = h256(hashString); + } + catch (dev::BadHexCharacter const&) + { + return formatFatalError("JSONError", "Invalid hex encoding of SMTLib2 auxiliary input."); + } + + m_compilerStack.addSMTLib2Response(hash, smtlib2Responses[hashString].asString()); + } + } + Json::Value const& settings = _input.get("settings", Json::Value()); if (settings.isMember("evmVersion")) @@ -518,6 +539,10 @@ Json::Value StandardCompiler::compileInternal(Json::Value const& _input) if (errors.size() > 0) output["errors"] = errors; + if (!m_compilerStack.unhandledSMTQueries().empty()) + for (string const& query: m_compilerStack.unhandledSMTQueries()) + output["auxiliaryInputRequested"]["smtlib2"]["0x" + keccak256(query).hex()] = query; + output["sources"] = Json::objectValue; unsigned sourceIndex = 0; for (string const& sourceName: analysisSuccess ? m_compilerStack.sourceNames() : vector())