diff options
24 files changed, 356 insertions, 26 deletions
diff --git a/Changelog.md b/Changelog.md index 449798a4..ca904ffc 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/libdevcore/JSON.cpp b/libdevcore/JSON.cpp index 6317cc89..086fae50 100644 --- a/libdevcore/JSON.cpp +++ b/libdevcore/JSON.cpp @@ -21,6 +21,8 @@ #include "JSON.h" +#include "CommonIO.h" + #include <sstream> #include <map> #include <memory> @@ -111,4 +113,10 @@ bool jsonParse(string const& _input, Json::Value& _json, string *_errs /* = null return parse(readerBuilder, _input, _json, _errs); } +bool jsonParseFile(string const& _fileName, Json::Value& _json, string *_errs /* = nullptr */) +{ + return jsonParse(readFileAsString(_fileName), _json, _errs); +} + + } // namespace dev diff --git a/libdevcore/JSON.h b/libdevcore/JSON.h index 1ce822cd..ecb93467 100644 --- a/libdevcore/JSON.h +++ b/libdevcore/JSON.h @@ -48,4 +48,11 @@ bool jsonParseStrict(std::string const& _input, Json::Value& _json, std::string* /// \return \c true if the document was successfully parsed, \c false if an error occurred. bool jsonParse(std::string const& _input, Json::Value& _json, std::string* _errs = nullptr); +/// Parse a JSON string (@a _input) and writes resulting JSON object to (@a _json) +/// \param _input file containing JSON input +/// \param _json [out] resulting JSON object +/// \param _errs [out] Formatted error messages +/// \return \c true if the document was successfully parsed, \c false if an error occurred. +bool jsonParseFile(std::string const& _fileName, Json::Value& _json, std::string* _errs = nullptr); + } diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index bb9b498f..5b7807f7 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -32,10 +32,19 @@ using namespace dev; using namespace langutil; using namespace dev::solidity; -SMTChecker::SMTChecker(ErrorReporter& _errorReporter, ReadCallback::Callback const& _readFileCallback): - m_interface(make_shared<smt::SMTPortfolio>(_readFileCallback)), +SMTChecker::SMTChecker(ErrorReporter& _errorReporter, map<h256, string> const& _smtlib2Responses): + m_interface(make_shared<smt::SMTPortfolio>(_smtlib2Responses)), m_errorReporter(_errorReporter) { +#if defined (HAVE_Z3) || defined (HAVE_CVC4) + if (!_smtlib2Responses.empty()) + m_errorReporter.warning( + "SMT-LIB2 query responses were given in the auxiliary input, " + "but this Solidity binary uses an SMT solver (Z3/CVC4) directly." + "These responses will be ignored." + "Consider disabling Z3/CVC4 at compilation time in order to use SMT-LIB2 responses." + ); +#endif } void SMTChecker::analyze(SourceUnit const& _source, shared_ptr<Scanner> const& _scanner) diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index 5f51beb7..34724848 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<h256, std::string> const& _smtlib2Responses); void analyze(SourceUnit const& _sources, std::shared_ptr<langutil::Scanner> 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<std::string> 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 55c72cfc..3cfa01b1 100644 --- a/libsolidity/formal/SMTLib2Interface.cpp +++ b/libsolidity/formal/SMTLib2Interface.cpp @@ -20,6 +20,8 @@ #include <liblangutil/Exceptions.h> #include <libsolidity/interface/ReadFile.h> +#include <libdevcore/Keccak256.h> + #include <boost/algorithm/string/predicate.hpp> #include <boost/algorithm/string/join.hpp> #include <boost/filesystem/operations.hpp> @@ -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<h256, string> const& _queryResponses): + m_queryResponses(_queryResponses) { reset(); } @@ -212,11 +214,12 @@ vector<string> 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_queryResponses.count(inputHash)) + return m_queryResponses.at(inputHash); + else + { + m_unhandledQueries.push_back(_input); + return "unknown\n"; + } } diff --git a/libsolidity/formal/SMTLib2Interface.h b/libsolidity/formal/SMTLib2Interface.h index 4f72d27c..55fc4096 100644 --- a/libsolidity/formal/SMTLib2Interface.h +++ b/libsolidity/formal/SMTLib2Interface.h @@ -22,6 +22,8 @@ #include <liblangutil/Exceptions.h> #include <libsolidity/interface/ReadFile.h> +#include <libdevcore/FixedHash.h> + #include <libdevcore/Common.h> #include <boost/noncopyable.hpp> @@ -42,7 +44,7 @@ namespace smt class SMTLib2Interface: public SolverInterface, public boost::noncopyable { public: - explicit SMTLib2Interface(ReadCallback::Callback const& _queryCallback); + explicit SMTLib2Interface(std::map<h256, std::string> const& _queryResponses); void reset() override; @@ -54,6 +56,8 @@ public: void addAssertion(Expression const& _expr) override; std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override; + std::vector<std::string> 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::vector<std::string> m_accumulatedOutput; std::set<std::string> m_variables; + + std::map<h256, std::string> const& m_queryResponses; + std::vector<std::string> m_unhandledQueries; }; } diff --git a/libsolidity/formal/SMTPortfolio.cpp b/libsolidity/formal/SMTPortfolio.cpp index 224e5cd6..2a109b89 100644 --- a/libsolidity/formal/SMTPortfolio.cpp +++ b/libsolidity/formal/SMTPortfolio.cpp @@ -23,27 +23,22 @@ #ifdef HAVE_CVC4 #include <libsolidity/formal/CVC4Interface.h> #endif -#if !defined (HAVE_Z3) && !defined (HAVE_CVC4) #include <libsolidity/formal/SMTLib2Interface.h> -#endif using namespace std; using namespace dev; using namespace dev::solidity; using namespace dev::solidity::smt; -SMTPortfolio::SMTPortfolio(ReadCallback::Callback const& _readCallback) +SMTPortfolio::SMTPortfolio(map<h256, string> const& _smtlib2Responses) { + m_solvers.emplace_back(make_shared<smt::SMTLib2Interface>(_smtlib2Responses)); #ifdef HAVE_Z3 m_solvers.emplace_back(make_shared<smt::Z3Interface>()); #endif #ifdef HAVE_CVC4 m_solvers.emplace_back(make_shared<smt::CVC4Interface>()); #endif -#if !defined (HAVE_Z3) && !defined (HAVE_CVC4) - m_solvers.emplace_back(make_shared<smt::SMTLib2Interface>(_readCallback)), -#endif - (void)_readCallback; } void SMTPortfolio::reset() diff --git a/libsolidity/formal/SMTPortfolio.h b/libsolidity/formal/SMTPortfolio.h index 12e2be66..7f5ba37e 100644 --- a/libsolidity/formal/SMTPortfolio.h +++ b/libsolidity/formal/SMTPortfolio.h @@ -22,8 +22,11 @@ #include <libsolidity/interface/ReadFile.h> +#include <libdevcore/FixedHash.h> + #include <boost/noncopyable.hpp> +#include <map> #include <vector> namespace dev @@ -42,7 +45,7 @@ namespace smt class SMTPortfolio: public SolverInterface, public boost::noncopyable { public: - SMTPortfolio(ReadCallback::Callback const& _readCallback); + SMTPortfolio(std::map<h256, std::string> const& _smtlib2Responses); void reset() override; @@ -54,6 +57,7 @@ public: void addAssertion(Expression const& _expr) override; std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override; + std::vector<std::string> 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 fd1abd61..cc8214de 100644 --- a/libsolidity/formal/SolverInterface.h +++ b/libsolidity/formal/SolverInterface.h @@ -284,6 +284,9 @@ public: virtual std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) = 0; + /// @returns a list of queries that the system was not able to respond to. + virtual std::vector<std::string> 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 a5674705..ae85276e 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 8c50266e..2c7add3b 100644 --- a/libsolidity/interface/CompilerStack.h +++ b/libsolidity/interface/CompilerStack.h @@ -153,6 +153,9 @@ 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; } + /// Parses all source units that were added /// @returns false on error. bool parse(); @@ -188,6 +191,10 @@ public: /// start line, start column, end line, end column std::tuple<int, int, int, int> positionFromSourceLocation(langutil::SourceLocation const& _sourceLocation) const; + /// @returns a list of unhandled queries to the SMT solver (has to be supplied in a second run + /// by calling @a addSMTLib2Response). + std::vector<std::string> const& unhandledSMTLib2Queries() const { return m_unhandledSMTLib2Queries; } + /// @returns a list of the contract names in the sources. std::vector<std::string> contractNames() const; @@ -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<Remapping> m_remappings; std::map<std::string const, Source> m_sources; + std::vector<std::string> m_unhandledSMTLib2Queries; + std::map<h256, std::string> m_smtlib2Responses; std::shared_ptr<GlobalContext> m_globalContext; std::vector<Source const*> m_sourceOrder; /// This is updated during compilation. diff --git a/libsolidity/interface/StandardCompiler.cpp b/libsolidity/interface/StandardCompiler.cpp index 291a1071..bf33b789 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["smtlib2responses"]; + 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.unhandledSMTLib2Queries().empty()) + for (string const& query: m_compilerStack.unhandledSMTLib2Queries()) + output["auxiliaryInputRequested"]["smtlib2queries"]["0x" + keccak256(query).hex()] = query; + output["sources"] = Json::objectValue; unsigned sourceIndex = 0; for (string const& sourceName: analysisSuccess ? m_compilerStack.sourceNames() : vector<string>()) diff --git a/test/boostTest.cpp b/test/boostTest.cpp index 5352ef85..6ff6d2d2 100644 --- a/test/boostTest.cpp +++ b/test/boostTest.cpp @@ -38,6 +38,7 @@ #include <test/Options.h> #include <test/libsolidity/ASTJSONTest.h> #include <test/libsolidity/SyntaxTest.h> +#include <test/libsolidity/SMTCheckerJSONTest.h> #include <test/libyul/YulOptimizerTest.h> #include <boost/algorithm/string.hpp> @@ -146,12 +147,21 @@ test_suite* init_unit_test_suite( int /*argc*/, char* /*argv*/[] ) dev::yul::test::YulOptimizerTest::create ) > 0, "no Yul Optimizer tests found"); if (!dev::test::Options::get().disableSMT) + { solAssert(registerTests( master, dev::test::Options::get().testPath / "libsolidity", "smtCheckerTests", SyntaxTest::create ) > 0, "no SMT checker tests found"); + + solAssert(registerTests( + master, + dev::test::Options::get().testPath / "libsolidity", + "smtCheckerTestsJSON", + SMTCheckerTest::create + ) > 0, "no SMT checker JSON tests found"); + } if (dev::test::Options::get().disableIPC) { for (auto suite: { diff --git a/test/libsolidity/SMTCheckerJSONTest.cpp b/test/libsolidity/SMTCheckerJSONTest.cpp new file mode 100644 index 00000000..6e1329a9 --- /dev/null +++ b/test/libsolidity/SMTCheckerJSONTest.cpp @@ -0,0 +1,128 @@ +/* + 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/SMTCheckerJSONTest.h> +#include <test/Options.h> +#include <libsolidity/interface/StandardCompiler.h> +#include <libdevcore/JSON.h> +#include <boost/algorithm/string.hpp> +#include <boost/algorithm/string/join.hpp> +#include <boost/algorithm/string/predicate.hpp> +#include <boost/throw_exception.hpp> +#include <fstream> +#include <memory> +#include <stdexcept> +#include <sstream> + +using namespace dev; +using namespace solidity; +using namespace dev::solidity::test; +using namespace dev::solidity::test::formatting; +using namespace std; +using namespace boost::unit_test; + +SMTCheckerTest::SMTCheckerTest(string const& _filename) +: SyntaxTest(_filename) +{ + BOOST_REQUIRE_MESSAGE(boost::algorithm::ends_with(_filename, ".sol"), "Invalid test contract file name: \"" + _filename + "\"."); + + string jsonFilename = _filename.substr(0, _filename.size() - 4) + ".json"; + BOOST_CHECK(jsonParseFile(jsonFilename, m_smtResponses)); + BOOST_CHECK(m_smtResponses.isObject()); +} + +bool SMTCheckerTest::run(ostream& _stream, string const& _linePrefix, bool const _formatted) +{ + StandardCompiler compiler; + + // Run the compiler and retrieve the smtlib2queries (1st run) + string versionPragma = "pragma solidity >=0.0;\n"; + Json::Value input = buildJson(versionPragma); + Json::Value result = compiler.compile(input); + + // This is the list of query hashes requested by the 1st run + vector<string> outHashes = hashesFromJson(result, "auxiliaryInputRequested", "smtlib2queries"); + + // This is the list of responses provided in the test + string auxInput("auxiliaryInput"); + BOOST_CHECK(m_smtResponses.isMember(auxInput)); + vector<string> inHashes = hashesFromJson(m_smtResponses, auxInput, "smtlib2responses"); + + // Ensure that the provided list matches the requested one + BOOST_CHECK_MESSAGE( + outHashes == inHashes, + "SMT query hashes differ: " + boost::algorithm::join(outHashes, ", ") + " x " + boost::algorithm::join(inHashes, ", ") + ); + + // Rerun the compiler with the provided hashed (2nd run) + input[auxInput] = m_smtResponses[auxInput]; + Json::Value endResult = compiler.compile(input); + + BOOST_CHECK(endResult.isMember("errors")); + Json::Value const& errors = endResult["errors"]; + for (auto const& error: errors) + { + BOOST_CHECK(error.isMember("type") && error["type"].isString()); + BOOST_CHECK(error.isMember("message") && error["message"].isString()); + if (!error.isMember("sourceLocation")) + continue; + Json::Value const& location = error["sourceLocation"]; + BOOST_CHECK(location.isMember("start") && location["start"].isInt()); + BOOST_CHECK(location.isMember("end") && location["end"].isInt()); + int start = location["start"].asInt(); + int end = location["end"].asInt(); + if (start >= static_cast<int>(versionPragma.size())) + start -= versionPragma.size(); + if (end >= static_cast<int>(versionPragma.size())) + end -= versionPragma.size(); + m_errorList.emplace_back(SyntaxTestError{ + error["type"].asString(), + error["message"].asString(), + start, + end + }); + } + + return printExpectationAndError(_stream, _linePrefix, _formatted); +} + +vector<string> SMTCheckerTest::hashesFromJson(Json::Value const& _jsonObj, string const& _auxInput, string const& _smtlib) +{ + vector<string> hashes; + Json::Value const& auxInputs = _jsonObj[_auxInput]; + if (!!auxInputs) + { + Json::Value const& smtlib = auxInputs[_smtlib]; + if (!!smtlib) + for (auto const& hashString: smtlib.getMemberNames()) + hashes.push_back(hashString); + } + return hashes; +} + +Json::Value SMTCheckerTest::buildJson(string const& _extra) +{ + string language = "\"language\": \"Solidity\""; + string sourceName = "\"A\""; + string sourceContent = "\"" + _extra + m_source + "\""; + string sourceObj = "{ \"content\": " + sourceContent + "}"; + string sources = " \"sources\": { " + sourceName + ": " + sourceObj + "}"; + string input = "{" + language + ", " + sources + "}"; + Json::Value source; + BOOST_REQUIRE(jsonParse(input, source)); + return source; +} diff --git a/test/libsolidity/SMTCheckerJSONTest.h b/test/libsolidity/SMTCheckerJSONTest.h new file mode 100644 index 00000000..cf41acac --- /dev/null +++ b/test/libsolidity/SMTCheckerJSONTest.h @@ -0,0 +1,53 @@ +/* + 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 <libdevcore/JSON.h> + +#include <string> + +namespace dev +{ +namespace solidity +{ +namespace test +{ + +class SMTCheckerTest: public SyntaxTest +{ +public: + static std::unique_ptr<TestCase> create(std::string const& _filename) + { + return std::unique_ptr<TestCase>(new SMTCheckerTest(_filename)); + } + SMTCheckerTest(std::string const& _filename); + + bool run(std::ostream& _stream, std::string const& _linePrefix = "", bool const _formatted = false) override; + +private: + std::vector<std::string> hashesFromJson(Json::Value const& _jsonObj, std::string const& _auxInput, std::string const& _smtlib); + Json::Value buildJson(std::string const& _extra); + + Json::Value m_smtResponses; +}; + +} +} +} diff --git a/test/libsolidity/SyntaxTest.cpp b/test/libsolidity/SyntaxTest.cpp index 45d32b55..c47ea599 100644 --- a/test/libsolidity/SyntaxTest.cpp +++ b/test/libsolidity/SyntaxTest.cpp @@ -92,6 +92,11 @@ bool SyntaxTest::run(ostream& _stream, string const& _linePrefix, bool const _fo }); } + return printExpectationAndError(_stream, _linePrefix, _formatted); +} + +bool SyntaxTest::printExpectationAndError(ostream& _stream, string const& _linePrefix, bool const _formatted) +{ if (m_expectations != m_errorList) { string nextIndentLevel = _linePrefix + " "; diff --git a/test/libsolidity/SyntaxTest.h b/test/libsolidity/SyntaxTest.h index 0f151e66..d286f934 100644 --- a/test/libsolidity/SyntaxTest.h +++ b/test/libsolidity/SyntaxTest.h @@ -67,7 +67,7 @@ public: } static std::string errorMessage(Exception const& _e); -private: +protected: static void printErrorList( std::ostream& _stream, std::vector<SyntaxTestError> const& _errors, @@ -75,6 +75,8 @@ private: bool const _formatted = false ); + virtual bool printExpectationAndError(std::ostream& _stream, std::string const& _linePrefix = "", bool const _formatted = false); + static std::vector<SyntaxTestError> parseExpectations(std::istream& _stream); std::string m_source; diff --git a/test/libsolidity/smtCheckerTestsJSON/multi.json b/test/libsolidity/smtCheckerTestsJSON/multi.json new file mode 100644 index 00000000..2ed5150d --- /dev/null +++ b/test/libsolidity/smtCheckerTestsJSON/multi.json @@ -0,0 +1,11 @@ +{ + "auxiliaryInput": + { + "smtlib2responses": + { + "0x0426cd198d1e7123a28ffac2b759a666b86508ad046babf5166500dd6d8ed308": "unsat\n(error \"line 31 column 26: model is not available\")", + "0xa51ca41ae407f5a727f27101cbc079834743cc8955f9f585582034ca634953f6": "sat\n((|EVALEXPR_0| 1))", + "0xe9477f683ff20aa57fcb08682150f86c5917e1d4c0686b278ab9b73446d0682c": "sat\n((|EVALEXPR_0| 0))" + } + } +} diff --git a/test/libsolidity/smtCheckerTestsJSON/multi.sol b/test/libsolidity/smtCheckerTestsJSON/multi.sol new file mode 100644 index 00000000..e0d69b1d --- /dev/null +++ b/test/libsolidity/smtCheckerTestsJSON/multi.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(uint x) public pure { + assert(x > 0); + assert(x > 100); + assert(x >= 0); + } +} +// ---- +// Warning: (82-95): Assertion violation happens here +// Warning: (99-114): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTestsJSON/simple.json b/test/libsolidity/smtCheckerTestsJSON/simple.json new file mode 100644 index 00000000..fd976b63 --- /dev/null +++ b/test/libsolidity/smtCheckerTestsJSON/simple.json @@ -0,0 +1,9 @@ +{ + "auxiliaryInput": + { + "smtlib2responses": + { + "0xe9477f683ff20aa57fcb08682150f86c5917e1d4c0686b278ab9b73446d0682c": "sat\n((|EVALEXPR_0| 0))" + } + } +} diff --git a/test/libsolidity/smtCheckerTestsJSON/simple.sol b/test/libsolidity/smtCheckerTestsJSON/simple.sol new file mode 100644 index 00000000..6bc7193d --- /dev/null +++ b/test/libsolidity/smtCheckerTestsJSON/simple.sol @@ -0,0 +1,10 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(uint x) public pure { + assert(x > 0); + } +} +// ---- +// Warning: (82-95): Assertion violation happens here diff --git a/test/tools/CMakeLists.txt b/test/tools/CMakeLists.txt index 19a1d958..a0fbe140 100644 --- a/test/tools/CMakeLists.txt +++ b/test/tools/CMakeLists.txt @@ -6,5 +6,5 @@ target_link_libraries(yulopti PRIVATE solidity ${Boost_PROGRAM_OPTIONS_LIBRARIES add_executable(isoltest isoltest.cpp ../Options.cpp ../Common.cpp ../libsolidity/TestCase.cpp ../libsolidity/SyntaxTest.cpp ../libsolidity/AnalysisFramework.cpp ../libsolidity/SolidityExecutionFramework.cpp ../ExecutionFramework.cpp - ../RPCSession.cpp ../libsolidity/ASTJSONTest.cpp ../libyul/YulOptimizerTest.cpp) + ../RPCSession.cpp ../libsolidity/ASTJSONTest.cpp ../libsolidity/SMTCheckerJSONTest.cpp ../libyul/YulOptimizerTest.cpp) target_link_libraries(isoltest PRIVATE libsolc solidity evmasm ${Boost_PROGRAM_OPTIONS_LIBRARIES} ${Boost_UNIT_TEST_FRAMEWORK_LIBRARIES}) diff --git a/test/tools/isoltest.cpp b/test/tools/isoltest.cpp index 1b6fd54a..f8e2dc58 100644 --- a/test/tools/isoltest.cpp +++ b/test/tools/isoltest.cpp @@ -21,6 +21,7 @@ #include <test/libsolidity/AnalysisFramework.h> #include <test/libsolidity/SyntaxTest.h> #include <test/libsolidity/ASTJSONTest.h> +#include <test/libsolidity/SMTCheckerJSONTest.h> #include <test/libyul/YulOptimizerTest.h> #include <boost/algorithm/string.hpp> @@ -412,6 +413,17 @@ Allowed options)", global_stats += *stats; else return 1; + + if (auto stats = runTestSuite( + "SMT Checker JSON", + testPath / "libsolidity", + "smtCheckerTestsJSON", + SMTCheckerTest::create, + formatted + )) + global_stats += *stats; + else + return 1; } cout << endl << "Summary: "; |