mirror of
https://github.com/ethereum/solidity
synced 2023-10-03 13:03:40 +00:00
Merge pull request #5527 from ethereum/smt_json_testcases
Remove boost test checks from SMTCheckerJSONTest
This commit is contained in:
commit
47bd906541
@ -38,11 +38,15 @@ using namespace boost::unit_test;
|
|||||||
SMTCheckerTest::SMTCheckerTest(string const& _filename)
|
SMTCheckerTest::SMTCheckerTest(string const& _filename)
|
||||||
: SyntaxTest(_filename)
|
: SyntaxTest(_filename)
|
||||||
{
|
{
|
||||||
BOOST_REQUIRE_MESSAGE(boost::algorithm::ends_with(_filename, ".sol"), "Invalid test contract file name: \"" + _filename + "\".");
|
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";
|
string jsonFilename = _filename.substr(0, _filename.size() - 4) + ".json";
|
||||||
BOOST_CHECK(jsonParseFile(jsonFilename, m_smtResponses));
|
if (
|
||||||
BOOST_CHECK(m_smtResponses.isObject());
|
!jsonParseFile(jsonFilename, m_smtResponses) ||
|
||||||
|
!m_smtResponses.isObject()
|
||||||
|
)
|
||||||
|
BOOST_THROW_EXCEPTION(runtime_error("Invalid JSON file."));
|
||||||
}
|
}
|
||||||
|
|
||||||
bool SMTCheckerTest::run(ostream& _stream, string const& _linePrefix, bool const _formatted)
|
bool SMTCheckerTest::run(ostream& _stream, string const& _linePrefix, bool const _formatted)
|
||||||
@ -59,42 +63,62 @@ bool SMTCheckerTest::run(ostream& _stream, string const& _linePrefix, bool const
|
|||||||
|
|
||||||
// This is the list of responses provided in the test
|
// This is the list of responses provided in the test
|
||||||
string auxInput("auxiliaryInput");
|
string auxInput("auxiliaryInput");
|
||||||
BOOST_CHECK(m_smtResponses.isMember(auxInput));
|
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");
|
vector<string> inHashes = hashesFromJson(m_smtResponses, auxInput, "smtlib2responses");
|
||||||
|
|
||||||
// Ensure that the provided list matches the requested one
|
// Ensure that the provided list matches the requested one
|
||||||
BOOST_CHECK_MESSAGE(
|
if (outHashes != inHashes)
|
||||||
outHashes == inHashes,
|
BOOST_THROW_EXCEPTION(runtime_error(
|
||||||
"SMT query hashes differ: " + boost::algorithm::join(outHashes, ", ") + " x " + boost::algorithm::join(inHashes, ", ")
|
"SMT query hashes differ: " +
|
||||||
);
|
boost::algorithm::join(outHashes, ", ") +
|
||||||
|
" x " +
|
||||||
|
boost::algorithm::join(inHashes, ", ")
|
||||||
|
));
|
||||||
|
|
||||||
// Rerun the compiler with the provided hashed (2nd run)
|
// Rerun the compiler with the provided hashed (2nd run)
|
||||||
input[auxInput] = m_smtResponses[auxInput];
|
input[auxInput] = m_smtResponses[auxInput];
|
||||||
Json::Value endResult = compiler.compile(input);
|
Json::Value endResult = compiler.compile(input);
|
||||||
|
|
||||||
BOOST_CHECK(endResult.isMember("errors"));
|
if (endResult.isMember("errors") && endResult["errors"].isArray())
|
||||||
Json::Value const& errors = endResult["errors"];
|
|
||||||
for (auto const& error: errors)
|
|
||||||
{
|
{
|
||||||
BOOST_CHECK(error.isMember("type") && error["type"].isString());
|
Json::Value const& errors = endResult["errors"];
|
||||||
BOOST_CHECK(error.isMember("message") && error["message"].isString());
|
for (auto const& error: errors)
|
||||||
if (!error.isMember("sourceLocation"))
|
{
|
||||||
continue;
|
if (
|
||||||
Json::Value const& location = error["sourceLocation"];
|
!error.isMember("type") ||
|
||||||
BOOST_CHECK(location.isMember("start") && location["start"].isInt());
|
!error["type"].isString()
|
||||||
BOOST_CHECK(location.isMember("end") && location["end"].isInt());
|
)
|
||||||
int start = location["start"].asInt();
|
BOOST_THROW_EXCEPTION(runtime_error("Error must have a type."));
|
||||||
int end = location["end"].asInt();
|
if (
|
||||||
if (start >= static_cast<int>(versionPragma.size()))
|
!error.isMember("message") ||
|
||||||
start -= versionPragma.size();
|
!error["message"].isString()
|
||||||
if (end >= static_cast<int>(versionPragma.size()))
|
)
|
||||||
end -= versionPragma.size();
|
BOOST_THROW_EXCEPTION(runtime_error("Error must have a message."));
|
||||||
m_errorList.emplace_back(SyntaxTestError{
|
if (!error.isMember("sourceLocation"))
|
||||||
error["type"].asString(),
|
continue;
|
||||||
error["message"].asString(),
|
Json::Value const& location = error["sourceLocation"];
|
||||||
start,
|
if (
|
||||||
end
|
!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();
|
||||||
|
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);
|
return printExpectationAndError(_stream, _linePrefix, _formatted);
|
||||||
@ -123,6 +147,7 @@ Json::Value SMTCheckerTest::buildJson(string const& _extra)
|
|||||||
string sources = " \"sources\": { " + sourceName + ": " + sourceObj + "}";
|
string sources = " \"sources\": { " + sourceName + ": " + sourceObj + "}";
|
||||||
string input = "{" + language + ", " + sources + "}";
|
string input = "{" + language + ", " + sources + "}";
|
||||||
Json::Value source;
|
Json::Value source;
|
||||||
BOOST_REQUIRE(jsonParse(input, source));
|
if (!jsonParse(input, source))
|
||||||
|
BOOST_THROW_EXCEPTION(runtime_error("Could not build JSON from string."));
|
||||||
return source;
|
return source;
|
||||||
}
|
}
|
||||||
|
Loading…
Reference in New Issue
Block a user