From 69e4e69e69d3626ad417bf2e5d42024e8933b013 Mon Sep 17 00:00:00 2001 From: Chris Chinchilla Date: Thu, 30 May 2019 14:37:17 +0200 Subject: [PATCH 01/13] Bring value types code examples inline with style guide --- docs/types/value-types.rst | 156 ++++++++++++++++++++----------------- 1 file changed, 86 insertions(+), 70 deletions(-) diff --git a/docs/types/value-types.rst b/docs/types/value-types.rst index 9c082f9b4..2f1cfd185 100644 --- a/docs/types/value-types.rst +++ b/docs/types/value-types.rst @@ -624,100 +624,116 @@ Example that shows how to use the members:: pragma solidity >=0.4.16 <0.7.0; + contract Example { - function f() public payable returns (bytes4) { - return this.f.selector; - } - function g() public { - this.f.gas(10).value(800)(); - } + function f() public payable returns (bytes4) { + return this.f.selector; + } + + function g() public { + this.f.gas(10).value(800)(); + } } Example that shows how to use internal function types:: pragma solidity >=0.4.16 <0.7.0; + library ArrayUtils { - // internal functions can be used in internal library functions because - // they will be part of the same code context - function map(uint[] memory self, function (uint) pure returns (uint) f) - internal - pure - returns (uint[] memory r) - { - r = new uint[](self.length); - for (uint i = 0; i < self.length; i++) { - r[i] = f(self[i]); + // internal functions can be used in internal library functions because + // they will be part of the same code context + function map(uint[] memory self, function (uint) pure returns (uint) f) + internal + pure + returns (uint[] memory r) + { + r = new uint[](self.length); + for (uint i = 0; i < self.length; i++) { + r[i] = f(self[i]); + } } - } - function reduce( - uint[] memory self, - function (uint, uint) pure returns (uint) f - ) - internal - pure - returns (uint r) - { - r = self[0]; - for (uint i = 1; i < self.length; i++) { - r = f(r, self[i]); + + function reduce( + uint[] memory self, + function (uint, uint) pure returns (uint) f + ) + internal + pure + returns (uint r) + { + r = self[0]; + for (uint i = 1; i < self.length; i++) { + r = f(r, self[i]); + } } - } - function range(uint length) internal pure returns (uint[] memory r) { - r = new uint[](length); - for (uint i = 0; i < r.length; i++) { - r[i] = i; + + function range(uint length) internal pure returns (uint[] memory r) { + r = new uint[](length); + for (uint i = 0; i < r.length; i++) { + r[i] = i; + } } - } } + contract Pyramid { - using ArrayUtils for *; - function pyramid(uint l) public pure returns (uint) { - return ArrayUtils.range(l).map(square).reduce(sum); - } - function square(uint x) internal pure returns (uint) { - return x * x; - } - function sum(uint x, uint y) internal pure returns (uint) { - return x + y; - } + using ArrayUtils for *; + + function pyramid(uint l) public pure returns (uint) { + return ArrayUtils.range(l).map(square).reduce(sum); + } + + function square(uint x) internal pure returns (uint) { + return x * x; + } + + function sum(uint x, uint y) internal pure returns (uint) { + return x + y; + } } Another example that uses external function types:: pragma solidity >=0.4.22 <0.7.0; + contract Oracle { - struct Request { - bytes data; - function(uint) external callback; - } - Request[] requests; - event NewRequest(uint); - function query(bytes memory data, function(uint) external callback) public { - requests.push(Request(data, callback)); - emit NewRequest(requests.length - 1); - } - function reply(uint requestID, uint response) public { - // Here goes the check that the reply comes from a trusted source - requests[requestID].callback(response); - } + struct Request { + bytes data; + function(uint) external callback; + } + + Request[] private requests; + event NewRequest(uint); + + function query(bytes memory data, function(uint) external callback) public { + requests.push(Request(data, callback)); + emit NewRequest(requests.length - 1); + } + + function reply(uint requestID, uint response) public { + // Here goes the check that the reply comes from a trusted source + requests[requestID].callback(response); + } } + contract OracleUser { - Oracle constant oracle = Oracle(0x1234567); // known contract - uint exchangeRate; - function buySomething() public { - oracle.query("USD", this.oracleResponse); - } - function oracleResponse(uint response) public { - require( - msg.sender == address(oracle), - "Only oracle can call this." - ); - exchangeRate = response; - } + Oracle constant private ORACLE_CONST = Oracle(0x1234567); // known contract + uint private exchangeRate; + + function buySomething() public { + ORACLE_CONST.query("USD", this.oracleResponse); + } + + function oracleResponse(uint response) public { + require( + msg.sender == address(ORACLE_CONST), + "Only oracle can call this." + ); + exchangeRate = response; + } } .. note:: From d9ce9cab99d71c9c112eb2f7125e71d2e7b011af Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Tue, 4 Jun 2019 14:23:44 +0200 Subject: [PATCH 02/13] [SMTChecker] Use smtlib's implies instead of \!a or b --- libsolidity/formal/CVC4Interface.cpp | 2 ++ libsolidity/formal/SolverInterface.h | 8 +++++++- libsolidity/formal/Z3Interface.cpp | 2 ++ test/libsolidity/smtCheckerTestsJSON/multi.json | 4 ++-- 4 files changed, 13 insertions(+), 3 deletions(-) diff --git a/libsolidity/formal/CVC4Interface.cpp b/libsolidity/formal/CVC4Interface.cpp index 71f657471..b46d8ec38 100644 --- a/libsolidity/formal/CVC4Interface.cpp +++ b/libsolidity/formal/CVC4Interface.cpp @@ -145,6 +145,8 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr) return arguments[0].andExpr(arguments[1]); else if (n == "or") return arguments[0].orExpr(arguments[1]); + else if (n == "implies") + return m_context.mkExpr(CVC4::kind::IMPLIES, arguments[0], arguments[1]); else if (n == "=") return m_context.mkExpr(CVC4::kind::EQUAL, arguments[0], arguments[1]); else if (n == "<") diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h index 0c7f1dbdf..5610a5fd6 100644 --- a/libsolidity/formal/SolverInterface.h +++ b/libsolidity/formal/SolverInterface.h @@ -133,6 +133,7 @@ public: {"not", 1}, {"and", 2}, {"or", 2}, + {"implies", 2}, {"=", 2}, {"<", 2}, {"<=", 2}, @@ -160,7 +161,12 @@ public: static Expression implies(Expression _a, Expression _b) { - return !std::move(_a) || std::move(_b); + return Expression( + "implies", + std::move(_a), + std::move(_b), + Kind::Bool + ); } /// select is the SMT representation of an array index access. diff --git a/libsolidity/formal/Z3Interface.cpp b/libsolidity/formal/Z3Interface.cpp index 4d7ea8347..20c7452b5 100644 --- a/libsolidity/formal/Z3Interface.cpp +++ b/libsolidity/formal/Z3Interface.cpp @@ -144,6 +144,8 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr) return arguments[0] && arguments[1]; else if (n == "or") return arguments[0] || arguments[1]; + else if (n == "implies") + return z3::implies(arguments[0], arguments[1]); else if (n == "=") return arguments[0] == arguments[1]; else if (n == "<") diff --git a/test/libsolidity/smtCheckerTestsJSON/multi.json b/test/libsolidity/smtCheckerTestsJSON/multi.json index ba4cf2637..f892c28fe 100644 --- a/test/libsolidity/smtCheckerTestsJSON/multi.json +++ b/test/libsolidity/smtCheckerTestsJSON/multi.json @@ -3,8 +3,8 @@ { "smtlib2responses": { - "0x092d52dc5c2b54c1909592f7b3c8efedfd87afc0223ce421a24a1cc7905006b4": "sat\n((|EVALEXPR_0| 1))\n", - "0x8faacfc008b6f2278b5927ff22d76832956dfb46b3c21a64fab96583c241b88f": "unsat\n", + "0x0a0e9583fd983e7ce82e96bd95f7c0eb831e2dd3ce3364035e30bf1d22823b34": "sat\n((|EVALEXPR_0| 1))\n", + "0x15353582486fb1dac47801edbb366ae40a59ef0191ebe7c09ca32bdabecc2f1a": "unsat\n", "0xa66d08de30c873ca7d0e7e9e426f278640e0ee463a1aed2e4e80baee916b6869": "sat\n((|EVALEXPR_0| 0))\n" } } From 9f5340fa537267fb6759f91c4f9f79b69015ade4 Mon Sep 17 00:00:00 2001 From: Daniel Kirchner Date: Tue, 4 Jun 2019 14:55:45 +0200 Subject: [PATCH 03/13] Try to find Z3 using CONFIG_MODE before manual search. --- Changelog.md | 4 +++ cmake/FindZ3.cmake | 60 ++++++++++++++++++++++++-------------- libsolidity/CMakeLists.txt | 2 +- 3 files changed, 43 insertions(+), 23 deletions(-) diff --git a/Changelog.md b/Changelog.md index f89ac5187..c4c063dbe 100644 --- a/Changelog.md +++ b/Changelog.md @@ -11,6 +11,10 @@ Compiler Features: Bugfixes: +Build System: + * Attempt to use stock Z3 cmake files to find Z3 and only fall back to manual discovery. + + ### 0.5.9 (2019-05-28) diff --git a/cmake/FindZ3.cmake b/cmake/FindZ3.cmake index bdd8ce72f..4b63ed4cb 100644 --- a/cmake/FindZ3.cmake +++ b/cmake/FindZ3.cmake @@ -1,29 +1,45 @@ if (USE_Z3) - find_path(Z3_INCLUDE_DIR NAMES z3++.h PATH_SUFFIXES z3) - find_library(Z3_LIBRARY NAMES z3) - find_program(Z3_EXECUTABLE z3 PATH_SUFFIXES bin) - - if(Z3_INCLUDE_DIR AND Z3_LIBRARY AND Z3_EXECUTABLE) - execute_process (COMMAND ${Z3_EXECUTABLE} -version - OUTPUT_VARIABLE libz3_version_str - ERROR_QUIET - OUTPUT_STRIP_TRAILING_WHITESPACE) - - string(REGEX REPLACE "^Z3 version ([0-9.]+).*" "\\1" - Z3_VERSION_STRING "${libz3_version_str}") - unset(libz3_version_str) - endif() - mark_as_advanced(Z3_VERSION_STRING z3_DIR) + # Save and clear Z3_FIND_VERSION, since the + # Z3 config module cannot handle version requirements. + set(Z3_FIND_VERSION_ORIG ${Z3_FIND_VERSION}) + set(Z3_FIND_VERSION) + # Try to find Z3 using its stock cmake files. + find_package(Z3 QUIET CONFIG) + # Restore Z3_FIND_VERSION for find_package_handle_standard_args. + set(Z3_FIND_VERSION ${Z3_FIND_VERSION_ORIG}) + set(Z3_FIND_VERSION_ORIG) include(FindPackageHandleStandardArgs) - find_package_handle_standard_args(Z3 - REQUIRED_VARS Z3_LIBRARY Z3_INCLUDE_DIR - VERSION_VAR Z3_VERSION_STRING) - if (NOT TARGET Z3::Z3) - add_library(Z3::Z3 UNKNOWN IMPORTED) - set_property(TARGET Z3::Z3 PROPERTY IMPORTED_LOCATION ${Z3_LIBRARY}) - set_property(TARGET Z3::Z3 PROPERTY INTERFACE_INCLUDE_DIRECTORIES ${Z3_INCLUDE_DIR}) + if (Z3_FOUND) + set(Z3_VERSION ${Z3_VERSION_STRING}) + find_package_handle_standard_args(Z3 CONFIG_MODE) + else() + find_path(Z3_INCLUDE_DIR NAMES z3++.h PATH_SUFFIXES z3) + find_library(Z3_LIBRARY NAMES z3) + find_program(Z3_EXECUTABLE z3 PATH_SUFFIXES bin) + + if(Z3_INCLUDE_DIR AND Z3_LIBRARY AND Z3_EXECUTABLE) + execute_process (COMMAND ${Z3_EXECUTABLE} -version + OUTPUT_VARIABLE libz3_version_str + ERROR_QUIET + OUTPUT_STRIP_TRAILING_WHITESPACE) + + string(REGEX REPLACE "^Z3 version ([0-9.]+).*" "\\1" + Z3_VERSION_STRING "${libz3_version_str}") + unset(libz3_version_str) + endif() + mark_as_advanced(Z3_VERSION_STRING z3_DIR) + + find_package_handle_standard_args(Z3 + REQUIRED_VARS Z3_LIBRARY Z3_INCLUDE_DIR + VERSION_VAR Z3_VERSION_STRING) + + if (NOT TARGET z3::libz3) + add_library(z3::libz3 UNKNOWN IMPORTED) + set_property(TARGET z3::libz3 PROPERTY IMPORTED_LOCATION ${Z3_LIBRARY}) + set_property(TARGET z3::libz3 PROPERTY INTERFACE_INCLUDE_DIRECTORIES ${Z3_INCLUDE_DIR}) + endif() endif() else() set(Z3_FOUND FALSE) diff --git a/libsolidity/CMakeLists.txt b/libsolidity/CMakeLists.txt index 572038d22..fd9cd772a 100644 --- a/libsolidity/CMakeLists.txt +++ b/libsolidity/CMakeLists.txt @@ -140,7 +140,7 @@ add_library(solidity ${sources} ${z3_SRCS} ${cvc4_SRCS}) target_link_libraries(solidity PUBLIC yul evmasm langutil devcore ${Boost_FILESYSTEM_LIBRARY} ${Boost_SYSTEM_LIBRARY}) if (${Z3_FOUND}) - target_link_libraries(solidity PUBLIC Z3::Z3) + target_link_libraries(solidity PUBLIC z3::libz3) endif() if (${CVC4_FOUND}) From 31ef421fff1f2468165e2abc6c289f2888b7b7ec Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Tue, 4 Jun 2019 14:43:26 +0200 Subject: [PATCH 04/13] [SMTChecker] Keep a copy of assertions that are added to the solvers --- libsolidity/formal/SMTPortfolio.cpp | 16 ++++++++++++++++ libsolidity/formal/SMTPortfolio.h | 5 +++++ 2 files changed, 21 insertions(+) diff --git a/libsolidity/formal/SMTPortfolio.cpp b/libsolidity/formal/SMTPortfolio.cpp index 09a311f4f..ea2f3d9ee 100644 --- a/libsolidity/formal/SMTPortfolio.cpp +++ b/libsolidity/formal/SMTPortfolio.cpp @@ -43,18 +43,21 @@ SMTPortfolio::SMTPortfolio(map const& _smtlib2Responses) void SMTPortfolio::reset() { + m_assertions.clear(); for (auto const& s: m_solvers) s->reset(); } void SMTPortfolio::push() { + m_assertions.push_back(Expression(true)); for (auto const& s: m_solvers) s->push(); } void SMTPortfolio::pop() { + m_assertions.pop_back(); for (auto const& s: m_solvers) s->pop(); } @@ -67,10 +70,23 @@ void SMTPortfolio::declareVariable(string const& _name, Sort const& _sort) void SMTPortfolio::addAssertion(Expression const& _expr) { + if (m_assertions.empty()) + m_assertions.push_back(_expr); + else + m_assertions.back() = _expr && move(m_assertions.back()); + for (auto const& s: m_solvers) s->addAssertion(_expr); } +Expression SMTPortfolio::assertions() +{ + if (m_assertions.empty()) + return Expression(true); + + return m_assertions.back(); +} + /* * Broadcasts the SMT query to all solvers and returns a single result. * This comment explains how this result is decided. diff --git a/libsolidity/formal/SMTPortfolio.h b/libsolidity/formal/SMTPortfolio.h index ebe98261f..1f61ead8d 100644 --- a/libsolidity/formal/SMTPortfolio.h +++ b/libsolidity/formal/SMTPortfolio.h @@ -52,6 +52,9 @@ public: void declareVariable(std::string const&, Sort const&) override; void addAssertion(Expression const& _expr) override; + + Expression assertions(); + std::pair> check(std::vector const& _expressionsToEvaluate) override; std::vector unhandledQueries() override; @@ -60,6 +63,8 @@ private: static bool solverAnswered(CheckResult result); std::vector> m_solvers; + + std::vector m_assertions; }; } From 91653526bbcd77ee380cceeddd184d0b6becb981 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Tue, 4 Jun 2019 14:51:57 +0200 Subject: [PATCH 05/13] [SMTChecker] Use SMTPortfolio directly instead of pointer to SolverInterface --- libsolidity/formal/SMTChecker.cpp | 62 +++++++++++++++---------------- libsolidity/formal/SMTChecker.h | 10 +++-- 2 files changed, 38 insertions(+), 34 deletions(-) diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index dbd287876..2ececeeba 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -34,10 +34,10 @@ using namespace langutil; using namespace dev::solidity; SMTChecker::SMTChecker(ErrorReporter& _errorReporter, map const& _smtlib2Responses): - m_interface(make_unique(_smtlib2Responses)), + m_interface(_smtlib2Responses), m_errorReporterReference(_errorReporter), m_errorReporter(m_smtErrors), - m_context(*m_interface) + m_context(m_interface) { #if defined (HAVE_Z3) || defined (HAVE_CVC4) if (!_smtlib2Responses.empty()) @@ -56,11 +56,11 @@ void SMTChecker::analyze(SourceUnit const& _source, shared_ptr const& _ if (_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker)) _source.accept(*this); - solAssert(m_interface->solvers() > 0, ""); + solAssert(m_interface.solvers() > 0, ""); // If this check is true, Z3 and CVC4 are not available // and the query answers were not provided, since SMTPortfolio // guarantees that SmtLib2Interface is the first solver. - if (!m_interface->unhandledQueries().empty() && m_interface->solvers() == 1) + if (!m_interface.unhandledQueries().empty() && m_interface.solvers() == 1) { if (!m_noSolverWarning) { @@ -106,7 +106,7 @@ bool SMTChecker::visit(FunctionDefinition const& _function) // Not visited by a function call if (m_callStack.empty()) { - m_interface->reset(); + m_interface.reset(); m_context.reset(); m_pathConditions.clear(); m_callStack.clear(); @@ -302,13 +302,13 @@ bool SMTChecker::visit(ForStatement const& _node) checkBooleanNotConstant(*_node.condition(), "For loop condition is always $VALUE."); } - m_interface->push(); + m_interface.push(); if (_node.condition()) - m_interface->addAssertion(expr(*_node.condition())); + m_interface.addAssertion(expr(*_node.condition())); _node.body().accept(*this); if (_node.loopExpression()) _node.loopExpression()->accept(*this); - m_interface->pop(); + m_interface.pop(); auto indicesAfterLoop = copyVariableIndices(); // We reset the execution to before the loop @@ -693,7 +693,7 @@ void SMTChecker::endVisit(FunctionCall const& _funCall) solAssert(value, ""); smt::Expression thisBalance = m_context.balance(); - setSymbolicUnknownValue(thisBalance, TypeProvider::uint256(), *m_interface); + setSymbolicUnknownValue(thisBalance, TypeProvider::uint256(), m_interface); checkCondition(thisBalance < expr(*value), _funCall.location(), "Insufficient funds", "address(this).balance", &thisBalance); m_context.transfer(m_context.thisAddress(), expr(address), expr(*value)); @@ -737,7 +737,7 @@ void SMTChecker::visitGasLeft(FunctionCall const& _funCall) // We set the current value to unknown anyway to add type constraints. m_context.setUnknownValue(*symbolicVar); if (index > 0) - m_interface->addAssertion(symbolicVar->currentValue() <= symbolicVar->valueAtIndex(index - 1)); + m_interface.addAssertion(symbolicVar->currentValue() <= symbolicVar->valueAtIndex(index - 1)); } void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall) @@ -819,7 +819,7 @@ void SMTChecker::abstractFunctionCall(FunctionCall const& _funCall) smtArguments.push_back(expr(*arg)); defineExpr(_funCall, (*m_context.expression(_funCall.expression()))(smtArguments)); m_uninterpretedTerms.insert(&_funCall); - setSymbolicUnknownValue(expr(_funCall), _funCall.annotation().type, *m_interface); + setSymbolicUnknownValue(expr(_funCall), _funCall.annotation().type, m_interface); } void SMTChecker::endVisit(Identifier const& _identifier) @@ -911,7 +911,7 @@ void SMTChecker::endVisit(Literal const& _literal) auto stringType = TypeProvider::stringMemory(); auto stringLit = dynamic_cast(_literal.annotation().type); solAssert(stringLit, ""); - auto result = smt::newSymbolicVariable(*stringType, stringLit->richIdentifier(), *m_interface); + auto result = smt::newSymbolicVariable(*stringType, stringLit->richIdentifier(), m_interface); m_context.createExpression(_literal, result.second); } m_errorReporter.warning( @@ -936,10 +936,10 @@ void SMTChecker::endVisit(Return const& _return) solAssert(components.size() == returnParams.size(), ""); for (unsigned i = 0; i < returnParams.size(); ++i) if (components.at(i)) - m_interface->addAssertion(expr(*components.at(i)) == m_context.newValue(*returnParams.at(i))); + m_interface.addAssertion(expr(*components.at(i)) == m_context.newValue(*returnParams.at(i))); } else if (returnParams.size() == 1) - m_interface->addAssertion(expr(*_return.expression()) == m_context.newValue(*returnParams.front())); + m_interface.addAssertion(expr(*_return.expression()) == m_context.newValue(*returnParams.front())); } } @@ -981,7 +981,7 @@ bool SMTChecker::visit(MemberAccess const& _memberAccess) if (_memberAccess.memberName() == "balance") { defineExpr(_memberAccess, m_context.balance(expr(_memberAccess.expression()))); - setSymbolicUnknownValue(*m_context.expression(_memberAccess), *m_interface); + setSymbolicUnknownValue(*m_context.expression(_memberAccess), m_interface); m_uninterpretedTerms.insert(&_memberAccess); return false; } @@ -1028,7 +1028,7 @@ void SMTChecker::endVisit(IndexAccess const& _indexAccess) setSymbolicUnknownValue( expr(_indexAccess), _indexAccess.annotation().type, - *m_interface + m_interface ); m_uninterpretedTerms.insert(&_indexAccess); } @@ -1080,7 +1080,7 @@ void SMTChecker::arrayIndexAssignment(Expression const& _expr, smt::Expression c expr(*indexAccess.indexExpression()), _rightHandSide ); - m_interface->addAssertion(m_context.newValue(*varDecl) == store); + m_interface.addAssertion(m_context.newValue(*varDecl) == store); // Update the SMT select value after the assignment, // necessary for sound models. defineExpr(indexAccess, smt::Expression::select( @@ -1211,7 +1211,7 @@ smt::Expression SMTChecker::arithmeticOperation( if (_op == Token::Div || _op == Token::Mod) { checkCondition(_right == 0, _location, "Division by zero", "", &_right); - m_interface->addAssertion(_right != 0); + m_interface.addAssertion(_right != 0); } addOverflowTarget( @@ -1393,7 +1393,7 @@ void SMTChecker::assignment(VariableDeclaration const& _variable, smt::Expressio addOverflowTarget(OverflowTarget::Type::All, TypeProvider::uint(160), _value, _location); else if (type->category() == Type::Category::Mapping) arrayAssignment(); - m_interface->addAssertion(m_context.newValue(_variable) == _value); + m_interface.addAssertion(m_context.newValue(_variable) == _value); } SMTChecker::VariableIndices SMTChecker::visitBranch(ASTNode const* _statement, smt::Expression _condition) @@ -1422,7 +1422,7 @@ void SMTChecker::checkCondition( smt::Expression const* _additionalValue ) { - m_interface->push(); + m_interface.push(); addPathConjoinedExpression(_condition); vector expressionsToEvaluate; @@ -1534,7 +1534,7 @@ void SMTChecker::checkCondition( m_errorReporter.warning(_location, "Error trying to invoke SMT solver."); break; } - m_interface->pop(); + m_interface.pop(); } void SMTChecker::checkBooleanNotConstant(Expression const& _condition, string const& _description) @@ -1543,15 +1543,15 @@ void SMTChecker::checkBooleanNotConstant(Expression const& _condition, string co if (dynamic_cast(&_condition)) return; - m_interface->push(); + m_interface.push(); addPathConjoinedExpression(expr(_condition)); auto positiveResult = checkSatisfiable(); - m_interface->pop(); + m_interface.pop(); - m_interface->push(); + m_interface.push(); addPathConjoinedExpression(!expr(_condition)); auto negatedResult = checkSatisfiable(); - m_interface->pop(); + m_interface.pop(); if (positiveResult == smt::CheckResult::ERROR || negatedResult == smt::CheckResult::ERROR) m_errorReporter.warning(_condition.location(), "Error trying to invoke SMT solver."); @@ -1596,7 +1596,7 @@ SMTChecker::checkSatisfiableAndGenerateModel(vector const& _exp vector values; try { - tie(result, values) = m_interface->check(_expressionsToEvaluate); + tie(result, values) = m_interface.check(_expressionsToEvaluate); } catch (smt::SolverError const& _e) { @@ -1632,7 +1632,7 @@ void SMTChecker::initializeFunctionCallParameters(CallableDeclaration const& _fu for (unsigned i = 0; i < funParams.size(); ++i) if (createVariable(*funParams[i])) { - m_interface->addAssertion(_callArgs[i] == m_context.newValue(*funParams[i])); + m_interface.addAssertion(_callArgs[i] == m_context.newValue(*funParams[i])); if (funParams[i]->annotation().type->category() == Type::Category::Mapping) m_arrayAssignmentHappened = true; } @@ -1698,7 +1698,7 @@ void SMTChecker::mergeVariables(set const& _variable int trueIndex = _indicesEndTrue.at(decl); int falseIndex = _indicesEndFalse.at(decl); solAssert(trueIndex != falseIndex, ""); - m_interface->addAssertion(m_context.newValue(*decl) == smt::Expression::ite( + m_interface.addAssertion(m_context.newValue(*decl) == smt::Expression::ite( _condition, valueAtIndex(*decl, trueIndex), valueAtIndex(*decl, falseIndex)) @@ -1758,7 +1758,7 @@ void SMTChecker::defineExpr(Expression const& _e, smt::Expression _value) { createExpr(_e); solAssert(smt::smtKind(_e.annotation().type->category()) != smt::Kind::Function, "Equality operator applied to type that is not fully supported"); - m_interface->addAssertion(expr(_e) == _value); + m_interface.addAssertion(expr(_e) == _value); } void SMTChecker::popPathCondition() @@ -1807,12 +1807,12 @@ void SMTChecker::pushCallStack(CallStackEntry _entry) void SMTChecker::addPathConjoinedExpression(smt::Expression const& _e) { - m_interface->addAssertion(currentPathConditions() && _e); + m_interface.addAssertion(currentPathConditions() && _e); } void SMTChecker::addPathImpliedExpression(smt::Expression const& _e) { - m_interface->addAssertion(smt::Expression::implies(currentPathConditions(), _e)); + m_interface.addAssertion(smt::Expression::implies(currentPathConditions(), _e)); } bool SMTChecker::isRootFunction() diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index 54254c3a6..661dff342 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -19,7 +19,7 @@ #include -#include +#include #include #include @@ -53,7 +53,7 @@ public: /// This is used if the SMT solver is not directly linked into this binary. /// @returns a list of inputs to the SMT solver that were not part of the argument to /// the constructor. - std::vector unhandledQueries() { return m_interface->unhandledQueries(); } + std::vector unhandledQueries() { return m_interface.unhandledQueries(); } /// @returns the FunctionDefinition of a called function if possible and should inline, /// otherwise nullptr. @@ -91,6 +91,10 @@ private: void endVisit(IndexAccess const& _node) override; bool visit(InlineAssembly const& _node) override; + smt::Expression assertions() { return m_interface.assertions(); } + void push() { m_interface.push(); } + void pop() { m_interface.pop(); } + /// Do not visit subtree if node is a RationalNumber. /// Symbolic _expr is the rational literal. bool shortcutRationalNumber(Expression const& _expr); @@ -270,7 +274,7 @@ private: /// @returns the VariableDeclaration referenced by an Identifier or nullptr. VariableDeclaration const* identifierToVariable(Expression const& _expr); - std::unique_ptr m_interface; + smt::SMTPortfolio m_interface; smt::VariableUsage m_variableUsage; bool m_loopExecutionHappened = false; bool m_arrayAssignmentHappened = false; From 4de1e20954bab153e07005403b94198bbc06c9d9 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Tue, 4 Jun 2019 14:54:06 +0200 Subject: [PATCH 06/13] [SMTChecker] Exit early if no pragma --- libsolidity/formal/SMTChecker.cpp | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index dbd287876..6bd973e19 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -52,9 +52,12 @@ SMTChecker::SMTChecker(ErrorReporter& _errorReporter, map const& _ void SMTChecker::analyze(SourceUnit const& _source, shared_ptr const& _scanner) { + if (!_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker)) + return; + m_scanner = _scanner; - if (_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker)) - _source.accept(*this); + + _source.accept(*this); solAssert(m_interface->solvers() > 0, ""); // If this check is true, Z3 and CVC4 are not available From f281c94b42564d6ac7f52909cc6640bca41b1f3a Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Tue, 4 Jun 2019 14:29:35 +0200 Subject: [PATCH 07/13] [SMTChecker] Test that non-Boolean literals are actually integers --- libsolidity/formal/CVC4Interface.cpp | 10 ++++++++-- libsolidity/formal/Z3Interface.cpp | 10 ++++++++-- 2 files changed, 16 insertions(+), 4 deletions(-) diff --git a/libsolidity/formal/CVC4Interface.cpp b/libsolidity/formal/CVC4Interface.cpp index b46d8ec38..217aa816f 100644 --- a/libsolidity/formal/CVC4Interface.cpp +++ b/libsolidity/formal/CVC4Interface.cpp @@ -132,8 +132,14 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr) else if (n == "false") return m_context.mkConst(false); else - // We assume it is an integer... - return m_context.mkConst(CVC4::Rational(n)); + try + { + return m_context.mkConst(CVC4::Rational(n)); + } + catch (...) + { + solAssert(false, ""); + } } solAssert(_expr.hasCorrectArity(), ""); diff --git a/libsolidity/formal/Z3Interface.cpp b/libsolidity/formal/Z3Interface.cpp index 20c7452b5..fdb04956e 100644 --- a/libsolidity/formal/Z3Interface.cpp +++ b/libsolidity/formal/Z3Interface.cpp @@ -131,8 +131,14 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr) else if (n == "false") return m_context.bool_val(false); else - // We assume it is an integer... - return m_context.int_val(n.c_str()); + try + { + return m_context.int_val(n.c_str()); + } + catch (...) + { + solAssert(false, ""); + } } solAssert(_expr.hasCorrectArity(), ""); From 5677bedf3483046c91d5fd29d4aa61b1de183f8c Mon Sep 17 00:00:00 2001 From: Daniel Kirchner Date: Wed, 5 Jun 2019 11:55:26 +0200 Subject: [PATCH 08/13] Require gcc >= 5.0. --- Changelog.md | 1 + cmake/EthCompilerSettings.cmake | 6 +++--- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/Changelog.md b/Changelog.md index c4c063dbe..37da04f32 100644 --- a/Changelog.md +++ b/Changelog.md @@ -13,6 +13,7 @@ Bugfixes: Build System: * Attempt to use stock Z3 cmake files to find Z3 and only fall back to manual discovery. + * Generate a cmake error for gcc versions older than 5.0. diff --git a/cmake/EthCompilerSettings.cmake b/cmake/EthCompilerSettings.cmake index 3fe98188d..7ffb45964 100644 --- a/cmake/EthCompilerSettings.cmake +++ b/cmake/EthCompilerSettings.cmake @@ -41,11 +41,11 @@ if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU") OR ("${CMAKE_CXX_COMPILER_ID}" MA # Additional GCC-specific compiler settings. if ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU") - # Check that we've got GCC 4.7 or newer. + # Check that we've got GCC 5.0 or newer. execute_process( COMMAND ${CMAKE_CXX_COMPILER} -dumpversion OUTPUT_VARIABLE GCC_VERSION) - if (NOT (GCC_VERSION VERSION_GREATER 4.7 OR GCC_VERSION VERSION_EQUAL 4.7)) - message(FATAL_ERROR "${PROJECT_NAME} requires g++ 4.7 or greater.") + if (NOT (GCC_VERSION VERSION_GREATER 5.0 OR GCC_VERSION VERSION_EQUAL 5.0)) + message(FATAL_ERROR "${PROJECT_NAME} requires g++ 5.0 or greater.") endif () # Additional Clang-specific compiler settings. From b80cc42a7cacaf1ebf6d9a1f7692ac002631cf05 Mon Sep 17 00:00:00 2001 From: Christian Parpart Date: Mon, 3 Jun 2019 16:54:03 +0200 Subject: [PATCH 09/13] yul: AsmPrinter fix when appending type name but no type-name is available. --- libyul/AsmPrinter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/libyul/AsmPrinter.cpp b/libyul/AsmPrinter.cpp index a3d9eafc3..71151a0cf 100644 --- a/libyul/AsmPrinter.cpp +++ b/libyul/AsmPrinter.cpp @@ -266,7 +266,7 @@ string AsmPrinter::formatTypedName(TypedName _variable) const string AsmPrinter::appendTypeName(YulString _type) const { - if (m_yul) + if (m_yul && !_type.empty()) return ":" + _type.str(); return ""; } From f99d78117e80c57335c7f8bff373e39d6b719b6e Mon Sep 17 00:00:00 2001 From: Chris Chinchilla Date: Thu, 30 May 2019 14:34:52 +0200 Subject: [PATCH 10/13] Bring code examples for Style Guide inline with style guide Add back accidentally removed public --- docs/style-guide.rst | 75 ++++++++++++++++++++++++++------------------ 1 file changed, 45 insertions(+), 30 deletions(-) diff --git a/docs/style-guide.rst b/docs/style-guide.rst index 10cbffb67..fb38f2d93 100644 --- a/docs/style-guide.rst +++ b/docs/style-guide.rst @@ -757,20 +757,26 @@ No:: pragma solidity >=0.4.0 <0.7.0; + // Base contracts just to make this compile contract B { constructor(uint) public { } } + + contract C { constructor(uint, uint) public { } } + + contract D { constructor(uint) public { } } + contract A is B, C, D { uint x; @@ -778,12 +784,12 @@ No:: B(param1) C(param2, param3) D(param4) - public - { + public { x = param5; } } + contract X is B, C, D { uint x; @@ -792,10 +798,11 @@ No:: C(param2, param3) D(param4) public { - x = param5; - } + x = param5; + } } + When declaring short functions with a single statement, it is permissible to do it on a single line. Permissible:: @@ -973,27 +980,32 @@ Yes:: pragma solidity >=0.4.0 <0.7.0; + // Owned.sol contract Owned { - address public owner; + address public owner; - constructor() public { - owner = msg.sender; - } + constructor() public { + owner = msg.sender; + } - modifier onlyOwner { - require(msg.sender == owner); - _; - } + modifier onlyOwner { + require(msg.sender == owner); + _; + } - function transferOwnership(address newOwner) public onlyOwner { - owner = newOwner; - } + function transferOwnership(address newOwner) public onlyOwner { + owner = newOwner; + } } - // Congress.sol +and in ``Congress.sol``:: + + pragma solidity >=0.4.0 <0.7.0; + import "./Owned.sol"; + contract Congress is Owned, TokenRecipient { //... } @@ -1002,32 +1014,34 @@ No:: pragma solidity >=0.4.0 <0.7.0; + // owned.sol contract owned { - address public owner; + address public owner; - constructor() public { - owner = msg.sender; - } + constructor() public { + owner = msg.sender; + } - modifier onlyOwner { - require(msg.sender == owner); - _; - } + modifier onlyOwner { + require(msg.sender == owner); + _; + } - function transferOwnership(address newOwner) public onlyOwner { - owner = newOwner; - } + function transferOwnership(address newOwner) public onlyOwner { + owner = newOwner; + } } - // Congress.sol +and in ``Congress.sol``:: + import "./owned.sol"; + contract Congress is owned, tokenRecipient { //... } - Struct Names ========================== @@ -1104,6 +1118,7 @@ added looks like the one below:: pragma solidity >=0.4.0 <0.7.0; + /// @author The Solidity Team /// @title A simple storage example contract SimpleStorage { @@ -1126,4 +1141,4 @@ added looks like the one below:: It is recommended that Solidity contracts are fully annontated using `NatSpec `_ for all public interfaces (everything in the ABI). -Please see the section about `NatSpec `_ for a detailed explanation. +Please see the section about `NatSpec `_ for a detailed explanation. \ No newline at end of file From 6368cd4c82f00a26b93e1799b80c53bc9b033e58 Mon Sep 17 00:00:00 2001 From: Daniel Kirchner Date: Thu, 6 Jun 2019 13:16:27 +0200 Subject: [PATCH 11/13] AsmParser: disallow trailing commas in function call arguments. --- Changelog.md | 1 + libyul/AsmParser.cpp | 10 ++++++---- ...{empty_fun_arg.sol => empty_fun_arg_beginning.sol} | 3 +-- .../inlineAssembly/invalid/empty_fun_arg_end.sol | 11 +++++++++++ .../inlineAssembly/invalid/empty_fun_arg_middle.sol | 10 ++++++++++ 5 files changed, 29 insertions(+), 6 deletions(-) rename test/libsolidity/syntaxTests/inlineAssembly/invalid/{empty_fun_arg.sol => empty_fun_arg_beginning.sol} (63%) create mode 100644 test/libsolidity/syntaxTests/inlineAssembly/invalid/empty_fun_arg_end.sol create mode 100644 test/libsolidity/syntaxTests/inlineAssembly/invalid/empty_fun_arg_middle.sol diff --git a/Changelog.md b/Changelog.md index 37da04f32..c26815ad8 100644 --- a/Changelog.md +++ b/Changelog.md @@ -9,6 +9,7 @@ Compiler Features: Bugfixes: + * Yul / Inline Assembly Parser: Disallow trailing commas in function call arguments. Build System: diff --git a/libyul/AsmParser.cpp b/libyul/AsmParser.cpp index 3f29f6fa5..9686e7dde 100644 --- a/libyul/AsmParser.cpp +++ b/libyul/AsmParser.cpp @@ -609,12 +609,14 @@ Expression Parser::parseCall(Parser::ElementaryOperation&& _initialOp) else ret = std::move(boost::get(_initialOp)); expectToken(Token::LParen); - while (currentToken() != Token::RParen) + if (currentToken() != Token::RParen) { ret.arguments.emplace_back(parseExpression()); - if (currentToken() == Token::RParen) - break; - expectToken(Token::Comma); + while (currentToken() != Token::RParen) + { + expectToken(Token::Comma); + ret.arguments.emplace_back(parseExpression()); + } } ret.location.end = endPosition(); expectToken(Token::RParen); diff --git a/test/libsolidity/syntaxTests/inlineAssembly/invalid/empty_fun_arg.sol b/test/libsolidity/syntaxTests/inlineAssembly/invalid/empty_fun_arg_beginning.sol similarity index 63% rename from test/libsolidity/syntaxTests/inlineAssembly/invalid/empty_fun_arg.sol rename to test/libsolidity/syntaxTests/inlineAssembly/invalid/empty_fun_arg_beginning.sol index 9acac7a64..9d99c8b4d 100644 --- a/test/libsolidity/syntaxTests/inlineAssembly/invalid/empty_fun_arg.sol +++ b/test/libsolidity/syntaxTests/inlineAssembly/invalid/empty_fun_arg_beginning.sol @@ -3,10 +3,9 @@ contract C { assembly { function f(a, b) {} f() - f(1,) f(,1) } } } // ---- -// ParserError: (113-114): Literal, identifier or instruction expected. +// ParserError: (101-102): Literal, identifier or instruction expected. diff --git a/test/libsolidity/syntaxTests/inlineAssembly/invalid/empty_fun_arg_end.sol b/test/libsolidity/syntaxTests/inlineAssembly/invalid/empty_fun_arg_end.sol new file mode 100644 index 000000000..0d041492d --- /dev/null +++ b/test/libsolidity/syntaxTests/inlineAssembly/invalid/empty_fun_arg_end.sol @@ -0,0 +1,11 @@ +contract C { + function f() public pure { + assembly { + function f(a, b) {} + f() + f(1,) + } + } +} +// ---- +// ParserError: (103-104): Literal, identifier or instruction expected. diff --git a/test/libsolidity/syntaxTests/inlineAssembly/invalid/empty_fun_arg_middle.sol b/test/libsolidity/syntaxTests/inlineAssembly/invalid/empty_fun_arg_middle.sol new file mode 100644 index 000000000..09e0ba038 --- /dev/null +++ b/test/libsolidity/syntaxTests/inlineAssembly/invalid/empty_fun_arg_middle.sol @@ -0,0 +1,10 @@ +contract C { + function f() public pure { + assembly { + function f(a, b, c) {} + f(1,,1) + } + } +} +// ---- +// ParserError: (96-97): Literal, identifier or instruction expected. From 2dbdddc7e5ded27b5bcdd9d6bb66367e3ff8c67b Mon Sep 17 00:00:00 2001 From: Daniel Kirchner Date: Thu, 6 Jun 2019 13:17:08 +0200 Subject: [PATCH 12/13] Fix argument count for require with message and string literals. --- libsolidity/codegen/ir/IRGeneratorForStatements.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/libsolidity/codegen/ir/IRGeneratorForStatements.cpp b/libsolidity/codegen/ir/IRGeneratorForStatements.cpp index d5975b717..e9adf36a2 100644 --- a/libsolidity/codegen/ir/IRGeneratorForStatements.cpp +++ b/libsolidity/codegen/ir/IRGeneratorForStatements.cpp @@ -550,13 +550,14 @@ void IRGeneratorForStatements::endVisit(FunctionCall const& _functionCall) solAssert(arguments.size() > 0, "Expected at least one parameter for require/assert"); solAssert(arguments.size() <= 2, "Expected no more than two parameters for require/assert"); + Type const* messageArgumentType = arguments.size() > 1 ? arguments[1]->annotation().type : nullptr; string requireOrAssertFunction = m_utils.requireOrAssertFunction( functionType->kind() == FunctionType::Kind::Assert, - arguments.size() > 1 ? arguments[1]->annotation().type : nullptr + messageArgumentType ); m_code << move(requireOrAssertFunction) << "(" << m_context.variable(*arguments[0]); - if (arguments.size() > 1) + if (messageArgumentType && messageArgumentType->sizeOnStack() > 0) m_code << ", " << m_context.variable(*arguments[1]); m_code << ")\n"; From 8e20a5e59acc0541cc755f1609e45021b46fb416 Mon Sep 17 00:00:00 2001 From: Daniel Kirchner Date: Thu, 6 Jun 2019 18:02:48 +0200 Subject: [PATCH 13/13] Allow extracted semantics tests to run both with and without Yul. --- test/libsolidity/SemanticTest.cpp | 136 ++++++++++++++++++------------ test/libsolidity/SemanticTest.h | 2 + 2 files changed, 83 insertions(+), 55 deletions(-) diff --git a/test/libsolidity/SemanticTest.cpp b/test/libsolidity/SemanticTest.cpp index f7d08e67c..adc3e0650 100644 --- a/test/libsolidity/SemanticTest.cpp +++ b/test/libsolidity/SemanticTest.cpp @@ -46,8 +46,18 @@ SemanticTest::SemanticTest(string const& _filename, string const& _ipcPath, lang m_source = parseSourceAndSettings(file); if (m_settings.count("compileViaYul")) { - m_validatedSettings["compileViaYul"] = m_settings["compileViaYul"]; - m_compileViaYul = true; + if (m_settings["compileViaYul"] == "also") + { + m_validatedSettings["compileViaYul"] = m_settings["compileViaYul"]; + m_runWithYul = true; + m_runWithoutYul = true; + } + else + { + m_validatedSettings["compileViaYul"] = "only"; + m_runWithYul = true; + m_runWithoutYul = false; + } m_settings.erase("compileViaYul"); } parseExpectations(file); @@ -55,68 +65,84 @@ SemanticTest::SemanticTest(string const& _filename, string const& _ipcPath, lang TestCase::TestResult SemanticTest::run(ostream& _stream, string const& _linePrefix, bool _formatted) { - - - bool success = true; - for (auto& test: m_tests) - test.reset(); - - for (auto& test: m_tests) + for(bool compileViaYul: set{!m_runWithoutYul, m_runWithYul}) { - if (&test == &m_tests.front()) - if (test.call().isConstructor) - deploy("", 0, test.call().arguments.rawBytes()); + bool success = true; + + m_compileViaYul = compileViaYul; + if (compileViaYul) + AnsiColorized(_stream, _formatted, {BOLD, CYAN}) << _linePrefix << "Running via Yul:" << endl; + + for (auto& test: m_tests) + test.reset(); + + for (auto& test: m_tests) + { + if (&test == &m_tests.front()) + if (test.call().isConstructor) + deploy("", 0, test.call().arguments.rawBytes()); + else + soltestAssert(deploy("", 0, bytes()), "Failed to deploy contract."); else - soltestAssert(deploy("", 0, bytes()), "Failed to deploy contract."); - else - soltestAssert(!test.call().isConstructor, "Constructor has to be the first function call."); + soltestAssert(!test.call().isConstructor, "Constructor has to be the first function call."); - if (test.call().isConstructor) - { - if (m_transactionSuccessful == test.call().expectations.failure) - success = false; + if (test.call().isConstructor) + { + if (m_transactionSuccessful == test.call().expectations.failure) + success = false; - test.setFailure(!m_transactionSuccessful); - test.setRawBytes(bytes()); + test.setFailure(!m_transactionSuccessful); + test.setRawBytes(bytes()); + } + else + { + bytes output = callContractFunctionWithValueNoEncoding( + test.call().signature, + test.call().value, + test.call().arguments.rawBytes() + ); + + if ((m_transactionSuccessful == test.call().expectations.failure) || (output != test.call().expectations.rawBytes())) + success = false; + + test.setFailure(!m_transactionSuccessful); + test.setRawBytes(std::move(output)); + test.setContractABI(m_compiler.contractABI(m_compiler.lastContractName())); + } } - else + + if (!success) { - bytes output = callContractFunctionWithValueNoEncoding( - test.call().signature, - test.call().value, - test.call().arguments.rawBytes() - ); - - if ((m_transactionSuccessful == test.call().expectations.failure) || (output != test.call().expectations.rawBytes())) - success = false; - - test.setFailure(!m_transactionSuccessful); - test.setRawBytes(std::move(output)); - test.setContractABI(m_compiler.contractABI(m_compiler.lastContractName())); + AnsiColorized(_stream, _formatted, {BOLD, CYAN}) << _linePrefix << "Expected result:" << endl; + for (auto const& test: m_tests) + { + ErrorReporter errorReporter; + _stream << test.format(errorReporter, _linePrefix, false, _formatted) << endl; + _stream << errorReporter.format(_linePrefix, _formatted); + } + _stream << endl; + AnsiColorized(_stream, _formatted, {BOLD, CYAN}) << _linePrefix << "Obtained result:" << endl; + for (auto const& test: m_tests) + { + ErrorReporter errorReporter; + _stream << test.format(errorReporter, _linePrefix, true, _formatted) << endl; + _stream << errorReporter.format(_linePrefix, _formatted); + } + AnsiColorized(_stream, _formatted, {BOLD, RED}) << _linePrefix << endl << _linePrefix + << "Attention: Updates on the test will apply the detected format displayed." << endl; + if (compileViaYul && m_runWithoutYul) + { + _stream << _linePrefix << endl << _linePrefix; + AnsiColorized(_stream, _formatted, {RED_BACKGROUND}) << "Note that the test passed without Yul."; + _stream << endl; + } + else if (!compileViaYul && m_runWithYul) + AnsiColorized(_stream, _formatted, {BOLD, YELLOW}) << _linePrefix << endl << _linePrefix + << "Note that the test also has to pass via Yul." << endl; + return TestResult::Failure; } } - if (!success) - { - AnsiColorized(_stream, _formatted, {BOLD, CYAN}) << _linePrefix << "Expected result:" << endl; - for (auto const& test: m_tests) - { - ErrorReporter errorReporter; - _stream << test.format(errorReporter, _linePrefix, false, _formatted) << endl; - _stream << errorReporter.format(_linePrefix, _formatted); - } - _stream << endl; - AnsiColorized(_stream, _formatted, {BOLD, CYAN}) << _linePrefix << "Obtained result:" << endl; - for (auto const& test: m_tests) - { - ErrorReporter errorReporter; - _stream << test.format(errorReporter, _linePrefix, true, _formatted) << endl; - _stream << errorReporter.format(_linePrefix, _formatted); - } - AnsiColorized(_stream, _formatted, {BOLD, RED}) << _linePrefix << endl << _linePrefix - << "Attention: Updates on the test will apply the detected format displayed." << endl; - return TestResult::Failure; - } return TestResult::Success; } diff --git a/test/libsolidity/SemanticTest.h b/test/libsolidity/SemanticTest.h index 019ca4b9f..ac9fb7dba 100644 --- a/test/libsolidity/SemanticTest.h +++ b/test/libsolidity/SemanticTest.h @@ -65,6 +65,8 @@ public: private: std::string m_source; std::vector m_tests; + bool m_runWithYul = false; + bool m_runWithoutYul = true; }; }