diff options
Diffstat (limited to 'test/libsolidity')
62 files changed, 768 insertions, 732 deletions
diff --git a/test/libsolidity/ASTJSONTest.h b/test/libsolidity/ASTJSONTest.h index 9760ef66..dcdaf221 100644 --- a/test/libsolidity/ASTJSONTest.h +++ b/test/libsolidity/ASTJSONTest.h @@ -18,7 +18,7 @@ #pragma once #include <test/libsolidity/FormattedScope.h> -#include <test/libsolidity/TestCase.h> +#include <test/TestCase.h> #include <iosfwd> #include <string> diff --git a/test/libsolidity/SMTChecker.cpp b/test/libsolidity/SMTChecker.cpp index 13fcc5b4..a49618bd 100644 --- a/test/libsolidity/SMTChecker.cpp +++ b/test/libsolidity/SMTChecker.cpp @@ -56,599 +56,6 @@ protected: BOOST_FIXTURE_TEST_SUITE(SMTChecker, SMTCheckerFramework) -BOOST_AUTO_TEST_CASE(smoke_test) -{ - string text = R"( - contract C { } - )"; - CHECK_SUCCESS_NO_WARNINGS(text); -} - -BOOST_AUTO_TEST_CASE(simple_overflow) -{ - string text = R"( - contract C { - function f(uint a, uint b) public pure returns (uint) { return a + b; } - } - )"; - CHECK_WARNING(text, "Overflow (resulting value larger than"); -} - -BOOST_AUTO_TEST_CASE(warn_on_typecast) -{ - string text = R"( - contract C { - function f() public pure returns (uint) { - return uint8(1); - } - } - )"; - CHECK_WARNING(text, "Assertion checker does not yet implement this expression."); -} - -BOOST_AUTO_TEST_CASE(warn_on_struct) -{ - string text = R"( - pragma experimental ABIEncoderV2; - contract C { - struct A { uint a; uint b; } - function f() public pure returns (A memory) { - return A({ a: 1, b: 2 }); - } - } - )"; - CHECK_WARNING_ALLOW_MULTI(text, (vector<string>{ - "Experimental feature", - "Assertion checker does not yet implement this expression.", - "Assertion checker does not yet support the type of this variable." - })); -} - -BOOST_AUTO_TEST_CASE(simple_assert) -{ - string text = R"( - contract C { - function f(uint a) public pure { assert(a == 2); } - } - )"; - CHECK_WARNING(text, "Assertion violation happens here"); -} - -BOOST_AUTO_TEST_CASE(simple_assert_with_require) -{ - string text = R"( - contract C { - function f(uint a) public pure { require(a < 10); assert(a < 20); } - } - )"; - CHECK_SUCCESS_NO_WARNINGS(text); -} - -BOOST_AUTO_TEST_CASE(assignment_in_declaration) -{ - string text = R"( - contract C { - function f() public pure { uint a = 2; assert(a == 2); } - } - )"; - CHECK_SUCCESS_NO_WARNINGS(text); -} - -BOOST_AUTO_TEST_CASE(branches_merge_variables) -{ - // Branch does not touch variable a - string text = R"( - contract C { - function f(uint x) public pure { - uint a = 3; - if (x > 10) { - } - assert(a == 3); - } - } - )"; - CHECK_SUCCESS_NO_WARNINGS(text); - // Positive branch touches variable a, but assertion should still hold. - text = R"( - contract C { - function f(uint x) public pure { - uint a = 3; - if (x > 10) { - a = 3; - } - assert(a == 3); - } - } - )"; - CHECK_SUCCESS_NO_WARNINGS(text); - // Negative branch touches variable a, but assertion should still hold. - text = R"( - contract C { - function f(uint x) public pure { - uint a = 3; - if (x > 10) { - } else { - a = 3; - } - assert(a == 3); - } - } - )"; - CHECK_SUCCESS_NO_WARNINGS(text); - // Variable is not merged, if it is only read. - text = R"( - contract C { - function f(uint x) public pure { - uint a = 3; - if (x > 10) { - assert(a == 3); - } else { - assert(a == 3); - } - assert(a == 3); - } - } - )"; - CHECK_SUCCESS_NO_WARNINGS(text); - // Variable is reset in both branches - text = R"( - contract C { - function f(uint x) public pure { - uint a = 2; - if (x > 10) { - a = 3; - } else { - a = 3; - } - assert(a == 3); - } - } - )"; - CHECK_SUCCESS_NO_WARNINGS(text); - // Variable is reset in both branches - text = R"( - contract C { - function f(uint x) public pure { - uint a = 2; - if (x > 10) { - a = 3; - } else { - a = 4; - } - assert(a >= 3); - } - } - )"; - CHECK_SUCCESS_NO_WARNINGS(text); -} - -BOOST_AUTO_TEST_CASE(branches_assert_condition) -{ - string text = R"( - contract C { - function f(uint x) public pure { - if (x > 10) { - assert(x > 9); - } - else - { - assert(x < 11); - } - } - } - )"; - CHECK_SUCCESS_NO_WARNINGS(text); - text = R"( - contract C { - function f(uint x) public pure { - if (x > 10) { - assert(x > 9); - } - else if (x > 2) - { - assert(x <= 10 && x > 2); - } - else - { - assert(0 <= x && x <= 2); - } - } - } - )"; - CHECK_SUCCESS_NO_WARNINGS(text); -} - -BOOST_AUTO_TEST_CASE(ways_to_merge_variables) -{ - string text = R"( - contract C { - function f(uint x) public pure { - uint a = 3; - if (x > 10) { - a++; - } - assert(a == 3); - } - } - )"; - CHECK_WARNING(text, "Assertion violation happens here"); - text = R"( - contract C { - function f(uint x) public pure { - uint a = 3; - if (x > 10) { - ++a; - } - assert(a == 3); - } - } - )"; - CHECK_WARNING(text, "Assertion violation happens here"); - text = R"( - contract C { - function f(uint x) public pure { - uint a = 3; - if (x > 10) { - a = 5; - } - assert(a == 3); - } - } - )"; - CHECK_WARNING(text, "Assertion violation happens here"); -} - -BOOST_AUTO_TEST_CASE(bool_simple) -{ - string text = R"( - contract C { - function f(bool x) public pure { - assert(x); - } - } - )"; - CHECK_WARNING(text, "Assertion violation happens here"); - text = R"( - contract C { - function f(bool x, bool y) public pure { - assert(x == y); - } - } - )"; - CHECK_WARNING(text, "Assertion violation happens here"); - text = R"( - contract C { - function f(bool x, bool y) public pure { - bool z = x || y; - assert(!(x && y) || z); - } - } - )"; - CHECK_SUCCESS_NO_WARNINGS(text); - text = R"( - contract C { - function f(bool x) public pure { - if (x) { - assert(x); - } else { - assert(!x); - } - } - } - )"; - CHECK_SUCCESS_NO_WARNINGS(text); - text = R"( - contract C { - function f(bool x) public pure { - bool y = x; - assert(x == y); - } - } - )"; - CHECK_SUCCESS_NO_WARNINGS(text); - text = R"( - contract C { - function f(bool x) public pure { - require(x); - bool y; - y = false; - assert(x || y); - } - } - )"; - CHECK_SUCCESS_NO_WARNINGS(text); -} - -BOOST_AUTO_TEST_CASE(bool_int_mixed) -{ - string text = R"( - contract C { - function f(bool x) public pure { - uint a; - if (x) - a = 1; - assert(!x || a > 0); - } - } - )"; - CHECK_SUCCESS_NO_WARNINGS(text); - text = R"( - contract C { - function f(bool x, uint a) public pure { - require(!x || a > 0); - uint b = a; - assert(!x || b > 0); - } - } - )"; - CHECK_SUCCESS_NO_WARNINGS(text); - text = R"( - contract C { - function f(bool x, bool y) public pure { - uint a; - if (x) { - if (y) { - a = 0; - } else { - a = 1; - } - } else { - if (y) { - a = 1; - } else { - a = 0; - } - } - bool xor_x_y = (x && !y) || (!x && y); - assert(!xor_x_y || a > 0); - } - } - )"; - CHECK_SUCCESS_NO_WARNINGS(text); -} - -BOOST_AUTO_TEST_CASE(storage_value_vars) -{ - string text = R"( - contract C - { - address a; - bool b; - uint c; - function f(uint x) public { - if (x == 0) - { - a = 0x0000000000000000000000000000000000000100; - b = true; - } - else - { - a = 0x0000000000000000000000000000000000000200; - b = false; - } - assert(a > 0x0000000000000000000000000000000000000000 && b); - } - } - )"; - CHECK_WARNING(text, "Assertion violation happens here"); - text = R"( - contract C - { - address a; - bool b; - uint c; - function f() public view { - assert(c > 0); - } - } - )"; - CHECK_WARNING(text, "Assertion violation happens here"); - text = R"( - contract C - { - function f(uint x) public { - if (x == 0) - { - a = 0x0000000000000000000000000000000000000100; - b = true; - } - else - { - a = 0x0000000000000000000000000000000000000200; - b = false; - } - assert(b == (a < 0x0000000000000000000000000000000000000200)); - } - - function g() public view { - require(a < 0x0000000000000000000000000000000000000100); - assert(c >= 0); - } - address a; - bool b; - uint c; - } - )"; - CHECK_SUCCESS_NO_WARNINGS(text); - text = R"( - contract C - { - function f() public view { - assert(c > 0); - } - uint c; - } - )"; - CHECK_WARNING(text, "Assertion violation happens here"); - -} - -BOOST_AUTO_TEST_CASE(while_loop_simple) -{ - // Check that variables are cleared - string text = R"( - contract C { - function f(uint x) public pure { - x = 2; - while (x > 1) { - x = 2; - } - assert(x == 2); - } - } - )"; - CHECK_WARNING(text, "Assertion violation happens here"); - // Check that condition is assumed. - text = R"( - contract C { - function f(uint x) public pure { - while (x == 2) { - assert(x == 2); - } - } - } - )"; - CHECK_SUCCESS_NO_WARNINGS(text); - // Check that condition is not assumed after the body anymore - text = R"( - contract C { - function f(uint x) public pure { - while (x == 2) { - } - assert(x == 2); - } - } - )"; - CHECK_WARNING(text, "Assertion violation happens here"); - // Check that negation of condition is not assumed after the body anymore - text = R"( - contract C { - function f(uint x) public pure { - while (x == 2) { - } - assert(x != 2); - } - } - )"; - CHECK_WARNING(text, "Assertion violation happens here"); - // Check that side-effects of condition are taken into account - text = R"( - contract C { - function f(uint x, uint y) public pure { - x = 7; - while ((x = y) > 0) { - } - assert(x == 7); - } - } - )"; - CHECK_WARNING(text, "Assertion violation happens here"); -} - -BOOST_AUTO_TEST_CASE(constant_condition) -{ - string text = R"( - contract C { - function f(uint x) public pure { - if (x >= 0) { revert(); } - } - } - )"; - CHECK_WARNING_ALLOW_MULTI(text, (vector<string>{ - "Condition is always true", - "Assertion checker does not yet implement this type of function call" - })); - text = R"( - contract C { - function f(uint x) public pure { - if (x >= 10) { if (x < 10) { revert(); } } - } - } - )"; - CHECK_WARNING_ALLOW_MULTI(text, (vector<string>{ - "Condition is always false", - "Assertion checker does not yet implement this type of function call" - })); - // a plain literal constant is fine - text = R"( - contract C { - function f(uint) public pure { - if (true) { revert(); } - } - } - )"; - CHECK_WARNING(text, "Assertion checker does not yet implement this type of function call"); -} - - -BOOST_AUTO_TEST_CASE(for_loop) -{ - string text = R"( - contract C { - function f(uint x) public pure { - require(x == 2); - for (;;) {} - assert(x == 2); - } - } - )"; - CHECK_SUCCESS_NO_WARNINGS(text); - text = R"( - contract C { - function f(uint x) public pure { - for (; x == 2; ) { - assert(x == 2); - } - } - } - )"; - CHECK_SUCCESS_NO_WARNINGS(text); - text = R"( - contract C { - function f(uint x) public pure { - for (uint y = 2; x < 10; ) { - assert(y == 2); - } - } - } - )"; - CHECK_SUCCESS_NO_WARNINGS(text); - text = R"( - contract C { - function f(uint x) public pure { - for (uint y = 2; x < 10; y = 3) { - assert(y == 2); - } - } - } - )"; - CHECK_WARNING(text, "Assertion violation"); - text = R"( - contract C { - function f(uint x) public pure { - uint y; - for (y = 2; x < 10; ) { - y = 3; - } - assert(y == 3); - } - } - )"; - CHECK_WARNING(text, "Assertion violation"); - text = R"( - contract C { - function f(uint x) public pure { - uint y; - for (y = 2; x < 10; ) { - y = 3; - } - assert(y == 2); - } - } - )"; - CHECK_WARNING(text, "Assertion violation"); -} - BOOST_AUTO_TEST_CASE(division) { string text = R"( diff --git a/test/libsolidity/SMTCheckerJSONTest.cpp b/test/libsolidity/SMTCheckerJSONTest.cpp new file mode 100644 index 00000000..6e1329a9 --- /dev/null +++ b/test/libsolidity/SMTCheckerJSONTest.cpp @@ -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; +} diff --git a/test/libsolidity/SMTCheckerJSONTest.h b/test/libsolidity/SMTCheckerJSONTest.h new file mode 100644 index 00000000..cf41acac --- /dev/null +++ b/test/libsolidity/SMTCheckerJSONTest.h @@ -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; +}; + +} +} +} diff --git a/test/libsolidity/SolidityEndToEndTest.cpp b/test/libsolidity/SolidityEndToEndTest.cpp index 041f29a8..e591432a 100644 --- a/test/libsolidity/SolidityEndToEndTest.cpp +++ b/test/libsolidity/SolidityEndToEndTest.cpp @@ -9388,6 +9388,25 @@ BOOST_AUTO_TEST_CASE(using_for_by_name) ABI_CHECK(callContractFunction("x()"), encodeArgs(u256(6 * 7))); } +BOOST_AUTO_TEST_CASE(bound_function_in_function) +{ + char const* sourceCode = R"( + library L { + function g(function() internal returns (uint) _t) internal returns (uint) { return _t(); } + } + contract C { + using L for *; + function f() public returns (uint) { + return t.g(); + } + function t() public pure returns (uint) { return 7; } + } + )"; + compileAndRun(sourceCode, 0, "L"); + compileAndRun(sourceCode, 0, "C", bytes(), map<string, Address>{{"L", m_contractAddress}}); + ABI_CHECK(callContractFunction("f()"), encodeArgs(u256(7))); +} + BOOST_AUTO_TEST_CASE(bound_function_in_var) { char const* sourceCode = R"( diff --git a/test/libsolidity/SyntaxTest.cpp b/test/libsolidity/SyntaxTest.cpp index 45d32b55..c47ea599 100644 --- a/test/libsolidity/SyntaxTest.cpp +++ b/test/libsolidity/SyntaxTest.cpp @@ -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 + " "; diff --git a/test/libsolidity/SyntaxTest.h b/test/libsolidity/SyntaxTest.h index 0f151e66..12c14087 100644 --- a/test/libsolidity/SyntaxTest.h +++ b/test/libsolidity/SyntaxTest.h @@ -19,7 +19,7 @@ #include <test/libsolidity/AnalysisFramework.h> #include <test/libsolidity/FormattedScope.h> -#include <test/libsolidity/TestCase.h> +#include <test/TestCase.h> #include <liblangutil/Exceptions.h> #include <iosfwd> @@ -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; diff --git a/test/libsolidity/TestCase.cpp b/test/libsolidity/TestCase.cpp deleted file mode 100644 index 17972269..00000000 --- a/test/libsolidity/TestCase.cpp +++ /dev/null @@ -1,56 +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/>. -*/ - -#include <test/libsolidity/TestCase.h> - -#include <boost/algorithm/string.hpp> -#include <boost/algorithm/string/predicate.hpp> - -#include <stdexcept> - -using namespace dev; -using namespace solidity; -using namespace dev::solidity::test; -using namespace std; - -bool TestCase::isTestFilename(boost::filesystem::path const& _filename) -{ - string extension = _filename.extension().string(); - return (extension == ".sol" || extension == ".yul") && - !boost::starts_with(_filename.string(), "~") && - !boost::starts_with(_filename.string(), "."); -} - -string TestCase::parseSource(istream& _stream) -{ - string source; - string line; - string const delimiter("// ----"); - while (getline(_stream, line)) - if (boost::algorithm::starts_with(line, delimiter)) - break; - else - source += line + "\n"; - return source; -} - -void TestCase::expect(string::iterator& _it, string::iterator _end, string::value_type _c) -{ - if (_it == _end || *_it != _c) - throw runtime_error(string("Invalid test expectation. Expected: \"") + _c + "\"."); - ++_it; -} diff --git a/test/libsolidity/TestCase.h b/test/libsolidity/TestCase.h deleted file mode 100644 index 3c05ae4e..00000000 --- a/test/libsolidity/TestCase.h +++ /dev/null @@ -1,80 +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/>. -*/ - -#pragma once - -#include <boost/filesystem.hpp> - -#include <iosfwd> -#include <memory> -#include <string> - -namespace dev -{ -namespace solidity -{ -namespace test -{ - -/** Common superclass of SyntaxTest and SemanticsTest. */ -class TestCase -{ -public: - using TestCaseCreator = std::unique_ptr<TestCase>(*)(std::string const&); - - virtual ~TestCase() {} - - /// Runs the test case. - /// Outputs error messages to @arg _stream. Each line of output is prefixed with @arg _linePrefix. - /// Optionally, color-coding can be enabled (if @arg _formatted is set to true). - /// @returns true, if the test case succeeds, false otherwise - virtual bool run(std::ostream& _stream, std::string const& _linePrefix = "", bool const _formatted = false) = 0; - - /// Outputs the test contract to @arg _stream. - /// Each line of output is prefixed with @arg _linePrefix. - /// If @arg _formatted is true, color-coding may be used to indicate - /// error locations in the contract, if applicable. - virtual void printSource(std::ostream &_stream, std::string const &_linePrefix = "", bool const _formatted = false) const = 0; - /// Outputs test expectations to @arg _stream that match the actual results of the test. - /// Each line of output is prefixed with @arg _linePrefix. - virtual void printUpdatedExpectations(std::ostream& _stream, std::string const& _linePrefix) const = 0; - - static bool isTestFilename(boost::filesystem::path const& _filename); - -protected: - static std::string parseSource(std::istream& _file); - static void expect(std::string::iterator& _it, std::string::iterator _end, std::string::value_type _c); - - template<typename IteratorType> - static void skipWhitespace(IteratorType& _it, IteratorType _end) - { - while (_it != _end && isspace(*_it)) - ++_it; - } - - template<typename IteratorType> - static void skipSlashes(IteratorType& _it, IteratorType _end) - { - while (_it != _end && *_it == '/') - ++_it; - } - -}; - -} -} -} diff --git a/test/libsolidity/smtCheckerTests/complex/warn_on_struct.sol b/test/libsolidity/smtCheckerTests/complex/warn_on_struct.sol new file mode 100644 index 00000000..6d9afe7c --- /dev/null +++ b/test/libsolidity/smtCheckerTests/complex/warn_on_struct.sol @@ -0,0 +1,14 @@ +pragma experimental SMTChecker; + +contract C { + struct A { uint a; uint b; } + function f() public pure returns (uint) { + A memory a = A({ a: 1, b: 2 }); + } +} +// ---- +// Warning: (133-143): Unused local variable. +// Warning: (133-143): Assertion checker does not yet support the type of this variable. +// Warning: (146-163): Assertion checker does not yet implement this expression. +// Warning: (146-163): Internal error: Expression undefined for SMT solver. +// Warning: (146-163): Assertion checker does not yet implement this type. diff --git a/test/libsolidity/smtCheckerTests/complex/warn_on_typecast.sol b/test/libsolidity/smtCheckerTests/complex/warn_on_typecast.sol new file mode 100644 index 00000000..be785414 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/complex/warn_on_typecast.sol @@ -0,0 +1,8 @@ +pragma experimental SMTChecker; +contract C { + function f() public pure returns (uint) { + return uint8(1); + } +} +// ---- +// Warning: (106-114): Assertion checker does not yet implement this expression. diff --git a/test/libsolidity/smtCheckerTests/control_flow/assignment_in_declaration.sol b/test/libsolidity/smtCheckerTests/control_flow/assignment_in_declaration.sol new file mode 100644 index 00000000..0c701672 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/control_flow/assignment_in_declaration.sol @@ -0,0 +1,4 @@ +pragma experimental SMTChecker; +contract C { + function f() public pure { uint a = 2; assert(a == 2); } +} diff --git a/test/libsolidity/smtCheckerTests/control_flow/branches_assert_condition_1.sol b/test/libsolidity/smtCheckerTests/control_flow/branches_assert_condition_1.sol new file mode 100644 index 00000000..64f6e012 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/control_flow/branches_assert_condition_1.sol @@ -0,0 +1,12 @@ +pragma experimental SMTChecker; +contract C { + function f(uint x) public pure { + if (x > 10) { + assert(x > 9); + } + else + { + assert(x < 11); + } + } +} diff --git a/test/libsolidity/smtCheckerTests/control_flow/branches_assert_condition_2.sol b/test/libsolidity/smtCheckerTests/control_flow/branches_assert_condition_2.sol new file mode 100644 index 00000000..e39ab844 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/control_flow/branches_assert_condition_2.sol @@ -0,0 +1,16 @@ +pragma experimental SMTChecker; +contract C { + function f(uint x) public pure { + if (x > 10) { + assert(x > 9); + } + else if (x > 2) + { + assert(x <= 10 && x > 2); + } + else + { + assert(0 <= x && x <= 2); + } + } +} diff --git a/test/libsolidity/smtCheckerTests/control_flow/branches_merge_variables_1.sol b/test/libsolidity/smtCheckerTests/control_flow/branches_merge_variables_1.sol new file mode 100644 index 00000000..f93e32e4 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/control_flow/branches_merge_variables_1.sol @@ -0,0 +1,10 @@ +pragma experimental SMTChecker; +// Branch does not touch variable a +contract C { + function f(uint x) public pure { + uint a = 3; + if (x > 10) { + } + assert(a == 3); + } +} diff --git a/test/libsolidity/smtCheckerTests/control_flow/branches_merge_variables_2.sol b/test/libsolidity/smtCheckerTests/control_flow/branches_merge_variables_2.sol new file mode 100644 index 00000000..c00ef787 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/control_flow/branches_merge_variables_2.sol @@ -0,0 +1,11 @@ +pragma experimental SMTChecker; +// Positive branch touches variable a, but assertion should still hold. +contract C { + function f(uint x) public pure { + uint a = 3; + if (x > 10) { + a = 3; + } + assert(a == 3); + } +} diff --git a/test/libsolidity/smtCheckerTests/control_flow/branches_merge_variables_3.sol b/test/libsolidity/smtCheckerTests/control_flow/branches_merge_variables_3.sol new file mode 100644 index 00000000..4e18aa88 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/control_flow/branches_merge_variables_3.sol @@ -0,0 +1,12 @@ +pragma experimental SMTChecker; +// Negative branch touches variable a, but assertion should still hold. +contract C { + function f(uint x) public pure { + uint a = 3; + if (x > 10) { + } else { + a = 3; + } + assert(a == 3); + } +} diff --git a/test/libsolidity/smtCheckerTests/control_flow/branches_merge_variables_4.sol b/test/libsolidity/smtCheckerTests/control_flow/branches_merge_variables_4.sol new file mode 100644 index 00000000..e3a02704 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/control_flow/branches_merge_variables_4.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; +// Variable is not merged, if it is only read. +contract C { + function f(uint x) public pure { + uint a = 3; + if (x > 10) { + assert(a == 3); + } else { + assert(a == 3); + } + assert(a == 3); + } +} diff --git a/test/libsolidity/smtCheckerTests/control_flow/branches_merge_variables_5.sol b/test/libsolidity/smtCheckerTests/control_flow/branches_merge_variables_5.sol new file mode 100644 index 00000000..0bd1cf3a --- /dev/null +++ b/test/libsolidity/smtCheckerTests/control_flow/branches_merge_variables_5.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; +// Variable is reset in both branches +contract C { + function f(uint x) public pure { + uint a = 2; + if (x > 10) { + a = 3; + } else { + a = 3; + } + assert(a == 3); + } +} diff --git a/test/libsolidity/smtCheckerTests/control_flow/branches_merge_variables_6.sol b/test/libsolidity/smtCheckerTests/control_flow/branches_merge_variables_6.sol new file mode 100644 index 00000000..8e477179 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/control_flow/branches_merge_variables_6.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; +// Variable is reset in both branches +contract C { + function f(uint x) public pure { + uint a = 2; + if (x > 10) { + a = 3; + } else { + a = 4; + } + assert(a >= 3); + } +} diff --git a/test/libsolidity/smtCheckerTests/control_flow/ways_to_merge_variables_1.sol b/test/libsolidity/smtCheckerTests/control_flow/ways_to_merge_variables_1.sol new file mode 100644 index 00000000..16d6fdfe --- /dev/null +++ b/test/libsolidity/smtCheckerTests/control_flow/ways_to_merge_variables_1.sol @@ -0,0 +1,12 @@ +pragma experimental SMTChecker; +contract C { + function f(uint x) public pure { + uint a = 3; + if (x > 10) { + a++; + } + assert(a == 3); + } +} +// ---- +// Warning: (159-173): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/control_flow/ways_to_merge_variables_2.sol b/test/libsolidity/smtCheckerTests/control_flow/ways_to_merge_variables_2.sol new file mode 100644 index 00000000..e25ab20f --- /dev/null +++ b/test/libsolidity/smtCheckerTests/control_flow/ways_to_merge_variables_2.sol @@ -0,0 +1,12 @@ +pragma experimental SMTChecker; +contract C { + function f(uint x) public pure { + uint a = 3; + if (x > 10) { + ++a; + } + assert(a == 3); + } +} +// ---- +// Warning: (159-173): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/control_flow/ways_to_merge_variables_3.sol b/test/libsolidity/smtCheckerTests/control_flow/ways_to_merge_variables_3.sol new file mode 100644 index 00000000..03ae7216 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/control_flow/ways_to_merge_variables_3.sol @@ -0,0 +1,12 @@ +pragma experimental SMTChecker; +contract C { + function f(uint x) public pure { + uint a = 3; + if (x > 10) { + a = 5; + } + assert(a == 3); + } +} +// ---- +// Warning: (161-175): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/functions/function_call_does_not_clear_local_vars.sol b/test/libsolidity/smtCheckerTests/functions/function_call_does_not_clear_local_vars.sol new file mode 100644 index 00000000..b4260224 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/function_call_does_not_clear_local_vars.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; +contract C { + function f() public { + uint a = 3; + this.f(); + assert(a == 3); + f(); + assert(a == 3); + } +} +// ---- +// Warning: (99-107): Assertion checker does not yet implement this type of function call. +// Warning: (141-144): Assertion checker does not support recursive function calls. diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_1.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_1.sol new file mode 100644 index 00000000..8988efad --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_1.sol @@ -0,0 +1,8 @@ +pragma experimental SMTChecker; +contract C { + function f(uint x) public pure { + require(x == 2); + for (;;) {} + assert(x == 2); + } +} diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_2.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_2.sol new file mode 100644 index 00000000..58c9f3a7 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_2.sol @@ -0,0 +1,8 @@ +pragma experimental SMTChecker; +contract C { + function f(uint x) public pure { + for (; x == 2; ) { + assert(x == 2); + } + } +} diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_3.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_3.sol new file mode 100644 index 00000000..8bf9bdc7 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_3.sol @@ -0,0 +1,8 @@ +pragma experimental SMTChecker; +contract C { + function f(uint x) public pure { + for (uint y = 2; x < 10; ) { + assert(y == 2); + } + } +} diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_4.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_4.sol new file mode 100644 index 00000000..4d082026 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_4.sol @@ -0,0 +1,10 @@ +pragma experimental SMTChecker; +contract C { + function f(uint x) public pure { + for (uint y = 2; x < 10; y = 3) { + assert(y == 2); + } + } +} +// ---- +// Warning: (136-150): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_5.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_5.sol new file mode 100644 index 00000000..2c84960f --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_5.sol @@ -0,0 +1,12 @@ +pragma experimental SMTChecker; +contract C { + function f(uint x) public pure { + uint y; + for (y = 2; x < 10; ) { + y = 3; + } + assert(y == 3); + } +} +// ---- +// Warning: (167-181): Assertion violation happens here\nNote that some information is erased after the execution of loops.\nYou can re-introduce information using require(). diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_6.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_6.sol new file mode 100644 index 00000000..90c4c328 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_6.sol @@ -0,0 +1,12 @@ +pragma experimental SMTChecker; +contract C { + function f(uint x) public pure { + uint y; + for (y = 2; x < 10; ) { + y = 3; + } + assert(y == 2); + } +} +// ---- +// Warning: (167-181): Assertion violation happens here\nNote that some information is erased after the execution of loops.\nYou can re-introduce information using require(). diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_simple_1.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_simple_1.sol new file mode 100644 index 00000000..074be86f --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/while_loop_simple_1.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; +// Check that variables are cleared +contract C { + function f(uint x) public pure { + x = 2; + while (x > 1) { + x = 2; + } + assert(x == 2); + } +} +// ---- +// Warning: (194-208): Assertion violation happens here\nNote that some information is erased after the execution of loops.\nYou can re-introduce information using require(). diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_simple_2.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_simple_2.sol new file mode 100644 index 00000000..92a3f0fe --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/while_loop_simple_2.sol @@ -0,0 +1,9 @@ +pragma experimental SMTChecker; +// Check that condition is assumed. +contract C { + function f(uint x) public pure { + while (x == 2) { + assert(x == 2); + } + } +} diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_simple_3.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_simple_3.sol new file mode 100644 index 00000000..a37df888 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/while_loop_simple_3.sol @@ -0,0 +1,11 @@ +pragma experimental SMTChecker; +// Check that condition is not assumed after the body anymore +contract C { + function f(uint x) public pure { + while (x == 2) { + } + assert(x == 2); + } +} +// ---- +// Warning: (187-201): Assertion violation happens here\nNote that some information is erased after the execution of loops.\nYou can re-introduce information using require(). diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_simple_4.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_simple_4.sol new file mode 100644 index 00000000..f71da865 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/while_loop_simple_4.sol @@ -0,0 +1,11 @@ +pragma experimental SMTChecker; +// Check that negation of condition is not assumed after the body anymore +contract C { + function f(uint x) public pure { + while (x == 2) { + } + assert(x != 2); + } +} +// ---- +// Warning: (199-213): Assertion violation happens here\nNote that some information is erased after the execution of loops.\nYou can re-introduce information using require(). diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_simple_5.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_simple_5.sol new file mode 100644 index 00000000..41559c99 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/while_loop_simple_5.sol @@ -0,0 +1,12 @@ +pragma experimental SMTChecker; +// Check that side-effects of condition are taken into account +contract C { + function f(uint x, uint y) public pure { + x = 7; + while ((x = y) > 0) { + } + assert(x == 7); + } +} +// ---- +// Warning: (216-230): Assertion violation happens here\nNote that some information is erased after the execution of loops.\nYou can re-introduce information using require(). diff --git a/test/libsolidity/smtCheckerTests/overflow/simple_overflow.sol b/test/libsolidity/smtCheckerTests/overflow/simple_overflow.sol new file mode 100644 index 00000000..894ff1a4 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/overflow/simple_overflow.sol @@ -0,0 +1,6 @@ +pragma experimental SMTChecker; +contract C { + function f(uint a, uint b) public pure returns (uint) { return a + b; } +} +// ---- +// Warning: (112-117): Overflow (resulting value larger than 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) happens here diff --git a/test/libsolidity/smtCheckerTests/simple/smoke_test.sol b/test/libsolidity/smtCheckerTests/simple/smoke_test.sol new file mode 100644 index 00000000..8b7b77da --- /dev/null +++ b/test/libsolidity/smtCheckerTests/simple/smoke_test.sol @@ -0,0 +1,3 @@ +pragma experimental SMTChecker; +contract C { +} diff --git a/test/libsolidity/smtCheckerTests/types/bool_int_mixed_1.sol b/test/libsolidity/smtCheckerTests/types/bool_int_mixed_1.sol new file mode 100644 index 00000000..d611cc17 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/bool_int_mixed_1.sol @@ -0,0 +1,9 @@ +pragma experimental SMTChecker; +contract C { + function f(bool x) public pure { + uint a; + if(x) + a = 1; + assert(!x || a > 0); + } +} diff --git a/test/libsolidity/smtCheckerTests/types/bool_int_mixed_2.sol b/test/libsolidity/smtCheckerTests/types/bool_int_mixed_2.sol new file mode 100644 index 00000000..24640c5a --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/bool_int_mixed_2.sol @@ -0,0 +1,8 @@ +pragma experimental SMTChecker; +contract C { + function f(bool x, uint a) public pure { + require(!x || a > 0); + uint b = a; + assert(!x || b > 0); + } +} diff --git a/test/libsolidity/smtCheckerTests/types/bool_int_mixed_3.sol b/test/libsolidity/smtCheckerTests/types/bool_int_mixed_3.sol new file mode 100644 index 00000000..f872e82f --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/bool_int_mixed_3.sol @@ -0,0 +1,21 @@ +pragma experimental SMTChecker; +contract C { + function f(bool x, bool y) public pure { + uint a; + if (x) { + if (y) { + a = 0; + } else { + a = 1; + } + } else { + if (y) { + a = 1; + } else { + a = 0; + } + } + bool xor_x_y = (x && !y) || (!x && y); + assert(!xor_x_y || a > 0); + } +} diff --git a/test/libsolidity/smtCheckerTests/types/bool_simple_1.sol b/test/libsolidity/smtCheckerTests/types/bool_simple_1.sol new file mode 100644 index 00000000..76b4b08b --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/bool_simple_1.sol @@ -0,0 +1,8 @@ +pragma experimental SMTChecker; +contract C { + function f(bool x) public pure { + assert(x); + } +} +// ---- +// Warning: (90-99): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/bool_simple_2.sol b/test/libsolidity/smtCheckerTests/types/bool_simple_2.sol new file mode 100644 index 00000000..5c166c02 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/bool_simple_2.sol @@ -0,0 +1,8 @@ +pragma experimental SMTChecker; +contract C { + function f(bool x, bool y) public pure { + assert(x == y); + } +} +// ---- +// Warning: (98-112): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/bool_simple_3.sol b/test/libsolidity/smtCheckerTests/types/bool_simple_3.sol new file mode 100644 index 00000000..1d2ab49f --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/bool_simple_3.sol @@ -0,0 +1,7 @@ +pragma experimental SMTChecker; +contract C { + function f(bool x, bool y) public pure { + bool z = x || y; + assert(!(x && y) || z); + } +} diff --git a/test/libsolidity/smtCheckerTests/types/bool_simple_4.sol b/test/libsolidity/smtCheckerTests/types/bool_simple_4.sol new file mode 100644 index 00000000..c40404a4 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/bool_simple_4.sol @@ -0,0 +1,10 @@ +pragma experimental SMTChecker; +contract C { + function f(bool x) public pure { + if(x) { + assert(x); + } else { + assert(!x); + } + } +} diff --git a/test/libsolidity/smtCheckerTests/types/bool_simple_5.sol b/test/libsolidity/smtCheckerTests/types/bool_simple_5.sol new file mode 100644 index 00000000..4cecebbc --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/bool_simple_5.sol @@ -0,0 +1,7 @@ +pragma experimental SMTChecker; +contract C { + function f(bool x) public pure { + bool y = x; + assert(x == y); + } +} diff --git a/test/libsolidity/smtCheckerTests/types/bool_simple_6.sol b/test/libsolidity/smtCheckerTests/types/bool_simple_6.sol new file mode 100644 index 00000000..90350bb6 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/bool_simple_6.sol @@ -0,0 +1,9 @@ +pragma experimental SMTChecker; +contract C { + function f(bool x) public pure { + require(x); + bool y; + y = false; + assert(x || y); + } +} diff --git a/test/libsolidity/smtCheckerTests/types/storage_value_vars_1.sol b/test/libsolidity/smtCheckerTests/types/storage_value_vars_1.sol new file mode 100644 index 00000000..84f6c77e --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/storage_value_vars_1.sol @@ -0,0 +1,22 @@ +pragma experimental SMTChecker; +contract C +{ + address a; + bool b; + uint c; + function f(uint x) public { + if (x == 0) + { + a = 0x0000000000000000000000000000000000000100; + b = true; + } + else + { + a = 0x0000000000000000000000000000000000000200; + b = false; + } + assert(a > 0x0000000000000000000000000000000000000000 && b); + } +} +// ---- +// Warning: (362-421): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/storage_value_vars_2.sol b/test/libsolidity/smtCheckerTests/types/storage_value_vars_2.sol new file mode 100644 index 00000000..bceddb38 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/storage_value_vars_2.sol @@ -0,0 +1,12 @@ +pragma experimental SMTChecker; +contract C +{ + address a; + bool b; + uint c; + function f() public view { + assert(c > 0); + } +} +// ---- +// Warning: (123-136): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/storage_value_vars_3.sol b/test/libsolidity/smtCheckerTests/types/storage_value_vars_3.sol new file mode 100644 index 00000000..39049b99 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/storage_value_vars_3.sol @@ -0,0 +1,25 @@ +pragma experimental SMTChecker; +contract C +{ + function f(uint x) public { + if (x == 0) + { + a = 0x0000000000000000000000000000000000000100; + b = true; + } + else + { + a = 0x0000000000000000000000000000000000000200; + b = false; + } + assert(b == (a < 0x0000000000000000000000000000000000000200)); + } + + function g() public view { + require(a < 0x0000000000000000000000000000000000000100); + assert(c >= 0); + } + address a; + bool b; + uint c; +} diff --git a/test/libsolidity/smtCheckerTests/types/storage_value_vars_4.sol b/test/libsolidity/smtCheckerTests/types/storage_value_vars_4.sol new file mode 100644 index 00000000..88b6b0ae --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/storage_value_vars_4.sol @@ -0,0 +1,10 @@ +pragma experimental SMTChecker; +contract C +{ + function f() public view { + assert(c > 0); + } + uint c; +} +// ---- +// Warning: (84-97): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/verification_target/constant_condition_1.sol b/test/libsolidity/smtCheckerTests/verification_target/constant_condition_1.sol new file mode 100644 index 00000000..b9fae4ee --- /dev/null +++ b/test/libsolidity/smtCheckerTests/verification_target/constant_condition_1.sol @@ -0,0 +1,9 @@ +pragma experimental SMTChecker; +contract C { + function f(uint x) public pure { + if (x >= 0) { revert(); } + } +} +// ---- +// Warning: (94-100): Condition is always true. +// Warning: (104-112): Assertion checker does not yet implement this type of function call. diff --git a/test/libsolidity/smtCheckerTests/verification_target/constant_condition_2.sol b/test/libsolidity/smtCheckerTests/verification_target/constant_condition_2.sol new file mode 100644 index 00000000..aaa613ea --- /dev/null +++ b/test/libsolidity/smtCheckerTests/verification_target/constant_condition_2.sol @@ -0,0 +1,9 @@ +pragma experimental SMTChecker; +contract C { + function f(uint x) public pure { + if (x >= 10) { if (x < 10) { revert(); } } + } +} +// ---- +// Warning: (109-115): Condition is always false. +// Warning: (119-127): Assertion checker does not yet implement this type of function call. diff --git a/test/libsolidity/smtCheckerTests/verification_target/constant_condition_3.sol b/test/libsolidity/smtCheckerTests/verification_target/constant_condition_3.sol new file mode 100644 index 00000000..f22cd65e --- /dev/null +++ b/test/libsolidity/smtCheckerTests/verification_target/constant_condition_3.sol @@ -0,0 +1,9 @@ +pragma experimental SMTChecker; +// a plain literal constant is fine +contract C { + function f(uint) public pure { + if (true) { revert(); } + } +} +// ---- +// Warning: (136-144): Assertion checker does not yet implement this type of function call. diff --git a/test/libsolidity/smtCheckerTests/verification_target/simple_assert.sol b/test/libsolidity/smtCheckerTests/verification_target/simple_assert.sol new file mode 100644 index 00000000..8bd6e61a --- /dev/null +++ b/test/libsolidity/smtCheckerTests/verification_target/simple_assert.sol @@ -0,0 +1,6 @@ +pragma experimental SMTChecker; +contract C { + function f(uint a) public pure { assert(a == 2); } +} +// ---- +// Warning: (82-96): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/verification_target/simple_assert_with_require.sol b/test/libsolidity/smtCheckerTests/verification_target/simple_assert_with_require.sol new file mode 100644 index 00000000..b66ae245 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/verification_target/simple_assert_with_require.sol @@ -0,0 +1,4 @@ +pragma experimental SMTChecker; +contract C { + function f(uint a) public pure { require(a < 10); assert(a < 20); } +} diff --git a/test/libsolidity/smtCheckerTestsJSON/multi.json b/test/libsolidity/smtCheckerTestsJSON/multi.json new file mode 100644 index 00000000..2ed5150d --- /dev/null +++ b/test/libsolidity/smtCheckerTestsJSON/multi.json @@ -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))" + } + } +} diff --git a/test/libsolidity/smtCheckerTestsJSON/multi.sol b/test/libsolidity/smtCheckerTestsJSON/multi.sol new file mode 100644 index 00000000..e0d69b1d --- /dev/null +++ b/test/libsolidity/smtCheckerTestsJSON/multi.sol @@ -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 diff --git a/test/libsolidity/smtCheckerTestsJSON/simple.json b/test/libsolidity/smtCheckerTestsJSON/simple.json new file mode 100644 index 00000000..fd976b63 --- /dev/null +++ b/test/libsolidity/smtCheckerTestsJSON/simple.json @@ -0,0 +1,9 @@ +{ + "auxiliaryInput": + { + "smtlib2responses": + { + "0xe9477f683ff20aa57fcb08682150f86c5917e1d4c0686b278ab9b73446d0682c": "sat\n((|EVALEXPR_0| 0))" + } + } +} diff --git a/test/libsolidity/smtCheckerTestsJSON/simple.sol b/test/libsolidity/smtCheckerTestsJSON/simple.sol new file mode 100644 index 00000000..6bc7193d --- /dev/null +++ b/test/libsolidity/smtCheckerTestsJSON/simple.sol @@ -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 diff --git a/test/libsolidity/syntaxTests/bound/bound_all.sol b/test/libsolidity/syntaxTests/bound/bound_all.sol new file mode 100644 index 00000000..29f55b88 --- /dev/null +++ b/test/libsolidity/syntaxTests/bound/bound_all.sol @@ -0,0 +1,10 @@ +library L { + function g(function() internal returns (uint) _t) internal returns (uint) { return _t(); } +} +contract C { + using L for *; + function f() public returns (uint) { + return t.g(); + } + function t() public pure returns (uint) { return 7; } +} diff --git a/test/libsolidity/syntaxTests/bound/bound_call.sol b/test/libsolidity/syntaxTests/bound/bound_call.sol new file mode 100644 index 00000000..281f19b4 --- /dev/null +++ b/test/libsolidity/syntaxTests/bound/bound_call.sol @@ -0,0 +1,7 @@ +library D { function double(uint self) internal pure returns (uint) { return 2*self; } } +contract C { + using D for uint; + function f(uint a) public pure { + a.double(); + } +} diff --git a/test/libsolidity/syntaxTests/bound/bound_no_call.sol b/test/libsolidity/syntaxTests/bound/bound_no_call.sol new file mode 100644 index 00000000..dcb3c3c5 --- /dev/null +++ b/test/libsolidity/syntaxTests/bound/bound_no_call.sol @@ -0,0 +1,7 @@ +library D { function double(uint self) public pure returns (uint) { return 2*self; } } +contract C { + using D for uint; + function f(uint a) public pure { + a.double; + } +} |