diff options
author | Leonardo <leo@ethereum.org> | 2018-10-18 00:35:48 +0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-10-18 00:35:48 +0800 |
commit | 3db1ce0e144b9d35aa894b5e485c0761ab5aa033 (patch) | |
tree | bbb20e367700c44629747af6ec7b8b6341d62c1d /libsolidity | |
parent | 9d00f710bc9564e2f99dade0200795cfd2ff7fa8 (diff) | |
parent | afe83cc28b2b0f31a00911ed0b540e1beb038736 (diff) | |
download | dexon-solidity-3db1ce0e144b9d35aa894b5e485c0761ab5aa033.tar dexon-solidity-3db1ce0e144b9d35aa894b5e485c0761ab5aa033.tar.gz dexon-solidity-3db1ce0e144b9d35aa894b5e485c0761ab5aa033.tar.bz2 dexon-solidity-3db1ce0e144b9d35aa894b5e485c0761ab5aa033.tar.lz dexon-solidity-3db1ce0e144b9d35aa894b5e485c0761ab5aa033.tar.xz dexon-solidity-3db1ce0e144b9d35aa894b5e485c0761ab5aa033.tar.zst dexon-solidity-3db1ce0e144b9d35aa894b5e485c0761ab5aa033.zip |
Merge pull request #5235 from ethereum/smt_refactor_types
[SMTChecker] Refactoring types
Diffstat (limited to 'libsolidity')
-rw-r--r-- | libsolidity/formal/SMTChecker.cpp | 93 | ||||
-rw-r--r-- | libsolidity/formal/SMTChecker.h | 31 | ||||
-rw-r--r-- | libsolidity/formal/SSAVariable.cpp | 62 | ||||
-rw-r--r-- | libsolidity/formal/SSAVariable.h | 50 | ||||
-rw-r--r-- | libsolidity/formal/SymbolicAddressVariable.cpp | 41 | ||||
-rw-r--r-- | libsolidity/formal/SymbolicAddressVariable.h | 44 | ||||
-rw-r--r-- | libsolidity/formal/SymbolicBoolVariable.cpp | 12 | ||||
-rw-r--r-- | libsolidity/formal/SymbolicBoolVariable.h | 8 | ||||
-rw-r--r-- | libsolidity/formal/SymbolicIntVariable.cpp | 46 | ||||
-rw-r--r-- | libsolidity/formal/SymbolicIntVariable.h | 9 | ||||
-rw-r--r-- | libsolidity/formal/SymbolicTypes.cpp | 110 | ||||
-rw-r--r-- | libsolidity/formal/SymbolicTypes.h | 54 | ||||
-rw-r--r-- | libsolidity/formal/SymbolicVariable.cpp | 7 | ||||
-rw-r--r-- | libsolidity/formal/SymbolicVariable.h | 29 |
14 files changed, 378 insertions, 218 deletions
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 0cb75530..671c2049 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -22,6 +22,7 @@ #include <libsolidity/formal/SSAVariable.h> #include <libsolidity/formal/SymbolicIntVariable.h> #include <libsolidity/formal/VariableUsage.h> +#include <libsolidity/formal/SymbolicTypes.h> #include <libsolidity/interface/ErrorReporter.h> @@ -107,20 +108,18 @@ bool SMTChecker::visit(IfStatement const& _node) if (isRootFunction()) checkBooleanNotConstant(_node.condition(), "Condition is always $VALUE."); - auto countersEndTrue = visitBranch(_node.trueStatement(), expr(_node.condition())); + auto indicesEndTrue = visitBranch(_node.trueStatement(), expr(_node.condition())); vector<VariableDeclaration const*> touchedVariables = m_variableUsage->touchedVariables(_node.trueStatement()); - decltype(countersEndTrue) countersEndFalse; + decltype(indicesEndTrue) indicesEndFalse; if (_node.falseStatement()) { - countersEndFalse = visitBranch(*_node.falseStatement(), !expr(_node.condition())); + indicesEndFalse = visitBranch(*_node.falseStatement(), !expr(_node.condition())); touchedVariables += m_variableUsage->touchedVariables(*_node.falseStatement()); } else - { - countersEndFalse = m_variables; - } + indicesEndFalse = copyVariableIndices(); - mergeVariables(touchedVariables, expr(_node.condition()), countersEndTrue, countersEndFalse); + mergeVariables(touchedVariables, expr(_node.condition()), indicesEndTrue, indicesEndFalse); return false; } @@ -176,7 +175,6 @@ bool SMTChecker::visit(ForStatement const& _node) checkBooleanNotConstant(*_node.condition(), "For loop condition is always $VALUE."); } - VariableSequenceCounters sequenceCountersStart = m_variables; m_interface->push(); if (_node.condition()) m_interface->addAssertion(expr(*_node.condition())); @@ -187,7 +185,6 @@ bool SMTChecker::visit(ForStatement const& _node) m_interface->pop(); m_loopExecutionHappened = true; - std::swap(sequenceCountersStart, m_variables); resetVariables(touchedVariables); @@ -220,7 +217,7 @@ void SMTChecker::endVisit(Assignment const& _assignment) _assignment.location(), "Assertion checker does not yet implement compound assignment." ); - else if (!SSAVariable::isSupportedType(_assignment.annotation().type->category())) + else if (!isSupportedType(_assignment.annotation().type->category())) m_errorReporter.warning( _assignment.location(), "Assertion checker does not yet implement type " + _assignment.annotation().type->toString() @@ -260,14 +257,14 @@ void SMTChecker::endVisit(TupleExpression const& _tuple) void SMTChecker::checkUnderOverflow(smt::Expression _value, IntegerType const& _type, SourceLocation const& _location) { checkCondition( - _value < SymbolicIntVariable::minValue(_type), + _value < minValue(_type), _location, "Underflow (resulting value less than " + formatNumber(_type.minValue()) + ")", "<result>", &_value ); checkCondition( - _value > SymbolicIntVariable::maxValue(_type), + _value > maxValue(_type), _location, "Overflow (resulting value larger than " + formatNumber(_type.maxValue()) + ")", "<result>", @@ -281,7 +278,7 @@ void SMTChecker::endVisit(UnaryOperation const& _op) { case Token::Not: // ! { - solAssert(SSAVariable::isBool(_op.annotation().type->category()), ""); + solAssert(isBool(_op.annotation().type->category()), ""); defineExpr(_op, !expr(_op.subExpression())); break; } @@ -289,7 +286,7 @@ void SMTChecker::endVisit(UnaryOperation const& _op) case Token::Dec: // -- (pre- or postfix) { - solAssert(SSAVariable::isInteger(_op.annotation().type->category()), ""); + solAssert(isInteger(_op.annotation().type->category()), ""); solAssert(_op.subExpression().annotation().lValueRequested, ""); if (Identifier const* identifier = dynamic_cast<Identifier const*>(&_op.subExpression())) { @@ -461,7 +458,7 @@ void SMTChecker::endVisit(Identifier const& _identifier) { // Will be translated as part of the node that requested the lvalue. } - else if (SSAVariable::isSupportedType(_identifier.annotation().type->category())) + else if (isSupportedType(_identifier.annotation().type->category())) { if (VariableDeclaration const* decl = dynamic_cast<VariableDeclaration const*>(_identifier.annotation().referencedDeclaration)) defineExpr(_identifier, currentValue(*decl)); @@ -567,13 +564,13 @@ void SMTChecker::arithmeticOperation(BinaryOperation const& _op) void SMTChecker::compareOperation(BinaryOperation const& _op) { solAssert(_op.annotation().commonType, ""); - if (SSAVariable::isSupportedType(_op.annotation().commonType->category())) + if (isSupportedType(_op.annotation().commonType->category())) { smt::Expression left(expr(_op.leftExpression())); smt::Expression right(expr(_op.rightExpression())); Token::Value op = _op.getOperator(); shared_ptr<smt::Expression> value; - if (SSAVariable::isInteger(_op.annotation().commonType->category())) + if (isNumber(_op.annotation().commonType->category())) { value = make_shared<smt::Expression>( op == Token::Equal ? (left == right) : @@ -586,7 +583,7 @@ void SMTChecker::compareOperation(BinaryOperation const& _op) } else // Bool { - solUnimplementedAssert(SSAVariable::isBool(_op.annotation().commonType->category()), "Operation not yet supported"); + solUnimplementedAssert(isBool(_op.annotation().commonType->category()), "Operation not yet supported"); value = make_shared<smt::Expression>( op == Token::Equal ? (left == right) : /*op == Token::NotEqual*/ (left != right) @@ -649,24 +646,22 @@ void SMTChecker::assignment(VariableDeclaration const& _variable, smt::Expressio m_interface->addAssertion(newValue(_variable) == _value); } -SMTChecker::VariableSequenceCounters SMTChecker::visitBranch(Statement const& _statement, smt::Expression _condition) +SMTChecker::VariableIndices SMTChecker::visitBranch(Statement const& _statement, smt::Expression _condition) { return visitBranch(_statement, &_condition); } -SMTChecker::VariableSequenceCounters SMTChecker::visitBranch(Statement const& _statement, smt::Expression const* _condition) +SMTChecker::VariableIndices SMTChecker::visitBranch(Statement const& _statement, smt::Expression const* _condition) { - VariableSequenceCounters beforeVars = m_variables; - + auto indicesBeforeBranch = copyVariableIndices(); if (_condition) pushPathCondition(*_condition); _statement.accept(*this); if (_condition) popPathCondition(); - - std::swap(m_variables, beforeVars); - - return beforeVars; + auto indicesAfterBranch = copyVariableIndices(); + resetVariableIndices(indicesBeforeBranch); + return indicesAfterBranch; } void SMTChecker::checkCondition( @@ -899,19 +894,19 @@ void SMTChecker::resetVariables(vector<VariableDeclaration const*> _variables) } } -void SMTChecker::mergeVariables(vector<VariableDeclaration const*> const& _variables, smt::Expression const& _condition, VariableSequenceCounters const& _countersEndTrue, VariableSequenceCounters const& _countersEndFalse) +void SMTChecker::mergeVariables(vector<VariableDeclaration const*> const& _variables, smt::Expression const& _condition, VariableIndices const& _indicesEndTrue, VariableIndices const& _indicesEndFalse) { set<VariableDeclaration const*> uniqueVars(_variables.begin(), _variables.end()); for (auto const* decl: uniqueVars) { - solAssert(_countersEndTrue.count(decl) && _countersEndFalse.count(decl), ""); - int trueCounter = _countersEndTrue.at(decl).index(); - int falseCounter = _countersEndFalse.at(decl).index(); - solAssert(trueCounter != falseCounter, ""); + solAssert(_indicesEndTrue.count(decl) && _indicesEndFalse.count(decl), ""); + int trueIndex = _indicesEndTrue.at(decl); + int falseIndex = _indicesEndFalse.at(decl); + solAssert(trueIndex != falseIndex, ""); m_interface->addAssertion(newValue(*decl) == smt::Expression::ite( _condition, - valueAtSequence(*decl, trueCounter), - valueAtSequence(*decl, falseCounter)) + valueAtIndex(*decl, trueIndex), + valueAtIndex(*decl, falseIndex)) ); } } @@ -921,10 +916,11 @@ bool SMTChecker::createVariable(VariableDeclaration const& _varDecl) // This might be the case for multiple calls to the same function. if (hasVariable(_varDecl)) return true; - else if (SSAVariable::isSupportedType(_varDecl.type()->category())) + auto const& type = _varDecl.type(); + if (isSupportedType(type->category())) { solAssert(m_variables.count(&_varDecl) == 0, ""); - m_variables.emplace(&_varDecl, SSAVariable(*_varDecl.type(), _varDecl.name() + "_" + to_string(_varDecl.id()), *m_interface)); + m_variables.emplace(&_varDecl, newSymbolicVariable(*type, _varDecl.name() + "_" + to_string(_varDecl.id()), *m_interface)); return true; } else @@ -950,32 +946,31 @@ bool SMTChecker::knownVariable(VariableDeclaration const& _decl) smt::Expression SMTChecker::currentValue(VariableDeclaration const& _decl) { solAssert(knownVariable(_decl), ""); - return m_variables.at(&_decl)(); + return m_variables.at(&_decl)->currentValue(); } -smt::Expression SMTChecker::valueAtSequence(VariableDeclaration const& _decl, int _sequence) +smt::Expression SMTChecker::valueAtIndex(VariableDeclaration const& _decl, int _index) { solAssert(knownVariable(_decl), ""); - return m_variables.at(&_decl)(_sequence); + return m_variables.at(&_decl)->valueAtIndex(_index); } smt::Expression SMTChecker::newValue(VariableDeclaration const& _decl) { solAssert(knownVariable(_decl), ""); - ++m_variables.at(&_decl); - return m_variables.at(&_decl)(); + return m_variables.at(&_decl)->increaseIndex(); } void SMTChecker::setZeroValue(VariableDeclaration const& _decl) { solAssert(knownVariable(_decl), ""); - m_variables.at(&_decl).setZeroValue(); + m_variables.at(&_decl)->setZeroValue(); } void SMTChecker::setUnknownValue(VariableDeclaration const& _decl) { solAssert(knownVariable(_decl), ""); - m_variables.at(&_decl).setUnknownValue(); + m_variables.at(&_decl)->setUnknownValue(); } smt::Expression SMTChecker::expr(Expression const& _e) @@ -1074,3 +1069,17 @@ bool SMTChecker::visitedFunction(FunctionDefinition const* _funDef) { return contains(m_functionPath, _funDef); } + +SMTChecker::VariableIndices SMTChecker::copyVariableIndices() +{ + VariableIndices indices; + for (auto const& var: m_variables) + indices.emplace(var.first, var.second->index()); + return indices; +} + +void SMTChecker::resetVariableIndices(VariableIndices const& _indices) +{ + for (auto const& var: _indices) + m_variables.at(var.first)->index() = var.second; +} diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index bef6ea0c..0b078556 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -19,14 +19,14 @@ #include <libsolidity/formal/SolverInterface.h> - -#include <libsolidity/formal/SSAVariable.h> +#include <libsolidity/formal/SymbolicVariable.h> #include <libsolidity/ast/ASTVisitor.h> #include <libsolidity/interface/ReadFile.h> #include <map> +#include <unordered_map> #include <string> #include <vector> @@ -86,13 +86,13 @@ private: void assignment(VariableDeclaration const& _variable, smt::Expression const& _value, SourceLocation const& _location); /// Maps a variable to an SSA index. - using VariableSequenceCounters = std::map<VariableDeclaration const*, SSAVariable>; + using VariableIndices = std::unordered_map<VariableDeclaration const*, int>; /// 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. - /// @returns the variable sequence counter after visiting the branch. - VariableSequenceCounters visitBranch(Statement const& _statement, smt::Expression const* _condition = nullptr); - VariableSequenceCounters visitBranch(Statement const& _statement, smt::Expression _condition); + /// @returns the variable indices after visiting the branch. + VariableIndices visitBranch(Statement const& _statement, smt::Expression const* _condition = nullptr); + VariableIndices visitBranch(Statement const& _statement, smt::Expression _condition); /// Check that a condition can be satisfied. void checkCondition( @@ -125,7 +125,7 @@ private: /// Given two different branches and the touched variables, /// merge the touched variables into after-branch ite variables /// using the branch condition as guard. - void mergeVariables(std::vector<VariableDeclaration const*> const& _variables, smt::Expression const& _condition, VariableSequenceCounters const& _countersEndTrue, VariableSequenceCounters const& _countersEndFalse); + void mergeVariables(std::vector<VariableDeclaration const*> const& _variables, smt::Expression const& _condition, VariableIndices const& _indicesEndTrue, VariableIndices const& _indicesEndFalse); /// Tries to create an uninitialized variable and returns true on success. /// This fails if the type is not supported. bool createVariable(VariableDeclaration const& _varDecl); @@ -133,16 +133,16 @@ private: static std::string uniqueSymbol(Expression const& _expr); /// @returns true if _delc is a variable that is known at the current point, i.e. - /// has a valid sequence number + /// has a valid index bool knownVariable(VariableDeclaration const& _decl); /// @returns an expression denoting the value of the variable declared in @a _decl /// at the current point. smt::Expression currentValue(VariableDeclaration const& _decl); /// @returns an expression denoting the value of the variable declared in @a _decl - /// at the given sequence point. Does not ensure that this sequence point exists. - smt::Expression valueAtSequence(VariableDeclaration const& _decl, int _sequence); - /// Allocates a new sequence number for the declaration, updates the current - /// sequence number to this value and returns the expression. + /// at the given index. Does not ensure that this index exists. + smt::Expression valueAtIndex(VariableDeclaration const& _decl, int _index); + /// Allocates a new index for the declaration, updates the current + /// index to this value and returns the expression. smt::Expression newValue(VariableDeclaration const& _decl); /// Sets the value of the declaration to zero. @@ -176,13 +176,18 @@ private: /// Checks if VariableDeclaration was seen. bool hasVariable(VariableDeclaration const& _e) const; + /// Copy the SSA indices of m_variables. + VariableIndices copyVariableIndices(); + /// Resets the variable indices. + void resetVariableIndices(VariableIndices const& _indices); + std::shared_ptr<smt::SolverInterface> m_interface; std::shared_ptr<VariableUsage> m_variableUsage; bool m_loopExecutionHappened = false; /// An Expression may have multiple smt::Expression due to /// repeated calls to the same function. std::multimap<Expression const*, smt::Expression> m_expressions; - std::map<VariableDeclaration const*, SSAVariable> m_variables; + std::unordered_map<VariableDeclaration const*, std::shared_ptr<SymbolicVariable>> m_variables; std::vector<smt::Expression> m_pathConditions; ErrorReporter& m_errorReporter; diff --git a/libsolidity/formal/SSAVariable.cpp b/libsolidity/formal/SSAVariable.cpp index ceeea49a..dbc58664 100644 --- a/libsolidity/formal/SSAVariable.cpp +++ b/libsolidity/formal/SSAVariable.cpp @@ -17,71 +17,17 @@ #include <libsolidity/formal/SSAVariable.h> -#include <libsolidity/formal/SymbolicBoolVariable.h> -#include <libsolidity/formal/SymbolicIntVariable.h> - -#include <libsolidity/ast/AST.h> - using namespace std; -using namespace dev; using namespace dev::solidity; -SSAVariable::SSAVariable( - Type const& _type, - string const& _uniqueName, - smt::SolverInterface& _interface -) +SSAVariable::SSAVariable() { resetIndex(); - - if (isInteger(_type.category())) - m_symbolicVar = make_shared<SymbolicIntVariable>(_type, _uniqueName, _interface); - else if (isBool(_type.category())) - m_symbolicVar = make_shared<SymbolicBoolVariable>(_type, _uniqueName, _interface); - else - { - solAssert(false, ""); - } -} - -bool SSAVariable::isSupportedType(Type::Category _category) -{ - return isInteger(_category) || isBool(_category); -} - -bool SSAVariable::isInteger(Type::Category _category) -{ - return _category == Type::Category::Integer || _category == Type::Category::Address; -} - -bool SSAVariable::isBool(Type::Category _category) -{ - return _category == Type::Category::Bool; } 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()); + m_currentIndex = 0; + m_nextFreeIndex.reset (new int); + *m_nextFreeIndex = 1; } diff --git a/libsolidity/formal/SSAVariable.h b/libsolidity/formal/SSAVariable.h index f4a4e93e..d357740d 100644 --- a/libsolidity/formal/SSAVariable.h +++ b/libsolidity/formal/SSAVariable.h @@ -17,8 +17,6 @@ #pragma once -#include <libsolidity/formal/SymbolicVariable.h> - #include <memory> namespace dev @@ -32,57 +30,23 @@ namespace solidity class SSAVariable { public: - /// @param _type Forwarded to the symbolic var. - /// @param _interface Forwarded to the symbolic var such that it can give constraints to the solver. - SSAVariable( - Type const& _type, - std::string const& _uniqueName, - smt::SolverInterface& _interface - ); - + SSAVariable(); 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 index() const { return m_currentIndex; } + int& index() { return m_currentIndex; } int operator++() { - return m_currentSequenceCounter = (*m_nextFreeSequenceCounter)++; + return m_currentIndex = (*m_nextFreeIndex)++; } - 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 and Bool are supported. - static bool isSupportedType(Type::Category _category); - static bool isInteger(Type::Category _category); - static bool isBool(Type::Category _category); - 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 + int m_currentIndex; + /// The next free index is a shared pointer because we want /// the copy and the copied to share it. - std::shared_ptr<int> m_nextFreeSequenceCounter; + std::shared_ptr<int> m_nextFreeIndex; }; } diff --git a/libsolidity/formal/SymbolicAddressVariable.cpp b/libsolidity/formal/SymbolicAddressVariable.cpp new file mode 100644 index 00000000..68b95080 --- /dev/null +++ b/libsolidity/formal/SymbolicAddressVariable.cpp @@ -0,0 +1,41 @@ +/* + 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/SymbolicAddressVariable.h> + +#include <libsolidity/formal/SymbolicTypes.h> + +using namespace std; +using namespace dev; +using namespace dev::solidity; + +SymbolicAddressVariable::SymbolicAddressVariable( + Type const& _type, + string const& _uniqueName, + smt::SolverInterface& _interface +): + SymbolicIntVariable(_type, _uniqueName, _interface) +{ + solAssert(isAddress(_type.category()), ""); +} + +void SymbolicAddressVariable::setUnknownValue() +{ + IntegerType intType{160}; + m_interface.addAssertion(currentValue() >= minValue(intType)); + m_interface.addAssertion(currentValue() <= maxValue(intType)); +} diff --git a/libsolidity/formal/SymbolicAddressVariable.h b/libsolidity/formal/SymbolicAddressVariable.h new file mode 100644 index 00000000..4a0f2361 --- /dev/null +++ b/libsolidity/formal/SymbolicAddressVariable.h @@ -0,0 +1,44 @@ +/* + 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/SymbolicIntVariable.h> + +namespace dev +{ +namespace solidity +{ + +/** + * Specialization of SymbolicVariable for Address + */ +class SymbolicAddressVariable: public SymbolicIntVariable +{ +public: + SymbolicAddressVariable( + Type const& _type, + std::string const& _uniqueName, + smt::SolverInterface& _interface + ); + + /// Sets the variable to the full valid value range. + void setUnknownValue(); +}; + +} +} diff --git a/libsolidity/formal/SymbolicBoolVariable.cpp b/libsolidity/formal/SymbolicBoolVariable.cpp index 5e5aec8f..9c41ca9d 100644 --- a/libsolidity/formal/SymbolicBoolVariable.cpp +++ b/libsolidity/formal/SymbolicBoolVariable.cpp @@ -17,8 +17,6 @@ #include <libsolidity/formal/SymbolicBoolVariable.h> -#include <libsolidity/ast/AST.h> - using namespace std; using namespace dev; using namespace dev::solidity; @@ -33,16 +31,16 @@ SymbolicBoolVariable::SymbolicBoolVariable( solAssert(_type.category() == Type::Category::Bool, ""); } -smt::Expression SymbolicBoolVariable::valueAtSequence(int _seq) const +smt::Expression SymbolicBoolVariable::valueAtIndex(int _index) const { - return m_interface.newBool(uniqueSymbol(_seq)); + return m_interface.newBool(uniqueSymbol(_index)); } -void SymbolicBoolVariable::setZeroValue(int _seq) +void SymbolicBoolVariable::setZeroValue() { - m_interface.addAssertion(valueAtSequence(_seq) == smt::Expression(false)); + m_interface.addAssertion(currentValue() == smt::Expression(false)); } -void SymbolicBoolVariable::setUnknownValue(int) +void SymbolicBoolVariable::setUnknownValue() { } diff --git a/libsolidity/formal/SymbolicBoolVariable.h b/libsolidity/formal/SymbolicBoolVariable.h index 33ac9061..85e41b3b 100644 --- a/libsolidity/formal/SymbolicBoolVariable.h +++ b/libsolidity/formal/SymbolicBoolVariable.h @@ -37,12 +37,12 @@ public: ); /// Sets the var to false. - void setZeroValue(int _seq); - /// Does nothing since the SMT solver already knows the valid values. - void setUnknownValue(int _seq); + void setZeroValue(); + /// Does nothing since the SMT solver already knows the valid values for Bool. + void setUnknownValue(); protected: - smt::Expression valueAtSequence(int _seq) const; + smt::Expression valueAtIndex(int _index) const; }; } diff --git a/libsolidity/formal/SymbolicIntVariable.cpp b/libsolidity/formal/SymbolicIntVariable.cpp index 0adb9d09..cf1a7486 100644 --- a/libsolidity/formal/SymbolicIntVariable.cpp +++ b/libsolidity/formal/SymbolicIntVariable.cpp @@ -17,6 +17,8 @@ #include <libsolidity/formal/SymbolicIntVariable.h> +#include <libsolidity/formal/SymbolicTypes.h> + using namespace std; using namespace dev; using namespace dev::solidity; @@ -28,47 +30,23 @@ SymbolicIntVariable::SymbolicIntVariable( ): SymbolicVariable(_type, _uniqueName, _interface) { - solAssert( - _type.category() == Type::Category::Integer || - _type.category() == Type::Category::Address, - "" - ); -} - -smt::Expression SymbolicIntVariable::valueAtSequence(int _seq) const -{ - return m_interface.newInteger(uniqueSymbol(_seq)); -} - -void SymbolicIntVariable::setZeroValue(int _seq) -{ - m_interface.addAssertion(valueAtSequence(_seq) == 0); + solAssert(isNumber(_type.category()), ""); } -void SymbolicIntVariable::setUnknownValue(int _seq) +smt::Expression SymbolicIntVariable::valueAtIndex(int _index) const { - if (m_type.category() == Type::Category::Integer) - { - auto intType = dynamic_cast<IntegerType const*>(&m_type); - solAssert(intType, ""); - m_interface.addAssertion(valueAtSequence(_seq) >= minValue(*intType)); - m_interface.addAssertion(valueAtSequence(_seq) <= maxValue(*intType)); - } - else - { - solAssert(m_type.category() == Type::Category::Address, ""); - IntegerType addrType{160}; - m_interface.addAssertion(valueAtSequence(_seq) >= minValue(addrType)); - m_interface.addAssertion(valueAtSequence(_seq) <= maxValue(addrType)); - } + return m_interface.newInteger(uniqueSymbol(_index)); } -smt::Expression SymbolicIntVariable::minValue(IntegerType const& _t) +void SymbolicIntVariable::setZeroValue() { - return smt::Expression(_t.minValue()); + m_interface.addAssertion(currentValue() == 0); } -smt::Expression SymbolicIntVariable::maxValue(IntegerType const& _t) +void SymbolicIntVariable::setUnknownValue() { - return smt::Expression(_t.maxValue()); + auto intType = dynamic_cast<IntegerType const*>(&m_type); + solAssert(intType, ""); + m_interface.addAssertion(currentValue() >= minValue(*intType)); + m_interface.addAssertion(currentValue() <= maxValue(*intType)); } diff --git a/libsolidity/formal/SymbolicIntVariable.h b/libsolidity/formal/SymbolicIntVariable.h index 92eeb13d..110ebb09 100644 --- a/libsolidity/formal/SymbolicIntVariable.h +++ b/libsolidity/formal/SymbolicIntVariable.h @@ -37,15 +37,12 @@ public: ); /// Sets the var to 0. - void setZeroValue(int _seq); + void setZeroValue(); /// 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); + virtual void setUnknownValue(); protected: - smt::Expression valueAtSequence(int _seq) const; + smt::Expression valueAtIndex(int _index) const; }; } diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp new file mode 100644 index 00000000..2d993865 --- /dev/null +++ b/libsolidity/formal/SymbolicTypes.cpp @@ -0,0 +1,110 @@ +/* + 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/SymbolicTypes.h> + +#include <libsolidity/formal/SymbolicBoolVariable.h> +#include <libsolidity/formal/SymbolicIntVariable.h> +#include <libsolidity/formal/SymbolicAddressVariable.h> + +#include <libsolidity/ast/Types.h> + +#include <memory> + +using namespace std; +using namespace dev::solidity; + +bool dev::solidity::isSupportedType(Type::Category _category) +{ + return isInteger(_category) || + isAddress(_category) || + isBool(_category); +} + +shared_ptr<SymbolicVariable> dev::solidity::newSymbolicVariable( + Type const& _type, + std::string const& _uniqueName, + smt::SolverInterface& _solver +) +{ + if (!isSupportedType(_type)) + return nullptr; + if (isBool(_type.category())) + return make_shared<SymbolicBoolVariable>(_type, _uniqueName, _solver); + else if (isInteger(_type.category())) + return make_shared<SymbolicIntVariable>(_type, _uniqueName, _solver); + else if (isAddress(_type.category())) + return make_shared<SymbolicAddressVariable>(_type, _uniqueName, _solver); + else + solAssert(false, ""); +} + +bool dev::solidity::isSupportedType(Type const& _type) +{ + return isSupportedType(_type.category()); +} + +bool dev::solidity::isInteger(Type::Category _category) +{ + return _category == Type::Category::Integer; +} + +bool dev::solidity::isInteger(Type const& _type) +{ + return isInteger(_type.category()); +} + +bool dev::solidity::isAddress(Type::Category _category) +{ + return _category == Type::Category::Address; +} + +bool dev::solidity::isAddress(Type const& _type) +{ + return isAddress(_type.category()); +} + +bool dev::solidity::isNumber(Type::Category _category) +{ + return isInteger(_category) || + isAddress(_category); +} + +bool dev::solidity::isNumber(Type const& _type) +{ + return isNumber(_type.category()); +} + +bool dev::solidity::isBool(Type::Category _category) +{ + return _category == Type::Category::Bool; +} + +bool dev::solidity::isBool(Type const& _type) +{ + return isBool(_type.category()); +} + +smt::Expression dev::solidity::minValue(IntegerType const& _type) +{ + return smt::Expression(_type.minValue()); +} + +smt::Expression dev::solidity::maxValue(IntegerType const& _type) +{ + return smt::Expression(_type.maxValue()); +} diff --git a/libsolidity/formal/SymbolicTypes.h b/libsolidity/formal/SymbolicTypes.h new file mode 100644 index 00000000..77822fed --- /dev/null +++ b/libsolidity/formal/SymbolicTypes.h @@ -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/>. +*/ + +#pragma once + +#include <libsolidity/formal/SolverInterface.h> +#include <libsolidity/formal/SymbolicVariable.h> + +#include <libsolidity/ast/AST.h> +#include <libsolidity/ast/Types.h> + +namespace dev +{ +namespace solidity +{ + +/// So far int, bool and address are supported. +/// Returns true if type is supported. +bool isSupportedType(Type::Category _category); +bool isSupportedType(Type const& _type); + +bool isInteger(Type::Category _category); +bool isInteger(Type const& _type); + +bool isAddress(Type::Category _category); +bool isAddress(Type const& _type); + +bool isNumber(Type::Category _category); +bool isNumber(Type const& _type); + +bool isBool(Type::Category _category); +bool isBool(Type const& _type); + +std::shared_ptr<SymbolicVariable> newSymbolicVariable(Type const& _type, std::string const& _uniqueName, smt::SolverInterface& _solver); + +smt::Expression minValue(IntegerType const& _type); +smt::Expression maxValue(IntegerType const& _type); + +} +} diff --git a/libsolidity/formal/SymbolicVariable.cpp b/libsolidity/formal/SymbolicVariable.cpp index afbc01ba..c042ec48 100644 --- a/libsolidity/formal/SymbolicVariable.cpp +++ b/libsolidity/formal/SymbolicVariable.cpp @@ -30,13 +30,14 @@ SymbolicVariable::SymbolicVariable( ): m_type(_type), m_uniqueName(_uniqueName), - m_interface(_interface) + m_interface(_interface), + m_ssa(make_shared<SSAVariable>()) { } -string SymbolicVariable::uniqueSymbol(int _seq) const +string SymbolicVariable::uniqueSymbol(int _index) const { - return m_uniqueName + "_" + to_string(_seq); + return m_uniqueName + "_" + to_string(_index); } diff --git a/libsolidity/formal/SymbolicVariable.h b/libsolidity/formal/SymbolicVariable.h index 977515f8..417e1f92 100644 --- a/libsolidity/formal/SymbolicVariable.h +++ b/libsolidity/formal/SymbolicVariable.h @@ -17,6 +17,8 @@ #pragma once +#include <libsolidity/formal/SSAVariable.h> + #include <libsolidity/formal/SolverInterface.h> #include <libsolidity/ast/Types.h> @@ -43,25 +45,36 @@ public: ); virtual ~SymbolicVariable() = default; - smt::Expression operator()(int _seq) const + smt::Expression currentValue() const + { + return valueAtIndex(m_ssa->index()); + } + + virtual smt::Expression valueAtIndex(int _index) const = 0; + + smt::Expression increaseIndex() { - return valueAtSequence(_seq); + ++(*m_ssa); + return currentValue(); } - std::string uniqueSymbol(int _seq) const; + int index() const { return m_ssa->index(); } + int& index() { return m_ssa->index(); } /// 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; + /// Inherited types must implement. + virtual void setZeroValue() = 0; + /// The unknown value is the full range of valid values. + /// It is sub-type dependent, but not mandatory. + virtual void setUnknownValue() {} protected: - virtual smt::Expression valueAtSequence(int _seq) const = 0; + std::string uniqueSymbol(int _index) const; Type const& m_type; std::string m_uniqueName; smt::SolverInterface& m_interface; + std::shared_ptr<SSAVariable> m_ssa = nullptr; }; } |