2018-11-15 15:47:52 +00:00
|
|
|
/*
|
|
|
|
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>
|
2020-01-14 16:48:17 +00:00
|
|
|
#include <test/Common.h>
|
2020-03-10 12:41:10 +00:00
|
|
|
|
|
|
|
#include <libsolidity/formal/ModelChecker.h>
|
2018-11-15 15:47:52 +00:00
|
|
|
#include <libsolidity/interface/StandardCompiler.h>
|
2020-01-06 10:52:23 +00:00
|
|
|
#include <libsolutil/CommonIO.h>
|
|
|
|
#include <libsolutil/JSON.h>
|
2020-03-10 12:41:10 +00:00
|
|
|
|
2018-11-15 15:47:52 +00:00
|
|
|
#include <boost/algorithm/string.hpp>
|
|
|
|
#include <boost/algorithm/string/join.hpp>
|
|
|
|
#include <boost/algorithm/string/predicate.hpp>
|
2020-01-14 14:55:31 +00:00
|
|
|
#include <boost/test/unit_test.hpp>
|
2018-11-15 15:47:52 +00:00
|
|
|
#include <boost/throw_exception.hpp>
|
2020-03-10 12:41:10 +00:00
|
|
|
|
2018-11-15 15:47:52 +00:00
|
|
|
#include <fstream>
|
|
|
|
#include <memory>
|
|
|
|
#include <stdexcept>
|
|
|
|
#include <sstream>
|
|
|
|
|
|
|
|
using namespace std;
|
2019-12-23 15:50:30 +00:00
|
|
|
using namespace solidity;
|
|
|
|
using namespace solidity::frontend;
|
|
|
|
using namespace solidity::frontend::test;
|
|
|
|
using namespace solidity::util;
|
|
|
|
using namespace solidity::util::formatting;
|
2018-11-15 15:47:52 +00:00
|
|
|
using namespace boost::unit_test;
|
|
|
|
|
2019-12-03 15:50:28 +00:00
|
|
|
SMTCheckerJSONTest::SMTCheckerJSONTest(string const& _filename, langutil::EVMVersion _evmVersion)
|
2019-03-15 16:22:04 +00:00
|
|
|
: SyntaxTest(_filename, _evmVersion)
|
2018-11-15 15:47:52 +00:00
|
|
|
{
|
2018-11-28 12:03:51 +00:00
|
|
|
if (!boost::algorithm::ends_with(_filename, ".sol"))
|
|
|
|
BOOST_THROW_EXCEPTION(runtime_error("Invalid test contract file name: \"" + _filename + "\"."));
|
2018-11-15 15:47:52 +00:00
|
|
|
|
|
|
|
string jsonFilename = _filename.substr(0, _filename.size() - 4) + ".json";
|
2018-11-28 12:03:51 +00:00
|
|
|
if (
|
2019-12-03 14:13:52 +00:00
|
|
|
!jsonParseStrict(readFileAsString(jsonFilename), m_smtResponses) ||
|
2018-11-28 12:03:51 +00:00
|
|
|
!m_smtResponses.isObject()
|
|
|
|
)
|
|
|
|
BOOST_THROW_EXCEPTION(runtime_error("Invalid JSON file."));
|
2020-03-10 12:41:10 +00:00
|
|
|
|
|
|
|
if (ModelChecker::availableSolvers().none())
|
|
|
|
m_shouldRun = false;
|
2018-11-15 15:47:52 +00:00
|
|
|
}
|
|
|
|
|
2019-12-03 15:50:28 +00:00
|
|
|
TestCase::TestResult SMTCheckerJSONTest::run(ostream& _stream, string const& _linePrefix, bool _formatted)
|
2018-11-15 15:47:52 +00:00
|
|
|
{
|
|
|
|
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");
|
2018-11-28 12:03:51 +00:00
|
|
|
if (!m_smtResponses.isMember(auxInput))
|
|
|
|
BOOST_THROW_EXCEPTION(runtime_error("JSON file does not contain field \"auxiliaryInput\"."));
|
|
|
|
|
2018-11-15 15:47:52 +00:00
|
|
|
vector<string> inHashes = hashesFromJson(m_smtResponses, auxInput, "smtlib2responses");
|
|
|
|
|
|
|
|
// Ensure that the provided list matches the requested one
|
2018-11-28 12:03:51 +00:00
|
|
|
if (outHashes != inHashes)
|
|
|
|
BOOST_THROW_EXCEPTION(runtime_error(
|
|
|
|
"SMT query hashes differ: " +
|
|
|
|
boost::algorithm::join(outHashes, ", ") +
|
|
|
|
" x " +
|
|
|
|
boost::algorithm::join(inHashes, ", ")
|
|
|
|
));
|
2018-11-15 15:47:52 +00:00
|
|
|
|
|
|
|
// Rerun the compiler with the provided hashed (2nd run)
|
|
|
|
input[auxInput] = m_smtResponses[auxInput];
|
|
|
|
Json::Value endResult = compiler.compile(input);
|
|
|
|
|
2018-11-28 12:03:51 +00:00
|
|
|
if (endResult.isMember("errors") && endResult["errors"].isArray())
|
2018-11-15 15:47:52 +00:00
|
|
|
{
|
2018-11-28 12:03:51 +00:00
|
|
|
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."));
|
|
|
|
int start = location["start"].asInt();
|
|
|
|
int end = location["end"].asInt();
|
2019-08-16 12:50:31 +00:00
|
|
|
std::string sourceName;
|
|
|
|
if (location.isMember("source") && location["source"].isString())
|
|
|
|
sourceName = location["source"].asString();
|
2018-11-28 12:03:51 +00:00
|
|
|
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(),
|
2019-08-16 12:50:31 +00:00
|
|
|
sourceName,
|
2018-11-28 12:03:51 +00:00
|
|
|
start,
|
|
|
|
end
|
|
|
|
});
|
|
|
|
}
|
2018-11-15 15:47:52 +00:00
|
|
|
}
|
|
|
|
|
2019-05-07 13:33:22 +00:00
|
|
|
return printExpectationAndError(_stream, _linePrefix, _formatted) ? TestResult::Success : TestResult::Failure;
|
2018-11-15 15:47:52 +00:00
|
|
|
}
|
|
|
|
|
2019-12-03 15:50:28 +00:00
|
|
|
vector<string> SMTCheckerJSONTest::hashesFromJson(Json::Value const& _jsonObj, string const& _auxInput, string const& _smtlib)
|
2018-11-15 15:47:52 +00:00
|
|
|
{
|
|
|
|
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;
|
|
|
|
}
|
|
|
|
|
2019-12-03 15:50:28 +00:00
|
|
|
Json::Value SMTCheckerJSONTest::buildJson(string const& _extra)
|
2018-11-15 15:47:52 +00:00
|
|
|
{
|
|
|
|
string language = "\"language\": \"Solidity\"";
|
2019-08-16 12:50:31 +00:00
|
|
|
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 += "}";
|
2018-11-15 15:47:52 +00:00
|
|
|
string input = "{" + language + ", " + sources + "}";
|
|
|
|
Json::Value source;
|
2019-12-03 14:13:52 +00:00
|
|
|
if (!jsonParseStrict(input, source))
|
2019-08-16 12:50:31 +00:00
|
|
|
BOOST_THROW_EXCEPTION(runtime_error("Could not build JSON from string: " + input));
|
2018-11-15 15:47:52 +00:00
|
|
|
return source;
|
|
|
|
}
|