diff options
author | chriseth <chris@ethereum.org> | 2017-09-28 21:24:24 +0800 |
---|---|---|
committer | Alex Beregszaszi <alex@rtfs.hu> | 2017-11-22 10:35:34 +0800 |
commit | b37377641dd1cac7d1b5d5307ea6f7517c0f321f (patch) | |
tree | 87f0fa99f5eec5d1f41b5c0ea7f5e3f3ebf7d391 | |
parent | f62caf587e9df37c67518d199065ab50bcbb320c (diff) | |
download | dexon-solidity-b37377641dd1cac7d1b5d5307ea6f7517c0f321f.tar dexon-solidity-b37377641dd1cac7d1b5d5307ea6f7517c0f321f.tar.gz dexon-solidity-b37377641dd1cac7d1b5d5307ea6f7517c0f321f.tar.bz2 dexon-solidity-b37377641dd1cac7d1b5d5307ea6f7517c0f321f.tar.lz dexon-solidity-b37377641dd1cac7d1b5d5307ea6f7517c0f321f.tar.xz dexon-solidity-b37377641dd1cac7d1b5d5307ea6f7517c0f321f.tar.zst dexon-solidity-b37377641dd1cac7d1b5d5307ea6f7517c0f321f.zip |
Track usage of variables.
-rw-r--r-- | libsolidity/formal/SMTChecker.cpp | 130 | ||||
-rw-r--r-- | libsolidity/formal/SMTChecker.h | 25 | ||||
-rw-r--r-- | libsolidity/formal/VariableUsage.cpp | 80 | ||||
-rw-r--r-- | libsolidity/formal/VariableUsage.h | 50 |
4 files changed, 215 insertions, 70 deletions
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 0dc6e642..428afa9f 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -23,6 +23,8 @@ #include <libsolidity/formal/SMTLib2Interface.h> #endif +#include <libsolidity/formal/VariableUsage.h> + #include <libsolidity/interface/ErrorReporter.h> #include <boost/range/adaptor/map.hpp> @@ -44,23 +46,15 @@ SMTChecker::SMTChecker(ErrorReporter& _errorReporter, ReadCallback::Callback con void SMTChecker::analyze(SourceUnit const& _source) { + m_variableUsage = make_shared<VariableUsage>(_source); if (_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker)) _source.accept(*this); } void SMTChecker::endVisit(VariableDeclaration const& _varDecl) { - if (_varDecl.value()) - { - m_errorReporter.warning( - _varDecl.location(), - "Assertion checker does not yet support this." - ); - } - else if (_varDecl.isLocalOrReturn()) - createVariable(_varDecl, true); - else if (_varDecl.isCallableParameter()) - createVariable(_varDecl, false); + if (_varDecl.isLocalVariable() && _varDecl.type()->isValueType() &&_varDecl.value()) + assignment(_varDecl, *_varDecl.value()); } bool SMTChecker::visit(FunctionDefinition const& _function) @@ -77,6 +71,7 @@ bool SMTChecker::visit(FunctionDefinition const& _function) m_currentSequenceCounter.clear(); m_nextFreeSequenceCounter.clear(); m_conditionalExecutionHappened = false; + initializeLocalVariables(_function); return true; } @@ -94,9 +89,13 @@ bool SMTChecker::visit(IfStatement const& _node) // TODO Check if condition is always true - auto touchedVariables = visitBranch(_node.trueStatement(), expr(_node.condition())); + visitBranch(_node.trueStatement(), expr(_node.condition())); + vector<Declaration const*> touchedVariables = m_variableUsage->touchedVariables(_node.trueStatement()); if (_node.falseStatement()) - touchedVariables += visitBranch(*_node.falseStatement(), !expr(_node.condition())); + { + visitBranch(*_node.falseStatement(), !expr(_node.condition())); + touchedVariables += m_variableUsage->touchedVariables(*_node.falseStatement()); + } resetVariables(touchedVariables); @@ -111,20 +110,21 @@ bool SMTChecker::visit(WhileStatement const& _node) // uint x = 1; // while (x ++ > 0) { assert(x == 2); } // solution: clear variables first, then execute and assert condition, then executed body. + + auto touchedVariables = m_variableUsage->touchedVariables(_node); + resetVariables(touchedVariables); if (_node.isDoWhile()) { - auto touchedVariables = visitBranch(_node.body()); - // TODO what about the side-effects of this? - // If we have a "break", this might never be executed. + visitBranch(_node.body()); + // TODO the assertions generated in the body should still be active in the condition _node.condition().accept(*this); - resetVariables(touchedVariables); } else { _node.condition().accept(*this); - auto touchedVariables = visitBranch(_node.body(), expr(_node.condition())); - resetVariables(touchedVariables); + visitBranch(_node.body(), expr(_node.condition())); } + resetVariables(touchedVariables); return false; } @@ -140,8 +140,7 @@ void SMTChecker::endVisit(VariableDeclarationStatement const& _varDecl) { if (_varDecl.initialValue()) // TODO more checks? - // TODO add restrictions about type (might be assignment from smaller type) - m_interface->addAssertion(newValue(*_varDecl.declarations()[0]) == expr(*_varDecl.initialValue())); + assignment(*_varDecl.declarations()[0], *_varDecl.initialValue()); } else m_errorReporter.warning( @@ -170,9 +169,7 @@ void SMTChecker::endVisit(Assignment const& _assignment) { Declaration const* decl = identifier->annotation().referencedDeclaration; if (knownVariable(*decl)) - // TODO more checks? - // TODO add restrictions about type (might be assignment from smaller type) - m_interface->addAssertion(newValue(*decl) == expr(_assignment.rightHandSide())); + assignment(*decl, _assignment.rightHandSide()); else m_errorReporter.warning( _assignment.location(), @@ -249,23 +246,17 @@ void SMTChecker::endVisit(Identifier const& _identifier) { Declaration const* decl = _identifier.annotation().referencedDeclaration; solAssert(decl, ""); - if (dynamic_cast<IntegerType const*>(_identifier.annotation().type.get())) + if (_identifier.annotation().lValueRequested) { - m_interface->addAssertion(expr(_identifier) == currentValue(*decl)); - return; + // Will be translated as part of the node that requested the lvalue. } + else if (dynamic_cast<IntegerType const*>(_identifier.annotation().type.get())) + m_interface->addAssertion(expr(_identifier) == currentValue(*decl)); else if (FunctionType const* fun = dynamic_cast<FunctionType const*>(_identifier.annotation().type.get())) { if (fun->kind() == FunctionType::Kind::Assert || fun->kind() == FunctionType::Kind::Require) return; - // TODO for others, clear our knowledge about storage and memory } - m_errorReporter.warning( - _identifier.location(), - "Assertion checker does not yet support the type of this expression (" + - _identifier.annotation().type->toString() + - ")." - ); } void SMTChecker::endVisit(Literal const& _literal) @@ -281,7 +272,7 @@ void SMTChecker::endVisit(Literal const& _literal) else m_errorReporter.warning( _literal.location(), - "Assertion checker does not yet support the type of this expression (" + + "Assertion checker does not yet support the type of this literal (" + _literal.annotation().type->toString() + ")." ); @@ -379,12 +370,19 @@ void SMTChecker::booleanOperation(BinaryOperation const& _op) ); } -set<Declaration const*> SMTChecker::visitBranch(Statement const& _statement, smt::Expression _condition) +void SMTChecker::assignment(Declaration const& _variable, Expression const& _value) { - return visitBranch(_statement, &_condition); + // TODO more checks? + // TODO add restrictions about type (might be assignment from smaller type) + m_interface->addAssertion(newValue(_variable) == expr(_value)); } -set<Declaration const*> SMTChecker::visitBranch(Statement const& _statement, smt::Expression const* _condition) +void SMTChecker::visitBranch(Statement const& _statement, smt::Expression _condition) +{ + visitBranch(_statement, &_condition); +} + +void SMTChecker::visitBranch(Statement const& _statement, smt::Expression const* _condition) { VariableSequenceCounters sequenceCountersStart = m_currentSequenceCounter; @@ -395,18 +393,7 @@ set<Declaration const*> SMTChecker::visitBranch(Statement const& _statement, smt m_interface->pop(); m_conditionalExecutionHappened = true; - - set<Declaration const*> touched; - for (auto const& seq: m_currentSequenceCounter) - { - if (!sequenceCountersStart.count(seq.first)) - touched.insert(seq.first); - else if (sequenceCountersStart[seq.first] != seq.second) - touched.insert(seq.first); - } m_currentSequenceCounter = sequenceCountersStart; - - return touched; } void SMTChecker::checkCondition( @@ -504,16 +491,36 @@ void SMTChecker::checkCondition( m_interface->pop(); } -void SMTChecker::resetVariables(set<Declaration const*> _variables) +void SMTChecker::initializeLocalVariables(FunctionDefinition const& _function) +{ + for (auto const& variable: _function.localVariables()) + { + createVariable(*variable); + setZeroValue(*variable); + } + for (auto const& param: _function.parameters()) + { + createVariable(*param); + setUnknownValue(*param); + } + if (_function.returnParameterList()) + for (auto const& retParam: _function.returnParameters()) + { + createVariable(*retParam); + setZeroValue(*retParam); + } +} + +void SMTChecker::resetVariables(vector<Declaration const*> _variables) { for (auto const* decl: _variables) { newValue(*decl); - setValue(*decl, false); + setUnknownValue(*decl); } } -void SMTChecker::createVariable(VariableDeclaration const& _varDecl, bool _setToZero) +void SMTChecker::createVariable(VariableDeclaration const& _varDecl) { if (dynamic_cast<IntegerType const*>(_varDecl.type().get())) { @@ -523,7 +530,6 @@ void SMTChecker::createVariable(VariableDeclaration const& _varDecl, bool _setTo m_currentSequenceCounter[&_varDecl] = 0; m_nextFreeSequenceCounter[&_varDecl] = 1; m_variables.emplace(&_varDecl, m_interface->newFunction(uniqueSymbol(_varDecl), smt::Sort::Int, smt::Sort::Int)); - setValue(_varDecl, _setToZero); } else m_errorReporter.warning( @@ -565,17 +571,17 @@ smt::Expression SMTChecker::newValue(Declaration const& _decl) return currentValue(_decl); } -void SMTChecker::setValue(Declaration const& _decl, bool _setToZero) +void SMTChecker::setZeroValue(Declaration const& _decl) { - auto const& intType = dynamic_cast<IntegerType const&>(*_decl.type()); + solAssert(_decl.type()->category() == Type::Category::Integer, ""); + m_interface->addAssertion(currentValue(_decl) == 0); +} - if (_setToZero) - m_interface->addAssertion(currentValue(_decl) == 0); - else - { - m_interface->addAssertion(currentValue(_decl) >= minValue(intType)); - m_interface->addAssertion(currentValue(_decl) <= maxValue(intType)); - } +void SMTChecker::setUnknownValue(Declaration const& _decl) +{ + auto const& intType = dynamic_cast<IntegerType const&>(*_decl.type()); + m_interface->addAssertion(currentValue(_decl) >= minValue(intType)); + m_interface->addAssertion(currentValue(_decl) <= maxValue(intType)); } smt::Expression SMTChecker::minValue(IntegerType const& _t) diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index 6575dc1b..b2726a42 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -17,8 +17,11 @@ #pragma once -#include <libsolidity/ast/ASTVisitor.h> + #include <libsolidity/formal/SolverInterface.h> + +#include <libsolidity/ast/ASTVisitor.h> + #include <libsolidity/interface/ReadFile.h> #include <map> @@ -29,6 +32,7 @@ namespace dev namespace solidity { +class VariableUsage; class ErrorReporter; class SMTChecker: private ASTConstVisitor @@ -61,11 +65,12 @@ private: void compareOperation(BinaryOperation const& _op); void booleanOperation(BinaryOperation const& _op); + void assignment(Declaration const& _variable, Expression const& _value); + // Visits the branch given by the statement, pushes and pops the SMT checker. - // @returns the set of touched declarations // @param _condition if present, asserts that this condition is true within the branch. - std::set<Declaration const*> visitBranch(Statement const& _statement, smt::Expression const* _condition = nullptr); - std::set<Declaration const*> visitBranch(Statement const& _statement, smt::Expression _condition); + void visitBranch(Statement const& _statement, smt::Expression const* _condition = nullptr); + void visitBranch(Statement const& _statement, smt::Expression _condition); void checkCondition( smt::Expression _condition, @@ -75,8 +80,9 @@ private: smt::Expression* _additionalValue = nullptr ); - void resetVariables(std::set<Declaration const*> _variables); - void createVariable(VariableDeclaration const& _varDecl, bool _setToZero); + void initializeLocalVariables(FunctionDefinition const& _function); + void resetVariables(std::vector<Declaration const*> _variables); + void createVariable(VariableDeclaration const& _varDecl); static std::string uniqueSymbol(Declaration const& _decl); static std::string uniqueSymbol(Expression const& _expr); @@ -94,8 +100,10 @@ private: /// sequence number to this value and returns the expression. smt::Expression newValue(Declaration const& _decl); - /// Sets the value of the declaration either to zero or to its intrinsic range. - void setValue(Declaration const& _decl, bool _setToZero); + /// Sets the value of the declaration to zero. + void setZeroValue(Declaration const& _decl); + /// Resets the variable to an unknown value (in its range). + void setUnknownValue(Declaration const& decl); static smt::Expression minValue(IntegerType const& _t); static smt::Expression maxValue(IntegerType const& _t); @@ -110,6 +118,7 @@ private: smt::Expression var(Declaration const& _decl); std::shared_ptr<smt::SolverInterface> m_interface; + std::shared_ptr<VariableUsage> m_variableUsage; bool m_conditionalExecutionHappened = false; std::map<Declaration const*, int> m_currentSequenceCounter; std::map<Declaration const*, int> m_nextFreeSequenceCounter; diff --git a/libsolidity/formal/VariableUsage.cpp b/libsolidity/formal/VariableUsage.cpp new file mode 100644 index 00000000..4e96059d --- /dev/null +++ b/libsolidity/formal/VariableUsage.cpp @@ -0,0 +1,80 @@ +/* + This file is part of solidity. + + solidity is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + solidity is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with solidity. If not, see <http://www.gnu.org/licenses/>. +*/ + +#include <libsolidity/formal/VariableUsage.h> + +#include <libsolidity/ast/ASTVisitor.h> + +using namespace std; +using namespace dev; +using namespace dev::solidity; + +VariableUsage::VariableUsage(ASTNode const& _node) +{ + auto nodeFun = [&](ASTNode const& n) -> bool + { + if (Identifier const* identifier = dynamic_cast<decltype(identifier)>(&n)) + { + Declaration const* declaration = identifier->annotation().referencedDeclaration; + solAssert(declaration, ""); + if (VariableDeclaration const* varDecl = dynamic_cast<VariableDeclaration const*>(declaration)) + if ( + varDecl->isLocalVariable() && + identifier->annotation().lValueRequested && + varDecl->annotation().type->isValueType() + ) + m_touchedVariable[&n] = varDecl; + } + return true; + }; + auto edgeFun = [&](ASTNode const& _parent, ASTNode const& _child) + { + if (m_touchedVariable.count(&_child) || m_children.count(&_child)) + m_children[&_parent].push_back(&_child); + }; + + ASTReduce reducer(nodeFun, edgeFun); + _node.accept(reducer); +} + +vector<Declaration const*> VariableUsage::touchedVariables(ASTNode const& _node) const +{ + if (!m_children.count(&_node) && !m_touchedVariable.count(&_node)) + return {}; + + set<Declaration const*> touched; + vector<ASTNode const*> toVisit; + toVisit.push_back(&_node); + + while (!toVisit.empty()) + { + ASTNode const* n = toVisit.back(); + toVisit.pop_back(); + if (m_children.count(n)) + { + solAssert(!m_touchedVariable.count(n), ""); + toVisit += m_children.at(n); + } + else + { + solAssert(m_touchedVariable.count(n), ""); + touched.insert(m_touchedVariable.at(n)); + } + } + + return {touched.begin(), touched.end()}; +} diff --git a/libsolidity/formal/VariableUsage.h b/libsolidity/formal/VariableUsage.h new file mode 100644 index 00000000..62561cce --- /dev/null +++ b/libsolidity/formal/VariableUsage.h @@ -0,0 +1,50 @@ +/* + This file is part of solidity. + + solidity is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + solidity is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with solidity. If not, see <http://www.gnu.org/licenses/>. +*/ + +#pragma once + +#include <map> +#include <set> +#include <vector> + +namespace dev +{ +namespace solidity +{ + +class ASTNode; +class Declaration; + +/** + * This class collects information about which local variables of value type + * are modified in which parts of the AST. + */ +class VariableUsage +{ +public: + explicit VariableUsage(ASTNode const& _node); + + std::vector<Declaration const*> touchedVariables(ASTNode const& _node) const; + +private: + // Variable touched by a specific AST node. + std::map<ASTNode const*, Declaration const*> m_touchedVariable; + std::map<ASTNode const*, std::vector<ASTNode const*>> m_children; +}; + +} +} |