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