diff options
| -rw-r--r-- | libsolidity/formal/SMTChecker.cpp | 87 | ||||
| -rw-r--r-- | libsolidity/formal/SMTChecker.h | 15 | ||||
| -rw-r--r-- | libsolidity/formal/SSAVariable.cpp | 73 | ||||
| -rw-r--r-- | libsolidity/formal/SSAVariable.h | 88 | ||||
| -rw-r--r-- | libsolidity/formal/SymbolicIntVariable.cpp | 56 | ||||
| -rw-r--r-- | libsolidity/formal/SymbolicIntVariable.h | 50 | ||||
| -rw-r--r-- | libsolidity/formal/SymbolicVariable.cpp | 40 | ||||
| -rw-r--r-- | libsolidity/formal/SymbolicVariable.h | 69 |
8 files changed, 414 insertions, 64 deletions
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index a64024b3..1da5b291 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -23,6 +23,8 @@ #include <libsolidity/formal/SMTLib2Interface.h> #endif +#include <libsolidity/formal/SSAVariable.h> +#include <libsolidity/formal/SymbolicIntVariable.h> #include <libsolidity/formal/VariableUsage.h> #include <libsolidity/interface/ErrorReporter.h> @@ -69,8 +71,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 +92,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 +157,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 +168,7 @@ bool SMTChecker::visit(ForStatement const& _node) m_interface->pop(); m_conditionalExecutionHappened = true; - m_currentSequenceCounter = sequenceCountersStart; + std::swap(sequenceCountersStart, m_variables); resetVariables(touchedVariables); @@ -240,14 +245,14 @@ void SMTChecker::endVisit(TupleExpression const& _tuple) void SMTChecker::checkUnderOverflow(smt::Expression _value, IntegerType const& _type, SourceLocation const& _location) { checkCondition( - _value < minValue(_type), + _value < SymbolicIntVariable::minValue(_type), _location, "Underflow (resulting value less than " + formatNumber(_type.minValue()) + ")", "value", &_value ); checkCondition( - _value > maxValue(_type), + _value > SymbolicIntVariable::maxValue(_type), _location, "Overflow (resulting value larger than " + formatNumber(_type.maxValue()) + ")", "value", @@ -365,7 +370,7 @@ void SMTChecker::endVisit(Identifier const& _identifier) { // Will be translated as part of the node that requested the lvalue. } - else if (dynamic_cast<IntegerType const*>(_identifier.annotation().type.get())) + else if (SSAVariable::supportedType(_identifier.annotation().type.get())) defineExpr(_identifier, currentValue(*decl)); else if (FunctionType const* fun = dynamic_cast<FunctionType const*>(_identifier.annotation().type.get())) { @@ -514,7 +519,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 +528,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 +715,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, @@ -722,14 +728,10 @@ void SMTChecker::mergeVariables(vector<Declaration const*> const& _variables, sm bool SMTChecker::createVariable(VariableDeclaration const& _varDecl) { - if (dynamic_cast<IntegerType const*>(_varDecl.type().get())) + if (SSAVariable::supportedType(_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 +744,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 +751,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 +829,6 @@ void SMTChecker::defineExpr(Expression const& _e, smt::Expression _value) m_interface->addAssertion(expr(_e) == _value); } -smt::Expression SMTChecker::var(Declaration const& _decl) -{ - solAssert(m_variables.count(&_decl), ""); - return m_variables.at(&_decl); -} - 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..7e7996cf 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. @@ -139,18 +140,12 @@ private: /// 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); - /// Returns the expression corresponding to the AST node. Throws if the expression does not exist. smt::Expression expr(Expression const& _e); /// Creates the expression (value can be arbitrary) 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 +161,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..4e6bcbcb --- /dev/null +++ b/libsolidity/formal/SSAVariable.cpp @@ -0,0 +1,73 @@ +/* + 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_symbolicVar = make_shared<SymbolicIntVariable>(_decl, _interface); + else + { + solAssert(false, ""); + } +} + +bool SSAVariable::supportedType(Type const* _decl) +{ + return dynamic_cast<IntegerType const*>(_decl); +} + +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_symbolicVar->setZeroValue(index()); +} + +void SSAVariable::setUnknownValue() +{ + m_symbolicVar->setUnknownValue(index()); +} diff --git a/libsolidity/formal/SSAVariable.h b/libsolidity/formal/SSAVariable.h new file mode 100644 index 00000000..275e8590 --- /dev/null +++ b/libsolidity/formal/SSAVariable.h @@ -0,0 +1,88 @@ +/* + 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: + /// @param _decl Used to determine the type and forwarded to the symbolic var. + /// @param _interface Forwarded to the symbolic var such that it can give constraints to the solver. + SSAVariable( + Declaration const* _decl, + smt::SolverInterface& _interface + ); + + void resetIndex(); + + /// This function returns the current index of this SSA variable. + int index() const; + /// This function returns the next free index of this SSA variable. + 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); + } + + /// These two functions forward the call to the symbolic var + /// which generates the constraints according to the type. + void setZeroValue(); + void setUnknownValue(); + + /// So far Int is supported. + static bool supportedType(Type const* _decl); + +private: + smt::Expression valueAtSequence(int _seq) const + { + return (*m_symbolicVar)(_seq); + } + + std::shared_ptr<SymbolicVariable> m_symbolicVar = nullptr; + int m_currentSequenceCounter; + /// The next free sequence counter is a shared pointer because we want + /// the copy and the copied to share it. + std::shared_ptr<int> m_nextFreeSequenceCounter; +}; + +} +} diff --git a/libsolidity/formal/SymbolicIntVariable.cpp b/libsolidity/formal/SymbolicIntVariable.cpp new file mode 100644 index 00000000..d08dc155 --- /dev/null +++ b/libsolidity/formal/SymbolicIntVariable.cpp @@ -0,0 +1,56 @@ +/* + 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) +{ + return smt::Expression(_t.minValue()); +} + +smt::Expression SymbolicIntVariable::maxValue(IntegerType const& _t) +{ + return smt::Expression(_t.maxValue()); +} diff --git a/libsolidity/formal/SymbolicIntVariable.h b/libsolidity/formal/SymbolicIntVariable.h new file mode 100644 index 00000000..afa25f1b --- /dev/null +++ b/libsolidity/formal/SymbolicIntVariable.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 <libsolidity/formal/SymbolicVariable.h> + +#include <libsolidity/ast/Types.h> + +namespace dev +{ +namespace solidity +{ + +/** + * Specialization of SymbolicVariable for Integers + */ +class SymbolicIntVariable: public SymbolicVariable +{ +public: + SymbolicIntVariable( + Declaration const* _decl, + smt::SolverInterface& _interface + ); + + /// Sets the var to 0. + void setZeroValue(int _seq); + /// Sets the variable to the full valid value range. + void setUnknownValue(int _seq); + + static smt::Expression minValue(IntegerType const& _t); + static smt::Expression maxValue(IntegerType const& _t); +}; + +} +} diff --git a/libsolidity/formal/SymbolicVariable.cpp b/libsolidity/formal/SymbolicVariable.cpp new file mode 100644 index 00000000..629049ea --- /dev/null +++ b/libsolidity/formal/SymbolicVariable.cpp @@ -0,0 +1,40 @@ +/* + 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..93258250 --- /dev/null +++ b/libsolidity/formal/SymbolicVariable.h @@ -0,0 +1,69 @@ +/* + 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: + SymbolicVariable( + Declaration const* _decl, + smt::SolverInterface& _interface + ); + + smt::Expression operator()(int _seq) const + { + return valueAtSequence(_seq); + } + + std::string uniqueSymbol() const; + + /// Sets the var to the default value of its type. + virtual void setZeroValue(int _seq) = 0; + /// The unknown value is the full range of valid values, + /// and that's sub-type dependent. + 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; +}; + +} +} |