From 07fac9e38173e7a2a8871ff2aa3c9b41f880f0da Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Fri, 12 Apr 2019 14:44:18 +0200 Subject: [PATCH] [SMTChecker] Allow SymbolicVariable from smt::Sort --- libsolidity/formal/SolverInterface.h | 1 + libsolidity/formal/SymbolicTypes.cpp | 2 + libsolidity/formal/SymbolicVariables.cpp | 58 +++++++++++++++--------- libsolidity/formal/SymbolicVariables.h | 26 +++++++---- 4 files changed, 57 insertions(+), 30 deletions(-) diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h index 042a16ab6..0c7f1dbdf 100644 --- a/libsolidity/formal/SolverInterface.h +++ b/libsolidity/formal/SolverInterface.h @@ -297,6 +297,7 @@ public: Expression newVariable(std::string _name, SortPointer _sort) { // Subclasses should do something here + solAssert(_sort, ""); declareVariable(_name, *_sort); return Expression(std::move(_name), {}, std::move(_sort)); } diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp index e72e22339..1497fa5e7 100644 --- a/libsolidity/formal/SymbolicTypes.cpp +++ b/libsolidity/formal/SymbolicTypes.cpp @@ -236,6 +236,7 @@ void dev::solidity::smt::setSymbolicZeroValue(SymbolicVariable const& _variable, void dev::solidity::smt::setSymbolicZeroValue(smt::Expression _expr, TypePointer const& _type, smt::SolverInterface& _interface) { + solAssert(_type, ""); if (isInteger(_type->category())) _interface.addAssertion(_expr == 0); else if (isBool(_type->category())) @@ -249,6 +250,7 @@ void dev::solidity::smt::setSymbolicUnknownValue(SymbolicVariable const& _variab void dev::solidity::smt::setSymbolicUnknownValue(smt::Expression _expr, TypePointer const& _type, smt::SolverInterface& _interface) { + solAssert(_type, ""); if (isEnum(_type->category())) { auto enumType = dynamic_cast(_type.get()); diff --git a/libsolidity/formal/SymbolicVariables.cpp b/libsolidity/formal/SymbolicVariables.cpp index bdc341c43..8196d95e9 100644 --- a/libsolidity/formal/SymbolicVariables.cpp +++ b/libsolidity/formal/SymbolicVariables.cpp @@ -26,14 +26,30 @@ using namespace dev::solidity; SymbolicVariable::SymbolicVariable( TypePointer _type, - string const& _uniqueName, + string _uniqueName, smt::SolverInterface& _interface ): m_type(move(_type)), - m_uniqueName(_uniqueName), + m_uniqueName(move(_uniqueName)), m_interface(_interface), m_ssa(make_shared()) { + solAssert(m_type, ""); + m_sort = smtSort(*m_type); + solAssert(m_sort, ""); +} + +SymbolicVariable::SymbolicVariable( + smt::SortPointer _sort, + string _uniqueName, + smt::SolverInterface& _interface +): + m_sort(move(_sort)), + m_uniqueName(move(_uniqueName)), + m_interface(_interface), + m_ssa(make_shared()) +{ + solAssert(m_sort, ""); } smt::Expression SymbolicVariable::currentValue() const @@ -48,7 +64,7 @@ string SymbolicVariable::currentName() const smt::Expression SymbolicVariable::valueAtIndex(int _index) const { - return m_interface.newVariable(uniqueSymbol(_index), smtSort(*m_type)); + return m_interface.newVariable(uniqueSymbol(_index), m_sort); } string SymbolicVariable::uniqueSymbol(unsigned _index) const @@ -64,55 +80,55 @@ smt::Expression SymbolicVariable::increaseIndex() SymbolicBoolVariable::SymbolicBoolVariable( TypePointer _type, - string const& _uniqueName, + string _uniqueName, smt::SolverInterface& _interface ): - SymbolicVariable(move(_type), _uniqueName, _interface) + SymbolicVariable(move(_type), move(_uniqueName), _interface) { solAssert(m_type->category() == Type::Category::Bool, ""); } SymbolicIntVariable::SymbolicIntVariable( TypePointer _type, - string const& _uniqueName, + string _uniqueName, smt::SolverInterface& _interface ): - SymbolicVariable(move(_type), _uniqueName, _interface) + SymbolicVariable(move(_type), move(_uniqueName), _interface) { solAssert(isNumber(m_type->category()), ""); } SymbolicAddressVariable::SymbolicAddressVariable( - string const& _uniqueName, + string _uniqueName, smt::SolverInterface& _interface ): - SymbolicIntVariable(make_shared(160), _uniqueName, _interface) + SymbolicIntVariable(make_shared(160), move(_uniqueName), _interface) { } SymbolicFixedBytesVariable::SymbolicFixedBytesVariable( unsigned _numBytes, - string const& _uniqueName, + string _uniqueName, smt::SolverInterface& _interface ): - SymbolicIntVariable(make_shared(_numBytes * 8), _uniqueName, _interface) + SymbolicIntVariable(make_shared(_numBytes * 8), move(_uniqueName), _interface) { } SymbolicFunctionVariable::SymbolicFunctionVariable( TypePointer _type, - string const& _uniqueName, + string _uniqueName, smt::SolverInterface& _interface ): - SymbolicVariable(move(_type), _uniqueName, _interface), - m_declaration(m_interface.newVariable(currentName(), smtSort(*m_type))) + SymbolicVariable(move(_type), move(_uniqueName), _interface), + m_declaration(m_interface.newVariable(currentName(), m_sort)) { solAssert(m_type->category() == Type::Category::Function, ""); } void SymbolicFunctionVariable::resetDeclaration() { - m_declaration = m_interface.newVariable(currentName(), smtSort(*m_type)); + m_declaration = m_interface.newVariable(currentName(), m_sort); } smt::Expression SymbolicFunctionVariable::increaseIndex() @@ -129,30 +145,30 @@ smt::Expression SymbolicFunctionVariable::operator()(vector _ar SymbolicMappingVariable::SymbolicMappingVariable( TypePointer _type, - string const& _uniqueName, + string _uniqueName, smt::SolverInterface& _interface ): - SymbolicVariable(move(_type), _uniqueName, _interface) + SymbolicVariable(move(_type), move(_uniqueName), _interface) { solAssert(isMapping(m_type->category()), ""); } SymbolicArrayVariable::SymbolicArrayVariable( TypePointer _type, - string const& _uniqueName, + string _uniqueName, smt::SolverInterface& _interface ): - SymbolicVariable(move(_type), _uniqueName, _interface) + SymbolicVariable(move(_type), move(_uniqueName), _interface) { solAssert(isArray(m_type->category()), ""); } SymbolicEnumVariable::SymbolicEnumVariable( TypePointer _type, - string const& _uniqueName, + string _uniqueName, smt::SolverInterface& _interface ): - SymbolicVariable(move(_type), _uniqueName, _interface) + SymbolicVariable(move(_type), move(_uniqueName), _interface) { solAssert(isEnum(m_type->category()), ""); } diff --git a/libsolidity/formal/SymbolicVariables.h b/libsolidity/formal/SymbolicVariables.h index 89df13f35..0c65a34a6 100644 --- a/libsolidity/formal/SymbolicVariables.h +++ b/libsolidity/formal/SymbolicVariables.h @@ -37,7 +37,12 @@ class SymbolicVariable public: SymbolicVariable( TypePointer _type, - std::string const& _uniqueName, + std::string _uniqueName, + smt::SolverInterface& _interface + ); + SymbolicVariable( + smt::SortPointer _sort, + std::string _uniqueName, smt::SolverInterface& _interface ); @@ -60,6 +65,9 @@ public: protected: std::string uniqueSymbol(unsigned _index) const; + /// SMT sort. + smt::SortPointer m_sort; + /// Solidity type, used for size and range in number types. TypePointer m_type; std::string m_uniqueName; smt::SolverInterface& m_interface; @@ -74,7 +82,7 @@ class SymbolicBoolVariable: public SymbolicVariable public: SymbolicBoolVariable( TypePointer _type, - std::string const& _uniqueName, + std::string _uniqueName, smt::SolverInterface& _interface ); }; @@ -87,7 +95,7 @@ class SymbolicIntVariable: public SymbolicVariable public: SymbolicIntVariable( TypePointer _type, - std::string const& _uniqueName, + std::string _uniqueName, smt::SolverInterface& _interface ); }; @@ -99,7 +107,7 @@ class SymbolicAddressVariable: public SymbolicIntVariable { public: SymbolicAddressVariable( - std::string const& _uniqueName, + std::string _uniqueName, smt::SolverInterface& _interface ); }; @@ -112,7 +120,7 @@ class SymbolicFixedBytesVariable: public SymbolicIntVariable public: SymbolicFixedBytesVariable( unsigned _numBytes, - std::string const& _uniqueName, + std::string _uniqueName, smt::SolverInterface& _interface ); }; @@ -125,7 +133,7 @@ class SymbolicFunctionVariable: public SymbolicVariable public: SymbolicFunctionVariable( TypePointer _type, - std::string const& _uniqueName, + std::string _uniqueName, smt::SolverInterface& _interface ); @@ -148,7 +156,7 @@ class SymbolicMappingVariable: public SymbolicVariable public: SymbolicMappingVariable( TypePointer _type, - std::string const& _uniqueName, + std::string _uniqueName, smt::SolverInterface& _interface ); }; @@ -161,7 +169,7 @@ class SymbolicArrayVariable: public SymbolicVariable public: SymbolicArrayVariable( TypePointer _type, - std::string const& _uniqueName, + std::string _uniqueName, smt::SolverInterface& _interface ); }; @@ -174,7 +182,7 @@ class SymbolicEnumVariable: public SymbolicVariable public: SymbolicEnumVariable( TypePointer _type, - std::string const& _uniqueName, + std::string _uniqueName, smt::SolverInterface& _interface ); };