diff options
Diffstat (limited to 'libsolidity/formal')
| -rw-r--r-- | libsolidity/formal/SMTChecker.cpp | 81 | ||||
| -rw-r--r-- | libsolidity/formal/SMTChecker.h | 12 | ||||
| -rw-r--r-- | libsolidity/formal/SSAVariable.cpp | 66 | ||||
| -rw-r--r-- | libsolidity/formal/SSAVariable.h | 79 | ||||
| -rw-r--r-- | libsolidity/formal/SymbolicIntVariable.cpp | 54 | ||||
| -rw-r--r-- | libsolidity/formal/SymbolicIntVariable.h | 51 | ||||
| -rw-r--r-- | libsolidity/formal/SymbolicVariable.cpp | 38 | ||||
| -rw-r--r-- | libsolidity/formal/SymbolicVariable.h | 68 |
8 files changed, 395 insertions, 54 deletions
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index a64024b3..37dce96c 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -23,6 +23,7 @@ #include <libsolidity/formal/SMTLib2Interface.h> #endif +#include <libsolidity/formal/SSAVariable.h> #include <libsolidity/formal/VariableUsage.h> #include <libsolidity/interface/ErrorReporter.h> @@ -69,8 +70,7 @@ bool SMTChecker::visit(FunctionDefinition const& _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_currentSequenceCounter.clear(); - m_nextFreeSequenceCounter.clear(); + m_variables.clear(); m_pathConditions.clear(); m_conditionalExecutionHappened = false; initializeLocalVariables(_function); @@ -91,14 +91,18 @@ bool SMTChecker::visit(IfStatement const& _node) checkBooleanNotConstant(_node.condition(), "Condition is always $VALUE."); - auto countersEndFalse = m_currentSequenceCounter; auto countersEndTrue = visitBranch(_node.trueStatement(), expr(_node.condition())); vector<Declaration const*> touchedVariables = m_variableUsage->touchedVariables(_node.trueStatement()); + decltype(countersEndTrue) countersEndFalse; if (_node.falseStatement()) { countersEndFalse = visitBranch(*_node.falseStatement(), !expr(_node.condition())); touchedVariables += m_variableUsage->touchedVariables(*_node.falseStatement()); } + else + { + countersEndFalse = m_variables; + } mergeVariables(touchedVariables, expr(_node.condition()), countersEndTrue, countersEndFalse); @@ -152,7 +156,7 @@ bool SMTChecker::visit(ForStatement const& _node) checkBooleanNotConstant(*_node.condition(), "For loop condition is always $VALUE."); } - VariableSequenceCounters sequenceCountersStart = m_currentSequenceCounter; + VariableSequenceCounters sequenceCountersStart = m_variables; m_interface->push(); if (_node.condition()) m_interface->addAssertion(expr(*_node.condition())); @@ -163,7 +167,7 @@ bool SMTChecker::visit(ForStatement const& _node) m_interface->pop(); m_conditionalExecutionHappened = true; - m_currentSequenceCounter = sequenceCountersStart; + std::swap(sequenceCountersStart, m_variables); resetVariables(touchedVariables); @@ -514,7 +518,7 @@ SMTChecker::VariableSequenceCounters SMTChecker::visitBranch(Statement const& _s SMTChecker::VariableSequenceCounters SMTChecker::visitBranch(Statement const& _statement, smt::Expression const* _condition) { - VariableSequenceCounters sequenceCountersStart = m_currentSequenceCounter; + VariableSequenceCounters beforeVars = m_variables; if (_condition) pushPathCondition(*_condition); @@ -523,8 +527,9 @@ SMTChecker::VariableSequenceCounters SMTChecker::visitBranch(Statement const& _s popPathCondition(); m_conditionalExecutionHappened = true; - std::swap(sequenceCountersStart, m_currentSequenceCounter); - return sequenceCountersStart; + std::swap(m_variables, beforeVars); + + return beforeVars; } void SMTChecker::checkCondition( @@ -709,8 +714,8 @@ void SMTChecker::mergeVariables(vector<Declaration const*> const& _variables, sm set<Declaration const*> uniqueVars(_variables.begin(), _variables.end()); for (auto const* decl: uniqueVars) { - int trueCounter = _countersEndTrue.at(decl); - int falseCounter = _countersEndFalse.at(decl); + int trueCounter = _countersEndTrue.at(decl).index(); + int falseCounter = _countersEndFalse.at(decl).index(); solAssert(trueCounter != falseCounter, ""); m_interface->addAssertion(newValue(*decl) == smt::Expression::ite( _condition, @@ -724,12 +729,8 @@ bool SMTChecker::createVariable(VariableDeclaration const& _varDecl) { if (dynamic_cast<IntegerType const*>(_varDecl.type().get())) { - solAssert(m_currentSequenceCounter.count(&_varDecl) == 0, ""); - solAssert(m_nextFreeSequenceCounter.count(&_varDecl) == 0, ""); solAssert(m_variables.count(&_varDecl) == 0, ""); - m_currentSequenceCounter[&_varDecl] = 0; - m_nextFreeSequenceCounter[&_varDecl] = 1; - m_variables.emplace(&_varDecl, m_interface->newFunction(uniqueSymbol(_varDecl), smt::Sort::Int, smt::Sort::Int)); + m_variables.emplace(&_varDecl, SSAVariable(&_varDecl, *m_interface)); return true; } else @@ -742,11 +743,6 @@ bool SMTChecker::createVariable(VariableDeclaration const& _varDecl) } } -string SMTChecker::uniqueSymbol(Declaration const& _decl) -{ - return _decl.name() + "_" + to_string(_decl.id()); -} - string SMTChecker::uniqueSymbol(Expression const& _expr) { return "expr_" + to_string(_expr.id()); @@ -754,48 +750,38 @@ string SMTChecker::uniqueSymbol(Expression const& _expr) bool SMTChecker::knownVariable(Declaration const& _decl) { - return m_currentSequenceCounter.count(&_decl); + return m_variables.count(&_decl); } smt::Expression SMTChecker::currentValue(Declaration const& _decl) { - solAssert(m_currentSequenceCounter.count(&_decl), ""); - return valueAtSequence(_decl, m_currentSequenceCounter.at(&_decl)); + solAssert(knownVariable(_decl), ""); + return m_variables.at(&_decl)(); } -smt::Expression SMTChecker::valueAtSequence(const Declaration& _decl, int _sequence) +smt::Expression SMTChecker::valueAtSequence(Declaration const& _decl, int _sequence) { - return var(_decl)(_sequence); + solAssert(knownVariable(_decl), ""); + return m_variables.at(&_decl)(_sequence); } smt::Expression SMTChecker::newValue(Declaration const& _decl) { - solAssert(m_nextFreeSequenceCounter.count(&_decl), ""); - m_currentSequenceCounter[&_decl] = m_nextFreeSequenceCounter[&_decl]++; - return currentValue(_decl); + solAssert(knownVariable(_decl), ""); + ++m_variables.at(&_decl); + return m_variables.at(&_decl)(); } void SMTChecker::setZeroValue(Declaration const& _decl) { - solAssert(_decl.type()->category() == Type::Category::Integer, ""); - m_interface->addAssertion(currentValue(_decl) == 0); + solAssert(knownVariable(_decl), ""); + m_variables.at(&_decl).setZeroValue(); } 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) -{ - return smt::Expression(_t.minValue()); -} - -smt::Expression SMTChecker::maxValue(IntegerType const& _t) -{ - return smt::Expression(_t.maxValue()); + solAssert(knownVariable(_decl), ""); + m_variables.at(&_decl).setUnknownValue(); } smt::Expression SMTChecker::expr(Expression const& _e) @@ -842,12 +828,15 @@ void SMTChecker::defineExpr(Expression const& _e, smt::Expression _value) m_interface->addAssertion(expr(_e) == _value); } -smt::Expression SMTChecker::var(Declaration const& _decl) +smt::Expression SMTChecker::minValue(IntegerType const& _t) { - solAssert(m_variables.count(&_decl), ""); - return m_variables.at(&_decl); + return smt::Expression(_t.minValue()); } +smt::Expression SMTChecker::maxValue(IntegerType const& _t) +{ + return smt::Expression(_t.maxValue()); +} void SMTChecker::popPathCondition() { solAssert(m_pathConditions.size() > 0, "Cannot pop path condition, empty."); diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index b57f0f96..7481e1c8 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -20,6 +20,8 @@ #include <libsolidity/formal/SolverInterface.h> +#include <libsolidity/formal/SSAVariable.h> + #include <libsolidity/ast/ASTVisitor.h> #include <libsolidity/interface/ReadFile.h> @@ -76,7 +78,7 @@ private: void assignment(Declaration const& _variable, smt::Expression const& _value, SourceLocation const& _location); /// Maps a variable to an SSA index. - using VariableSequenceCounters = std::map<Declaration const*, int>; + using VariableSequenceCounters = std::map<Declaration const*, SSAVariable>; /// Visits the branch given by the statement, pushes and pops the current path conditions. /// @param _condition if present, asserts that this condition is true within the branch. @@ -118,7 +120,6 @@ private: /// This fails if the type is not supported. bool createVariable(VariableDeclaration const& _varDecl); - static std::string uniqueSymbol(Declaration const& _decl); static std::string uniqueSymbol(Expression const& _expr); /// @returns true if _delc is a variable that is known at the current point, i.e. @@ -148,9 +149,6 @@ private: void createExpr(Expression const& _e); /// Creates the expression and sets its value. void defineExpr(Expression const& _e, smt::Expression _value); - /// Returns the function declaration corresponding to the given variable. - /// The function takes one argument which is the "sequence number". - smt::Expression var(Declaration const& _decl); /// Adds a new path condition void pushPathCondition(smt::Expression const& _e); @@ -166,10 +164,8 @@ private: 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; std::map<Expression const*, smt::Expression> m_expressions; - std::map<Declaration const*, smt::Expression> m_variables; + std::map<Declaration const*, SSAVariable> m_variables; std::vector<smt::Expression> m_pathConditions; ErrorReporter& m_errorReporter; diff --git a/libsolidity/formal/SSAVariable.cpp b/libsolidity/formal/SSAVariable.cpp new file mode 100644 index 00000000..d6e97a8d --- /dev/null +++ b/libsolidity/formal/SSAVariable.cpp @@ -0,0 +1,66 @@ +/* + 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/SSAVariable.h> + +#include <libsolidity/formal/SymbolicIntVariable.h> + +#include <libsolidity/ast/AST.h> + +using namespace std; +using namespace dev; +using namespace dev::solidity; + +SSAVariable::SSAVariable(Declaration const* _decl, + smt::SolverInterface& _interface) +{ + resetIndex(); + + if (dynamic_cast<IntegerType const*>(_decl->type().get())) + m_symbVar = make_shared<SymbolicIntVariable>(_decl, _interface); + else + { + //solAssert(false, ""); + } +} + +void SSAVariable::resetIndex() +{ + m_currentSequenceCounter = 0; + m_nextFreeSequenceCounter.reset (new int); + *m_nextFreeSequenceCounter = 1; +} + +int SSAVariable::index() const +{ + return m_currentSequenceCounter; +} + +int SSAVariable::next() const +{ + return *m_nextFreeSequenceCounter; +} + +void SSAVariable::setZeroValue() +{ + m_symbVar->setZeroValue(index()); +} + +void SSAVariable::setUnknownValue() +{ + m_symbVar->setUnknownValue(index()); +} diff --git a/libsolidity/formal/SSAVariable.h b/libsolidity/formal/SSAVariable.h new file mode 100644 index 00000000..3d7eb80c --- /dev/null +++ b/libsolidity/formal/SSAVariable.h @@ -0,0 +1,79 @@ +/* + 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 <libsolidity/formal/SymbolicVariable.h> + +#include <memory> + +namespace dev +{ +namespace solidity +{ + +class Declaration; + +/** + * This class represents the SSA representation of a program variable. + */ +class SSAVariable +{ +public: + explicit SSAVariable(Declaration const* _decl, + smt::SolverInterface& _interface); + SSAVariable(SSAVariable const&) = default; + SSAVariable(SSAVariable&&) = default; + SSAVariable& operator=(SSAVariable const&) = default; + SSAVariable& operator=(SSAVariable&&) = default; + + void resetIndex(); + + int index() const; + int next() const; + + int operator++() + { + return m_currentSequenceCounter = (*m_nextFreeSequenceCounter)++; + } + + smt::Expression operator()() const + { + return valueAtSequence(index()); + } + + smt::Expression operator()(int _seq) const + { + return valueAtSequence(_seq); + } + + void setZeroValue(); + void setUnknownValue(); + +private: + smt::Expression valueAtSequence(int _seq) const + { + return (*m_symbVar)(_seq); + } + + std::shared_ptr<SymbolicVariable> m_symbVar = nullptr; + int m_currentSequenceCounter; + std::shared_ptr<int> m_nextFreeSequenceCounter; +}; + +} +} diff --git a/libsolidity/formal/SymbolicIntVariable.cpp b/libsolidity/formal/SymbolicIntVariable.cpp new file mode 100644 index 00000000..6ed7037f --- /dev/null +++ b/libsolidity/formal/SymbolicIntVariable.cpp @@ -0,0 +1,54 @@ +/* + 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/SymbolicIntVariable.h> + +#include <libsolidity/ast/AST.h> + +using namespace std; +using namespace dev; +using namespace dev::solidity; + +SymbolicIntVariable::SymbolicIntVariable(Declaration const* _decl, + smt::SolverInterface&_interface) + : SymbolicVariable(_decl, _interface) +{ + solAssert(m_declaration->type()->category() == Type::Category::Integer, ""); + m_expression = make_shared<smt::Expression>(m_interface.newFunction(uniqueSymbol(), smt::Sort::Int, smt::Sort::Int)); +} + +void SymbolicIntVariable::setZeroValue(int _seq) +{ + m_interface.addAssertion(valueAtSequence(_seq) == 0); +} + +void SymbolicIntVariable::setUnknownValue(int _seq) +{ + auto const& intType = dynamic_cast<IntegerType const&>(*m_declaration->type()); + m_interface.addAssertion(valueAtSequence(_seq) >= minValue(intType)); + m_interface.addAssertion(valueAtSequence(_seq) <= maxValue(intType)); +} + +smt::Expression SymbolicIntVariable::minValue(IntegerType const& _t) const +{ + return smt::Expression(_t.minValue()); +} + +smt::Expression SymbolicIntVariable::maxValue(IntegerType const& _t) const +{ + return smt::Expression(_t.maxValue()); +} diff --git a/libsolidity/formal/SymbolicIntVariable.h b/libsolidity/formal/SymbolicIntVariable.h new file mode 100644 index 00000000..efe05af8 --- /dev/null +++ b/libsolidity/formal/SymbolicIntVariable.h @@ -0,0 +1,51 @@ +/* + 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 <libsolidity/formal/SymbolicVariable.h> + +#include <libsolidity/ast/Types.h> + +namespace dev +{ +namespace solidity +{ + +/** + * Specialization of SymbolicVariable for Integers + */ +class SymbolicIntVariable : public SymbolicVariable +{ +public: + explicit SymbolicIntVariable(Declaration const* _decl, + smt::SolverInterface& _interface); + SymbolicIntVariable(SymbolicIntVariable const&) = default; + SymbolicIntVariable(SymbolicIntVariable&&) = default; + SymbolicIntVariable& operator=(SymbolicIntVariable const&) = default; + SymbolicIntVariable& operator=(SymbolicIntVariable&&) = default; + + void setZeroValue(int _seq); + void setUnknownValue(int _seq); + +private: + smt::Expression minValue(IntegerType const& _t) const; + smt::Expression maxValue(IntegerType const& _t) const; +}; + +} +} diff --git a/libsolidity/formal/SymbolicVariable.cpp b/libsolidity/formal/SymbolicVariable.cpp new file mode 100644 index 00000000..13f5d9b6 --- /dev/null +++ b/libsolidity/formal/SymbolicVariable.cpp @@ -0,0 +1,38 @@ +/* + 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/SymbolicVariable.h> + +#include <libsolidity/ast/AST.h> + +using namespace std; +using namespace dev; +using namespace dev::solidity; + +SymbolicVariable::SymbolicVariable(Declaration const* _decl, + smt::SolverInterface& _interface) + : m_declaration(_decl), + m_interface(_interface) +{ +} + +string SymbolicVariable::uniqueSymbol() const +{ + return m_declaration->name() + "_" + to_string(m_declaration->id()); +} + + diff --git a/libsolidity/formal/SymbolicVariable.h b/libsolidity/formal/SymbolicVariable.h new file mode 100644 index 00000000..4de59504 --- /dev/null +++ b/libsolidity/formal/SymbolicVariable.h @@ -0,0 +1,68 @@ +/* + 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 <libsolidity/formal/SolverInterface.h> + +#include <libsolidity/ast/AST.h> + +#include <memory> + +namespace dev +{ +namespace solidity +{ + +class Declaration; + +/** + * This class represents the symbolic version of a program variable. + */ +class SymbolicVariable +{ +public: + explicit SymbolicVariable(Declaration const* _decl, + smt::SolverInterface& _interface); + SymbolicVariable(SymbolicVariable const&) = default; + SymbolicVariable(SymbolicVariable&&) = default; + SymbolicVariable& operator=(SymbolicVariable const&) = default; + SymbolicVariable& operator=(SymbolicVariable&&) = default; + + smt::Expression operator()(int _seq) const + { + return valueAtSequence(_seq); + } + + std::string uniqueSymbol() const; + + virtual void setZeroValue(int _seq) = 0; + virtual void setUnknownValue(int _seq) = 0; + +protected: + smt::Expression valueAtSequence(int _seq) const + { + return (*m_expression)(_seq); + } + + Declaration const* m_declaration; + std::shared_ptr<smt::Expression> m_expression = nullptr; + smt::SolverInterface& m_interface; +}; + +} +} |