cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Merge pull request #9872 from ethereum/smt_remove_tests

Browse Source 
Extract boost smt and remove unused tests
This commit is contained in:
chriseth 2020-09-24 13:20:19 +02:00 committed by GitHub
commit a9f9b4db27
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
9 changed files with 44 additions and 375 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
test/CMakeLists.txt
View File

@ -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

1
test/InteractiveTests.h
View File

@ -25,7 +25,6 @@
#include <test/libsolidity/SyntaxTest.h>
#include <test/libsolidity/SemanticTest.h>
#include <test/libsolidity/SMTCheckerTest.h>
#include <test/libsolidity/SMTCheckerJSONTest.h>
#include <test/libyul/EwasmTranslationTest.h>
#include <test/libyul/YulOptimizerTest.h>
#include <test/libyul/YulInterpreterTest.h>

3
test/boostTest.cpp
View File

@ -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;
}

143
test/libsolidity/SMTChecker.cpp
View File

@ -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 <http://www.gnu.org/licenses/>.
*/
/**
* Unit tests for the SMT checker.
*/
#include <test/libsolidity/AnalysisFramework.h>
#include <test/Common.h>
#include <boost/test/unit_test.hpp>
#include <string>
using namespace std;
using namespace solidity::langutil;
namespace solidity::frontend::test
{
class SMTCheckerFramework: public AnalysisFramework
{
protected:
std::pair<SourceUnit const*, ErrorList>
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()
}

176
test/libsolidity/SMTCheckerJSONTest.cpp
View File

@ -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 <http://www.gnu.org/licenses/>.
*/
// SPDX-License-Identifier: GPL-3.0
#include <test/libsolidity/SMTCheckerJSONTest.h>
#include <test/Common.h>
#include <libsolidity/formal/ModelChecker.h>
#include <libsolidity/interface/StandardCompiler.h>
#include <libsolutil/CommonIO.h>
#include <libsolutil/JSON.h>
#include <boost/algorithm/string.hpp>
#include <boost/algorithm/string/join.hpp>
#include <boost/algorithm/string/predicate.hpp>
#include <boost/test/unit_test.hpp>
#include <boost/throw_exception.hpp>
#include <fstream>
#include <memory>
#include <stdexcept>
#include <sstream>
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<string> 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<string> 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>(langutil::ErrorId{error["errorId"].asUInt()}),
error["message"].asString(),
sourceName,
static_cast<int>(start),
static_cast<int>(end)
});
}
}
return conclude(_stream, _linePrefix, _formatted);
}
vector<string> SMTCheckerJSONTest::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 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;
}

48
test/libsolidity/SMTCheckerJSONTest.h
View File

@ -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 <http://www.gnu.org/licenses/>.
*/
// SPDX-License-Identifier: GPL-3.0
#pragma once
#include <test/libsolidity/SyntaxTest.h>
#include <libsolutil/JSON.h>
#include <string>
namespace solidity::frontend::test
{
class SMTCheckerJSONTest: public SyntaxTest
{
public:
static std::unique_ptr<TestCase> create(Config const& _config)
{
return std::make_unique<SMTCheckerJSONTest>(_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<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;
};
}

25
test/libsolidity/smtCheckerTests/imports/import_base.sol Normal file
View File

@ -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.

19
test/libsolidity/smtCheckerTests/imports/import_library.sol Normal file
View File

@ -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)

1
test/tools/CMakeLists.txt
View File

@ -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