From 8eba66daf9cd9e50d52d838a3ec0dc32ce95fa65 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Wed, 23 Sep 2020 17:55:55 +0200 Subject: [PATCH] Extract boost smt and remove unused tests --- test/CMakeLists.txt | 3 - test/InteractiveTests.h | 1 - test/boostTest.cpp | 3 - test/libsolidity/SMTChecker.cpp | 143 -------------- test/libsolidity/SMTCheckerJSONTest.cpp | 176 ------------------ test/libsolidity/SMTCheckerJSONTest.h | 48 ----- .../smtCheckerTests/imports/import_base.sol | 25 +++ .../imports/import_library.sol | 19 ++ test/tools/CMakeLists.txt | 1 - 9 files changed, 44 insertions(+), 375 deletions(-) delete mode 100644 test/libsolidity/SMTChecker.cpp delete mode 100644 test/libsolidity/SMTCheckerJSONTest.cpp delete mode 100644 test/libsolidity/SMTCheckerJSONTest.h create mode 100644 test/libsolidity/smtCheckerTests/imports/import_base.sol create mode 100644 test/libsolidity/smtCheckerTests/imports/import_library.sol diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt index 3567f20ce..052929c09 100644 --- a/test/CMakeLists.txt +++ b/test/CMakeLists.txt @@ -79,9 +79,6 @@ set(libsolidity_sources libsolidity/SemanticTest.cpp libsolidity/SemanticTest.h libsolidity/SemVerMatcher.cpp - libsolidity/SMTChecker.cpp - libsolidity/SMTCheckerJSONTest.cpp - libsolidity/SMTCheckerJSONTest.h libsolidity/SMTCheckerTest.cpp libsolidity/SMTCheckerTest.h libsolidity/SolidityCompiler.cpp diff --git a/test/InteractiveTests.h b/test/InteractiveTests.h index 7ecc8de5e..2daf716aa 100644 --- a/test/InteractiveTests.h +++ b/test/InteractiveTests.h @@ -25,7 +25,6 @@ #include #include #include -#include #include #include #include diff --git a/test/boostTest.cpp b/test/boostTest.cpp index 18a5a2ea8..81aae19ab 100644 --- a/test/boostTest.cpp +++ b/test/boostTest.cpp @@ -205,9 +205,6 @@ test_suite* init_unit_test_suite( int /*argc*/, char* /*argv*/[] ) removeTestSuite(suite); } - if (solidity::test::CommonOptions::get().disableSMT) - removeTestSuite("SMTChecker"); - return nullptr; } diff --git a/test/libsolidity/SMTChecker.cpp b/test/libsolidity/SMTChecker.cpp deleted file mode 100644 index a7347a21a..000000000 --- a/test/libsolidity/SMTChecker.cpp +++ /dev/null @@ -1,143 +0,0 @@ -/* - 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 . -*/ -/** - * Unit tests for the SMT checker. - */ - -#include -#include - -#include - -#include - -using namespace std; -using namespace solidity::langutil; - -namespace solidity::frontend::test -{ - -class SMTCheckerFramework: public AnalysisFramework -{ -protected: - std::pair - parseAnalyseAndReturnError( - std::string const& _source, - bool _reportWarnings = false, - bool _insertLicenseAndVersionPragma = true, - bool _allowMultipleErrors = false, - bool _allowRecoveryErrors = false - ) override - { - return AnalysisFramework::parseAnalyseAndReturnError( - "pragma experimental SMTChecker;\n" + _source, - _reportWarnings, - _insertLicenseAndVersionPragma, - _allowMultipleErrors, - _allowRecoveryErrors - ); - } -}; - -BOOST_FIXTURE_TEST_SUITE(SMTChecker, SMTCheckerFramework) - -BOOST_AUTO_TEST_CASE(import_base, *boost::unit_test::label("no_options")) -{ - CompilerStack c; - c.setSources({ - {"base", R"( - pragma solidity >=0.0; - contract Base { - uint x; - address a; - function f() internal returns (uint) { - a = address(this); - ++x; - return 2; - } - } - )"}, - {"der", R"( - pragma solidity >=0.0; - pragma experimental SMTChecker; - import "base"; - contract Der is Base { - function g(uint y) public { - x += f(); - assert(y > x); - } - } - )"} - }); - c.setEVMVersion(solidity::test::CommonOptions::get().evmVersion()); - BOOST_CHECK(c.compile()); - - unsigned asserts = 0; - for (auto const& e: c.errors()) - { - string const* msg = e->comment(); - BOOST_REQUIRE(msg); - if (msg->find("Assertion violation") != string::npos) - ++asserts; - } - BOOST_CHECK_EQUAL(asserts, 1); -} - -BOOST_AUTO_TEST_CASE(import_library, *boost::unit_test::label("no_options")) -{ - CompilerStack c; - c.setSources({ - {"lib", R"( - pragma solidity >=0.0; - library L { - uint constant one = 1; - function f() internal pure returns (uint) { - return one; - } - } - )"}, - {"c", R"( - pragma solidity >=0.0; - pragma experimental SMTChecker; - import "lib"; - contract C { - function g(uint x) public pure { - uint y = L.f(); - assert(x > y); - } - } - )"} - }); - c.setEVMVersion(solidity::test::CommonOptions::get().evmVersion()); - BOOST_CHECK(c.compile()); - - unsigned asserts = 0; - for (auto const& e: c.errors()) - { - string const* msg = e->comment(); - BOOST_REQUIRE(msg); - if (msg->find("Assertion violation") != string::npos) - ++asserts; - } - BOOST_CHECK_EQUAL(asserts, 1); - -} - - -BOOST_AUTO_TEST_SUITE_END() - -} diff --git a/test/libsolidity/SMTCheckerJSONTest.cpp b/test/libsolidity/SMTCheckerJSONTest.cpp deleted file mode 100644 index ca6608905..000000000 --- a/test/libsolidity/SMTCheckerJSONTest.cpp +++ /dev/null @@ -1,176 +0,0 @@ -/* - 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 . -*/ -// SPDX-License-Identifier: GPL-3.0 - -#include -#include - -#include -#include -#include -#include - -#include -#include -#include -#include -#include - -#include -#include -#include -#include - -using namespace std; -using namespace solidity; -using namespace solidity::frontend; -using namespace solidity::frontend::test; -using namespace solidity::util; -using namespace solidity::util::formatting; -using namespace boost::unit_test; - -SMTCheckerJSONTest::SMTCheckerJSONTest(string const& _filename, langutil::EVMVersion _evmVersion) -: SyntaxTest(_filename, _evmVersion) -{ - if (!boost::algorithm::ends_with(_filename, ".sol")) - BOOST_THROW_EXCEPTION(runtime_error("Invalid test contract file name: \"" + _filename + "\".")); - - string jsonFilename = _filename.substr(0, _filename.size() - 4) + ".json"; - if ( - !jsonParseStrict(readFileAsString(jsonFilename), m_smtResponses) || - !m_smtResponses.isObject() - ) - BOOST_THROW_EXCEPTION(runtime_error("Invalid JSON file.")); - - if (ModelChecker::availableSolvers().none()) - m_shouldRun = false; -} - -TestCase::TestResult SMTCheckerJSONTest::run(ostream& _stream, string const& _linePrefix, bool _formatted) -{ - StandardCompiler compiler; - - // Run the compiler and retrieve the smtlib2queries (1st run) - string preamble = "pragma solidity >=0.0;\n// SPDX-License-Identifier: GPL-3.0\n"; - Json::Value input = buildJson(preamble); - Json::Value result = compiler.compile(input); - - // This is the list of query hashes requested by the 1st run - vector outHashes = hashesFromJson(result, "auxiliaryInputRequested", "smtlib2queries"); - - // This is the list of responses provided in the test - string auxInput("auxiliaryInput"); - if (!m_smtResponses.isMember(auxInput)) - BOOST_THROW_EXCEPTION(runtime_error("JSON file does not contain field \"auxiliaryInput\".")); - - vector inHashes = hashesFromJson(m_smtResponses, auxInput, "smtlib2responses"); - - // Ensure that the provided list matches the requested one - if (outHashes != inHashes) - BOOST_THROW_EXCEPTION(runtime_error( - "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); - - if (endResult.isMember("errors") && endResult["errors"].isArray()) - { - Json::Value const& errors = endResult["errors"]; - for (auto const& error: errors) - { - if ( - !error.isMember("type") || - !error["type"].isString() - ) - BOOST_THROW_EXCEPTION(runtime_error("Error must have a type.")); - if ( - !error.isMember("message") || - !error["message"].isString() - ) - BOOST_THROW_EXCEPTION(runtime_error("Error must have a message.")); - if (!error.isMember("sourceLocation")) - continue; - Json::Value const& location = error["sourceLocation"]; - if ( - !location.isMember("start") || - !location["start"].isInt() || - !location.isMember("end") || - !location["end"].isInt() - ) - BOOST_THROW_EXCEPTION(runtime_error("Error must have a SourceLocation with start and end.")); - size_t start = location["start"].asUInt(); - size_t end = location["end"].asUInt(); - std::string sourceName; - if (location.isMember("source") && location["source"].isString()) - sourceName = location["source"].asString(); - if (start >= preamble.size()) - start -= preamble.size(); - if (end >= preamble.size()) - end -= preamble.size(); - m_errorList.emplace_back(SyntaxTestError{ - error["type"].asString(), - error["errorId"].isNull() ? nullopt : optional(langutil::ErrorId{error["errorId"].asUInt()}), - error["message"].asString(), - sourceName, - static_cast(start), - static_cast(end) - }); - } - } - - return conclude(_stream, _linePrefix, _formatted); -} - -vector SMTCheckerJSONTest::hashesFromJson(Json::Value const& _jsonObj, string const& _auxInput, string const& _smtlib) -{ - vector 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 SMTCheckerJSONTest::buildJson(string const& _extra) -{ - string language = "\"language\": \"Solidity\""; - string sources = " \"sources\": { "; - bool first = true; - for (auto [sourceName, sourceContent]: m_sources) - { - string sourceObj = "{ \"content\": \"" + _extra + sourceContent + "\"}"; - if (!first) - sources += ", "; - sources += "\"" + sourceName + "\": " + sourceObj; - first = false; - } - sources += "}"; - string input = "{" + language + ", " + sources + "}"; - Json::Value source; - if (!jsonParseStrict(input, source)) - BOOST_THROW_EXCEPTION(runtime_error("Could not build JSON from string: " + input)); - return source; -} diff --git a/test/libsolidity/SMTCheckerJSONTest.h b/test/libsolidity/SMTCheckerJSONTest.h deleted file mode 100644 index 6de7f36c9..000000000 --- a/test/libsolidity/SMTCheckerJSONTest.h +++ /dev/null @@ -1,48 +0,0 @@ -/* - 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 . -*/ -// SPDX-License-Identifier: GPL-3.0 - -#pragma once - -#include - -#include - -#include - -namespace solidity::frontend::test -{ - -class SMTCheckerJSONTest: public SyntaxTest -{ -public: - static std::unique_ptr create(Config const& _config) - { - return std::make_unique(_config.filename, _config.evmVersion); - } - SMTCheckerJSONTest(std::string const& _filename, langutil::EVMVersion _evmVersion); - - TestResult run(std::ostream& _stream, std::string const& _linePrefix = "", bool _formatted = false) override; - -private: - std::vector 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/smtCheckerTests/imports/import_base.sol b/test/libsolidity/smtCheckerTests/imports/import_base.sol new file mode 100644 index 000000000..a65f8b3f5 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/imports/import_base.sol @@ -0,0 +1,25 @@ +==== Source: base ==== +contract Base { + uint x; + address a; + function f() internal returns (uint) { + a = address(this); + ++x; + return 2; + } +} +==== Source: der ==== +pragma experimental SMTChecker; +import "base"; +contract Der is Base { + function g(uint y) public { + x += f(); + assert(y > x); + } +} +// ---- +// Warning 1218: (der:101-109): Error trying to invoke SMT solver. +// Warning 6328: (der:113-126): Assertion violation happens here. +// Warning 2661: (base:100-103): Overflow (resulting value larger than 2**256 - 1) happens here. +// Warning 2661: (der:101-109): Overflow (resulting value larger than 2**256 - 1) happens here. +// Warning 2661: (base:100-103): Overflow (resulting value larger than 2**256 - 1) happens here. diff --git a/test/libsolidity/smtCheckerTests/imports/import_library.sol b/test/libsolidity/smtCheckerTests/imports/import_library.sol new file mode 100644 index 000000000..b6c6702bc --- /dev/null +++ b/test/libsolidity/smtCheckerTests/imports/import_library.sol @@ -0,0 +1,19 @@ +==== Source: c ==== +pragma experimental SMTChecker; +import "lib"; +contract C { + function g(uint x) public pure { + uint y = L.f(); + assert(x > y); + } +} +==== Source: lib ==== +library L { + uint constant one = 1; + function f() internal pure returns (uint) { + return one; + } +} +// ---- +// Warning 6328: (c:113-126): Assertion violation happens here. +// Warning 8364: (c:104-105): Assertion checker does not yet implement type type(library L) diff --git a/test/tools/CMakeLists.txt b/test/tools/CMakeLists.txt index c8add4ce7..dc0d58bce 100644 --- a/test/tools/CMakeLists.txt +++ b/test/tools/CMakeLists.txt @@ -31,7 +31,6 @@ add_executable(isoltest ../libsolidity/ABIJsonTest.cpp ../libsolidity/ASTJSONTest.cpp ../libsolidity/SMTCheckerTest.cpp - ../libsolidity/SMTCheckerJSONTest.cpp ../libyul/Common.cpp ../libyul/EwasmTranslationTest.cpp ../libyul/FunctionSideEffects.cpp