From ea4b9e2f989a630f8f81a154760110f01a8ee214 Mon Sep 17 00:00:00 2001 From: chriseth Date: Mon, 9 Dec 2019 11:57:44 +0100 Subject: [PATCH 01/12] Changelog wording. --- Changelog.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Changelog.md b/Changelog.md index a691203c2..ef537243f 100644 --- a/Changelog.md +++ b/Changelog.md @@ -1,9 +1,9 @@ -### 0.5.14 (unreleased) +### 0.5.14 (2019-12-09) Language Features: * Allow to obtain the selector of public or external library functions via a member ``.selector``. - * Parser: Allow splitting string and hexadecimal string literals into multiple parts. - * Inline Assembly: Support referencing other constants. + * Parser: Allow splitting hexadecimal and regular string literals into multiple parts. + * Inline Assembly: Support constants that reference other constants. Compiler Features: From 9d2fc7ec8bb4bb710ca3562ccbcac4a25986431b Mon Sep 17 00:00:00 2001 From: chriseth Date: Mon, 9 Dec 2019 12:34:21 +0100 Subject: [PATCH 02/12] Sort changelog. --- Changelog.md | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/Changelog.md b/Changelog.md index ef537243f..d491e6f72 100644 --- a/Changelog.md +++ b/Changelog.md @@ -2,28 +2,28 @@ Language Features: * Allow to obtain the selector of public or external library functions via a member ``.selector``. - * Parser: Allow splitting hexadecimal and regular string literals into multiple parts. * Inline Assembly: Support constants that reference other constants. + * Parser: Allow splitting hexadecimal and regular string literals into multiple parts. Compiler Features: - * Set the default EVM version to "Istanbul". * Commandline Interface: Allow translation from yul / strict assembly to EWasm using ``solc --yul --yul-dialect evm --machine eWasm`` + * Set the default EVM version to "Istanbul". * SMTChecker: Add support to constructors including constructor inheritance. * Yul: When compiling via Yul, string literals from the Solidity code are kept as string literals if every character is safely printable. * Yul Optimizer: Perform loop-invariant code motion. -Build System: - * Update to emscripten version 1.39.3. - - Bugfixes: * SMTChecker: Fix internal error when using ``abi.decode``. * SMTChecker: Fix internal error when using arrays or mappings of functions. * SMTChecker: Fix internal error in array of structs type. - * Yul: Consider infinite loops and recursion to be not removable. * Version Checker: 0.5.x-prerelease will match `pragma solidity ^0.5`. + * Yul: Consider infinite loops and recursion to be not removable. + + +Build System: + * Update to emscripten version 1.39.3. ### 0.5.13 (2019-11-14) From 63962f835dc4b85b6c700fdb63e22896853165be Mon Sep 17 00:00:00 2001 From: chriseth Date: Mon, 9 Dec 2019 12:52:56 +0100 Subject: [PATCH 03/12] Update bug list. --- docs/bugs_by_version.json | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/docs/bugs_by_version.json b/docs/bugs_by_version.json index 402997af1..c412be830 100644 --- a/docs/bugs_by_version.json +++ b/docs/bugs_by_version.json @@ -758,6 +758,10 @@ "bugs": [], "released": "2019-11-14" }, + "0.5.14": { + "bugs": [], + "released": "2019-12-09" + }, "0.5.2": { "bugs": [ "SignedArrayStorageCopy", From 3e8584bd21c5793a96a81d85c61e9eed44ff6a4f Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Tue, 3 Dec 2019 16:50:04 +0100 Subject: [PATCH 04/12] Pull SyntaxTest::run content into separate functions --- test/libsolidity/SyntaxTest.cpp | 121 ++++++++++++++++++-------------- test/libsolidity/SyntaxTest.h | 6 +- 2 files changed, 73 insertions(+), 54 deletions(-) diff --git a/test/libsolidity/SyntaxTest.cpp b/test/libsolidity/SyntaxTest.cpp index 41a4dd18b..5ab84b06d 100644 --- a/test/libsolidity/SyntaxTest.cpp +++ b/test/libsolidity/SyntaxTest.cpp @@ -73,59 +73,9 @@ SyntaxTest::SyntaxTest(string const& _filename, langutil::EVMVersion _evmVersion TestCase::TestResult SyntaxTest::run(ostream& _stream, string const& _linePrefix, bool _formatted) { - string const versionPragma = "pragma solidity >=0.0;\n"; - compiler().reset(); - auto sourcesWithPragma = m_sources; - for (auto& source: sourcesWithPragma) - source.second = versionPragma + source.second; - compiler().setSources(sourcesWithPragma); - compiler().setEVMVersion(m_evmVersion); - compiler().setParserErrorRecovery(m_parserErrorRecovery); - compiler().setOptimiserSettings( - m_optimiseYul ? - OptimiserSettings::full() : - OptimiserSettings::minimal() - ); - if (compiler().parse()) - if (compiler().analyze()) - try - { - if (!compiler().compile()) - BOOST_THROW_EXCEPTION(runtime_error("Compilation failed even though analysis was successful.")); - } - catch (UnimplementedFeatureError const& _e) - { - m_errorList.emplace_back(SyntaxTestError{ - "UnimplementedFeatureError", - errorMessage(_e), - "", - -1, - -1 - }); - } - - for (auto const& currentError: filterErrors(compiler().errors(), true)) - { - int locationStart = -1, locationEnd = -1; - string sourceName; - if (auto location = boost::get_error_info(*currentError)) - { - // ignore the version pragma inserted by the testing tool when calculating locations. - if (location->start >= static_cast(versionPragma.size())) - locationStart = location->start - versionPragma.size(); - if (location->end >= static_cast(versionPragma.size())) - locationEnd = location->end - versionPragma.size(); - if (location->source) - sourceName = location->source->name(); - } - m_errorList.emplace_back(SyntaxTestError{ - currentError->typeName(), - errorMessage(*currentError), - sourceName, - locationStart, - locationEnd - }); - } + setupCompiler(); + parseAndAnalyze(); + filterObtainedErrors(); return printExpectationAndError(_stream, _linePrefix, _formatted) ? TestResult::Success : TestResult::Failure; } @@ -207,6 +157,71 @@ void SyntaxTest::printSource(ostream& _stream, string const& _linePrefix, bool _ } } +void SyntaxTest::setupCompiler() +{ + string const versionPragma = "pragma solidity >=0.0;\n"; + compiler().reset(); + auto sourcesWithPragma = m_sources; + for (auto& source: sourcesWithPragma) + source.second = versionPragma + source.second; + compiler().setSources(sourcesWithPragma); + compiler().setEVMVersion(m_evmVersion); + compiler().setParserErrorRecovery(m_parserErrorRecovery); + compiler().setOptimiserSettings( + m_optimiseYul ? + OptimiserSettings::full() : + OptimiserSettings::minimal() + ); +} + +void SyntaxTest::parseAndAnalyze() +{ + if (compiler().parse()) + if (compiler().analyze()) + try + { + if (!compiler().compile()) + BOOST_THROW_EXCEPTION(runtime_error("Compilation failed even though analysis was successful.")); + } + catch (UnimplementedFeatureError const& _e) + { + m_errorList.emplace_back(SyntaxTestError{ + "UnimplementedFeatureError", + errorMessage(_e), + "", + -1, + -1 + }); + } +} + +void SyntaxTest::filterObtainedErrors() +{ + string const versionPragma = "pragma solidity >=0.0;\n"; + for (auto const& currentError: filterErrors(compiler().errors(), true)) + { + int locationStart = -1, locationEnd = -1; + string sourceName; + if (auto location = boost::get_error_info(*currentError)) + { + // ignore the version pragma inserted by the testing tool when calculating locations. + if (location->start >= static_cast(versionPragma.size())) + locationStart = location->start - versionPragma.size(); + if (location->end >= static_cast(versionPragma.size())) + locationEnd = location->end - versionPragma.size(); + if (location->source) + sourceName = location->source->name(); + } + m_errorList.emplace_back(SyntaxTestError{ + currentError->typeName(), + errorMessage(*currentError), + sourceName, + locationStart, + locationEnd + }); + } +} + void SyntaxTest::printErrorList( ostream& _stream, vector const& _errorList, diff --git a/test/libsolidity/SyntaxTest.h b/test/libsolidity/SyntaxTest.h index 53c06d3fe..7d8ccdc69 100644 --- a/test/libsolidity/SyntaxTest.h +++ b/test/libsolidity/SyntaxTest.h @@ -52,7 +52,7 @@ struct SyntaxTestError }; -class SyntaxTest: AnalysisFramework, public EVMVersionRestrictedTestCase +class SyntaxTest: public AnalysisFramework, public EVMVersionRestrictedTestCase { public: static std::unique_ptr create(Config const& _config) @@ -76,6 +76,10 @@ public: static std::string errorMessage(Exception const& _e); protected: + void setupCompiler(); + void parseAndAnalyze(); + void filterObtainedErrors(); + static void printErrorList( std::ostream& _stream, std::vector const& _errors, From 225041738ea2e8e1deda668647487415e8258ae4 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Tue, 3 Dec 2019 16:50:28 +0100 Subject: [PATCH 05/12] Add SMTCheckerTest for isoltest --- libsolidity/formal/CHC.cpp | 24 ++++++--- libsolidity/formal/CHC.h | 3 ++ libsolidity/formal/ModelChecker.cpp | 12 +++++ libsolidity/formal/ModelChecker.h | 3 ++ libsolidity/interface/CompilerStack.cpp | 11 +++- libsolidity/interface/CompilerStack.h | 5 ++ test/CMakeLists.txt | 2 + test/InteractiveTests.h | 5 +- test/libsolidity/SMTCheckerJSONTest.cpp | 8 +-- test/libsolidity/SMTCheckerJSONTest.h | 6 +-- test/libsolidity/SMTCheckerTest.cpp | 71 +++++++++++++++++++++++++ test/libsolidity/SMTCheckerTest.h | 55 +++++++++++++++++++ test/libsolidity/SyntaxTest.cpp | 33 ++++++------ test/tools/CMakeLists.txt | 1 + 14 files changed, 204 insertions(+), 35 deletions(-) create mode 100644 test/libsolidity/SMTCheckerTest.cpp create mode 100644 test/libsolidity/SMTCheckerTest.h diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 5e9495192..bf9d6de30 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -48,7 +48,8 @@ CHC::CHC( #else m_interface(make_shared(_smtlib2Responses)), #endif - m_outerErrorReporter(_errorReporter) + m_outerErrorReporter(_errorReporter), + m_enabledSolvers(_enabledSolvers) { (void)_smtlib2Responses; (void)_enabledSolvers; @@ -58,15 +59,22 @@ void CHC::analyze(SourceUnit const& _source) { solAssert(_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker), ""); + bool usesZ3 = false; #ifdef HAVE_Z3 - auto z3Interface = dynamic_pointer_cast(m_interface); - solAssert(z3Interface, ""); - m_context.setSolver(z3Interface->z3Interface()); -#else - auto smtlib2Interface = dynamic_pointer_cast(m_interface); - solAssert(smtlib2Interface, ""); - m_context.setSolver(smtlib2Interface->smtlib2Interface()); + usesZ3 = m_enabledSolvers.z3; + if (usesZ3) + { + auto z3Interface = dynamic_pointer_cast(m_interface); + solAssert(z3Interface, ""); + m_context.setSolver(z3Interface->z3Interface()); + } #endif + if (!usesZ3) + { + auto smtlib2Interface = dynamic_pointer_cast(m_interface); + solAssert(smtlib2Interface, ""); + m_context.setSolver(smtlib2Interface->smtlib2Interface()); + } m_context.clear(); m_context.setAssertionAccumulation(false); m_variableUsage.setFunctionInlining(false); diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h index a5ab9e06b..8c3216085 100644 --- a/libsolidity/formal/CHC.h +++ b/libsolidity/formal/CHC.h @@ -208,6 +208,9 @@ private: /// ErrorReporter that comes from CompilerStack. langutil::ErrorReporter& m_outerErrorReporter; + + /// SMT solvers that are chosen at runtime. + smt::SMTSolverChoice m_enabledSolvers; }; } diff --git a/libsolidity/formal/ModelChecker.cpp b/libsolidity/formal/ModelChecker.cpp index 508509805..75b5df67f 100644 --- a/libsolidity/formal/ModelChecker.cpp +++ b/libsolidity/formal/ModelChecker.cpp @@ -46,3 +46,15 @@ vector ModelChecker::unhandledQueries() { return m_bmc.unhandledQueries() + m_chc.unhandledQueries(); } + +smt::SMTSolverChoice ModelChecker::availableSolvers() +{ + smt::SMTSolverChoice available = smt::SMTSolverChoice::None(); +#ifdef HAVE_Z3 + available.z3 = true; +#endif +#ifdef HAVE_CVC4 + available.cvc4 = true; +#endif + return available; +} diff --git a/libsolidity/formal/ModelChecker.h b/libsolidity/formal/ModelChecker.h index d7ec7c1b3..42d8ac2c9 100644 --- a/libsolidity/formal/ModelChecker.h +++ b/libsolidity/formal/ModelChecker.h @@ -59,6 +59,9 @@ public: /// the constructor. std::vector unhandledQueries(); + /// @returns SMT solvers that are available via the C++ API. + static smt::SMTSolverChoice availableSolvers(); + private: /// Bounded Model Checker engine. BMC m_bmc; diff --git a/libsolidity/interface/CompilerStack.cpp b/libsolidity/interface/CompilerStack.cpp index e605c6b48..c0cadf839 100644 --- a/libsolidity/interface/CompilerStack.cpp +++ b/libsolidity/interface/CompilerStack.cpp @@ -79,6 +79,7 @@ static int g_compilerStackCounts = 0; CompilerStack::CompilerStack(ReadCallback::Callback const& _readFile): m_readFile{_readFile}, + m_enabledSMTSolvers{smt::SMTSolverChoice::All()}, m_generateIR{false}, m_generateEWasm{false}, m_errorList{}, @@ -132,6 +133,13 @@ void CompilerStack::setEVMVersion(langutil::EVMVersion _version) m_evmVersion = _version; } +void CompilerStack::setSMTSolverChoice(smt::SMTSolverChoice _enabledSMTSolvers) +{ + if (m_stackState >= ParsingPerformed) + BOOST_THROW_EXCEPTION(CompilerError() << errinfo_comment("Must set enabled SMT solvers before parsing.")); + m_enabledSMTSolvers = _enabledSMTSolvers; +} + void CompilerStack::setLibraries(std::map const& _libraries) { if (m_stackState >= ParsingPerformed) @@ -179,6 +187,7 @@ void CompilerStack::reset(bool _keepSettings) m_remappings.clear(); m_libraries.clear(); m_evmVersion = langutil::EVMVersion(); + m_enabledSMTSolvers = smt::SMTSolverChoice::All(); m_generateIR = false; m_generateEWasm = false; m_optimiserSettings = OptimiserSettings::minimal(); @@ -372,7 +381,7 @@ bool CompilerStack::analyze() if (noErrors) { - ModelChecker modelChecker(m_errorReporter, m_smtlib2Responses); + ModelChecker modelChecker(m_errorReporter, m_smtlib2Responses, m_enabledSMTSolvers); for (Source const* source: m_sourceOrder) modelChecker.analyze(*source->ast); m_unhandledSMTLib2Queries += modelChecker.unhandledQueries(); diff --git a/libsolidity/interface/CompilerStack.h b/libsolidity/interface/CompilerStack.h index 005ef911f..769375342 100644 --- a/libsolidity/interface/CompilerStack.h +++ b/libsolidity/interface/CompilerStack.h @@ -26,6 +26,7 @@ #include #include #include +#include #include #include @@ -152,6 +153,9 @@ public: /// Must be set before parsing. void setEVMVersion(langutil::EVMVersion _version = langutil::EVMVersion{}); + /// Set which SMT solvers should be enabled. + void setSMTSolverChoice(smt::SMTSolverChoice _enabledSolvers); + /// Sets the requested contract names by source. /// If empty, no filtering is performed and every contract /// found in the supplied sources is compiled. @@ -413,6 +417,7 @@ private: ReadCallback::Callback m_readFile; OptimiserSettings m_optimiserSettings; langutil::EVMVersion m_evmVersion; + smt::SMTSolverChoice m_enabledSMTSolvers; std::map> m_requestedContractNames; bool m_generateIR; bool m_generateEWasm; diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt index b0c3b47da..8424e957b 100644 --- a/test/CMakeLists.txt +++ b/test/CMakeLists.txt @@ -91,6 +91,8 @@ set(libsolidity_sources libsolidity/SMTChecker.cpp libsolidity/SMTCheckerJSONTest.cpp libsolidity/SMTCheckerJSONTest.h + libsolidity/SMTCheckerTest.cpp + libsolidity/SMTCheckerTest.h libsolidity/SolidityCompiler.cpp libsolidity/SolidityEndToEndTest.cpp libsolidity/SolidityExecutionFramework.cpp diff --git a/test/InteractiveTests.h b/test/InteractiveTests.h index 591d1d7ed..e1cb6c08f 100644 --- a/test/InteractiveTests.h +++ b/test/InteractiveTests.h @@ -23,6 +23,7 @@ #include #include #include +#include #include #include #include @@ -65,8 +66,8 @@ Testsuite const g_interactiveTestsuites[] = { {"Semantic", "libsolidity", "semanticTests", false, true, &SemanticTest::create}, {"JSON AST", "libsolidity", "ASTJSON", false, false, &ASTJSONTest::create}, {"JSON ABI", "libsolidity", "ABIJson", false, false, &ABIJsonTest::create}, - {"SMT Checker", "libsolidity", "smtCheckerTests", true, false, &SyntaxTest::create}, - {"SMT Checker JSON", "libsolidity", "smtCheckerTestsJSON", true, false, &SMTCheckerTest::create}, + {"SMT Checker", "libsolidity", "smtCheckerTests", true, false, &SMTCheckerTest::create}, + {"SMT Checker JSON", "libsolidity", "smtCheckerTestsJSON", true, false, &SMTCheckerJSONTest::create}, {"Gas Estimates", "libsolidity", "gasTests", false, false, &GasTest::create} }; diff --git a/test/libsolidity/SMTCheckerJSONTest.cpp b/test/libsolidity/SMTCheckerJSONTest.cpp index 19bdcaacc..59425b6a5 100644 --- a/test/libsolidity/SMTCheckerJSONTest.cpp +++ b/test/libsolidity/SMTCheckerJSONTest.cpp @@ -36,7 +36,7 @@ using namespace dev; using namespace std; using namespace boost::unit_test; -SMTCheckerTest::SMTCheckerTest(string const& _filename, langutil::EVMVersion _evmVersion) +SMTCheckerJSONTest::SMTCheckerJSONTest(string const& _filename, langutil::EVMVersion _evmVersion) : SyntaxTest(_filename, _evmVersion) { if (!boost::algorithm::ends_with(_filename, ".sol")) @@ -50,7 +50,7 @@ SMTCheckerTest::SMTCheckerTest(string const& _filename, langutil::EVMVersion _ev BOOST_THROW_EXCEPTION(runtime_error("Invalid JSON file.")); } -TestCase::TestResult SMTCheckerTest::run(ostream& _stream, string const& _linePrefix, bool _formatted) +TestCase::TestResult SMTCheckerJSONTest::run(ostream& _stream, string const& _linePrefix, bool _formatted) { StandardCompiler compiler; @@ -129,7 +129,7 @@ TestCase::TestResult SMTCheckerTest::run(ostream& _stream, string const& _linePr return printExpectationAndError(_stream, _linePrefix, _formatted) ? TestResult::Success : TestResult::Failure; } -vector SMTCheckerTest::hashesFromJson(Json::Value const& _jsonObj, string const& _auxInput, string const& _smtlib) +vector SMTCheckerJSONTest::hashesFromJson(Json::Value const& _jsonObj, string const& _auxInput, string const& _smtlib) { vector hashes; Json::Value const& auxInputs = _jsonObj[_auxInput]; @@ -143,7 +143,7 @@ vector SMTCheckerTest::hashesFromJson(Json::Value const& _jsonObj, strin return hashes; } -Json::Value SMTCheckerTest::buildJson(string const& _extra) +Json::Value SMTCheckerJSONTest::buildJson(string const& _extra) { string language = "\"language\": \"Solidity\""; string sources = " \"sources\": { "; diff --git a/test/libsolidity/SMTCheckerJSONTest.h b/test/libsolidity/SMTCheckerJSONTest.h index 8cff67a78..027e87418 100644 --- a/test/libsolidity/SMTCheckerJSONTest.h +++ b/test/libsolidity/SMTCheckerJSONTest.h @@ -30,14 +30,14 @@ namespace solidity namespace test { -class SMTCheckerTest: public SyntaxTest +class SMTCheckerJSONTest: public SyntaxTest { public: static std::unique_ptr create(Config const& _config) { - return std::make_unique(_config.filename, _config.evmVersion); + return std::make_unique(_config.filename, _config.evmVersion); } - SMTCheckerTest(std::string const& _filename, langutil::EVMVersion _evmVersion); + SMTCheckerJSONTest(std::string const& _filename, langutil::EVMVersion _evmVersion); TestResult run(std::ostream& _stream, std::string const& _linePrefix = "", bool _formatted = false) override; diff --git a/test/libsolidity/SMTCheckerTest.cpp b/test/libsolidity/SMTCheckerTest.cpp new file mode 100644 index 000000000..3b9532c03 --- /dev/null +++ b/test/libsolidity/SMTCheckerTest.cpp @@ -0,0 +1,71 @@ +/* + 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 . +*/ + +#include +#include + +#include + +using namespace langutil; +using namespace dev::solidity; +using namespace dev::solidity::test; +using namespace dev; +using namespace std; + +SMTCheckerTest::SMTCheckerTest(string const& _filename, langutil::EVMVersion _evmVersion): SyntaxTest(_filename, _evmVersion) +{ + if (m_settings.count("SMTSolvers")) + { + auto const& choice = m_settings.at("SMTSolvers"); + if (choice == "any") + m_enabledSolvers = smt::SMTSolverChoice::All(); + else if (choice == "z3") + m_enabledSolvers = smt::SMTSolverChoice::Z3(); + else if (choice == "cvc4") + m_enabledSolvers = smt::SMTSolverChoice::CVC4(); + else if (choice == "none") + m_enabledSolvers = smt::SMTSolverChoice::None(); + else + BOOST_THROW_EXCEPTION(runtime_error("Invalid SMT solver choice.")); + } + else + m_enabledSolvers = smt::SMTSolverChoice::All(); +} + +TestCase::TestResult SMTCheckerTest::run(ostream& _stream, string const& _linePrefix, bool _formatted) +{ + setupCompiler(); + compiler().setSMTSolverChoice(m_enabledSolvers); + parseAndAnalyze(); + filterObtainedErrors(); + + return printExpectationAndError(_stream, _linePrefix, _formatted) ? TestResult::Success : TestResult::Failure; +} + +bool SMTCheckerTest::validateSettings(langutil::EVMVersion _evmVersion) +{ + auto available = ModelChecker::availableSolvers(); + if (!available.z3) + m_enabledSolvers.z3 = false; + if (!available.cvc4) + m_enabledSolvers.cvc4 = false; + + if (m_enabledSolvers.none()) + return false; + + return SyntaxTest::validateSettings(_evmVersion); +} diff --git a/test/libsolidity/SMTCheckerTest.h b/test/libsolidity/SMTCheckerTest.h new file mode 100644 index 000000000..e48a587f1 --- /dev/null +++ b/test/libsolidity/SMTCheckerTest.h @@ -0,0 +1,55 @@ +/* + 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 . +*/ + +#pragma once + +#include + +#include + +#include + +namespace dev +{ +namespace solidity +{ +namespace test +{ + +class SMTCheckerTest: public SyntaxTest +{ +public: + static std::unique_ptr create(Config const& _config) + { + return std::make_unique(_config.filename, _config.evmVersion); + } + SMTCheckerTest(std::string const& _filename, langutil::EVMVersion _evmVersion); + + TestResult run(std::ostream& _stream, std::string const& _linePrefix = "", bool _formatted = false) override; + + bool validateSettings(langutil::EVMVersion _evmVersion) override; + +protected: + /// This is set via option SMTSolvers in the test. + /// The possible options are `all`, `z3`, `cvc4`, `none`, + /// where if none is given the default used option is `all`. + smt::SMTSolverChoice m_enabledSolvers; +}; + +} +} +} diff --git a/test/libsolidity/SyntaxTest.cpp b/test/libsolidity/SyntaxTest.cpp index 5ab84b06d..bafae4cc7 100644 --- a/test/libsolidity/SyntaxTest.cpp +++ b/test/libsolidity/SyntaxTest.cpp @@ -176,23 +176,22 @@ void SyntaxTest::setupCompiler() void SyntaxTest::parseAndAnalyze() { - if (compiler().parse()) - if (compiler().analyze()) - try - { - if (!compiler().compile()) - BOOST_THROW_EXCEPTION(runtime_error("Compilation failed even though analysis was successful.")); - } - catch (UnimplementedFeatureError const& _e) - { - m_errorList.emplace_back(SyntaxTestError{ - "UnimplementedFeatureError", - errorMessage(_e), - "", - -1, - -1 - }); - } + if (compiler().parse() && compiler().analyze()) + try + { + if (!compiler().compile()) + BOOST_THROW_EXCEPTION(runtime_error("Compilation failed even though analysis was successful.")); + } + catch (UnimplementedFeatureError const& _e) + { + m_errorList.emplace_back(SyntaxTestError{ + "UnimplementedFeatureError", + errorMessage(_e), + "", + -1, + -1 + }); + } } void SyntaxTest::filterObtainedErrors() diff --git a/test/tools/CMakeLists.txt b/test/tools/CMakeLists.txt index 70a79ffdf..46156c219 100644 --- a/test/tools/CMakeLists.txt +++ b/test/tools/CMakeLists.txt @@ -29,6 +29,7 @@ add_executable(isoltest ../ExecutionFramework.cpp ../libsolidity/ABIJsonTest.cpp ../libsolidity/ASTJSONTest.cpp + ../libsolidity/SMTCheckerTest.cpp ../libsolidity/SMTCheckerJSONTest.cpp ../libyul/Common.cpp ../libyul/EWasmTranslationTest.cpp From b870e4ea31774fed327d8ae24ccaca51e43a623d Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Wed, 4 Dec 2019 13:11:13 +0100 Subject: [PATCH 06/12] Extract SMTChecker division tests --- test/libsolidity/SMTChecker.cpp | 80 ------------------- .../smtCheckerTests/operators/division_1.sol | 8 ++ .../smtCheckerTests/operators/division_2.sol | 7 ++ .../smtCheckerTests/operators/division_3.sol | 9 +++ .../smtCheckerTests/operators/division_4.sol | 8 ++ .../smtCheckerTests/operators/division_5.sol | 11 +++ .../smtCheckerTests/operators/division_6.sol | 13 +++ .../smtCheckerTests/operators/division_7.sol | 8 ++ 8 files changed, 64 insertions(+), 80 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/operators/division_1.sol create mode 100644 test/libsolidity/smtCheckerTests/operators/division_2.sol create mode 100644 test/libsolidity/smtCheckerTests/operators/division_3.sol create mode 100644 test/libsolidity/smtCheckerTests/operators/division_4.sol create mode 100644 test/libsolidity/smtCheckerTests/operators/division_5.sol create mode 100644 test/libsolidity/smtCheckerTests/operators/division_6.sol create mode 100644 test/libsolidity/smtCheckerTests/operators/division_7.sol diff --git a/test/libsolidity/SMTChecker.cpp b/test/libsolidity/SMTChecker.cpp index c7414d824..3513a31cb 100644 --- a/test/libsolidity/SMTChecker.cpp +++ b/test/libsolidity/SMTChecker.cpp @@ -59,86 +59,6 @@ protected: BOOST_FIXTURE_TEST_SUITE(SMTChecker, SMTCheckerFramework) -BOOST_AUTO_TEST_CASE(division) -{ - string text = R"( - contract C { - function f(uint x, uint y) public pure returns (uint) { - return x / y; - } - } - )"; - CHECK_WARNING(text, "Division by zero"); - text = R"( - contract C { - function f(uint x, uint y) public pure returns (uint) { - require(y != 0); - return x / y; - } - } - )"; - CHECK_SUCCESS_NO_WARNINGS(text); - text = R"( - contract C { - function f(int x, int y) public pure returns (int) { - require(y != 0); - return x / y; - } - } - )"; - CHECK_WARNING(text, "Overflow"); - text = R"( - contract C { - function f(int x, int y) public pure returns (int) { - require(y != 0); - require(y != -1); - return x / y; - } - } - )"; - CHECK_SUCCESS_NO_WARNINGS(text); - text = R"( - contract C { - function mul(uint256 a, uint256 b) internal pure returns (uint256) { - uint256 c; - if (a != 0) { - c = a * b; - require(c / a == b); - } - return c; - } - } - )"; - CHECK_SUCCESS_OR_WARNING(text, "might happen"); - text = R"( - contract C { - function mul(uint256 a, uint256 b) internal pure returns (uint256) { - if (a == 0) { - return 0; - } - // TODO remove when SMTChecker sees that this code is the `else` of the `return`. - require(a != 0); - uint256 c = a * b; - require(c / a == b); - return c; - } - } - )"; - CHECK_SUCCESS_OR_WARNING(text, "might happen"); - text = R"( - contract C { - function div(uint256 a, uint256 b) internal pure returns (uint256) { - require(b > 0); - uint256 c = a / b; - return c; - } - } - )"; - CHECK_SUCCESS_NO_WARNINGS(text); - - -} - BOOST_AUTO_TEST_CASE(division_truncates_correctly) { string text = R"( diff --git a/test/libsolidity/smtCheckerTests/operators/division_1.sol b/test/libsolidity/smtCheckerTests/operators/division_1.sol new file mode 100644 index 000000000..9f434cbbc --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/division_1.sol @@ -0,0 +1,8 @@ +pragma experimental SMTChecker; +contract C { + function f(uint x, uint y) public pure returns (uint) { + return x / y; + } +} +// ---- +// Warning: (111-116): Division by zero happens here diff --git a/test/libsolidity/smtCheckerTests/operators/division_2.sol b/test/libsolidity/smtCheckerTests/operators/division_2.sol new file mode 100644 index 000000000..9ccf84c47 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/division_2.sol @@ -0,0 +1,7 @@ +pragma experimental SMTChecker; +contract C { + function f(uint x, uint y) public pure returns (uint) { + require(y != 0); + return x / y; + } +} diff --git a/test/libsolidity/smtCheckerTests/operators/division_3.sol b/test/libsolidity/smtCheckerTests/operators/division_3.sol new file mode 100644 index 000000000..348a2e183 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/division_3.sol @@ -0,0 +1,9 @@ +pragma experimental SMTChecker; +contract C { + function f(int x, int y) public pure returns (int) { + require(y != 0); + return x / y; + } +} +// ---- +// Warning: (127-132): Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here diff --git a/test/libsolidity/smtCheckerTests/operators/division_4.sol b/test/libsolidity/smtCheckerTests/operators/division_4.sol new file mode 100644 index 000000000..ce67e3375 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/division_4.sol @@ -0,0 +1,8 @@ +pragma experimental SMTChecker; +contract C { + function f(int x, int y) public pure returns (int) { + require(y != 0); + require(y != -1); + return x / y; + } +} diff --git a/test/libsolidity/smtCheckerTests/operators/division_5.sol b/test/libsolidity/smtCheckerTests/operators/division_5.sol new file mode 100644 index 000000000..ed6966223 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/division_5.sol @@ -0,0 +1,11 @@ +pragma experimental SMTChecker; +contract C { + function mul(uint256 a, uint256 b) internal pure returns (uint256) { + uint256 c; + if (a != 0) { + c = a * b; + require(c / a == b); + } + return c; + } +} diff --git a/test/libsolidity/smtCheckerTests/operators/division_6.sol b/test/libsolidity/smtCheckerTests/operators/division_6.sol new file mode 100644 index 000000000..24e7a6325 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/division_6.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; +contract C { + function mul(uint256 a, uint256 b) internal pure returns (uint256) { + if (a == 0) { + return 0; + } + // TODO remove when SMTChecker sees that this code is the `else` of the `return`. + require(a != 0); + uint256 c = a * b; + require(c / a == b); + return c; + } +} diff --git a/test/libsolidity/smtCheckerTests/operators/division_7.sol b/test/libsolidity/smtCheckerTests/operators/division_7.sol new file mode 100644 index 000000000..bcde257eb --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/division_7.sol @@ -0,0 +1,8 @@ +pragma experimental SMTChecker; +contract C { + function div(uint256 a, uint256 b) internal pure returns (uint256) { + require(b > 0); + uint256 c = a / b; + return c; + } +} From ae6cdc34423d04a4bca1370da80ff3dcaeeb58c8 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Wed, 4 Dec 2019 13:17:05 +0100 Subject: [PATCH 07/12] Extract more SMTChecker division tests --- test/libsolidity/SMTChecker.cpp | 54 ------------------- .../division_truncates_correctly_1.sol | 8 +++ .../division_truncates_correctly_2.sol | 8 +++ .../division_truncates_correctly_3.sol | 8 +++ .../division_truncates_correctly_4.sol | 8 +++ .../division_truncates_correctly_5.sol | 8 +++ 6 files changed, 40 insertions(+), 54 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_1.sol create mode 100644 test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_2.sol create mode 100644 test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_3.sol create mode 100644 test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_4.sol create mode 100644 test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_5.sol diff --git a/test/libsolidity/SMTChecker.cpp b/test/libsolidity/SMTChecker.cpp index 3513a31cb..71e0557a6 100644 --- a/test/libsolidity/SMTChecker.cpp +++ b/test/libsolidity/SMTChecker.cpp @@ -59,60 +59,6 @@ protected: BOOST_FIXTURE_TEST_SUITE(SMTChecker, SMTCheckerFramework) -BOOST_AUTO_TEST_CASE(division_truncates_correctly) -{ - string text = R"( - contract C { - function f(uint x, uint y) public pure { - x = 7; - y = 2; - assert(x / y == 3); - } - } - )"; - CHECK_SUCCESS_NO_WARNINGS(text); - text = R"( - contract C { - function f(int x, int y) public pure { - x = 7; - y = 2; - assert(x / y == 3); - } - } - )"; - CHECK_SUCCESS_NO_WARNINGS(text); - text = R"( - contract C { - function f(int x, int y) public pure { - x = -7; - y = 2; - assert(x / y == -3); - } - } - )"; - CHECK_SUCCESS_NO_WARNINGS(text); - text = R"( - contract C { - function f(int x, int y) public pure { - x = 7; - y = -2; - assert(x / y == -3); - } - } - )"; - CHECK_SUCCESS_NO_WARNINGS(text); - text = R"( - contract C { - function f(int x, int y) public pure { - x = -7; - y = -2; - assert(x / y == 3); - } - } - )"; - CHECK_SUCCESS_NO_WARNINGS(text); -} - BOOST_AUTO_TEST_CASE(compound_assignment_division) { string text = R"( diff --git a/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_1.sol b/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_1.sol new file mode 100644 index 000000000..6bbc56a40 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_1.sol @@ -0,0 +1,8 @@ +pragma experimental SMTChecker; +contract C { + function f(uint x, uint y) public pure { + x = 7; + y = 2; + assert(x / y == 3); + } +} diff --git a/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_2.sol b/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_2.sol new file mode 100644 index 000000000..6478e3298 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_2.sol @@ -0,0 +1,8 @@ +pragma experimental SMTChecker; +contract C { + function f(int x, int y) public pure { + x = 7; + y = 2; + assert(x / y == 3); + } +} diff --git a/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_3.sol b/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_3.sol new file mode 100644 index 000000000..1e58d709a --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_3.sol @@ -0,0 +1,8 @@ +pragma experimental SMTChecker; +contract C { + function f(int x, int y) public pure { + x = -7; + y = 2; + assert(x / y == -3); + } +} diff --git a/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_4.sol b/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_4.sol new file mode 100644 index 000000000..9f8452bb2 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_4.sol @@ -0,0 +1,8 @@ +pragma experimental SMTChecker; +contract C { + function f(int x, int y) public pure { + x = 7; + y = -2; + assert(x / y == -3); + } +} diff --git a/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_5.sol b/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_5.sol new file mode 100644 index 000000000..2ac471156 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_5.sol @@ -0,0 +1,8 @@ +pragma experimental SMTChecker; +contract C { + function f(int x, int y) public pure { + x = -7; + y = -2; + assert(x / y == 3); + } +} From 02343208ada9364f0e973aeae9c14a9db7d87e88 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Wed, 4 Dec 2019 13:20:43 +0100 Subject: [PATCH 08/12] Extract SMTChecker compound assignment division tests --- test/libsolidity/SMTChecker.cpp | 42 ------------------- .../compound_assignment_division_1.sol | 12 ++++++ .../compound_assignment_division_2.sol | 13 ++++++ .../compound_assignment_division_3.sol | 13 ++++++ 4 files changed, 38 insertions(+), 42 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/operators/compound_assignment_division_1.sol create mode 100644 test/libsolidity/smtCheckerTests/operators/compound_assignment_division_2.sol create mode 100644 test/libsolidity/smtCheckerTests/operators/compound_assignment_division_3.sol diff --git a/test/libsolidity/SMTChecker.cpp b/test/libsolidity/SMTChecker.cpp index 71e0557a6..ead2ea44c 100644 --- a/test/libsolidity/SMTChecker.cpp +++ b/test/libsolidity/SMTChecker.cpp @@ -59,48 +59,6 @@ protected: BOOST_FIXTURE_TEST_SUITE(SMTChecker, SMTCheckerFramework) -BOOST_AUTO_TEST_CASE(compound_assignment_division) -{ - string text = R"( - contract C { - function f(uint x) public pure { - require(x == 2); - uint y = 10; - y /= y / x; - assert(y == x); - assert(y == 0); - } - } - )"; - CHECK_WARNING(text, "Assertion violation"); - text = R"( - contract C { - uint[] array; - function f(uint x, uint p) public { - require(x == 2); - array[p] = 10; - array[p] /= array[p] / x; - assert(array[p] == x); - assert(array[p] == 0); - } - } - )"; - CHECK_WARNING(text, "Assertion violation"); - text = R"( - contract C { - mapping (uint => uint) map; - function f(uint x, uint p) public { - require(x == 2); - map[p] = 10; - map[p] /= map[p] / x; - assert(map[p] == x); - assert(map[p] == 0); - } - } - )"; - CHECK_WARNING(text, "Assertion violation"); -} - BOOST_AUTO_TEST_CASE(mod) { string text = R"( diff --git a/test/libsolidity/smtCheckerTests/operators/compound_assignment_division_1.sol b/test/libsolidity/smtCheckerTests/operators/compound_assignment_division_1.sol new file mode 100644 index 000000000..2e07fc9c1 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/compound_assignment_division_1.sol @@ -0,0 +1,12 @@ +pragma experimental SMTChecker; +contract C { + function f(uint x) public pure { + require(x == 2); + uint y = 10; + y /= y / x; + assert(y == x); + assert(y == 0); + } +} +// ---- +// Warning: (147-161): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/operators/compound_assignment_division_2.sol b/test/libsolidity/smtCheckerTests/operators/compound_assignment_division_2.sol new file mode 100644 index 000000000..f7c347047 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/compound_assignment_division_2.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; +contract C { + uint[] array; + function f(uint x, uint p) public { + require(x == 2); + array[p] = 10; + array[p] /= array[p] / x; + assert(array[p] == x); + assert(array[p] == 0); + } +} +// ---- +// Warning: (188-209): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/operators/compound_assignment_division_3.sol b/test/libsolidity/smtCheckerTests/operators/compound_assignment_division_3.sol new file mode 100644 index 000000000..5b466f173 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/compound_assignment_division_3.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; +contract C { + mapping (uint => uint) map; + function f(uint x, uint p) public { + require(x == 2); + map[p] = 10; + map[p] /= map[p] / x; + assert(map[p] == x); + assert(map[p] == 0); + } +} +// ---- +// Warning: (194-213): Assertion violation happens here From 77b9416d3eb511249a1527f4eb8e0a24e762af38 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Wed, 4 Dec 2019 13:21:55 +0100 Subject: [PATCH 09/12] Extract SMTChecker mod test --- test/libsolidity/SMTChecker.cpp | 16 ---------------- .../smtCheckerTests/operators/mod.sol | 10 ++++++++++ 2 files changed, 10 insertions(+), 16 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/operators/mod.sol diff --git a/test/libsolidity/SMTChecker.cpp b/test/libsolidity/SMTChecker.cpp index ead2ea44c..52ba30b3f 100644 --- a/test/libsolidity/SMTChecker.cpp +++ b/test/libsolidity/SMTChecker.cpp @@ -59,22 +59,6 @@ protected: BOOST_FIXTURE_TEST_SUITE(SMTChecker, SMTCheckerFramework) -BOOST_AUTO_TEST_CASE(mod) -{ - string text = R"( - contract C { - function f(int x, int y) public pure { - require(y == -10); - require(x == 100); - int z1 = x % y; - int z2 = x % -y; - assert(z1 == z2); - } - } - )"; - CHECK_SUCCESS_NO_WARNINGS(text); -} - BOOST_AUTO_TEST_CASE(import_base) { CompilerStack c; diff --git a/test/libsolidity/smtCheckerTests/operators/mod.sol b/test/libsolidity/smtCheckerTests/operators/mod.sol new file mode 100644 index 000000000..6a0730c01 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/mod.sol @@ -0,0 +1,10 @@ +pragma experimental SMTChecker; +contract C { + function f(int x, int y) public pure { + require(y == -10); + require(x == 100); + int z1 = x % y; + int z2 = x % -y; + assert(z1 == z2); + } +} From 8d5f5a5cbeb2a00929b3a013bf513f9958c4de41 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Wed, 4 Dec 2019 13:26:22 +0100 Subject: [PATCH 10/12] Remove deprecated code --- test/libsolidity/AnalysisFramework.h | 13 ------------- 1 file changed, 13 deletions(-) diff --git a/test/libsolidity/AnalysisFramework.h b/test/libsolidity/AnalysisFramework.h index 8eae8c125..3fcb9e74a 100644 --- a/test/libsolidity/AnalysisFramework.h +++ b/test/libsolidity/AnalysisFramework.h @@ -153,19 +153,6 @@ do \ } \ while(0) -#define CHECK_SUCCESS_OR_WARNING(text, substring) \ -do \ -{ \ - auto sourceAndError = parseAnalyseAndReturnError((text), true); \ - auto const& errors = sourceAndError.second; \ - if (!errors.empty()) \ - { \ - auto message = searchErrors(errors, {{(Error::Type::Warning), (substring)}}); \ - BOOST_CHECK_MESSAGE(message.empty(), message); \ - } \ -} \ -while(0) - } } } From beed0f6a27bde67656b95a2225cb32d5329a3850 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Wed, 4 Dec 2019 16:39:34 +0100 Subject: [PATCH 11/12] Set tests that CVC4 can't handle to Z3 only --- .../inheritance/implicit_constructor_hierarchy.sol | 2 ++ .../inheritance/implicit_only_constructor_hierarchy.sol | 2 ++ test/libsolidity/smtCheckerTests/invariants/loop_basic.sol | 2 ++ test/libsolidity/smtCheckerTests/invariants/loop_basic_for.sol | 3 ++- test/libsolidity/smtCheckerTests/invariants/loop_nested.sol | 2 ++ .../libsolidity/smtCheckerTests/invariants/loop_nested_for.sol | 2 ++ .../libsolidity/smtCheckerTests/invariants/state_machine_1.sol | 2 ++ .../smtCheckerTests/invariants/state_machine_1_fail.sol | 2 ++ test/libsolidity/smtCheckerTests/loops/do_while_1_fail.sol | 2 ++ .../smtCheckerTests/loops/do_while_1_false_positives.sol | 2 ++ test/libsolidity/smtCheckerTests/loops/do_while_break.sol | 2 ++ test/libsolidity/smtCheckerTests/loops/do_while_break_2.sol | 2 ++ .../smtCheckerTests/loops/do_while_break_2_fail.sol | 2 ++ test/libsolidity/smtCheckerTests/loops/do_while_break_fail.sol | 2 ++ test/libsolidity/smtCheckerTests/loops/do_while_continue.sol | 2 ++ test/libsolidity/smtCheckerTests/loops/for_1_break.sol | 2 ++ test/libsolidity/smtCheckerTests/loops/for_1_break_fail.sol | 2 ++ test/libsolidity/smtCheckerTests/loops/for_1_continue.sol | 2 ++ test/libsolidity/smtCheckerTests/loops/for_1_continue_fail.sol | 2 ++ test/libsolidity/smtCheckerTests/loops/for_1_fail.sol | 2 ++ .../libsolidity/smtCheckerTests/loops/for_1_false_positive.sol | 2 ++ test/libsolidity/smtCheckerTests/loops/for_break_direct.sol | 2 ++ test/libsolidity/smtCheckerTests/loops/for_loop_1.sol | 2 ++ test/libsolidity/smtCheckerTests/loops/for_loop_2.sol | 2 ++ test/libsolidity/smtCheckerTests/loops/for_loop_3.sol | 2 ++ test/libsolidity/smtCheckerTests/loops/for_loop_4.sol | 2 ++ test/libsolidity/smtCheckerTests/loops/for_loop_5.sol | 2 ++ test/libsolidity/smtCheckerTests/loops/for_loop_6.sol | 3 ++- .../loops/for_loop_array_assignment_memory_memory.sol | 2 ++ .../loops/for_loop_array_assignment_memory_storage.sol | 2 ++ .../loops/for_loop_array_assignment_storage_memory.sol | 2 ++ .../loops/for_loop_array_assignment_storage_storage.sol | 2 ++ .../smtCheckerTests/loops/for_loop_trivial_condition_1.sol | 2 ++ .../smtCheckerTests/loops/for_loop_trivial_condition_2.sol | 2 ++ .../smtCheckerTests/loops/for_loop_trivial_condition_3.sol | 2 ++ .../smtCheckerTests/loops/for_loop_unreachable_1.sol | 2 ++ test/libsolidity/smtCheckerTests/loops/while_1.sol | 2 ++ test/libsolidity/smtCheckerTests/loops/while_1_break.sol | 2 ++ test/libsolidity/smtCheckerTests/loops/while_1_break_fail.sol | 2 ++ test/libsolidity/smtCheckerTests/loops/while_1_continue.sol | 2 ++ .../smtCheckerTests/loops/while_1_continue_fail.sol | 2 ++ test/libsolidity/smtCheckerTests/loops/while_1_fail.sol | 2 ++ test/libsolidity/smtCheckerTests/loops/while_1_infinite.sol | 3 ++- test/libsolidity/smtCheckerTests/loops/while_2.sol | 2 ++ test/libsolidity/smtCheckerTests/loops/while_2_break.sol | 2 ++ test/libsolidity/smtCheckerTests/loops/while_2_break_fail.sol | 2 ++ test/libsolidity/smtCheckerTests/loops/while_2_fail.sol | 2 ++ test/libsolidity/smtCheckerTests/loops/while_break_direct.sol | 2 ++ .../loops/while_loop_array_assignment_memory_memory.sol | 2 ++ .../loops/while_loop_array_assignment_memory_storage.sol | 2 ++ test/libsolidity/smtCheckerTests/loops/while_loop_simple_1.sol | 2 ++ test/libsolidity/smtCheckerTests/loops/while_loop_simple_2.sol | 2 ++ test/libsolidity/smtCheckerTests/loops/while_loop_simple_3.sol | 2 ++ test/libsolidity/smtCheckerTests/loops/while_loop_simple_4.sol | 3 ++- test/libsolidity/smtCheckerTests/loops/while_loop_simple_5.sol | 2 ++ test/libsolidity/smtCheckerTests/loops/while_nested_break.sol | 2 ++ .../smtCheckerTests/loops/while_nested_break_fail.sol | 2 ++ .../smtCheckerTests/loops/while_nested_continue.sol | 2 ++ .../smtCheckerTests/loops/while_nested_continue_fail.sol | 2 ++ .../smtCheckerTests/operators/delete_array_index_2d.sol | 2 ++ test/libsolidity/smtCheckerTests/types/mapping_4.sol | 3 ++- 61 files changed, 122 insertions(+), 5 deletions(-) diff --git a/test/libsolidity/smtCheckerTests/inheritance/implicit_constructor_hierarchy.sol b/test/libsolidity/smtCheckerTests/inheritance/implicit_constructor_hierarchy.sol index 1eeb4e640..37210a843 100644 --- a/test/libsolidity/smtCheckerTests/inheritance/implicit_constructor_hierarchy.sol +++ b/test/libsolidity/smtCheckerTests/inheritance/implicit_constructor_hierarchy.sol @@ -14,3 +14,5 @@ contract C is B { assert(x == 2); } } +// ==== +// SMTSolvers: z3 diff --git a/test/libsolidity/smtCheckerTests/inheritance/implicit_only_constructor_hierarchy.sol b/test/libsolidity/smtCheckerTests/inheritance/implicit_only_constructor_hierarchy.sol index c724b7289..1ff4219d0 100644 --- a/test/libsolidity/smtCheckerTests/inheritance/implicit_only_constructor_hierarchy.sol +++ b/test/libsolidity/smtCheckerTests/inheritance/implicit_only_constructor_hierarchy.sol @@ -18,3 +18,5 @@ contract C is B { assert(x == 0); } } +// ==== +// SMTSolvers: z3 diff --git a/test/libsolidity/smtCheckerTests/invariants/loop_basic.sol b/test/libsolidity/smtCheckerTests/invariants/loop_basic.sol index 9bfdaf643..d24b19e1e 100644 --- a/test/libsolidity/smtCheckerTests/invariants/loop_basic.sol +++ b/test/libsolidity/smtCheckerTests/invariants/loop_basic.sol @@ -9,3 +9,5 @@ contract Simple { assert(y == x); } } +// ==== +// SMTSolvers: z3 diff --git a/test/libsolidity/smtCheckerTests/invariants/loop_basic_for.sol b/test/libsolidity/smtCheckerTests/invariants/loop_basic_for.sol index 55019cf0c..3e059b516 100644 --- a/test/libsolidity/smtCheckerTests/invariants/loop_basic_for.sol +++ b/test/libsolidity/smtCheckerTests/invariants/loop_basic_for.sol @@ -7,4 +7,5 @@ contract Simple { assert(y == x); } } -// ---- +// ==== +// SMTSolvers: z3 diff --git a/test/libsolidity/smtCheckerTests/invariants/loop_nested.sol b/test/libsolidity/smtCheckerTests/invariants/loop_nested.sol index b17140a0d..867403b61 100644 --- a/test/libsolidity/smtCheckerTests/invariants/loop_nested.sol +++ b/test/libsolidity/smtCheckerTests/invariants/loop_nested.sol @@ -15,3 +15,5 @@ contract Simple { assert(y == x); } } +// ==== +// SMTSolvers: z3 diff --git a/test/libsolidity/smtCheckerTests/invariants/loop_nested_for.sol b/test/libsolidity/smtCheckerTests/invariants/loop_nested_for.sol index ac7f0f7d1..9cfd4569f 100644 --- a/test/libsolidity/smtCheckerTests/invariants/loop_nested_for.sol +++ b/test/libsolidity/smtCheckerTests/invariants/loop_nested_for.sol @@ -12,3 +12,5 @@ contract Simple { assert(y == x); } } +// ==== +// SMTSolvers: z3 diff --git a/test/libsolidity/smtCheckerTests/invariants/state_machine_1.sol b/test/libsolidity/smtCheckerTests/invariants/state_machine_1.sol index 9cc43504c..c181e6f51 100644 --- a/test/libsolidity/smtCheckerTests/invariants/state_machine_1.sol +++ b/test/libsolidity/smtCheckerTests/invariants/state_machine_1.sol @@ -30,3 +30,5 @@ contract C { assert(x < 9); } } +// ==== +// SMTSolvers: z3 diff --git a/test/libsolidity/smtCheckerTests/invariants/state_machine_1_fail.sol b/test/libsolidity/smtCheckerTests/invariants/state_machine_1_fail.sol index 7699337a1..997113689 100644 --- a/test/libsolidity/smtCheckerTests/invariants/state_machine_1_fail.sol +++ b/test/libsolidity/smtCheckerTests/invariants/state_machine_1_fail.sol @@ -28,5 +28,7 @@ contract C { assert(x < 2); } } +// ==== +// SMTSolvers: z3 // ---- // Warning: (311-324): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/do_while_1_fail.sol b/test/libsolidity/smtCheckerTests/loops/do_while_1_fail.sol index 38be76ca0..ebf023e27 100644 --- a/test/libsolidity/smtCheckerTests/loops/do_while_1_fail.sol +++ b/test/libsolidity/smtCheckerTests/loops/do_while_1_fail.sol @@ -11,6 +11,8 @@ contract C assert(x < 14); } } +// ==== +// SMTSolvers: z3 // ---- // Warning: (150-155): Overflow (resulting value larger than 2**256 - 1) happens here // Warning: (179-193): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/do_while_1_false_positives.sol b/test/libsolidity/smtCheckerTests/loops/do_while_1_false_positives.sol index c5f5cf44d..f46a3f5a4 100644 --- a/test/libsolidity/smtCheckerTests/loops/do_while_1_false_positives.sol +++ b/test/libsolidity/smtCheckerTests/loops/do_while_1_false_positives.sol @@ -13,5 +13,7 @@ contract C assert(x > 0); } } +// ==== +// SMTSolvers: z3 // ---- // Warning: (150-155): Overflow (resulting value larger than 2**256 - 1) happens here diff --git a/test/libsolidity/smtCheckerTests/loops/do_while_break.sol b/test/libsolidity/smtCheckerTests/loops/do_while_break.sol index 7bdcc251e..0c870972d 100644 --- a/test/libsolidity/smtCheckerTests/loops/do_while_break.sol +++ b/test/libsolidity/smtCheckerTests/loops/do_while_break.sol @@ -10,6 +10,8 @@ contract C { assert(x == 0); } } +// ==== +// SMTSolvers: z3 // ---- // Warning: (104-109): Unreachable code. // Warning: (122-128): Unreachable code. diff --git a/test/libsolidity/smtCheckerTests/loops/do_while_break_2.sol b/test/libsolidity/smtCheckerTests/loops/do_while_break_2.sol index c3635a976..a209c4807 100644 --- a/test/libsolidity/smtCheckerTests/loops/do_while_break_2.sol +++ b/test/libsolidity/smtCheckerTests/loops/do_while_break_2.sol @@ -14,6 +14,8 @@ contract C { assert(a == 1); } } +// ==== +// SMTSolvers: z3 // ---- // Warning: (128-133): Unreachable code. // Warning: (147-151): Unreachable code. diff --git a/test/libsolidity/smtCheckerTests/loops/do_while_break_2_fail.sol b/test/libsolidity/smtCheckerTests/loops/do_while_break_2_fail.sol index 4b1824e23..90f4d3cf8 100644 --- a/test/libsolidity/smtCheckerTests/loops/do_while_break_2_fail.sol +++ b/test/libsolidity/smtCheckerTests/loops/do_while_break_2_fail.sol @@ -14,6 +14,8 @@ contract C { assert(a == 2); } } +// ==== +// SMTSolvers: z3 // ---- // Warning: (128-133): Unreachable code. // Warning: (147-151): Unreachable code. diff --git a/test/libsolidity/smtCheckerTests/loops/do_while_break_fail.sol b/test/libsolidity/smtCheckerTests/loops/do_while_break_fail.sol index d8cd8f0c7..fa23aafd2 100644 --- a/test/libsolidity/smtCheckerTests/loops/do_while_break_fail.sol +++ b/test/libsolidity/smtCheckerTests/loops/do_while_break_fail.sol @@ -10,6 +10,8 @@ contract C { assert(x == 1); } } +// ==== +// SMTSolvers: z3 // ---- // Warning: (104-109): Unreachable code. // Warning: (122-128): Unreachable code. diff --git a/test/libsolidity/smtCheckerTests/loops/do_while_continue.sol b/test/libsolidity/smtCheckerTests/loops/do_while_continue.sol index 9527b1e46..88c38ebda 100644 --- a/test/libsolidity/smtCheckerTests/loops/do_while_continue.sol +++ b/test/libsolidity/smtCheckerTests/loops/do_while_continue.sol @@ -10,5 +10,7 @@ contract C { assert(x == 0); } } +// ==== +// SMTSolvers: z3 // ---- // Warning: (107-112): Unreachable code. diff --git a/test/libsolidity/smtCheckerTests/loops/for_1_break.sol b/test/libsolidity/smtCheckerTests/loops/for_1_break.sol index 32dc51dd8..c6b8eedb4 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_1_break.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_1_break.sol @@ -15,3 +15,5 @@ contract C assert(x >= 10); } } +// ==== +// SMTSolvers: z3 diff --git a/test/libsolidity/smtCheckerTests/loops/for_1_break_fail.sol b/test/libsolidity/smtCheckerTests/loops/for_1_break_fail.sol index b25d5fdad..2422cc177 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_1_break_fail.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_1_break_fail.sol @@ -14,5 +14,7 @@ contract C assert(x >= 10); } } +// ==== +// SMTSolvers: z3 // ---- // Warning: (201-216): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/for_1_continue.sol b/test/libsolidity/smtCheckerTests/loops/for_1_continue.sol index 7ba4c611a..fba0909d3 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_1_continue.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_1_continue.sol @@ -13,3 +13,5 @@ contract C assert(x > 0); } } +// ==== +// SMTSolvers: z3 diff --git a/test/libsolidity/smtCheckerTests/loops/for_1_continue_fail.sol b/test/libsolidity/smtCheckerTests/loops/for_1_continue_fail.sol index fb0fcb6c7..7f73f86c1 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_1_continue_fail.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_1_continue_fail.sol @@ -14,5 +14,7 @@ contract C assert(x > 15); } } +// ==== +// SMTSolvers: z3 // ---- // Warning: (185-199): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/for_1_fail.sol b/test/libsolidity/smtCheckerTests/loops/for_1_fail.sol index 33ecb9925..11c08b768 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_1_fail.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_1_fail.sol @@ -11,6 +11,8 @@ contract C assert(x < 14); } } +// ==== +// SMTSolvers: z3 // ---- // Warning: (176-181): Overflow (resulting value larger than 2**256 - 1) happens here // Warning: (189-203): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol b/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol index 11cd22d11..e57c62313 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol @@ -13,6 +13,8 @@ contract C assert(x > 0); } } +// ==== +// SMTSolvers: z3 // ---- // Warning: (296-309): Error trying to invoke SMT solver. // Warning: (176-181): Overflow (resulting value larger than 2**256 - 1) happens here diff --git a/test/libsolidity/smtCheckerTests/loops/for_break_direct.sol b/test/libsolidity/smtCheckerTests/loops/for_break_direct.sol index 2d932b438..df99d17af 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_break_direct.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_break_direct.sol @@ -8,5 +8,7 @@ contract C assert(x == 0); } } +// ==== +// SMTSolvers: z3 // ---- // Warning: (102-105): Unreachable code. diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_1.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_1.sol index 8988efadb..c3e66e5e3 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_loop_1.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_1.sol @@ -6,3 +6,5 @@ contract C { assert(x == 2); } } +// ==== +// SMTSolvers: z3 diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_2.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_2.sol index 58c9f3a78..b409ae987 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_loop_2.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_2.sol @@ -6,3 +6,5 @@ contract C { } } } +// ==== +// SMTSolvers: z3 diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_3.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_3.sol index 8bf9bdc7e..578c7f5a8 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_loop_3.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_3.sol @@ -6,3 +6,5 @@ contract C { } } } +// ==== +// SMTSolvers: z3 diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_4.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_4.sol index 4d082026d..c242a5800 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_loop_4.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_4.sol @@ -6,5 +6,7 @@ contract C { } } } +// ==== +// SMTSolvers: z3 // ---- // 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 index eb62d36ed..066a3e76d 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_loop_5.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_5.sol @@ -8,5 +8,7 @@ contract C { assert(y == 3); } } +// ==== +// SMTSolvers: z3 // ---- // Warning: (167-181): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_6.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_6.sol index 9c54822e3..06895a9e3 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_loop_6.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_6.sol @@ -9,4 +9,5 @@ contract C { assert(y < 4); } } -// ---- +// ==== +// SMTSolvers: z3 diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_memory_memory.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_memory_memory.sol index 0694493f5..1a9216de0 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_memory_memory.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_memory_memory.sol @@ -14,6 +14,8 @@ contract LoopFor2 { assert(b[0] == 900); } } +// ==== +// SMTSolvers: z3 // ---- // Warning: (281-301): Assertion violation happens here // Warning: (305-324): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_memory_storage.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_memory_storage.sol index d06f1cb5d..82a91bf75 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_memory_storage.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_memory_storage.sol @@ -16,6 +16,8 @@ contract LoopFor2 { assert(b[0] == 900); } } +// ==== +// SMTSolvers: z3 // ---- // Warning: (274-294): Assertion violation happens here // Warning: (321-340): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_memory.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_memory.sol index d7d88424a..9e7a83866 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_memory.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_memory.sol @@ -17,5 +17,7 @@ contract LoopFor2 { assert(b[0] == 900); } } +// ==== +// SMTSolvers: z3 // ---- // Warning: (312-331): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_storage.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_storage.sol index a6793af13..8146a7f19 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_storage.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_storage.sol @@ -17,6 +17,8 @@ contract LoopFor2 { assert(b[0] == 900); } } +// ==== +// SMTSolvers: z3 // ---- // Warning: (290-309): Assertion violation happens here // Warning: (313-332): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_1.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_1.sol index 0c65b2b6b..321da4e4a 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_1.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_1.sol @@ -6,5 +6,7 @@ contract C { assert(x == 2); } } +// ==== +// SMTSolvers: z3 // ---- // Warning: (122-128): Condition is always true. diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_2.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_2.sol index d3cb887b4..2bca54b24 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_2.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_2.sol @@ -9,5 +9,7 @@ contract C { assert(x == 2); } } +// ==== +// SMTSolvers: z3 // ---- // Warning: (138-144): Condition is always true. diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_3.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_3.sol index bb928e2c1..433e003c1 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_3.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_3.sol @@ -13,5 +13,7 @@ contract C { assert(x == 2); } } +// ==== +// SMTSolvers: z3 // ---- // Warning: (115-121): Unused local variable. diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_unreachable_1.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_unreachable_1.sol index f77a983af..563e7cb16 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_loop_unreachable_1.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_unreachable_1.sol @@ -6,5 +6,7 @@ contract C { assert(x == 2); } } +// ==== +// SMTSolvers: z3 // ---- // Warning: (122-127): Condition is always false. diff --git a/test/libsolidity/smtCheckerTests/loops/while_1.sol b/test/libsolidity/smtCheckerTests/loops/while_1.sol index cb7fc5272..a2a251c5b 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_1.sol +++ b/test/libsolidity/smtCheckerTests/loops/while_1.sol @@ -13,4 +13,6 @@ contract C assert(x > 0); } } +// ==== +// SMTSolvers: z3 // ---- diff --git a/test/libsolidity/smtCheckerTests/loops/while_1_break.sol b/test/libsolidity/smtCheckerTests/loops/while_1_break.sol index 6deb0461b..d2c2eda68 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_1_break.sol +++ b/test/libsolidity/smtCheckerTests/loops/while_1_break.sol @@ -15,3 +15,5 @@ contract C assert(x >= 10); } } +// ==== +// SMTSolvers: z3 diff --git a/test/libsolidity/smtCheckerTests/loops/while_1_break_fail.sol b/test/libsolidity/smtCheckerTests/loops/while_1_break_fail.sol index f187eac3e..1e8157cee 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_1_break_fail.sol +++ b/test/libsolidity/smtCheckerTests/loops/while_1_break_fail.sol @@ -15,5 +15,7 @@ contract C assert(x >= 10); } } +// ==== +// SMTSolvers: z3 // ---- // Warning: (218-233): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/while_1_continue.sol b/test/libsolidity/smtCheckerTests/loops/while_1_continue.sol index ff22d139e..9c86b8824 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_1_continue.sol +++ b/test/libsolidity/smtCheckerTests/loops/while_1_continue.sol @@ -14,3 +14,5 @@ contract C assert(x >= 10); } } +// ==== +// SMTSolvers: z3 diff --git a/test/libsolidity/smtCheckerTests/loops/while_1_continue_fail.sol b/test/libsolidity/smtCheckerTests/loops/while_1_continue_fail.sol index c8e14258e..06b6eba2e 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_1_continue_fail.sol +++ b/test/libsolidity/smtCheckerTests/loops/while_1_continue_fail.sol @@ -17,6 +17,8 @@ contract C assert(x >= 17); } } +// ==== +// SMTSolvers: z3 // ---- // Warning: (169-176): Unreachable code. // Warning: (227-242): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/while_1_fail.sol b/test/libsolidity/smtCheckerTests/loops/while_1_fail.sol index 6964f7c87..793907bdd 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_1_fail.sol +++ b/test/libsolidity/smtCheckerTests/loops/while_1_fail.sol @@ -10,5 +10,7 @@ contract C assert(x < 14); } } +// ==== +// SMTSolvers: z3 // ---- // Warning: (139-153): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/while_1_infinite.sol b/test/libsolidity/smtCheckerTests/loops/while_1_infinite.sol index 54b32b432..99cc76afb 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_1_infinite.sol +++ b/test/libsolidity/smtCheckerTests/loops/while_1_infinite.sol @@ -18,4 +18,5 @@ contract C assert(x > 0); } } -// ---- +// ==== +// SMTSolvers: z3 diff --git a/test/libsolidity/smtCheckerTests/loops/while_2.sol b/test/libsolidity/smtCheckerTests/loops/while_2.sol index 00a71aca6..f01c51efe 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_2.sol +++ b/test/libsolidity/smtCheckerTests/loops/while_2.sol @@ -11,3 +11,5 @@ contract C { assert(x < 2); } } +// ==== +// SMTSolvers: z3 diff --git a/test/libsolidity/smtCheckerTests/loops/while_2_break.sol b/test/libsolidity/smtCheckerTests/loops/while_2_break.sol index 12fe93b55..680b42be0 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_2_break.sol +++ b/test/libsolidity/smtCheckerTests/loops/while_2_break.sol @@ -12,5 +12,7 @@ contract C assert(x == 1); } } +// ==== +// SMTSolvers: z3 // ---- // Warning: (128-131): Unreachable code. diff --git a/test/libsolidity/smtCheckerTests/loops/while_2_break_fail.sol b/test/libsolidity/smtCheckerTests/loops/while_2_break_fail.sol index efd9bb18b..78cac6021 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_2_break_fail.sol +++ b/test/libsolidity/smtCheckerTests/loops/while_2_break_fail.sol @@ -11,6 +11,8 @@ contract C assert(x == 2); } } +// ==== +// SMTSolvers: z3 // ---- // Warning: (120-123): Unreachable code. // Warning: (131-145): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/while_2_fail.sol b/test/libsolidity/smtCheckerTests/loops/while_2_fail.sol index 3c3e50468..74d36522d 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_2_fail.sol +++ b/test/libsolidity/smtCheckerTests/loops/while_2_fail.sol @@ -11,4 +11,6 @@ contract C { assert(x == 2); } } +// ==== +// SMTSolvers: z3 // ---- diff --git a/test/libsolidity/smtCheckerTests/loops/while_break_direct.sol b/test/libsolidity/smtCheckerTests/loops/while_break_direct.sol index 8961f97d8..0ed591599 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_break_direct.sol +++ b/test/libsolidity/smtCheckerTests/loops/while_break_direct.sol @@ -9,5 +9,7 @@ contract C assert(x == 0); } } +// ==== +// SMTSolvers: z3 // ---- // Warning: (98-104): Condition is always true. diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_memory.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_memory.sol index 132ec285e..92a8a8be7 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_memory.sol +++ b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_memory.sol @@ -16,6 +16,8 @@ contract LoopFor2 { assert(b[0] == 900); } } +// ==== +// SMTSolvers: z3 // ---- // Warning: (281-301): Assertion violation happens here // Warning: (305-324): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_storage.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_storage.sol index 70bd231bb..c4669b1ba 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_storage.sol +++ b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_storage.sol @@ -20,6 +20,8 @@ contract LoopFor2 { assert(b[0] == 900); } } +// ==== +// SMTSolvers: z3 // ---- // Warning: (362-382): Assertion violation happens here // Warning: (409-428): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_simple_1.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_simple_1.sol index 9b5d04c37..3caaf1388 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_loop_simple_1.sol +++ b/test/libsolidity/smtCheckerTests/loops/while_loop_simple_1.sol @@ -9,5 +9,7 @@ contract C { assert(x == 2); } } +// ==== +// SMTSolvers: z3 // ---- // Warning: (194-208): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_simple_2.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_simple_2.sol index 92a3f0fed..67d26068b 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_loop_simple_2.sol +++ b/test/libsolidity/smtCheckerTests/loops/while_loop_simple_2.sol @@ -7,3 +7,5 @@ contract C { } } } +// ==== +// SMTSolvers: z3 diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_simple_3.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_simple_3.sol index f3634edb2..7476d2853 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_loop_simple_3.sol +++ b/test/libsolidity/smtCheckerTests/loops/while_loop_simple_3.sol @@ -7,5 +7,7 @@ contract C { assert(x == 2); } } +// ==== +// SMTSolvers: z3 // ---- // Warning: (187-201): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_simple_4.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_simple_4.sol index 792a90e23..c7c2a9a9b 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_loop_simple_4.sol +++ b/test/libsolidity/smtCheckerTests/loops/while_loop_simple_4.sol @@ -7,4 +7,5 @@ contract C { assert(x != 2); } } -// ---- +// ==== +// SMTSolvers: z3 diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_simple_5.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_simple_5.sol index 6c81e36fb..c85e7e3fb 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_loop_simple_5.sol +++ b/test/libsolidity/smtCheckerTests/loops/while_loop_simple_5.sol @@ -8,5 +8,7 @@ contract C { assert(x == 7); } } +// ==== +// SMTSolvers: z3 // ---- // Warning: (216-230): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/while_nested_break.sol b/test/libsolidity/smtCheckerTests/loops/while_nested_break.sol index b79e714ce..41e01585e 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_nested_break.sol +++ b/test/libsolidity/smtCheckerTests/loops/while_nested_break.sol @@ -28,3 +28,5 @@ contract C assert(x >= 15); } } +// ==== +// SMTSolvers: z3 diff --git a/test/libsolidity/smtCheckerTests/loops/while_nested_break_fail.sol b/test/libsolidity/smtCheckerTests/loops/while_nested_break_fail.sol index 986e7205b..e9752b3a8 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_nested_break_fail.sol +++ b/test/libsolidity/smtCheckerTests/loops/while_nested_break_fail.sol @@ -28,6 +28,8 @@ contract C assert(x >= 20); } } +// ==== +// SMTSolvers: z3 // ---- // Warning: (329-344): Assertion violation happens here // Warning: (380-395): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/while_nested_continue.sol b/test/libsolidity/smtCheckerTests/loops/while_nested_continue.sol index 775d0b92f..72b0c4d24 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_nested_continue.sol +++ b/test/libsolidity/smtCheckerTests/loops/while_nested_continue.sol @@ -26,3 +26,5 @@ contract C assert(x >= 15); } } +// ==== +// SMTSolvers: z3 diff --git a/test/libsolidity/smtCheckerTests/loops/while_nested_continue_fail.sol b/test/libsolidity/smtCheckerTests/loops/while_nested_continue_fail.sol index 71238c3be..4447cf6d7 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_nested_continue_fail.sol +++ b/test/libsolidity/smtCheckerTests/loops/while_nested_continue_fail.sol @@ -26,6 +26,8 @@ contract C assert(x >= 20); } } +// ==== +// SMTSolvers: z3 // ---- // Warning: (323-338): Assertion violation happens here // Warning: (362-377): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/operators/delete_array_index_2d.sol b/test/libsolidity/smtCheckerTests/operators/delete_array_index_2d.sol index 3e13c7f84..06ef66be9 100644 --- a/test/libsolidity/smtCheckerTests/operators/delete_array_index_2d.sol +++ b/test/libsolidity/smtCheckerTests/operators/delete_array_index_2d.sol @@ -13,3 +13,5 @@ contract C assert(a[1][1] == 0); } } +// ==== +// SMTSolvers: z3 diff --git a/test/libsolidity/smtCheckerTests/types/mapping_4.sol b/test/libsolidity/smtCheckerTests/types/mapping_4.sol index 7356a3b6b..fc098ba1b 100644 --- a/test/libsolidity/smtCheckerTests/types/mapping_4.sol +++ b/test/libsolidity/smtCheckerTests/types/mapping_4.sol @@ -8,4 +8,5 @@ contract C assert(x != map[x]); } } -// ---- +// ==== +// SMTSolvers: z3 From 9c3503834dd4d5560f08e50376ba8a1abef8ef6c Mon Sep 17 00:00:00 2001 From: chriseth Date: Mon, 9 Dec 2019 11:58:27 +0100 Subject: [PATCH 12/12] Fix semver matcher differently. --- Changelog.md | 2 +- liblangutil/SemVerHandler.cpp | 12 +----------- test/libsolidity/SemVerMatcher.cpp | 19 ++++++++++++++----- 3 files changed, 16 insertions(+), 17 deletions(-) diff --git a/Changelog.md b/Changelog.md index d491e6f72..0247137b3 100644 --- a/Changelog.md +++ b/Changelog.md @@ -18,7 +18,7 @@ Bugfixes: * SMTChecker: Fix internal error when using ``abi.decode``. * SMTChecker: Fix internal error when using arrays or mappings of functions. * SMTChecker: Fix internal error in array of structs type. - * Version Checker: 0.5.x-prerelease will match `pragma solidity ^0.5`. + * Version Checker: ``^0`` should match ``0.5.0``, but no prerelease. * Yul: Consider infinite loops and recursion to be not removable. diff --git a/liblangutil/SemVerHandler.cpp b/liblangutil/SemVerHandler.cpp index 611f058ae..cc414b1d7 100644 --- a/liblangutil/SemVerHandler.cpp +++ b/liblangutil/SemVerHandler.cpp @@ -88,7 +88,7 @@ bool SemVerMatchExpression::MatchComponent::matches(SemVerVersion const& _versio if (!comp.matches(_version)) return false; - if (comp.version.numbers[0] == 0) + if (comp.version.numbers[0] == 0 && comp.levelsPresent != 1) comp.levelsPresent = 2; else comp.levelsPresent = 1; @@ -107,17 +107,7 @@ bool SemVerMatchExpression::MatchComponent::matches(SemVerVersion const& _versio } if (cmp == 0 && !_version.prerelease.empty() && didCompare) - { cmp = -1; - for (unsigned i = levelsPresent; i < 3; i++) - { - if (_version.numbers[i] > 0) - { - cmp = 0; - break; - } - } - } switch (prefix) { diff --git a/test/libsolidity/SemVerMatcher.cpp b/test/libsolidity/SemVerMatcher.cpp index 7dae613a8..e0e643968 100644 --- a/test/libsolidity/SemVerMatcher.cpp +++ b/test/libsolidity/SemVerMatcher.cpp @@ -141,14 +141,14 @@ BOOST_AUTO_TEST_CASE(positive_range) {"^0.1.2", "0.1.2"}, {"^0.1", "0.1.2"}, {"^1.2", "1.4.2"}, - {"^1.2", "1.2.1-pre"}, {"^1.2", "1.2.0"}, - {"^1", "1.2.0-pre"}, {"^1", "1.2.0"}, {"<=1.2.3", "1.2.3-beta"}, {">1.2", "1.3.0-beta"}, {"<1.2.3", "1.2.3-beta"}, - {"^1.2 ^1", "1.4.2"} + {"^1.2 ^1", "1.4.2"}, + {"^0", "0.5.1"}, + {"^0", "0.1.1"}, }; for (auto const& t: tests) { @@ -163,13 +163,14 @@ BOOST_AUTO_TEST_CASE(positive_range) BOOST_AUTO_TEST_CASE(negative_range) { - // Positive range tests + // Negative range tests vector> tests = { {"1.0.0 - 2.0.0", "2.2.3"}, {"1.0", "1.0.0-pre"}, {"1", "1.0.0-pre"}, {"^1.2.3", "1.2.3-pre"}, {"^1.2", "1.2.0-pre"}, + {"^1.2", "1.2.1-pre"}, {"^1.2.3", "1.2.3-beta"}, {"=0.7.x", "0.7.0-asdf"}, {">=0.7.x", "0.7.0-asdf"}, @@ -212,8 +213,16 @@ BOOST_AUTO_TEST_CASE(negative_range) {"=1.2.3", "1.2.3-beta"}, {">1.2", "1.2.8"}, {"^1.2.3", "2.0.0-alpha"}, + {"^0.6", "0.6.2-alpha"}, + {"^0.6", "0.6.0-alpha"}, + {"^1.2", "1.2.1-pre"}, {"^1.2.3", "1.2.2"}, - {"^1.2", "1.1.9"} + {"^1", "1.2.0-pre"}, + {"^1", "1.2.0-pre"}, + {"^1.2", "1.1.9"}, + {"^0", "0.5.1-pre"}, + {"^0", "0.0.0-pre"}, + {"^0", "1.0.0"}, }; for (auto const& t: tests) {