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 (limited to 'libsolidity/formal') 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 From aa23326e06b00ecbaab032d333a15b28f5aa71d7 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Wed, 17 Oct 2018 11:32:01 +0200 Subject: Consistent renaming of 'counters' and 'sequence' to 'index' --- libsolidity/formal/SMTChecker.cpp | 58 ++++++++++++++--------------- libsolidity/formal/SMTChecker.h | 26 ++++++------- libsolidity/formal/SSAVariable.cpp | 6 +-- libsolidity/formal/SSAVariable.h | 12 +++--- libsolidity/formal/SymbolicBoolVariable.cpp | 6 +-- libsolidity/formal/SymbolicBoolVariable.h | 2 +- libsolidity/formal/SymbolicIntVariable.cpp | 14 +++---- libsolidity/formal/SymbolicIntVariable.h | 2 +- libsolidity/formal/SymbolicVariable.cpp | 4 +- libsolidity/formal/SymbolicVariable.h | 12 +++--- 10 files changed, 71 insertions(+), 71 deletions(-) (limited to 'libsolidity/formal') diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index d84d6794..8787d25a 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -108,18 +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 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 = copyVariableSequenceCounters(); + indicesEndFalse = copyVariableIndices(); - mergeVariables(touchedVariables, expr(_node.condition()), countersEndTrue, countersEndFalse); + mergeVariables(touchedVariables, expr(_node.condition()), indicesEndTrue, indicesEndFalse); return false; } @@ -646,22 +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) { - auto countersBeforeBranch = copyVariableSequenceCounters(); + auto indicesBeforeBranch = copyVariableIndices(); if (_condition) pushPathCondition(*_condition); _statement.accept(*this); if (_condition) popPathCondition(); - auto countersAfterBranch = copyVariableSequenceCounters(); - resetVariableCounters(countersBeforeBranch); - return countersAfterBranch; + auto indicesAfterBranch = copyVariableIndices(); + resetVariableIndices(indicesBeforeBranch); + return indicesAfterBranch; } void SMTChecker::checkCondition( @@ -894,19 +894,19 @@ void SMTChecker::resetVariables(vector _variables) } } -void SMTChecker::mergeVariables(vector const& _variables, smt::Expression const& _condition, VariableSequenceCounters const& _countersEndTrue, VariableSequenceCounters const& _countersEndFalse) +void SMTChecker::mergeVariables(vector const& _variables, smt::Expression const& _condition, VariableIndices const& _indicesEndTrue, VariableIndices const& _indicesEndFalse) { set uniqueVars(_variables.begin(), _variables.end()); for (auto const* decl: uniqueVars) { - solAssert(_countersEndTrue.count(decl) && _countersEndFalse.count(decl), ""); - int trueCounter = _countersEndTrue.at(decl); - int falseCounter = _countersEndFalse.at(decl); - 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)) ); } } @@ -946,19 +946,19 @@ bool SMTChecker::knownVariable(VariableDeclaration const& _decl) smt::Expression SMTChecker::currentValue(VariableDeclaration const& _decl) { solAssert(knownVariable(_decl), ""); - return m_variables.at(&_decl)->current(); + 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)->valueAtSequence(_sequence); + return m_variables.at(&_decl)->valueAtIndex(_index); } smt::Expression SMTChecker::newValue(VariableDeclaration const& _decl) { solAssert(knownVariable(_decl), ""); - return m_variables.at(&_decl)->increase(); + return m_variables.at(&_decl)->increaseIndex(); } void SMTChecker::setZeroValue(VariableDeclaration const& _decl) @@ -1070,16 +1070,16 @@ bool SMTChecker::visitedFunction(FunctionDefinition const* _funDef) return contains(m_functionPath, _funDef); } -SMTChecker::VariableSequenceCounters SMTChecker::copyVariableSequenceCounters() +SMTChecker::VariableIndices SMTChecker::copyVariableIndices() { - VariableSequenceCounters counters; - for (auto var: m_variables) - counters.emplace(var.first, var.second->index()); - return counters; + VariableIndices indices; + for (auto const& var: m_variables) + indices.emplace(var.first, var.second->index()); + return indices; } -void SMTChecker::resetVariableCounters(VariableSequenceCounters const& _counters) +void SMTChecker::resetVariableIndices(VariableIndices const& _indices) { - for (auto var: _counters) + 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 ae697204..0b078556 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -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::unordered_map; + using VariableIndices = 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. - /// @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 const& _variables, smt::Expression const& _condition, VariableSequenceCounters const& _countersEndTrue, VariableSequenceCounters const& _countersEndFalse); + void mergeVariables(std::vector 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. @@ -177,9 +177,9 @@ private: bool hasVariable(VariableDeclaration const& _e) const; /// Copy the SSA indices of m_variables. - VariableSequenceCounters copyVariableSequenceCounters(); - /// Resets the variable counters. - void resetVariableCounters(VariableSequenceCounters const& _counters); + VariableIndices copyVariableIndices(); + /// Resets the variable indices. + void resetVariableIndices(VariableIndices const& _indices); std::shared_ptr m_interface; std::shared_ptr m_variableUsage; diff --git a/libsolidity/formal/SSAVariable.cpp b/libsolidity/formal/SSAVariable.cpp index aeb12c9f..dbc58664 100644 --- a/libsolidity/formal/SSAVariable.cpp +++ b/libsolidity/formal/SSAVariable.cpp @@ -27,7 +27,7 @@ SSAVariable::SSAVariable() void SSAVariable::resetIndex() { - m_currentSequenceCounter = 0; - m_nextFreeSequenceCounter.reset (new int); - *m_nextFreeSequenceCounter = 1; + m_currentIndex = 0; + m_nextFreeIndex.reset (new int); + *m_nextFreeIndex = 1; } diff --git a/libsolidity/formal/SSAVariable.h b/libsolidity/formal/SSAVariable.h index f8317b79..d357740d 100644 --- a/libsolidity/formal/SSAVariable.h +++ b/libsolidity/formal/SSAVariable.h @@ -34,19 +34,19 @@ public: void resetIndex(); /// This function returns the current index of this SSA variable. - int index() const { return m_currentSequenceCounter; } - int& index() { return m_currentSequenceCounter; } + int index() const { return m_currentIndex; } + int& index() { return m_currentIndex; } int operator++() { - return m_currentSequenceCounter = (*m_nextFreeSequenceCounter)++; + return m_currentIndex = (*m_nextFreeIndex)++; } private: - 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 m_nextFreeSequenceCounter; + std::shared_ptr m_nextFreeIndex; }; } diff --git a/libsolidity/formal/SymbolicBoolVariable.cpp b/libsolidity/formal/SymbolicBoolVariable.cpp index f65ecd37..9c41ca9d 100644 --- a/libsolidity/formal/SymbolicBoolVariable.cpp +++ b/libsolidity/formal/SymbolicBoolVariable.cpp @@ -31,14 +31,14 @@ 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() { - m_interface.addAssertion(current() == smt::Expression(false)); + m_interface.addAssertion(currentValue() == smt::Expression(false)); } void SymbolicBoolVariable::setUnknownValue() diff --git a/libsolidity/formal/SymbolicBoolVariable.h b/libsolidity/formal/SymbolicBoolVariable.h index 3d735889..85e41b3b 100644 --- a/libsolidity/formal/SymbolicBoolVariable.h +++ b/libsolidity/formal/SymbolicBoolVariable.h @@ -42,7 +42,7 @@ public: 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 877495bd..d75275c6 100644 --- a/libsolidity/formal/SymbolicIntVariable.cpp +++ b/libsolidity/formal/SymbolicIntVariable.cpp @@ -35,14 +35,14 @@ SymbolicIntVariable::SymbolicIntVariable( ); } -smt::Expression SymbolicIntVariable::valueAtSequence(int _seq) const +smt::Expression SymbolicIntVariable::valueAtIndex(int _index) const { - return m_interface.newInteger(uniqueSymbol(_seq)); + return m_interface.newInteger(uniqueSymbol(_index)); } void SymbolicIntVariable::setZeroValue() { - m_interface.addAssertion(current() == 0); + m_interface.addAssertion(currentValue() == 0); } void SymbolicIntVariable::setUnknownValue() @@ -51,15 +51,15 @@ void SymbolicIntVariable::setUnknownValue() { auto intType = dynamic_cast(&m_type); solAssert(intType, ""); - m_interface.addAssertion(current() >= minValue(*intType)); - m_interface.addAssertion(current() <= maxValue(*intType)); + m_interface.addAssertion(currentValue() >= minValue(*intType)); + m_interface.addAssertion(currentValue() <= maxValue(*intType)); } else { solAssert(m_type.category() == Type::Category::Address, ""); IntegerType addrType{160}; - m_interface.addAssertion(current() >= minValue(addrType)); - m_interface.addAssertion(current() <= maxValue(addrType)); + m_interface.addAssertion(currentValue() >= minValue(addrType)); + m_interface.addAssertion(currentValue() <= maxValue(addrType)); } } diff --git a/libsolidity/formal/SymbolicIntVariable.h b/libsolidity/formal/SymbolicIntVariable.h index 3b0c0311..d0ac3888 100644 --- a/libsolidity/formal/SymbolicIntVariable.h +++ b/libsolidity/formal/SymbolicIntVariable.h @@ -45,7 +45,7 @@ public: static smt::Expression maxValue(IntegerType const& _t); protected: - smt::Expression valueAtSequence(int _seq) const; + smt::Expression valueAtIndex(int _index) const; }; } diff --git a/libsolidity/formal/SymbolicVariable.cpp b/libsolidity/formal/SymbolicVariable.cpp index 18cf00dc..c042ec48 100644 --- a/libsolidity/formal/SymbolicVariable.cpp +++ b/libsolidity/formal/SymbolicVariable.cpp @@ -35,9 +35,9 @@ SymbolicVariable::SymbolicVariable( { } -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 9ed5ce01..215c9ac1 100644 --- a/libsolidity/formal/SymbolicVariable.h +++ b/libsolidity/formal/SymbolicVariable.h @@ -45,17 +45,17 @@ public: ); virtual ~SymbolicVariable() = default; - smt::Expression current() const + smt::Expression currentValue() const { - return valueAtSequence(m_ssa->index()); + return valueAtIndex(m_ssa->index()); } - virtual smt::Expression valueAtSequence(int _seq) const = 0; + virtual smt::Expression valueAtIndex(int _index) const = 0; - smt::Expression increase() + smt::Expression increaseIndex() { ++(*m_ssa); - return current(); + return currentValue(); } int index() const { return m_ssa->index(); } @@ -68,7 +68,7 @@ public: virtual void setUnknownValue() = 0; protected: - std::string uniqueSymbol(int _seq) const; + std::string uniqueSymbol(int _index) const; Type const& m_type; std::string m_uniqueName; -- cgit From afe83cc28b2b0f31a00911ed0b540e1beb038736 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Wed, 17 Oct 2018 15:56:44 +0200 Subject: Refactor SymbolicAddressVariable and SymbolicVariable allocation --- libsolidity/formal/SMTChecker.cpp | 6 +-- libsolidity/formal/SymbolicAddressVariable.cpp | 41 +++++++++++++++++ libsolidity/formal/SymbolicAddressVariable.h | 44 ++++++++++++++++++ libsolidity/formal/SymbolicIntVariable.cpp | 36 +++------------ libsolidity/formal/SymbolicIntVariable.h | 5 +-- libsolidity/formal/SymbolicTypes.cpp | 62 +++++++++++++++++++++----- libsolidity/formal/SymbolicTypes.h | 9 ++++ libsolidity/formal/SymbolicVariable.h | 7 +-- 8 files changed, 159 insertions(+), 51 deletions(-) create mode 100644 libsolidity/formal/SymbolicAddressVariable.cpp create mode 100644 libsolidity/formal/SymbolicAddressVariable.h (limited to 'libsolidity/formal') diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 8787d25a..671c2049 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -257,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()) + ")", "", &_value ); checkCondition( - _value > SymbolicIntVariable::maxValue(_type), + _value > maxValue(_type), _location, "Overflow (resulting value larger than " + formatNumber(_type.maxValue()) + ")", "", @@ -570,7 +570,7 @@ void SMTChecker::compareOperation(BinaryOperation const& _op) smt::Expression right(expr(_op.rightExpression())); Token::Value op = _op.getOperator(); shared_ptr value; - if (isInteger(_op.annotation().commonType->category())) + if (isNumber(_op.annotation().commonType->category())) { value = make_shared( op == Token::Equal ? (left == right) : 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 . +*/ + +#include + +#include + +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 . +*/ + +#pragma once + +#include + +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/SymbolicIntVariable.cpp b/libsolidity/formal/SymbolicIntVariable.cpp index d75275c6..cf1a7486 100644 --- a/libsolidity/formal/SymbolicIntVariable.cpp +++ b/libsolidity/formal/SymbolicIntVariable.cpp @@ -17,6 +17,8 @@ #include +#include + using namespace std; using namespace dev; using namespace dev::solidity; @@ -28,11 +30,7 @@ SymbolicIntVariable::SymbolicIntVariable( ): SymbolicVariable(_type, _uniqueName, _interface) { - solAssert( - _type.category() == Type::Category::Integer || - _type.category() == Type::Category::Address, - "" - ); + solAssert(isNumber(_type.category()), ""); } smt::Expression SymbolicIntVariable::valueAtIndex(int _index) const @@ -47,28 +45,8 @@ void SymbolicIntVariable::setZeroValue() void SymbolicIntVariable::setUnknownValue() { - if (m_type.category() == Type::Category::Integer) - { - auto intType = dynamic_cast(&m_type); - solAssert(intType, ""); - m_interface.addAssertion(currentValue() >= minValue(*intType)); - m_interface.addAssertion(currentValue() <= maxValue(*intType)); - } - else - { - solAssert(m_type.category() == Type::Category::Address, ""); - IntegerType addrType{160}; - m_interface.addAssertion(currentValue() >= minValue(addrType)); - m_interface.addAssertion(currentValue() <= maxValue(addrType)); - } -} - -smt::Expression SymbolicIntVariable::minValue(IntegerType const& _t) -{ - return smt::Expression(_t.minValue()); -} - -smt::Expression SymbolicIntVariable::maxValue(IntegerType const& _t) -{ - return smt::Expression(_t.maxValue()); + auto intType = dynamic_cast(&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 d0ac3888..110ebb09 100644 --- a/libsolidity/formal/SymbolicIntVariable.h +++ b/libsolidity/formal/SymbolicIntVariable.h @@ -39,10 +39,7 @@ public: /// Sets the var to 0. void setZeroValue(); /// Sets the variable to the full valid value range. - void setUnknownValue(); - - static smt::Expression minValue(IntegerType const& _t); - static smt::Expression maxValue(IntegerType const& _t); + virtual void setUnknownValue(); protected: smt::Expression valueAtIndex(int _index) const; diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp index deb52ac1..2d993865 100644 --- a/libsolidity/formal/SymbolicTypes.cpp +++ b/libsolidity/formal/SymbolicTypes.cpp @@ -19,6 +19,7 @@ #include #include +#include #include @@ -29,7 +30,27 @@ using namespace dev::solidity; bool dev::solidity::isSupportedType(Type::Category _category) { - return isInteger(_category) || isBool(_category); + return isInteger(_category) || + isAddress(_category) || + isBool(_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 if (isAddress(_type.category())) + return make_shared(_type, _uniqueName, _solver); + else + solAssert(false, ""); } bool dev::solidity::isSupportedType(Type const& _type) @@ -39,7 +60,7 @@ bool dev::solidity::isSupportedType(Type const& _type) bool dev::solidity::isInteger(Type::Category _category) { - return _category == Type::Category::Integer || _category == Type::Category::Address; + return _category == Type::Category::Integer; } bool dev::solidity::isInteger(Type const& _type) @@ -47,6 +68,27 @@ 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; @@ -57,16 +99,12 @@ 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) +smt::Expression dev::solidity::minValue(IntegerType const& _type) { - 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, ""); + 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 index f9df6853..77822fed 100644 --- a/libsolidity/formal/SymbolicTypes.h +++ b/libsolidity/formal/SymbolicTypes.h @@ -36,10 +36,19 @@ 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 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.h b/libsolidity/formal/SymbolicVariable.h index 215c9ac1..417e1f92 100644 --- a/libsolidity/formal/SymbolicVariable.h +++ b/libsolidity/formal/SymbolicVariable.h @@ -62,10 +62,11 @@ public: int& index() { return m_ssa->index(); } /// Sets the var to the default value of its type. + /// Inherited types must implement. virtual void setZeroValue() = 0; - /// The unknown value is the full range of valid values, - /// and that's sub-type dependent. - virtual void setUnknownValue() = 0; + /// The unknown value is the full range of valid values. + /// It is sub-type dependent, but not mandatory. + virtual void setUnknownValue() {} protected: std::string uniqueSymbol(int _index) const; -- cgit