diff options
| -rw-r--r-- | CMakeLists.txt | 2 | ||||
| -rw-r--r-- | Changelog.md | 1 | ||||
| -rw-r--r-- | cmake/EthCompilerSettings.cmake | 5 | ||||
| -rw-r--r-- | libsolidity/formal/SMTChecker.cpp | 44 | ||||
| -rw-r--r-- | libsolidity/formal/SMTChecker.h | 4 | ||||
| -rw-r--r-- | libsolidity/formal/VariableUsage.cpp | 1 | ||||
| -rw-r--r-- | test/libsolidity/SMTChecker.cpp | 76 |
7 files changed, 125 insertions, 8 deletions
diff --git a/CMakeLists.txt b/CMakeLists.txt index 4ac56b43..0c05208f 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -21,7 +21,7 @@ include(EthCcache) # Let's find our dependencies include(EthDependencies) include(jsoncpp) -include_directories(${JSONCPP_INCLUDE_DIR}) +include_directories(SYSTEM ${JSONCPP_INCLUDE_DIR}) find_package(Threads) diff --git a/Changelog.md b/Changelog.md index dcf16191..d6f54070 100644 --- a/Changelog.md +++ b/Changelog.md @@ -10,6 +10,7 @@ Features: * Optimizer: Remove unnecessary masking of the result of known short instructions (``ADDRESS``, ``CALLER``, ``ORIGIN`` and ``COINBASE``). * Parser: Display nicer error messages by showing the actual tokens and not internal names. * Parser: Use the entire location of the token instead of only its starting position as source location for parser errors. + * SMT Checker: Support state variables of integer and bool type. * Type Checker: Deprecate the ``years`` unit denomination and raise a warning for it (or an error as experimental 0.5.0 feature). * Type Checker: Make literals (without explicit type casting) an error for tight packing as experimental 0.5.0 feature. * Type Checker: Warn about wildcard tuple assignments (this will turn into an error with version 0.5.0). diff --git a/cmake/EthCompilerSettings.cmake b/cmake/EthCompilerSettings.cmake index c73536ad..683d1d2e 100644 --- a/cmake/EthCompilerSettings.cmake +++ b/cmake/EthCompilerSettings.cmake @@ -62,8 +62,9 @@ if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU") OR ("${CMAKE_CXX_COMPILER_ID}" MA # Additional Clang-specific compiler settings. elseif ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") if ("${CMAKE_SYSTEM_NAME}" MATCHES "Darwin") - # Set stack size to 16MB - by default Apple's clang defines a stack size of 8MB, some tests require more. - set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -Wl,-stack_size -Wl,0x1000000") + # Set stack size to 32MB - by default Apple's clang defines a stack size of 8MB. + # Normally 16MB is enough to run all tests, but it will exceed the stack, if -DSANITIZE=address is used. + set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -Wl,-stack_size -Wl,0x2000000") endif() # Some Linux-specific Clang settings. We don't want these for OS X. diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index c4dee22d..425c5c1e 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -58,6 +58,19 @@ void SMTChecker::analyze(SourceUnit const& _source) _source.accept(*this); } +bool SMTChecker::visit(ContractDefinition const& _contract) +{ + for (auto _var : _contract.stateVariables()) + if (_var->type()->isValueType()) + createVariable(*_var); + return true; +} + +void SMTChecker::endVisit(ContractDefinition const&) +{ + m_stateVariables.clear(); +} + void SMTChecker::endVisit(VariableDeclaration const& _varDecl) { if (_varDecl.isLocalVariable() && _varDecl.type()->isValueType() &&_varDecl.value()) @@ -72,13 +85,13 @@ bool SMTChecker::visit(FunctionDefinition const& _function) "Assertion checker does not yet support constructors and functions with modifiers." ); m_currentFunction = &_function; - // We only handle local variables, so we clear at the beginning of the function. - // If we add storage variables, those should be cleared differently. m_interface->reset(); m_variables.clear(); + m_variables.insert(m_stateVariables.begin(), m_stateVariables.end()); m_pathConditions.clear(); m_loopExecutionHappened = false; initializeLocalVariables(_function); + resetStateVariables(); return true; } @@ -586,6 +599,12 @@ void SMTChecker::checkCondition( expressionsToEvaluate.emplace_back(currentValue(*var)); expressionNames.push_back(var->name()); } + for (auto const& var: m_stateVariables) + if (knownVariable(*var.first)) + { + expressionsToEvaluate.emplace_back(currentValue(*var.first)); + expressionNames.push_back(var.first->name()); + } } smt::CheckResult result; vector<string> values; @@ -607,7 +626,8 @@ void SMTChecker::checkCondition( message << " for:\n"; solAssert(values.size() == expressionNames.size(), ""); for (size_t i = 0; i < values.size(); ++i) - message << " " << expressionNames.at(i) << " = " << values.at(i) << "\n"; + if (expressionsToEvaluate.at(i).name != values.at(i)) + message << " " << expressionNames.at(i) << " = " << values.at(i) << "\n"; } else message << "."; @@ -722,6 +742,15 @@ void SMTChecker::initializeLocalVariables(FunctionDefinition const& _function) setZeroValue(*retParam); } +void SMTChecker::resetStateVariables() +{ + for (auto const& variable: m_stateVariables) + { + newValue(*variable.first); + setUnknownValue(*variable.first); + } +} + void SMTChecker::resetVariables(vector<Declaration const*> _variables) { for (auto const* decl: _variables) @@ -752,7 +781,14 @@ bool SMTChecker::createVariable(VariableDeclaration const& _varDecl) if (SSAVariable::isSupportedType(_varDecl.type()->category())) { solAssert(m_variables.count(&_varDecl) == 0, ""); - m_variables.emplace(&_varDecl, SSAVariable(_varDecl, *m_interface)); + solAssert(m_stateVariables.count(&_varDecl) == 0, ""); + if (_varDecl.isLocalVariable()) + m_variables.emplace(&_varDecl, SSAVariable(_varDecl, *m_interface)); + else + { + solAssert(_varDecl.isStateVariable(), ""); + m_stateVariables.emplace(&_varDecl, SSAVariable(_varDecl, *m_interface)); + } return true; } else diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index fd54fb5c..50d40ab9 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -50,6 +50,8 @@ private: // because the order of expression evaluation is undefined // TODO: or just force a certain order, but people might have a different idea about that. + virtual bool visit(ContractDefinition const& _node) override; + virtual void endVisit(ContractDefinition const& _node) override; virtual void endVisit(VariableDeclaration const& _node) override; virtual bool visit(FunctionDefinition const& _node) override; virtual void endVisit(FunctionDefinition const& _node) override; @@ -111,6 +113,7 @@ private: smt::CheckResult checkSatisfiable(); void initializeLocalVariables(FunctionDefinition const& _function); + void resetStateVariables(); void resetVariables(std::vector<Declaration const*> _variables); /// Given two different branches and the touched variables, /// merge the touched variables into after-branch ite variables @@ -163,6 +166,7 @@ private: bool m_loopExecutionHappened = false; std::map<Expression const*, smt::Expression> m_expressions; std::map<Declaration const*, SSAVariable> m_variables; + std::map<Declaration const*, SSAVariable> m_stateVariables; std::vector<smt::Expression> m_pathConditions; ErrorReporter& m_errorReporter; diff --git a/libsolidity/formal/VariableUsage.cpp b/libsolidity/formal/VariableUsage.cpp index 4e96059d..c2dea844 100644 --- a/libsolidity/formal/VariableUsage.cpp +++ b/libsolidity/formal/VariableUsage.cpp @@ -33,7 +33,6 @@ VariableUsage::VariableUsage(ASTNode const& _node) solAssert(declaration, ""); if (VariableDeclaration const* varDecl = dynamic_cast<VariableDeclaration const*>(declaration)) if ( - varDecl->isLocalVariable() && identifier->annotation().lValueRequested && varDecl->annotation().type->isValueType() ) diff --git a/test/libsolidity/SMTChecker.cpp b/test/libsolidity/SMTChecker.cpp index beb933a4..71fdb906 100644 --- a/test/libsolidity/SMTChecker.cpp +++ b/test/libsolidity/SMTChecker.cpp @@ -467,6 +467,82 @@ BOOST_AUTO_TEST_CASE(bool_int_mixed) CHECK_SUCCESS_NO_WARNINGS(text); } +BOOST_AUTO_TEST_CASE(storage_value_vars) +{ + string text = R"( + contract C + { + address a; + bool b; + uint c; + function f(uint x) public { + if (x == 0) + { + a = 100; + b = true; + } + else + { + a = 200; + b = false; + } + assert(a > 0 && b); + } + } + )"; + CHECK_WARNING(text, "Assertion violation happens here"); + text = R"( + contract C + { + address a; + bool b; + uint c; + function f() public view { + assert(c > 0); + } + } + )"; + CHECK_WARNING(text, "Assertion violation happens here"); + text = R"( + contract C + { + function f(uint x) public { + if (x == 0) + { + a = 100; + b = true; + } + else + { + a = 200; + b = false; + } + assert(b == (a < 200)); + } + + function g() public view { + require(a < 100); + assert(c >= 0); + } + address a; + bool b; + uint c; + } + )"; + CHECK_SUCCESS_NO_WARNINGS(text); + text = R"( + contract C + { + function f() public view { + assert(c > 0); + } + uint c; + } + )"; + CHECK_WARNING(text, "Assertion violation happens here"); + +} + BOOST_AUTO_TEST_CASE(while_loop_simple) { // Check that variables are cleared |