diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 631a9eee1..51b310ae8 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 95e01708a..376b73fdb 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 67a18540d..000000000 --- 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 3c9c379a6..000000000 --- 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 4d753c5c6..000000000 --- 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 438af2c68..000000000 --- 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.h b/libsolidity/formal/SymbolicIntVariable.h deleted file mode 100644 index a9e51b1b7..000000000 --- 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 7e5db7bd6..3eb1c1ce6 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 0887fa41a..dcdd9ea42 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 530564d28..000000000 --- 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/SymbolicIntVariable.cpp b/libsolidity/formal/SymbolicVariables.cpp similarity index 51% rename from libsolidity/formal/SymbolicIntVariable.cpp rename to libsolidity/formal/SymbolicVariables.cpp index a5939842b..85818ba07 100644 --- a/libsolidity/formal/SymbolicIntVariable.cpp +++ b/libsolidity/formal/SymbolicVariables.cpp @@ -15,14 +15,57 @@ along with solidity. If not, see . */ -#include +#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, @@ -50,3 +93,20 @@ void SymbolicIntVariable::setUnknownValue() 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/SymbolicVariable.h b/libsolidity/formal/SymbolicVariables.h similarity index 56% rename from libsolidity/formal/SymbolicVariable.h rename to libsolidity/formal/SymbolicVariables.h index e554139fc..4fd9b2451 100644 --- a/libsolidity/formal/SymbolicVariable.h +++ b/libsolidity/formal/SymbolicVariables.h @@ -33,7 +33,7 @@ namespace solidity class Type; /** - * This class represents the symbolic version of a program variable. + * This abstract class represents the symbolic version of a program variable. */ class SymbolicVariable { @@ -78,5 +78,72 @@ protected: 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 + ); +}; + } } diff --git a/test/libsolidity/smtCheckerTests/special/blockhash.sol b/test/libsolidity/smtCheckerTests/special/blockhash.sol index d0f263eb3..1c6939142 100644 --- a/test/libsolidity/smtCheckerTests/special/blockhash.sol +++ b/test/libsolidity/smtCheckerTests/special/blockhash.sol @@ -7,8 +7,4 @@ contract C } } // ---- -// Warning: (86-98): Assertion checker does not yet support this special variable. -// Warning: (86-98): Assertion checker does not yet implement this type. -// Warning: (86-102): Assertion checker does not yet implement the type bytes32 for comparisons -// Warning: (86-102): Internal error: Expression undefined for SMT solver. // Warning: (79-103): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/special/msg_sig.sol b/test/libsolidity/smtCheckerTests/special/msg_sig.sol index 6f8321791..109470a83 100644 --- a/test/libsolidity/smtCheckerTests/special/msg_sig.sol +++ b/test/libsolidity/smtCheckerTests/special/msg_sig.sol @@ -7,8 +7,4 @@ contract C } } // ---- -// Warning: (86-93): Assertion checker does not yet support this special variable. -// Warning: (86-93): Assertion checker does not yet implement this type. -// Warning: (86-107): Assertion checker does not yet implement the type bytes4 for comparisons -// Warning: (86-107): Internal error: Expression undefined for SMT solver. // Warning: (79-108): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/fixed_bytes_1.sol b/test/libsolidity/smtCheckerTests/types/fixed_bytes_1.sol new file mode 100644 index 000000000..541fff54e --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/fixed_bytes_1.sol @@ -0,0 +1,16 @@ +pragma experimental SMTChecker; + +contract C +{ + bytes32 x; + function f(bytes8 y) public view { + assert(x != y); + assert(x != g()); + } + function g() public view returns (bytes32) { + return x; + } +} +// ---- +// Warning: (96-110): Assertion violation happens here +// Warning: (114-130): Assertion violation happens here