From ec39fdcb3c6b3d5eb07ea6768fb3926fe54dc47e Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Mon, 15 Oct 2018 17:32:17 +0200 Subject: [SMTChecker] Refactoring types --- libsolidity/formal/SMTChecker.cpp | 65 +++++++++++++++----------- libsolidity/formal/SMTChecker.h | 13 ++++-- libsolidity/formal/SSAVariable.cpp | 56 +--------------------- libsolidity/formal/SSAVariable.h | 42 ++--------------- libsolidity/formal/SymbolicBoolVariable.cpp | 8 ++-- libsolidity/formal/SymbolicBoolVariable.h | 6 +-- libsolidity/formal/SymbolicIntVariable.cpp | 14 +++--- libsolidity/formal/SymbolicIntVariable.h | 4 +- libsolidity/formal/SymbolicTypes.cpp | 72 +++++++++++++++++++++++++++++ libsolidity/formal/SymbolicTypes.h | 45 ++++++++++++++++++ libsolidity/formal/SymbolicVariable.cpp | 3 +- libsolidity/formal/SymbolicVariable.h | 24 +++++++--- 12 files changed, 202 insertions(+), 150 deletions(-) create mode 100644 libsolidity/formal/SymbolicTypes.cpp create mode 100644 libsolidity/formal/SymbolicTypes.h diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 0cb75530..d84d6794 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -22,6 +22,7 @@ #include #include #include +#include #include @@ -116,9 +117,7 @@ bool SMTChecker::visit(IfStatement const& _node) touchedVariables += m_variableUsage->touchedVariables(*_node.falseStatement()); } else - { - countersEndFalse = m_variables; - } + countersEndFalse = copyVariableSequenceCounters(); mergeVariables(touchedVariables, expr(_node.condition()), countersEndTrue, countersEndFalse); @@ -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() @@ -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(&_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(_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 value; - if (SSAVariable::isInteger(_op.annotation().commonType->category())) + if (isInteger(_op.annotation().commonType->category())) { value = make_shared( 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( op == Token::Equal ? (left == right) : /*op == Token::NotEqual*/ (left != right) @@ -656,17 +653,15 @@ SMTChecker::VariableSequenceCounters SMTChecker::visitBranch(Statement const& _s SMTChecker::VariableSequenceCounters SMTChecker::visitBranch(Statement const& _statement, smt::Expression const* _condition) { - VariableSequenceCounters beforeVars = m_variables; - + auto countersBeforeBranch = copyVariableSequenceCounters(); if (_condition) pushPathCondition(*_condition); _statement.accept(*this); if (_condition) popPathCondition(); - - std::swap(m_variables, beforeVars); - - return beforeVars; + auto countersAfterBranch = copyVariableSequenceCounters(); + resetVariableCounters(countersBeforeBranch); + return countersAfterBranch; } void SMTChecker::checkCondition( @@ -905,8 +900,8 @@ void SMTChecker::mergeVariables(vector const& _varia for (auto const* decl: uniqueVars) { solAssert(_countersEndTrue.count(decl) && _countersEndFalse.count(decl), ""); - int trueCounter = _countersEndTrue.at(decl).index(); - int falseCounter = _countersEndFalse.at(decl).index(); + int trueCounter = _countersEndTrue.at(decl); + int falseCounter = _countersEndFalse.at(decl); solAssert(trueCounter != falseCounter, ""); m_interface->addAssertion(newValue(*decl) == smt::Expression::ite( _condition, @@ -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)->current(); } smt::Expression SMTChecker::valueAtSequence(VariableDeclaration const& _decl, int _sequence) { solAssert(knownVariable(_decl), ""); - return m_variables.at(&_decl)(_sequence); + return m_variables.at(&_decl)->valueAtSequence(_sequence); } smt::Expression SMTChecker::newValue(VariableDeclaration const& _decl) { solAssert(knownVariable(_decl), ""); - ++m_variables.at(&_decl); - return m_variables.at(&_decl)(); + return m_variables.at(&_decl)->increase(); } 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::VariableSequenceCounters SMTChecker::copyVariableSequenceCounters() +{ + VariableSequenceCounters counters; + for (auto var: m_variables) + counters.emplace(var.first, var.second->index()); + return counters; +} + +void SMTChecker::resetVariableCounters(VariableSequenceCounters const& _counters) +{ + for (auto var: _counters) + m_variables.at(var.first)->index() = var.second; +} diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index bef6ea0c..ae697204 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -19,14 +19,14 @@ #include - -#include +#include #include #include #include +#include #include #include @@ -86,7 +86,7 @@ private: void assignment(VariableDeclaration const& _variable, smt::Expression const& _value, SourceLocation const& _location); /// Maps a variable to an SSA index. - using VariableSequenceCounters = std::map; + using VariableSequenceCounters = std::unordered_map; /// 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. @@ -176,13 +176,18 @@ private: /// Checks if VariableDeclaration was seen. bool hasVariable(VariableDeclaration const& _e) const; + /// Copy the SSA indices of m_variables. + VariableSequenceCounters copyVariableSequenceCounters(); + /// Resets the variable counters. + void resetVariableCounters(VariableSequenceCounters const& _counters); + std::shared_ptr m_interface; std::shared_ptr m_variableUsage; bool m_loopExecutionHappened = false; /// An Expression may have multiple smt::Expression due to /// repeated calls to the same function. std::multimap m_expressions; - std::map m_variables; + std::unordered_map> m_variables; std::vector m_pathConditions; ErrorReporter& m_errorReporter; diff --git a/libsolidity/formal/SSAVariable.cpp b/libsolidity/formal/SSAVariable.cpp index ceeea49a..aeb12c9f 100644 --- a/libsolidity/formal/SSAVariable.cpp +++ b/libsolidity/formal/SSAVariable.cpp @@ -17,46 +17,12 @@ #include -#include -#include - -#include - 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(_type, _uniqueName, _interface); - else if (isBool(_type.category())) - m_symbolicVar = make_shared(_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() @@ -65,23 +31,3 @@ void SSAVariable::resetIndex() 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 index f4a4e93e..f8317b79 100644 --- a/libsolidity/formal/SSAVariable.h +++ b/libsolidity/formal/SSAVariable.h @@ -17,8 +17,6 @@ #pragma once -#include - #include namespace dev @@ -32,53 +30,19 @@ 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_currentSequenceCounter; } + int& index() { return m_currentSequenceCounter; } 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 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 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. diff --git a/libsolidity/formal/SymbolicBoolVariable.cpp b/libsolidity/formal/SymbolicBoolVariable.cpp index 5e5aec8f..f65ecd37 100644 --- a/libsolidity/formal/SymbolicBoolVariable.cpp +++ b/libsolidity/formal/SymbolicBoolVariable.cpp @@ -17,8 +17,6 @@ #include -#include - using namespace std; using namespace dev; using namespace dev::solidity; @@ -38,11 +36,11 @@ smt::Expression SymbolicBoolVariable::valueAtSequence(int _seq) const return m_interface.newBool(uniqueSymbol(_seq)); } -void SymbolicBoolVariable::setZeroValue(int _seq) +void SymbolicBoolVariable::setZeroValue() { - m_interface.addAssertion(valueAtSequence(_seq) == smt::Expression(false)); + m_interface.addAssertion(current() == smt::Expression(false)); } -void SymbolicBoolVariable::setUnknownValue(int) +void SymbolicBoolVariable::setUnknownValue() { } diff --git a/libsolidity/formal/SymbolicBoolVariable.h b/libsolidity/formal/SymbolicBoolVariable.h index 33ac9061..3d735889 100644 --- a/libsolidity/formal/SymbolicBoolVariable.h +++ b/libsolidity/formal/SymbolicBoolVariable.h @@ -37,9 +37,9 @@ 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; diff --git a/libsolidity/formal/SymbolicIntVariable.cpp b/libsolidity/formal/SymbolicIntVariable.cpp index 0adb9d09..877495bd 100644 --- a/libsolidity/formal/SymbolicIntVariable.cpp +++ b/libsolidity/formal/SymbolicIntVariable.cpp @@ -40,26 +40,26 @@ smt::Expression SymbolicIntVariable::valueAtSequence(int _seq) const return m_interface.newInteger(uniqueSymbol(_seq)); } -void SymbolicIntVariable::setZeroValue(int _seq) +void SymbolicIntVariable::setZeroValue() { - m_interface.addAssertion(valueAtSequence(_seq) == 0); + m_interface.addAssertion(current() == 0); } -void SymbolicIntVariable::setUnknownValue(int _seq) +void SymbolicIntVariable::setUnknownValue() { if (m_type.category() == Type::Category::Integer) { auto intType = dynamic_cast(&m_type); solAssert(intType, ""); - m_interface.addAssertion(valueAtSequence(_seq) >= minValue(*intType)); - m_interface.addAssertion(valueAtSequence(_seq) <= maxValue(*intType)); + m_interface.addAssertion(current() >= minValue(*intType)); + m_interface.addAssertion(current() <= 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)); + m_interface.addAssertion(current() >= minValue(addrType)); + m_interface.addAssertion(current() <= maxValue(addrType)); } } diff --git a/libsolidity/formal/SymbolicIntVariable.h b/libsolidity/formal/SymbolicIntVariable.h index 92eeb13d..3b0c0311 100644 --- a/libsolidity/formal/SymbolicIntVariable.h +++ b/libsolidity/formal/SymbolicIntVariable.h @@ -37,9 +37,9 @@ 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); + void setUnknownValue(); static smt::Expression minValue(IntegerType const& _t); static smt::Expression maxValue(IntegerType const& _t); diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp new file mode 100644 index 00000000..deb52ac1 --- /dev/null +++ b/libsolidity/formal/SymbolicTypes.cpp @@ -0,0 +1,72 @@ +/* + 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 . +*/ + +#include + +#include +#include + +#include + +#include + +using namespace std; +using namespace dev::solidity; + +bool dev::solidity::isSupportedType(Type::Category _category) +{ + return isInteger(_category) || isBool(_category); +} + +bool dev::solidity::isSupportedType(Type const& _type) +{ + return isSupportedType(_type.category()); +} + +bool dev::solidity::isInteger(Type::Category _category) +{ + return _category == Type::Category::Integer || _category == Type::Category::Address; +} + +bool dev::solidity::isInteger(Type const& _type) +{ + return isInteger(_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()); +} + +shared_ptr 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(_type, _uniqueName, _solver); + else if (isInteger(_type.category())) + return make_shared(_type, _uniqueName, _solver); + else + solAssert(false, ""); +} + + diff --git a/libsolidity/formal/SymbolicTypes.h b/libsolidity/formal/SymbolicTypes.h new file mode 100644 index 00000000..f9df6853 --- /dev/null +++ b/libsolidity/formal/SymbolicTypes.h @@ -0,0 +1,45 @@ +/* + 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 . +*/ + +#pragma once + +#include +#include + +#include +#include + +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 isBool(Type::Category _category); +bool isBool(Type const& _type); + +std::shared_ptr newSymbolicVariable(Type const& _type, std::string const& _uniqueName, smt::SolverInterface& _solver); + +} +} diff --git a/libsolidity/formal/SymbolicVariable.cpp b/libsolidity/formal/SymbolicVariable.cpp index afbc01ba..18cf00dc 100644 --- a/libsolidity/formal/SymbolicVariable.cpp +++ b/libsolidity/formal/SymbolicVariable.cpp @@ -30,7 +30,8 @@ SymbolicVariable::SymbolicVariable( ): m_type(_type), m_uniqueName(_uniqueName), - m_interface(_interface) + m_interface(_interface), + m_ssa(make_shared()) { } diff --git a/libsolidity/formal/SymbolicVariable.h b/libsolidity/formal/SymbolicVariable.h index 977515f8..9ed5ce01 100644 --- a/libsolidity/formal/SymbolicVariable.h +++ b/libsolidity/formal/SymbolicVariable.h @@ -17,6 +17,8 @@ #pragma once +#include + #include #include @@ -43,25 +45,35 @@ public: ); virtual ~SymbolicVariable() = default; - smt::Expression operator()(int _seq) const + smt::Expression current() const { - return valueAtSequence(_seq); + return valueAtSequence(m_ssa->index()); } - std::string uniqueSymbol(int _seq) const; + virtual smt::Expression valueAtSequence(int _seq) const = 0; + + smt::Expression increase() + { + ++(*m_ssa); + return current(); + } + + 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; + virtual void setZeroValue() = 0; /// The unknown value is the full range of valid values, /// and that's sub-type dependent. - virtual void setUnknownValue(int _seq) = 0; + virtual void setUnknownValue() = 0; protected: - virtual smt::Expression valueAtSequence(int _seq) const = 0; + std::string uniqueSymbol(int _seq) const; Type const& m_type; std::string m_uniqueName; smt::SolverInterface& m_interface; + std::shared_ptr m_ssa = nullptr; }; } -- cgit