From d8cbf321dafbe85f6fde07b5dd4ce7a3abffaeb6 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Mon, 22 Oct 2018 10:29:03 +0200 Subject: Grouping of symbolic variables in the same file and support to FixedBytes --- libsolidity/formal/SMTChecker.cpp | 2 - libsolidity/formal/SMTChecker.h | 2 +- libsolidity/formal/SymbolicAddressVariable.cpp | 40 ------- libsolidity/formal/SymbolicAddressVariable.h | 43 ------- libsolidity/formal/SymbolicBoolVariable.cpp | 46 -------- libsolidity/formal/SymbolicBoolVariable.h | 49 -------- libsolidity/formal/SymbolicIntVariable.cpp | 52 --------- libsolidity/formal/SymbolicIntVariable.h | 49 -------- libsolidity/formal/SymbolicTypes.cpp | 16 ++- libsolidity/formal/SymbolicTypes.h | 3 +- libsolidity/formal/SymbolicVariable.cpp | 43 ------- libsolidity/formal/SymbolicVariable.h | 82 -------------- libsolidity/formal/SymbolicVariables.cpp | 112 +++++++++++++++++++ libsolidity/formal/SymbolicVariables.h | 149 +++++++++++++++++++++++++ 14 files changed, 276 insertions(+), 412 deletions(-) delete mode 100644 libsolidity/formal/SymbolicAddressVariable.cpp delete mode 100644 libsolidity/formal/SymbolicAddressVariable.h delete mode 100644 libsolidity/formal/SymbolicBoolVariable.cpp delete mode 100644 libsolidity/formal/SymbolicBoolVariable.h delete mode 100644 libsolidity/formal/SymbolicIntVariable.cpp delete mode 100644 libsolidity/formal/SymbolicIntVariable.h delete mode 100644 libsolidity/formal/SymbolicVariable.cpp delete mode 100644 libsolidity/formal/SymbolicVariable.h create mode 100644 libsolidity/formal/SymbolicVariables.cpp create mode 100644 libsolidity/formal/SymbolicVariables.h (limited to 'libsolidity') diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 631a9eee..51b310ae 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -19,8 +19,6 @@ #include -#include -#include #include #include diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index 95e01708..376b73fd 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -19,7 +19,7 @@ #include -#include +#include #include diff --git a/libsolidity/formal/SymbolicAddressVariable.cpp b/libsolidity/formal/SymbolicAddressVariable.cpp deleted file mode 100644 index 67a18540..00000000 --- a/libsolidity/formal/SymbolicAddressVariable.cpp +++ /dev/null @@ -1,40 +0,0 @@ -/* - 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( - string const& _uniqueName, - smt::SolverInterface& _interface -): - SymbolicIntVariable(make_shared(160), _uniqueName, _interface) -{ -} - -void SymbolicAddressVariable::setUnknownValue() -{ - auto intType = dynamic_cast(m_type.get()); - solAssert(intType, ""); - m_interface.addAssertion(currentValue() >= minValue(*intType)); - m_interface.addAssertion(currentValue() <= maxValue(*intType)); -} diff --git a/libsolidity/formal/SymbolicAddressVariable.h b/libsolidity/formal/SymbolicAddressVariable.h deleted file mode 100644 index 3c9c379a..00000000 --- a/libsolidity/formal/SymbolicAddressVariable.h +++ /dev/null @@ -1,43 +0,0 @@ -/* - 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( - 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 deleted file mode 100644 index 4d753c5c..00000000 --- a/libsolidity/formal/SymbolicBoolVariable.cpp +++ /dev/null @@ -1,46 +0,0 @@ -/* - 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 - -using namespace std; -using namespace dev; -using namespace dev::solidity; - -SymbolicBoolVariable::SymbolicBoolVariable( - TypePointer _type, - string const& _uniqueName, - smt::SolverInterface&_interface -): - SymbolicVariable(move(_type), _uniqueName, _interface) -{ - solAssert(m_type->category() == Type::Category::Bool, ""); -} - -smt::Expression SymbolicBoolVariable::valueAtIndex(int _index) const -{ - return m_interface.newBool(uniqueSymbol(_index)); -} - -void SymbolicBoolVariable::setZeroValue() -{ - m_interface.addAssertion(currentValue() == smt::Expression(false)); -} - -void SymbolicBoolVariable::setUnknownValue() -{ -} diff --git a/libsolidity/formal/SymbolicBoolVariable.h b/libsolidity/formal/SymbolicBoolVariable.h deleted file mode 100644 index 438af2c6..00000000 --- a/libsolidity/formal/SymbolicBoolVariable.h +++ /dev/null @@ -1,49 +0,0 @@ -/* - 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 Bool - */ -class SymbolicBoolVariable: public SymbolicVariable -{ -public: - SymbolicBoolVariable( - TypePointer _type, - std::string const& _uniqueName, - smt::SolverInterface& _interface - ); - - /// Sets the var to false. - void setZeroValue(); - /// Does nothing since the SMT solver already knows the valid values for Bool. - void setUnknownValue(); - -protected: - smt::Expression valueAtIndex(int _index) const; -}; - -} -} diff --git a/libsolidity/formal/SymbolicIntVariable.cpp b/libsolidity/formal/SymbolicIntVariable.cpp deleted file mode 100644 index a5939842..00000000 --- a/libsolidity/formal/SymbolicIntVariable.cpp +++ /dev/null @@ -1,52 +0,0 @@ -/* - 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; - -SymbolicIntVariable::SymbolicIntVariable( - TypePointer _type, - string const& _uniqueName, - smt::SolverInterface& _interface -): - SymbolicVariable(move(_type), _uniqueName, _interface) -{ - solAssert(isNumber(m_type->category()), ""); -} - -smt::Expression SymbolicIntVariable::valueAtIndex(int _index) const -{ - return m_interface.newInteger(uniqueSymbol(_index)); -} - -void SymbolicIntVariable::setZeroValue() -{ - m_interface.addAssertion(currentValue() == 0); -} - -void SymbolicIntVariable::setUnknownValue() -{ - auto intType = dynamic_cast(m_type.get()); - 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 deleted file mode 100644 index a9e51b1b..00000000 --- a/libsolidity/formal/SymbolicIntVariable.h +++ /dev/null @@ -1,49 +0,0 @@ -/* - 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 Integers - */ -class SymbolicIntVariable: public SymbolicVariable -{ -public: - SymbolicIntVariable( - TypePointer _type, - std::string const& _uniqueName, - smt::SolverInterface& _interface - ); - - /// Sets the var to 0. - void setZeroValue(); - /// Sets the variable to the full valid value range. - virtual void setUnknownValue(); - -protected: - smt::Expression valueAtIndex(int _index) const; -}; - -} -} diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp index 7e5db7bd..3eb1c1ce 100644 --- a/libsolidity/formal/SymbolicTypes.cpp +++ b/libsolidity/formal/SymbolicTypes.cpp @@ -17,10 +17,6 @@ #include -#include -#include -#include - #include #include @@ -55,6 +51,12 @@ pair> dev::solidity::newSymbolicVariable( var = make_shared(make_shared(256), _uniqueName, _solver); else if (isInteger(_type.category())) var = make_shared(type, _uniqueName, _solver); + else if (isFixedBytes(_type.category())) + { + auto fixedBytesType = dynamic_cast(type.get()); + solAssert(fixedBytesType, ""); + var = make_shared(fixedBytesType->numBytes(), _uniqueName, _solver); + } else if (isAddress(_type.category())) var = make_shared(_uniqueName, _solver); else if (isRational(_type.category())) @@ -86,6 +88,11 @@ bool dev::solidity::isRational(Type::Category _category) return _category == Type::Category::RationalNumber; } +bool dev::solidity::isFixedBytes(Type::Category _category) +{ + return _category == Type::Category::FixedBytes; +} + bool dev::solidity::isAddress(Type::Category _category) { return _category == Type::Category::Address; @@ -95,6 +102,7 @@ bool dev::solidity::isNumber(Type::Category _category) { return isInteger(_category) || isRational(_category) || + isFixedBytes(_category) || isAddress(_category); } diff --git a/libsolidity/formal/SymbolicTypes.h b/libsolidity/formal/SymbolicTypes.h index 0887fa41..dcdd9ea4 100644 --- a/libsolidity/formal/SymbolicTypes.h +++ b/libsolidity/formal/SymbolicTypes.h @@ -18,7 +18,7 @@ #pragma once #include -#include +#include #include #include @@ -35,6 +35,7 @@ bool isSupportedType(Type const& _type); bool isInteger(Type::Category _category); bool isRational(Type::Category _category); +bool isFixedBytes(Type::Category _category); bool isAddress(Type::Category _category); bool isNumber(Type::Category _category); bool isBool(Type::Category _category); diff --git a/libsolidity/formal/SymbolicVariable.cpp b/libsolidity/formal/SymbolicVariable.cpp deleted file mode 100644 index 530564d2..00000000 --- a/libsolidity/formal/SymbolicVariable.cpp +++ /dev/null @@ -1,43 +0,0 @@ -/* - 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; - -SymbolicVariable::SymbolicVariable( - TypePointer _type, - string const& _uniqueName, - smt::SolverInterface& _interface -): - m_type(move(_type)), - m_uniqueName(_uniqueName), - m_interface(_interface), - m_ssa(make_shared()) -{ -} - -string SymbolicVariable::uniqueSymbol(unsigned _index) const -{ - return m_uniqueName + "_" + to_string(_index); -} - - diff --git a/libsolidity/formal/SymbolicVariable.h b/libsolidity/formal/SymbolicVariable.h deleted file mode 100644 index e554139f..00000000 --- a/libsolidity/formal/SymbolicVariable.h +++ /dev/null @@ -1,82 +0,0 @@ -/* - 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 -{ - -class Type; - -/** - * This class represents the symbolic version of a program variable. - */ -class SymbolicVariable -{ -public: - SymbolicVariable( - TypePointer _type, - std::string const& _uniqueName, - smt::SolverInterface& _interface - ); - - virtual ~SymbolicVariable() = default; - - smt::Expression currentValue() const - { - return valueAtIndex(m_ssa->index()); - } - - virtual smt::Expression valueAtIndex(int _index) const = 0; - - smt::Expression increaseIndex() - { - ++(*m_ssa); - return currentValue(); - } - - unsigned index() const { return m_ssa->index(); } - unsigned& 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. - /// It is sub-type dependent, but not mandatory. - virtual void setUnknownValue() {} - -protected: - std::string uniqueSymbol(unsigned _index) const; - - TypePointer m_type = nullptr; - std::string m_uniqueName; - smt::SolverInterface& m_interface; - std::shared_ptr m_ssa = nullptr; -}; - -} -} diff --git a/libsolidity/formal/SymbolicVariables.cpp b/libsolidity/formal/SymbolicVariables.cpp new file mode 100644 index 00000000..85818ba0 --- /dev/null +++ b/libsolidity/formal/SymbolicVariables.cpp @@ -0,0 +1,112 @@ +/* + 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 + +using namespace std; +using namespace dev; +using namespace dev::solidity; + +SymbolicVariable::SymbolicVariable( + TypePointer _type, + string const& _uniqueName, + smt::SolverInterface& _interface +): + m_type(move(_type)), + m_uniqueName(_uniqueName), + m_interface(_interface), + m_ssa(make_shared()) +{ +} + +string SymbolicVariable::uniqueSymbol(unsigned _index) const +{ + return m_uniqueName + "_" + to_string(_index); +} + +SymbolicBoolVariable::SymbolicBoolVariable( + TypePointer _type, + string const& _uniqueName, + smt::SolverInterface&_interface +): + SymbolicVariable(move(_type), _uniqueName, _interface) +{ + solAssert(m_type->category() == Type::Category::Bool, ""); +} + +smt::Expression SymbolicBoolVariable::valueAtIndex(int _index) const +{ + return m_interface.newBool(uniqueSymbol(_index)); +} + +void SymbolicBoolVariable::setZeroValue() +{ + m_interface.addAssertion(currentValue() == smt::Expression(false)); +} + +void SymbolicBoolVariable::setUnknownValue() +{ +} + +SymbolicIntVariable::SymbolicIntVariable( + TypePointer _type, + string const& _uniqueName, + smt::SolverInterface& _interface +): + SymbolicVariable(move(_type), _uniqueName, _interface) +{ + solAssert(isNumber(m_type->category()), ""); +} + +smt::Expression SymbolicIntVariable::valueAtIndex(int _index) const +{ + return m_interface.newInteger(uniqueSymbol(_index)); +} + +void SymbolicIntVariable::setZeroValue() +{ + m_interface.addAssertion(currentValue() == 0); +} + +void SymbolicIntVariable::setUnknownValue() +{ + auto intType = dynamic_cast(m_type.get()); + solAssert(intType, ""); + m_interface.addAssertion(currentValue() >= minValue(*intType)); + m_interface.addAssertion(currentValue() <= maxValue(*intType)); +} + +SymbolicAddressVariable::SymbolicAddressVariable( + string const& _uniqueName, + smt::SolverInterface& _interface +): + SymbolicIntVariable(make_shared(160), _uniqueName, _interface) +{ +} + +SymbolicFixedBytesVariable::SymbolicFixedBytesVariable( + unsigned _numBytes, + string const& _uniqueName, + smt::SolverInterface& _interface +): + SymbolicIntVariable(make_shared(_numBytes * 8), _uniqueName, _interface) +{ +} diff --git a/libsolidity/formal/SymbolicVariables.h b/libsolidity/formal/SymbolicVariables.h new file mode 100644 index 00000000..4fd9b245 --- /dev/null +++ b/libsolidity/formal/SymbolicVariables.h @@ -0,0 +1,149 @@ +/* + 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 +{ + +class Type; + +/** + * This abstract class represents the symbolic version of a program variable. + */ +class SymbolicVariable +{ +public: + SymbolicVariable( + TypePointer _type, + std::string const& _uniqueName, + smt::SolverInterface& _interface + ); + + virtual ~SymbolicVariable() = default; + + smt::Expression currentValue() const + { + return valueAtIndex(m_ssa->index()); + } + + virtual smt::Expression valueAtIndex(int _index) const = 0; + + smt::Expression increaseIndex() + { + ++(*m_ssa); + return currentValue(); + } + + unsigned index() const { return m_ssa->index(); } + unsigned& 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. + /// It is sub-type dependent, but not mandatory. + virtual void setUnknownValue() {} + +protected: + std::string uniqueSymbol(unsigned _index) const; + + TypePointer m_type = nullptr; + std::string m_uniqueName; + smt::SolverInterface& m_interface; + std::shared_ptr m_ssa = nullptr; +}; + +/** + * Specialization of SymbolicVariable for Bool + */ +class SymbolicBoolVariable: public SymbolicVariable +{ +public: + SymbolicBoolVariable( + TypePointer _type, + std::string const& _uniqueName, + smt::SolverInterface& _interface + ); + + /// Sets the var to false. + void setZeroValue(); + /// Does nothing since the SMT solver already knows the valid values for Bool. + void setUnknownValue(); + +protected: + smt::Expression valueAtIndex(int _index) const; +}; + +/** + * Specialization of SymbolicVariable for Integers + */ +class SymbolicIntVariable: public SymbolicVariable +{ +public: + SymbolicIntVariable( + TypePointer _type, + std::string const& _uniqueName, + smt::SolverInterface& _interface + ); + + /// Sets the var to 0. + void setZeroValue(); + /// Sets the variable to the full valid value range. + void setUnknownValue(); + +protected: + smt::Expression valueAtIndex(int _index) const; +}; + +/** + * Specialization of SymbolicVariable for Address + */ +class SymbolicAddressVariable: public SymbolicIntVariable +{ +public: + SymbolicAddressVariable( + std::string const& _uniqueName, + smt::SolverInterface& _interface + ); +}; + +/** + * Specialization of SymbolicVariable for FixedBytes + */ +class SymbolicFixedBytesVariable: public SymbolicIntVariable +{ +public: + SymbolicFixedBytesVariable( + unsigned _numBytes, + std::string const& _uniqueName, + smt::SolverInterface& _interface + ); +}; + +} +} -- cgit