From 2dbb35d4a8fc4321d59a670343b439232c92eaa9 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Wed, 18 Apr 2018 23:14:45 +0200 Subject: [PATCH 1/3] [SMTChecker] Support to integer and Bool storage vars --- Changelog.md | 1 + libsolidity/formal/SMTChecker.cpp | 33 ++++++++++++-- libsolidity/formal/SMTChecker.h | 2 + libsolidity/formal/VariableUsage.cpp | 1 - test/libsolidity/SMTChecker.cpp | 66 ++++++++++++++++++++++++++++ 5 files changed, 98 insertions(+), 5 deletions(-) diff --git a/Changelog.md b/Changelog.md index 6f6f672c9..e0b8cbc64 100644 --- a/Changelog.md +++ b/Changelog.md @@ -25,6 +25,7 @@ Features: * Build system: Support Ubuntu Bionic. * SMTChecker: Integration with CVC4 SMT solver * Syntax Checker: Warn about functions named "constructor". + * SMTChecker: Support to integer and Bool state variables Bugfixes: * Type Checker: Improve error message for failed function overload resolution. diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index c4dee22d2..358f1c582 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -62,6 +62,8 @@ void SMTChecker::endVisit(VariableDeclaration const& _varDecl) { if (_varDecl.isLocalVariable() && _varDecl.type()->isValueType() &&_varDecl.value()) assignment(_varDecl, *_varDecl.value(), _varDecl.location()); + else if (_varDecl.isStateVariable() && _varDecl.type()->isValueType()) + createVariable(_varDecl); } bool SMTChecker::visit(FunctionDefinition const& _function) @@ -72,13 +74,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 +588,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 values; @@ -607,7 +615,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 +731,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 _variables) { for (auto const* decl: _variables) @@ -752,7 +770,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 fd54fb5c7..6e64235eb 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -111,6 +111,7 @@ private: smt::CheckResult checkSatisfiable(); void initializeLocalVariables(FunctionDefinition const& _function); + void resetStateVariables(); void resetVariables(std::vector _variables); /// Given two different branches and the touched variables, /// merge the touched variables into after-branch ite variables @@ -163,6 +164,7 @@ private: bool m_loopExecutionHappened = false; std::map m_expressions; std::map m_variables; + std::map m_stateVariables; std::vector m_pathConditions; ErrorReporter& m_errorReporter; diff --git a/libsolidity/formal/VariableUsage.cpp b/libsolidity/formal/VariableUsage.cpp index 4e96059da..c2dea844a 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(declaration)) if ( - varDecl->isLocalVariable() && identifier->annotation().lValueRequested && varDecl->annotation().type->isValueType() ) diff --git a/test/libsolidity/SMTChecker.cpp b/test/libsolidity/SMTChecker.cpp index beb933a4e..ce3569f3b 100644 --- a/test/libsolidity/SMTChecker.cpp +++ b/test/libsolidity/SMTChecker.cpp @@ -467,6 +467,72 @@ 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 + { + address a; + bool b; + uint 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); + } + + } + )"; + CHECK_SUCCESS_NO_WARNINGS(text); +} + BOOST_AUTO_TEST_CASE(while_loop_simple) { // Check that variables are cleared From 4117e859eb5780873177cf1c93eb8379e17ed247 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Mon, 30 Apr 2018 16:30:41 +0200 Subject: [PATCH 2/3] [SMTChecker] Declaring all state vars before any function is visited --- Changelog.md | 2 +- libsolidity/formal/SMTChecker.cpp | 15 +++++++++++++-- libsolidity/formal/SMTChecker.h | 2 ++ test/libsolidity/SMTChecker.cpp | 11 +++++++++++ 4 files changed, 27 insertions(+), 3 deletions(-) diff --git a/Changelog.md b/Changelog.md index e0b8cbc64..0817faab4 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). @@ -25,7 +26,6 @@ Features: * Build system: Support Ubuntu Bionic. * SMTChecker: Integration with CVC4 SMT solver * Syntax Checker: Warn about functions named "constructor". - * SMTChecker: Support to integer and Bool state variables Bugfixes: * Type Checker: Improve error message for failed function overload resolution. diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 358f1c582..425c5c1e3 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -58,12 +58,23 @@ 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()) assignment(_varDecl, *_varDecl.value(), _varDecl.location()); - else if (_varDecl.isStateVariable() && _varDecl.type()->isValueType()) - createVariable(_varDecl); } bool SMTChecker::visit(FunctionDefinition const& _function) diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index 6e64235eb..50d40ab9c 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; diff --git a/test/libsolidity/SMTChecker.cpp b/test/libsolidity/SMTChecker.cpp index ce3569f3b..5f54db6d8 100644 --- a/test/libsolidity/SMTChecker.cpp +++ b/test/libsolidity/SMTChecker.cpp @@ -531,6 +531,17 @@ BOOST_AUTO_TEST_CASE(storage_value_vars) } )"; 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) From a0b42105e49456faf89dd0d86cfba2a6219c514e Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Wed, 2 May 2018 15:52:23 +0200 Subject: [PATCH 3/3] Testing state vars that are declared after functions that use them --- test/libsolidity/SMTChecker.cpp | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/test/libsolidity/SMTChecker.cpp b/test/libsolidity/SMTChecker.cpp index 5f54db6d8..71fdb906f 100644 --- a/test/libsolidity/SMTChecker.cpp +++ b/test/libsolidity/SMTChecker.cpp @@ -506,9 +506,6 @@ BOOST_AUTO_TEST_CASE(storage_value_vars) text = R"( contract C { - address a; - bool b; - uint c; function f(uint x) public { if (x == 0) { @@ -527,7 +524,9 @@ BOOST_AUTO_TEST_CASE(storage_value_vars) require(a < 100); assert(c >= 0); } - + address a; + bool b; + uint c; } )"; CHECK_SUCCESS_NO_WARNINGS(text);