mirror of
https://github.com/ethereum/solidity
synced 2023-10-03 13:03:40 +00:00
Add SMTChecker tests for standard JSON
This commit is contained in:
Leonardo Alt
committed by
Alex Beregszaszi
Alex Beregszaszi
parent
6251a289dd
commit
0ff4cbe51b
@@ -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;
|
||||
}
|
||||
@@ -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;
|
||||
};
|
||||
|
||||
}
|
||||
}
|
||||
}
|
||||
@@ -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 + " ";
|
||||
|
||||
@@ -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;
|
||||
|
||||
@@ -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))"
|
||||
}
|
||||
}
|
||||
}
|
||||
@@ -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
|
||||
@@ -0,0 +1,9 @@
|
||||
{
|
||||
"auxiliaryInput":
|
||||
{
|
||||
"smtlib2responses":
|
||||
{
|
||||
"0xe9477f683ff20aa57fcb08682150f86c5917e1d4c0686b278ab9b73446d0682c": "sat\n((|EVALEXPR_0| 0))"
|
||||
}
|
||||
}
|
||||
}
|
||||
@@ -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
|
||||
Reference in New Issue
Block a user